Z3
Public Member Functions
ApplyResult Class Reference
+ Inheritance diagram for ApplyResult:

Public Member Functions

int getNumSubgoals () throws Z3Exception
 
Goal[] getSubgoals () throws Z3Exception
 
Model convertModel (int i, Model m) throws Z3Exception
 
String toString ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

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.

Member Function Documentation

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.

Returns
A model for g
Exceptions
Z3Exception

Definition at line 57 of file ApplyResult.java.

58  {
59  return new Model(getContext(),
60  Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
61  }
int getNumSubgoals ( ) throws Z3Exception
inline

The number of Subgoals.

Definition at line 29 of file ApplyResult.java.

Referenced by ApplyResult.getSubgoals(), and Goal.simplify().

30  {
31  return Native.applyResultGetNumSubgoals(getContext().nCtx(),
32  getNativeObject());
33  }
Goal [] getSubgoals ( ) throws Z3Exception
inline

Retrieves the subgoals from the ApplyResult.

Exceptions
Z3Exception

Definition at line 40 of file ApplyResult.java.

Referenced by Goal.simplify().

41  {
42  int n = getNumSubgoals();
43  Goal[] res = new Goal[n];
44  for (int i = 0; i < n; i++)
45  res[i] = new Goal(getContext(),
46  Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
47  return res;
48  }
String toString ( )
inline

A string representation of the ApplyResult.

Definition at line 66 of file ApplyResult.java.

67  {
68  try
69  {
70  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
71  } catch (Z3Exception e)
72  {
73  return "Z3Exception: " + e.getMessage();
74  }
75  }