在Z3中将一个字转换成一组字节

Question

我正在Z3/Python中运行以下测试：

def test_converting_word_into_byte_array():
    bytes_in_word = 4
    word_size = 8 * bytes_in_word
    word = BitVec('word', word_size)
    word_in_bytes = Array('bytes(word)', BitVecSort(word_size), BitVecSort(8))
    read = BitVec('read', word_size)
    pointer = BitVecVal(0, word_size)
    answer_array = Array('final(word)', BitVecSort(word_size), BitVecSort(8))

    solver = Solver()
    solver.add(word == BitVecVal(2, word_size))
    for byte in range(bytes_in_word):
        solver.add(Select(word_in_bytes, byte) == Extract(word_size - 1 - 8 * byte, word_size - 1 - 7 - 8 * byte, word))
    new_array = Lambda([read],
        If(
            And(ULE(pointer, read), ULE(read, pointer + bytes_in_word - 1)),
            Select(word_in_bytes, read - pointer),
            Select(K(BitVecSort(word_size), BitVecVal(0, 8)), read)))
    solver.add(answer_array == new_array)

    assert str(solver.check()) == "sat"
    print(solver.model())

虽然解决方案令人满意，但最终解算器模型似乎是错误的：

[final(word) = Lambda(k!0, 2),
 bytes(word) = Lambda(k!0, If(k!0 == 3, 2, 0)),
 word = 2]

问题

由于If条件的设置，当2的值应该等价于bytes(word)时，为什么final(word)要取2的值？你知道吗

Answer 1

在程序中使用数组作为lambda。Lambda不是官方SMTLib语言（http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf）的一部分，因此很难说这是否应该被允许，以及后果如何。但是，正如您所发现的，这似乎是一个受支持的z3扩展，并且您发现了一个bug！你知道吗

请在他们的问题站点https://github.com/Z3Prover/z3/issues报告。你知道吗

注意。Python编码确实把这个问题混为一谈，使它很难阅读。以下是我创建的一个更易于阅读的SMTLib基准测试：

(set-logic ALL)

(declare-fun inp () (Array Int Int))
(declare-fun out () (Array Int Int))

(assert (= (select inp 0) 0))
(assert (= (select inp 1) 0))
(assert (= (select inp 2) 1))

(assert (= out (lambda ((i Int))
                       (ite (and (<= 0 i) (<= i 2))
                            (select inp i)
                            0))))

(check-sat)

(get-value ((select inp 0)))
(get-value ((select inp 1)))
(get-value ((select inp 2)))
(get-value ((select out 0)))
(get-value ((select out 1)))
(get-value ((select out 2)))

为此，z3报告：

sat
(((select inp 0) 0))
(((select inp 1) 0))
(((select inp 2) 1))
(((select out 0) 2))
(((select out 1) 2))
(((select out 2) 2))

但很明显，我们期望在0-2范围内等价。我强烈建议您报告这个SMTLib版本的问题，而不是原始的Python。你知道吗

注意。lambda和数组的混合绝对是Z3的扩展。例如，这就是CVC4在基准测试中所说的：

(error "Subexpressions must have a common base type:
Equation: (= out (lambda ((i Int)) (ite (and (<= 0 i) (<= i 2)) (select inp i) 0)))
Type 1: (Array Int Int)
Type 2: (-> Int Int)
")

所以，你使用的是一个特定于z3的扩展。虽然这不是一件坏事，但必须牢记在心。你知道吗