Does Z3 support variable-only patterns in quantified formulas?

Question

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))))

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)

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

:pattern ((read ?f ?x))

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)?

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.

Nikolaj Bjorner Nikolaj Bjorner · Accepted Answer · 2015-01-15T04:03:27

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.

Does Z3 support variable-only patterns in quantified formulas?

1 Answers