z3 - 代数实数：z3 在漂亮打印时是否进行舍入？

Question

如果我发出：

(set-option :pp-decimal true)
(set-option :pp-decimal-precision 10)

Z3 是否在实数的第 10 位之后进行四舍五入？或者它只是将剩余的数字切掉而不进行任何四舍五入？

Answer 1

在 Z3 4.0 中，代数数alpha使用单变量多项式p和两个二进制有理数表示：lower和upper。二元有理数是整数和自然数形式a/2^k的有理数。我们有那是区间中唯一的根。什么时候选择akalphap(lower, upper)

（设置选项：pp-decimal true）

（设置选项：pp-decimal-precision N）

提供。首先，我压缩/细化间隔(lower, upper)直到upper - lower < 1/10^N. 然后，我窥视上限（这是一个二进制有理数），并通过在第 N 位后截断以十进制显示。更准确地说，细化实际上是执行到 为止upper - lower < 1/16^N。

我意识到这不是一个理想的解决方案，但对于大多数用途来说已经足够了。