Z3精度爲實數和小數值

Z3中Real變量的通常精度是多少？是否使用了精確算術？Z3精度爲實數和小數值

有沒有辦法手動設置精度等級？

如果Real意味着必須使用精確算術，那麼對於精度有限的浮點值是否還有其他數據類型？

最後：從這個角度來看，z3與其他流行的SMT解算器有什麼不同，還是這種標準化的SMT-LIB定義？

來源

2017-06-14 Andrea Callia D' Iddio

看到這個答案：z3 existential theory of the reals

關於打印精度，看到這一個：algebraic reals: does z3 do rounding when pretty printing?

簡而言之，是的，他們精確地表示爲多項式的根。並非每個實數都可以用Real類型表示（超越，e，pi等）。但是所有的多項式根都是可表示的。

This paper討論如何也處理先驗。

來源

2017-06-14 16:02:15

非常感謝Levent！那麼默認情況下，z3總是試圖找到一個確切的解決方案？還是有一些精度限制？ –

這是'Reals'的決定程序。只要模型值可表示爲多項式的根，Z3就可以找到它們。（當然，假設你擁有無限的計算資源）。注意，在這裏很容易打破「完整性」：例如，當你混合使用「Real」和「Int」時，你會立即遇到問題，因爲組合一般來說這兩者是不可判定的。看到這個答案：https://stackoverflow.com/questions/42133675/get-fractional-part-of-real-in-qf-ufnra/42147549#42147549 –

Z3精度爲實數和小數值

回答

相關問題