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 () |
Package Functions | |
Goal (Context ctx, long obj) throws Z3Exception | |
Goal (Context ctx, boolean models, boolean unsatCores, boolean proofs) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) 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.
Goal | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Goal | ( | Context | ctx, |
boolean | models, | ||
boolean | unsatCores, | ||
boolean | proofs | ||
) | throws Z3Exception [inline, package] |
void add | ( | BoolExpr... | constraints | ) | throws Z3Exception [inline] |
Adds the constraints to the given goal.
Z3Exception |
Definition at line 79 of file Goal.java.
{ getContext().checkContextMatch(constraints); for (BoolExpr c : constraints) { Native.goalAssert(getContext().nCtx(), getNativeObject(), c.getNativeObject()); } }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
int getDepth | ( | ) | throws Z3Exception [inline] |
The depth of the goal. This tracks how many transformations were applied to it.
Definition at line 101 of file Goal.java.
{ return Native.goalDepth(getContext().nCtx(), getNativeObject()); }
BoolExpr [] getFormulas | ( | ) | throws Z3Exception [inline] |
The formulas in the goal.
Z3Exception |
Definition at line 127 of file Goal.java.
{ int n = size(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = new BoolExpr(getContext(), Native.goalFormula(getContext() .nCtx(), getNativeObject(), i)); return res; }
int getNumExprs | ( | ) | throws Z3Exception [inline] |
The number of formulas, subformulas and terms in the goal.
Definition at line 140 of file Goal.java.
{ return Native.goalNumExprs(getContext().nCtx(), getNativeObject()); }
Z3_goal_prec getPrecision | ( | ) | throws Z3Exception [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().
{ return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(), getNativeObject())); }
boolean inconsistent | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal contains `false'.
Definition at line 92 of file Goal.java.
{ return Native.goalInconsistent(getContext().nCtx(), getNativeObject()); }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 234 of file Goal.java.
{ getContext().goal_DRQ().incAndClear(getContext(), o); super.incRef(o); }
boolean isDecidedSat | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal is empty, and it is precise or the product of an under approximation.
Definition at line 149 of file Goal.java.
{ return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject()); }
boolean isDecidedUnsat | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal contains `false', and it is precise or the product of an over approximation.
Definition at line 158 of file Goal.java.
{ return Native .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject()); }
boolean isGarbage | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).
Definition at line 69 of file Goal.java.
{ return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
boolean isOverApproximation | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal is an over-approximation.
Definition at line 60 of file Goal.java.
{ return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER; }
boolean isPrecise | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal is precise.
Definition at line 44 of file Goal.java.
{ return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE; }
boolean isUnderApproximation | ( | ) | throws Z3Exception [inline] |
Indicates whether the goal is an under-approximation.
Definition at line 52 of file Goal.java.
{ return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER; }
void reset | ( | ) | throws Z3Exception [inline] |
Erases all formulas from the given goal.
Definition at line 109 of file Goal.java.
{ Native.goalReset(getContext().nCtx(), getNativeObject()); }
Goal simplify | ( | ) | throws Z3Exception [inline] |
Simplifies the goal. Essentially invokes the `simplify' tactic on the goal.
Definition at line 180 of file Goal.java.
{ Tactic t = getContext().mkTactic("simplify"); ApplyResult res = t.apply(this); if (res.getNumSubgoals() == 0) throw new Z3Exception("No subgoals"); else return res.getSubgoals()[0]; }
Goal simplify | ( | Params | p | ) | throws Z3Exception [inline] |
Simplifies the goal. Essentially invokes the `simplify' tactic on the goal.
Definition at line 195 of file Goal.java.
{ Tactic t = getContext().mkTactic("simplify"); ApplyResult res = t.apply(this, p); if (res.getNumSubgoals() == 0) throw new Z3Exception("No subgoals"); else return res.getSubgoals()[0]; }
int size | ( | ) | throws Z3Exception [inline] |
The number of formulas in the goal.
Definition at line 117 of file Goal.java.
Referenced by Goal.getFormulas().
{ return Native.goalSize(getContext().nCtx(), getNativeObject()); }
String toString | ( | ) | [inline] |
Goal to string conversion.
Definition at line 211 of file Goal.java.
{ try { return Native.goalToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }
Goal translate | ( | Context | ctx | ) | throws Z3Exception [inline] |
Translates (copies) the Goal to the target Context ctx .
Z3Exception |
Definition at line 170 of file Goal.java.
{ return new Goal(ctx, Native.goalTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx())); }