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

【问题标题】：Non-linear arithmetic and uninterpreted functions非线性算术和未解释的函数
【发布时间】：2012-05-19 23:06:47
【问题描述】：

(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 对上述问题给出“模型不可用”。有没有办法将逻辑设置为可以同时处理两者的东西？谢谢。

【问题讨论】：

标签： z3

【解决方案1】：

新的非线性求解器尚未与其他理论（数组、未解释函数、位向量）集成。在 Z3 4.0 中，它只能用于解决仅包含非线性算术断言的问题。这将在未来的版本中更改。

【讨论】：