Solvers.
More...
Solvers.
Definition at line 30 of file Solver.cs.
§ Add()
void Add |
( |
params BoolExpr [] |
constraints | ) |
|
|
inline |
Alias for Assert.
Definition at line 124 of file Solver.cs.
void Assert(params BoolExpr[] constraints)
Assert a constraint (or multiple) into the solver.
§ Assert()
void Assert |
( |
params BoolExpr [] |
constraints | ) |
|
|
inline |
Assert a constraint (or multiple) into the solver.
Definition at line 109 of file Solver.cs.
111 Contract.Requires(constraints != null);
112 Contract.Requires(Contract.ForAll(constraints, c => c != null));
114 Context.CheckContextMatch<BoolExpr>(constraints);
115 foreach (BoolExpr a
in constraints)
117 Native.Z3_solver_assert(Context.nCtx, NativeObject, a.NativeObject);
§ AssertAndTrack() [1/2]
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.
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");
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);
§ AssertAndTrack() [2/2]
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.
167 Contract.Requires(constraint != null);
168 Contract.Requires(p != null);
169 Context.CheckContextMatch(constraint);
170 Context.CheckContextMatch(p);
172 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.NativeObject);
§ Check()
Checks whether the assertions in the solver are consistent or not.
- See also
- Model, UnsatCore, Proof
Definition at line 209 of file Solver.cs.
212 if (assumptions == null || assumptions.Length == 0)
213 r = (
Z3_lbool)Native.Z3_solver_check(Context.nCtx, NativeObject);
215 r = (
Z3_lbool)Native.Z3_solver_check_assumptions(Context.nCtx, NativeObject, (uint)assumptions.Length, AST.ArrayToNative(assumptions));
216 return lboolToStatus(r);
Z3_lbool
Lifted Boolean type: false, undefined, true.
§ Consequences()
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.
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);
Z3_lbool
Lifted Boolean type: false, undefined, true.
§ Pop()
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.
94 Native.Z3_solver_pop(Context.nCtx, NativeObject, n);
§ Push()
Creates a backtracking point.
- See also
- Pop
Definition at line 82 of file Solver.cs.
84 Native.Z3_solver_push(Context.nCtx, NativeObject);
§ Reset()
Resets the Solver.
This removes all assertions from the solver.
Definition at line 101 of file Solver.cs.
103 Native.Z3_solver_reset(Context.nCtx, NativeObject);
§ ToString()
override string ToString |
( |
| ) |
|
|
inline |
A string representation of the solver.
Definition at line 343 of file Solver.cs.
345 return Native.Z3_solver_to_string(Context.nCtx, NativeObject);
§ Translate()
Create a clone of the current solver with respect to ctx
.
Definition at line 319 of file Solver.cs.
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));
§ Assertions
The set of asserted formulas.
Definition at line 191 of file Solver.cs.
§ Help
A string that describes all available solver parameters.
Definition at line 36 of file Solver.cs.
§ Model
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
The number of assertions in the solver.
Definition at line 179 of file Solver.cs.
§ NumScopes
The current number of backtracking points (scopes).
- See also
- Pop, Push
Definition at line 74 of file Solver.cs.
§ ParameterDescriptions
Retrieves parameter descriptions for solver.
Definition at line 63 of file Solver.cs.
§ Parameters
Sets the solver parameters.
Definition at line 49 of file Solver.cs.
§ Proof
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
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 307 of file Solver.cs.
§ Statistics
§ UnsatCore
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.