非线性算术和未解释的功能(Non-linear arithmetic and uninterpret

(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:

新的非线性解法器不与其他的理论（数组，unintepreted功能，位向量），但一体化。 在Z3 4.0，它只能被用于解决仅包含非线性算术断言问题。 这将在未来的版本中改变。

文章来源: Non-linear arithmetic and uninterpreted functions