非线性算术和未解释函数 [英] Non-linear arithmetic and uninterpreted functions

问题描述

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

I have two independent assertions one in non-linear arithmetic and other uninterpreted functions. Z3 gives a "model is not available" to the problem above. Is there a way to set the logic to something that can handle both at the same time? Thank you.

推荐答案

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

The new nonlinear solver is not integrated with other theories (arrays, unintepreted functions, bit-vectors) yet. In Z3 4.0, it can only be used to solve problems that contain only nonlinear arithmetic assertions. This is will change in future versions.

这篇关于非线性算术和未解释函数的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！