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.Collections.Generic;
23 
24 namespace Microsoft.Z3
25 {
29  [ContractVerification(true)]
30  public class Solver : Z3Object
31  {
35  public string Help
36  {
37  get
38  {
39  Contract.Ensures(Contract.Result<string>() != null);
40 
41  return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
42  }
43  }
44 
48  public Params Parameters
49  {
50  set
51  {
52  Contract.Requires(value != null);
53 
54  Context.CheckContextMatch(value);
55  Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
56  }
57  }
58 
62  public ParamDescrs ParameterDescriptions
63  {
64  get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
65  }
66 
67 
73  public uint NumScopes
74  {
75  get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
76  }
77 
82  public void Push()
83  {
84  Native.Z3_solver_push(Context.nCtx, NativeObject);
85  }
86 
92  public void Pop(uint n = 1)
93  {
94  Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
95  }
96 
101  public void Reset()
102  {
103  Native.Z3_solver_reset(Context.nCtx, NativeObject);
104  }
105 
109  public void Assert(params BoolExpr[] constraints)
110  {
111  Contract.Requires(constraints != null);
112  Contract.Requires(Contract.ForAll(constraints, c => c != null));
113 
114  Context.CheckContextMatch<BoolExpr>(constraints);
115  foreach (BoolExpr a in constraints)
116  {
117  Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
118  }
119  }
120 
124  public void Add(params BoolExpr[] constraints)
125  {
126  Assert(constraints);
127  }
128 
140  public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
141  {
142  Contract.Requires(constraints != null);
143  Contract.Requires(Contract.ForAll(constraints, c => c != null));
144  Contract.Requires(Contract.ForAll(ps, c => c != null));
145  Context.CheckContextMatch<BoolExpr>(constraints);
146  Context.CheckContextMatch<BoolExpr>(ps);
147  if (constraints.Length != ps.Length)
148  throw new Z3Exception("Argument size mismatch");
149 
150  for (int i = 0 ; i < constraints.Length; i++)
151  Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
152  }
153 
165  public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
166  {
167  Contract.Requires(constraint != null);
168  Contract.Requires(p != null);
169  Context.CheckContextMatch(constraint);
170  Context.CheckContextMatch(p);
171 
172  Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
173  }
174 
178  public uint NumAssertions
179  {
180  get
181  {
182  ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
183  return assertions.Size;
184  }
185  }
186 
190  public BoolExpr[] Assertions
191  {
192  get
193  {
194  Contract.Ensures(Contract.Result<BoolExpr[]>() != null);
195 
196  ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
197  return assertions.ToBoolExprArray();
198  }
199  }
200 
209  public Status Check(params Expr[] assumptions)
210  {
211  Z3_lbool r;
212  if (assumptions == null || assumptions.Length == 0)
213  r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
214  else
215  r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
216  return lboolToStatus(r);
217  }
218 
234  public Status Consequences(IEnumerable<BoolExpr> assumptions, IEnumerable<Expr> variables, out BoolExpr[] consequences)
235  {
236  ASTVector result = new ASTVector(Context);
237  ASTVector asms = new ASTVector(Context);
238  ASTVector vars = new ASTVector(Context);
239  foreach (var asm in assumptions) asms.Push(asm);
240  foreach (var v in variables) vars.Push(v);
241  Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
242  consequences = result.ToBoolExprArray();
243  return lboolToStatus(r);
244  }
245 
253  public Model Model
254  {
255  get
256  {
257  IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
258  if (x == IntPtr.Zero)
259  return null;
260  else
261  return new Model(Context, x);
262  }
263  }
264 
272  public Expr Proof
273  {
274  get
275  {
276  IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
277  if (x == IntPtr.Zero)
278  return null;
279  else
280  return Expr.Create(Context, x);
281  }
282  }
283 
292  public BoolExpr[] UnsatCore
293  {
294  get
295  {
296  Contract.Ensures(Contract.Result<Expr[]>() != null);
297 
298  ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
299  return core.ToBoolExprArray();
300  }
301  }
302 
306  public string ReasonUnknown
307  {
308  get
309  {
310  Contract.Ensures(Contract.Result<string>() != null);
311 
312  return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
313  }
314  }
315 
319  public Solver Translate(Context ctx)
320  {
321  Contract.Requires(ctx != null);
322  Contract.Ensures(Contract.Result<Solver>() != null);
323  return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
324  }
325 
326 
330  public Statistics Statistics
331  {
332  get
333  {
334  Contract.Ensures(Contract.Result<Statistics>() != null);
335 
336  return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
337  }
338  }
339 
343  public override string ToString()
344  {
345  return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
346  }
347 
348  #region Internal
349  internal Solver(Context ctx, IntPtr obj)
350  : base(ctx, obj)
351  {
352  Contract.Requires(ctx != null);
353  }
354 
355  internal class DecRefQueue : IDecRefQueue
356  {
357  public DecRefQueue() : base() { }
358  public DecRefQueue(uint move_limit) : base(move_limit) { }
359  internal override void IncRef(Context ctx, IntPtr obj)
360  {
361  Native.Z3_solver_inc_ref(ctx.nCtx, obj);
362  }
363 
364  internal override void DecRef(Context ctx, IntPtr obj)
365  {
366  Native.Z3_solver_dec_ref(ctx.nCtx, obj);
367  }
368  };
369 
370  internal override void IncRef(IntPtr o)
371  {
372  Context.Solver_DRQ.IncAndClear(Context, o);
373  base.IncRef(o);
374  }
375 
376  internal override void DecRef(IntPtr o)
377  {
378  Context.Solver_DRQ.Add(o);
379  base.DecRef(o);
380  }
381 
382  private Status lboolToStatus(Z3_lbool r)
383  {
384  switch (r)
385  {
386  case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
387  case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
388  default: return Status.UNKNOWN;
389  }
390  }
391 
392  #endregion
393  }
394 }
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:165
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:140
Boolean expressions
Definition: BoolExpr.cs:31
Status Consequences(IEnumerable< BoolExpr > assumptions, IEnumerable< Expr > variables, out BoolExpr[] consequences)
Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is a...
Definition: Solver.cs:234
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
Definition: Solver.cs:209
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Solver.cs:124
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:29
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:109
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4938
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:105
void Push()
Creates a backtracking point.
Definition: Solver.cs:82
override string ToString()
A string representation of the solver.
Definition: Solver.cs:343
void Reset()
Resets the Solver.
Definition: Solver.cs:101
Status
Status values.
Definition: Status.cs:27
Solver Translate(Context ctx)
Create a clone of the current solver with respect to ctx.
Definition: Solver.cs:319
BoolExpr [] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:129
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
DecRefQueue interface
Definition: IDecRefQueue.cs:32
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:29
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
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
void Pop(uint n=1)
Backtracks n backtracking points.
Definition: Solver.cs:92
Solvers.
Definition: Solver.cs:30