Z3py返回不支持的操作数，使用pow()函数

Question

我刚开始用Z3。我一直试图用Z3解决一个问题，但我做不到。我有一个c/c++代码，如下所示：

n4 = 0
if ( j1 != j6 )
    ++n4;
if ( j1 + 1 != j2 )
    ++n4;
if ( j4 + 1 != j1 )
    ++n4;
if ( j3 + 4 != j6 )
    ++n4;
if ( j5 + 2 != j3 )
    ++n4;
n5 = n4 + (j4 ^ 102) + j7;

n5变量必须大于零。我写的Z3py代码如下：

^{pr2}$

运行脚本后，我收到以下错误：

TypeError: unsupported operand type(s) for ** or pow(): 'instance' and 'int'

提前谢谢。在

Answer 1

我不知道你真正的问题是什么，但我想我会用我理解的方式来翻译C++代码。 我避免了IntVector，但使用了Int来创建和。在

我想出了下面的代码。
它会打印模型，希望能帮到你。在

# import all of z3, because why not; define solver
from z3 import *
s = Solver()

# define j
for i in range(1,8):
    globals()['j%i' % i] = BitVec ('j%i' % i, 8)

# define 8-bit BitVector (BV) (not Integer in the mathematical sense)
n4 = BitVec('n4', 8)

# create an Int so we can use Sum (we could also create BV for each if and then sum directly)
su = Int("sum")
s.add(su == Sum(
            If(eq(j1, j6), 0, 1),
            If(j1+1 != j2, 1, 0),
            If(j4+1 != j1, 1, 0),
            If(j3+4 != j6, 1, 0),
            If(j5+2 != j3, 1, 0)
            )
     )
# we used an int, so we need to convert to a BV
s.add(n4 == Int2BV(su, 8))

# create n5 as an 8-bit BV and make sure it's value matches the formula
n5 = BitVec('n5', 8)
s.add(n5 == (n4 + (j4 ^ 102) + j7))  # I assume you meant ^ and not **
# requirement, n5 > 0 (could be merged with the lines above, avoiding the creation of n5 BV)
s.add(n5 > 0)

# iterate over solutions
while s.check() == sat:
    print(s.model())  # Python3 uses brackets