Interface DatatypeSort<Name>

A Sort representing an algebraic datatype.

After creation, this sort will have constructor, recognizer, and accessor functions dynamically attached based on the declared constructors.

interface DatatypeSort<Name extends string = "main"> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    accessor(
        constructorIdx: number,
        accessorIdx: number,
    ): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    cast(other: CoercibleToExpr<Name>): DatatypeExpr<Name>;
    cast(other: DatatypeExpr<Name>): DatatypeExpr<Name>;
    constructorDecl(idx: number): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    kind(): Z3_sort_kind;
    name(): string | number;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    numConstructors(): number;
    recognizer(idx: number): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    sexpr(): string;
    subsort(other: Sort<Name>): boolean;
}

Type Parameters

  • Name extends string = "main"

Hierarchy (View Summary)

Properties

ctx

Accessors

ast

Methods

accessor cast constructorDecl eqIdentity hash id kind name neqIdentity numConstructors recognizer sexpr subsort

Properties

Readonlyctx

ctx: Context<Name>

Accessors

ast

Methods

accessor

cast

constructorDecl

eqIdentity

hash

id

kind

name

neqIdentity

numConstructors

recognizer

sexpr

subsort

Settings

Member Visibility

On This Page

Properties
Accessors
Methods