z3：枚举类型、ADT 和递归函数

问题描述

我正在尝试使用 z3 来解决一些约束系统。

问题的直觉或一般编码是通过三种枚举类型 Variable、Field 和 Class 完成的，以及由 Path 或 Variable 扩展的 Path 组成的 ADT Field。（语法为 x 或 p.f）。还有一个（递归）函数 substitute 用另一个路径替换路径中的变量。有两个属性 path-equivalence 和 instance-of（归纳地）通过全量化断言定义。

下面是一个更具体的自然数示例：

类是Zero、Succ和Nat，我们有一个变量a和一个字段p。我们知道如果路径是类 Zero 的实例，则路径也是类 Nat 的实例，如果路径是类 Succ 的实例并且路径有一个字段p 类的 Nat，那么路径也是类 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（无限域）有关，或者与这两个属性的公理定义有关。

解决这种行为的可能方向是什么？例如。有没有一种方法可以将求解器有问题的构造转化为更合适的（或完全不同的）？

解决方法

量词对于 SMT 求解器来说很难。递归定义对于 SMT 求解器来说很难。您的问题是两者兼而有之，难怪 z3 遇到困难。

始终牢记 SMT 求解器不进行归纳。任何关于递归定义的有趣性质的证明都需要归纳。想象一下，您将如何手动证明您想要的财产。你会用归纳法吗？如果是这样，你已经卡住了； z3 帮不了你。

关于使用 z3 的量词和归纳证明的使用堆栈溢出有无数查询；这是莱昂纳多的一个很好的答案，可以通读：Quantifier Vs Non-Quantifier

你能做什么？不多，如果您想要开箱即用的 SMT 解决方案。也许您可以使用模式 (https://rise4fun.com/z3/tutorialcontent/guide#h28)，这至少很难使用，而且我在这里没有看到直接的应用程序。

然而，乍一看，您的问题似乎最好由 horn-solver 解决：https://rise4fun.com/z3/tutorialcontent/fixedpoints 看看您是否可以采用那里的技术来解决您的问题。如果没有，我建议您使用实际的定理证明器（如 Isabelle、HOL、ACL2 等），它们几乎都提供 SMT 策略来帮助您。

长话短说； SMT 求解器很难处理量词和递归定义。任何需要归纳的属性都无法证明是开箱即用的。如果你幸运的话，你会得到一个反例，如果存在的话；最常见的是，您会在电子匹配引擎中获得循环行为。

旁注顺便说一句，您可以增加详细程度来运行 z3 以查看它在做什么。试试 z3 -v:3 如果你在你的程序上这样做，你会看到它不断扩展递归定义，这永远不会证明一个定理；但如果在它探索的深度有一个反例，可能会找到一个反例。这不是最容易阅读的输出，但可以让您了解递归函数求解器在实践中是如何工作的。（基本上是通过按需展开。）

smt z3