Z3
Solver.cs
Go to the documentation of this file.
1/*++
2Copyright (c) 2012 Microsoft Corporation
3
4Module Name:
5
6 Solver.cs
7
8Abstract:
9
10 Z3 Managed API: Solvers
11
12Author:
13
14 Christoph Wintersteiger (cwinter) 2012-03-22
15
16Notes:
17
18--*/
19
20using System;
21using System.Diagnostics;
22using System.Linq;
23using System.Collections.Generic;
24
25namespace Microsoft.Z3
26{
30 public class Solver : Z3Object
31 {
35 public string Help
36 {
37 get
38 {
39
40 return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
41 }
42 }
43
48 {
49 set
50 {
51 Debug.Assert(value != null);
52
53 Context.CheckContextMatch(value);
54 Native.Z3_solver_set_params(Context.nCtx, NativeObject, value.NativeObject);
55 }
56 }
57
61 public void Set(string name, bool value) { Parameters = Context.MkParams().Add(name, value); }
65 public void Set(string name, uint value) { Parameters = Context.MkParams().Add(name, value); }
69 public void Set(string name, double value) { Parameters = Context.MkParams().Add(name, value); }
73 public void Set(string name, string value) { Parameters = Context.MkParams().Add(name, value); }
77 public void Set(string name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
81 public void Set(Symbol name, bool value) { Parameters = Context.MkParams().Add(name, value); }
85 public void Set(Symbol name, uint value) { Parameters = Context.MkParams().Add(name, value); }
89 public void Set(Symbol name, double value) { Parameters = Context.MkParams().Add(name, value); }
93 public void Set(Symbol name, string value) { Parameters = Context.MkParams().Add(name, value); }
97 public void Set(Symbol name, Symbol value) { Parameters = Context.MkParams().Add(name, value); }
98
99
100
105 {
106 get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
107 }
108
109
115 public uint NumScopes
116 {
117 get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
118 }
119
124 public void Push()
125 {
126 Native.Z3_solver_push(Context.nCtx, NativeObject);
127 }
128
134 public void Pop(uint n = 1)
135 {
136 Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
137 }
138
143 public void Reset()
144 {
145 Native.Z3_solver_reset(Context.nCtx, NativeObject);
146 }
147
151 public void Assert(params BoolExpr[] constraints)
152 {
153 Debug.Assert(constraints != null);
154 Debug.Assert(constraints.All(c => c != null));
155
156 Context.CheckContextMatch<BoolExpr>(constraints);
157 foreach (BoolExpr a in constraints)
158 {
159 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
160 }
161 }
162
166 public void Add(params BoolExpr[] constraints)
167 {
168 Assert(constraints);
169 }
170
174 public void Add(IEnumerable<BoolExpr> constraints)
175 {
176 Assert(constraints.ToArray());
177 }
178
190 public void AssertAndTrack(BoolExpr[] constraints, BoolExpr[] ps)
191 {
192 Debug.Assert(constraints != null);
193 Debug.Assert(constraints.All(c => c != null));
194 Debug.Assert(ps.All(c => c != null));
195 Context.CheckContextMatch<BoolExpr>(constraints);
196 Context.CheckContextMatch<BoolExpr>(ps);
197 if (constraints.Length != ps.Length)
198 throw new Z3Exception("Argument size mismatch");
199
200 for (int i = 0 ; i < constraints.Length; i++)
201 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
202 }
203
215 public void AssertAndTrack(BoolExpr constraint, BoolExpr p)
216 {
217 Debug.Assert(constraint != null);
218 Debug.Assert(p != null);
219 Context.CheckContextMatch(constraint);
220 Context.CheckContextMatch(p);
221
222 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
223 }
224
228 public void FromFile(string file)
229 {
230 Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);
231 }
232
236 public void FromString(string str)
237 {
238 Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);
239 }
240
244 public uint NumAssertions
245 {
246 get
247 {
248 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
249 return assertions.Size;
250 }
251 }
252
257 {
258 get
259 {
260
261 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
262 return assertions.ToBoolExprArray();
263 }
264 }
265
270 {
271 get
272 {
273
274 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_units(Context.nCtx, NativeObject));
275 return assertions.ToBoolExprArray();
276 }
277 }
278
287 public Status Check(params Expr[] assumptions)
288 {
289 Z3_lbool r;
290 if (assumptions == null || assumptions.Length == 0)
291 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
292 else
293 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
294 return lboolToStatus(r);
295 }
296
305 public Status Check(IEnumerable<BoolExpr> assumptions)
306 {
307 Z3_lbool r;
308 BoolExpr[] asms = assumptions.ToArray();
309 if (asms.Length == 0)
310 r = (Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
311 else
312 r = (Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)asms.Length, AST.ArrayToNative(asms));
313 return lboolToStatus(r);
314 }
315
331 public Status Consequences(IEnumerable<BoolExpr> assumptions, IEnumerable<Expr> variables, out BoolExpr[] consequences)
332 {
333 ASTVector result = new ASTVector(Context);
334 ASTVector asms = new ASTVector(Context);
335 ASTVector vars = new ASTVector(Context);
336 foreach (var asm in assumptions) asms.Push(asm);
337 foreach (var v in variables) vars.Push(v);
338 Z3_lbool r = (Z3_lbool)Native.Z3_solver_get_consequences(Context.nCtx, NativeObject, asms.NativeObject, vars.NativeObject, result.NativeObject);
339 consequences = result.ToBoolExprArray();
340 return lboolToStatus(r);
341 }
342
351 {
352 get
353 {
354 IntPtr x = Native.Z3_solver_get_model(Context.nCtx, NativeObject);
355 if (x == IntPtr.Zero)
356 return null;
357 else
358 return new Model(Context, x);
359 }
360 }
361
369 public Expr Proof
370 {
371 get
372 {
373 IntPtr x = Native.Z3_solver_get_proof(Context.nCtx, NativeObject);
374 if (x == IntPtr.Zero)
375 return null;
376 else
377 return Expr.Create(Context, x);
378 }
379 }
380
390 {
391 get
392 {
393
394 ASTVector core = new ASTVector(Context, Native.Z3_solver_get_unsat_core(Context.nCtx, NativeObject));
395 return core.ToBoolExprArray();
396 }
397 }
398
402 public string ReasonUnknown
403 {
404 get
405 {
406
407 return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
408 }
409 }
410
414 public uint BacktrackLevel { get; set; }
415
419 public BoolExpr[] CubeVariables { get; set; }
420
421
425 public IEnumerable<BoolExpr[]> Cube()
426 {
427 ASTVector cv = new ASTVector(Context);
428 if (CubeVariables != null)
429 foreach (var b in CubeVariables) cv.Push(b);
430
431 while (true) {
432 var lvl = BacktrackLevel;
433 BacktrackLevel = uint.MaxValue;
434 ASTVector r = new ASTVector(Context, Native.Z3_solver_cube(Context.nCtx, NativeObject, cv.NativeObject, lvl));
435 var v = r.ToBoolExprArray();
436 CubeVariables = cv.ToBoolExprArray();
437 if (v.Length == 1 && v[0].IsFalse) {
438 break;
439 }
440 yield return v;
441 if (v.Length == 0) {
442 break;
443 }
444 }
445 }
446
451 {
452 Debug.Assert(ctx != null);
453 return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
454 }
455
459 public void ImportModelConverter(Solver src)
460 {
461 Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
462 }
463
468 {
469 get
470 {
471
472 return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
473 }
474 }
475
479 public override string ToString()
480 {
481 return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
482 }
483
484 #region Internal
485 internal Solver(Context ctx, IntPtr obj)
486 : base(ctx, obj)
487 {
488 Debug.Assert(ctx != null);
489 this.BacktrackLevel = uint.MaxValue;
490 }
491
492 internal class DecRefQueue : IDecRefQueue
493 {
494 public DecRefQueue() : base() { }
495 public DecRefQueue(uint move_limit) : base(move_limit) { }
496 internal override void IncRef(Context ctx, IntPtr obj)
497 {
498 Native.Z3_solver_inc_ref(ctx.nCtx, obj);
499 }
500
501 internal override void DecRef(Context ctx, IntPtr obj)
502 {
503 Native.Z3_solver_dec_ref(ctx.nCtx, obj);
504 }
505 };
506
507 internal override void IncRef(IntPtr o)
508 {
509 Context.Solver_DRQ.IncAndClear(Context, o);
510 base.IncRef(o);
511 }
512
513 internal override void DecRef(IntPtr o)
514 {
515 Context.Solver_DRQ.Add(o);
516 base.DecRef(o);
517 }
518
519 private Status lboolToStatus(Z3_lbool r)
520 {
521 switch (r)
522 {
523 case Z3_lbool.Z3_L_TRUE: return Status.SATISFIABLE;
524 case Z3_lbool.Z3_L_FALSE: return Status.UNSATISFIABLE;
525 default: return Status.UNKNOWN;
526 }
527 }
528
529 #endregion
530 }
531}
The abstract syntax tree (AST) class.
Definition: AST.cs:31
Vectors of ASTs.
Definition: ASTVector.cs:29
BoolExpr[] ToBoolExprArray()
Translates an ASTVector into a BoolExpr[]
Definition: ASTVector.cs:127
uint Size
The size of the vector
Definition: ASTVector.cs:34
Boolean expressions
Definition: BoolExpr.cs:32
The main interaction with Z3 happens via the Context.
Definition: Context.cs:32
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
IDecRefQueue Solver_DRQ
Solver DRQ
Definition: Context.cs:4780
Expressions are terms.
Definition: Expr.cs:31
A Model contains interpretations (assignments) of constants and functions.
Definition: Model.cs:30
A ParamDescrs describes a set of parameters.
Definition: ParamDescrs.cs:29
A Params objects represents a configuration in the form of Symbol/value pairs.
Definition: Params.cs:29
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33
void Set(string name, uint value)
Sets parameter on the solver
Definition: Solver.cs:65
BoolExpr[] Assertions
The set of asserted formulas.
Definition: Solver.cs:257
void Set(string name, double value)
Sets parameter on the solver
Definition: Solver.cs:69
Model Model
The model of the last Check(params Expr[] assumptions).
Definition: Solver.cs:351
string Help
A string that describes all available solver parameters.
Definition: Solver.cs:36
void Set(string name, string value)
Sets parameter on the solver
Definition: Solver.cs:73
void Pop(uint n=1)
Backtracks n backtracking points.
Definition: Solver.cs:134
Solver Translate(Context ctx)
Create a clone of the current solver with respect to ctx.
Definition: Solver.cs:450
void Add(IEnumerable< BoolExpr > constraints)
Alias for Assert.
Definition: Solver.cs:174
void Reset()
Resets the Solver.
Definition: Solver.cs:143
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:215
void Set(Symbol name, Symbol value)
Sets parameter on the solver
Definition: Solver.cs:97
void Push()
Creates a backtracking point.
Definition: Solver.cs:124
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:151
IEnumerable< BoolExpr[]> Cube()
Return a set of cubes.
Definition: Solver.cs:425
void FromString(string str)
Load solver assertions from a string.
Definition: Solver.cs:236
uint NumAssertions
The number of assertions in the solver.
Definition: Solver.cs:245
Params Parameters
Sets the solver parameters.
Definition: Solver.cs:48
Statistics Statistics
Solver statistics.
Definition: Solver.cs:468
uint NumScopes
The current number of backtracking points (scopes).
Definition: Solver.cs:116
Status Check(IEnumerable< BoolExpr > assumptions)
Checks whether the assertions in the solver are consistent or not.
Definition: Solver.cs:305
void Set(Symbol name, string value)
Sets parameter on the solver
Definition: Solver.cs:93
void ImportModelConverter(Solver src)
Import model converter from other solver.
Definition: Solver.cs:459
ParamDescrs ParameterDescriptions
Retrieves parameter descriptions for solver.
Definition: Solver.cs:105
Expr Proof
The proof of the last Check(params Expr[] assumptions).
Definition: Solver.cs:370
Status Check(params Expr[] assumptions)
Checks whether the assertions in the solver are consistent or not.
Definition: Solver.cs:287
BoolExpr[] UnsatCore
The unsat core of the last Check.
Definition: Solver.cs:390
BoolExpr[] Units
Currently inferred units.
Definition: Solver.cs:270
uint BacktrackLevel
Backtrack level that can be adjusted by conquer process
Definition: Solver.cs:414
override string ToString()
A string representation of the solver.
Definition: Solver.cs:479
void FromFile(string file)
Load solver assertions from a file.
Definition: Solver.cs:228
void Set(string name, bool value)
Sets parameter on the solver
Definition: Solver.cs:61
string ReasonUnknown
A brief justification of why the last call to Check returned UNKNOWN.
Definition: Solver.cs:403
void Set(Symbol name, double value)
Sets parameter on the solver
Definition: Solver.cs:89
void Set(Symbol name, bool value)
Sets parameter on the solver
Definition: Solver.cs:81
void Add(params BoolExpr[] constraints)
Alias for Assert.
Definition: Solver.cs:166
BoolExpr[] CubeVariables
Variables available and returned by the cuber.
Definition: Solver.cs:419
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:190
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:331
void Set(string name, Symbol value)
Sets parameter on the solver
Definition: Solver.cs:77
void Set(Symbol name, uint value)
Sets parameter on the solver
Definition: Solver.cs:85
Objects of this class track statistical information about solvers.
Definition: Statistics.cs:30
Symbols are used to name several term and type constructors.
Definition: Symbol.cs:30
The exception base class for error reporting from Z3
Definition: Z3Exception.cs:32
Internal base class for interfacing with native Z3 objects. Should not be used externally.
Definition: Z3Object.cs:33
Status
Status values.
Definition: Status.cs:29
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102