Z3 |

Data Structures | Public Member Functions | Properties
Solver Class Reference

Solvers. More...

Inheritance diagram for Solver:

## Data Structures
class | DecRefQueue

## Public Member Functions
void | Set (string name, bool value)
| Sets parameter on the solver More...
void | Set (string name, uint value)
| Sets parameter on the solver More...
void | Set (string name, double value)
| Sets parameter on the solver More...
void | Set (string name, string value)
| Sets parameter on the solver More...
void | Set (string name, Symbol value)
| Sets parameter on the solver More...
void | Set (Symbol name, bool value)
| Sets parameter on the solver More...
void | Set (Symbol name, uint value)
| Sets parameter on the solver More...
void | Set (Symbol name, double value)
| Sets parameter on the solver More...
void | Set (Symbol name, string value)
| Sets parameter on the solver More...
void | Set (Symbol name, Symbol value)
| Sets parameter on the solver More...
void | Push ()
| Creates a backtracking point. More...
void | Pop (uint n=1)
| Backtracks n backtracking points. More...
void | Reset ()
| Resets the Solver. More...
void | Assert (params BoolExpr[] constraints)
| Assert a constraint (or multiple) into the solver. More...
void | Add (params BoolExpr[] constraints)
| Alias for Assert. More...
void | Add (IEnumerable< BoolExpr > constraints)
| Alias for Assert. More...
void | AssertAndTrack (BoolExpr[] constraints, BoolExpr[] ps)
| Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps. More...
void | AssertAndTrack (BoolExpr constraint, BoolExpr p)
| Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p. More...
void | FromFile (string file)
| Load solver assertions from a file. More...
void | FromString (string str)
| Load solver assertions from a string. More...
Status | Check (params Expr[] assumptions)
| Checks whether the assertions in the solver are consistent or not. More...
Status | Check (IEnumerable< BoolExpr > assumptions)
| Checks whether the assertions in the solver are consistent or not. More...
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 an implication of the form More...
IEnumerable< BoolExpr[]> | Cube ()
| Return a set of cubes. More...
Solver | Translate (Context ctx)
| Create a clone of the current solver with respect to `ctx`. More...
void | ImportModelConverter (Solver src)
| Import model converter from other solver. More...
override string | ToString ()
| A string representation of the solver. More...
Public Member Functions inherited from Z3Object
void | Dispose ()
| Disposes of the underlying native Z3 object. More...

## Properties
string | Help`[get]`
| A string that describes all available solver parameters. More...
Params | Parameters`[set]`
| Sets the solver parameters. More...
ParamDescrs | ParameterDescriptions`[get]`
| Retrieves parameter descriptions for solver. More...
uint | NumScopes`[get]`
| The current number of backtracking points (scopes). More...
uint | NumAssertions`[get]`
| The number of assertions in the solver. More...
BoolExpr[] | Assertions`[get]`
| The set of asserted formulas. More...
BoolExpr[] | Units`[get]`
| Currently inferred units. More...
Model | Model`[get]`
| The model of the last `Check(params Expr[] assumptions)`. More...
Expr | Proof`[get]`
| The proof of the last `Check(params Expr[] assumptions)`. More...
BoolExpr[] | UnsatCore`[get]`
| The unsat core of the last `Check`. More...
string | ReasonUnknown`[get]`
| A brief justification of why the last call to `Check` returned `UNKNOWN`. More...
uint | BacktrackLevel`[get, set]`
| Backtrack level that can be adjusted by conquer process More...
BoolExpr[] | CubeVariables`[get, set]`
| Variables available and returned by the cuber. More...
Statistics | Statistics`[get]`
| Solver statistics. More...

## Detailed Description

Solvers.

Definition at line 30 of file Solver.cs.

## Member Function Documentation

## ◆ Add() [1/2]

void Add | ( | IEnumerable< BoolExpr > | constraints | ) |
| inline

Alias for Assert.

Definition at line 174 of file Solver.cs.

175 {
176 Assert(constraints.ToArray());
177 }
Microsoft.Z3.Solver.Assert
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:151

## ◆ Add() [2/2]

void Add | ( | params BoolExpr[] | constraints | ) |
| inline

Alias for Assert.

Definition at line 166 of file Solver.cs.

167 {
168 Assert(constraints);
169 }

## ◆ Assert()

void Assert | ( | params BoolExpr[] | constraints | ) |
| inline

Assert a constraint (or multiple) into the solver.

Definition at line 151 of file Solver.cs.

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 }

Referenced by Solver.Add(), Context.MkSolver(), and Solver.Translate().

## ◆ AssertAndTrack() [1/2]

void AssertAndTrack | ( | BoolExpr | constraint,
|  | BoolExpr | p
| ) |  |
| inline

Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.

This API is an alternative to Check(Expr[]) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using AssertAndTrack(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check(Expr[]) with assumptions.

Definition at line 215 of file Solver.cs.

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 }

## ◆ AssertAndTrack() [2/2]

void AssertAndTrack | ( | BoolExpr[] | constraints,
|  | BoolExpr[] | ps
| ) |  |
| inline

Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.

This API is an alternative to Check(Expr[]) with assumptions for extracting unsat cores. Both APIs can be used in the same solver. The unsat core will contain a combination of the Boolean variables provided using AssertAndTrack(BoolExpr[],BoolExpr[]) and the Boolean literals provided using Check(Expr[]) with assumptions.

Definition at line 190 of file Solver.cs.

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 }

## ◆ Check() [1/2]

Status Check | ( | IEnumerable< BoolExpr > | assumptions | ) |
| inline

Checks whether the assertions in the solver are consistent or not.

See also
  Model, UnsatCore, Proof

Definition at line 305 of file Solver.cs.

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 }
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ Check() [2/2]

Status Check | ( | params Expr[] | assumptions | ) |
| inline

Checks whether the assertions in the solver are consistent or not.

See also
  Model, UnsatCore, Proof

Definition at line 287 of file Solver.cs.

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 }

## ◆ Consequences()

Status Consequences | ( | IEnumerable< BoolExpr > | assumptions,
|  | IEnumerable< Expr > | variables,
|  | out BoolExpr[] | consequences
| ) |  |
| inline

Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form

      relevant-assumptions Implies variable = value

where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of the implication indicates how a variable is fixed.

See also
  Model, UnsatCore, Proof

Definition at line 331 of file Solver.cs.

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 }

## ◆ Cube()

IEnumerable< BoolExpr[]> Cube | ( |  | ) |
| inline

Return a set of cubes.

Definition at line 425 of file Solver.cs.

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 }
Microsoft.Z3.Solver.BacktrackLevel
uint BacktrackLevel
Backtrack level that can be adjusted by conquer process
Definition: Solver.cs:414
Microsoft.Z3.Solver.CubeVariables
BoolExpr[] CubeVariables
Variables available and returned by the cuber.
Definition: Solver.cs:419

## ◆ FromFile()

void FromFile | ( | string | file | ) |
| inline

Load solver assertions from a file.

Definition at line 228 of file Solver.cs.

229 {
230 Native.Z3_solver_from_file(Context.nCtx, NativeObject, file);
231 }

## ◆ FromString()

void FromString | ( | string | str | ) |
| inline

Load solver assertions from a string.

Definition at line 236 of file Solver.cs.

237 {
238 Native.Z3_solver_from_string(Context.nCtx, NativeObject, str);
239 }

## ◆ ImportModelConverter()

void ImportModelConverter | ( | Solver | src | ) |
| inline

Import model converter from other solver.

Definition at line 459 of file Solver.cs.

460 {
461 Native.Z3_solver_import_model_converter(Context.nCtx, src.NativeObject, NativeObject);
462 }

## ◆ Pop()

void Pop | ( | uint | n = `1` | ) |
| inline

Backtracks n backtracking points.

Note that an exception is thrown if n is not smaller than `NumScopes`

See also
  Push

Definition at line 134 of file Solver.cs.

135 {
136 Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
137 }

## ◆ Push()

void Push | ( |  | ) |
| inline

Creates a backtracking point.

See also
  Pop

Definition at line 124 of file Solver.cs.

125 {
126 Native.Z3_solver_push(Context.nCtx, NativeObject);
127 }

## ◆ Reset()

void Reset | ( |  | ) |
| inline

Resets the Solver.

This removes all assertions from the solver.

Definition at line 143 of file Solver.cs.

144 {
145 Native.Z3_solver_reset(Context.nCtx, NativeObject);
146 }

## ◆ Set() [1/10]

void Set | ( | string | name,
|  | bool | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 61 of file Solver.cs.

61{ Parameters = Context.MkParams().Add(name, value); }
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
Microsoft.Z3.Params.Add
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33
Microsoft.Z3.Solver.Parameters
Params Parameters
Sets the solver parameters.
Definition: Solver.cs:48

## ◆ Set() [2/10]

void Set | ( | string | name,
|  | double | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 69 of file Solver.cs.

69{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [3/10]

void Set | ( | string | name,
|  | string | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 73 of file Solver.cs.

73{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [4/10]

void Set | ( | string | name,
|  | Symbol | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 77 of file Solver.cs.

77{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [5/10]

void Set | ( | string | name,
|  | uint | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 65 of file Solver.cs.

65{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [6/10]

void Set | ( | Symbol | name,
|  | bool | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 81 of file Solver.cs.

81{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [7/10]

void Set | ( | Symbol | name,
|  | double | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 89 of file Solver.cs.

89{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [8/10]

void Set | ( | Symbol | name,
|  | string | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 93 of file Solver.cs.

93{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [9/10]

void Set | ( | Symbol | name,
|  | Symbol | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 97 of file Solver.cs.

97{ Parameters = Context.MkParams().Add(name, value); }

## ◆ Set() [10/10]

void Set | ( | Symbol | name,
|  | uint | value
| ) |  |
| inline

Sets parameter on the solver

Definition at line 85 of file Solver.cs.

85{ Parameters = Context.MkParams().Add(name, value); }

## ◆ ToString()

override string ToString | ( |  | ) |
| inline

A string representation of the solver.

Definition at line 479 of file Solver.cs.

480 {
481 return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
482 }

## ◆ Translate()

Solver Translate | ( | Context | ctx | ) |
| inline

Create a clone of the current solver with respect to `ctx`.

Definition at line 450 of file Solver.cs.

451 {
452 Debug.Assert(ctx != null);
453 return new Solver(ctx, Native.Z3_solver_translate(Context.nCtx, NativeObject, ctx.nCtx));
454 }

## Property Documentation

## ◆ Assertions

BoolExpr [] Assertions
| get

The set of asserted formulas.

Definition at line 256 of file Solver.cs.

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 }

## ◆ BacktrackLevel

uint BacktrackLevel
| get set

Backtrack level that can be adjusted by conquer process

Definition at line 414 of file Solver.cs.

414{ get; set; }

Referenced by Solver.Cube().

## ◆ CubeVariables

BoolExpr [] CubeVariables
| get set

Variables available and returned by the cuber.

Definition at line 419 of file Solver.cs.

419{ get; set; }

Referenced by Solver.Cube().

## ◆ Help

string Help
| get

A string that describes all available solver parameters.

Definition at line 35 of file Solver.cs.

36 {
37 get
38 {
39
40 return Native.Z3_solver_get_help(Context.nCtx, NativeObject);
41 }
42 }

## ◆ Model

Model Model
| get

The model of the last `Check(params Expr[] assumptions)`.

The result is `null` if `Check(params Expr[] assumptions)` was not invoked before, if its results was not `SATISFIABLE`, or if model production is not enabled.

Definition at line 350 of file Solver.cs.

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 }
Microsoft.Z3.Solver.Model
Model Model
The model of the last Check(params Expr[] assumptions).
Definition: Solver.cs:351

## ◆ NumAssertions

uint NumAssertions
| get

The number of assertions in the solver.

Definition at line 244 of file Solver.cs.

245 {
246 get
247 {
248 ASTVector assertions = new ASTVector(Context, Native.Z3_solver_get_assertions(Context.nCtx, NativeObject));
249 return assertions.Size;
250 }
251 }

## ◆ NumScopes

uint NumScopes
| get

The current number of backtracking points (scopes).

See also
  Pop, Push

Definition at line 115 of file Solver.cs.

116 {
117 get { return Native.Z3_solver_get_num_scopes(Context.nCtx, NativeObject); }
118 }

## ◆ ParameterDescriptions

ParamDescrs ParameterDescriptions
| get

Retrieves parameter descriptions for solver.

Definition at line 104 of file Solver.cs.

105 {
106 get { return new ParamDescrs(Context, Native.Z3_solver_get_param_descrs(Context.nCtx, NativeObject)); }
107 }

## ◆ Parameters

Params Parameters
| set

Sets the solver parameters.

Definition at line 47 of file Solver.cs.

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 }

Referenced by Solver.Set().

## ◆ Proof

Expr Proof
| get

The proof of the last `Check(params Expr[] assumptions)`.

The result is `null` if `Check(params Expr[] assumptions)` was not invoked before, if its results was not `UNSATISFIABLE`, or if proof production is disabled.

Definition at line 369 of file Solver.cs.

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 }

## ◆ ReasonUnknown

string ReasonUnknown
| get

A brief justification of why the last call to `Check` returned `UNKNOWN`.

Definition at line 402 of file Solver.cs.

403 {
404 get
405 {
406
407 return Native.Z3_solver_get_reason_unknown(Context.nCtx, NativeObject);
408 }
409 }

## ◆ Statistics

Statistics Statistics
| get

Solver statistics.

Definition at line 467 of file Solver.cs.

468 {
469 get
470 {
471
472 return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
473 }
474 }
Microsoft.Z3.Solver.Statistics
Statistics Statistics
Solver statistics.
Definition: Solver.cs:468

## ◆ Units

BoolExpr [] Units
| get

Currently inferred units.

Definition at line 269 of file Solver.cs.

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 }

## ◆ UnsatCore

BoolExpr [] UnsatCore
| get

The unsat core of the last `Check`.

The unsat core is a subset of `Assertions` The result is empty if `Check` was not invoked before, if its results was not `UNSATISFIABLE`, or if core production is disabled.

Definition at line 389 of file Solver.cs.

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 }