Public Member Functions | |
Z3_goal_prec | getPrecision () throws Z3Exception |
boolean | isPrecise () throws Z3Exception |
boolean | isUnderApproximation () throws Z3Exception |
boolean | isOverApproximation () throws Z3Exception |
boolean | isGarbage () throws Z3Exception |
void | add (BoolExpr...constraints) throws Z3Exception |
boolean | inconsistent () throws Z3Exception |
int | getDepth () throws Z3Exception |
void | reset () throws Z3Exception |
int | size () throws Z3Exception |
BoolExpr[] | getFormulas () throws Z3Exception |
int | getNumExprs () throws Z3Exception |
boolean | isDecidedSat () throws Z3Exception |
boolean | isDecidedUnsat () throws Z3Exception |
Goal | translate (Context ctx) throws Z3Exception |
Goal | simplify () throws Z3Exception |
Goal | simplify (Params p) throws Z3Exception |
String | toString () |
![]() | |
void | dispose () throws Z3Exception |
![]() | |
void | dispose () throws Z3Exception |
Additional Inherited Members | |
![]() | |
void | finalize () throws Z3Exception |
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
|
inline |
Adds the constraints to the given goal.
Z3Exception |
|
inline |
|
inline |
|
inline |
|
inline |
The precision of the goal.
Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.
Definition at line 35 of file Goal.java.
Referenced by Goal.isGarbage(), Goal.isOverApproximation(), Goal.isPrecise(), and Goal.isUnderApproximation().
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
Definition at line 69 of file Goal.java.
|
inline |
Indicates whether the goal is an over-approximation.
Definition at line 60 of file Goal.java.
|
inline |
Indicates whether the goal is precise.
Definition at line 44 of file Goal.java.
|
inline |
Indicates whether the goal is an under-approximation.
Definition at line 52 of file Goal.java.
|
inline |
|
inline |
|
inline |
|
inline |
The number of formulas in the goal.
Definition at line 117 of file Goal.java.
Referenced by Goal.getFormulas().
|
inline |
|
inline |
Translates (copies) the Goal to the target Context ctx .
Z3Exception |