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 () |
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
to the given goal.
Z3Exception |
Definition at line 79 of file Goal.java.
Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().
|
inline |
|
inline |
|
inline |
The formulas in the goal.
Z3Exception |
Definition at line 128 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 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 |
The number of formulas in the goal.
Definition at line 118 of file Goal.java.
Referenced by Goal.AsBoolExpr(), and Goal.getFormulas().
|
inline |