在 Z3 中使用函数、实数和量词答案

【问题标题】：Using functions, reals, and quantifiers in Z3在 Z3 中使用函数、实数和量词
【发布时间】：2014-09-13 13:40:22
【问题描述】：

我正在尝试向 Z3 提出涉及未解释函数（始终使用域 int）、实数和量词的查询。我知道添加量词通常会导致unknown 结果，但我对这发生的速度感到惊讶：

(declare-fun $in1 (Int) Real)
(declare-fun $in2 (Int) Real)
(assert (< ($in1 0) ($in2 0)))
(assert (forall (($$out Real))
  (not (and (< ($in1 0) $$out) (< $$out ($in2 0))))))
(check-sat)

此查询应返回 unsat，但会超时并返回 unknown。是否有我可以设置的标志或选项可能导致 Z3 解决此查询？我不希望不得不将所有未解释的函数展平为标量，但这是我可以做的。

【问题讨论】：

标签： z3

【解决方案1】：

Arie Gurfinkel 指出(check-sat-using qe-sat) 解决了这个问题。

【讨论】：

【解决方案2】：

是的，看起来这是 Z3 的硬实例。电子匹配无法证明不可满足性，之后 MBQI 基本上开始枚举实数，这不会导致这里的目标。

如果您只想快速获得结果但不关心未知数，只需将 smt.mbqi.max_iterations 设置为足够小的值。您还可以尝试通过提供实例化模式来帮助电子匹配引擎（参见例如quantifier section in the Z3 guide）。

还有一个相关问题可能有助于理解：Z3 patterns and injectivity

【讨论】：