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