代数实数：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的有理数，其中a是整数，而k是自然数。我们有alpha是区间内p的唯一根。当选项

（设定选项：PP-十进制真）

（设定选项：PP-小数精度N）被提供

。首先，我挤压/细化区间(lower, upper)，直到upper - lower < 1/10^N。然后，我查看上限（这是一个二元有理数），并在第N位后切分显示为十进制数。更确切地说，细化实际上执行到upper - lower < 1/16^N。

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