代数的実数：かなり印刷するとz3は丸めますか？

Question

は私が発行した場合：

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

んZ3は、実数の10番目の数字の後に任意の丸めを行いますか？それとも、四捨五入せずに残りの数字を切り捨てるだけですか？ lowerとupper：Z3 4.0で

Answer 1

は、代数的数alphaは、単変量多項式pと2つの2進有理数を使用して表されます。 2進有理数は、a/2^kという形式の有理数であり、aは整数であり、kは自然数である。我々はalphaが(lower, upper)の間のpの唯一の根であるとします。場合オプション

（セットオプション：真PP-10進数）

（セットオプション：PP-小数精度のN）

が設けられています。まず、間隔(lower, upper)を絞り込み、upper - lower < 1/10^Nまで絞り込みます。次に、上限（バイナリの有理数）を覗いて、N番目の桁の後で切り捨てることで10進数で表示します。より正確には、この洗練は実際にはupper - lower < 1/16^Nまで実行されます。

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