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>;
    fromString(s: string): void;
    maximize(expr: Arith<Name>): void;
    minimize(expr: Arith<Name>): void;
    model(): Model<Name>;
    pop(num?: number): void;
    push(): void;
    release(): void;
    set(key: string, value: any): void;
}

Type Parameters

  • Name extends string = "main"

Properties

ctx ptr

Methods

add addAndTrack addSoft assertions check fromString maximize minimize model pop push release set

Properties

Readonlyctx

ctx: Context<Name>

Readonlyptr

ptr: Z3_optimize

Methods

add

addAndTrack

addSoft

assertions

check

fromString

maximize

minimize

model

pop

push

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

Settings

Member Visibility

On This Page

Properties
Methods