Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines
Public Member Functions | Package Functions
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 ()

Package Functions

 ApplyResult (Context ctx, long obj) throws Z3Exception
void incRef (long o) throws Z3Exception
void decRef (long o) 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.


Constructor & Destructor Documentation

ApplyResult ( Context  ctx,
long  obj 
) throws Z3Exception [inline, package]

Definition at line 77 of file ApplyResult.java.

    {
        super(ctx, obj);
    }

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()));
    }
void decRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 88 of file ApplyResult.java.

    {
        getContext().applyResult_DRQ().add(o);
        super.decRef(o);
    }
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;
    }
void incRef ( long  o) throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 82 of file ApplyResult.java.

    {
        getContext().applyResult_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }
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();
        }
    }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines