3

请参阅http://rise4fun.com/Z3Py/GTYu上的 PyZ3 程序。第一次调用check()工作正常，但如果我们向求解器添加约束并check()再次调用，我们会得到一个不一致的模型！

sy_i = Bool('sy_i')
s0_v, s1_v, s2_v, sx_v, sy_v = Reals('s0_v s1_v s2_v sx_v sy_v')

c = [s0_v >= 1,
     sx_v >= 1,

     s1_v >= s0_v * sx_v,

     sy_v >= 1,

     Or(Not(sy_i), s1_v == RealVal(0.0)),

     s2_v >= s1_v * sy_v
]

solver = Solver()
solver.add(c)
print solver.check()
print solver.model()

solver.add(True)
solver.check()
print solver.model()

有人知道发生了什么吗？

不稳定的 Z3 版本得到相同的结果。

附加上下文：

该程序是使用组合nlsat和bool求解器的更大程序的简化，遵循答案的重要建议：Z3 真实算术和数据类型理论集成不太好

请注意，该方法似乎工作得很好，但是当尝试添加更多约束并重用求解器时，就会出现这个问题。也许它错误地检测到了解决方法？

4

1 回答 1

2

默认求解器对象Solver()本质上是一组求解器。它还尝试检测使用模式（增量或非增量）。如果执行了多个check()，则假定用户处于“增量”模式，并使用不完整的非线性算术的通用增量求解器。

要强制 Z3 始终使用nlsat，我们应该使用创建求解器对象

solver = Tactic('qfnra-nlsat').solver()

如果我们这样做，我们仍然可以使用push(), pop(), multiple check()。但是，nlsat不会“重用”以前check()调用的工作。这是您的脚本的新版本。

于 2013-01-07T17:58:32.890 回答