代数实数:漂亮打印时 z3 是否进行四舍五入? [英] algebraic reals: does z3 do rounding when pretty printing?

问题描述

如果我发出:

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

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

Does Z3 do any rounding after the 10th digit of the real number? Or does it just chop the remaining digits without any rounding?

推荐答案

在 Z3 4.0 中，代数数 alpha 使用单变量多项式 p 和两个二进制有理数表示: lower 和 upper.二进制有理数是 a/2^k 形式的有理数，其中 a 是整数，k 是自然数.我们有 alpha 是区间 (lower, upper) 中 p 的唯一根.When the options

In Z3 4.0, an algebraic number alpha is represented using a univariate polynomial p and two binary rationals: lower and upper. A binary rational is a rational number of the form a/2^k where a is an integer and k a natural number. We have that alpha is the only root of p in the interval (lower, upper). When the options

(set-option :pp-decimal true)

(set-option :pp-decimal true)

(set-option :pp-decimal-precision N)

(set-option :pp-decimal-precision N)

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

are provided. First, I squeeze/refine the interval (lower, upper) until upper - lower < 1/10^N. Then, I peek the upper bound (which is a binary rational) and display it in decimal by chopping after the Nth digit. To be more precise, the refinement is actually performed until upper - lower < 1/16^N.

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

I realize this is not an ideal solution, but it is good enough for most purposes.

这篇关于代数实数:漂亮打印时 z3 是否进行四舍五入?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！