对Z3列表进行公理化的包含函数的不同方式 [英] Different ways of axiomatising a contains-function for Z3 lists

问题描述

将列表上的包含操作公正化（ on Rise4Fun ）as

 （declare-fun Seq.in（（List Int）Int）Bool）
 
（assert（for（（int int）） 
（不（Seq.in nil e））））
 
（assert（fors（（xs（List Int））（e Int））
（iff 
（not（= xs nil））
（= 
（Seq.in xs e）
（或
（= e（head xs））
 .in（尾xs）e）））））））
  

使Z3 4.0反驳断言

 （declare-const x Int）
（assert（Seq.in nil x））
 -sat）; UNSAT，如预期的
  

在我的眼中相当的公理化

$ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $ $（$）在xs e）false b $ b（=
（Seq.in xs e）
（或
（= e（head xs））
（Seq.in（尾部xs）e）））））））

结果 code>。

这可能是触发器的一个问题，还是有一些特定于列表域的东西，可以解释行为差异？

解决方案

您的脚本在rise4fun会禁用：mbqi 引擎。因此，Z3将尝试仅使用电子匹配来解决问题。当没有提供模式（aka触发器）时，Z3将推断我们的触发器。 Z3使用许多启发式来推断模式/触发器。其中一个与您的脚本相关，并解释发生了什么。 Z3永远不会选择产生匹配循环的模式/触发器。我们说一个模式/触发器P为量词Q产生一个匹配循环，当Q的一个实例将产生一个新的P的匹配。
让我们考虑量词

 （assert（for（（xs（List Int））（e Int））
（ite（= xs nil）
（=（Seq.in xs e ）
（= 
（Seq.in xs e）
（或
（= e（head xs））
（Seq.in（tail xs） e）））））））
  

Z3将不选择（Seq.in xs e）作为此量词的模式/触发器，因为它将产生一个匹配的循环。假设我们有一个地面术语（Seq.in a b）。此项符合模式（Seq.in xs e）。将 a 实例化量词将 b 将产生术语（Seq.in（尾）b）也匹配模式（Seq.in xs e）。
用（tail a）和 b 实例化量词将产生术语 （Seq.in（tail（tail a））b）它也匹配模式（Seq.in xs e），等等。

在搜索过程中，Z3将使用多个阈值来阻止匹配循环。但是，性能通常会受到影响。因此，默认情况下，Z3不会选择（Seq.in xs e）作为模式。而是选择（Seq.in（尾xs）e）。此模式不会产生匹配循环，但也可以防止Z3证明第二和第三个查询不能令人满意。
电子匹配引擎的任何限制通常由：mbqi 引擎处理。但是，您的脚本中的：mbqi 被禁用。

如果您提供第二和第三个查询的模式你的脚本Z3将证明所有的例子都是不能。这是您的示例与明确的模式/触发器：

http： //rise4fun.com/Z3/DkZd

第一个例子即使没有使用模式，因为只需要第一个量词来证明这个例子是

 （assert（for（（int Int））
（不（Seq.in nil e））））
  

请注意，（Seq.in nil e）是该量词的完美模式，它是由Z3选择的模式。

Axiomatising the contains-operation on lists (on Rise4Fun) as

(declare-fun Seq.in ((List Int) Int) Bool)

(assert (forall ((e Int))
  (not (Seq.in nil e))))

(assert (forall ((xs (List Int)) (e Int))
  (iff
    (not (= xs nil))
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

enables Z3 4.0 to refute the assertion

(declare-const x Int)
(assert (Seq.in nil x))
(check-sat) ; UNSAT, as expected

The in my eyes equivalent axiomatisation

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

results in unknown.

Could this be a problem with triggers or is there something specific to the List domain that could explain the difference in behaviour?

解决方案

Your script at rise4fun disables the :mbqi engine. Thus, Z3 will try to solve the problems using only E-matching. When patterns (aka triggers) are not provided, Z3 will infer the triggers for us. Z3 uses many heuristics for inferring patterns/triggers. One of them is relevant for your script, and explains what is going on. Z3 will never select a pattern/trigger that produces a "matching loop". We say a pattern/trigger P produces a matching loop for quantifier Q when an instance of Q will produce a new matching for P. Let us consider the quantifier

(assert (forall ((xs (List Int)) (e Int))
  (ite (= xs nil)
    (= (Seq.in xs e) false)
    (=
      (Seq.in xs e)
      (or
        (= e (head xs))
        (Seq.in (tail xs) e))))))

Z3 will not select (Seq.in xs e) as a pattern/trigger for this quantifier because it will produce a matching loop. Suppose we have a ground term (Seq.in a b). This term matches the pattern (Seq.in xs e). Instantiating the quantifier with a will b will produce the term (Seq.in (tail a) b) that also matches the pattern (Seq.in xs e). Instantiating the quantifier with (tail a) and b will produce the term (Seq.in (tail (tail a)) b) which also matches the pattern (Seq.in xs e), and so on.

During the search, Z3 will block matching loops using several thresholds. However, the performance is usually affected. Thus, by default, Z3 will not select (Seq.in xs e) as pattern. Instead, it will select (Seq.in (tail xs) e). This pattern does not produce a matching loop, but it also prevents Z3 from proving the second and third queries to be unsatisfiable. Any limitation of the E-matching engine is usually handled by the :mbqi engine. However, :mbqi is disabled in your script.

If you provide the patterns for the second and third queries in your script. Z3 will prove all examples to be unsat. Here is your example with explicit patterns/triggers:

http://rise4fun.com/Z3/DkZd

The first example goes through even without using patterns because only the first quantifier is needed to prove the example to be unsat.

(assert (forall ((e Int))
  (not (Seq.in nil e))))

Note that (Seq.in nil e) is a perfect pattern for this quantifier, and it is the one selected by Z3.

这篇关于对Z3列表进行公理化的包含函数的不同方式的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！