Interface FuncDecl<Name, DomainSort, RangeSort>

interface FuncDecl<
    Name extends string = "main",
    DomainSort extends Sort<Name>[] = Sort<Name>[],
    RangeSort extends Sort<Name> = Sort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    arity(): number;
    call(
        ...args: [
            ...{
                [Key in string
                | number
                | symbol]: DomainSort[Key<Key>] extends AnySort<Name>
                    ? CoercibleToMap<SortToExprMap<any[any], Name>, Name>
                    : DomainSort[Key<Key>]
            }[],
        ],
    ): SortToExprMap<RangeSort, Name>;
    domain<T extends number>(i: T): DomainSort[T];
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    kind(): Z3_decl_kind;
    name(): string | number;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    range(): RangeSort;
    sexpr(): string;
}

Type Parameters

Hierarchy (View Summary)

Properties

Accessors

Methods

  • Parameters

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

    Returns SortToExprMap<RangeSort, Name>