Z3 模式和注入性 [英] Z3 patterns and injectivity

问题描述

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

In the Z3 tutorial, section 13.2.3, there is a nice example on how to reduce the number of patterns that have to be instantiated when dealing with the axiomatisation of injectivity. In the example, the function f that has to be stated injective, takes an object of type A as input and return an object of type B. As far as I understand the sorts A and B are disjunct.

我有一个 SMT 问题 (FOL+EUF)，Z3 似乎无法终止，我正在尝试找出原因.我有一个函数 f:A->A，我断言它是单射的.会不会是f的域和codomain重合了?

I have an SMT problem (FOL+EUF) on which Z3 seems not to terminate, and I am trying to isolate the cause. I have a function f:A->A that I assert being injective. Could the problem be that the domain and codomain of f coincide?

预先感谢您的任何建议.

Thanks in advance for any suggestion.

推荐答案

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

Z3 does not terminate because it keeps trying to build an interpretation for the problem. Satisfiable problems containing injectivity axiom are usually hard for Z3. They usually fall in a class of problems that can't be decided by Z3 The Z3 guide describes most of the classes that can be decided by Z3. Moreover, Z3 can produce models for infinite domains such as integers and reals. However, in most cases, the functions produced by Z3 have finite ranges. For example, the quantifier forall x, y: x <= y implies f(x) <= f(y) can be satisfied by assigning f to a function that has a finite range. More information can be found in this article. Unfortunately, injectivity usually requires a range that is as "big" as the domain. Moreover, it is very easy to write axioms that can only be satisfied by an infinite universe. For example, the formula

(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 有无穷大时才能满足宇宙.

can only be satisfied if the universe of Value has one element or is infinite. Another problem is combining the injectivity axiom for a function f with axioms of the form forall x: f(x) != a. If f is a function from A to A, then the formula can only be satisfied if A has an infinite universe.

话虽如此，我们可以通过减少 Z3 模型查找器用于量化公式的资源"数量来防止非终止.选项

That being said, we can prevent the non-termination by reducing the amount of "resources" used by the Z3 model finder for quantified formulas. The options

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

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

If we use these options, Z3 will terminate in your example, but will return unknown. It also returns a "candidate" model. It is not really a model since it does not satisfy all universal quantifiers in the problem. The option

(set-option :mbqi-trace true)

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

will instruct Z3 to display which quantifiers were not satisfied.

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

Regarding the example in section 13.2.3, the function may use the same input and return types. Using the trick described in this section will only help unsatisfiable instances. Z3 will also not terminate (for satisfiable formulas) if you re-encode the injectivity axioms using this trick.

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

Note that the tutorial you cited is very old, and contains outdated information.

这篇关于Z3 模式和注入性的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！