z3 - 代数実数:きれいに印刷するときにz3は丸めを行いますか?

Question

私が発行した場合：

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

Z3 は実数の 10 桁目以降を丸めますか? それとも、丸めずに残りの桁を切り刻むだけですか?

Answer 1

Z3 4.0では、代数的数alphaは単変量多項式pと2つの2進有理数を使用して表さlowerれupperます。2進有理数は、が整数と自然数a/2^kである形式の有理数です。これが区間内の唯一のルートです。オプションの場合akalphap(lower, upper)

（set-option：pp-decimal true）

（set-option：pp-decimal-precision N）

提供されています。(lower, upper)まず、間隔を.まで絞り込みますupper - lower < 1/10^N。次に、上限（2進数の有理数）をピークし、N番目の桁の後に切り刻んで10進数で表示します。より正確には、リファインメントは実際にはまで実行されupper - lower < 1/16^Nます。

これは理想的な解決策ではありませんが、ほとんどの目的には十分です。