Z3Py：不等于元组的约束

Question

我有BOOLS的一串：

a=Bool('a') 
... 
z=Bool('z') 

如何收拾一些布尔变量来元组，然后加入他们的非平等的约束？

我想：

tuple1=(a,b,c,d) 
tuple2=(e,f,g,h) 
# so far so good 
s=Solver() 
s.add(tuple1 != tuple2) 

但是，这并不工作。

Answer 1

python元组不会被反映到Z3元组中。 您可以在以下wayL

from z3 import * 
a,b,c,d,e,f,g,h = Ints('a b c d e f g h') 

tuple = Datatype('tuple') 
tuple.declare('tuple',('1', IntSort()), ('2', IntSort()), ('3', IntSort()), ('4', IntSort())) 
tuple = tuple.create() 
tuple1=tuple.tuple(a,b,c,d) 
tuple2=tuple.tuple(e,f,g,h) 
# so far so good 
s=Solver() 
s.add(tuple1 != tuple2) 
print s.check() 
print s.model() 

为Z3创建一个元组类型在这种情况下，你会得到Z3理解元组disequality。 Z3不理解python元组之间的！=或==运算符。 也许有可能将python支持扩展到这种数据类型 ，但该分发不支持这种扩展。