Interface Quantifier<Name, QVarSorts, QSort>

interface Quantifier<
    Name extends string = "main",
    QVarSorts extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]],
    QSort extends
        BoolSort<Name> | SMTArraySort<Name, QVarSorts> =
        | BoolSort<Name>
        | SMTArraySort<Name, QVarSorts>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    arg(i: number): AnyExpr<Name>;
    body(): BodyT<Name, QVarSorts, QSort>;
    children(): [BodyT<Name, QVarSorts, QSort>];
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    is_exists(): boolean;
    is_forall(): boolean;
    is_lambda(): boolean;
    name(): string | number;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    no_pattern(i: number): Expr<Name, AnySort<Name>, unknown>;
    num_no_patterns(): number;
    num_patterns(): number;
    num_vars(): number;
    numArgs(): number;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    pattern(i: number): Pattern<Name>;
    sexpr(): string;
    var_name(i: number): string | number;
    var_sort<T extends number>(i: T): QVarSorts[T];
    weight(): number;
}

Type Parameters

Name extends string = "main"
QVarSorts extends NonEmptySortArray<Name> = [Sort<Name>, ...Sort<Name>[]]
QSort extends BoolSort<Name> | SMTArraySort<Name, QVarSorts> = BoolSort<Name> | SMTArraySort<Name, QVarSorts>

Hierarchy (View Summary)

Expr<Name, QSort>
- Quantifier

Index

Properties

ctx

Accessors

ast sort

Properties

`Readonly`ctx

ctx: Context<Name>

Accessors

ast

get ast(): Z3_ast
Returns Z3_ast
Inherited from Expr.ast
- Defined in src/high-level/types.ts:689

sort

get sort(): S
Returns S
Inherited from Expr.sort
- Defined in src/high-level/types.ts:1081

Methods

arg

arg(i: number): AnyExpr<Name>
Parameters
- i: number
Returns AnyExpr<Name>
Inherited from Expr.arg
- Defined in src/high-level/types.ts:1095

eq

eq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Expr.eq
- Defined in src/high-level/types.ts:1083

eqIdentity

eqIdentity(other: Ast<Name, unknown>): boolean
Parameters
- other: Ast<Name, unknown>
Returns boolean
Inherited from Expr.eqIdentity
- Defined in src/high-level/types.ts:694

hash

hash(): number
Returns number
Inherited from Expr.hash
- Defined in src/high-level/types.ts:700

id

id(): number
Returns number
Inherited from Expr.id
- Defined in src/high-level/types.ts:692

is_exists

is_exists(): boolean
Returns boolean
- Defined in src/high-level/types.ts:1908

is_forall

is_forall(): boolean
Returns boolean
- Defined in src/high-level/types.ts:1906

is_lambda

is_lambda(): boolean
Returns boolean
- Defined in src/high-level/types.ts:1910

name

name(): string | number
Returns string | number
Inherited from Expr.name
- Defined in src/high-level/types.ts:1089

neq

neq(other: CoercibleToExpr<Name>): Bool<Name>
Parameters
- other: CoercibleToExpr<Name>
Returns Bool<Name>
Inherited from Expr.neq
- Defined in src/high-level/types.ts:1085

neqIdentity

neqIdentity(other: Ast<Name, unknown>): boolean
Parameters
- other: Ast<Name, unknown>
Returns boolean
Inherited from Expr.neqIdentity
- Defined in src/high-level/types.ts:696

no_pattern

no_pattern(i: number): Expr<Name, AnySort<Name>, unknown>
Parameters
- i: number
Returns Expr<Name, AnySort<Name>, unknown>
- Defined in src/high-level/types.ts:1920

num_no_patterns

num_no_patterns(): number
Returns number
- Defined in src/high-level/types.ts:1918

num_patterns

num_patterns(): number
Returns number
- Defined in src/high-level/types.ts:1914

num_vars

num_vars(): number
Returns number
- Defined in src/high-level/types.ts:1924

numArgs

numArgs(): number
Returns number
Inherited from Expr.numArgs
- Defined in src/high-level/types.ts:1093

params

params(): (
    | string
    | number
    | Sort<Name>
    | Expr<Name, AnySort<Name>, unknown>
    | FuncDecl<Name, Sort<Name>[], Sort<Name>>
)[]
Returns (
    | string
    | number
    | Sort<Name>
    | Expr<Name, AnySort<Name>, unknown>
    | FuncDecl<Name, Sort<Name>[], Sort<Name>>
)[]
Inherited from Expr.params
- Defined in src/high-level/types.ts:1087

pattern

pattern(i: number): Pattern<Name>
Parameters
- i: number
Returns Pattern<Name>
- Defined in src/high-level/types.ts:1916

sexpr

sexpr(): string
Returns string
Inherited from Expr.sexpr
- Defined in src/high-level/types.ts:698

var_name

var_name(i: number): string | number
Parameters
- i: number
Returns string | number
- Defined in src/high-level/types.ts:1926

var_sort

var_sort<T extends number>(i: T): QVarSorts[T]
Type Parameters
- T extends number
Parameters
- i: T
Returns QVarSorts[T]
- Defined in src/high-level/types.ts:1928

weight

weight(): number
Returns number
- Defined in src/high-level/types.ts:1912

Interface Quantifier<Name, QVarSorts, QSort>

Type Parameters

Hierarchy (View Summary)

Index

Properties

Accessors

Methods

Properties

Readonlyctx

Accessors

ast

Returns Z3_ast

sort

Returns S

Methods

arg

Parameters

Returns AnyExpr<Name>

body

Returns BodyT<Name, QVarSorts, QSort>

children

Returns [BodyT<Name, QVarSorts, QSort>]

decl

Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>

eq

Parameters

Returns Bool<Name>

eqIdentity

Parameters

Returns boolean

hash

Returns number

id

Returns number

is_exists

Returns boolean

is_forall

Returns boolean

is_lambda

Returns boolean

name

Returns string | number

neq

Parameters

Returns Bool<Name>

neqIdentity

Parameters

Returns boolean

no_pattern

Parameters

Returns Expr<Name, AnySort<Name>, unknown>

num_no_patterns

Returns number

num_patterns

Returns number

num_vars

Returns number

numArgs

Returns number

params

Returns ( | string | number | Sort<Name> | Expr<Name, AnySort<Name>, unknown> | FuncDecl<Name, Sort<Name>[], Sort<Name>>)[]

pattern

Parameters

Returns Pattern<Name>

sexpr

Returns string

var_name

Parameters

Returns string | number

var_sort

Type Parameters

Parameters

Returns QVarSorts[T]

weight

Returns number

Settings

On This Page

`Readonly`ctx

Returns (
| string
| number
| Sort<Name>
| Expr<Name, AnySort<Name>, unknown>
| FuncDecl<Name, Sort<Name>[], Sort<Name>>
)[]