Z3
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Properties Friends Macros Modules 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 void Add(params BoolExpr[] constraints)
124  {
125  Assert(constraints);
126  }
127 
139  public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
140  {
141  Contract.Requires(constraints != null);
142  Contract.Requires(Contract.ForAll(constraints, c => c != null));
143  Contract.Requires(Contract.ForAll(ps, c => c != null));
144  Context.CheckContextMatch(constraints);
145  Context.CheckContextMatch(ps);
146  if (constraints.Length != ps.Length)
147  throw new Z3Exception("Argument size mismatch");
148 
149  for (int i = 0 ; i < constraints.Length; i++)
150  Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
151  }
152 
164  public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
165  {
166  Contract.Requires(constraint != null);
167  Contract.Requires(p != null);
168  Context.CheckContextMatch(constraint);
169  Context.CheckContextMatch(p);
170 
171  Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
172  }
173 
177  public uint NumAssertions
178  {
179  get
180  {
181  ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
182  return ass.Size;
183  }
184  }
185 
189  public BoolExpr[] Assertions
190  {
191  get
192  {
193  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
194 
195  ASTVector ass = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
196  uint n = ass.Size;
197  BoolExpr[] res = new BoolExpr[n];
198  for (uint i = 0; i < n; i++)
199  res[i] = new BoolExpr(Context, ass[i].NativeObject);
200  return res;
201  }
202  }
203 
212  public Status Check(params Expr[] assumptions)
213  {
214  Z3_lbool r;
215  if (assumptions == null || assumptions.Length == 0)
216  r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
217  else
218  r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
219  switch (r)
220  {
221  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
222  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
223  default: return Status.UNKNOWN;
224  }
225  }
226 
234  public Model Model
235  {
236  get
237  {
238  IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
239  if (x == IntPtr.Zero)
240  return null;
241  else
242  return new Model(Context, x);
243  }
244  }
245 
253  public Expr Proof
254  {
255  get
256  {
257  IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
258  if (x == IntPtr.Zero)
259  return null;
260  else
261  return Expr.Create(Context, x);
262  }
263  }
264 
273  public Expr[] UnsatCore
274  {
275  get
276  {
277  Contract.Ensures(Contract.Result<Expr[]>() != null);
278 
279  ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
280  uint n = core.Size;
281  Expr[] res = new Expr[n];
282  for (uint i = 0; i < n; i++)
283  res[i] = Expr.Create(Context, core[i].NativeObject);
284  return res;
285  }
286  }
287 
291  public string ReasonUnknown
292  {
293  get
294  {
295  Contract.Ensures(Contract.Result<string>() != null);
296 
297  return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
298  }
299  }
300 
304  public Statistics Statistics
305  {
306  get
307  {
308  Contract.Ensures(Contract.Result<Statistics>() != null);
309 
310  return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
311  }
312  }
313 
317  public override string ToString()
318  {
319  return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
320  }
321 
322  #region Internal
323  internal Solver(Context ctx, IntPtr obj)
324  : base(ctx, obj)
325  {
326  Contract.Requires(ctx != null);
327  }
328 
329  internal class DecRefQueue : IDecRefQueue
330  {
331  public override void IncRef(Context ctx, IntPtr obj)
332  {
333  Native.Z3_solver_inc_ref(ctx.nCtx, obj);
334  }
335 
336  public override void DecRef(Context ctx, IntPtr obj)
337  {
338  Native.Z3_solver_dec_ref(ctx.nCtx, obj);
339  }
340  };
341 
342  internal override void IncRef(IntPtr o)
343  {
344  Context.Solver_DRQ.IncAndClear(Context, o);
345  base.IncRef(o);
346  }
347 
348  internal override void DecRef(IntPtr o)
349  {
350  Context.Solver_DRQ.Add(o);
351  base.DecRef(o);
352  }
353  #endregion
354  }
355 }
static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:4983
static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2)
Definition: Native.cs:4931
void AssertAndTrack(BoolExpr constraint, BoolExpr p)
Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p...
Definition: Solver.cs:164
void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean con...
Definition: Solver.cs:139
static Z3_ast_vector Z3_solver_get_assertions(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4967
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
Definition: Solver.cs:212
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Solver.cs:123
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
static Z3_stats Z3_solver_get_statistics(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5023
static string Z3_solver_to_string(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5031
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:108
static void Z3_solver_reset(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4938
static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4895
Expressions are terms.
Definition: Expr.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
void Push()
Creates a backtracking point.
Definition: Solver.cs:81
static void Z3_solver_assert_and_track(Z3_context a0, Z3_solver a1, Z3_ast a2, Z3_ast a3)
Definition: Native.cs:4960
override string ToString()
A string representation of the solver.
Definition: Solver.cs:317
void Reset()
Resets the Solver.
Definition: Solver.cs:100
Status
Status values.
Definition: Status.cs:27
static int Z3_solver_check(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4975
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4991
A ParameterSet represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
static string Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5015
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
static Z3_ast Z3_solver_get_proof(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4999
static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2)
Definition: Native.cs:4903
The main interaction with Z3 happens via the Context.
Definition: Context.cs:31
Z3_lbool
Z3_lbool
Definition: Enumerations.cs:10
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:27
The abstract syntax tree (AST) class.
Definition: AST.cs:31
static string Z3_solver_get_help(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4887
static void Z3_solver_push(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4924
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:31
static void Z3_solver_assert(Z3_context a0, Z3_solver a1, Z3_ast a2)
Definition: Native.cs:4953
void Pop(uint n=1)
Backtracks n backtracking points.
Definition: Solver.cs:91
Solvers.
Definition: Solver.cs:29
static Z3_ast_vector Z3_solver_get_unsat_core(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5007
static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1)
Definition: Native.cs:4945