Interface Datatype<Name>

Helper class for declaring Z3 datatypes.

Follows the same pattern as Python Z3 API for declaring constructors before creating the actual datatype sort.

Example

const List = new ctx.Datatype('List');
List.declare('cons', ['car', ctx.Int.sort()], ['cdr', List]);
List.declare('nil');
const ListSort = List.create();
interface Datatype<Name extends string = "main"> {
    ctx: Context<Name>;
    name: string;
    create(): DatatypeSort<Name>;
    createPolymorphic(typeParams: AnySort<Name>[]): DatatypeSort<Name>;
    declare(
        name: string,
        ...fields: [string, Datatype<Name> | AnySort<Name>][],
    ): this;
}

Type Parameters

  • Name extends string = "main"

Properties

ctx name

Methods

create createPolymorphic declare

Properties

Readonlyctx

ctx: Context<Name>

Readonlyname

name: string

Methods

create

createPolymorphic

  • createPolymorphic(typeParams: AnySort<Name>[]): DatatypeSort<Name>

  • Create a polymorphic datatype sort with explicit type parameters. Type parameters should be sorts created with Context.TypeVariable. Self-recursive fields may reference this Datatype object directly.

    Parameters

    • typeParams: AnySort<Name>[]

      Array of type variable sorts

    Returns DatatypeSort<Name>

declare

  • declare(
        name: string,
        ...fields: [string, Datatype<Name> | AnySort<Name>][],
    ): this

  • Declare a constructor for this datatype.

    Parameters

    • name: string

      Constructor name

    • ...fields: [string, Datatype<Name> | AnySort<Name>][]

      Array of [field_name, field_sort] pairs

    Returns this

Settings

Member Visibility

On This Page

Properties
Methods