Z3
Public Member Functions
Solver Class Reference
+ Inheritance diagram for Solver:

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 ()
 
- Public Member Functions inherited from Z3Object
void dispose () throws Z3Exception
 
- Public Member Functions inherited from IDisposable
void dispose () throws Z3Exception
 

Additional Inherited Members

- Protected Member Functions inherited from Z3Object
void finalize () throws Z3Exception
 

Detailed Description

Solvers.

Definition at line 25 of file Solver.java.

Member Function Documentation

void add ( BoolExpr...  constraints) throws Z3Exception
inline

Assert a multiple constraints into the solver.

Exceptions
Z3Exception

Definition at line 108 of file Solver.java.

109  {
110  getContext().checkContextMatch(constraints);
111  for (BoolExpr a : constraints)
112  {
113  Native.solverAssert(getContext().nCtx(), getNativeObject(),
114  a.getNativeObject());
115  }
116  }
void assertAndTrack ( BoolExpr[]  constraints,
BoolExpr[]  ps 
) throws Z3Exception
inline

Definition at line 132 of file Solver.java.

133  {
134  getContext().checkContextMatch(constraints);
135  getContext().checkContextMatch(ps);
136  if (constraints.length != ps.length)
137  throw new Z3Exception("Argument size mismatch");
138 
139  for (int i = 0; i < constraints.length; i++)
140  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
141  constraints[i].getNativeObject(), ps[i].getNativeObject());
142  }
void assertAndTrack ( BoolExpr  constraint,
BoolExpr  p 
) throws Z3Exception
inline

Definition at line 157 of file Solver.java.

158  {
159  getContext().checkContextMatch(constraint);
160  getContext().checkContextMatch(p);
161 
162  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
163  constraint.getNativeObject(), p.getNativeObject());
164  }
Status check ( Expr...  assumptions) throws Z3Exception
inline

Checks whether the assertions in the solver are consistent or not.

See also
Model, UnsatCore, Proof

Definition at line 199 of file Solver.java.

200  {
201  Z3_lbool r;
202  if (assumptions == null)
203  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
204  getNativeObject()));
205  else
206  r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
207  .nCtx(), getNativeObject(), (int) assumptions.length, AST
208  .arrayToNative(assumptions)));
209  switch (r)
210  {
211  case Z3_L_TRUE:
212  return Status.SATISFIABLE;
213  case Z3_L_FALSE:
214  return Status.UNSATISFIABLE;
215  default:
216  return Status.UNKNOWN;
217  }
218  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:135
Status
Status values.
Definition: Status.cs:27
Status check ( ) throws Z3Exception
inline

Checks whether the assertions in the solver are consistent or not.

See also
Model, UnsatCore, Proof

Definition at line 225 of file Solver.java.

226  {
227  return check((Expr[]) null);
228  }
BoolExpr [] getAssertions ( ) throws Z3Exception
inline

The set of asserted formulas.

Exceptions
Z3Exception

Definition at line 183 of file Solver.java.

184  {
185  ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
186  getContext().nCtx(), getNativeObject()));
187  int n = ass.size();
188  BoolExpr[] res = new BoolExpr[n];
189  for (int i = 0; i < n; i++)
190  res[i] = new BoolExpr(getContext(), ass.get(i).getNativeObject());
191  return res;
192  }
String getHelp ( ) throws Z3Exception
inline

A string that describes all available solver parameters.

Definition at line 30 of file Solver.java.

31  {
32  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
33  }
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

, or if model production is not enabled.

Exceptions
Z3Exception

Definition at line 238 of file Solver.java.

239  {
240  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
241  if (x == 0)
242  return null;
243  else
244  return new Model(getContext(), x);
245  }
int getNumAssertions ( ) throws Z3Exception
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 171 of file Solver.java.

172  {
173  ASTVector ass = new ASTVector(getContext(), Native.solverGetAssertions(
174  getContext().nCtx(), getNativeObject()));
175  return ass.size();
176  }
int getNumScopes ( ) throws Z3Exception
inline

The current number of backtracking points (scopes).

See also
Pop, Push

Definition at line 62 of file Solver.java.

63  {
64  return Native
65  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
66  }
ParamDescrs getParameterDescriptions ( ) throws Z3Exception
inline

Retrieves parameter descriptions for solver.

Exceptions
Z3Exception

Definition at line 52 of file Solver.java.

53  {
54  return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
55  getContext().nCtx(), getNativeObject()));
56  }
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

, or if proof production is disabled.

Exceptions
Z3Exception

Definition at line 255 of file Solver.java.

256  {
257  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
258  if (x == 0)
259  return null;
260  else
261  return Expr.create(getContext(), x);
262  }
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.

289  {
290  return Native.solverGetReasonUnknown(getContext().nCtx(),
291  getNativeObject());
292  }
Statistics getStatistics ( ) throws Z3Exception
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 299 of file Solver.java.

300  {
301  return new Statistics(getContext(), Native.solverGetStatistics(
302  getContext().nCtx(), getNativeObject()));
303  }
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

, or if core production is disabled.

Exceptions
Z3Exception

Definition at line 272 of file Solver.java.

273  {
274 
275  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(
276  getContext().nCtx(), getNativeObject()));
277  int n = core.size();
278  Expr[] res = new Expr[n];
279  for (int i = 0; i < n; i++)
280  res[i] = Expr.create(getContext(), core.get(i).getNativeObject());
281  return res;
282  }
void pop ( ) throws Z3Exception
inline

Backtracks one backtracking point.

.

Definition at line 79 of file Solver.java.

80  {
81  pop(1);
82  }
void pop ( int  n) throws Z3Exception
inline

Backtracks n backtracking points.

Note that an exception is thrown if n is not smaller than

NumScopes
See also
Push

Definition at line 89 of file Solver.java.

90  {
91  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
92  }
void push ( ) throws Z3Exception
inline

Creates a backtracking point.

See also
Pop

Definition at line 71 of file Solver.java.

72  {
73  Native.solverPush(getContext().nCtx(), getNativeObject());
74  }
void reset ( ) throws Z3Exception
inline

Resets the Solver.

This removes all assertions from the solver.

Definition at line 98 of file Solver.java.

99  {
100  Native.solverReset(getContext().nCtx(), getNativeObject());
101  }
void setParameters ( Params  value) throws Z3Exception
inline

Sets the solver parameters.

Exceptions
Z3Exception

Definition at line 40 of file Solver.java.

41  {
42  getContext().checkContextMatch(value);
43  Native.solverSetParams(getContext().nCtx(), getNativeObject(),
44  value.getNativeObject());
45  }
String toString ( )
inline

A string representation of the solver.

Definition at line 308 of file Solver.java.

309  {
310  try
311  {
312  return Native
313  .solverToString(getContext().nCtx(), getNativeObject());
314  } catch (Z3Exception e)
315  {
316  return "Z3Exception: " + e.getMessage();
317  }
318  }