z3py能否通過閱讀模型添加新的斷言？

Question

我們可以使用下面的代碼來解決教程中的狗，貓，鼠標拼圖。

dog, cat, mouse = Ints('dog cat mouse') 

s = Solver(); 
s.add(dog>=1) 
s.add(cat>=1) 
s.add(mouse>=1) 
s.add(dog+cat+mouse==100) 
s.add(1500 * dog + 100 * cat + 25 * mouse == 10000) 

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

嗯，我知道我可以使用

m=s.model 
for d in m.decls(): 
    print "%s = %s" % (d.name(), m[d]) 

得到變量的名稱和值。例如，貓= 41。我不知道我可以創建的名稱和值，如貓新主張！= 41.我用

s.add(d.name != m[d]) 
s.add("%s != %s" % (d.name(), m[d])) 

但是，它們都不能正常工作。任何人都知道如何通過閱讀模型的名稱和值來添加新的斷言？非常感謝。

Answer 1

for d in m.decls():d是一個func_decl，即只是一個聲明，而不是一個變量（常量函數），所以我們需要將它應用到它的參數，這裏是空的。因此，我們可以這樣做：

m = s.model() 
for d in m.decls(): 
    v = d() # <-- Note parenthesis() 
    print("%s != %s" % (v, m[d])) 
    s.add(v != m[d]) 

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

得到

... 
cat != 41 
mouse != 56 
dog != 3 
[dog >= 1, 
cat >= 1, 
mouse >= 1, 
dog + cat + mouse == 100, 
1500*dog + 100*cat + 25*mouse == 10000, 
41 != cat, 
56 != mouse, 
3 != dog] 
unsat 

得到