在Z3Py中發出實際的號碼

在Z3Py中給出像Real('x')這樣的實際號碼，我該如何獲得其樓層或天花板？等同地，我該如何整理它？我發現to_int是SMT規範中的一件事，但我不知道如何從Python中調用它。在Z3Py中發出實際的號碼

函數「ToInt」發言。

from z3 import * 

x = Real('x') 
print ToInt(x) 
print ToInt(RealVal("1/2")) 
print simplify(ToInt(RealVal("1/2")))

2017-05-12 14:57:35

我很想知道'ToInt'/'to_int'是如何有效地解決實際求解器的性能問題。由於我們可以使用這個技巧編碼丟番圖方程（即用實數表示它，然後斷言小數部分爲零），我們是否應該期望得到'未知'結果更經常地存在to_int調用？我理解我的評論非常含糊，但想聽聽你對此的看法。 –

回答