.NET API Reference - Z3 Theorem Prover

The Z3 .NET API provides a managed, object-oriented interface to Z3. All classes are in the Microsoft.Z3 namespace.

Core Classes

Context

The central class that manages all Z3 objects.

class : IDisposable

The main context class. All Z3 objects are created and managed through a context.

// Constructors
Context()
Context(Dictionary<string, string> settings)

// Common settings:
// "model" -> "true" | "false"    // Enable model generation
// "proof" -> "true" | "false"    // Enable proof generation
// "timeout" -> "milliseconds"    // Set timeout

Solver

Create a new solver instance.

Solver MkSolver()
Solver MkSolver(Symbol logic)      // For specific logic
Solver MkSolver(Tactic t)          // Using a tactic

Params

Create a parameter set for configuring solvers and tactics.

void

Release all resources. Called automatically with using statement.

Solver

Incremental satisfiability solver.

class

Main interface for checking satisfiability.

void Assert(params BoolExpr[] constraints)  // Add constraints
void Assert(BoolExpr constraint)            // Add single constraint
Status Check()                               // Check satisfiability
Status Check(params Expr[] assumptions)      // Check with assumptions
Model Model { get; }                         // Get model (if SAT)
Expr[] UnsatCore { get; }                    // Get unsat core (if UNSAT)
BoolExpr[] Assertions { get; }               // Get all assertions
void Push()                                  // Create backtracking point
void Pop()                                   // Backtrack
void Pop(uint n)                             // Backtrack n scopes
void Reset()                                 // Reset solver
string ReasonUnknown { get; }                // Reason for UNKNOWN result

Status

Enumeration for solver results.

enum

Status.SATISFIABLE      // Formula is satisfiable
Status.UNSATISFIABLE    // Formula is unsatisfiable
Status.UNKNOWN          // Result is unknown

Model

A satisfying assignment for constraints.

class

Expr Evaluate(Expr t)                        // Evaluate expression
Expr Evaluate(Expr t, bool completion)       // Evaluate with model completion
FuncDecl[] ConstDecls { get; }               // All constants
FuncDecl[] FuncDecls { get; }                // All functions
Expr ConstInterp(FuncDecl decl)              // Get constant value
FuncInterp FuncInterp(FuncDecl decl)         // Get function interpretation
uint NumConsts { get; }                      // Number of constants
uint NumFuncs { get; }                       // Number of functions
string ToString()                            // String representation

Expression Classes

Expr

Base class for all expressions.

abstract class

Sort Sort { get; }                  // Get the sort (type)
bool IsConst { get; }               // Check if constant
bool IsInt { get; }                 // Check if integer
bool IsBool { get; }                // Check if boolean
bool IsReal { get; }                // Check if real
ASTKind ASTKind { get; }            // Get AST kind
string ToString()                   // String representation
string SExpr()                      // S-expression representation

BoolExpr

Boolean expressions.

class : Expr

Represents Boolean formulas.

BoolExpr

Create the true constant.

BoolExpr MkTrue()

BoolExpr

Create the false constant.

BoolExpr MkFalse()

BoolExpr

Create a Boolean variable.

BoolExpr MkBoolConst(string name)
BoolExpr MkBoolConst(Symbol name)

BoolExpr

BoolExpr MkNot(BoolExpr a)
BoolExpr MkAnd(params BoolExpr[] args)
BoolExpr MkOr(params BoolExpr[] args)
BoolExpr MkImplies(BoolExpr t1, BoolExpr t2)
BoolExpr MkIff(BoolExpr t1, BoolExpr t2)
BoolExpr MkXor(BoolExpr t1, BoolExpr t2)

ArithExpr

Base class for arithmetic expressions.

abstract class : Expr

Base for IntExpr and RealExpr.

IntExpr

Integer expressions.

class : ArithExpr

Represents integer terms.

IntExpr

Create integer constants.

IntExpr MkInt(int value)
IntExpr MkInt(long value)
IntExpr MkInt(uint value)
IntExpr MkInt(ulong value)
IntExpr MkInt(string numeral)

IntExpr

Create integer variables.

IntExpr MkIntConst(string name)
IntExpr MkIntConst(Symbol name)

RealExpr

Real (rational) expressions.

class : ArithExpr

Represents real terms.

RealExpr

Create real constants.

RealExpr MkReal(int num, int den)     // Fraction
RealExpr MkReal(int value)
RealExpr MkReal(long value)
RealExpr MkReal(string numeral)       // "3.14" or "22/7"

RealExpr

Create real variables.

RealExpr MkRealConst(string name)
RealExpr MkRealConst(Symbol name)

IntNum and RatNum

Numeric value classes.

class : ArithExpr

int Int { get; }                    // Get int value
long Int64 { get; }                 // Get long value
uint UInt { get; }                  // Get uint value
ulong UInt64 { get; }               // Get ulong value
string ToString()                   // String representation

class : RealExpr

IntNum Numerator { get; }           // Get numerator
IntNum Denominator { get; }         // Get denominator
double ToDouble()                   // Convert to double (approximate)
string ToDecimalString(uint precision)  // Decimal string

Arithmetic Operations

ArithExpr

ArithExpr MkAdd(params ArithExpr[] args)          // Addition
ArithExpr MkSub(params ArithExpr[] args)          // Subtraction
ArithExpr MkMul(params ArithExpr[] args)          // Multiplication
ArithExpr MkDiv(ArithExpr t1, ArithExpr t2)       // Division
IntExpr MkMod(IntExpr t1, IntExpr t2)             // Modulo
IntExpr MkRem(IntExpr t1, IntExpr t2)             // Remainder
ArithExpr MkUnaryMinus(ArithExpr t)               // Negation
ArithExpr MkPower(ArithExpr t1, ArithExpr t2)     // Exponentiation

Comparison Operations

BoolExpr

BoolExpr MkEq(Expr t1, Expr t2)                   // Equality
BoolExpr MkDistinct(params Expr[] args)           // Pairwise distinct
BoolExpr MkLt(ArithExpr t1, ArithExpr t2)         // Less than
BoolExpr MkLe(ArithExpr t1, ArithExpr t2)         // Less than or equal
BoolExpr MkGt(ArithExpr t1, ArithExpr t2)         // Greater than
BoolExpr MkGe(ArithExpr t1, ArithExpr t2)         // Greater than or equal

Bit-Vector Operations

BitVecExpr

BitVecSort MkBitVecSort(uint size)              // Create BV sort
BitVecExpr MkBV(int value, uint size)           // Create BV constant
BitVecExpr MkBV(long value, uint size)
BitVecExpr MkBVConst(string name, uint size)    // Create BV variable

// Arithmetic
BitVecExpr MkBVAdd(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVSub(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVMul(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVSDiv(BitVecExpr t1, BitVecExpr t2)  // Signed division
BitVecExpr MkBVUDiv(BitVecExpr t1, BitVecExpr t2)  // Unsigned division

// Bitwise
BitVecExpr MkBVAND(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVOR(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVXOR(BitVecExpr t1, BitVecExpr t2)
BitVecExpr MkBVNot(BitVecExpr t)
BitVecExpr MkBVNeg(BitVecExpr t)

// Shifts and rotates
BitVecExpr MkBVSHL(BitVecExpr t1, BitVecExpr t2)   // Shift left
BitVecExpr MkBVLSHR(BitVecExpr t1, BitVecExpr t2)  // Logical shift right
BitVecExpr MkBVASHR(BitVecExpr t1, BitVecExpr t2)  // Arithmetic shift right

Array Operations

ArrayExpr

ArraySort MkArraySort(Sort domain, Sort range)    // Create array sort
ArrayExpr MkArrayConst(string name, Sort domain, Sort range)
ArrayExpr MkConstArray(Sort domain, Expr value)   // Constant array

Expr MkSelect(ArrayExpr a, Expr i)                // Array read: a[i]
ArrayExpr MkStore(ArrayExpr a, Expr i, Expr v)    // Array write: a[i] := v

Quantifiers

BoolExpr

Create universal quantifier.

BoolExpr MkForall(
    Expr[] boundVars,        // Quantified variables
    BoolExpr body,            // Body
    uint weight = 1,          // Weight (for instantiation)
    Pattern[] patterns = null,// Patterns (triggers)
    Expr[] noPatterns = null, // No-patterns
    Symbol quantifierID = null,
    Symbol skolemID = null
)

// Simplified version
BoolExpr MkForall(Expr[] boundVars, BoolExpr body)

BoolExpr

Create existential quantifier (same signature as MkForall).

Pattern

Create a pattern (trigger) for quantifiers.

Pattern MkPattern(params Expr[] terms)

Datatypes

DatatypeSort

// Create constructor
Constructor MkConstructor(
    Symbol name,              // Constructor name
    Symbol recognizer,        // Recognizer name (is_name)
    Symbol[] fieldNames,      // Field names
    Sort[] sorts,             // Field types (null for recursive)
    uint[] sortRefs           // References to other datatypes
)

// Create datatype
DatatypeSort MkDatatype(Symbol name, Constructor[] constructors)

// Create mutually recursive datatypes
Sort[] MkDatatypeSorts(Symbol[] names, Constructor[][] constructors)

Tactics and Goals

Tactic

Tactic MkTactic(string name)                    // Create tactic
Tactic AndThen(params Tactic[] tactics)         // Sequential composition
Tactic OrElse(Tactic t1, Tactic t2)            // Try t1, if fails use t2
Tactic Repeat(Tactic t, uint max = uint.MaxValue)
Tactic TryFor(Tactic t, uint ms)                // Run with timeout

Goal MkGoal(bool models = true, bool unsatCores = false, bool proofs = false)
ApplyResult Apply(Tactic t, Goal g)             // Apply tactic to goal

Optimization

Optimize

Optimize MkOptimize()                           // Create optimizer

void Assert(params BoolExpr[] constraints)      // Add constraints
Optimize.Handle Maximize(ArithExpr obj)         // Maximize objective
Optimize.Handle Minimize(ArithExpr obj)         // Minimize objective
Status Check()                                   // Check and optimize
Model Model { get; }                             // Get optimal model

Version Information

class

static int Major { get; }
static int Minor { get; }
static int Build { get; }
static int Revision { get; }
static string ToString()            // "4.x.x.x"

Sorts (Types)

class

Sort IntSort { get; }               // Get integer sort
Sort RealSort { get; }              // Get real sort
Sort BoolSort { get; }              // Get boolean sort
Sort StringSort { get; }            // Get string sort

Symbol MkSymbol(string name)        // Create string symbol
Symbol MkSymbol(int i)              // Create integer symbol

SMT-LIB Parsing

BoolExpr[]

Parse SMT-LIB2 format string.

BoolExpr[] ParseSMTLIB2String(
    string str,                     // SMT-LIB2 string
    Symbol[] sortNames = null,      // Sort name bindings
    Sort[] sorts = null,            // Sort values
    Symbol[] declNames = null,      // Declaration name bindings
    FuncDecl[] decls = null         // Declaration values
)

BoolExpr[]

Parse SMT-LIB2 format file (same parameters).

Exception Handling

class : Exception

Exception thrown by Z3 operations.

try
{
    // Z3 operations
}
catch (Z3Exception ex)
{
    Console.WriteLine($"Z3 error: {ex.Message}");
}

Best Practices

Use Using Statements

Always use using for Context to ensure cleanup.

using (Context ctx = new Context())
{
    // Use Z3
}

Check Status First

Always check solver status before accessing Model.

if (solver.Check() == Status.SATISFIABLE)
{
    Model m = solver.Model;
}

Enable Model Generation

Set configuration if you need models.

var cfg = new Dictionary<string, string>
{ { "model", "true" } };
Context ctx = new Context(cfg);

Use Typed Expressions

Prefer typed expressions for safety.

IntExpr x = ctx.MkIntConst("x");
// Better than:
Expr x = ctx.MkIntConst("x");

Resources

Official .NET API Docs

Complete API documentation

.NET Examples

Example programs on GitHub

Getting Started

Learn the basics

Z3 Guide

Interactive tutorial

​Core Classes

​Context

​Solver

​Status

​Model

​Expression Classes

​Expr

​BoolExpr

​ArithExpr

​IntExpr

​RealExpr

​IntNum and RatNum

​Arithmetic Operations

​Comparison Operations

​Bit-Vector Operations

​Array Operations

​Quantifiers

​Datatypes

​Tactics and Goals

​Optimization

​Version Information

​Sorts (Types)

​SMT-LIB Parsing

​Exception Handling

​Best Practices

Use Using Statements

Check Status First

Enable Model Generation

Use Typed Expressions

​Resources

Official .NET API Docs

.NET Examples

Getting Started

Z3 Guide

Core Classes

Context

Solver

Status

Model

Expression Classes

Expr

BoolExpr

ArithExpr

IntExpr

RealExpr

IntNum and RatNum

Arithmetic Operations

Comparison Operations

Bit-Vector Operations

Array Operations

Quantifiers

Datatypes

Tactics and Goals

Optimization

Version Information

Sorts (Types)

SMT-LIB Parsing

Exception Handling

Best Practices

Resources