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

Member Function Documentation

◆ getNumSubgoals()

int getNumSubgoals ( )
inline

The number of Subgoals.

Definition at line 28 of file ApplyResult.java.

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

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

◆ getSubgoals()

Goal [] getSubgoals ( )
inline

Retrieves the subgoals from the ApplyResult.

Exceptions
Z3Exception

Definition at line 39 of file ApplyResult.java.

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  }

Referenced by Goal.simplify().

◆ toString()

String toString ( )
inline

A string representation of the ApplyResult.

Definition at line 53 of file ApplyResult.java.

53  {
54  return Native.applyResultToString(getContext().nCtx(), getNativeObject());
55  }