Microsoft Research Community

Suppose we want to axiomatize that the function f is injective. The first that may come to mind is to say that whenever f applied to x and y result in the same value, then also x equals y. In the Simplify format we can write the corresponding axiom:

  (BG_PUSH (FORALL (x y) (IMPLIES (EQ (f x) (f y)) (EQ x y))))

You may wonder how such quantified axioms get instantiated. A main mechanism used in Z3 is to instantiate quantifiers using ground terms that appear in the branch currently being examined during search. But, which terms are used, and how are the related to the axiom? A user can specify which terms are used for instantiation by supplying patterns. Z3 will automatically infer patterns if none are supplied. A pattern is a term or a set of terms that contain all the bound variables of the quantifier they are associated with. For example, a pattern for the axiom above should contain both x and y. But not every term is really relevant for the axiom, only the terms that contain an application of f are really relevant for the axiom, so we can indicate the pattern that is useful for this formula as:

  (BG_PUSH (FORALL (x y) (PATS (MPAT (f x) (f y))) (IMPLIES (EQ (f x) (f y)) (EQ x y))))

We used two constructs: PATS and MPAT. Here PATS is used to enclose a set of alternative patterns (a bound variable could be used in several different sub-terms), which sub-term should be the relevant pattern depends on what the formula says. The keyword MPAT encloses a multi-pattern, which is a sequence of terms that must all match with the current context in order for the quantifier to be instantiated. In this example, we used the two terms (f x) and (f y). So for every pair of occurrences of f in the current context, the axiom will instantiate the axiom. By the way, the axiom for injectivity is not the best one. It introduces a quadratic number of instances. A better axiom and pattern is:

  (BG_PUSH (FORALL (x) (PATS (f x)) (EQ (g (f x)) x)))

There is only a single pattern, consisting of the sub-term (f x). The axiom implies that f is injective because it says that g is an inverse function on the range of f. In general, quantifiers can be specified using the syntax:

  ((FORALL | EXISTS) (bound-id*) ((SKOLEMID id-or-num) | (QID id-or-num) | (PATS pattern*) | (NOPATS term*))* body)

  pattern ::= term | (MPAT term*) | PROMOTE

  bound-id ::= id [TYPE id]

  id-or-num ::= id | numeral

The keyword PROMOTE is used for controlling the weight of a quantifier. Promoted quantifiers are instantiated more eagerly than non-promoted quantifiers (using the default /mam command-line settings for the matching engine). The keyword SKOLEMID is used to supply a name-prefix for the skolem constants that are introduced if the quantifier gets skolemized. This happends when the quantifier
is asserted with existential force. For example

   (BG_PUSH (EXISTS (x) (SKOLEMID icecream) (EQ @true (LIKES x))))

introduces an existential force quantified formula that can be instantiated by a fresh constant. A model for the predicate likes will evaluate to true on this fresh constant. Z3 will generate a fresh name including the string icecream when creating this fresh constant.

z3.exe /m PARTIAL_MODELS=true icecream.smp
1: Invalid.
Counterexample:
partitions:
*2 {@true} -> 0:int
*3 {x.sk.icecream.0} -> 1:int
function interpretations:
LIKES -> {
  *3 -> *2
  else -> #unspecified
}

The keyword QID is used for identifying when and how often a quantifier is instantiated. The keyword NOPATS can be used to exclude a sub-term of the quantified formula body from being used as a pattern. Use NOPATS when no other patterns have been supplied.