Public Member Functions | |
Z3_goal_prec | getPrecision () |
boolean | isPrecise () |
boolean | isUnderApproximation () |
boolean | isOverApproximation () |
boolean | isGarbage () |
final void | add (Expr< BoolSort >... 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) |
Additional Inherited Members | |
Static Public Member Functions inherited from Z3Object | |
static long[] | arrayToNative (Z3Object[] a) |
static int | arrayLength (Z3Object[] a) |
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.
Adds the
to the given goal.
Z3Exception |
Definition at line 80 of file Goal.java.
Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().
|
inline |
Returns a string representation of the Goal.
Definition at line 222 of file Goal.java.
Convert a model for the goal into a model of the original goal from which this goal was derived.
Z3Exception |
Definition at line 250 of file Goal.java.
|
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 35 of file Goal.java.
Referenced by Goal.isGarbage(), Goal.isOverApproximation(), Goal.isPrecise(), and Goal.isUnderApproximation().
|
inline |
|
inline |
|
inline |
|
inline |
|
inline |
Indicates whether the goal is an over-approximation.
|
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 119 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
.
Z3Exception |
Definition at line 170 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__().