ApplyResult Class Reference

Inheritance diagram for ApplyResult:

Public Member Functions
int	getNumSubgoals () throws Z3Exception
Goal[]	getSubgoals () throws Z3Exception
Model	convertModel (int i, Model m) throws Z3Exception
String	toString ()
Public Member Functions inherited from Z3Object
void	dispose () throws Z3Exception
Public Member Functions inherited from IDisposable
void	dispose () throws Z3Exception

Additional Inherited Members
Protected Member Functions inherited from Z3Object
void	finalize () throws Z3Exception

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

Model convertModel ( int  i, Model  m  ) throws Z3Exception

inline

Convert a model for the subgoal i into a model for the original goal g, that the ApplyResult was obtained from.

Returns

A model for g

Exceptions

Z3Exception

Definition at line 57 of file ApplyResult.java.

    {
        return new Model(getContext(), 
            Native.applyResultConvertModel(getContext().nCtx(), getNativeObject(), i, m.getNativeObject()));
    }

int getNumSubgoals ( ) throws Z3Exception

inline

The number of Subgoals.

Definition at line 29 of file ApplyResult.java.

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

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

Goal [] getSubgoals ( ) throws Z3Exception

inline

Retrieves the subgoals from the ApplyResult.

Exceptions

Z3Exception

Definition at line 40 of file ApplyResult.java.

Referenced by Goal.simplify().

    {
        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;
    }

String toString ( )

inline

A string representation of the ApplyResult.

Definition at line 66 of file ApplyResult.java.

    {
        try
        {
            return Native.applyResultToString(getContext().nCtx(), getNativeObject());
        } catch (Z3Exception e)
        {
            return "Z3Exception: " + e.getMessage();
        }
    }