Interface FiniteSet<Name, ElemSort>

Represents a finite set expression

interface FiniteSet<
    Name extends string = "main",
    ElemSort extends Sort<Name> = Sort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    arg(i: number): AnyExpr<Name>;
    children(): AnyExpr<Name>[];
    contains(elem: Expr<Name, AnySort<Name>, unknown>): Bool<Name>;
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    diff(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    filter(f: Expr<Name, AnySort<Name>, unknown>): FiniteSet<Name, ElemSort>;
    hash(): number;
    id(): number;
    intersect(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
    map(f: Expr<Name, AnySort<Name>, unknown>): FiniteSet<Name, Sort<Name>>;
    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;
    size(): Expr<Name, AnySort<Name>, unknown>;
    subsetOf(other: FiniteSet<Name, ElemSort>): Bool<Name>;
    union(other: FiniteSet<Name, ElemSort>): FiniteSet<Name, ElemSort>;
}

Type Parameters

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

    The sort of elements in the finite set

Hierarchy (View Summary)

Properties

ctx

Accessors

ast sort

Methods

arg children contains decl diff eq eqIdentity filter hash id intersect map name neq neqIdentity numArgs params sexpr size subsetOf union

Properties

Readonlyctx

ctx: Context<Name>

Accessors

ast

sort

Methods

arg

children

contains

decl

diff

eq

eqIdentity

filter

hash

id

intersect

map

name

neq

neqIdentity

numArgs

params

sexpr

size

subsetOf

union

Settings

Member Visibility

On This Page

Properties
Accessors
Methods