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 ()
Package Functions
	Goal (Context ctx, long obj) throws Z3Exception
	Goal (Context ctx, boolean models, boolean unsatCores, boolean proofs) throws Z3Exception
void	incRef (long o) throws Z3Exception
void	decRef (long o) 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.

---

Constructor & Destructor Documentation

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

Definition at line 222 of file Goal.java.

Referenced by Goal.translate().

    {
        super(ctx, obj);
    }

Goal	(	Context	ctx,
		boolean	models,
		boolean	unsatCores,
		boolean	proofs
	)		throws Z3Exception [inline, package]

Definition at line 227 of file Goal.java.

    {
        super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
                (unsatCores) ? true : false, (proofs) ? true : false));
    }

---

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

void decRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 240 of file Goal.java.

    {
        getContext().goal_DRQ().add(o);
        super.decRef(o);
    }

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

void incRef

(

long

o

)

throws Z3Exception [inline, package]

Reimplemented from Z3Object.

Definition at line 234 of file Goal.java.

    {
        getContext().goal_DRQ().incAndClear(getContext(), o);
        super.incRef(o);
    }

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