Z3 卡住了解决一个看似简单的存在答案

【问题标题】：Z3 stuck solving a seemingly simple existentialZ3 卡住了解决一个看似简单的存在
【发布时间】：2019-09-14 17:12:16
【问题描述】：

我使用 Z3 定理证明器作为编译器的后端，以验证函数调用是否尊重它们的合同。然而，Z3 在解决看似简单的存在性查询时似乎陷入了困境。

我使用的是 Z3 版本 4.8.5 - 64 位（在 Linux 5.0 中）。我知道 SMT 求解器对于一阶逻辑并不完整（只要涉及量词），但我仍然希望以下工作。

这是一个显示问题的最小示例，它不会终止：

(declare-datatypes ()
  ((Term (structure (constructor Int) (arguments TermList)))
   (TermList empty (cons (head Term) (tail TermList)))))

(assert
  (forall ((A TermList) (B Term))
    (implies
      (= A (cons B empty))
      (exists ((C Term))
          (= A (cons C empty))))))

(check-sat)

这是 Z3 的一个众所周知的错误或限制吗？

是否有任何合理的替代方法可以以 Z3 可以处理的方式表示此查询？

【问题讨论】：

标签： z3

【解决方案1】：

这类问题不适合 SMT 求解器。有很多这样的疑问，这里有一些最相关的：

长话短说，使用更强大的系统来执行此类证明，该系统使用 SMT 求解器作为引擎盖下的证明工具。您将不得不进行一些手动“指导”，但如今定理证明器的策略语言已经非常完善，它们可以自动为您实现这种形式的大多数目标。（有关 Isabelle 的一些具体细节，请参阅本文：https://people.mpi-inf.mpg.de/~jblanche/frocos2011-dis-proof.pdf）

【讨论】：