Interface SMTSet<Name, ElemSort>

Represents Set expression

interface SMTSet<
    Name extends string = "main",
    ElemSort extends AnySort<Name> = Sort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    add(
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
    ): SMTSet<Name, ElemSort>;
    arg(i: number): AnyExpr<Name>;
    children(): AnyExpr<Name>[];
    complement(): SMTSet<Name, ElemSort>;
    contains(
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
    ): Bool<Name>;
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    del(
        elem: CoercibleToMap<SortToExprMap<ElemSort, Name>, Name>,
    ): SMTSet<Name, ElemSort>;
    diff(b: SMTSet<Name, ElemSort>): SMTSet<Name, ElemSort>;
    elemSort(): ElemSort;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    intersect(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
    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>>
    )[];
    sexpr(): string;
    subsetOf(b: SMTSet<Name, ElemSort>): Bool<Name>;
    union(...args: SMTSet<Name, ElemSort>[]): SMTSet<Name, ElemSort>;
}

Type Parameters

  • Name extends string = "main"
  • ElemSort extends AnySort<Name> = Sort<Name>

    The sort of the element of the set

Hierarchy (View Summary)

Properties

ctx

Accessors

ast sort

Methods

add arg children complement contains decl del diff elemSort eq eqIdentity hash id intersect name neq neqIdentity numArgs params sexpr subsetOf union

Properties

Readonlyctx

ctx: Context<Name>

Accessors

ast

sort

Methods

add

arg

children

complement

contains

decl

del

diff

elemSort

eq

eqIdentity

hash

id

intersect

name

neq

neqIdentity

numArgs

params

sexpr

subsetOf

union

Settings

Member Visibility

On This Page

Properties
Accessors
Methods