在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]

题

为什么final(word)接受2的值，因为bytes(word)条件是如何设置的，它应该等于If？

Answer 1

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

请在他们的问题网站上报告：https://github.com/Z3Prover/z3/issues。

NB。 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。

NB。 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的扩展。虽然这不是一件坏事，但要记住这一点。