Z3 contains an extension called muZ with fixed-point constraints.
This tutorial includes some examples that demonstrate features of this engine.
The following papers
μZ - An Efficient Engine for Fixed-Points with Constraints.
(CAV 2011) and
Generalized Property Directed Reachability (SAT 2012)
describe some of the main features of the engine.
Be sure to follow along with the examples by clicking the "edit" link in the
corner. See what the tool says, try your own formulas, and experiment!
Please send feedback, comments and/or corrections to
nbjorner@microsoft.com.
Introduction
This tutorial covers some of the fixedpoint utilities available with Z3.
The main features are a basic Datalog engine, an engine with relational
algebra and an engine based on a generalization of the Property
Directed Reachability algorithm, as well as the
Duality engine.
Basic Datalog
The default fixed-point engine is a bottom-up Datalog engine.
It works with finite relations and uses finite table representations
as hash tables as the default way to represent finite relations.
Relations, rules and queries
The first example illustrates how to declare relations, rules and
how to pose queries.
The example illustrates some of the basic constructs.
declares a 0-ary relation a.
Create the rule that a follows from b.
In general you can create a rule with multiple premises and a name using
the format
The name is optional. It is used for tracking the rule in derivation proofs.
Continuing with the example, a is false unless b is established.
Asks if relation a can be derived. The rules so far say that a
follows if b is established and that b follows if c
is established. But nothing establishes c and b is also not
established, so a cannot be derived.
Now it is the case that a can be derived.
Relations with arguments
Relations can take arguments. We illustrate relations with arguments
using edges and paths in a graph.
The example uses the declaration
to instrument the fixed-point engine that a
should be treated as a variable
appearing in rules.
Engine for Property Directed Reachability
A different underlying engine for fixed-points is based on
an algorithm for Property Directed Reachability (PDR).
The PDR engine is used by default for relations over integers, reals
and algebraic data-types.
The version in Z3 applies to Horn clauses with arithmetic and
Boolean domains.
The engine also works with domains using algebraic
data-types and bit-vectors, although it is currently not
overly tuned for either.
The PDR engine is targeted at applications from symbolic model
checking of software. The systems may be infinite state.
The following examples also serve a purpose of showing
how software model checking problems (of safety properties)
can be embedded into Horn clauses and solved using PDR.
Procedure Calls
McCarthy's 91 function illustrates a procedure that calls itself recursively
twice. The Horn clauses below encode the recursive function:
The general scheme for encoding recursive procedures is by creating a predicate
for each procedure and adding an additional output variable to the predicate.
Nested calls to procedures within a body can be encoded as a conjunction
of relations.
The first two queries are unsatisfiable. The PDR engine produces the same proof of unsatisfiability.
The proof is an inductive invariant for each recursive predicate.
Traffic Jam
A self-contained example that exercises the .NET API over C# is provided as a
separate download.
Syntax
Three different text-based input formats are accepted.
Basic datalog
Files with suffix .datalog are parsed using the BDDBDDB format.
The format can be used for comparing benchmarks with the BDDBDDB tool.
We use an artificial program to illustrate the basic Datalog format that complies to the format used by BDDBDDB.
SMT-LIB2 extension
The following commands are added to the SMT-LIB2 syntax:
(declare-var [var] [sort]) Declare a variable that is universally quantified in Horn clauses.
(declare-rel [relation-name] ([sorts])) Declare relation signature. Relations are uninterpreted.
(rule [universal-horn-formula]) Assert a rule or a fact as a universally quantified Horn formula.
(query [relation-name]) Pose a query. Is the relation non-empty.
(set-predicate-representation [function-name] [symbol]+) Specify the representation of a predicate.
Pure SMT-LIB2
Many problems about program safety can be reduced to pure
Horn clause satisfiability modulo theories (typically of arithmetic).
These problems are expressible directly in SMT-LIB2.
The repository Horn clause benchmarks in SMT-LIB2
contains more than 10,000 samples taken from different benchmarks and different encodings of the same benchmarks.
An assertion is Horn if it is an implication; the head of the implication
is either a formula using only interpreted functions, or it is an uninterpreted
predicate; the body of the implication is a formula in negation normal form
where the uninterpreted predicates occur positively.
Note the following:
To ensure that the fixedpoint engine is used, specify (set-logic HORN)
There is no separate query. Instead, queries correspond to Horn clause that have
no positive occurrence of any uninterpreted relation.
Programmatic API
You can interact with muZ over the programmatic API from Python, C, OCaml, Java, and .NET.
The APIs support adding rules and posing queries.