Interface Re<Name, SeqSortRef>

Regular expression expression

interface Re<
    Name extends string = "main",
    SeqSortRef extends SeqSort<Name> = SeqSort<Name>,
> {
    ctx: Context<Name>;
    get ast(): Z3_ast;
    get sort(): S;
    arg(i: number): AnyExpr<Name>;
    children(): AnyExpr<Name>[];
    complement(): Re<Name, SeqSortRef>;
    concat(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    diff(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    hash(): number;
    id(): number;
    intersect(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
    loop(lo: number, hi?: number): Re<Name, SeqSortRef>;
    name(): string | number;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    numArgs(): number;
    option(): Re<Name, SeqSortRef>;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    plus(): Re<Name, SeqSortRef>;
    power(n: number): Re<Name, SeqSortRef>;
    sexpr(): string;
    star(): Re<Name, SeqSortRef>;
    union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>;
}

Type Parameters

Name extends string = "main"
SeqSortRef extends SeqSort<Name> = SeqSort<Name>

Hierarchy (View Summary)

Expr<Name, ReSort<Name, SeqSortRef>, Z3_ast>
- Re

Index

Operations

complement concat diff intersect loop option plus power star union

Other

ctx ast sort arg children decl eq eqIdentity hash id name neq neqIdentity numArgs params sexpr

Operations

loop

loop(lo: number, hi?: number): Re<Name, SeqSortRef>
Create a bounded repetition of this regex
Parameters
- lo: number
  Minimum number of repetitions
- Optionalhi: number
  Maximum number of repetitions (0 means unbounded, i.e., at least lo)
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3271

option

option(): Re<Name, SeqSortRef>
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3248

plus

plus(): Re<Name, SeqSortRef>
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3242

power

power(n: number): Re<Name, SeqSortRef>
Parameters
- n: number
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3274

star

star(): Re<Name, SeqSortRef>
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3245

union

union(other: Re<Name, SeqSortRef>): Re<Name, SeqSortRef>
Parameters
- other: Re<Name, SeqSortRef>
Returns Re<Name, SeqSortRef>
- Defined in src/high-level/types.ts:3254

Other

`Readonly`ctx

ctx: Context<Name>

ast

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

sort

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

arg

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

children

children(): AnyExpr<Name>[]
Returns AnyExpr<Name>[]
Inherited from Expr.children
- Defined in src/high-level/types.ts:1856

decl

decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>
Returns FuncDecl<Name, Sort<Name>[], Sort<Name>>
Inherited from Expr.decl
- Defined in src/high-level/types.ts:1850

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:1842

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:954

hash

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

id

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

name

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

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:1844

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:956

numArgs

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

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:1846

sexpr

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

Interface Re<Name, SeqSortRef>

Type Parameters

Hierarchy (View Summary)

Index

Operations

Other

Operations

complement

Returns Re<Name, SeqSortRef>

concat

Parameters

Returns Re<Name, SeqSortRef>

diff

Parameters

Returns Re<Name, SeqSortRef>

intersect

Parameters

Returns Re<Name, SeqSortRef>

loop

Parameters

Returns Re<Name, SeqSortRef>

option

Returns Re<Name, SeqSortRef>

plus

Returns Re<Name, SeqSortRef>

power

Parameters

Returns Re<Name, SeqSortRef>

star

Returns Re<Name, SeqSortRef>

union

Parameters

Returns Re<Name, SeqSortRef>

Other

Readonlyctx

ast

Returns Z3_ast

sort

Returns S

arg

Parameters

Returns AnyExpr<Name>

children

Returns AnyExpr<Name>[]

decl

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

eq

Parameters

Returns Bool<Name>

eqIdentity

Parameters

Returns boolean

hash

Returns number

id

Returns number

name

Returns string | number

neq

Parameters

Returns Bool<Name>

neqIdentity

Parameters

Returns boolean

numArgs

Returns number

params

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

sexpr

Returns string

Settings

On This Page

`Readonly`ctx

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