Interface SMTArray<Name, DomainSort, RangeSort>

Represents Array expression

interface SMTArray<
    Name extends string = "main",
    DomainSort extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
    RangeSort extends Sort<Name> = Sort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    arg(i: number): AnyExpr<Name>;
    children(): AnyExpr<Name>[];
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    domain(): DomainSort[0];
    domain_n<T extends number>(i: T): DomainSort[T];
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    name(): string | number;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    numArgs(): number;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    range(): RangeSort;
    select(
        ...indices: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                    : DomainSort[Key<Key>]
            }[],
        ],
    ): SortToExprMap<RangeSort, Name>;
    sexpr(): string;
    store(
        ...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>;
}

Type Parameters

Hierarchy (View Summary)

Properties

ctx

Accessors

ast sort

Methods

arg children decl domain domain_n eq eqIdentity hash id name neq neqIdentity numArgs params range select sexpr store

Properties

Readonlyctx

ctx: Context<Name>

Accessors

ast

sort

Methods

arg

children

decl

domain

domain_n

eq

eqIdentity

hash

id

name

neq

neqIdentity

numArgs

params

range

select

  • select(
        ...indices: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                    : DomainSort[Key<Key>]
            }[],
        ],
    ): SortToExprMap<RangeSort, Name>

  • Parameters

    • ...indices: [
          ...{
              [Key in string
              | number
              | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                  ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                  : DomainSort[Key<Key>]
          }[],
      ]

    Returns SortToExprMap<RangeSort, Name>

sexpr

store

  • store(
        ...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>

  • value should be coercible to RangeSort

    Parameters

    • ...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>,
      ]

      (idx0, idx1, ..., idxN, value)

    Returns SMTArray<Name, DomainSort, RangeSort>

Settings

Member Visibility

On This Page

Properties
Accessors
Methods