z3 - 非线性算术和未解释的函数

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 中，它只能用于解决仅包含非线性算术断言的问题。这将在未来的版本中改变。