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>;
    Fixedpoint: new () => Fixedpoint<Name>;
    Float: FPCreation<Name>;
    FloatRM: FPRMCreation<Name>;
    Function: FuncDeclCreation<Name>;
    Goal: new (
        models?: boolean,
        unsat_cores?: boolean,
        proofs?: boolean,
    ) => Goal<Name>;
    Int: IntCreation<Name>;
    Model: new () => Model<Name>;
    name: Name;
    Optimize: new () => Optimize<Name>;
    Params: new () => Params<Name>;
    RCFNum: RCFNumCreation<Name>;
    Re: ReCreation<Name>;
    Real: RealCreation<Name>;
    RecFunc: RecFuncCreation<Name>;
    Seq: SeqCreation<Name>;
    Set: SMTSetCreation<Name>;
    Simplifier: new (name: string) => Simplifier<Name>;
    Solver: new (logic?: string) => Solver<Name>;
    Sort: SortCreation<Name>;
    String: StringCreation<Name>;
    Tactic: new (name: string) => Tactic<Name>;
    AllChar<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        reSort: ReSort<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    And(): Bool<Name>;
    And(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
    And(...args: (boolean | Bool<Name>)[]): Bool<Name>;
    And(...args: Probe<Name>[]): Probe<Name>;
    AndThen(
        t1: string | Tactic<Name>,
        t2: string | Tactic<Name>,
        ...ts: (string | Tactic<Name>)[],
    ): Tactic<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>;
    Complement<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    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>[];
    Diff<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        a: Re<Name, SeqSortRef>,
        b: Re<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    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>;
    Empty<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        reSort: ReSort<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    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>;
    Ext<
        DomainSort extends [Sort<Name>, ...Sort<Name>[]],
        RangeSort extends Sort<Name> = Sort<Name>,
    >(
        a: SMTArray<Name, DomainSort, RangeSort>,
        b: SMTArray<Name, DomainSort, RangeSort>,
    ): SortToExprMap<DomainSort[0], Name>;
    Extract<Bits extends number>(
        hi: number,
        lo: number,
        val: BitVec<Bits, Name>,
    ): BitVec<number, Name>;
    Fail(): Tactic<Name>;
    FailIf(p: Probe<Name>): Tactic<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;
    Full<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        reSort: ReSort<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    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>;
    InRe(
        seq: string | Seq<Name, Sort<Name>>,
        re: Re<Name, SeqSort<Name, Sort<Name>>>,
    ): Bool<Name>;
    Int2BV<Bits extends number>(
        a: number | bigint | Arith<Name>,
        bits: Bits,
    ): BitVec<Bits, Name>;
    interrupt(): void;
    Intersect<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        ...res: Re<Name, SeqSortRef>[],
    ): Re<Name, SeqSortRef>;
    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;
    isFP(obj: unknown): obj is FP<Name>;
    isFPRM(obj: unknown): obj is FPRM<Name>;
    isFPRMSort(obj: unknown): obj is FPRMSort<Name>;
    isFPSort(obj: unknown): obj is FPSort<Name>;
    isFPVal(obj: unknown): obj is FPNum<Name>;
    isFuncDecl(obj: unknown): obj is FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    isFuncInterp(obj: unknown): obj is FuncInterp<Name>;
    isGoal(obj: unknown): obj is Goal<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>>,
    >;
    isRCFNum(obj: unknown): obj is RCFNum<Name>;
    isReal(obj: unknown): boolean;
    isRealSort(obj: unknown): boolean;
    isRealVal(obj: unknown): obj is RatNum<Name>;
    isSeq(obj: unknown): obj is Seq<Name, Sort<Name>>;
    isSeqSort(obj: unknown): obj is SeqSort<Name, Sort<Name>>;
    isSort(obj: unknown): obj is Sort<Name>;
    isString(obj: unknown): obj is Seq<Name, Sort<Name>>;
    isStringSort(obj: unknown): obj is SeqSort<Name, 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>;
    Loop<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
        lo: number,
        hi?: number,
    ): Re<Name, SeqSortRef>;
    LT(a: Arith<Name>, b: CoercibleToArith<Name>): Bool<Name>;
    mkPartialOrder(
        sort: Sort<Name>,
        index: number,
    ): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    mkTransitiveClosure(
        f: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
    ): FuncDecl<Name, Sort<Name>[], Sort<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>;
    Option<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    Or(): Bool<Name>;
    Or(vector: AstVector<Name, Bool<Name>>): Bool<Name>;
    Or(...args: (boolean | Bool<Name>)[]): Bool<Name>;
    Or(...args: Probe<Name>[]): Probe<Name>;
    OrElse(
        t1: string | Tactic<Name>,
        t2: string | Tactic<Name>,
        ...ts: (string | Tactic<Name>)[],
    ): Tactic<Name>;
    ParAndThen(
        t1: string | Tactic<Name>,
        t2: string | Tactic<Name>,
    ): Tactic<Name>;
    ParOr(...tactics: (string | Tactic<Name>)[]): Tactic<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>;
    Plus<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    polynomialSubresultants(
        p: Arith<Name>,
        q: Arith<Name>,
        x: Arith<Name>,
    ): Promise<AstVector<Name, Arith<Name>>>;
    Power<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
        n: number,
    ): Re<Name, SeqSortRef>;
    Product(arg0: Arith<Name>, ...args: CoercibleToArith<Name>[]): Arith<Name>;
    Product<Bits extends number>(
        arg0: BitVec<Bits, Name>,
        ...args: CoercibleToBitVec<Bits, Name>[],
    ): BitVec<Bits, Name>;
    Range<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        lo: string | Seq<Name, SeqSortRef>,
        hi: string | Seq<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    ReConcat<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        ...res: Re<Name, SeqSortRef>[],
    ): Re<Name, SeqSortRef>;
    Repeat(t: string | Tactic<Name>, max?: number): Tactic<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>;
    setPrintMode(mode: Z3_ast_print_mode): void;
    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>>;
    Skip(): Tactic<Name>;
    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>;
    Star<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        re: Re<Name, SeqSortRef>,
    ): Re<Name, SeqSortRef>;
    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>;
    substituteFuns(
        t: Expr<Name, AnySort<Name>, unknown>,
        ...substitutions: [
            FuncDecl<Name, Sort<Name>[], Sort<Name>>,
            Expr<Name, AnySort<Name>, unknown>,
        ][],
    ): Expr<Name, AnySort<Name>, unknown>;
    substituteVars(
        t: Expr<Name, AnySort<Name>, unknown>,
        ...to: 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>;
    TryFor(t: string | Tactic<Name>, ms: number): Tactic<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>;
    Union<SeqSortRef extends SeqSort<Name, Sort<Name>>>(
        ...res: Re<Name, SeqSortRef>[],
    ): Re<Name, SeqSortRef>;
    updateField(
        t: DatatypeExpr<Name>,
        fieldAccessor: FuncDecl<Name, Sort<Name>[], Sort<Name>>,
        newValue: Expr<Name, AnySort<Name>, unknown>,
    ): DatatypeExpr<Name>;
    Var<S extends Sort<Name>>(idx: number, sort: S): SortToExprMap<S, Name>;
    When(p: Probe<Name>, t: string | Tactic<Name>): Tactic<Name>;
    With(t: string | Tactic<Name>, params: Record<string, any>): Tactic<Name>;
    Xor(a: boolean | Bool<Name>, b: boolean | Bool<Name>): Bool<Name>;
}