Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Groups Pages
Solver.cs
Go to the documentation of this file.
1 /*++
2 Copyright (c) 2012 Microsoft Corporation
3 
4 Module Name:
5 
6  Solver.cs
7 
8 Abstract:
9 
10  Z3 Managed API: Solvers
11 
12 Author:
13 
14  Christoph Wintersteiger (cwinter) 2012-03-22
15 
16 Notes:
17 
18 --*/
19 
20 using System;
21 using System.Diagnostics.Contracts;
22 
23 namespace Microsoft.Z3
24 {
28  [ContractVerification(true)]
29  public class Solver : Z3Object
30  {
34  public string Help
35  {
36  get
37  {
38  Contract.Ensures(Contract.Result<string>() != null);
39 
40  return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
41  }
42  }
43 
47  public Params Parameters
48  {
49  set
50  {
51  Contract.Requires(value != null);
52 
53  Context.CheckContextMatch(value);
54  Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
55  }
56  }
57 
61  public ParamDescrs ParameterDescriptions
62  {
63  get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
64  }
65 
66 
72  public uint NumScopes
73  {
74  get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
75  }
76 
81  public void Push()
82  {
83  Native.Z3_solver_push(Context.nCtx, NativeObject);
84  }
85 
91  public void Pop(uint n = 1)
92  {
93  Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
94  }
95 
100  public void Reset()
101  {
102  Native.Z3_solver_reset(Context.nCtx, NativeObject);
103  }
104 
108  public void Assert(params BoolExpr[] constraints)
109  {
110  Contract.Requires(constraints != null);
111  Contract.Requires(Contract.ForAll(constraints, c => c != null));
112 
113  Context.CheckContextMatch(constraints);
114  foreach (BoolExpr a in constraints)
115  {
116  Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
117  }
118  }
119 
123  public uint NumAssertions
124  {
125  get
126  {
127  ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
128  return ass.Size;
129  }
130  }
131 
135  public BoolExpr[] Assertions
136  {
137  get
138  {
139  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
140 
141  ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
142  uint n = ass.Size;
143  BoolExpr[] res = new BoolExpr[n];
144  for (uint i = 0; i < n; i++)
145  res[i] = new BoolExpr(Context, ass[i].NativeObject);
146  return res;
147  }
148  }
149 
158  public Status Check(params Expr[] assumptions)
159  {
160  Z3_lbool r;
161  if (assumptions == null)
162  r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
163  else
164  r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
165  switch (r)
166  {
167  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
168  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
169  default: return Status.UNKNOWN;
170  }
171  }
172 
180  public Model Model
181  {
182  get
183  {
184  IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
185  if (x == IntPtr.Zero)
186  return null;
187  else
188  return new Model(Context, x);
189  }
190  }
191 
199  public Expr Proof
200  {
201  get
202  {
203  IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
204  if (x == IntPtr.Zero)
205  return null;
206  else
207  return Expr.Create(Context, x);
208  }
209  }
210 
219  public Expr[] UnsatCore
220  {
221  get
222  {
223  Contract.Ensures(Contract.Result<Expr[]>() != null);
224 
225  ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
226  uint n = core.Size;
227  Expr[] res = new Expr[n];
228  for (uint i = 0; i < n; i++)
229  res[i] = Expr.Create(Context, core[i].NativeObject);
230  return res;
231  }
232  }
233 
237  public string ReasonUnknown
238  {
239  get
240  {
241  Contract.Ensures(Contract.Result<string>() != null);
242 
243  return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
244  }
245  }
246 
250  public Statistics Statistics
251  {
252  get
253  {
254  Contract.Ensures(Contract.Result<Statistics>() != null);
255 
256  return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
257  }
258  }
259 
263  public override string ToString()
264  {
265  return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
266  }
267 
268  #region Internal
269  internal Solver(Context ctx, IntPtr obj)
270  : base(ctx, obj)
271  {
272  Contract.Requires(ctx != null);
273  }
274 
275  internal class DecRefQueue : Z3.DecRefQueue
276  {
277  public override void IncRef(Context ctx, IntPtr obj)
278  {
279  Native.Z3_solver_inc_ref(ctx.nCtx, obj);
280  }
281 
282  public override void DecRef(Context ctx, IntPtr obj)
283  {
284  Native.Z3_solver_dec_ref(ctx.nCtx, obj);
285  }
286  };
287 
288  internal override void IncRef(IntPtr o)
289  {
290  Context.Solver_DRQ.IncAndClear(Context, o);
291  base.IncRef(o);
292  }
293 
294  internal override void DecRef(IntPtr o)
295  {
296  Context.Solver_DRQ.Add(o);
297  base.DecRef(o);
298  }
299  #endregion
300  }
301 }