Public Member Functions | |
String | getHelp () throws Z3Exception |
void | setParameters (Params value) throws Z3Exception |
ParamDescrs | getParameterDescriptions () throws Z3Exception |
int | getNumScopes () throws Z3Exception |
void | push () throws Z3Exception |
void | pop () throws Z3Exception |
void | pop (int n) throws Z3Exception |
void | reset () throws Z3Exception |
void | add (BoolExpr...constraints) throws Z3Exception |
void | assertAndTrack (BoolExpr[] constraints, BoolExpr[] ps) throws Z3Exception |
void | assertAndTrack (BoolExpr constraint, BoolExpr p) throws Z3Exception |
int | getNumAssertions () throws Z3Exception |
BoolExpr[] | getAssertions () throws Z3Exception |
Status | check (Expr...assumptions) throws Z3Exception |
Status | check () throws Z3Exception |
Model | getModel () throws Z3Exception |
Expr | getProof () throws Z3Exception |
Expr[] | getUnsatCore () throws Z3Exception |
String | getReasonUnknown () throws Z3Exception |
Statistics | getStatistics () throws Z3Exception |
String | toString () |
Package Functions | |
Solver (Context ctx, long obj) throws Z3Exception | |
void | incRef (long o) throws Z3Exception |
void | decRef (long o) throws Z3Exception |
Solvers.
Definition at line 25 of file Solver.java.
Solver | ( | Context | ctx, |
long | obj | ||
) | throws Z3Exception [inline, package] |
Definition at line 320 of file Solver.java.
{ super(ctx, obj); }
void add | ( | BoolExpr... | constraints | ) | throws Z3Exception [inline] |
Assert a multiple constraints into the solver.
Z3Exception |
Definition at line 108 of file Solver.java.
{ getContext().checkContextMatch(constraints); for (BoolExpr a : constraints) { Native.solverAssert(getContext().nCtx(), getNativeObject(), a.getNativeObject()); } }
void assertAndTrack | ( | BoolExpr[] | constraints, |
BoolExpr[] | ps | ||
) | throws Z3Exception [inline] |
Definition at line 132 of file Solver.java.
{ getContext().checkContextMatch(constraints); getContext().checkContextMatch(ps); if (constraints.length != ps.length) throw new Z3Exception("Argument size mismatch"); for (int i = 0; i < constraints.length; i++) Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(), constraints[i].getNativeObject(), ps[i].getNativeObject()); }
void assertAndTrack | ( | BoolExpr | constraint, |
BoolExpr | p | ||
) | throws Z3Exception [inline] |
Definition at line 157 of file Solver.java.
{ getContext().checkContextMatch(constraint); getContext().checkContextMatch(p); Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(), constraint.getNativeObject(), p.getNativeObject()); }
Status check | ( | Expr... | assumptions | ) | throws Z3Exception [inline] |
Checks whether the assertions in the solver are consistent or not.
Definition at line 199 of file Solver.java.
{ Z3_lbool r; if (assumptions == null) r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(), getNativeObject())); else r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext() .nCtx(), getNativeObject(), (int) assumptions.length, AST .arrayToNative(assumptions))); switch (r) { case Z3_L_TRUE: return Status.SATISFIABLE; case Z3_L_FALSE: return Status.UNSATISFIABLE; default: return Status.UNKNOWN; } }
Status check | ( | ) | throws Z3Exception [inline] |
Checks whether the assertions in the solver are consistent or not.
Definition at line 225 of file Solver.java.
{ return check((Expr[]) null); }
void decRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 331 of file Solver.java.
{ getContext().solver_DRQ().add(o); super.decRef(o); }
BoolExpr [] getAssertions | ( | ) | throws Z3Exception [inline] |
The set of asserted formulas.
Z3Exception |
Definition at line 183 of file Solver.java.
{ ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); int n = ass.size(); BoolExpr[] res = new BoolExpr[n]; for (int i = 0; i < n; i++) res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject()); return res; }
String getHelp | ( | ) | throws Z3Exception [inline] |
A string that describes all available solver parameters.
Definition at line 30 of file Solver.java.
{ return Native.solverGetHelp(getContext().nCtx(), getNativeObject()); }
Model getModel | ( | ) | throws Z3Exception [inline] |
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.
Z3Exception |
Definition at line 238 of file Solver.java.
{ long x = Native.solverGetModel(getContext().nCtx(), getNativeObject()); if (x == 0) return null; else return new Model(getContext(), x); }
int getNumAssertions | ( | ) | throws Z3Exception [inline] |
The number of assertions in the solver.
Z3Exception |
Definition at line 171 of file Solver.java.
{ ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions( getContext().nCtx(), getNativeObject())); return ass.size(); }
int getNumScopes | ( | ) | throws Z3Exception [inline] |
The current number of backtracking points (scopes).
Definition at line 62 of file Solver.java.
{ return Native .solverGetNumScopes(getContext().nCtx(), getNativeObject()); }
ParamDescrs getParameterDescriptions | ( | ) | throws Z3Exception [inline] |
Retrieves parameter descriptions for solver.
Z3Exception |
Definition at line 52 of file Solver.java.
{ return new ParamDescrs(getContext(), Native.solverGetParamDescrs( getContext().nCtx(), getNativeObject())); }
Expr getProof | ( | ) | throws Z3Exception [inline] |
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.
Z3Exception |
Definition at line 255 of file Solver.java.
{ long x = Native.solverGetProof(getContext().nCtx(), getNativeObject()); if (x == 0) return null; else return Expr.create(getContext(), x); }
String getReasonUnknown | ( | ) | throws Z3Exception [inline] |
A brief justification of why the last call to Check
returned UNKNOWN
.
Definition at line 288 of file Solver.java.
{ return Native.solverGetReasonUnknown(getContext().nCtx(), getNativeObject()); }
Statistics getStatistics | ( | ) | throws Z3Exception [inline] |
Solver statistics.
Z3Exception |
Definition at line 299 of file Solver.java.
{ return new Statistics(getContext(), Native.solverGetStatistics( getContext().nCtx(), getNativeObject())); }
Expr [] getUnsatCore | ( | ) | throws Z3Exception [inline] |
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.
Z3Exception |
Definition at line 272 of file Solver.java.
{ ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore( getContext().nCtx(), getNativeObject())); int n = core.size(); Expr[] res = new Expr[n]; for (int i = 0; i < n; i++) res[i] = Expr.create(getContext(), core.get(i).getNativeObject()); return res; }
void incRef | ( | long | o | ) | throws Z3Exception [inline, package] |
Reimplemented from Z3Object.
Definition at line 325 of file Solver.java.
{ getContext().solver_DRQ().incAndClear(getContext(), o); super.incRef(o); }
void pop | ( | ) | throws Z3Exception [inline] |
void pop | ( | int | n | ) | throws Z3Exception [inline] |
Backtracks n backtracking points. Note that an exception is thrown if n is not smaller than NumScopes
Definition at line 89 of file Solver.java.
{ Native.solverPop(getContext().nCtx(), getNativeObject(), n); }
void push | ( | ) | throws Z3Exception [inline] |
Creates a backtracking point.
Definition at line 71 of file Solver.java.
{ Native.solverPush(getContext().nCtx(), getNativeObject()); }
void reset | ( | ) | throws Z3Exception [inline] |
Resets the Solver. This removes all assertions from the solver.
Definition at line 98 of file Solver.java.
{ Native.solverReset(getContext().nCtx(), getNativeObject()); }
void setParameters | ( | Params | value | ) | throws Z3Exception [inline] |
Sets the solver parameters.
Z3Exception |
Definition at line 40 of file Solver.java.
{ getContext().checkContextMatch(value); Native.solverSetParams(getContext().nCtx(), getNativeObject(), value.getNativeObject()); }
String toString | ( | ) | [inline] |
A string representation of the solver.
Definition at line 308 of file Solver.java.
{ try { return Native .solverToString(getContext().nCtx(), getNativeObject()); } catch (Z3Exception e) { return "Z3Exception: " + e.getMessage(); } }