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 }