【发布时间】：2017-06-14 12:40:51
【问题描述】：
Z3 中Real 变量的通常精度是多少？是否使用精确算术？
有没有办法手动设置准确度级别？
如果Real 表示必须使用精确算术，是否还有其他精度有限的浮点值数据类型？
最后：从这个角度来看，z3 与其他流行的 SMT 求解器有什么不同，或者这在 SMT-LIB 定义中是标准化的吗？
【问题讨论】：
【发布时间】：2017-06-14 12:40:51
【问题描述】：
看到这个答案：z3 existential theory of the reals
关于打印精度，看这个：algebraic reals: does z3 do rounding when pretty printing?
简而言之，是的，它们精确地表示为多项式的根。不是每个实数都可以用Real 类型表示（超越数、e、pi 等）；但所有多项式根都是可表示的。
This paper 讨论如何同时处理先验。
【讨论】：
-
非常感谢 Levent！那么默认情况下z3总是试图找到一个精确的解决方案？还是对精度有一些限制？
-
这是
Reals的决策程序。只要模型值可以表示为多项式的根，Z3 就会找到它们。 （当然，假设您有无限的计算资源。）请注意，这里很容易打破“完整性”：例如，当您混合Real和Int时，您将立即遇到问题，因为组合两者一般是不可判定的。看到这个答案：stackoverflow.com/questions/42133675/…