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  }

◆ 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  }

◆ 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  }

◆ 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); }

◆ 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 257 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
getset

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
getset

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 36 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 351 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  }

◆ NumAssertions

uint NumAssertions
get

The number of assertions in the solver.

Definition at line 245 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 116 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 105 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 48 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 370 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 403 of file Solver.cs.

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

◆ Statistics

Solver statistics.

Definition at line 468 of file Solver.cs.

468  {
469  get
470  {
471 
472  return new Statistics(Context, Native.Z3_solver_get_statistics(Context.nCtx, NativeObject));
473  }
474  }

◆ Units

BoolExpr [] Units
get

Currently inferred units.

Definition at line 270 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 390 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  }
Microsoft.Z3.Solver.Model
Model Model
The model of the last Check(params Expr[] assumptions).
Definition: Solver.cs:351
Microsoft.Z3.Solver.CubeVariables
BoolExpr[] CubeVariables
Variables available and returned by the cuber.
Definition: Solver.cs:419
Microsoft.Z3.Solver.Parameters
Params Parameters
Sets the solver parameters.
Definition: Solver.cs:48
Microsoft.Z3.Solver.Assert
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:151
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:101
Microsoft.Z3.Params.Add
Params Add(Symbol name, bool value)
Adds a parameter setting.
Definition: Params.cs:33
Microsoft.Z3.Solver.BacktrackLevel
uint BacktrackLevel
Backtrack level that can be adjusted by conquer process
Definition: Solver.cs:414
Microsoft.Z3.Context.MkParams
Params MkParams()
Creates a new ParameterSet.
Definition: Context.cs:3290
Microsoft.Z3.Solver.Statistics
Statistics Statistics
Solver statistics.
Definition: Solver.cs:468