Package com.microsoft.z3

Class ApplyResult

java.lang.Object

com.microsoft.z3.Z3Object

com.microsoft.z3.ApplyResult

public class ApplyResult
extends Z3Object

ApplyResult objects represent the result of an application of a tactic to a goal. It contains the subgoals that were produced.

Method Summary

Modifier and Type	Method	Description
int	getNumSubgoals()	The number of Subgoals.
Goal[]	getSubgoals()	Retrieves the subgoals from the ApplyResult.
String	toString()	A string representation of the ApplyResult.

Methods inherited from class com.microsoft.z3.Z3Object

arrayLength, arrayToNative

Methods inherited from class java.lang.Object

clone, equals, finalize, getClass, hashCode, notify, notifyAll, wait, wait, wait

Method Details

getNumSubgoals

public int getNumSubgoals()

The number of Subgoals.

getSubgoals

public Goal[] getSubgoals()

Retrieves the subgoals from the ApplyResult.

Throws:

Z3Exception

toString

public String toString()

A string representation of the ApplyResult.

Overrides:

toString in class Object