代數實數：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。

我意識到這不是一個理想的解決方案，但它對於大多數目的來說已經足夠好了。