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

Public Member Functions

String getHelp ()
 
void setParameters (Params value)
 
ParamDescrs getParameterDescriptions ()
 
int getNumScopes ()
 
void push ()
 
void pop ()
 
void pop (int n)
 
void reset ()
 
void add (BoolExpr... constraints)
 
void fromFile (String file)
 
void fromString (String str)
 
void assertAndTrack (BoolExpr[] constraints, BoolExpr[] ps)
 
void assertAndTrack (BoolExpr constraint, BoolExpr p)
 
int getNumAssertions ()
 
BoolExpr [] getAssertions ()
 
Status check (Expr... assumptions)
 
Status check ()
 
Model getModel ()
 
Expr getProof ()
 
BoolExpr [] getUnsatCore ()
 
String getReasonUnknown ()
 
Solver translate (Context ctx)
 
Statistics getStatistics ()
 
String toString ()
 

Detailed Description

Solvers.

Definition at line 26 of file Solver.java.

Member Function Documentation

§ add()

void add ( BoolExpr...  constraints)
inline

Assert a multiple constraints into the solver.

Exceptions
Z3Exception

Definition at line 114 of file Solver.java.

115  {
116  getContext().checkContextMatch(constraints);
117  for (BoolExpr a : constraints)
118  {
119  Native.solverAssert(getContext().nCtx(), getNativeObject(),
120  a.getNativeObject());
121  }
122  }

§ assertAndTrack() [1/2]

void assertAndTrack ( BoolExpr []  constraints,
BoolExpr []  ps 
)
inline

Assert multiple constraints into the solver, and track them (in the unsat) core using the Boolean constants in ps.

Remarks: 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

and the Boolean literals provided using check() with assumptions.

Definition at line 155 of file Solver.java.

156  {
157  getContext().checkContextMatch(constraints);
158  getContext().checkContextMatch(ps);
159  if (constraints.length != ps.length) {
160  throw new Z3Exception("Argument size mismatch");
161  }
162 
163  for (int i = 0; i < constraints.length; i++) {
164  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
165  constraints[i].getNativeObject(), ps[i].getNativeObject());
166  }
167  }

§ assertAndTrack() [2/2]

void assertAndTrack ( BoolExpr  constraint,
BoolExpr  p 
)
inline

Assert a constraint into the solver, and track it (in the unsat) core using the Boolean constant p.

Remarks: 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 and the Boolean literals provided using check with assumptions.

Definition at line 182 of file Solver.java.

183  {
184  getContext().checkContextMatch(constraint);
185  getContext().checkContextMatch(p);
186 
187  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
188  constraint.getNativeObject(), p.getNativeObject());
189  }

§ check() [1/2]

Status check ( Expr...  assumptions)
inline

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

See also
getModel
getUnsatCore
getProof

Definition at line 220 of file Solver.java.

221  {
222  Z3_lbool r;
223  if (assumptions == null) {
224  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
225  getNativeObject()));
226  } else {
227  r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
228  .nCtx(), getNativeObject(), assumptions.length, AST
229  .arrayToNative(assumptions)));
230  }
231  switch (r)
232  {
233  case Z3_L_TRUE:
234  return Status.SATISFIABLE;
235  case Z3_L_FALSE:
236  return Status.UNSATISFIABLE;
237  default:
238  return Status.UNKNOWN;
239  }
240  }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:106

§ check() [2/2]

Status check ( )
inline

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

See also
getModel
getUnsatCore
getProof

Definition at line 249 of file Solver.java.

250  {
251  return check((Expr[]) null);
252  }

§ fromFile()

void fromFile ( String  file)
inline

Load solver assertions from a file.

Definition at line 127 of file Solver.java.

128  {
129  Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
130  }

§ fromString()

void fromString ( String  str)
inline

Load solver assertions from a string.

Definition at line 135 of file Solver.java.

136  {
137  Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
138  }

§ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Exceptions
Z3Exception

Definition at line 207 of file Solver.java.

208  {
209  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
210  return assrts.ToBoolExprArray();
211  }

§ getHelp()

String getHelp ( )
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  }

§ getModel()

Model getModel ( )
inline

The model of the last

Check

. Remarks: The result is

null

if

Check

was not invoked before, if its results was not

SATISFIABLE

, or if model production is not enabled.

Exceptions
Z3Exception

Definition at line 263 of file Solver.java.

264  {
265  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
266  if (x == 0) {
267  return null;
268  } else {
269  return new Model(getContext(), x);
270  }
271  }

§ getNumAssertions()

int getNumAssertions ( )
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 196 of file Solver.java.

197  {
198  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
199  return assrts.size();
200  }

§ getNumScopes()

int getNumScopes ( )
inline

The current number of backtracking points (scopes).

See also
pop
push

Definition at line 63 of file Solver.java.

64  {
65  return Native
66  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
67  }

§ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
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  }

§ getProof()

Expr getProof ( )
inline

The proof of the last

Check

. Remarks: The result is

null

if

Check

was not invoked before, if its results was not

UNSATISFIABLE

, or if proof production is disabled.

Exceptions
Z3Exception

Definition at line 282 of file Solver.java.

283  {
284  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
285  if (x == 0) {
286  return null;
287  } else {
288  return Expr.create(getContext(), x);
289  }
290  }

§ getReasonUnknown()

String getReasonUnknown ( )
inline

A brief justification of why the last call to

Check

returned

UNKNOWN

.

Definition at line 312 of file Solver.java.

313  {
314  return Native.solverGetReasonUnknown(getContext().nCtx(),
315  getNativeObject());
316  }

§ getStatistics()

Statistics getStatistics ( )
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 331 of file Solver.java.

332  {
333  return new Statistics(getContext(), Native.solverGetStatistics(
334  getContext().nCtx(), getNativeObject()));
335  }

§ getUnsatCore()

BoolExpr [] getUnsatCore ( )
inline

The unsat core of the last

Check

. Remarks: 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.

Exceptions
Z3Exception

Definition at line 301 of file Solver.java.

302  {
303 
304  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
305  return core.ToBoolExprArray();
306  }

§ pop() [1/2]

void pop ( )
inline

Backtracks one backtracking point. Remarks: .

Definition at line 82 of file Solver.java.

83  {
84  pop(1);
85  }

§ pop() [2/2]

void pop ( int  n)
inline

Backtracks

n

backtracking points. Remarks: Note that an exception is thrown if

n

is not smaller than

NumScopes
See also
push

Definition at line 94 of file Solver.java.

95  {
96  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
97  }

§ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 73 of file Solver.java.

74  {
75  Native.solverPush(getContext().nCtx(), getNativeObject());
76  }

§ reset()

void reset ( )
inline

Resets the Solver. Remarks: This removes all assertions from the solver.

Definition at line 104 of file Solver.java.

105  {
106  Native.solverReset(getContext().nCtx(), getNativeObject());
107  }

§ setParameters()

void setParameters ( Params  value)
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  }

§ toString()

String toString ( )
inline

A string representation of the solver.

Definition at line 341 of file Solver.java.

342  {
343  return Native
344  .solverToString(getContext().nCtx(), getNativeObject());
345  }

§ translate()

Solver translate ( Context  ctx)
inline

Create a clone of the current solver with respect to

ctx

.

Definition at line 321 of file Solver.java.

322  {
323  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
324  }