Interface Context<Name>

interface Context<Name extends string = "main"> {
    Array: SMTArrayCreation<Name>;
    AstMap: new <
        Key extends Ast<Name, unknown> = AnyAst<Name>,
        Value extends Ast<Name, unknown> = AnyAst<Name>,
    >() => AstMap<Name, Key, Value>;
    AstVector: new <Item extends Ast<Name, unknown> = AnyAst<Name>>() => AstVector<
        Name,
        Item,
    >;
    BitVec: BitVecCreation<Name>;
    Bool: BoolCreation<Name>;
    Datatype: DatatypeCreation<Name>;
    Function: FuncDeclCreation<Name>;
    Int: IntCreation<Name>;
    Model: new () => Model<Name>;
    name: Name;
    Optimize: new () => Optimize<Name>;
    Real: RealCreation<Name>;
    RecFunc: RecFuncCreation<Name>;
    Set: SMTSetCreation<Name>;
    Solver: new (logic?: string) => Solver<Name>;
    Sort: SortCreation<Name>;
    Tactic: new (name: string) => Tactic<Name>;
    And(): Bool<Name>;
    And(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
    And(...args: (boolean | Bool<Name>)[]): Bool<Name>;
    And(...args: Probe<Name>[]): Probe<Name>;
    ast_from_string(s: string): Ast<Name, unknown>;
    AtLeast(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name>;
    AtMost(args: [Bool<Name>, ...Bool<Name>[]], k: number): Bool<Name>;
    BUDiv<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        arg1: CoercibleToBitVec<Bits, Name>,
    ): BitVec<Bits, Name>;
    BV2Int(a: BitVec<number, Name>, isSigned: boolean): Arith<Name>;
    Cbrt(a: CoercibleToArith<Name>): Arith<Name>;
    Concat(...bitvecs: BitVec<number, Name>[]): BitVec<number, Name>;
    Cond(
        probe: Probe<Name>,
        onTrue: Tactic<Name>,
        onFalse: Tactic<Name>,
    ): Tactic<Name>;
    Const<S extends Sort<Name>>(name: string, sort: S): SortToExprMap<S, Name>;
    Consts<S extends Sort<Name>>(
        name: string | string[],
        sort: S,
    ): SortToExprMap<S, Name>[];
    Distinct(...args: CoercibleToExpr<Name>[]): Bool<Name>;
    Div(arg0: Arith<Name>, arg1: CoercibleToArith<Name>): Arith<Name>;
    Div<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        arg1: CoercibleToBitVec<Bits, Name>,
    ): BitVec<Bits, Name>;
    EmptySet<ElemSort extends AnySort<Name>>(
        sort: ElemSort,
    ): SMTSet<Name, ElemSort>;
    Eq(a: CoercibleToExpr<Name>, b: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(a: Ast<Name, unknown>, b: Ast<Name, unknown>): boolean;
    Exists<QVarSorts extends [Sort<Name>, ...Sort<Name>[]]>(
        quantifiers: [
            ...{
                [Key in string
                | number
                | symbol]: QVarSorts[Key<Key>] extends AnySort<Name>
                    ? SortToExprMap<any[any], Name>
                    : QVarSorts[Key<Key>]
            }[],
        ],
        body: Bool<Name>,
        weight?: number,
    ): Quantifier<Name, QVarSorts, BoolSort<Name>> & Bool<Name>;
    Extract<Bits extends number>(
        hi: number,
        lo: number,
        val: BitVec<Bits, Name>,
    ): BitVec<number, Name>;
    ForAll<QVarSorts extends [Sort<Name>, ...Sort<Name>[]]>(
        quantifiers: [
            ...{
                [Key in string
                | number
                | symbol]: QVarSorts[Key<Key>] extends AnySort<Name>
                    ? SortToExprMap<any[any], Name>
                    : QVarSorts[Key<Key>]
            }[],
        ],
        body: Bool<Name>,
        weight?: number,
    ): Quantifier<Name, QVarSorts, BoolSort<Name>> & Bool<Name>;
    FreshConst<S extends Sort<Name>>(
        sort: S,
        prefix?: string,
    ): SortToExprMap<S, Name>;
    from(primitive: boolean): Bool<Name>;
    from(primitive: number): IntNum<Name> | RatNum<Name>;
    from(primitive: CoercibleRational): RatNum<Name>;
    from(primitive: bigint): IntNum<Name>;
    from<E extends Expr<Name, AnySort<Name>, unknown>>(expr: E): E;
    FullSet<ElemSort extends AnySort<Name>>(
        sort: ElemSort,
    ): SMTSet<Name, ElemSort>;
    GE(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
    getVarIndex(obj: Expr<Name, AnySort<Name>, unknown>): number;
    GT(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
    If(
        condition: Probe<Name>,
        onTrue: Tactic<Name>,
        onFalse: Tactic<Name>,
    ): Tactic<Name>;
    If<
        OnTrueRef extends CoercibleToExpr<Name>,
        OnFalseRef extends CoercibleToExpr<Name>,
    >(
        condition: boolean | Bool<Name>,
        onTrue: OnTrueRef,
        onFalse: OnFalseRef,
    ): CoercibleFromMap<OnTrueRef, Name> | CoercibleFromMap<OnFalseRef, Name>;
    Iff(a: boolean | Bool<Name>, b: boolean | Bool<Name>): Bool<Name>;
    Implies(a: boolean | Bool<Name>, b: boolean | Bool<Name>): Bool<Name>;
    Int2BV<Bits extends number>(
        a: number | bigint | Arith<Name>,
        bits: Bits,
    ): BitVec<Bits, Name>;
    interrupt(): void;
    isAnd(obj: unknown): boolean;
    isApp(obj: unknown): boolean;
    isAppOf(obj: unknown, kind: Z3_decl_kind): boolean;
    isArith(obj: unknown): obj is Arith<Name>;
    isArithSort(obj: unknown): obj is ArithSort<Name>;
    isArray(
        obj: unknown,
    ): obj is SMTArray<Name, [Sort<Name>, ...Sort<Name>[]], Sort<Name>>;
    isArraySort(
        obj: unknown,
    ): obj is SMTArraySort<Name, [Sort<Name>, ...Sort<Name>[]], AnySort<Name>>;
    isAst(obj: unknown): obj is Ast<Name, unknown>;
    isAstVector(obj: unknown): obj is AstVector<Name, AnyAst<Name>>;
    isBitVec(obj: unknown): obj is BitVec<number, Name>;
    isBitVecSort(obj: unknown): obj is BitVecSort<number, Name>;
    isBitVecVal(obj: unknown): obj is BitVecNum<number, Name>;
    isBool(obj: unknown): obj is Bool<Name>;
    isConst(obj: unknown): boolean;
    isConstArray(obj: unknown): boolean;
    isDistinct(obj: unknown): boolean;
    isEq(obj: unknown): boolean;
    isExpr(obj: unknown): obj is Expr<Name, AnySort<Name>, unknown>;
    isFalse(obj: unknown): boolean;
    isFuncDecl(obj: unknown): obj is FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    isFuncInterp(obj: unknown): obj is FuncInterp<Name>;
    isImplies(obj: unknown): boolean;
    isInt(obj: unknown): boolean;
    IsInt(expr: string | number | CoercibleRational | Arith<Name>): Bool<Name>;
    isIntSort(obj: unknown): boolean;
    isIntVal(obj: unknown): obj is IntNum<Name>;
    isMember<ElemSort extends AnySort<Name>>(
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
        set: SMTSet<Name, ElemSort>,
    ): Bool<Name>;
    isModel(obj: unknown): obj is Model<Name>;
    isNot(obj: unknown): boolean;
    isOr(obj: unknown): boolean;
    isProbe(obj: unknown): obj is Probe<Name>;
    isQuantifier(
        obj: unknown,
    ): obj is Quantifier<
        Name,
        [Sort<Name>, ...Sort<Name>[]],

            | BoolSort<Name>
            | SMTArraySort<Name, [Sort<Name>, ...Sort<Name>[]], AnySort<Name>>,
    >;
    isReal(obj: unknown): boolean;
    isRealSort(obj: unknown): boolean;
    isRealVal(obj: unknown): obj is RatNum<Name>;
    isSort(obj: unknown): obj is Sort<Name>;
    isSubset<ElemSort extends AnySort<Name>>(
        a: SMTSet<Name, ElemSort>,
        b: SMTSet<Name, ElemSort>,
    ): Bool<Name>;
    isTactic(obj: unknown): obj is Tactic<Name>;
    isTrue(obj: unknown): boolean;
    isVar(obj: unknown): boolean;
    Lambda<
        DomainSort extends [Sort<Name>, ...Sort<Name>[]],
        RangeSort extends Sort<Name>,
    >(
        quantifiers: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? SortToExprMap<any[any], Name>
                    : DomainSort[Key<Key>]
            }[],
        ],
        expr: SortToExprMap<RangeSort, Name>,
    ): Quantifier<Name, DomainSort, SMTArraySort<Name, DomainSort, RangeSort>> & SMTArray<
        Name,
        DomainSort,
        RangeSort,
    >;
    LE(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
    LT(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
    Mod(a: Arith<Name>, b: CoercibleToArith<Name>): Arith<Name>;
    Mod<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): BitVec<Bits, Name>;
    Neg(a: Arith<Name>): Arith<Name>;
    Neg<Bits extends number>(a: BitVec<Bits, Name>): BitVec<Bits, Name>;
    Not(a: Probe<Name>): Probe<Name>;
    Not(a: boolean | Bool<Name>): Bool<Name>;
    Or(): Bool<Name>;
    Or(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
    Or(...args: (boolean | Bool<Name>)[]): Bool<Name>;
    Or(...args: Probe<Name>[]): Probe<Name>;
    PbEq(
        args: [Bool<Name>, ...Bool<Name>[]],
        coeffs: [number, ...number[]],
        k: number,
    ): Bool<Name>;
    PbGe(
        args: [Bool<Name>, ...Bool<Name>[]],
        coeffs: [number, ...number[]],
        k: number,
    ): Bool<Name>;
    PbLe(
        args: [Bool<Name>, ...Bool<Name>[]],
        coeffs: [number, ...number[]],
        k: number,
    ): Bool<Name>;
    Product(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
    Product<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        ...args: CoercibleToBitVec<Bits, Name>[],
    ): BitVec<Bits, Name>;
    Select<
        DomainSort extends [Sort<Name>, ...Sort<Name>[]],
        RangeSort extends Sort<Name> = Sort<Name>,
    >(
        array: SMTArray<Name, DomainSort, RangeSort>,
        ...indices: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                    : DomainSort[Key<Key>]
            }[],
        ],
    ): SortToExprMap<RangeSort, Name>;
    SetAdd<ElemSort extends AnySort<Name>>(
        set: SMTSet<Name, ElemSort>,
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
    ): SMTSet<Name, ElemSort>;
    SetComplement<ElemSort extends AnySort<Name>>(
        set: SMTSet<Name, ElemSort>,
    ): SMTSet<Name, ElemSort>;
    SetDel<ElemSort extends AnySort<Name>>(
        set: SMTSet<Name, ElemSort>,
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
    ): SMTSet<Name, ElemSort>;
    SetDifference<ElemSort extends AnySort<Name>>(
        a: SMTSet<Name, ElemSort>,
        b: SMTSet<Name, ElemSort>,
    ): SMTSet<Name, ElemSort>;
    SetIntersect<ElemSort extends AnySort<Name>>(
        ...args: SMTSet<Name, ElemSort>[],
    ): SMTSet<Name, ElemSort>;
    SetUnion<ElemSort extends AnySort<Name>>(
        ...args: SMTSet<Name, ElemSort>[],
    ): SMTSet<Name, ElemSort>;
    SGE<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    SGT<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    simplify(
        expr: Expr<Name, AnySort<Name>, unknown>,
    ): Promise<Expr<Name, AnySort<Name>, unknown>>;
    SLE<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    SLT<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    solve(
        ...assertions: Bool<Name>[],
    ): Promise<"unsat" | "unknown" | Model<Name>>;
    Sqrt(a: CoercibleToArith<Name>): Arith<Name>;
    Store<
        DomainSort extends [Sort<Name>, ...Sort<Name>[]],
        RangeSort extends Sort<Name> = Sort<Name>,
    >(
        array: SMTArray<Name, DomainSort, RangeSort>,
        ...indicesAndValue: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                    : DomainSort[Key<Key>]
            }[],
            CoercibleToMap<SortToExprMap<RangeSort, Name>, Name>,
        ],
    ): SMTArray<Name, DomainSort, RangeSort>;
    Sub(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
    Sub<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        ...args: CoercibleToBitVec<Bits, Name>[],
    ): BitVec<Bits, Name>;
    substitute(
        t: Expr<Name, AnySort<Name>, unknown>,
        ...substitutions: [
            Expr<Name, AnySort<Name>, unknown>,
            Expr<Name, AnySort<Name>, unknown>,
        ][],
    ): Expr<Name, AnySort<Name>, unknown>;
    Sum(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
    Sum<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        ...args: CoercibleToBitVec<Bits, Name>[],
    ): BitVec<Bits, Name>;
    ToInt(expr: string | number | CoercibleRational | Arith<Name>): Arith<Name>;
    ToReal(expr: bigint | Arith<Name>): Arith<Name>;
    UGE<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    UGT<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    ULE<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    ULT<Bits extends number>(
        a: BitVec<Bits, Name>,
        b: CoercibleToBitVec<Bits, Name>,
    ): Bool<Name>;
    Var<S extends Sort<Name>>(idx: number, sort: S): SortToExprMap<S, Name>;
    Xor(a: boolean | Bool<Name>, b: boolean | Bool<Name>): Bool<Name>;
}

Type Parameters

  • Name extends string = "main"

Classes

AstMap AstVector Model Solver Tactic

Expressions

Array BitVec Bool Datatype Function Int Real RecFunc Set Sort

Functions

eqIdentity from getVarIndex interrupt isAnd isApp isAppOf isArith isArithSort isArray isArraySort isAst isAstVector isBitVec isBitVecSort isBitVecVal isBool isConst isConstArray isDistinct isEq isExpr isFalse isFuncDecl isFuncInterp isImplies isInt isIntSort isIntVal isModel isNot isOr isProbe isQuantifier isReal isRealSort isRealVal isSort isTactic isTrue isVar solve

Operations

And ast_from_string AtLeast AtMost BV2Int Cbrt Concat Cond Const Consts Distinct EmptySet Eq Exists Extract ForAll FreshConst FullSet GE GT If Iff Implies Int2BV IsInt isMember isSubset Lambda LE LT Not Or PbEq PbGe PbLe Select SetAdd SetComplement SetDel SetDifference SetIntersect SetUnion SGE SGT SLE SLT Sqrt Store substitute Sum ToInt ToReal UGE UGT ULE ULT Var Xor

Other

name Optimize BUDiv Div Mod Neg Product simplify Sub

Classes

ReadonlyAstMap

AstMap: new <
    Key extends Ast<Name, unknown> = AnyAst<Name>,
    Value extends Ast<Name, unknown> = AnyAst<Name>,
>() => AstMap<Name, Key, Value>

ReadonlyAstVector

AstVector: new <Item extends Ast<Name, unknown> = AnyAst<Name>>() => AstVector<
    Name,
    Item,
>

ReadonlyModel

Model: new () => Model<Name>

Creates an empty Model

See

Solver.model for common usage of Model

ReadonlySolver

Solver: new (logic?: string) => Solver<Name>

Creates a Solver

Type declaration

    • new (logic?: string): Solver<Name>

    • Parameters

      • Optionallogic: string

        Optional logic which the solver will use. Creates a general Solver otherwise

      Returns Solver<Name>

ReadonlyTactic

Tactic: new (name: string) => Tactic<Name>

Expressions

ReadonlyArray

Array: SMTArrayCreation<Name>

ReadonlyBitVec

BitVec: BitVecCreation<Name>

ReadonlyBool

Bool: BoolCreation<Name>

ReadonlyDatatype

Datatype: DatatypeCreation<Name>

ReadonlyFunction

Function: FuncDeclCreation<Name>

ReadonlyInt

Int: IntCreation<Name>

ReadonlyReal

Real: RealCreation<Name>

ReadonlyRecFunc

RecFunc: RecFuncCreation<Name>

ReadonlySet

Set: SMTSetCreation<Name>

ReadonlySort

Sort: SortCreation<Name>

Functions

eqIdentity

from

getVarIndex

interrupt

isAnd

isApp

isAppOf

  • isAppOf(obj: unknown, kind: Z3_decl_kind): boolean

  • Parameters

    • obj: unknown
    • kind: Z3_decl_kind

    Returns boolean

isArith

isArithSort

isArray

isArraySort

isAst

isAstVector

isBitVec

isBitVecSort

isBitVecVal

isBool

isConst

isConstArray

isDistinct

isEq

isExpr

isFalse

isFuncDecl

isFuncInterp

isImplies

isInt

isIntSort

isIntVal

isModel

isNot

isOr

isProbe

isQuantifier

isReal

isRealSort

isRealVal

isSort

isTactic

isTrue

isVar

solve

  • solve(...assertions: Bool<Name>[]): Promise<"unsat" | "unknown" | Model<Name>>

  • Sugar function for getting a model for given assertions

    const x = Int.const('x');
    const y = Int.const('y');
    const result = await solve(x.le(y));
    if (isModel(result)) {
      console.log('Z3 found a solution');
      console.log(`x=${result.get(x)}, y=${result.get(y)}`);
    } else {
      console.error('No solution found');
    }

    Parameters

    Returns Promise<"unsat" | "unknown" | Model<Name>>

    See

    Solver

Operations

And

ast_from_string

AtLeast

AtMost

BV2Int

Cbrt

Concat

Cond

Const

Consts

Distinct

EmptySet

Eq

Exists

Extract

ForAll

FreshConst

FullSet

GE

GT

If

Iff

Implies

Int2BV

IsInt

isMember

isSubset

Lambda

LE

LT

Not

Or

PbEq

PbGe

PbLe

Select

SetAdd

SetComplement

SetDel

SetDifference

SetIntersect

SetUnion

SGE

SGT

SLE

SLT

Sqrt

Store

substitute

Sum

ToInt

ToReal

UGE

UGT

ULE

ULT

Var

Xor

Other

Readonlyname

name: Name

Name of the current Context

const c = new Context('main')

c.name
// 'main'

ReadonlyOptimize

Optimize: new () => Optimize<Name>

BUDiv

Div

Mod

Neg

Product

simplify

Sub

Settings

Member Visibility

On This Page

Classes
Expressions
Functions
Operations
Other