Z3
Data Structures | Public Member Functions | Properties
Solver Class Reference

Solvers. More...

+ Inheritance diagram for Solver:

Data Structures

class  DecRefQueue
 

Public Member Functions

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 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...
 
Status Check (params Expr[] 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...
 
Solver Translate (Context ctx)
 Create a clone of the current solver with respect to ctx. 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...
 
Model Model [get]
 The model of the last Check. More...
 
Expr Proof [get]
 The proof of the last Check. 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...
 
Statistics Statistics [get]
 Solver statistics. More...
 

Detailed Description

Solvers.

Definition at line 30 of file Solver.cs.

Member Function Documentation

§ Add()

void Add ( params BoolExpr []  constraints)
inline

Alias for Assert.

Definition at line 124 of file Solver.cs.

125  {
126  Assert(constraints);
127  }
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
Definition: Solver.cs:109

§ Assert()

void Assert ( params BoolExpr []  constraints)
inline

Assert a constraint (or multiple) into the solver.

Definition at line 109 of file Solver.cs.

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  }

§ AssertAndTrack() [1/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 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 with assumptions.

Definition at line 140 of file Solver.cs.

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  }

§ AssertAndTrack() [2/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 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 with assumptions.

Definition at line 165 of file Solver.cs.

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  }

§ Check()

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 209 of file Solver.cs.

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

§ 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 234 of file Solver.cs.

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

§ 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 92 of file Solver.cs.

93  {
94  Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
95  }

§ Push()

void Push ( )
inline

Creates a backtracking point.

See also
Pop

Definition at line 82 of file Solver.cs.

83  {
84  Native.Z3_solver_push(Context.nCtx, NativeObject);
85  }

§ Reset()

void Reset ( )
inline

Resets the Solver.

This removes all assertions from the solver.

Definition at line 101 of file Solver.cs.

102  {
103  Native.Z3_solver_reset(Context.nCtx, NativeObject);
104  }

§ ToString()

override string ToString ( )
inline

A string representation of the solver.

Definition at line 343 of file Solver.cs.

344  {
345  return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
346  }

§ Translate()

Solver Translate ( Context  ctx)
inline

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

Definition at line 319 of file Solver.cs.

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  }

Property Documentation

§ Assertions

BoolExpr [] Assertions
get

The set of asserted formulas.

Definition at line 191 of file Solver.cs.

§ Help

string Help
get

A string that describes all available solver parameters.

Definition at line 36 of file Solver.cs.

§ Model

Model Model
get

The model of the last Check.

The result is null if Check was not invoked before, if its results was not SATISFIABLE, or if model production is not enabled.

Definition at line 254 of file Solver.cs.

§ NumAssertions

uint NumAssertions
get

The number of assertions in the solver.

Definition at line 179 of file Solver.cs.

§ NumScopes

uint NumScopes
get

The current number of backtracking points (scopes).

See also
Pop, Push

Definition at line 74 of file Solver.cs.

§ ParameterDescriptions

ParamDescrs ParameterDescriptions
get

Retrieves parameter descriptions for solver.

Definition at line 63 of file Solver.cs.

§ Parameters

Params Parameters
set

Sets the solver parameters.

Definition at line 49 of file Solver.cs.

§ Proof

Expr Proof
get

The proof of the last Check.

The result is null if Check was not invoked before, if its results was not UNSATISFIABLE, or if proof production is disabled.

Definition at line 273 of file Solver.cs.

§ ReasonUnknown

string ReasonUnknown
get

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

Definition at line 307 of file Solver.cs.

§ Statistics

Solver statistics.

Definition at line 331 of file Solver.cs.

§ 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 293 of file Solver.cs.