Interface ApplyResult<Name>

ApplyResult contains the subgoals produced by applying a tactic to a goal.

interface ApplyResult<Name extends string = "main"> {
    ctx: Context<Name>;
    ptr: Z3_apply_result;
    getSubgoal(i: number): Goal<Name>;
    length(): number;
    toString(): string;
    [index: number]: Goal<Name>;
}

Type Parameters

Name extends string = "main"

Indexable

[index: number]: Goal<Name>
Get subgoal at index (alias for getSubgoal).

Index

Properties

Methods

getSubgoal length toString

Properties

`Readonly`ctx

ctx: Context<Name>

`Readonly`ptr

ptr: Z3_apply_result

Methods

getSubgoal

getSubgoal(i: number): Goal<Name>
Return a subgoal at the given index.
Parameters
- i: number
Returns Goal<Name>
- Defined in src/high-level/types.ts:3057

length

length(): number
Return the number of subgoals in the result.

Returns number
- Defined in src/high-level/types.ts:3052

toString

toString(): string
Return a string representation of the apply result.

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