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 }