重複在Z3py

Question

匹配模型

在下面的工作例子中，我試圖檢索匹配的型號，在這種情況下有兩種型號滿足：

t1= cl7   t2= cl4  t3= cl5 

和

t1= cl4   t2= cl3  t3= cl9 

的問題是重複匹配模型，直到運行解算器超時。 如何檢索滿意的模型而不重複。

非常感謝，

 S, (cl1, cl2, cl3, cl4, cl5, cl6, cl7,cl8,cl9) = EnumSort('S', ['cl1', 'cl2', 'cl3', 'cl4', 'cl5','cl6' ,'cl7', 'cl8', 'cl9']) 



     s = Solver() 

     x = Const('x', S) 
     def fun1(x): 
     return Or(x == cl1, x == cl2, x == cl3, x == cl4, x == cl5, x == cl6, x == cl7, x == cl8, x == cl9) 


     y1, y2 = Consts('y1 y2', S) 
     def fun2(y1, y2): 
      return Or(And(y1 == cl7, y2 == cl4), And(y1 == cl4, y2 == cl3), And(y1 == cl3, y2 == cl2),And(y1 == cl8, y2 == cl9)) 


     q1,q2 = Consts('q1 q2', S) 
     def fun3(q1,q2): 
     return Or(And(q1 == cl7, q2 == cl5), And(q1 == cl4, q2 == cl9)) 



t1, t2 ,t3 = Consts('t1 t2 t3', S) 

s.add(fun1(t1)) 
s.add(fun2(t1,t2)) 
s.add(fun3(t1,t3)) 


while s.check() == sat: 
s.add(Or(t1 != s.model()[t1], t2 != s.model()[t2],t3 != s.model()[t2])) 
print s.model() 

Answer 1

您似乎是在阻止新的滿足性再次檢查所使用的相同車型的一個小錯字，尤其是倒數第二行應該有t3 != s.model()[t3]而不是t3 != s.model()[t2] 。

下面是更新的例子，生成你把開頭的兩款車型（z3py鏈接：http://rise4fun.com/Z3Py/AxJv）：

S, (cl1, cl2, cl3, cl4, cl5, cl6, cl7,cl8,cl9) = EnumSort('S', ['cl1', 'cl2', 'cl3', 'cl4', 'cl5','cl6' ,'cl7', 'cl8', 'cl9']) 

s = Solver() 

x = Const('x', S) 
def fun1(x): 
    return Or(x == cl1, x == cl2, x == cl3, x == cl4, x == cl5, x == cl6, x == cl7, x == cl8, x == cl9) 

y1, y2 = Consts('y1 y2', S) 
def fun2(y1, y2): 
    return Or(And(y1 == cl7, y2 == cl4), And(y1 == cl4, y2 == cl3), And(y1 == cl3, y2 == cl2),And(y1 == cl8, y2 == cl9)) 

q1,q2 = Consts('q1 q2', S) 
def fun3(q1,q2): 
    return Or(And(q1 == cl7, q2 == cl5), And(q1 == cl4, q2 == cl9)) 

t1, t2 ,t3 = Consts('t1 t2 t3', S) 

s.add(fun1(t1)) 
s.add(fun2(t1,t2)) 
s.add(fun3(t1,t3)) 

while s.check() == sat: 
    s.add(Or(t1 != s.model()[t1], t2 != s.model()[t2], t3 != s.model()[t3])) 
    print s.model()