Goal Class Reference

Inheritance diagram for Goal:

Public Member Functions
Z3_goal_prec	getPrecision () throws Z3Exception
boolean	isPrecise () throws Z3Exception
boolean	isUnderApproximation () throws Z3Exception
boolean	isOverApproximation () throws Z3Exception
boolean	isGarbage () throws Z3Exception
void	add (BoolExpr...constraints) throws Z3Exception
boolean	inconsistent () throws Z3Exception
int	getDepth () throws Z3Exception
void	reset () throws Z3Exception
int	size () throws Z3Exception
BoolExpr[]	getFormulas () throws Z3Exception
int	getNumExprs () throws Z3Exception
boolean	isDecidedSat () throws Z3Exception
boolean	isDecidedUnsat () throws Z3Exception
Goal	translate (Context ctx) throws Z3Exception
Goal	simplify () throws Z3Exception
Goal	simplify (Params p) 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

A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed using tactics and solvers.

Definition at line 26 of file Goal.java.

Member Function Documentation

void add ( BoolExpr...  constraints ) throws Z3Exception

inline

Adds the constraints to the given goal.

Exceptions

Z3Exception

Definition at line 79 of file Goal.java.

    {
        getContext().checkContextMatch(constraints);
        for (BoolExpr c : constraints)
        {
            Native.goalAssert(getContext().nCtx(), getNativeObject(),
                    c.getNativeObject());
        }
    }

int getDepth ( ) throws Z3Exception

inline

The depth of the goal.

This tracks how many transformations were applied to it.

Definition at line 101 of file Goal.java.

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

BoolExpr [] getFormulas ( ) throws Z3Exception

inline

The formulas in the goal.

Exceptions

Z3Exception

Definition at line 127 of file Goal.java.

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

int getNumExprs ( ) throws Z3Exception

inline

The number of formulas, subformulas and terms in the goal.

Definition at line 140 of file Goal.java.

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

Z3_goal_prec getPrecision ( ) throws Z3Exception

inline

The precision of the goal.

Goals can be transformed using over and under approximations. An under approximation is applied when the objective is to find a model for a given goal. An over approximation is applied when the objective is to find a proof for a given goal.

Definition at line 35 of file Goal.java.

Referenced by Goal.isGarbage(), Goal.isOverApproximation(), Goal.isPrecise(), and Goal.isUnderApproximation().

    {
        return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
                getNativeObject()));
    }

boolean inconsistent ( ) throws Z3Exception

inline

Indicates whether the goal contains `false'.

Definition at line 92 of file Goal.java.

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

boolean isDecidedSat ( ) throws Z3Exception

inline

Indicates whether the goal is empty, and it is precise or the product of an under approximation.

Definition at line 149 of file Goal.java.

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

boolean isDecidedUnsat ( ) throws Z3Exception

inline

Indicates whether the goal contains `false', and it is precise or the product of an over approximation.

Definition at line 158 of file Goal.java.

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

boolean isGarbage ( ) throws Z3Exception

inline

Indicates whether the goal is garbage (i.e., the product of over- and under-approximations).

Definition at line 69 of file Goal.java.

    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
    }

boolean isOverApproximation ( ) throws Z3Exception

inline

Indicates whether the goal is an over-approximation.

Definition at line 60 of file Goal.java.

    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
    }

boolean isPrecise ( ) throws Z3Exception

inline

Indicates whether the goal is precise.

Definition at line 44 of file Goal.java.

    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
    }

boolean isUnderApproximation ( ) throws Z3Exception

inline

Indicates whether the goal is an under-approximation.

Definition at line 52 of file Goal.java.

    {
        return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
    }

void reset ( ) throws Z3Exception

inline

Erases all formulas from the given goal.

Definition at line 109 of file Goal.java.

    {
        Native.goalReset(getContext().nCtx(), getNativeObject());
    }

Goal simplify ( ) throws Z3Exception

inline

Simplifies the goal.

Essentially invokes the `simplify' tactic on the goal.

Definition at line 180 of file Goal.java.

    {
        Tactic t = getContext().mkTactic("simplify");
        ApplyResult res = t.apply(this);

        if (res.getNumSubgoals() == 0)
            throw new Z3Exception("No subgoals");
        else
            return res.getSubgoals()[0];
    }

Goal simplify ( Params  p ) throws Z3Exception

inline

Simplifies the goal.

Essentially invokes the `simplify' tactic on the goal.

Definition at line 195 of file Goal.java.

    {
        Tactic t = getContext().mkTactic("simplify");
        ApplyResult res = t.apply(this, p);

        if (res.getNumSubgoals() == 0)
            throw new Z3Exception("No subgoals");
        else
            return res.getSubgoals()[0];
    }

int size ( ) throws Z3Exception

inline

The number of formulas in the goal.

Definition at line 117 of file Goal.java.

Referenced by Goal.getFormulas().

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

String toString ( )

inline

Goal to string conversion.

Returns

A string representation of the Goal.

Definition at line 211 of file Goal.java.

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

Goal translate ( Context  ctx ) throws Z3Exception

inline

Translates (copies) the Goal to the target Context ctx .

Exceptions

Z3Exception

Definition at line 170 of file Goal.java.

    {
        return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
                getNativeObject(), ctx.nCtx()));
    }