z3 - 使用 def 时未知

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 将使用专门的求解器来解决它。unknown但是，当输入问题还包含 if-then-else 项（If您的 中的）时，此求解器可能会失败（返回Min）。 该错误已修复，将在下一个版本中提供。同时，您可以尝试以下解决方法之一：

• 在调用求解器之前强制 Z3 消除 if-then-else 项。您只需替换s = Solver()为s = Then('elim-term-ite', 'smt').solver(). 这是rise4fun 上修改后的脚本。

• 我们可以添加一个不在不同逻辑片段中的冗余断言。示例：z + w > 2。这是rise4fun 上修改后的脚本。