Z3Py：等しくないタプルの制約

Question

私はBoolsの束を持っている：

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

タプルにこれらのboolsの一部をパックした後、その非平等についての制約を追加する方法は？

私が試した：

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

しかし、それは動作しませんが。

Answer 1

pythonタプルはZ3タプルに反映されません。 あなたはZ3が理解タプルdisequalityを取得する。この場合、次の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は、Pythonタプルの間で！=または==演算子を理解しません。 おそらく、そのようなデータ型の にPythonサポートを拡張することは可能ですが、そのような拡張機能は配布されていません。