API Reference - Z3 Theorem Prover

Z3’s JavaScript bindings provide two APIs:

High-Level API: Z3Py-like object-oriented interface (recommended)
Low-Level API: Direct C API bindings

This reference covers the high-level API. For the low-level API, see the C API documentation.

Initialization

init()

Initializes the Z3 WebAssembly module.

function init(): Promise<{ 
  Context: ContextCtor, 
  em: EmscriptenModule,
  Z3: Z3LowLevel 
}>

Returns: Promise resolving to:

Context: High-level API context constructor
em: Emscripten module for advanced control
Z3: Low-level C-like API

Example:

const { Context, em, Z3 } = await init();

Context

Creates an isolated Z3 context. All operations must use objects from the same context.

Context(name)

function Context<Name extends string>(name: Name): Z3Context<Name>

Parameters:

name: String identifier for type safety (TypeScript only)

Returns: Object containing all Z3 operations and types Example:

const { Int, Real, Bool, Solver, Tactic } = new Context('main');

Sorts (Types)

Z3 sorts represent the types of expressions.

Integer and Real

Int

Sort

Integer arithmetic sort

Real

Sort

Real arithmetic sort

Methods:

Int.const(name: string): Create integer variable
Int.val(value: number | bigint): Create integer constant
Real.const(name: string): Create real variable
Real.val(numerator: number, denominator?: number): Create rational constant

Boolean

Bool

Sort

Boolean sort for true/false values

Methods:

Bool.const(name: string): Create boolean variable
Bool.val(value: boolean): Create boolean constant

Bit-Vectors

BitVec

Sort

Fixed-width bit-vector sort

Methods:

BitVec.const(name: string, bits: number): Create bit-vector variable
BitVec.val(value: number | bigint, bits: number): Create bit-vector constant

Example:

const x = BitVec.const('x', 8);  // 8-bit vector
const ff = BitVec.val(255, 8);   // value 255 as 8-bit

Arrays

Array

Sort

Array sort with index and value types

Methods:

Array.sort(indexSort: Sort, valueSort: Sort): Create array sort
Array.const(name: string, indexSort: Sort, valueSort: Sort): Create array variable
Array.K(domain: Sort, value: Expr): Create constant array

Example:

const arr = Array.const('arr', Int.sort(), Int.sort());
const constantArr = Array.K(Int.sort(), Int.val(42));

Expressions

All Z3 values and formulas are expressions.

Arithmetic Operations

add

method

Addition: a.add(b, c, ...)Supports multiple arguments for efficiency.

sub

method

Subtraction: a.sub(b)

mul

method

Multiplication: a.mul(b, c, ...)

div

method

Division: a.div(b)Integer division for Int, real division for Real.

mod

method

Modulo: a.mod(b)Integer expressions only.

pow

method

Power: a.pow(b)

Example:

const x = Int.const('x');
const y = Int.const('y');
const expr = x.mul(2).add(y).sub(5); // 2*x + y - 5

Comparison Operations

method

Equality: a.eq(b)Returns boolean expression.

neq

method

Inequality: a.neq(b)Equivalent to Not(a.eq(b)).

method

Less than: a.lt(b)

method

Less than or equal: a.le(b)

method

Greater than: a.gt(b)

method

Greater than or equal: a.ge(b)

Boolean Operations

These are provided as both methods and standalone functions:

And

function

Conjunction: And(a, b, c, ...)Returns true if all arguments are true.

function

Disjunction: Or(a, b, c, ...)Returns true if any argument is true.

Not

function

Negation: Not(a)

Implies

function

Implication: Implies(a, b)Equivalent to Or(Not(a), b).

Iff

function

If-and-only-if: Iff(a, b)True when both have same truth value.

Xor

function

Exclusive or: Xor(a, b)

Example:

const p = Bool.const('p');
const q = Bool.const('q');
const formula = And(
  Or(p, q),
  Not(And(p, q))
); // (p ∨ q) ∧ ¬(p ∧ q)

Bit-Vector Operations

bvadd

method

Bit-vector addition: a.add(b)

bvsub

method

Bit-vector subtraction: a.sub(b)

bvmul

method

Bit-vector multiplication: a.mul(b)

bvudiv

method

Unsigned division: a.udiv(b)

bvsdiv

method

Signed division: a.sdiv(b)

bvurem

method

Unsigned remainder: a.urem(b)

bvand

method

Bitwise AND: a.and(b)

bvor

method

Bitwise OR: a.or(b)

bvxor

method

Bitwise XOR: a.xor(b)

bvnot

method

Bitwise NOT: a.not()

bvshl

method

Shift left: a.shl(b)

bvlshr

method

Logical shift right: a.lshr(b)

bvashr

method

Arithmetic shift right: a.ashr(b)

Array Operations

select

method

Array read: arr.select(index)Returns value at index.

store

method

Array write: arr.store(index, value)Returns new array with updated value.

Example:

const arr = Array.const('arr', Int.sort(), Int.sort());
const i = Int.const('i');
const v = arr.select(i);  // arr[i]
const arr2 = arr.store(i, Int.val(42)); // arr[i := 42]

Solver

The solver checks satisfiability of constraints.

new Solver()

Creates a new solver instance.

class Solver<Name extends string> {
  add(...constraints: Bool<Name>[]): void;
  check(...assumptions: Bool<Name>[]): Promise<'sat' | 'unsat' | 'unknown'>;
  model(): Model<Name>;
  reset(): void;
  push(): void;
  pop(num?: number): void;
  toString(): string;
}

Methods

add

method

add(...constraints: Bool[]): void

Add constraints to the solver.Example:

solver.add(x.gt(0), y.lt(10));

check

method

check(...assumptions: Bool[]): Promise<'sat' | 'unsat' | 'unknown'>

Check satisfiability with optional assumptions.Returns:

'sat': Satisfiable (solution exists)
'unsat': Unsatisfiable (no solution)
'unknown': Solver could not determine

Example:

const result = await solver.check();
if (result === 'sat') {
  const model = solver.model();
}

model

method

model(): Model

Get the model (variable assignments) after a sat result.Throws: Error if called before check() or if result is not sat.

reset

method

reset(): void

Remove all constraints from the solver.

push

method

push(): void

Create a backtracking point.

pop

method

pop(num?: number): void

Backtrack to previous state.Parameters:

num: Number of scopes to pop (default: 1)

Example:

solver.add(x.gt(0));
solver.push();
solver.add(y.lt(10));
await solver.check(); // checks both constraints
solver.pop(); // removes y < 10
await solver.check(); // only checks x > 0

Model

Represents a solution (variable assignments).

Methods

eval

method

eval(expr: Expr, modelCompletion?: boolean): Expr

Evaluate expression in the model.Parameters:

expr: Expression to evaluate
modelCompletion: If true, assign default values to unbound variables (default: false)

Example:

const model = solver.model();
const xVal = model.eval(x);
console.log('x =', xVal.toString());

sexpr

method

sexpr(): string

Get S-expression representation of the model.Returns: SMT-LIB2 format string

toString

method

toString(): string

Get human-readable model representation.

Simplifier

Simplifiers preprocess expressions before solving.

new Simplifier(name)

class Simplifier<Name extends string> {
  constructor(name: string);
  andThen(other: Simplifier<Name>): Simplifier<Name>;
  usingParams(params: Params<Name>): Simplifier<Name>;
  help(): string;
  paramDescrs(): ParamDescrs<Name>;
}

Example:

const s1 = new Simplifier('solve-eqs');
const s2 = new Simplifier('simplify');
const composed = s1.andThen(s2);

solver.addSimplifier(composed);

Params

Parameter sets for configuring solvers and tactics.

new Params()

class Params<Name extends string> {
  set(key: string, value: boolean | number | string): void;
  toString(): string;
}

Example:

const params = new Params();
params.set('timeout', 5000);
params.set('max_steps', 1000);
params.set('elim_and', true);

Tactic

Tactics are solvers with specific strategies.

new Tactic(name)

class Tactic<Name extends string> {
  constructor(name: string);
  apply(goal: Goal<Name>): Promise<ApplyResult<Name>>;
  usingParams(params: Params<Name>): Tactic<Name>;
  andThen(other: Tactic<Name>): Tactic<Name>;
  orElse(other: Tactic<Name>): Tactic<Name>;
}

Common tactics:

'simplify': Simplify expressions
'solve-eqs': Solve equations
'qe': Quantifier elimination
'sat': SAT solver
'smt': SMT solver

Low-Level API

The low-level API provides direct access to Z3’s C API.

Differences from C API

Out Parameters

C functions with out parameters return objects:

// C: void Z3_rcf_get_numerator_denominator(ctx, a, &n, &d)
// JS:
const { n, d } = Z3.rcf_get_numerator_denominator(ctx, a);

Arrays

Array lengths are inferred:

// C: Z3_rcf_mk_roots(ctx, n, a, roots)
// JS:
const { rv, roots } = Z3.rcf_mk_roots(ctx, a);

Integers

JavaScript number for int, unsigned, float, double
JavaScript BigInt for int64_t, uint64_t

Null Pointers

Types ending in _opt accept/return null:

function model_get_const_interp(
  c: Z3_context, 
  m: Z3_model, 
  a: Z3_func_decl
): Z3_ast | null

Async Functions

Long-running operations are async:

Z3_simplify
Z3_solver_check
Z3_tactic_apply
And others (see installation page)

Example

const { Z3 } = await init();

const cfg = Z3.mk_config();
const ctx = Z3.mk_context(cfg);
Z3.del_config(cfg);

const intSort = Z3.mk_int_sort(ctx);
const x = Z3.mk_const(ctx, Z3.mk_string_symbol(ctx, 'x'), intSort);
const zero = Z3.mk_int(ctx, 0, intSort);
const constraint = Z3.mk_gt(ctx, x, zero);

const solver = Z3.mk_solver(ctx);
Z3.solver_assert(ctx, solver, constraint);

const result = await Z3.solver_check(ctx, solver);
console.log(result); // Z3_L_TRUE (1)

Type Definitions

Full TypeScript definitions are included:

import type {
  Context,
  Solver,
  Model,
  Expr,
  Arith,
  Bool,
  BitVec,
  Tactic,
  Simplifier,
  Params,
  Sort,
} from 'z3-solver';

Getting Started

Practical examples and tutorials

C API Docs

Low-level C API reference

TypeDoc

Auto-generated API documentation

GitHub Examples

More code examples

Python

C++

C

Java

.NET

JavaScript/TypeScript

Go

OCaml

​Initialization

​init()

​Context

​Context(name)

​Sorts (Types)

​Integer and Real

​Boolean

​Bit-Vectors

​Arrays

​Expressions

​Arithmetic Operations

​Comparison Operations

​Boolean Operations

​Bit-Vector Operations

​Array Operations

​Solver

​new Solver()

​Methods

​Model

​Methods

​Simplifier

​new Simplifier(name)

​Params

​new Params()

​Tactic

​new Tactic(name)

​Low-Level API

​Differences from C API

​Example

​Type Definitions

​Further Reading

Getting Started

C API Docs

TypeDoc

GitHub Examples

Build docs developers (and LLMs) love

Initialization

init()

Context

Context(name)

Sorts (Types)

Integer and Real

Boolean

Bit-Vectors

Arrays

Expressions

Arithmetic Operations

Comparison Operations

Boolean Operations

Bit-Vector Operations

Array Operations

Solver

new Solver()

Methods

Model

Methods

Simplifier

new Simplifier(name)

Params

new Params()

Tactic

new Tactic(name)

Low-Level API

Differences from C API

Example

Type Definitions

Further Reading