Public Member Functions | |
int | getNumSubgoals () throws Z3Exception |
Goal[] | getSubgoals () throws Z3Exception |
Model | convertModel (int i, Model m) throws Z3Exception |
String | toString () |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
Definition at line 24 of file ApplyResult.java.
|
inline |
Convert a model for the subgoal i into a model for the original goal g
, that the ApplyResult was obtained from.
g
Z3Exception |
Definition at line 57 of file ApplyResult.java.
|
inline |
The number of Subgoals.
Definition at line 29 of file ApplyResult.java.
Referenced by ApplyResult.getSubgoals(), and Goal.simplify().
|
inline |
Retrieves the subgoals from the ApplyResult.
Z3Exception |
Definition at line 40 of file ApplyResult.java.
Referenced by Goal.simplify().
|
inline |
A string representation of the ApplyResult.
Definition at line 66 of file ApplyResult.java.