我想知道同一列表公理的这两种编码之间有什么区别:
(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 相同,第一个版本返回未知。
最佳答案
带有量词的一阶逻辑本质上是半可判定的。在 SMT 上下文中,这意味着没有决策过程可以正确回答每个查询,例如 sat
/unsat
。
(撇开理论不谈,其实没那么重要:如果完全忽略效率考虑,那么有一些算法可以正确回答所有可满足的查询,但是没有算法可以正确推导unsat
。在后一种情况下,它们会永远循环。但这是一个题外话。)
因此,为了处理量词,SMT 求解器通常采用一种称为 E 匹配的技术。本质上,当他们形成提及未解释函数的基础术语时,他们会尝试实例化量化公理以匹配它们并相应地重写。这种技术在实践中非常有效,并且可以很好地解决典型的软件验证问题,但它显然不是万能的。详情参见这篇论文:https://pdfs.semanticscholar.org/4eb2/c5e05ab5c53f20c6050f8252a30cc23561be.pdf .
关于你的问题:本质上,当你有公理的 ite
形式时,电子匹配算法根本无法找到正确的替换来实例化你的公理。出于效率考虑,电子匹配器实际上会查看几乎“精确”的匹配。 (对此持保留态度;它比那更聪明,但聪明不了太多。)在实践中,太聪明几乎不会有返回,因为你最终可能会生成太多的匹配,并最终导致搜索空间爆炸。和往常一样,这是实用性、效率和覆盖尽可能多的案例之间的平衡。
Z3 允许指定模式在一定程度上指导搜索,但模式使用起来相当棘手且脆弱。 (我已经向您指出了模式文档中的正确位置,可惜 z3 文档站点暂时关闭,正如您自己注意到的那样!)您可能想尝试一下它们,看看它们是否能给您带来更好的结果。但经验法则是让量化公理尽可能简单明了。与第一个变体相比,您的第二个变体恰恰做到了这一点。对于这个特定问题,一定要把公理分成两部分,并分别断言这两部分以覆盖 nil/insert 情况。将它们组合成一条规则超出了当前电子匹配器的能力。
关于z3 - 同一公理的编码差异,我们在Stack Overflow上找到一个类似的问题: https://stackoverflow.com/questions/54046220/