如何在 Z3-PY 中实现 C 位运算符?

Question

我希望能够对我的Solver实现以下规则，其中"^"和"&"运算符是C中的"or"和"and"。input_list是一个 100 元素IntVector：

s.add(
((input_list[6] ^ input_list[10]) & 0xF) +
((input_list[3] + input_list[5] - 25) ^ (3*input_list[99])) == 73)

运行此代码会给出类型错误：

TypeError: unsupported operand type(s) for ^: 'ArithRef' and 'ArithRef'

将"^"和"&"替换为 Z3 的布尔运算符，如下所示：

s.add(
(And(Or(input_list[6],input_list[10]),0xF) +
Or((input_list[3] + input_list[5] - 25), (3*input_list[99]))) == 73)

给出此错误：

z3.z3types.Z3Exception: b'Sort mismatch at argument #1 for function (declare-fun or (Bool Bool) Bool) supplied sort is Int'

如何将此操作表示为 z3 求解器的规则？

Answer 1

这里的问题是 SMTLib(和 z3(中的Int类型是一个成熟的数学整数。它没有任何"位"，也不受任何限制。也就是说，它不是您可以对其执行按位操作的东西。您尚未提供实际的完全可执行代码，但这里有一个更简单的示例来说明您遇到的错误：

from z3 import *
x, y = Ints('x y')
s = Solver()
s.add(x ^ y == 0)
print(s.check())
print(s.model())

对于上面的代码，我得到：

Traceback (most recent call last):
File "a.py", line 6, in <module>
s.add(x ^ y == 0)
TypeError: unsupported operand type(s) for ^: 'ArithRef' and 'ArithRef'

(列表或向量等与这个问题无关;所以我省略了它们。

在 C 中，当您使用int类型时，它实际上指的是一个机器整数，即它具有固定宽度。在大多数计算机上通常为 64 位，但这取决于您使用的体系结构。因此，要在 z3 中执行相同的操作，您必须使用所谓的位向量，并准确指定您希望这些位向量有多宽。

下面是相同的代码，但这次使用 32 位机器算术：

from z3 import *
x, y = BitVecs('x y', 32)
s = Solver()
s.add(x ^ y == 0)
print(s.check())
print(s.model())

现在我得到：

sat
[y = 0, x = 0]

您可以在此处阅读有关 z3 中位精确算术的更多信息：https://ericpony.github.io/z3py-tutorial/guide-examples.htm