时间戳

首页 > 解决方案 > 我将如何在 Z3-PY 中实现 C 位运算符？

c - 我将如何在 Z3-PY 中实现 C 位运算符？

问题描述

我希望能够对我Solver的 s 实施以下规则，其中 '^' 和 '&' 运算符是 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 求解器的规则？

标签： cbitwise-operatorsz3z3py

解决方案

这里的问题是IntSMTLib（和 z3）中的类型是一个成熟的数学整数。它没有任何“位”，也不受任何方式的限制。也就是说，它不是您可以进行按位运算的东西。您还没有给出实际的完全可执行代码，但这里有一个更简单的示例来说明您遇到的错误：

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

推荐阅读