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();
        }
    }