Z3精度为实数和小数值

Z3中Real变量的通常精度是多少？是否使用了精确算术？Z3精度为实数和小数值

有没有办法手动设置精度等级？

如果Real意味着必须使用精确算术，那么对于精度有限的浮点值是否还有其他数据类型？

最后：从这个角度来看，z3与其他流行的SMT解算器有什么不同，还是这种标准化的SMT-LIB定义？

来源

2017-06-14 Andrea Callia D' Iddio

看到这个答案：z3 existential theory of the reals

关于打印精度，看到这一个：algebraic reals: does z3 do rounding when pretty printing?

简而言之，是的，他们精确地表示为多项式的根。并非每个实数都可以用Real类型表示（超越，e，pi等）。但是所有的多项式根都是可表示的。

This paper讨论如何也处理先验。

来源

2017-06-14 16:02:15

非常感谢Levent！那么默认情况下，z3总是试图找到一个确切的解决方案？还是有一些精度限制？ –

这是'Reals'的决定程序。只要模型值可表示为多项式的根，Z3就可以找到它们。（当然，假设你拥有无限的计算资源）。注意，在这里很容易打破“完整性”：例如，当你混合使用“Real”和“Int”时，你会立即遇到问题，因为组合一般来说这两者是不可判定的。看到这个答案：https://stackoverflow.com/questions/42133675/get-fractional-part-of-real-in-qf-ufnra/42147549#42147549 –

Z3精度为实数和小数值

回答

相关问题