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;
    assertions(): AstVector<Name, Bool<Name>>;
    check(
        ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
    ): Promise<CheckSatResult>;
    fromString(s: string): void;
    model(): Model<Name>;
    numScopes(): number;
    pop(num?: number): void;
    push(): void;
    reasonUnknown(): string;
    release(): void;
    reset(): void;
    set(key: string, value: any): void;
    unsatCore(): AstVector<Name, Bool<Name>>;
    unsatCore(): AstVector<Name, Bool<Name>>;
}

Type Parameters

  • Name extends string = "main"

Properties

ctx ptr

Methods

add addAndTrack assertions check fromString model numScopes pop push reasonUnknown release reset set unsatCore

Properties

Readonlyctx

ctx: Context<Name>

Readonlyptr

ptr: Z3_solver

Methods

add

addAndTrack

assertions

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

fromString

model

numScopes

pop

push

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

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

set

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

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

  • Returns AstVector<Name, Bool<Name>>

Settings

Member Visibility

On This Page

Properties
Methods