z3:枚举类型、ADT和递归函数
我正在尝试使用z3来解决一些约束系统。
问题的直观或一般编码是通过三种枚举类型Variable、Field和Class以及ADT Path来完成的，该枚举类型由Variable或用Path扩展的Field组成。(语法上是x或p.f)。还有一个(递归)函数substitute，它将一个路径中的变量替换为另一个路径。有两个属性path-equivalence和instance-of (归纳地)是通过全量化断言定义的。
下面是有关自然数的一个更具体的示例：
类是Zero、Succ和Nat，我们有一个变量a和一个字段p。我们知道，如果路径是类Zero的实例，那么路径也是类Nat的实例；如果路径是类Succ的实例，并且路径具有类Nat的字段p，那么路径也是类Nat的实例。
我们向求解器提出的问题是:是否可能a是Succ，a.p是Zero，而a不是Nat。预期的结果是它不是(unsat.)，因为这将违反上面提到的两个规则。
(declare-datatype Variable (a))
(declare-datatype Field (p))
(declare-datatype Class (Zero Nat Succ))
(declare-datatype Path ((path-base (path-id Variable)) (path-ext (path-object Path) (path-field Field))))
(declare-fun path-equivalence (Path Path) Bool)
(declare-fun instance-of (Path Class) Bool)
(define-fun-rec substitute ((p1 Path) (x1 Variable) (p2 Path)) Path
(ite (is-path-base p1)
(ite (= x1 (path-id p1)) p2 p1)
(path-ext (substitute (path-object p1) x1 p2) (path-field p1))))
(assert (instance-of (path-base a) Succ))
(assert (instance-of (path-ext (path-base a) p) Zero))
(assert (not (instance-of (path-base a) Nat)))
(assert (forall ((p3 Path)) (path-equivalence p3 p3)))
(assert (forall ((p5 Path) (p6 Path) (x2 Variable) (p7 Path) (p8 Path))
(=> (and (path-equivalence p8 p7) (path-equivalence (substitute p5 x2 p7) (substitute p6 x2 p7)))
(path-equivalence (substitute p5 x2 p8) (substitute p6 x2 p8)))))
(assert (forall ((p9 Path) (cls2 Class) (x3 Variable) (p10 Path) (p11 Path))
(=> (and (path-equivalence p11 p10) (instance-of (substitute p9 x3 p10) cls2))
(instance-of (substitute p9 x3 p11) cls2))))
(assert (forall ((p15 Path)) (=> (instance-of p15 Zero) (instance-of p15 Nat))))
(assert (forall ((p16 Path))
(=> (and (instance-of p16 Succ) (instance-of (path-ext p16 p) Nat)) (instance-of p16 Nat))))
(check-sat)到目前为止，求解器似乎能够反驳与所断言的公理相矛盾的问题。当我们试图解决没有违反规则的查询时，问题似乎就开始了。例如，有没有可能a是Succ，a.p是Zero，a不是Zero。
(declare-datatype Variable (a))
(declare-datatype Field (p))
(declare-datatype Class (Zero Nat Succ))
(declare-datatype Path ((path-base (path-id Variable)) (path-ext (path-object Path) (path-field Field))))
(declare-fun path-equivalence (Path Path) Bool)
(declare-fun instance-of (Path Class) Bool)
(define-fun-rec substitute ((p1 Path) (x1 Variable) (p2 Path)) Path
(ite (is-path-base p1)
(ite (= x1 (path-id p1)) p2 p1)
(path-ext (substitute (path-object p1) x1 p2) (path-field p1))))
(assert (not (=> (and (instance-of (path-base a) Succ) (instance-of (path-ext (path-base a) p) Zero))
(instance-of (path-base a) Zero))))
(assert (forall ((p3 Path)) (path-equivalence p3 p3)))
(assert (forall ((p5 Path) (p6 Path) (x2 Variable) (p7 Path) (p8 Path))
(=> (and (path-equivalence p8 p7) (path-equivalence (substitute p5 x2 p7) (substitute p6 x2 p7)))
(path-equivalence (substitute p5 x2 p8) (substitute p6 x2 p8)))))
(assert (forall ((p9 Path) (cls2 Class) (x3 Variable) (p10 Path) (p11 Path))
(=> (and (path-equivalence p11 p10) (instance-of (substitute p9 x3 p10) cls2))
(instance-of (substitute p9 x3 p11) cls2))))
(assert (forall ((p15 Path)) (=> (instance-of p15 Zero) (instance-of p15 Nat))))
(assert (forall ((p16 Path))
(=> (and (instance-of p16 Succ) (instance-of (path-ext p16 p) Nat)) (instance-of p16 Nat))))
(check-sat)预期的结果将是sat，但求解器基本上“永远运行”(我在大约30分钟后终止了调用)。
为什么会这样呢？我怀疑它可能与递归替换函数和ADT (无限域)有关，或者与这两个属性的公理定义有关。
解决此问题的可能方向是什么？例如，是否有一种方法可以将for the solver有问题的构造转换为更合适的构造(或者完全不同的构造)？
回答 1
Stack Overflow用户
发布于 2021-07-14 22:09:52
量词对于SMT求解器来说是很难的。递归定义对于SMT求解器来说是很困难的。您的问题将两者结合在一起，难怪z3的日子不好过。
请始终记住，SMT求解器不做归纳。关于递归定义的任何有趣性质的证明都需要归纳。想象一下，你将如何用手证明你想要的属性。你会使用归纳法吗？如果是这样的话，你已经被卡住了；z3不会帮你。
关于使用z3的量词和归纳证明的使用，堆栈溢出上有无数的疑问；这里有一个列奥纳多的好答案来通读：Quantifier Vs Non-Quantifier
你能做什么？如果你想要开箱即用的SMT解决方案，那就没什么好说的。也许您可以使用模式(https://rise4fun.com/z3/tutorialcontent/guide#h28)，它至少使用起来很棘手，而且我在这里看不到直接的应用程序。
然而，乍一看，您的问题可能更好地通过角解决程序来解决：https://rise4fun.com/z3/tutorialcontent/fixedpoints看看您是否可以采用其中的技术来应用于您的问题。如果没有，我建议使用实际的定理证明器(如Isabelle、HOL、ACL2等)。几乎所有这些都提供了SMT策略来帮助您。
长话短说；量词和递归定义对于SMT解算器来说很难处理。任何需要归纳的属性都无法证明开箱即用。如果幸运的话，您会得到一个反例；最常见的情况是，您会在e匹配引擎中得到一个循环行为。
顺便说一句，您可以通过增加冗长来运行z3来查看它在做什么。尝试z3 -v:3如果你在你的程序上这样做，你会看到它一直在扩展递归定义，这永远不会证明一个定理；但如果在它探索的深度有一个反例，可能会找到一个反例。这不是最容易阅读的输出，但可以让您了解递归函数求解器在实践中是如何工作的。(本质上是按需展开。)
https://stackoverflow.com/questions/68376516
复制相似问题
腾讯云开发者
