Public Member Functions | |
Z3_goal_prec | getPrecision () |
boolean | isPrecise () |
boolean | isUnderApproximation () |
boolean | isOverApproximation () |
boolean | isGarbage () |
void | add (BoolExpr...constraints) |
boolean | inconsistent () |
int | getDepth () |
void | reset () |
int | size () |
BoolExpr[] | getFormulas () |
int | getNumExprs () |
boolean | isDecidedSat () |
boolean | isDecidedUnsat () |
Goal | translate (Context ctx) |
Goal | simplify () |
Goal | simplify (Params p) |
String | toString () |
BoolExpr | AsBoolExpr () |
![]() | |
void | dispose () |
![]() | |
void | dispose () |
Additional Inherited Members | |
![]() | |
void | finalize () |
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
|
inline |
|
inline |
|
inline |
|
inline |
The formulas in the goal.
Z3Exception |
Definition at line 129 of file Goal.java.
Referenced by Goal.AsBoolExpr().
|
inline |
|
inline |
The precision of the goal. Remarks: 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 36 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 70 of file Goal.java.
|
inline |
Indicates whether the goal is an over-approximation.
Definition at line 61 of file Goal.java.
|
inline |
Indicates whether the goal is precise.
Definition at line 45 of file Goal.java.
|
inline |
Indicates whether the goal is an under-approximation.
Definition at line 53 of file Goal.java.
|
inline |
|
inline |
|
inline |
The number of formulas in the goal.
Definition at line 119 of file Goal.java.
Referenced by Goal.AsBoolExpr(), and Goal.getFormulas().
|
inline |