数据类型和量词模式/触发器

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。

为方便起见，这里是rise4fun 上的the example。

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

Answer 1

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

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

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

这样就可以推断出矛盾并推断出不饱和。

当 Snap 未被解释时，Z3 会尝试构建一个模型，其中 s1 和 s2 项不同。由于没有什么可以迫使这些术语相等，它们仍然是不同的

Answer 2

这不是一个错误，因为 z3 没有说 unsat 来表示 sat 公式（或 sat 表示 unsat 公式）。在存在量化公式的情况下，SMT 求解器（通常）不完整。所以他们有时会在不确定sat中的输入公式时回答unknown。

你的例子：

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

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