非線性算術和未解釋的函數

Question

(declare-const x Real) 
(declare-fun f (Real) Real) 
(assert (= (f 1.0) 0.0)) 
(assert (= (* x x) (* 1.0 1.0))) 
(check-sat) 
(get-model) 

我有兩個獨立的斷言之一在非線性算術和其他未解釋的函數。對於上面的問題，Z3給出了「型號不可用」。有沒有辦法將邏輯設置爲可同時處理兩者的東西？謝謝。

Answer 1

新的非線性求解器尚未與其他理論（數組，未定義的函數，位向量）整合。在Z3 4.0中，它只能用於解決只包含非線性算術斷言的問題。這將在未來的版本中改變。