Z3
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;
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<BoolExpr>(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 void Add(params BoolExpr[] constraints)
97  {
98  Assert(constraints);
99  }
100 
104  public bool Inconsistent
105  {
106  get { return Native.Z3_goal_inconsistent(Context.nCtx, NativeObject) != 0; }
107  }
108 
115  public uint Depth
116  {
117  get { return Native.Z3_goal_depth(Context.nCtx, NativeObject); }
118  }
119 
123  public void Reset()
124  {
125  Native.Z3_goal_reset(Context.nCtx, NativeObject);
126  }
127 
131  public uint Size
132  {
133  get { return Native.Z3_goal_size(Context.nCtx, NativeObject); }
134  }
135 
139  public BoolExpr[] Formulas
140  {
141  get
142  {
143  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
144 
145  uint n = Size;
146  BoolExpr[] res = new BoolExpr[n];
147  for (uint i = 0; i < n; i++)
148  res[i] = new BoolExpr(Context, Native.Z3_goal_formula(Context.nCtx, NativeObject, i));
149  return res;
150  }
151  }
152 
156  public uint NumExprs
157  {
158  get { return Native.Z3_goal_num_exprs(Context.nCtx, NativeObject); }
159  }
160 
164  public bool IsDecidedSat
165  {
166  get { return Native.Z3_goal_is_decided_sat(Context.nCtx, NativeObject) != 0; }
167  }
168 
172  public bool IsDecidedUnsat
173  {
174  get { return Native.Z3_goal_is_decided_unsat(Context.nCtx, NativeObject) != 0; }
175  }
176 
180  public Goal Translate(Context ctx)
181  {
182  Contract.Requires(ctx != null);
183 
184  return new Goal(ctx, Native.Z3_goal_translate(Context.nCtx, NativeObject, ctx.nCtx));
185  }
186 
191  public Goal Simplify(Params p = null)
192  {
193  Tactic t = Context.MkTactic("simplify");
194  ApplyResult res = t.Apply(this, p);
195 
196  if (res.NumSubgoals == 0)
197  throw new Z3Exception("No subgoals");
198  else
199  return res.Subgoals[0];
200  }
201 
206  public override string ToString()
207  {
208  return Native.Z3_goal_to_string(Context.nCtx, NativeObject);
209  }
210 
215  public BoolExpr AsBoolExpr() {
216  uint n = Size;
217  if (n == 0)
218  return Context.MkTrue();
219  else if (n == 1)
220  return Formulas[0];
221  else {
222  return Context.MkAnd(Formulas);
223  }
224  }
225 
226  #region Internal
227  internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
228 
229  internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
230  : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
231  {
232  Contract.Requires(ctx != null);
233  }
234 
235  internal class DecRefQueue : IDecRefQueue
236  {
237  public DecRefQueue() : base() { }
238  public DecRefQueue(uint move_limit) : base(move_limit) { }
239  internal override void IncRef(Context ctx, IntPtr obj)
240  {
241  Native.Z3_goal_inc_ref(ctx.nCtx, obj);
242  }
243 
244  internal override void DecRef(Context ctx, IntPtr obj)
245  {
246  Native.Z3_goal_dec_ref(ctx.nCtx, obj);
247  }
248  };
249 
250  internal override void IncRef(IntPtr o)
251  {
252  Context.Goal_DRQ.IncAndClear(Context, o);
253  base.IncRef(o);
254  }
255 
256  internal override void DecRef(IntPtr o)
257  {
258  Context.Goal_DRQ.Add(o);
259  base.DecRef(o);
260  }
261 
262  #endregion
263  }
264 }
BoolExpr MkAnd(params BoolExpr[] t)
Create an expression representing t[0] and t[1] and ....
Definition: Context.cs:967
void Reset()
Erases all formulas from the given goal.
Definition: Goal.cs:123
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Goal.cs:96
Tactic MkTactic(string name)
Creates a new Tactic.
Definition: Context.cs:3383
Goal [] Subgoals
Retrieves the subgoals from the ApplyResult.
Definition: ApplyResult.cs:44
BoolExpr AsBoolExpr()
Goal to BoolExpr conversion.
Definition: Goal.cs:215
IDecRefQueue Goal_DRQ
Goal DRQ
Definition: Context.cs:4913
Z3_goal_prec
A Goal is essentially a set of formulas. Z3 provide APIs for building strategies/tactics for solving ...
Definition: z3_api.h:1349
Boolean expressions
Definition: BoolExpr.cs:31
override string ToString()
Goal to string conversion.
Definition: Goal.cs:206
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80
BoolExpr MkTrue()
The true Term.
Definition: Context.cs:836
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:60
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:30
uint NumSubgoals
The number of Subgoals.
Definition: ApplyResult.cs:36
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Goal Simplify(Params p=null)
Simplifies the goal.
Definition: Goal.cs:191
A goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or transformed ...
Definition: Goal.cs:31
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .
Definition: Goal.cs:180