Interface Solver<Name>

interface Solver<Name extends string = "main"> {
    ctx: Context<Name>;
    ptr: Z3_solver;
    add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void;
    addAndTrack(expr: Bool<Name>, constant: string | Bool<Name>): void;
    addSimplifier(simplifier: Simplifier<Name>): void;
    assertions(): AstVector<Name, Bool<Name>>;
    check(
        ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
    ): Promise<CheckSatResult>;
    congruenceExplain(
        a: Expr<Name, AnySort<Name>, unknown>,
        b: Expr<Name, AnySort<Name>, unknown>,
    ): Expr<Name, AnySort<Name>, unknown>;
    congruenceNext(
        expr: Expr<Name, AnySort<Name>, unknown>,
    ): Expr<Name, AnySort<Name>, unknown>;
    congruenceRoot(
        expr: Expr<Name, AnySort<Name>, unknown>,
    ): Expr<Name, AnySort<Name>, unknown>;
    cube(
        vars?: AstVector<Name, Bool<Name>>,
        cutoff?: number,
    ): Promise<AstVector<Name, Bool<Name>>>;
    dimacs(includeNames?: boolean): string;
    fromFile(filename: string): void;
    fromString(s: string): void;
    getConsequences(
        assumptions: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
        variables: Expr<Name, AnySort<Name>, unknown>[],
    ): Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]>;
    model(): Model<Name>;
    nonUnits(): AstVector<Name, Bool<Name>>;
    numScopes(): number;
    pop(num?: number): void;
    proof(): null | Expr<Name, AnySort<Name>, unknown>;
    push(): void;
    reasonUnknown(): string;
    registerOnClause(
        callback: (
            proofHint: null | Expr<Name, AnySort<Name>, unknown>,
            deps: number[],
            clause: AstVector<Name, Bool<Name>>,
        ) => void,
    ): void;
    release(): void;
    reset(): void;
    set(key: string, value: any): void;
    setInitialValue(
        variable: Expr<Name, AnySort<Name>, unknown>,
        value: Expr<Name, AnySort<Name>, unknown>,
    ): void;
    solveFor(
        variables: Expr<Name, AnySort<Name>, unknown>[],
        terms: Expr<Name, AnySort<Name>, unknown>[],
        guards: Bool<Name>[],
    ): void;
    statistics(): Statistics<Name>;
    toSmtlib2(status?: string): string;
    trail(): AstVector<Name, Bool<Name>>;
    trailLevels(): number[];
    translate(target: Context<Name>): Solver<Name>;
    units(): AstVector<Name, Bool<Name>>;
    unsatCore(): AstVector<Name, Bool<Name>>;
}

Type Parameters

Name extends string = "main"

Properties

`Readonly`ctx

ctx: Context<Name>

`Readonly`ptr

ptr: Z3_solver

Methods

add

add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void
Parameters
- ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]
Returns void
- Defined in src/high-level/types.ts:1070

addAndTrack

addAndTrack(expr: Bool<Name>, constant: string | Bool<Name>): void
Assert a constraint and associate it with a tracking literal (Boolean constant). This is the TypeScript equivalent of assertAndTrack in other Z3 language bindings.

When the solver returns unsat, the tracked literals that contributed to unsatisfiability can be retrieved via unsatCore.
Parameters
- expr: Bool<Name>
  The Boolean expression to assert
- constant: string | Bool<Name>
  A Boolean constant (or its name as a string) used as the tracking literal
Returns void
Example
```
const solver = new Solver();
const x = Int.const('x');
const p1 = Bool.const('p1');
const p2 = Bool.const('p2');
solver.addAndTrack(x.gt(0), p1);
solver.addAndTrack(x.lt(0), p2);
if (await solver.check() === 'unsat') {
  const core = solver.unsatCore(); // contains p1 and p2
}
```
- Defined in src/high-level/types.ts:1095

addSimplifier

addSimplifier(simplifier: Simplifier<Name>): void
Attach a simplifier to the solver for incremental pre-processing. The solver will use the simplifier for incremental pre-processing of assertions.
Parameters
- simplifier: Simplifier<Name>
  The simplifier to attach
Returns void
- Defined in src/high-level/types.ts:1102

assertions

assertions(): AstVector<Name, Bool<Name>>
Returns AstVector<Name, Bool<Name>>
- Defined in src/high-level/types.ts:1104

check

check(
...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
): Promise<CheckSatResult>
Check whether the assertions in the solver are consistent or not.

Optionally, you can provide additional boolean expressions as assumptions. These assumptions are temporary and only used for this check - they are not permanently added to the solver.
Parameters
- ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]
  Optional assumptions to check in addition to the solver's assertions. These are temporary and do not modify the solver state.
Returns Promise<CheckSatResult>
A promise resolving to: - 'sat' if the assertions (plus assumptions) are satisfiable - 'unsat' if they are unsatisfiable - 'unknown' if Z3 cannot determine satisfiability
Example
```
const solver = new Solver();
const x = Int.const('x');
solver.add(x.gt(0));

// Check without assumptions
await solver.check(); // 'sat'

// Check with temporary assumption (doesn't modify solver)
await solver.check(x.lt(0)); // 'unsat'
await solver.check(); // still 'sat' - assumption was temporary
```
See
unsatCore - Retrieve unsat core after checking with assumptions
- Defined in src/high-level/types.ts:1138

congruenceExplain

congruenceExplain(
a: Expr<Name, AnySort<Name>, unknown>,
b: Expr<Name, AnySort<Name>, unknown>,
): Expr<Name, AnySort<Name>, unknown>
Explain why two expressions are congruent according to the solver's reasoning. Returns a proof term explaining the congruence.

Note: This works primarily with SimpleSolver and may not work with terms eliminated during preprocessing.
Parameters
- a: Expr<Name, AnySort<Name>, unknown>
  First expression
- b: Expr<Name, AnySort<Name>, unknown>
  Second expression
Returns Expr<Name, AnySort<Name>, unknown>
An expression representing the proof of congruence
Example
```
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
solver.add(x.eq(y));
await solver.check();
const explanation = solver.congruenceExplain(x, y);
```
- Defined in src/high-level/types.ts:1432

congruenceNext

congruenceNext(
expr: Expr<Name, AnySort<Name>, unknown>,
): Expr<Name, AnySort<Name>, unknown>
Retrieve the next expression in the congruence class containing the given expression. The congruence class forms a circular linked list.

Note: This works primarily with SimpleSolver and may not work with terms eliminated during preprocessing.
Parameters
- expr: Expr<Name, AnySort<Name>, unknown>
  The expression to find the next congruent expression for
Returns Expr<Name, AnySort<Name>, unknown>
The next expression in the congruence class
Example
```
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
const z = Int.const('z');
solver.add(x.eq(y));
solver.add(y.eq(z));
await solver.check();
const next = solver.congruenceNext(x);
```
- Defined in src/high-level/types.ts:1409

congruenceRoot

congruenceRoot(
expr: Expr<Name, AnySort<Name>, unknown>,
): Expr<Name, AnySort<Name>, unknown>
Retrieve the root of the congruence class containing the given expression. This is useful for understanding equality reasoning in the solver.

Note: This works primarily with SimpleSolver and may not work with terms eliminated during preprocessing.
Parameters
- expr: Expr<Name, AnySort<Name>, unknown>
  The expression to find the congruence root for
Returns Expr<Name, AnySort<Name>, unknown>
The root expression of the congruence class
Example
```
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
solver.add(x.eq(y));
await solver.check();
const root = solver.congruenceRoot(x);
```
- Defined in src/high-level/types.ts:1385

cube

cube(
vars?: AstVector<Name, Bool<Name>>,
cutoff?: number,
): Promise<AstVector<Name, Bool<Name>>>
Extract cubes from the solver for cube-and-conquer parallel solving. Each call returns the next cube (conjunction of literals) from the solver. Returns an empty AstVector when the search space is exhausted.
Parameters
- Optionalvars: AstVector<Name, Bool<Name>>
  Optional vector of variables to use as cube variables
- Optionalcutoff: number
  Backtrack level cutoff for cube generation (default: 0xFFFFFFFF)
Returns Promise<AstVector<Name, Bool<Name>>>
A promise resolving to an AstVector containing the cube literals
Example
```
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
solver.add(x.or(y));
const cube = await solver.cube(undefined, 1);
console.log('Cube length:', cube.length());
```
- Defined in src/high-level/types.ts:1304

dimacs

dimacs(includeNames?: boolean): string
Convert the solver's Boolean formula to DIMACS CNF format.
Parameters
- OptionalincludeNames: boolean
  If true, include variable names in the output (default: true)
Returns string
A string containing the DIMACS CNF representation
- Defined in src/high-level/types.ts:1476

fromFile

fromFile(filename: string): void
Load SMT-LIB2 format assertions from a file into the solver.
Parameters
- filename: string
  Path to the file containing SMT-LIB2 format assertions
Returns void
Example
```
const solver = new Solver();
solver.fromFile('problem.smt2');
const result = await solver.check();
```
- Defined in src/high-level/types.ts:1446

fromString

fromString(s: string): void
Parameters
- s: string
Returns void
- Defined in src/high-level/types.ts:1106

getConsequences

getConsequences(
assumptions: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
variables: Expr<Name, AnySort<Name>, unknown>[],
): Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]>
Retrieve fixed assignments to a set of variables as consequences given assumptions. Each consequence is an implication: assumptions => variable = value.
Parameters
- assumptions: (Bool<Name> | AstVector<Name, Bool<Name>>)[]
  Assumptions to use during consequence finding
- variables: Expr<Name, AnySort<Name>, unknown>[]
  Variables to find consequences for
Returns Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]>
A promise resolving to the status and a vector of consequence expressions
Example
```
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
solver.add(x.implies(y));
const [status, consequences] = await solver.getConsequences([], [x, y]);
```
- Defined in src/high-level/types.ts:1323

model

model(): Model<Name>
Returns Model<Name>
- Defined in src/high-level/types.ts:1173

nonUnits

nonUnits(): AstVector<Name, Bool<Name>>
Retrieve the set of tracked boolean literals that are not unit literals.

Returns AstVector<Name, Bool<Name>>
An AstVector containing the non-unit literals
Example
```
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
solver.add(x.or(y));
await solver.check();
const nonUnits = solver.nonUnits();
```
- Defined in src/high-level/types.ts:1244

numScopes

numScopes(): number
Returns number
- Defined in src/high-level/types.ts:1066

pop

pop(num?: number): void
Parameters
- Optionalnum: number
Returns void
- Defined in src/high-level/types.ts:1064

proof

proof(): null | Expr<Name, AnySort<Name>, unknown>
Retrieve a proof of unsatisfiability after a check that returned 'unsat'. Requires proof production to be enabled.

Returns null | Expr<Name, AnySort<Name>, unknown>
An expression representing the proof, or null if unavailable
- Defined in src/high-level/types.ts:1490

push

push(): void
Returns void
- Defined in src/high-level/types.ts:1062

reasonUnknown

reasonUnknown(): string
Return a string describing why the last call to check returned 'unknown'.

Returns string
A string explaining the reason, or an empty string if the last check didn't return unknown
Example
```
const result = await solver.check();
if (result === 'unknown') {
  console.log('Reason:', solver.reasonUnknown());
}
```
- Defined in src/high-level/types.ts:1209

registerOnClause

registerOnClause(
    callback: (
        proofHint: null | Expr<Name, AnySort<Name>, unknown>,
        deps: number[],
        clause: AstVector<Name, Bool<Name>>,
    ) => void,
): void
Register a callback that is invoked when clauses are inferred during solving. The callback is called when a clause is:
- asserted to the CDCL engine (input clause after pre-processing)
- inferred by CDCL(T) using a SAT or theory conflict/propagation
- deleted by the CDCL(T) engine
Requires the Emscripten module to be passed to createApi.
Parameters
- callback: (
      proofHint: null | Expr<Name, AnySort<Name>, unknown>,
      deps: number[],
      clause: AstVector<Name, Bool<Name>>,
  ) => void
  Function called with:
  - proofHint: optional proof hint expression (may be null)
  - deps: array of clause dependency indices
  - clause: the clause as a vector of literals
Returns void
- Defined in src/high-level/types.ts:1513

release

release(): void
Manually decrease the reference count of the solver This is automatically done when the solver is garbage collected, but calling this eagerly can help release memory sooner.

Returns void
- Defined in src/high-level/types.ts:1497

reset

reset(): void
Returns void
- Defined in src/high-level/types.ts:1068

set

set(key: string, value: any): void
Parameters
- key: string
- value: any
Returns void
- Defined in src/high-level/types.ts:1057

setInitialValue

setInitialValue(
variable: Expr<Name, AnySort<Name>, unknown>,
value: Expr<Name, AnySort<Name>, unknown>,
): void
Set an initial value hint for a variable to guide the solver's search heuristics. This can improve performance when a good initial value is known.
Parameters
- variable: Expr<Name, AnySort<Name>, unknown>
  The variable to set an initial value for
- value: Expr<Name, AnySort<Name>, unknown>
  The initial value for the variable
Returns void
Example
```
const solver = new Solver();
const x = Int.const('x');
solver.setInitialValue(x, Int.val(42));
solver.add(x.gt(0));
await solver.check();
```
- Defined in src/high-level/types.ts:1363

solveFor

solveFor(
    variables: Expr<Name, AnySort<Name>, unknown>[],
    terms: Expr<Name, AnySort<Name>, unknown>[],
    guards: Bool<Name>[],
): void
Solve constraints treating given variables symbolically, replacing their occurrences by terms. Guards condition the substitutions.
Parameters
- variables: Expr<Name, AnySort<Name>, unknown>[]
  Variables to solve for
- terms: Expr<Name, AnySort<Name>, unknown>[]
  Substitution terms for the variables
- guards: Bool<Name>[]
  Boolean guards for the substitutions
Returns void
Example
```
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
solver.add(x.eq(y.add(1)));
solver.solveFor([x], [y.add(1)], []);
```
- Defined in src/high-level/types.ts:1345

statistics

statistics(): Statistics<Name>

Retrieve statistics for the solver. Returns performance metrics, memory usage, decision counts, and other diagnostic information.

Returns Statistics<Name>

A Statistics object containing solver metrics

Example

const solver = new Solver();
const x = Int.const('x');
solver.add(x.gt(0));
await solver.check();
const stats = solver.statistics();
console.log('Statistics size:', stats.size());
for (const entry of stats) {
  console.log(`${entry.key}: ${entry.value}`);
}

toSmtlib2

toSmtlib2(status?: string): string
Convert the solver's assertions to SMT-LIB2 format as a benchmark.

This exports the current set of assertions in the solver as an SMT-LIB2 string, which can be used for bug reporting, sharing problems, or benchmarking.
Parameters
- Optionalstatus: string
  Status string such as "sat", "unsat", or "unknown" (default: "unknown")
Returns string
A string representation of the solver's assertions in SMT-LIB2 format
Example
```
const solver = new Solver();
const x = Int.const('x');
const y = Int.const('y');
solver.add(x.gt(0));
solver.add(y.eq(x.add(1)));
const smtlib2 = solver.toSmtlib2('unknown');
console.log(smtlib2); // Prints SMT-LIB2 formatted problem
```
- Defined in src/high-level/types.ts:1468

trail

trail(): AstVector<Name, Bool<Name>>
Retrieve the trail of boolean literals assigned by the solver during solving. The trail represents the sequence of decisions and propagations made by the solver.

Returns AstVector<Name, Bool<Name>>
An AstVector containing the trail of assigned literals
Example
```
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
solver.add(x.implies(y));
solver.add(x);
await solver.check();
const trail = solver.trail();
console.log('Trail length:', trail.length());
```
- Defined in src/high-level/types.ts:1264

trailLevels

trailLevels(): number[]
Retrieve the decision levels for each literal in the solver's trail. The returned array has one entry per trail literal, indicating at which decision level it was assigned.

Returns number[]
An array of numbers where element i is the decision level of the i-th trail literal
Example
```
const solver = new Solver();
const x = Bool.const('x');
solver.add(x);
await solver.check();
const levels = solver.trailLevels();
console.log('Trail levels:', levels);
```
- Defined in src/high-level/types.ts:1283

translate

translate(target: Context<Name>): Solver<Name>
Translate the solver to a different context.
Parameters
- target: Context<Name>
  The target context
Returns Solver<Name>
A new Solver instance in the target context
- Defined in src/high-level/types.ts:1483

units

units(): AstVector<Name, Bool<Name>>
Retrieve the set of literals that were inferred by the solver as unit literals. These are boolean literals that the solver has determined must be true in all models.

Returns AstVector<Name, Bool<Name>>
An AstVector containing the unit literals
Example
```
const solver = new Solver();
const x = Bool.const('x');
solver.add(x.or(x)); // simplifies to x
await solver.check();
const units = solver.units();
console.log('Unit literals:', units.length());
```
- Defined in src/high-level/types.ts:1227

unsatCore

unsatCore(): AstVector<Name, Bool<Name>>
Retrieve the unsat core after a check that returned 'unsat'.

The unsat core is a (typically small) subset of the assumptions that were sufficient to determine unsatisfiability. This is useful for understanding which assumptions are conflicting.

Note: To use unsat cores effectively, you should call check with assumptions (not just assertions added via add).

Returns AstVector<Name, Bool<Name>>
An AstVector containing the subset of assumptions that caused UNSAT
Example
```
const solver = new Solver();
const x = Bool.const('x');
const y = Bool.const('y');
const z = Bool.const('z');
solver.add(x.or(y));
solver.add(x.or(z));

const result = await solver.check(x.not(), y.not(), z.not());
if (result === 'unsat') {
  const core = solver.unsatCore();
  // core will contain a minimal set of conflicting assumptions
  console.log('UNSAT core size:', core.length());
}
```
See
check - Check with assumptions to use with unsat core
- Defined in src/high-level/types.ts:1171

Interface Solver<Name>

Type Parameters

Index

Properties

Methods

Properties

Readonlyctx

Readonlyptr

Methods

add

Parameters

Returns void

addAndTrack

Parameters

Returns void

Example

addSimplifier

Parameters

Returns void

assertions

Returns AstVector<Name, Bool<Name>>

check

Parameters

Returns Promise<CheckSatResult>

Example

See

congruenceExplain

Parameters

Returns Expr<Name, AnySort<Name>, unknown>

Example

congruenceNext

Parameters

Returns Expr<Name, AnySort<Name>, unknown>

Example

congruenceRoot

Parameters

Returns Expr<Name, AnySort<Name>, unknown>

Example

cube

Parameters

Returns Promise<AstVector<Name, Bool<Name>>>

Example

dimacs

Parameters

Returns string

fromFile

Parameters

Returns void

Example

fromString

Parameters

Returns void

getConsequences

Parameters

Returns Promise<[CheckSatResult, AstVector<Name, Bool<Name>>]>

Example

model

Returns Model<Name>

nonUnits

Returns AstVector<Name, Bool<Name>>

Example

numScopes

Returns number

pop

Parameters

Returns void

proof

Returns null | Expr<Name, AnySort<Name>, unknown>

push

Returns void

reasonUnknown

Returns string

Example

registerOnClause

Parameters

Returns void

release

Returns void

reset

Returns void

`Readonly`ctx

`Readonly`ptr