Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 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 
211  #region Internal
212  internal Goal(Context ctx, IntPtr obj) : base(ctx, obj) { Contract.Requires(ctx != null); }
213 
214  internal Goal(Context ctx, bool models, bool unsatCores, bool proofs)
215  : base(ctx, Native.Z3_mk_goal(ctx.nCtx, (models) ? 1 : 0, (unsatCores) ? 1 : 0, (proofs) ? 1 : 0))
216  {
217  Contract.Requires(ctx != null);
218  }
219 
220  internal class DecRefQueue : IDecRefQueue
221  {
222  public override void IncRef(Context ctx, IntPtr obj)
223  {
224  Native.Z3_goal_inc_ref(ctx.nCtx, obj);
225  }
226 
227  public override void DecRef(Context ctx, IntPtr obj)
228  {
229  Native.Z3_goal_dec_ref(ctx.nCtx, obj);
230  }
231  };
232 
233  internal override void IncRef(IntPtr o)
234  {
235  Context.Goal_DRQ.IncAndClear(Context, o);
236  base.IncRef(o);
237  }
238 
239  internal override void DecRef(IntPtr o)
240  {
241  Context.Goal_DRQ.Add(o);
242  base.DecRef(o);
243  }
244 
245  #endregion
246  }
247 }
static uint Z3_goal_num_exprs(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4461
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:2957
static uint Z3_goal_depth(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4430
static int Z3_goal_inconsistent(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4422
Goal[] Subgoals
Retrieves the subgoals from the ApplyResult.
Definition: ApplyResult.cs:44
override string ToString()
Goal to string conversion.
Definition: Goal.cs:206
static uint Z3_goal_precision(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4407
static Z3_ast Z3_goal_formula(Z3_context a0, Z3_goal a1, uint a2)
Definition: Native.cs:4453
Tactics are the basic building block for creating custom solvers for specific problem domains...
Definition: Tactic.cs:32
Z3_goal_prec
Z3_goal_prec
void Assert(params BoolExpr[] constraints)
Adds the constraints to the given goal.
Definition: Goal.cs:80
static string Z3_goal_to_string(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4493
static int Z3_goal_is_decided_unsat(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4477
static Z3_goal Z3_goal_translate(Z3_context a0, Z3_goal a1, Z3_context a2)
Definition: Native.cs:4485
ApplyResult Apply(Goal g, Params p=null)
Execute the tactic over the goal.
Definition: Tactic.cs:60
static uint Z3_goal_size(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4445
ApplyResult objects represent the result of an application of a tactic to a goal. It contains the sub...
Definition: ApplyResult.cs:30
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
static void Z3_goal_assert(Z3_context a0, Z3_goal a1, Z3_ast a2)
Definition: Native.cs:4415
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
static int Z3_goal_is_decided_sat(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4469
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
static void Z3_goal_reset(Z3_context a0, Z3_goal a1)
Definition: Native.cs:4438
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:31
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
Z3_goal Z3_API Z3_mk_goal(__in Z3_context c, __in Z3_bool models, __in Z3_bool unsat_cores, __in Z3_bool proofs)
Create a goal (aka problem). A goal is essentially a set of formulas, that can be solved and/or trans...
Goal Translate(Context ctx)
Translates (copies) the Goal to the target Context ctx .
Definition: Goal.cs:180