【发布时间】：2013-10-23 20:53:59
【问题描述】：
Z3 决定非线性实数运算的存在片段吗？ 也就是说，我可以用它作为一个决策过程来测试一个 带 + 和 x 的无量词公式对实数有解？
【问题讨论】：
标签： z3
【发布时间】：2013-10-23 20:53:59
【问题描述】：
是的，Z3 对非线性多项式实数算术的存在片段有一个决策过程。当然，程序是完整的模可用资源。该程序相当昂贵。 This article 描述了在 Z3 中实现的过程。
这是一个小例子（也可以在线获取here）：
(declare-const a Real)
(declare-const b Real)
(assert (= (^ a 5) (+ a 1)))
(assert (= (^ b 3) (+ (^ a 2) 1)))
(check-sat)
(get-model)
(set-option :pp-decimal true) ;; force Z3 to display the result in decimal notation
(get-model)
这是一个相关的问题：
【讨论】：