Z3 模式和单射性

Question

在 Z3 教程的第 13.2.3 节中，有一个很好的示例说明在处理单射性公理化时如何减少必须实例化的模式数量。在这个例子中，必须声明单射的函数 f 将 A 类型的对象作为输入并返回 B 类型的对象。据我所知，A 和 B 的种类是分离的。

我有一个 SMT 问题 (FOL+EUF)，Z3 似乎没有终止，我正在尝试找出原因。我有一个函数 f:A->A，我断言它是单射的。问题可能是 f 的域和辅域重合吗？

提前感谢您的任何建议。

Answer 1

Z3 不会终止，因为它一直在尝试为问题建立解释。包含单射性公理的可满足问题对于 Z3 通常是困难的。它们通常属于 Z3 无法决定的一类问题Z3 guide描述了 Z3 可以决定的大部分类。此外，Z3 可以为整数和实数等无限域生成模型。但是，在大多数情况下，Z3 生成的函数具有有限 范围。例如，量词 forall x, y: x <= y implies f(x) <= f(y)可以通过分配 f 来满足到具有有限范围的函数。更多信息可以在 this article 中找到.不幸的是，内射性通常需要一个与定义域一样“大”的范围。而且，写出只能由无限宇宙满足的公理是非常容易的。例如，公式

(assert
   (forall ((d1 Value)(d2 Value)(d3 Value)(d4 Value))
      (! (=>
         (and (= (ENC d1 d2) (ENC d3 d4)))
         (and (= d1 d3) (= d2 d4))
      )
      :pattern ((ENC d1 d2) (ENC d3 d4)))
   )
)

只有Value的宇宙才能满足有一个元素或者是无限的。另一个问题是结合函数的内射性公理 f公理形式为 forall x: f(x) != a .如果f是来自 A 的函数至 A , 那么只有 A 才能满足公式有一个无限的宇宙。

也就是说，我们可以通过减少 Z3 模型查找器用于量化公式的“资源”量来防止未终止。选项

(set-option :auto-config false)
(set-option :mbqi-max-iterations 10)

如果我们使用这些选项，Z3 将在您的示例中终止，但会返回 unknown .它还返回一个“候选”模型。它不是真正的模型，因为它不满足问题中的所有通用量词。选项

(set-option :mbqi-trace true)

将指示 Z3 显示哪些量词不满足。

关于 13.2.3 节中的示例，函数可以使用相同的输入和返回类型。使用本节中描述的技巧只会帮助无法满足的实例。如果您使用此技巧重新编码内射性公理，Z3 也不会终止(对于可满足的公式)。

请注意，您引用的教程很旧，并且包含过时的信息。