The Z3 Java API provides an object-oriented interface to Z3. All classes are in the com.microsoft.z3 package.
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. // Constructor Context () Context ( HashMap < String, String > settings) // Configuration 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 (e.g., QF_LIA) Solver mkSolver ( Tactic t) // Using a tactic
Create a parameter set for configuring solvers and tactics.
Solver Incremental satisfiability solver.
Main interface for checking satisfiability. void add ( BoolExpr ... constraints ) // Add constraints void add ( BoolExpr constraint) // Add single constraint Status check () // Check satisfiability Status check ( Expr ... assumptions ) // Check with assumptions Model getModel () // Get model (if SAT) Expr [] getUnsatCore () // Get unsat core (if UNSAT) void push () // Create backtracking point void pop () // Backtrack void pop ( int n) // Backtrack n scopes void reset () // Reset solver
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, boolean modelCompletion) // Evaluate expression FuncDecl [] getConstDecls () // Get all constants FuncDecl [] getFuncDecls () // Get all functions Expr getConstInterp ( FuncDecl decl) // Get constant value FuncInterp getFuncInterp ( FuncDecl decl) // Get function interpretation String toString () // String representation
Expression Classes Expr Base class for all expressions.
Sort getSort () // Get the sort (type) of expression boolean isConst () // Check if constant boolean isInt () // Check if integer boolean isBool () // Check if boolean String toString () // String representation String getSExpr () // 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 ( BoolExpr ... args ) BoolExpr mkOr ( 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 (Int and Real).
ArithExpr
abstract class extends Expr
Base for IntExpr and RealExpr.
IntExpr Integer expressions.
Represents integer terms.
Create integer constants. IntExpr mkInt ( int value) IntExpr mkInt ( long 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)
Arithmetic Operations ArithExpr mkAdd ( ArithExpr ... args ) // Addition ArithExpr mkSub ( ArithExpr ... args ) // Subtraction ArithExpr mkMul ( 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 ( 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 ( int size) // Create BV sort BitVecExpr mkBV ( int value, int size) // Create BV constant BitVecExpr mkBVConst ( String name, int 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 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 int weight, // Weight (for instantiation) Pattern [] patterns, // Patterns (triggers) Expr [] noPatterns, // No-patterns Symbol quantifierID, // Quantifier ID Symbol skolemID // Skolem ID ) // Simplified version BoolExpr mkForall ( Expr [] boundVars, BoolExpr body, int weight, Pattern [] patterns, Expr [] noPatterns, Symbol qid, Symbol skid)
Create existential quantifier (same signature as mkForall).
Create a pattern (trigger) for quantifiers. Pattern mkPattern ( 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) int [] 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 ( Tactic ... tactics ) // Sequential composition Tactic orElse ( Tactic t1, Tactic t2) // Try t1, if fails use t2 Tactic repeat ( Tactic t, int max) // Repeat tactic Tactic tryFor ( Tactic t, int ms) // Run with timeout Goal mkGoal ( boolean models, boolean unsatCores, boolean proofs) ApplyResult apply ( Tactic t, Goal g) // Apply tactic to goal
Optimization Optimize mkOptimize () // Create optimizer void add ( BoolExpr ... constraints ) // Add constraints Optimize . Handle maximize ( ArithExpr obj) // Maximize objective Optimize . Handle minimize ( ArithExpr obj) // Minimize objective Status check () // Check and optimize Model getModel () // Get optimal model
Utilities static int getMajor () static int getMinor () static int getBuildNumber () static int getRevisionNumber () static String getFullVersion () // "4.x.x.x" static String getString () // "Z3 4.x.x"
Symbol mkSymbol ( String name) // Create string symbol Symbol mkSymbol ( int i) // Create integer symbol
Sort getIntSort () // Get integer sort Sort getRealSort () // Get real sort Sort getBoolSort () // Get boolean sort Sort getStringSort () // Get string sort
SMT-LIB Parsing Parse SMT-LIB2 format string. BoolExpr [] parseSMTLIB2String ( String str, // SMT-LIB2 string Symbol [] sortNames, // Sort name bindings Sort [] sorts, // Sort values Symbol [] declNames, // Declaration name bindings FuncDecl [] decls // Declaration values ) // Simple version BoolExpr [] parseSMTLIB2String ( String str)
Parse SMT-LIB2 format file (same parameters as parseSMTLIB2String).
Exception Handling Exception thrown by Z3 operations. try { // Z3 operations } catch ( Z3Exception e ) { System . err . println ( "Z3 error: " + e . getMessage ()); }
Best Practices
Use Try-With-Resources Always use try-with-resources for Context to ensure cleanup. try ( Context ctx = new Context ()) { // Use Z3 }
Check Status First Always check solver status before accessing results. if ( solver . check () == Status . SATISFIABLE ) { Model m = solver . getModel (); }
Enable Model Generation Set configuration if you need models. HashMap < String , String > cfg = new HashMap <>(); cfg . put ( "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 Java API Docs Complete Javadoc documentation
Java Examples Example programs on GitHub
Getting Started Learn the basics
Z3 Guide Interactive tutorial
