Solvers.
More...
Solvers.
Definition at line 29 of file Solver.cs.
void Add |
( |
params BoolExpr[] |
constraints | ) |
|
|
inline |
Alias for Assert.
Definition at line 123 of file Solver.cs.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
void Assert |
( |
params BoolExpr[] |
constraints | ) |
|
|
inline |
Assert a constraint (or multiple) into the solver.
Definition at line 108 of file Solver.cs.
110 Contract.Requires(constraints != null);
111 Contract.Requires(Contract.ForAll(constraints, c => c != null));
113 Context.CheckContextMatch(constraints);
114 foreach (BoolExpr a
in constraints)
116 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
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 139 of file Solver.cs.
141 Contract.Requires(constraints != null);
142 Contract.Requires(Contract.ForAll(constraints, c => c != null));
143 Contract.Requires(Contract.ForAll(ps, c => c != null));
144 Context.CheckContextMatch(constraints);
145 Context.CheckContextMatch(ps);
146 if (constraints.Length != ps.Length)
147 throw new Z3Exception(
"Argument size mismatch");
149 for (
int i = 0 ; i < constraints.Length; i++)
150 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraints[i].NativeObject, ps[i].NativeObject);
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 164 of file Solver.cs.
166 Contract.Requires(constraint != null);
167 Contract.Requires(p != null);
168 Context.CheckContextMatch(constraint);
169 Context.CheckContextMatch(p);
171 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
Checks whether the assertions in the solver are consistent or not.
- See also
- Model, UnsatCore, Proof
Definition at line 208 of file Solver.cs.
211 if (assumptions == null || assumptions.Length == 0)
212 r = (
Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
214 r = (
Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
219 default:
return Status.UNKNOWN;
Z3_lbool
Lifted Boolean type: false, undefined, true.
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.
93 Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
Creates a backtracking point.
- See also
- Pop
Definition at line 81 of file Solver.cs.
83 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.
102 Native.Z3_solver_reset(Context.nCtx, NativeObject);
override string ToString |
( |
| ) |
|
|
inline |
A string representation of the solver.
Definition at line 309 of file Solver.cs.
311 return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
The set of asserted formulas.
Definition at line 190 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 231 of file Solver.cs.
The number of assertions in the solver.
Definition at line 178 of file Solver.cs.
The current number of backtracking points (scopes).
- See also
- Pop, Push
Definition at line 73 of file Solver.cs.
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 250 of file Solver.cs.
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 284 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 270 of file Solver.cs.