在 Z3 中定义带有约束的代数数据类型

我看过一些在线材料，用于定义代数数据类型，例如 Z3 中的 IntList。我想知道如何定义具有逻辑约束的代数数据类型。例如，如何定义代表正整数的 PosSort。

SMT中的全部功能

在 SMT 中函数总是完整的，这提出了如何对部分函数（例如数据类型构造函数）进行编码的问题PosSort。因此，如果 Z3/SMT 对代数数据类型的内置支持支持部分数据类型构造函数（并且SMT-LIB 2.6标准 http://smtlib.cs.uiowa.edu/papers/smt-lib-reference-v2.6-r2017-07-18.pdf看来同意）。

偏函数编码：理论

然而，并非所有希望都破灭了，但您可能必须自己对 ADT 进行编码。假设一个总函数f: A -> B，它应该建模部分数据类型构造函数f': A ~> B都属于谁的域名a满足p(a). Here, A可能Int, B可能List[A], p(a)可能0 < a and f(a)可以定义为f(a) := a :: Nil（我在这里使用伪代码，但你应该明白）。

一种方法是确保f从未应用于a这并不积极。根据您的 SMT 代码的来源，可以在每次应用之前检查该约束f（并提出错误f不适用）。

另一种方法是不指定f并有条件地定义它，例如沿着0 < a ==> f(a) := a :: Nil。这边走，f仍然是总计（正如之前所说，您很可能不得不忍受），但其值未定义a <= 0。因此，当你试图证明一些事情时f(a)，例如那head(f(a)) == a，那么这应该会失败（假设head(a :: _)定义为a).

编码部分函数：一个实际例子

我懒得在 SMT 中编写示例，但是整数列表的这种编码 http://viper.ethz.ch/examples/encoding-adts.html（使用一种名为 Viper 的验证语言）应该会给你一个关于如何编码的非常具体的想法整数列表使用未解释的函数和公理。该示例基本上可以以一对一的方式翻译为SMT-LIB。

更改该示例，使其公理化列表正整数很简单：只需添加约束head < 0对于每一个谈论列表头的公理。 IE。使用以下替代公理：

axiom destruct_over_construct_Cons {
  forall head: Int, tail: list :: {Cons(head, tail)}
    0 < head ==>
         head_Cons(Cons(head, tail)) == head
      && tail_Cons(Cons(head, tail)) == tail
}

...

axiom type_of_Cons {
  forall head: Int, tail: list :: 
    0 < head ==> type(Cons(head, tail)) == type_Cons()
}

如果您在线运行包含这些更改的示例，则测试method test_quantifiers()应该立即失败。在列表元素上添加必要的约束，即将其更改为

method test_quantifiers() {
    /* The elements of a deconstructed Cons are equivalent to the corresponding arguments of Cons */
    assert forall head: Int, tail: list, xs: list ::
      0 < head ==>
        is_Cons(xs) ==> (head == head_Cons(xs) && tail == tail_Cons(xs) <==> Cons(head, tail) == xs)

    /* Two Cons are equal iff their constructors' arguments are equal */
    assert forall head1: Int, head2: Int, tail1: list, tail2: list ::
      (0 < head1 && 0 < head2) ==>
        (Cons(head1, tail1) == Cons(head2, tail2)
          <==> 
        head1 == head2 && tail1 == tail2)
}

应该会使验证再次成功。