Z3 列表的包含函数公理化的不同方法

公理化列表上的包含操作（在 Rise4Fun 上) as

(declare-fun Seq.in ((List Int) Int) Bool)

(assert (forall ((e Int))
  (not (Seq.in nil e))))

(assert (forall ((xs (List Int)) (e Int))
  (iff
    (not (= xs nil))
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

使Z3 4.0能够反驳该断言

(declare-const x Int)
(assert (Seq.in nil x))
(check-sat) ; UNSAT, as expected

我眼中的等价公理化

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

结果是unknown.

这可能是触发器的问题，还是列表域特有的东西可以解释行为的差异？

您在rise4fun 的脚本禁用了:mbqi引擎。因此，Z3将尝试仅使用E匹配来解决问题。当未提供模式（又称触发器）时，Z3 将为我们推断触发器。 Z3 使用许多启发式方法来推断模式/触发器。其中之一与您的脚本相关，并解释了正在发生的事情。 Z3 永远不会选择产生“匹配循环”的模式/触发器。当 Q 的实例将为 P 生成新的匹配时，我们说模式/触发器 P 为量词 Q 生成匹配循环。 让我们考虑一下量词

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z3 will not select (Seq.in xs e)作为该量词的模式/触发器，因为它将产生匹配循环。假设我们有一个基础项(Seq.in a b)。该术语与模式匹配(Seq.in xs e)。实例化量词a will b将产生术语(Seq.in (tail a) b)也符合模式(Seq.in xs e)。 实例化量词(tail a) and b将产生术语(Seq.in (tail (tail a)) b)这也符合模式(Seq.in xs e)， 等等。

在搜索过程中，Z3 将使用多个阈值来阻止匹配循环。然而，性能通常会受到影响。因此，默认情况下，Z3不会选择(Seq.in xs e)作为模式。相反，它会选择(Seq.in (tail xs) e)。此模式不会产生匹配循环，但它也会阻止 Z3 证明第二个和第三个查询不可满足。 电子匹配引擎的任何限制通常由:mbqi引擎。然而，:mbqi在您的脚本中被禁用。

如果您在脚本中提供第二个和第三个查询的模式。 Z3将证明所有例子都是unsat。这是带有显式模式/触发器的示例：

http://rise4fun.com/Z3/DkZd

即使不使用模式，第一个示例也会完成，因为只需要第一个量词来证明该示例是unsat.

(assert (forall ((e Int))
  (not (Seq.in nil e))))

注意(Seq.in nil e)是该量词的完美模式，也是 Z3 选择的模式。