两次打电话检查应该有效吗？

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.