Solvers.
Definition at line 25 of file Solver.java.
Assert a multiple constraints into the solver.
- Exceptions
-
Definition at line 108 of file Solver.java.
110 getContext().checkContextMatch(constraints);
113 Native.solverAssert(getContext().nCtx(), getNativeObject(),
114 a.getNativeObject());
Definition at line 132 of file Solver.java.
134 getContext().checkContextMatch(constraints);
135 getContext().checkContextMatch(ps);
136 if (constraints.length != ps.length)
137 throw new Z3Exception(
"Argument size mismatch");
139 for (
int i = 0; i < constraints.length; i++)
140 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
141 constraints[i].getNativeObject(), ps[i].getNativeObject());
Definition at line 157 of file Solver.java.
159 getContext().checkContextMatch(constraint);
160 getContext().checkContextMatch(p);
162 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
163 constraint.getNativeObject(), p.getNativeObject());
Checks whether the assertions in the solver are consistent or not.
- See also
- Model, UnsatCore, Proof
Definition at line 199 of file Solver.java.
202 if (assumptions == null)
203 r =
Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
206 r =
Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
207 .nCtx(), getNativeObject(), (
int) assumptions.length, AST
208 .arrayToNative(assumptions)));
212 return Status.SATISFIABLE;
214 return Status.UNSATISFIABLE;
Z3_lbool
Lifted Boolean type: false, undefined, true.
Checks whether the assertions in the solver are consistent or not.
- See also
- Model, UnsatCore, Proof
Definition at line 225 of file Solver.java.
227 return check((Expr[]) null);
The set of asserted formulas.
- Exceptions
-
Definition at line 183 of file Solver.java.
185 ASTVector ass =
new ASTVector(getContext(), Native.solverGetAssertions(
186 getContext().nCtx(), getNativeObject()));
189 for (
int i = 0; i < n; i++)
190 res[i] =
new BoolExpr(getContext(), ass.get(i).getNativeObject());
A string that describes all available solver parameters.
Definition at line 30 of file Solver.java.
32 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
The model of the last Check
.
The result is
if
was not invoked before, if its results was not
, or if model production is not enabled.
- Exceptions
-
Definition at line 238 of file Solver.java.
240 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
244 return new Model(getContext(), x);
The number of assertions in the solver.
- Exceptions
-
Definition at line 171 of file Solver.java.
173 ASTVector ass =
new ASTVector(getContext(), Native.solverGetAssertions(
174 getContext().nCtx(), getNativeObject()));
The current number of backtracking points (scopes).
- See also
- Pop, Push
Definition at line 62 of file Solver.java.
65 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
Retrieves parameter descriptions for solver.
- Exceptions
-
Definition at line 52 of file Solver.java.
54 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
55 getContext().nCtx(), getNativeObject()));
The proof of the last Check
.
The result is
if
was not invoked before, if its results was not
, or if proof production is disabled.
- Exceptions
-
Definition at line 255 of file Solver.java.
257 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
261 return Expr.create(getContext(), x);
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 288 of file Solver.java.
290 return Native.solverGetReasonUnknown(getContext().nCtx(),
Solver statistics.
- Exceptions
-
Definition at line 299 of file Solver.java.
301 return new Statistics(getContext(), Native.solverGetStatistics(
302 getContext().nCtx(), getNativeObject()));
The unsat core of the last Check
.
The unsat core is a subset of
The result is empty if
was not invoked before, if its results was not
, or if core production is disabled.
- Exceptions
-
Definition at line 272 of file Solver.java.
275 ASTVector core =
new ASTVector(getContext(), Native.solverGetUnsatCore(
276 getContext().nCtx(), getNativeObject()));
278 Expr[] res =
new Expr[n];
279 for (
int i = 0; i < n; i++)
280 res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
Backtracks one backtracking point.
.
Definition at line 79 of file Solver.java.
Backtracks n backtracking points.
Note that an exception is thrown if n is not smaller than
- See also
- Push
Definition at line 89 of file Solver.java.
91 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
Creates a backtracking point.
- See also
- Pop
Definition at line 71 of file Solver.java.
73 Native.solverPush(getContext().nCtx(), getNativeObject());
Resets the Solver.
This removes all assertions from the solver.
Definition at line 98 of file Solver.java.
100 Native.solverReset(getContext().nCtx(), getNativeObject());
Sets the solver parameters.
- Exceptions
-
Definition at line 40 of file Solver.java.
42 getContext().checkContextMatch(value);
43 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
44 value.getNativeObject());
A string representation of the solver.
Definition at line 308 of file Solver.java.
313 .solverToString(getContext().nCtx(), getNativeObject());
314 }
catch (Z3Exception e)
316 return "Z3Exception: " + e.getMessage();