Goal Class Reference

Inheritance diagram for Goal:

Public Member Functions
Z3_goal_prec	getPrecision ()
boolean	isPrecise ()
boolean	isUnderApproximation ()
boolean	isOverApproximation ()
boolean	isGarbage ()
void	add (BoolExpr ... constraints)
boolean	inconsistent ()
int	getDepth ()
void	reset ()
int	size ()
BoolExpr []	getFormulas ()
int	getNumExprs ()
boolean	isDecidedSat ()
boolean	isDecidedUnsat ()
Goal	translate (Context ctx)
Goal	simplify ()
Goal	simplify (Params p)
String	toString ()
BoolExpr	AsBoolExpr ()

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

add()

void add ( BoolExpr ...  constraints )

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

Referenced by Solver.__iadd__(), Fixedpoint.__iadd__(), and Optimize.__iadd__().

AsBoolExpr()

BoolExpr AsBoolExpr ( )

inline

Goal to BoolExpr conversion.

Returns a string representation of the Goal.

Definition at line 222 of file Goal.java.

                                 {
        int n = size();
        if (n == 0) {
            return getContext().mkTrue();
        } else if (n == 1) {
            return getFormulas()[0];
        } else {
            return getContext().mkAnd(getFormulas());
        }
    }

getDepth()

int getDepth ( )

inline

The depth of the goal. Remarks: This tracks how many transformations were applied to it.

Definition at line 102 of file Goal.java.

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

getFormulas()

BoolExpr [] getFormulas ( )

inline

The formulas in the goal.

Exceptions

Z3Exception

Definition at line 128 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;
    }

Referenced by Goal.AsBoolExpr().

getNumExprs()

int getNumExprs ( )

inline

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

Definition at line 141 of file Goal.java.

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

getPrecision()

Z3_goal_prec getPrecision ( )

inline

The precision of the goal. Remarks: 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.

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

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

inconsistent()

boolean inconsistent ( )

inline

Indicates whether the goal contains ‘false’.

Definition at line 92 of file Goal.java.

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

isDecidedSat()

boolean isDecidedSat ( )

inline

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

Definition at line 150 of file Goal.java.

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

isDecidedUnsat()

boolean isDecidedUnsat ( )

inline

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

Definition at line 159 of file Goal.java.

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

isGarbage()

boolean isGarbage ( )

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

isOverApproximation()

boolean isOverApproximation ( )

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

isPrecise()

boolean isPrecise ( )

inline

Indicates whether the goal is precise.

Definition at line 44 of file Goal.java.

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

isUnderApproximation()

boolean isUnderApproximation ( )

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

reset()

void reset ( )

inline

Erases all formulas from the given goal.

Definition at line 110 of file Goal.java.

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

simplify() [1/2]

Goal simplify ( )

inline

Simplifies the goal. Remarks: Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 181 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];
    }

simplify() [2/2]

Goal simplify ( Params  p )

inline

Simplifies the goal. Remarks: Essentially invokes the ‘simplify’ tactic on the goal.

Definition at line 197 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];
    }

size()

int size ( )

inline

The number of formulas in the goal.

Definition at line 118 of file Goal.java.

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

Referenced by ParamDescrsRef.__len__(), Goal.__len__(), BitVecNumRef.as_signed_long(), Goal.AsBoolExpr(), Goal.getFormulas(), and BitVecSortRef.subsort().

toString()

String toString ( )

inline

Goal to string conversion.

Returns

A string representation of the Goal.

Definition at line 213 of file Goal.java.

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

translate()

Goal translate ( Context  ctx )

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