|
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...
|
|
void | Dispose () |
| Disposes of the underlying native Z3 object. More...
|
|
Solvers.
Definition at line 30 of file Solver.cs.
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.
217 Debug.Assert(constraint !=
null);
218 Debug.Assert(p !=
null);
219 Context.CheckContextMatch(constraint);
220 Context.CheckContextMatch(p);
222 Native.Z3_solver_assert_and_track(Context.nCtx, NativeObject, constraint.NativeObject, p.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(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.
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");
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);