Public Member Functions | |
int | getNumSubgoals () throws Z3Exception |
Goal[] | getSubgoals () throws Z3Exception |
Model | convertModel (int i, Model m) throws Z3Exception |
String | toString () |
Package Functions | |
ApplyResult (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.
Definition at line 24 of file ApplyResult.java.
ApplyResult | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 77 of file ApplyResult.java.
{ super(ctx, obj); }
Model convertModel | ( | int | i, |
Model | m | ||
) | throws Z3Exception [inline] |
Convert a model for the subgoal i into a model for the original goal g
, that the ApplyResult was obtained from.
g
Z3Exception |
Definition at line 57 of file ApplyResult.java.
{ return new Model(getContext(), Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject())); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 88 of file ApplyResult.java.
{ getContext().applyResult_DRQ().add(o); super.decRef(o); }
int getNumSubgoals | ( | ) | throws Z3Exception [inline] |
The number of Subgoals.
Definition at line 29 of file ApplyResult.java.
Referenced by ApplyResult.getSubgoals(), and Goal.simplify().
{ return Native.applyResultGetNumSubgoals(getContext().nCtx(), getNativeObject()); }
Goal [] getSubgoals | ( | ) | throws Z3Exception [inline] |
Retrieves the subgoals from the ApplyResult.
Z3Exception |
Definition at line 40 of file ApplyResult.java.
Referenced by Goal.simplify().
{ int n = getNumSubgoals(); Goal[] res = new Goal[n]; for (int i = 0; i < n; i++) res[i] = new Goal(getContext(), Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i)); return res; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 82 of file ApplyResult.java.
{ getContext().applyResult_DRQ().incAndClear(getContext(), o); super.incRef(o); }
String toString | ( | ) | [inline] |
A string representation of the ApplyResult.
Definition at line 66 of file ApplyResult.java.
{ try { return Native.applyResultToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }