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.
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
Create a new solver instance. Solver MkSolver () Solver MkSolver( Symbol logic ) // For specific logic Solver MkSolver( Tactic t ) // Using a tactic
Create a parameter set for configuring solvers and tactics.
Release all resources. Called automatically with using statement.
Solver Incremental satisfiability solver.
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.
Status . SATISFIABLE // Formula is satisfiable Status . UNSATISFIABLE // Formula is unsatisfiable Status . UNKNOWN // Result is unknown
Model A satisfying assignment for constraints.
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.
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.
Represents Boolean formulas.
Create the true constant. Create the false constant. Create a Boolean variable. BoolExpr MkBoolConst ( string name ) BoolExpr MkBoolConst( Symbol name )
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.
Base for IntExpr and RealExpr.
IntExpr Integer expressions.
Represents integer terms.
Create integer constants. IntExpr MkInt ( int value ) IntExpr MkInt( long value ) IntExpr MkInt( uint value ) IntExpr MkInt( ulong value ) IntExpr MkInt( string numeral )
Create integer variables. IntExpr MkIntConst ( string name ) IntExpr MkIntConst( Symbol name )
RealExpr Real (rational) expressions.
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"
Create real variables. RealExpr MkRealConst ( string name ) RealExpr MkRealConst( Symbol name )
IntNum and RatNum Numeric value classes.
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
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 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 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 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 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 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 )
Create existential quantifier (same signature as MkForall).
Create a pattern (trigger) for quantifiers. Pattern MkPattern ( params Expr [] terms )
Datatypes // 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 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 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
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) 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 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 )
Parse SMT-LIB2 format file (same parameters).
Exception Handling 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
