Solvers.
More...

void  Push () 
 Creates a backtracking point.


void  Pop (uint n=1) 
 Backtracks n backtracking points.


void  Reset () 
 Resets the Solver.


void  Assert (params BoolExpr[] constraints) 
 Assert a constraint (or multiple) into the solver.


Status  Check (params Expr[] assumptions) 
 Checks whether the assertions in the solver are consistent or not.


override string  ToString () 
 A string representation of the solver.


void  Dispose () 
 Disposes of the underlying native Z3 object.


Solvers.
Definition at line 29 of file Solver.cs.
void Assert 
( 
params BoolExpr[] 
constraints  ) 


inline 
Assert a constraint (or multiple) into the solver.
Definition at line 108 of file Solver.cs.
{
Contract.Requires(constraints != null);
Contract.Requires(Contract.ForAll(constraints, c => c != null));
Context.CheckContextMatch(constraints);
foreach (BoolExpr a in constraints)
{
Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
}
}
Checks whether the assertions in the solver are consistent or not.
 See Also
 Model, UnsatCore, Proof
Definition at line 158 of file Solver.cs.
{
if (assumptions == null)
r = (
Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
else
r = (
Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
switch (r)
{
default:
return Status.UNKNOWN;
}
}
Backtracks n backtracking points.
Note that an exception is thrown if n is not smaller than NumScopes
 See Also
 Push
Definition at line 91 of file Solver.cs.
{
Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
}
Creates a backtracking point.
 See Also
 Pop
Definition at line 81 of file Solver.cs.
{
Native.Z3_solver_push(Context.nCtx, NativeObject);
}
Resets the Solver.
This removes all assertions from the solver.
Definition at line 100 of file Solver.cs.
{
Native.Z3_solver_reset(Context.nCtx, NativeObject);
}
override string ToString 
( 
 ) 


inline 
A string representation of the solver.
Definition at line 263 of file Solver.cs.
{
return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
}
The set of asserted formulas.
Definition at line 136 of file Solver.cs.
A string that describes all available solver parameters.
Definition at line 35 of file Solver.cs.
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 181 of file Solver.cs.
The number of assertions in the solver.
Definition at line 124 of file Solver.cs.
The current number of backtracking points (scopes).
 See Also
 Pop, Push
Definition at line 73 of file Solver.cs.
ParamDescrs ParameterDescriptions 

get 
Retrieves parameter descriptions for solver.
Definition at line 62 of file Solver.cs.
Sets the solver parameters.
Definition at line 48 of file Solver.cs.
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 200 of file Solver.cs.
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 238 of file Solver.cs.
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 220 of file Solver.cs.