python - 调用 check 两次应该工作吗？

Question

在 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 real arithmetics and data types theories integrating not that well

请注意，该方法似乎工作得很好，但当尝试添加更多约束并重用求解器时，就会出现此问题。可能是误测了求解方法？

Answer 1

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

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

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

如果我们这样做，我们仍然可以使用 push()、pop()、多个 check()。但是，nlsat 不会“重用”之前的 check() 调用的工作。 Here is the new version of your script .