使用def的時候UNKNOWN

Question

這個簡單的例子爲我生成UNKNOWN，我想有些東西我不明白def的。

from z3 import * 
s = Solver() 
def Min(b, r): 
    return If(b, r, 1) 
a = Real('a') 
b = Bool('b') 

s.add(a==0.9) 
s.add(a<=Min(b,0.9)) 

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

Answer 1

您沒有犯任何錯誤。這是Z3解算器中的一個問題。你的問題出現在一個叫做「差異邏輯」的算術片段中。如果算術原子可以寫成x - y <= k，其中k是數字，則此片段中存在問題。當這個片段出現問題時，Z3將使用專門的求解器。但是，如果輸入問題還包含if-then-else項（您的Min中的If），則此解算器可能失敗（返回unknown）。 The bug has been fixed，並將在下一個版本中提供。同時，您可以嘗試以下解決方法之一：

• 強制Z3在調用求解器之前消除if-then-else項。您只需將s = Solver()替換爲s = Then('elim-term-ite', 'smt').solver()即可。 Here is the modified script at rise4fun.

• 我們可以添加一個不在不同邏輯片段中的冗餘斷言。例如：z + w > 2。 Here is the modified script at rise4fun.