The Z3 Constraint Solver, a developer perspective

Z3 is a high-performance SMT solver developed at Microsoft Research. It have been integrated with many many tools that came out from Microsoft for program analysis, testing, and verification.

What SAT means ?

SAT refers to Boolean satisfiability problem where we want to determine if there exists an interpretation that satisfies a given Boolean formula. In other words, it establishes if the variables of a given Boolean formula can be assigned in such a way as to make the formula evaluate to true.

What SMT means ?

SMT stands for Satiability Modulo Theories. SMT instance is a formula in first-order logic, where some functions and predicates have additional interpretations. SMT problem is a decision problem of determining whether such a formula is satisfiable or not.

An SMT instance is a generalization of a Boolean SAT instance in which various sets of variables are replaced by predicates over a suitable set of non-binary variables.

These predicates are classified according to the theory they belong to. For instance, linear inequalities over real variables are evaluated using the rules of the theory of linear real arithmetic.

What SMT solver means ?

The goal of an SMT solver is to determine whether an SMT instance can evaluate to true or not. The same analog applies for SAT solvers.

SMT solvers

There is a lot of SMT solvers available but there is only one SMT solver with C# APIs, it is Z3. For a list of available SMT solvers, refer to this page.

Download Z3

You can download Z3 from http://z3.codeplex.com/ . I downloaded Z3 4.3.0 and extracted it to C:\z3.

C# Example

In the following example we going to let Z3 solve the following equation system:

• x > 0
• y = x + 1 
• y < 3

Solving the equations means finding values for x and y that make the whole formula evaluates to true.

• Let’s create a new console application project in Visual Studio.
• Add reference to Microsoft.Z3.dll which is located in the bin directory of the Z3 installation directory.
• Copy the file libz3.dll from the bin directory of the Z3 installation directory to your project build directory.
• Now edit your code to look like the following:

using System;
using Microsoft.Z3;

namespace Z3Demo1
{
    class Program
    {
        static void Main(string[] args)
        {
            using (Context ctx = new Context())
            {
                Expr x = ctx.MkConst("x", ctx.MkIntSort());
                Expr y = ctx.MkConst("y", ctx.MkIntSort());
                Expr zero = ctx.MkNumeral(0, ctx.MkIntSort());
                Expr one = ctx.MkNumeral(1, ctx.MkIntSort());
                Expr three = ctx.MkNumeral(3, ctx.MkIntSort());
                
                Solver s = ctx.MkSolver();
                s.Assert(ctx.MkAnd(ctx.MkGt((ArithExpr)x, (ArithExpr)zero), ctx.MkEq((ArithExpr)y, 
                    ctx.MkAdd((ArithExpr)x, (ArithExpr)one)), ctx.MkLt((ArithExpr)y, (ArithExpr)three)));
                Console.WriteLine(s.Check());

                Model m = s.Model;
                foreach (FuncDecl d in m.Decls)
                        Console.WriteLine(d.Name + " -> " + m.ConstInterp(d));
                    
                Console.ReadLine();
            }
        }
    }
}

Now let’s run the code above and see the output. The solver says the equation system is satisfiable and then gives us the x and y values that satisfy.

How it works ?

To interact with Z3 through C#, you need a Context object. Variables and numerals in your equations are modeled as Expr objects. You get these objects using member functions in the Context object (MkConts(), MkNumeral(),….). You construct your operand using member functions in the Context object (MkGt(), MkAdd(), MkLt(),…). To solve all the equations together you need to hock them up using AND operator, which is implemented using Context.MkAnd(). After hocking everything in one AND, you pass that the solver through Solver.Assert(). And as you may guessed, you obtain this Solver using Context.MkSolver().

Solver.Check() will tell you whether this equation system can be solved or not. To get the variables’ assignments that the come up with, get a Model object Solver.Model. Then use the Delcs collection to get all symbols that have an interpretation in the model. Model.ConstInterp() will get the symbol assigned value.

In this post we briefly introduced SAT, SMT, and their solvers. Then we explored the only SMT solver that written in C# and had a C# API. Now you can play with as many equations as you want and check them for satisfiability and even got the solution values.