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 в следующем 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 до таких типов данных , но дистрибутив не поддерживает такие расширения.