数据类型和量词 patterns/triggers

Question

我观察到 Z3 的量词触发行为存在差异（我尝试了 4.4.0 和 4.4.2.3f02beb8203b），我无法解释。考虑以下程序：

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-datatypes () ((Snap
  (Snap.unit)
  (Snap.combine (Snap.first Snap) (Snap.second Snap))
)))

(declare-fun fun (Snap Int) Bool)
(declare-fun bar (Int) Int)
(declare-const s1 Snap)
(declare-const s2 Snap)

(assert (forall ((i Int)) (!
  (> (bar i) 0)
  :pattern ((fun s1 i))
)))

(assert (fun s2 5))

(assert (not (> (bar 5) 0)))
(check-sat) ; unsat

据我了解，unsat 是 意外的：Z3 应该无法触发 forall，因为它由模式 (fun s1 i)，而 Z3 不应该（实际上不能）证明 s1 = s2.

相比之下，如果我声明 Snap 是一个未解释的排序，那么最后的 check-sat 会产生 unknown - 这就是我 期望的 :

(set-option :auto_config false)
(set-option :smt.mbqi false)

(declare-sort Snap 0)

...

(check-sat) ; unknown

如果我假设 s1 和 s2 不同，即

(assert (not (= s1 s2)))

那么最终的 check-sat 在这两种情况下都会产生 unknown。

为了方便起见，这里是the example在rise4fun.

问：行为上的差异是错误，还是有意为之？

Answer 1

这不是错误，因为 z3 不会为 sat 公式说 unsat（或 sat 为 unsat 公式）。在存在量化公式的情况下，SMT 求解器（通常）是不完整的。所以当他们不确定 sat.

中的输入公式时，他们有时会回答 unknown

以你的例子为例：

a - 使用匹配技术，当您假设 s1 和 s2 不同时，z3 无法证明公式是正常的。事实上，没有 (fun s1 5) 形式 (fun s1 5) 的 matches 模式 (fun s1 i)，这将允许从您的 (> (bar 5) 0) 生成有用的实例量化公式;

b - 当您不假设 s1 和 s2 不同时，您也无法获得证明。除了 z3 可能在内部假定 s1 = s2 当 Snap 是数据类型时。只要没有与s1 = s2相矛盾的地方，这就是正确的。由于这一点和匹配模相等性，基础项 (fun s2 5) 匹配模式 (fun s1 i)，并且生成了证明不可满足性所需的实例。

Answer 2

断言 (not (= s1 s2)) 是必不可少的。使用基于模式的量词实例化，如果搜索的当前状态满足 s1 = s2，则模式匹配。在代数数据类型的情况下，Z3 试图通过在构造函数应用方面构建最小模型来满足具有代数数据类型的公式。在 Snap 作为代数数据类型的情况下，s1 和 s2 的最小模型都为 Snap.unit。那时，触发器被启用，因为术语 E-match。换句话说，对同余取模，可以实例化变量 I，使得 (fun s1 I) 匹配 (fun s2 5)，但设置 I <- 5。启用触发器后，量词被实例化，公理

(=> (forall I F(I))  (F(5)))

添加（其中F是量词下的公式）。

这样就可以推断出矛盾，推断出不满足。

当 Snap 未被解释时，Z3 尝试构建一个模型，其中项 s1 和 s2 不同。由于没有什么可以强制这些项相等，因此它们保持不同

数据类型和量词 patterns/triggers

Datatypes and quantifier patterns/triggers

z3