在 Z3Py 中评估 BitVec

Question

我正在学习Z3，可能我的问题不适用，请耐心等待。

假设我有以下内容：

c1, c2 = z3.BitVec('c1', 32), z3.BitVec('c2', 32)

c1 = c1 + c1
c2 = c2 + c2
c2 = c2 + c1
c1 = c1 + c2

e1 = z3.simplify(c1)
e2 = z3.simplify(c2)

当我打印他们的 sexpr() 时：

print "e1=", e1.sexpr()
print "e2=", e2.sexpr()

Output:

e1= (bvadd (bvmul #x00000004 c1) (bvmul #x00000002 c2))
e2= (bvadd (bvmul #x00000002 c2) (bvmul #x00000002 c1))

我的问题是，如何计算用户提供的 c1 和 c2 值的 'e1' 和 'e2' 的数值？

例如，e1(c1=1, c2=1) == 6, e2(c1=1, c2=1) == 4

谢谢！

Answer 1

我明白了。我不得不引入两个单独的变量来保存表达式。然后我不得不引入两个结果变量，我可以为它们查询模型的值：

e1, e2, c1, c2, r1, r2 = z3.BitVec('e1', 32), z3.BitVec('e2', 32), z3.BitVec('c1', 32), 
                         z3.BitVec('c2', 32), z3.BitVec('r1', 32), z3.BitVec('r2', 32)

e1 = c1
e2 = c2

e1 = e1 + e1
e2 = e2 + e2
e2 = e2 + e1
e1 = e1 + e2

e1 = z3.simplify(e1)
e2 = z3.simplify(e2)

print "e1=", e1
print "e2=", e2

s = z3.Solver()

s.add(c1 == 5, c2 == 1, e1 == r1, e2 == r2)
if s.check() == z3.sat:
    m = s.model()
    print 'r1=', m[r1].as_long()
    print 'r2=', m[r2].as_long()

在 Z3Py 中评估 BitVec

Evaluate a BitVec in Z3Py

expression

evaluate

z3py