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

Public Member Functions

int getNumSubgoals ()
 
Goal[] getSubgoals ()
 
String toString ()
 

Additional Inherited Members

- Static Public Member Functions inherited from Z3Object
static long[] arrayToNative (Z3Object[] a)
 
static int arrayLength (Z3Object[] a)
 

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 26 of file ApplyResult.java.

Member Function Documentation

◆ getNumSubgoals()

int getNumSubgoals ( )
inline

The number of Subgoals.

Definition at line 30 of file ApplyResult.java.

31  {
32  return Native.applyResultGetNumSubgoals(getContext().nCtx(),
33  getNativeObject());
34  }

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

◆ getSubgoals()

Goal [] getSubgoals ( )
inline

Retrieves the subgoals from the ApplyResult.

Exceptions
Z3Exception

Definition at line 41 of file ApplyResult.java.

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

Referenced by Goal.simplify().

◆ toString()

String toString ( )
inline

A string representation of the ApplyResult.

Definition at line 55 of file ApplyResult.java.

55  {
56  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
57  }