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

Public Member Functions

int getNumSubgoals ()
 
Goal [] getSubgoals ()
 
Model convertModel (int i, Model m)
 
String toString ()
 

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

§ convertModel()

Model convertModel ( int  i,
Model  m 
)
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 56 of file ApplyResult.java.

57  {
58  return new Model(getContext(),
59  Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
60  }

§ getNumSubgoals()

int getNumSubgoals ( )
inline

The number of Subgoals.

Definition at line 28 of file ApplyResult.java.

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

29  {
30  return Native.applyResultGetNumSubgoals(getContext().nCtx(),
31  getNativeObject());
32  }

§ getSubgoals()

Goal [] getSubgoals ( )
inline

Retrieves the subgoals from the ApplyResult.

Exceptions
Z3Exception

Definition at line 39 of file ApplyResult.java.

Referenced by Goal.simplify().

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

§ toString()

String toString ( )
inline

A string representation of the ApplyResult.

Definition at line 66 of file ApplyResult.java.

66  {
67  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
68  }