3

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

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

提前感谢您的任何建议。

4

1 回答 1

6

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

(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 也不会终止（对于可满足的公式）。

请注意，您引用的教程非常古老，并且包含过时的信息。

于 2012-12-15T05:56:41.273 回答