如果我发出：
(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在区间(lower, upper) 。 当选项
（设置选项：PP-十进制真）
（设定选项：PP-小数精度N）
是提供。 首先，我挤/缩小的间隔(lower, upper)直到upper - lower < 1/10^N 。 然后，我偷看上限（其为二进制理性）和第N个位之后斩波十进制显示它。 为了更精确，实际进行细化，直到upper - lower < 1/16^N 。
我知道这是不是一个理想的解决方案，但它对于大多数来说已经足够好。
文章来源: algebraic reals: does z3 do rounding when pretty printing?
