z3 - z3 实数的存在论

Question

Z3 决定非线性实数运算的存在片段吗？也就是说，我可以用它作为一个决策过程来测试一个带有 + 和 x 的无量词公式是否有一个实数的解？

Answer 1

是的，Z3 有一个用于非线性多项式实数算术存在片段的决策过程。当然，程序是完整的模可用资源。该程序相当昂贵。本文描述了在 Z3 中实现的过程。

这是一个小例子（也可以在这里在线获得）：

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

这是一个相关的问题：

• Z3 支持非线性算术