Interface Solver<Name>

Readonlyctx

Readonlyptr

add

• add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void

• Parameters

  • ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]

  Returns void

addAndTrack

• addAndTrack(expr: Bool<Name>, constant: string | Bool<Name>): void

• Parameters

  • expr: Bool<Name>
  • constant: string | Bool<Name>

  Returns void

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

assertions

• assertions(): AstVector<Name, Bool<Name>>

• Returns AstVector<Name, Bool<Name>>

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
  Copy

  See

  unsatCore - Retrieve unsat core after checking with assumptions

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

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

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

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();
  Copy

fromString

• fromString(s: string): void

• Parameters

  • s: string

  Returns void

model

• model(): Model<Name>

• Returns Model<Name>

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();
  Copy

numScopes

• numScopes(): number

• Returns number

pop

• pop(num?: number): void

• Parameters

  • Optionalnum: number

  Returns void

push

• push(): void

• Returns void

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());
  }
  Copy

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

reset

• reset(): void

• Returns void

set

• set(key: string, value: any): void

• Parameters

  • key: string
  • value: any

  Returns void

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}`);
  }
  Copy

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
  Copy

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());
  Copy

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());
  Copy

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());
  }
  Copy

  See

  check - Check with assumptions to use with unsat core