Z3
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 assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
182  return assertions.Size;
183  }
184  }
185 
189  public BoolExpr[] Assertions
190  {
191  get
192  {
193  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
194 
195  ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
196  return assertions.ToBoolExprArray();
197  }
198  }
199 
208  public Status Check(params Expr[] assumptions)
209  {
210  Z3_lbool r;
211  if (assumptions == null || assumptions.Length == 0)
212  r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
213  else
214  r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
215  switch (r)
216  {
217  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
218  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
219  default: return Status.UNKNOWN;
220  }
221  }
222 
230  public Model Model
231  {
232  get
233  {
234  IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
235  if (x == IntPtr.Zero)
236  return null;
237  else
238  return new Model(Context, x);
239  }
240  }
241 
249  public Expr Proof
250  {
251  get
252  {
253  IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
254  if (x == IntPtr.Zero)
255  return null;
256  else
257  return Expr.Create(Context, x);
258  }
259  }
260 
269  public BoolExpr[] UnsatCore
270  {
271  get
272  {
273  Contract.Ensures(Contract.Result<Expr[]>() != null);
274 
275  ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
276  return core.ToBoolExprArray();
277  }
278  }
279 
283  public string ReasonUnknown
284  {
285  get
286  {
287  Contract.Ensures(Contract.Result<string>() != null);
288 
289  return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
290  }
291  }
292 
296  public Statistics Statistics
297  {
298  get
299  {
300  Contract.Ensures(Contract.Result<Statistics>() != null);
301 
302  return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
303  }
304  }
305 
309  public override string ToString()
310  {
311  return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
312  }
313 
314  #region Internal
315  internal Solver(Context ctx, IntPtr obj)
316  : base(ctx, obj)
317  {
318  Contract.Requires(ctx != null);
319  }
320 
321  internal class DecRefQueue : IDecRefQueue
322  {
323  public DecRefQueue() : base() { }
324  public DecRefQueue(uint move_limit) : base(move_limit) { }
325  internal override void IncRef(Context ctx, IntPtr obj)
326  {
327  Native.Z3_solver_inc_ref(ctx.nCtx, obj);
328  }
329 
330  internal override void DecRef(Context ctx, IntPtr obj)
331  {
332  Native.Z3_solver_dec_ref(ctx.nCtx, obj);
333  }
334  };
335 
336  internal override void IncRef(IntPtr o)
337  {
338  Context.Solver_DRQ.IncAndClear(Context, o);
339  base.IncRef(o);
340  }
341 
342  internal override void DecRef(IntPtr o)
343  {
344  Context.Solver_DRQ.Add(o);
345  base.DecRef(o);
346  }
347  #endregion
348  }
349 }
static int Z3_solver_check_assumptions(Z3_context a0, Z3_solver a1, uint a2, [In] Z3_ast[] a3)
Definition: Native.cs:5437
static void Z3_solver_pop(Z3_context a0, Z3_solver a1, uint a2)
Definition: Native.cs:5385
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
using System
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:5421
Boolean expressions
Definition: BoolExpr.cs:31
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
Definition: Solver.cs:208
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:5477
static string Z3_solver_to_string(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5485
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:5392
static Z3_param_descrs Z3_solver_get_param_descrs(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5349
static void Z3_solver_inc_ref(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5364
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4519
Vectors of ASTs.
Definition: ASTVector.cs:28
Expressions are terms.
Definition: Expr.cs:29
uint Size
The size of the vector
Definition: ASTVector.cs:34
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:143
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:5414
override string ToString()
A string representation of the solver.
Definition: Solver.cs:309
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:5429
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
static Z3_model Z3_solver_get_model(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5445
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
static void Z3_solver_dec_ref(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5371
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
static string Z3_solver_get_reason_unknown(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5469
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:5453
static void Z3_solver_set_params(Z3_context a0, Z3_solver a1, Z3_params a2)
Definition: Native.cs:5357
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:5341
static void Z3_solver_push(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5378
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:5407
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:5461
static uint Z3_solver_get_num_scopes(Z3_context a0, Z3_solver a1)
Definition: Native.cs:5399