Interface Seq<Name, ElemSort>

Sequence expression (includes strings)

interface Seq<
    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>;
    asString(): string;
    at(index: number | bigint | Arith<Name>): Seq<Name, ElemSort>;
    children(): AnyExpr<Name>[];
    concat(other: string | Seq<Name, ElemSort>): Seq<Name, ElemSort>;
    contains(substr: string | Seq<Name, ElemSort>): Bool<Name>;
    decl(): FuncDecl<Name, Sort<Name>[], Sort<Name>>;
    eq(other: CoercibleToExpr<Name>): Bool<Name>;
    eqIdentity(other: Ast<Name, unknown>): boolean;
    extract(
        offset: number | bigint | Arith<Name>,
        length: number | bigint | Arith<Name>,
    ): Seq<Name, ElemSort>;
    foldl(
        f: Expr<Name, AnySort<Name>, unknown>,
        a: Expr<Name, AnySort<Name>, unknown>,
    ): Expr<Name, AnySort<Name>, unknown>;
    foldli(
        f: Expr<Name, AnySort<Name>, unknown>,
        i: number | bigint | Arith<Name>,
        a: Expr<Name, AnySort<Name>, unknown>,
    ): Expr<Name, AnySort<Name>, unknown>;
    hash(): number;
    id(): number;
    indexOf(
        substr: string | Seq<Name, ElemSort>,
        offset?: number | bigint | Arith<Name>,
    ): Arith<Name>;
    isString(): boolean;
    lastIndexOf(substr: string | Seq<Name, ElemSort>): Arith<Name>;
    le(other: string | Seq<Name, ElemSort>): Bool<Name>;
    length(): Arith<Name>;
    lt(other: string | Seq<Name, ElemSort>): Bool<Name>;
    map(f: Expr<Name, AnySort<Name>, unknown>): Seq<Name, Sort<Name>>;
    mapi(
        f: Expr<Name, AnySort<Name>, unknown>,
        i: number | bigint | Arith<Name>,
    ): Seq<Name, Sort<Name>>;
    name(): string | number;
    neq(other: CoercibleToExpr<Name>): Bool<Name>;
    neqIdentity(other: Ast<Name, unknown>): boolean;
    nth(
        index: number | bigint | Arith<Name>,
    ): Expr<Name, AnySort<Name>, unknown>;
    numArgs(): number;
    params(): (
        | string
        | number
        | Sort<Name>
        | Expr<Name, AnySort<Name>, unknown>
        | FuncDecl<Name, Sort<Name>[], Sort<Name>>
    )[];
    prefixOf(s: string | Seq<Name, ElemSort>): Bool<Name>;
    replace(
        src: string | Seq<Name, ElemSort>,
        dst: string | Seq<Name, ElemSort>,
    ): Seq<Name, ElemSort>;
    replaceAll(
        src: string | Seq<Name, ElemSort>,
        dst: string | Seq<Name, ElemSort>,
    ): Seq<Name, ElemSort>;
    replaceRe(
        re: Re<Name, SeqSort<Name, Sort<Name>>>,
        dst: string | Seq<Name, ElemSort>,
    ): Seq<Name, ElemSort>;
    replaceReAll(
        re: Re<Name, SeqSort<Name, Sort<Name>>>,
        dst: string | Seq<Name, ElemSort>,
    ): Seq<Name, ElemSort>;
    sexpr(): string;
    suffixOf(s: string | Seq<Name, ElemSort>): Bool<Name>;
    toCode(): Arith<Name>;
    toInt(): Arith<Name>;
}

Type Parameters

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

Hierarchy (View Summary)

Expr<Name, SeqSort<Name, ElemSort>, Z3_ast>
- Seq

Index

Operations

at

at(index: number | bigint | Arith<Name>): Seq<Name, ElemSort>
Parameters
- index: number | bigint | Arith<Name>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3635

concat

concat(other: string | Seq<Name, ElemSort>): Seq<Name, ElemSort>
Parameters
- other: string | Seq<Name, ElemSort>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3629

contains

contains(substr: string | Seq<Name, ElemSort>): Bool<Name>
Parameters
- substr: string | Seq<Name, ElemSort>
Returns Bool<Name>
- Defined in src/high-level/types.ts:3650

extract

extract(
offset: number | bigint | Arith<Name>,
length: number | bigint | Arith<Name>,
): Seq<Name, ElemSort>
Parameters
- offset: number | bigint | Arith<Name>
- length: number | bigint | Arith<Name>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3641

foldl

foldl(
f: Expr<Name, AnySort<Name>, unknown>,
a: Expr<Name, AnySort<Name>, unknown>,
): Expr<Name, AnySort<Name>, unknown>
Left-fold function f over the sequence with initial accumulator a (seq.foldl).
Parameters
- f: Expr<Name, AnySort<Name>, unknown>
- a: Expr<Name, AnySort<Name>, unknown>
Returns Expr<Name, AnySort<Name>, unknown>
- Defined in src/high-level/types.ts:3710

foldli

foldli(
    f: Expr<Name, AnySort<Name>, unknown>,
    i: number | bigint | Arith<Name>,
    a: Expr<Name, AnySort<Name>, unknown>,
): Expr<Name, AnySort<Name>, unknown>
Left-fold function f with index over the sequence with initial accumulator a (seq.foldli).
Parameters
- f: Expr<Name, AnySort<Name>, unknown>
- i: number | bigint | Arith<Name>
- a: Expr<Name, AnySort<Name>, unknown>
Returns Expr<Name, AnySort<Name>, unknown>
- Defined in src/high-level/types.ts:3716

indexOf

indexOf(
substr: string | Seq<Name, ElemSort>,
offset?: number | bigint | Arith<Name>,
): Arith<Name>
Parameters
- substr: string | Seq<Name, ElemSort>
- Optionaloffset: number | bigint | Arith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:3644

lastIndexOf

lastIndexOf(substr: string | Seq<Name, ElemSort>): Arith<Name>
Parameters
- substr: string | Seq<Name, ElemSort>
Returns Arith<Name>
- Defined in src/high-level/types.ts:3647

le

le(other: string | Seq<Name, ElemSort>): Bool<Name>
String less-than-or-equal comparison (str.le).
Parameters
- other: string | Seq<Name, ElemSort>
Returns Bool<Name>
- Defined in src/high-level/types.ts:3692

length

length(): Arith<Name>
Returns Arith<Name>
- Defined in src/high-level/types.ts:3632

lt

lt(other: string | Seq<Name, ElemSort>): Bool<Name>
String less-than comparison (str.lt).
Parameters
- other: string | Seq<Name, ElemSort>
Returns Bool<Name>
- Defined in src/high-level/types.ts:3686

map

map(f: Expr<Name, AnySort<Name>, unknown>): Seq<Name, Sort<Name>>
Apply function f to each element of the sequence (seq.map).
Parameters
- f: Expr<Name, AnySort<Name>, unknown>
Returns Seq<Name, Sort<Name>>
- Defined in src/high-level/types.ts:3698

mapi

mapi(
f: Expr<Name, AnySort<Name>, unknown>,
i: number | bigint | Arith<Name>,
): Seq<Name, Sort<Name>>
Apply function f to each element and its index in the sequence (seq.mapi).
Parameters
- f: Expr<Name, AnySort<Name>, unknown>
- i: number | bigint | Arith<Name>
Returns Seq<Name, Sort<Name>>
- Defined in src/high-level/types.ts:3704

nth

nth(index: number | bigint | Arith<Name>): Expr<Name, AnySort<Name>, unknown>
Parameters
- index: number | bigint | Arith<Name>
Returns Expr<Name, AnySort<Name>, unknown>
- Defined in src/high-level/types.ts:3638

prefixOf

prefixOf(s: string | Seq<Name, ElemSort>): Bool<Name>
Parameters
- s: string | Seq<Name, ElemSort>
Returns Bool<Name>
- Defined in src/high-level/types.ts:3653

replace

replace(
src: string | Seq<Name, ElemSort>,
dst: string | Seq<Name, ElemSort>,
): Seq<Name, ElemSort>
Parameters
- src: string | Seq<Name, ElemSort>
- dst: string | Seq<Name, ElemSort>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3659

replaceAll

replaceAll(
src: string | Seq<Name, ElemSort>,
dst: string | Seq<Name, ElemSort>,
): Seq<Name, ElemSort>
Parameters
- src: string | Seq<Name, ElemSort>
- dst: string | Seq<Name, ElemSort>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3662

replaceRe

replaceRe(
re: Re<Name, SeqSort<Name, Sort<Name>>>,
dst: string | Seq<Name, ElemSort>,
): Seq<Name, ElemSort>
Parameters
- re: Re<Name, SeqSort<Name, Sort<Name>>>
- dst: string | Seq<Name, ElemSort>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3665

replaceReAll

replaceReAll(
re: Re<Name, SeqSort<Name, Sort<Name>>>,
dst: string | Seq<Name, ElemSort>,
): Seq<Name, ElemSort>
Parameters
- re: Re<Name, SeqSort<Name, Sort<Name>>>
- dst: string | Seq<Name, ElemSort>
Returns Seq<Name, ElemSort>
- Defined in src/high-level/types.ts:3668

suffixOf

suffixOf(s: string | Seq<Name, ElemSort>): Bool<Name>
Parameters
- s: string | Seq<Name, ElemSort>
Returns Bool<Name>
- Defined in src/high-level/types.ts:3656

toCode

toCode(): Arith<Name>
Convert a single-character string to its Unicode code point (str.to_code).

Returns Arith<Name>
- Defined in src/high-level/types.ts:3680

toInt

toInt(): Arith<Name>
Convert a string to its integer value (str.to.int).

Returns Arith<Name>
- Defined in src/high-level/types.ts:3674

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

sort

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

arg

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

asString

asString(): string
Get string value if this is a concrete string

Returns string
- Defined in src/high-level/types.ts:3626

children

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

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

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

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

hash

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

id

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

isString

isString(): boolean
Check if this is a string value

Returns boolean
- Defined in src/high-level/types.ts:3621

name

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

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

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

numArgs

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

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

sexpr

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

Interface Seq<Name, ElemSort>

Type Parameters

Hierarchy (View Summary)

Index

Operations

Other

Operations

at

Parameters

Returns Seq<Name, ElemSort>

concat

Parameters

Returns Seq<Name, ElemSort>

contains

Parameters

Returns Bool<Name>

extract

Parameters

Returns Seq<Name, ElemSort>

foldl

Parameters

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

foldli

Parameters

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

indexOf

Parameters

Returns Arith<Name>

lastIndexOf

Parameters

Returns Arith<Name>

le

Parameters

Returns Bool<Name>

length

Returns Arith<Name>

lt

Parameters

Returns Bool<Name>

map

Parameters

Returns Seq<Name, Sort<Name>>

mapi

Parameters

Returns Seq<Name, Sort<Name>>

nth

Parameters

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

prefixOf

Parameters

Returns Bool<Name>

replace

Parameters

Returns Seq<Name, ElemSort>

replaceAll

Parameters

Returns Seq<Name, ElemSort>

replaceRe

Parameters

Returns Seq<Name, ElemSort>

replaceReAll

Parameters

Returns Seq<Name, ElemSort>

suffixOf

Parameters

Returns Bool<Name>

toCode

Returns Arith<Name>

toInt

Returns Arith<Name>

Other

Readonlyctx

ast

Returns Z3_ast

sort

Returns S

arg

Parameters

Returns AnyExpr<Name>

asString

`Readonly`ctx

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