Z3
src/api/java/Goal.java
Go to the documentation of this file.
00001 
00018 package com.microsoft.z3;
00019 
00020 import com.microsoft.z3.enumerations.Z3_goal_prec;
00021 
00026 public class Goal extends Z3Object
00027 {
00035     public Z3_goal_prec getPrecision() throws Z3Exception
00036     {
00037         return Z3_goal_prec.fromInt(Native.goalPrecision(getContext().nCtx(),
00038                 getNativeObject()));
00039     }
00040 
00044     public boolean isPrecise() throws Z3Exception
00045     {
00046         return getPrecision() == Z3_goal_prec.Z3_GOAL_PRECISE;
00047     }
00048 
00052     public boolean isUnderApproximation() throws Z3Exception
00053     {
00054         return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER;
00055     }
00056 
00060     public boolean isOverApproximation() throws Z3Exception
00061     {
00062         return getPrecision() == Z3_goal_prec.Z3_GOAL_OVER;
00063     }
00064 
00069     public boolean isGarbage() throws Z3Exception
00070     {
00071         return getPrecision() == Z3_goal_prec.Z3_GOAL_UNDER_OVER;
00072     }
00073 
00079     public void add(BoolExpr ... constraints) throws Z3Exception
00080     {
00081         getContext().checkContextMatch(constraints);
00082         for (BoolExpr c : constraints)
00083         {
00084             Native.goalAssert(getContext().nCtx(), getNativeObject(),
00085                     c.getNativeObject());
00086         }
00087     }
00088 
00092     public boolean inconsistent() throws Z3Exception
00093     {
00094         return Native.goalInconsistent(getContext().nCtx(), getNativeObject());
00095     }
00096 
00101     public int getDepth() throws Z3Exception
00102     {
00103         return Native.goalDepth(getContext().nCtx(), getNativeObject());
00104     }
00105 
00109     public void reset() throws Z3Exception
00110     {
00111         Native.goalReset(getContext().nCtx(), getNativeObject());
00112     }
00113 
00117     public int size() throws Z3Exception
00118     {
00119         return Native.goalSize(getContext().nCtx(), getNativeObject());
00120     }
00121 
00127     public BoolExpr[] getFormulas() throws Z3Exception
00128     {
00129         int n = size();
00130         BoolExpr[] res = new BoolExpr[n];
00131         for (int i = 0; i < n; i++)
00132             res[i] = new BoolExpr(getContext(), Native.goalFormula(getContext()
00133                     .nCtx(), getNativeObject(), i));
00134         return res;
00135     }
00136 
00140     public int getNumExprs() throws Z3Exception
00141     {
00142         return Native.goalNumExprs(getContext().nCtx(), getNativeObject());
00143     }
00144 
00149     public boolean isDecidedSat() throws Z3Exception
00150     {
00151         return Native.goalIsDecidedSat(getContext().nCtx(), getNativeObject());
00152     }
00153 
00158     public boolean isDecidedUnsat() throws Z3Exception
00159     {
00160         return Native
00161                 .goalIsDecidedUnsat(getContext().nCtx(), getNativeObject());
00162     }
00163 
00170     public Goal translate(Context ctx) throws Z3Exception
00171     {
00172         return new Goal(ctx, Native.goalTranslate(getContext().nCtx(),
00173                 getNativeObject(), ctx.nCtx()));
00174     }
00175 
00180     public Goal simplify() throws Z3Exception
00181     {
00182         Tactic t = getContext().mkTactic("simplify");
00183         ApplyResult res = t.apply(this);
00184 
00185         if (res.getNumSubgoals() == 0)
00186             throw new Z3Exception("No subgoals");
00187         else
00188             return res.getSubgoals()[0];
00189     }
00190     
00195     public Goal simplify(Params p) throws Z3Exception
00196     {
00197         Tactic t = getContext().mkTactic("simplify");
00198         ApplyResult res = t.apply(this, p);
00199 
00200         if (res.getNumSubgoals() == 0)
00201             throw new Z3Exception("No subgoals");
00202         else
00203             return res.getSubgoals()[0];
00204     }
00205 
00211     public String toString()
00212     {
00213         try
00214         {
00215             return Native.goalToString(getContext().nCtx(), getNativeObject());
00216         } catch (Z3Exception e)
00217         {
00218             return "Z3Exception: " + e.getMessage();
00219         }
00220     }
00221 
00222     Goal(Context ctx, long obj) throws Z3Exception
00223     {
00224         super(ctx, obj);
00225     }
00226 
00227     Goal(Context ctx, boolean models, boolean unsatCores, boolean proofs)
00228             throws Z3Exception
00229     {
00230         super(ctx, Native.mkGoal(ctx.nCtx(), (models) ? true : false,
00231                 (unsatCores) ? true : false, (proofs) ? true : false));
00232     }
00233 
00234     void incRef(long o) throws Z3Exception
00235     {
00236         getContext().goal_DRQ().incAndClear(getContext(), o);
00237         super.incRef(o);
00238     }
00239 
00240     void decRef(long o) throws Z3Exception
00241     {
00242         getContext().goal_DRQ().add(o);
00243         super.decRef(o);
00244     }
00245 
00246 }
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Defines