Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Goal.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Goal.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Goal
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-21
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
30  [ContractVerification(true)]
31  public class Goal : Z3Object
32  {
41  public Z3_goal_prec Precision
42  {
43  get { return (Z3_goal_prec)Native.Z3_goal_precision(Context.nCtx, NativeObject); }
44  }
45 
49  public bool IsPrecise
50  {
51  get { return Precision == Z3_goal_prec.Z3_GOAL_PRECISE; }
52  }
56  public bool IsUnderApproximation
57  {
58  get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER; }
59  }
60 
64  public bool IsOverApproximation
65  {
66  get { return Precision == Z3_goal_prec.Z3_GOAL_OVER; }
67  }
68 
72  public bool IsGarbage
73  {
74  get { return Precision == Z3_goal_prec.Z3_GOAL_UNDER_OVER; }
75  }
76 
80  public void Assert(params BoolExpr[] constraints)
81  {
82  Contract.Requires(constraints != null);
83  Contract.Requires(Contract.ForAll(constraints, c => c != null));
84 
85  Context.CheckContextMatch(constraints);
86  foreach (BoolExpr c in constraints)
87  {
88  Contract.Assert(c != null); // It was an assume, now made an assert just to be sure we do not regress
89  Native.Z3_goal_assert(Context.nCtx, NativeObject, c.NativeObject);
90  }
91  }
92 
96  public bool Inconsistent
97  {
98  get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
99  }
100 
107  public uint Depth
108  {
109  get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
110  }
111 
115  public void Reset()
116  {
117  Native.Z3_goal_reset(Context.nCtx, NativeObject);
118  }
119 
123  public uint Size
124  {
125  get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
126  }
127 
131  public BoolExpr[] Formulas
132  {
133  get
134  {
135  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
136 
137  uint n = Size;
138  BoolExpr[] res = new BoolExpr[n];
139  for (uint i = 0; i < n; i++)
140  res[i] = new BoolExpr(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
141  return res;
142  }
143  }
144 
148  public uint NumExprs
149  {
150  get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
151  }
152 
156  public bool IsDecidedSat
157  {
158  get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
159  }
160 
164  public bool IsDecidedUnsat
165  {
166  get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
167  }
168 
172  public Goal Translate(Context ctx)
173  {
174  Contract.Requires(ctx != null);
175 
176  return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
177  }
178 
183  public Goal Simplify(Params p = null)
184  {
185  Tactic t = Context.MkTactic("simplify");
186  ApplyResult res = t.Apply(this, p);
187 
188  if (res.NumSubgoals == 0)
189  return Context.MkGoal();
190  else
191  return res.Subgoals[0];
192  }
193 
198  public override string ToString()
199  {
200  return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
201  }
202 
203  #region Internal
204  internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
205 
206  internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
207  : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
208  {
209  Contract.Requires(ctx != null);
210  }
211 
212  internal class DecRefQueue : Z3.DecRefQueue
213  {
214  public override void IncRef(Context ctx, IntPtr obj)
215  {
216  Native.Z3_goal_inc_ref(ctx.nCtx, obj);
217  }
218 
219  public override void DecRef(Context ctx, IntPtr obj)
220  {
221  Native.Z3_goal_dec_ref(ctx.nCtx, obj);
222  }
223  };
224 
225  internal override void IncRef(IntPtr o)
226  {
227  Context.Goal_DRQ.IncAndClear(Context, o);
228  base.IncRef(o);
229  }
230 
231  internal override void DecRef(IntPtr o)
232  {
233  Context.Goal_DRQ.Add(o);
234  base.DecRef(o);
235  }
236 
237  #endregion
238  }
239 }