同一公理的编码差异答案

【问题标题】：difference in encoding of the same axiom同一公理的编码差异
【发布时间】：2019-05-31 10:55:30
【问题描述】：

我想知道同一个列表公理的这两种编码有什么区别：

(define-sort T1 () Int)

(declare-fun list_length ( (List T1) ) Int)

(assert (forall ( (i T1) (l (List T1)) )
                (ite (= l (as nil (List T1)))
                     (= (list_length l) 0)
                     (= (list_length (insert i l)) (+ 1 (list_length l))))))

和

(define-sort T1 () Int)

(declare-fun list_length ( (List T1) ) Int)

(assert (= (list_length (as nil (List T1))) 0))

(assert (forall ( (i T1) (l (List T1)) )
                (= (list_length (insert i l)) (+ 1 (list_length l)))))

对于这个基准：

(declare-const a T1)
(declare-const b T1)

(assert (not
         (= (list_length (insert b (insert a (as nil (List T1))))) 2)))

(check-sat)

不知何故，z3 能够推断出第二个版本，但不是第一个版本（它似乎只是永远循环）。

编辑：与 cvc4 相同，第一个版本返回未知。

【问题讨论】：

标签： z3 smt cvc4

【解决方案1】：

带量词的一阶逻辑本质上是半可判定的。在 SMT 上下文中，这意味着没有决策过程可以正确回答每个查询，如 sat/unsat。

(抛开理论不谈，没那么重要：如果你完全忽略效率考虑，那么有算法可以正确回答所有可满足的查询，但没有算法可以正确推断@987654324 @。在后一种情况下，它们会永远循环。但这是题外话。）

因此，为了处理量词，SMT 求解器通常采用称为 E-matching 的技术。本质上，当它们形成一个提及未解释函数的基本术语时，它们会尝试实例化量化的公理以匹配它们并相应地重写。这种技术在实践中非常有效，并且可以很好地解决典型的软件验证问题，但它显然不是灵丹妙药。详情见本文：https://pdfs.semanticscholar.org/4eb2/c5e05ab5c53f20c6050f8252a30cc23561be.pdf。

关于您的问题：本质上，当您拥有公理的 ite 形式时，电子匹配算法根本无法找到合适的替换来实例化您的公理。出于效率考虑，e-matcher 确实着眼于几乎“精确”的匹配。（对此持保留态度；它比那更聪明，但不是很多。）在这里太聪明在实践中几乎没有回报，因为您最终可能会生成太多匹配并最终爆炸您的搜索空间。像往常一样，它是实用性、效率和尽可能多的案例之间的平衡。

Z3 允许指定模式以在一定程度上指导搜索，但模式使用起来相当棘手且脆弱。（我会在模式文档中为您指出正确的位置，可惜 z3 文档站点暂时关闭了，正如您自己注意到的那样！）您可能想与它们一起玩，看看它们是否能给您带来更好的结果.但经验法则是让你的量化公理尽可能简单明了。与第一个变体相比，您的第二个变体正是这样做的。对于这个特定的问题，绝对将公理分成两部分，并分别断言以涵盖nil/insert 的情况。将它们组合成一个规则简直超出了当前电子匹配器的能力。

【讨论】：