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.

    {
        return Native.applyResultGetNumSubgoals(getContext().nCtx(),
                getNativeObject());
    }

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.

    {
        int n = getNumSubgoals();
        Goal[] res = new Goal[n];
        for (int i = 0; i < n; i++)
            res[i] = new Goal(getContext(), 
                Native.applyResultGetSubgoal(getContext().nCtx(), getNativeObject(), i));
        return res;
    }

Referenced by Goal.simplify().

toString()

String toString ( )

inline

A string representation of the ApplyResult.

Definition at line 53 of file ApplyResult.java.

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