Z3Py：添加两个向量不等式的约束

Question

（主题）

这是我的尝试：

#!/usr/bin/python
from z3 import *

s=Solver()

veclen=3

tmp_false=BoolVector ('tmp_false', veclen)
for x in range(veclen):
    s.add(tmp_false[x]==False)

tmp=BoolVector ('tmp', veclen)

s.add(tmp!=tmp_false) # not working

# I want here tmp equals to anything except False,False,False

print s.check()
print s.model()

我会使用元组，但向量的长度是在运行时设置的。我应该使用数组吗？或元组中类似 LISP 的cons-cells，如Z3 手册中所述？

Answer 1

BoolVector 函数只是创建一个列表结构。 python 列表上的 != 运算符不会创建表达式。它只是评估为 "true"。所以你并不是真的向 Z3 发送表达式。要创建元组表达式，您可以使用代数数据类型。记录类型是代数数据类型的特例，Z3 了解如何推理这些。例如，您可以这样写：

from z3 import *

s=Solver()

Bv = Datatype("record")
Bv.declare('mk', ('1', BoolSort()), ('2', BoolSort()), ('3', BoolSort()))   
Bv = Bv.create()

tmp_false = Bv.mk(False, False, False)
tmp = Const('tmp', Bv)

print tmp != tmp_false
s.add(tmp!=tmp_false) 

# I want here tmp equals to anything except False,False,False

print s.check()
print s.model()

Z3Py：添加两个向量不等式的约束

Z3Py: add constraint of two vectors inequality

z3

z3py