Go to the documentation of this file.00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014
00015
00016
00017
00018
00019
00020 using System;
00021 using System.Diagnostics.Contracts;
00022
00023 namespace Microsoft.Z3
00024 {
00030 [ContractVerification(true)]
00031 public class Goal : Z3Object
00032 {
00041 public Z3_goal_prec Precision
00042 {
00043 get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
00044 }
00045
00049 public bool IsPrecise
00050 {
00051 get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
00052 }
00056 public bool IsUnderApproximation
00057 {
00058 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
00059 }
00060
00064 public bool IsOverApproximation
00065 {
00066 get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
00067 }
00068
00072 public bool IsGarbage
00073 {
00074 get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
00075 }
00076
00080 public void Assert(params BoolExpr[] constraints)
00081 {
00082 Contract.Requires(constraints != null);
00083 Contract.Requires(Contract.ForAll(constraints, c => c != null));
00084
00085 Context.CheckContextMatch(constraints);
00086 foreach (BoolExpr c in constraints)
00087 {
00088 Contract.Assert(c != null);
00089 Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
00090 }
00091 }
00092
00096 public void Add(params BoolExpr[] constraints)
00097 {
00098 Assert(constraints);
00099 }
00100
00104 public bool Inconsistent
00105 {
00106 get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
00107 }
00108
00115 public uint Depth
00116 {
00117 get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
00118 }
00119
00123 public void Reset()
00124 {
00125 Native.Z3_goal_reset(Context.nCtx, NativeObject);
00126 }
00127
00131 public uint Size
00132 {
00133 get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
00134 }
00135
00139 public BoolExpr[] Formulas
00140 {
00141 get
00142 {
00143 Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
00144
00145 uint n = Size;
00146 BoolExpr[] res = new BoolExpr[n];
00147 for (uint i = 0; i < n; i++)
00148 res[i] = new BoolExpr(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
00149 return res;
00150 }
00151 }
00152
00156 public uint NumExprs
00157 {
00158 get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
00159 }
00160
00164 public bool IsDecidedSat
00165 {
00166 get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
00167 }
00168
00172 public bool IsDecidedUnsat
00173 {
00174 get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
00175 }
00176
00180 public Goal Translate(Context ctx)
00181 {
00182 Contract.Requires(ctx != null);
00183
00184 return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
00185 }
00186
00191 public Goal Simplify(Params p = null)
00192 {
00193 Tactic t = Context.MkTactic("simplify");
00194 ApplyResult res = t.Apply(this, p);
00195
00196 if (res.NumSubgoals == 0)
00197 throw new Z3Exception("No subgoals");
00198 else
00199 return res.Subgoals[0];
00200 }
00201
00206 public override string ToString()
00207 {
00208 return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
00209 }
00210
00211 #region Internal
00212 internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
00213
00214 internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
00215 : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
00216 {
00217 Contract.Requires(ctx != null);
00218 }
00219
00220 internal class DecRefQueue : IDecRefQueue
00221 {
00222 public override void IncRef(Context ctx, IntPtr obj)
00223 {
00224 Native.Z3_goal_inc_ref(ctx.nCtx, obj);
00225 }
00226
00227 public override void DecRef(Context ctx, IntPtr obj)
00228 {
00229 Native.Z3_goal_dec_ref(ctx.nCtx, obj);
00230 }
00231 };
00232
00233 internal override void IncRef(IntPtr o)
00234 {
00235 Context.Goal_DRQ.IncAndClear(Context, o);
00236 base.IncRef(o);
00237 }
00238
00239 internal override void DecRef(IntPtr o)
00240 {
00241 Context.Goal_DRQ.Add(o);
00242 base.DecRef(o);
00243 }
00244
00245 #endregion
00246 }
00247 }