Z3模式和注入性

Question

在Z3教程的第13.2.3节中,有一个很好的例子,说明如何减少在处理注入的公理化时必须实例化的模式数量.在该示例中,必须以单数形式表示的函数f将类型A的对象作为输入并返回类型B的对象.据我所知,排序A和B是分离的.

我有一个SMT问题(FOL + EUF)Z3似乎没有终止,我试图找出原因.我有一个函数f:A-> A我认为是单射的.问题可能是f的域和codomain重合吗？

提前感谢任何建议.

Answer 1

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

请注意,您引用的教程非常陈旧,并且包含过时的信息.