Interface Optimize<Name>

interface Optimize<Name extends string = "main"> {
    ctx: Context<Name>;
    ptr: Z3_optimize;
    add(...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[]): void;
    addAndTrack(expr: Bool<Name>, constant: string | Bool<Name>): void;
    addSoft(
        expr: Bool<Name>,
        weight: string | number | bigint | CoercibleRational,
        id?: string | number,
    ): void;
    assertions(): AstVector<Name, Bool<Name>>;
    check(
        ...exprs: (Bool<Name> | AstVector<Name, Bool<Name>>)[],
    ): Promise<CheckSatResult>;
    fromFile(filename: string): void;
    fromString(s: string): void;
    getLower(index: number): Expr<Name, AnySort<Name>, unknown>;
    getUpper(index: number): Expr<Name, AnySort<Name>, unknown>;
    maximize(expr: Arith<Name> | BitVec<number, Name>): number;
    minimize(expr: Arith<Name> | BitVec<number, Name>): number;
    model(): Model<Name>;
    objectives(): AstVector<Name, Expr<Name, AnySort<Name>, unknown>>;
    pop(num?: number): void;
    push(): void;
    reasonUnknown(): string;
    release(): void;
    set(key: string, value: any): void;
    setInitialValue(
        variable: Expr<Name, AnySort<Name>, unknown>,
        value: Expr<Name, AnySort<Name>, unknown>,
    ): void;
    statistics(): Statistics<Name>;
    translate(target: Context<Name>): Optimize<Name>;
    unsatCore(): AstVector<Name, Bool<Name>>;
}

Type Parameters

  • Name extends string = "main"

Properties

ctx ptr

Methods

add addAndTrack addSoft assertions check fromFile fromString getLower getUpper maximize minimize model objectives pop push reasonUnknown release set setInitialValue statistics translate unsatCore

Properties

Readonlyctx

ctx: Context<Name>

Readonlyptr

ptr: Z3_optimize

Methods

add

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 optimizer returns unsat, the tracked literals that contributed to unsatisfiability can be used to identify which constraints caused the conflict.

    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 opt = new Optimize();
    const x = Int.const('x');
    const p1 = Bool.const('p1');
    const p2 = Bool.const('p2');
    opt.addAndTrack(x.gt(0), p1);
    opt.addAndTrack(x.lt(0), p2);
    const result = await opt.check(); // 'unsat'

addSoft

assertions

check

fromFile

  • fromFile(filename: string): void

  • Load SMT-LIB2 format assertions from a file into the optimizer.

    Parameters

    • filename: string

      Path to the file containing SMT-LIB2 format assertions

    Returns void

fromString

getLower

getUpper

maximize

  • maximize(expr: Arith<Name> | BitVec<number, Name>): number

  • Add a maximization objective.

    Parameters

    Returns number

    A zero-based numeric handle index for this objective, used to retrieve bounds via getLower/getUpper after calling check

    Example

    const opt = new Optimize();
    const x = Int.const('x');
    opt.add(x.ge(0), x.le(10));
    const h = opt.maximize(x);
    await opt.check();
    console.log('Max x:', opt.getUpper(h).toString()); // '10'

minimize

  • minimize(expr: Arith<Name> | BitVec<number, Name>): number

  • Add a minimization objective.

    Parameters

    Returns number

    A zero-based numeric handle index for this objective, used to retrieve bounds via getLower/getUpper after calling check

    Example

    const opt = new Optimize();
    const x = Int.const('x');
    opt.add(x.ge(0), x.le(10));
    const h = opt.minimize(x);
    await opt.check();
    console.log('Min x:', opt.getLower(h).toString()); // '0'

model

objectives

pop

push

reasonUnknown

release

  • release(): void

  • Manually decrease the reference count of the optimize This is automatically done when the optimize is garbage collected, but calling this eagerly can help release memory sooner.

    Returns void

set

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 optimizer'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 opt = new Optimize();
    const x = Int.const('x');
    opt.setInitialValue(x, Int.val(42));
    opt.add(x.gt(0));
    opt.maximize(x);
    await opt.check();

statistics

translate

unsatCore

Settings

Member Visibility

On This Page

Properties
Methods