Quantifiers
Z3 is a decision procedure for the combination of the previous quantifier-free theories. That is, it can answer whether a quantifier-free formula, modulo the theories referenced by the formula, is satisfiable or whether it is unsatisfiable. Z3 also accepts and can work with formulas that use quantifiers. It is no longer a decision procedure for such formulas in general (and for good reasons, as there can be no decision procedure for first-order logic).
Nevertheless, Z3 is often able to handle formulas involving quantifiers. It uses several approaches to handle quantifiers. The most prolific approach is using pattern-based quantifier instantiation. This approach allows instantiating quantified formulas with ground terms that appear in the current search context based on pattern annotations on quantifiers. The pattern-based instantiation method is quite effective, even though it is inherently incomplete.
Z3 also contains a model-based quantifier instantiation component that uses a model construction to find good terms to instantiate quantifiers with; and Z3 also handles many decidable fragments.
Modeling with Quantifiers
Suppose we want to model an object oriented type system with single inheritance. We would need a predicate for sub-typing. Sub-typing should be a partial order, and respect single inheritance. For some built-in type constructors, such as for array-of, sub-typing should be monotone.
Raymond Smullyan's puzzles are famous logical brain teasers. You can use predicate logic to encode and solve these. On a fictional island, all inhabitants are either knights, who always tell the truth, or knaves, who always lie. John and Bill are residents of the island of knights and knaves.
Another related Smullyan puzzle asks John and Bill are standing at a fork in the road. You know that one of them is a knight and the other a knave, but you don't know which. You also know that one road leads to Death, and the other leads to Freedom. By asking one yes/no question, can you determine the road to Freedom? We leave solving this puzzle as an exercise. You can either provide a direct answer and check it, or create a search space of abstract syntax, create an interpreter for the syntax and have z3 search for the question.
Patterns
The Stanford Pascal verifier and the subsequent Simplify theorem prover pioneered the use of pattern-based quantifier instantiation. The basic idea behind pattern-based quantifier instantiation is in a sense straight-forward. Annotate a quantified formula using a pattern that contains all the bound variables. So a pattern is an expression (that does not contain binding operations, such as quantifiers) that contains variables bound by a quantifier. Then instantiate the quantifier whenever a term that matches the pattern is created during search. This is a conceptually easy starting point, but there are several subtleties that are important.
In the following example, the first two options make sure that Model-based quantifier instantiation and saturation engines are disabled. We also annotate the quantified formula with the pattern (f (g x)). Since there is no ground instance of this pattern, the quantifier is not instantiated, and Z3 fails to show that the formula is unsatisfiable.
When the more permissive pattern (g x) is used. Z3 proves the formula to be unsatisfiable. More restrictive patterns minimize the number of instantiations (and potentially improve performance), but they may also make Z3 less complete.
Some patterns may also create long instantiation chains. Consider the following assertion.
(assert (forall (x Type) (y Type) (! (= (subtype x y) (subtype (array-of x) (array-of y))) :pattern ((subtype x y)) ))
The axiom gets instantiated whenever there is some ground term of the form (subtype s t). The instantiation causes a fresh ground term (subtype (array-of s) (array-of t)), which enables a new instantiation. This undesirable situation is called a matching loop. Z3 uses many heuristics to break matching loops.
Before elaborating on the subtleties, we should address an important first question. What defines the terms that are created during search? In the context of most SMT solvers, and of the Simplify theorem prover, terms exist as part of the input formula, they are of course also created by instantiating quantifiers, but terms are also implicitly created when equalities are asserted. The last point means that terms are considered up to congruence and pattern matching takes place modulo ground equalities. We call the matching problem E-matching. For example, if we have the following equalities
The terms (f a) and (f (g b)) are equal modulo the equalities. The pattern (f (g x)) can be matched and x bound to b (and the equality (= (f (g b)) b) is deduced.
While E-matching is an NP-complete problem, the main sources of overhead in larger verification problems comes from matching thousands of patterns in the context of an evolving set of terms and equalities. Z3 integrates an efficient E-matching engine using term indexing techniques.
Multi-patterns
In some cases, there is no pattern that contains all bound variables and does not contain interpreted symbols. In these cases, we use multi-patterns. In the following example, the quantified formula states that f is injective. This quantified formula is annotated with the multi-pattern (f x) (f y)
The quantified formula is instantiated for every pair of occurrences of f. A simple trick allows formulating injectivity of f in such a way that only a linear number of instantiations is required. The trick is to realize that f is injective if and only if it has a partial inverse.
No patterns
The annotation no-pattern can be used to instrument Z3 not to use a certain sub-expression as a pattern. The pattern inference engine may otherwise choose arbitrary sub-expressions as patterns to direct quantifier instantiation.
Model-based Quantifier Instantiation
The model-based quantifier instantiation (MBQI) is essentially a counter-example based refinement loop, where candidate models are built and checked. When the model checking step fails, it creates new quantifier instantiations. The models are returned as simple functional programs. In the following example, the model provides an interpretation for function f and constants a and b. One can easily check that the returned model does indeed satisfy the quantifier.
The command eval evaluates an expression in the last model produced by Z3. It is essentially executing the function program produced by Z3.
MBQI is a decision procedure for several useful fragments. It may find models even for formulas that are not in any of these fragments. We describe some of these fragments.
Effectively Propositional
The effectively propositional class of formulas (aka The Bernays-Schonfinkel class) is a decidable fragment of first-order logic formulas. It corresponds to formulas which, when written in prenex normal form contain only constants, universal quantifiers, and functions that return Boolean values (aka predicates).
Problems arising from program verification often involve establishing facts of quantifier-free formulas, but the facts themselves use relations and functions that are conveniently axiomatized using a background theory that uses quantified formulas. One set of examples of this situation comprise of formulas involving partial-orders. The following example axiomatizes a subtype partial order relation that has the tree property. That is, if x and y are subtypes of z, then x is a subtype of y or y is a subtype of x. The option (set-option :model.compact true) instructs Z3 to eliminate trivial redundancies from the generated model. In this example, Z3 also creates a finite interpretation for the uninterpreted sort T.
Note that it uses two auxiliary functions (subtype!25 and k!24) that were not part of your formula. They are auxiliary definitions created by Z3 during the model construction procedure. We can also ask questions by using the eval command. For example,
(eval (subtype int-type complex-type))
executes (evaluates) the given expression using the produced functional program (model).
Constraints over sets (Boolean Algebras) can be encoded into this fragment by treating sets as unary predicates and lifting equalities between sets as formula equivalence.
Stratified Sorts Fragment
The stratified sorts fragment is another decidable fragment of many sorted first-order logic formulas. It corresponds to formulas which, when written in prenex normal form, there is a function level from sorts to naturals, and for every function
declare-fun f (S_1 ... S_n) R)
level(R) level(S_i).
Array Property Fragment
The array property fragment can encode properties about uni-dimensional, and is strong enough to say an array is sorted. More information about this fragment can be found in the paper What's Decidable About Arrays.
(set-option :smt.mbqi true) (set-option :model.compact true)
List Fragment
The list fragment can encode properties about data-structures such as lists. For each quantified axiom q in this fragment, there is an easy way to satisfy q. More information about this fragment can be found in the paper Data Structure Specifications via Local Equality Axioms.
Essentially (Almost) Uninterpreted Fragment
The essentially almost uninterpreted fragment subsumes the previous fragments, and uses a more relaxed notion of stratification. More information about this fragment can be found in the paper Complete instantiation for quantified formulas in Satisfiability Modulo Theories. The model based quantifier instantiation approach used in Z3 is also described in this paper. Stratified data-structures (such as arrays of pointers) can be encoded in this fragment.
Shifts on streams (or arrays) can also be encoded.
Quantified Bit-Vector Formulas
A quantified bit-Vector formula (QBVF) is a many sorted first-order logic formula where the sort of every variable is a bit-vector sort. The QBVF satisfiability problem, is the problem of deciding whether a QBVF is satisfiable modulo the theory of bit-vectors. This problem is decidable because every universal (existential) quantifier can be expanded into a conjunction (disjunction) of potentially exponential, but finite size. A distinguishing feature in QBVF is the support for uninterpreted function and predicate symbols. More information about this fragment can be found in the paper Efficiently Solving Quantified Bit-Vector Formulas.
Conditional (and Pseudo) Macros
Quantifiers defining macros are also automatically detected by the Model Finder. In the following example, the first three quantifiers are defining f by cases.
My formula is not in any of the fragments above
Even if your formula is not in any of the fragments above. Z3 may still find a model for it. For example, The following simple example is not in the fragments described above.
The Z3 preprocessor has many options that may improve the performance of the model finder. In the following example, macro-finder will expand quantifiers representing macros at preprocessing time.
It is very effective in this benchmark since it contains many quantifiers of the form
forall x. p(x) = ....
The Z3 model finder is more effective if the input formula does not contain nested quantifiers. If that is not the case for your formula, you can use the option
(set-option :smt.pull-nested-quantifiers true)
The following challenge problem from the paper SEM a system for enumerating models is proved to be unsatisfiable in less than one second by Z3.
Quantifier reasoning is undecidable. Z3 attempts to find a refutation or a finite model of quantified formulas. When formulas are satisfiable but have no finite models, z3 will likely diverge. The following example illustrates a formula that only has infinite models.