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 }
com.microsoft.z3.ApplyResult.getNumSubgoals
int getNumSubgoals()
Definition: ApplyResult.java:28

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 }