Z3 是否支持量化公式中的仅变量模式? [英] Does Z3 support variable-only patterns in quantified formulas?

问题描述

我想使用仅变量模式来获得使用量化公理编码的某些理论的决策程序.更准确地说，我想强制这些公理中的某些变量使用相应类型的所有项进行实例化.这些变量仅出现在谓词符号下方，因此不会有创建匹配循环的危险.

I'd like to use variable-only patterns to obtain decision procedures for certain theories encoded using quantified axioms. More precisely, I want to enforce that certain variables in these axioms are instantiated with all terms of the corresponding sort. These variables only appear below predicate symbols, so there is no danger for creating matching loops.

例如，考虑以下部分查询:

For example, consider the following partial query:

(declare-sort Loc 0)
(declare-sort Map 2)
(declare-fun read ((Map Loc Loc) Loc) Loc)
(declare-fun Btwn ((Map Loc Loc) Loc Loc Loc) Bool)
... 
(assert (forall ((?f (Map Loc Loc)) (?x Loc) (?y Loc))
           (or (not (= (read ?f ?x) ?x)) (not (Btwn ?f ?x ?y ?y)) (= ?x ?y))))

在公理中，我想为所有与 read ?f ?x?f 和 ?x> 和变量 ?y 以及所有排序项 Loc.

In the axiom, I'd like to instantiate the variables ?f and ?x for all ground terms matching read ?f ?x and the variable ?y with all terms of sort Loc.

如果我将以下多模式添加到公理中:

If I add the following multi-pattern to the axiom:

:pattern ((read ?f ?x) ?y)

然后 Z3 报告仅变量模式 ?y 的错误.如果我在模式中省略 ?y 如下:

then Z3 reports an error for the variable-only pattern ?y. If I omit ?y in the pattern as follows:

:pattern ((read ?f ?x))

然后 Z3 报告警告说并非所有变量都出现在模式中.似乎无法抑制此警告.此外，在这种情况下，我不确定该模式是否确实产生了预期的实例化.是否有解决方案可以提供我正在寻找的实例(没有警告)?

then Z3 reports a warning saying that not all variables occur in the pattern. It seems impossible to suppress this warning. Also, in this case, I am not sure whether the pattern actually yields the intended instantiations. Is there a solution that gives me the instantiations I am looking for (without warnings)?

请注意，我感兴趣的理论不属于单独使用 MBQI 产生决策程序的任何片段(据我所知).我可以预先部分实例化公理以获得 EPR 理论(这是我目前所做的)，但我更希望求解器为我做这件事.

Note that the theories I am interested in don't fall into any of the fragments for which MBQI alone yields a decision procedure (as far as I understand). I can partially instantiate the axioms up-front to obtain an EPR theory (which is what I do at the moment), but I'd rather like the solver to do this for me.

推荐答案

基于模式的实例化引擎要求变量在函数符号的范围内.否则，变量可以匹配任何适当类型的基本术语，这不会很好地工作，尤其是当实例化创建与变量相同类型的新术语时.您可以在 Z3 中做的是指定一个使用两个谓词的多模式:((read ?f ?x) (Btwn ?f ?x ?y ?y)).您还可以指定在您的原始问题中没有出现的辅助谓词.例如，谓词 (Known ?y).您还必须添加公理来控制您想知道哪些术语.然后你可以使用多模式 ((read ?f ?x) (known ?y)).当然，这通常会比第一个多模式创建更多的实例.

The pattern-based instantiation engine requires variables to be in the scope of a function symbol. Otherwise, a variable, can match any ground term of the appropriate type and this does not work well, especially when instantiation creates fresh terms of the same type as the variable. What you can do in Z3 is to specify a multi-pattern that uses both predicates: ((read ?f ?x) (Btwn ?f ?x ?y ?y)). You could also specify auxiliary predicates that don't occur in your original problem. For example, a predicate (Known ?y). You would have to also add axioms to control which terms you want to be known. Then you can use the multi-pattern ((read ?f ?x) (known ?y)). Of course, this will most often create many more instantiations than the first multi-pattern.

这篇关于Z3 是否支持量化公式中的仅变量模式?的文章就介绍到这了，希望我们推荐的答案对大家有所帮助，也希望大家多多支持IT屋！