1

将列表（在 Rise4Fun 上）上的包含操作公理化为

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

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

4

1 回答 1

2

您在rise4fun 的脚本会禁用:mbqi引擎。因此，Z3 将尝试仅使用 E-matching 来解决问题。当没有提供模式（又名触发器）时，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不会选择(Seq.in xs e)作为此量词的模式/触发器，因为它会产生匹配循环。假设我们有一个基本项(Seq.in a b)。该术语与模式匹配(Seq.in xs e)。实例化量词a将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 证明第二个和第三个查询是不可满足的。E-matching 引擎的任何限制通常由:mbqi引擎处理。但是，:mbqi在您的脚本中被禁用。

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

http://rise4fun.com/Z3/DkZd

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

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

请注意，这(Seq.in nil e)是这个量词的完美模式，它是 Z3 选择的模式。

于 2012-06-20T19:52:45.597 回答