Interface SMTArraySort<Name, DomainSort, RangeSort>

A Sort representing a SMT Array with range of sort range and a domain of sort domain

interface SMTArraySort<
    Name extends string = "main",
    DomainSort extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
    RangeSort extends AnySort<Name> = AnySort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    cast(expr: CoercibleToExpr<Name>): Expr<Name, AnySort<Name>, unknown>;
    domain(): DomainSort[0];
    domain_n<T extends number>(i: T): DomainSort[T];
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    kind(): Z3_sort_kind;
    name(): string | number;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    range(): RangeSort;
    sexpr(): string;
    subsort(other: Sort<Name>): boolean;
}

Type Parameters

  • Name extends string = "main"
  • DomainSort extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]]

    The sort of the domain of the array (provided as an array of sorts)

  • RangeSort extends AnySort<Name> = AnySort<Name>

    The sort of the array range

Hierarchy (View Summary)

Properties

ctx

Accessors

ast

Methods

cast domain domain_n eqIdentity hash id kind name neqIdentity range sexpr subsort

Properties

Readonlyctx

ctx: Context<Name>

Accessors

ast

Methods

cast

domain

domain_n

eqIdentity

hash

id

kind

name

neqIdentity

range

sexpr

subsort

Settings

Member Visibility

On This Page

Properties
Accessors
Methods