This site uses cookies for analytics, personalized content and ads. By continuing to browse this site, you agree to this use. Learn more

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.

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.

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.

(declare-rel a ()) (declare-rel b ()) (declare-rel c ()) (rule (=> b a)) (rule (=> c b)) (set-option :fixedpoint.engine datalog) (query a) (rule c) (query a :print-answer true)The example illustrates some of the basic constructs.

(declare-rel a ())declares a 0-ary relation

(rule (=> b a))Create the rule that

(rule (=> (and b c) a) name)The

(query r)Asks if relation

(rule c)Now it is the case that

Relations can take arguments. We illustrate relations with arguments using edges and paths in a graph.

load in editor(set-option :fixedpoint.engine datalog) (define-sort s () (_ BitVec 3)) (declare-rel edge (s s)) (declare-rel path (s s)) (declare-var a s) (declare-var b s) (declare-var c s) (rule (=> (edge a b) (path a b))) (rule (=> (and (path a b) (path b c)) (path a c))) (rule (edge #b001 #b010)) (rule (edge #b001 #b011)) (rule (edge #b010 #b100)) (declare-rel q1 ()) (declare-rel q2 ()) (declare-rel q3 (s)) (rule (=> (path #b001 #b100) q1)) (rule (=> (path #b011 #b100) q2)) (rule (=> (path #b001 b) (q3 b))) (query q1) (query q2) (query q3 :print-answer true)The example uses the declaration

(declare-var a s)to instrument the fixed-point engine that

McCarthy's 91 function illustrates a procedure that calls itself recursively twice. The Horn clauses below encode the recursive function:

mc(x) = if x > 100 then x - 10 else mc(mc(x+11))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. load in editor

(declare-rel mc (Int Int)) (declare-var n Int) (declare-var m Int) (declare-var p Int) (rule (=> (> m 100) (mc m (- m 10)))) (rule (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n))) (declare-rel q1 (Int Int)) (rule (=> (and (mc m n) (< n 91)) (q1 m n))) (query q1 :print-certificate true) (declare-rel q2 (Int Int)) (rule (=> (and (mc m n) (not (= n 91)) (<= m 101)) (q2 m n))) (query q2 :print-certificate true) (declare-rel q3 (Int Int)) (rule (=> (and (mc m n) (< n 92)) (q3 m n))) (query q3 :print-certificate true)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.

A self-contained example that exercises the .NET API over C# is provided as a separate download.

Three different text-based input formats are accepted.

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.

Z 64 P0(x: Z) input Gt0(x : Z, y : Z) input R(x : Z) printtuples S(x : Z) printtuples Gt(x : Z, y : Z) printtuples Gt(x,y) :- Gt0(x,y). Gt(x,y) :- Gt(x,z), Gt(z,y). R(x) :- Gt(x,_). S(x) :- Gt(x,x0), Gt0(x,y), Gt0(y,z), P0(z). Gt0("a","b"). Gt0("b","c"). Gt0("c","d"). Gt0("a1","b"). Gt0("b","a1"). Gt0("d","d1"). Gt0("d1","d"). P0("a1").

`(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.

(set-logic HORN) (declare-fun mc (Int Int) Bool) (assert (forall ((m Int)) (=> (> m 100) (mc m (- m 10))))) (assert (forall ((m Int) (n Int) (p Int)) (=> (and (<= m 100) (mc (+ m 11) p) (mc p n)) (mc m n)))) (assert (forall ((m Int) (n Int)) (=> (and (mc m n) (<= m 101)) (= n 91)))) (check-sat) (get-model)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.

You can interact with muZ over the programmatic API from Python, C, OCaml, Java, and .NET. The APIs support adding rules and posing queries.

- To add a rule, call: Z3_fixedpoint_add_rule.
- To query, use: Z3_fixedpoint_query.