Java API Reference - Z3 Theorem Prover

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.

class

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

Solver

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

Params

Create a parameter set for configuring solvers and tactics.

Solver

Incremental satisfiability solver.

class

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.

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, 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.

abstract class

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.

class extends 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(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).

abstract class extends Expr

Base for IntExpr and RealExpr.

IntExpr

Integer expressions.

class extends ArithExpr

Represents integer terms.

IntExpr

Create integer constants.

IntExpr mkInt(int value)
IntExpr mkInt(long value)
IntExpr mkInt(String numeral)

IntExpr

Create integer variables.

IntExpr mkIntConst(String name)
IntExpr mkIntConst(Symbol name)

RealExpr

Real (rational) expressions.

class extends 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)

Arithmetic Operations

ArithExpr

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

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

BitVecExpr

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

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
    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)

BoolExpr

Create existential quantifier (same signature as mkForall).

Pattern

Create a pattern (trigger) for quantifiers.

Pattern mkPattern(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)
    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

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

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

class

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"

class

Symbol mkSymbol(String name)        // Create string symbol
Symbol mkSymbol(int i)              // Create integer symbol

class

Sort getIntSort()                   // Get integer sort
Sort getRealSort()                  // Get real sort
Sort getBoolSort()                  // Get boolean sort
Sort getStringSort()                // Get string sort

SMT-LIB Parsing

BoolExpr[]

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)

BoolExpr[]

Parse SMT-LIB2 format file (same parameters as parseSMTLIB2String).

Exception Handling

class extends Exception

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

​Core Classes

​Context

​Solver

​Status

​Model

​Expression Classes

​Expr

​BoolExpr

​ArithExpr

​IntExpr

​RealExpr

​Arithmetic Operations

​Comparison Operations

​Bit-Vector Operations

​Array Operations

​Quantifiers

​Datatypes

​Tactics and Goals

​Optimization

​Utilities

​SMT-LIB Parsing

​Exception Handling

​Best Practices

Use Try-With-Resources

Check Status First

Enable Model Generation

Use Typed Expressions

​Resources

Official Java API Docs

Java Examples

Getting Started

Z3 Guide

Core Classes

Context

Solver

Status

Model

Expression Classes

Expr

BoolExpr

ArithExpr

IntExpr

RealExpr

Arithmetic Operations

Comparison Operations

Bit-Vector Operations

Array Operations

Quantifiers

Datatypes

Tactics and Goals

Optimization

Utilities

SMT-LIB Parsing

Exception Handling

Best Practices

Resources