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 () |
Model | convertModel (Model m) |
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 |
Definition at line 79 of file Goal.java.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
|
inline |
Convert a model for the goal into a model of the original goal from which this goal was derived.
g
Z3Exception |
Definition at line 249 of file Goal.java.
|
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).
|
inline |
|
inline |
Indicates whether the goal is precise.
|
inline |
Indicates whether the goal is an under-approximation.
|
inline |
|
inline |
Simplifies the goal. Remarks: Essentially invokes the ‘simplify’ tactic on the goal.
|
inline |
The number of formulas in the goal.
Definition at line 118 of file Goal.java.
Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Goal.AsBoolExpr(), Goal.getFormulas(), and BitVecSortRef.subsort().
|
inline |
Translates (copies) the Goal to the target Context ctx
.
Z3Exception |
Definition at line 169 of file Goal.java.
Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().