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 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 25 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 113 of file Solver.java.

Referenced by Fixedpoint.__iadd__(), and Optimize.__iadd__().

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

§ 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 137 of file Solver.java.

138  {
139  getContext().checkContextMatch(constraints);
140  getContext().checkContextMatch(ps);
141  if (constraints.length != ps.length) {
142  throw new Z3Exception("Argument size mismatch");
143  }
144 
145  for (int i = 0; i < constraints.length; i++) {
146  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
147  constraints[i].getNativeObject(), ps[i].getNativeObject());
148  }
149  }

§ 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 164 of file Solver.java.

165  {
166  getContext().checkContextMatch(constraint);
167  getContext().checkContextMatch(p);
168 
169  Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
170  constraint.getNativeObject(), p.getNativeObject());
171  }

§ 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 202 of file Solver.java.

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

§ 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 231 of file Solver.java.

232  {
233  return check((Expr[]) null);
234  }

§ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Exceptions
Z3Exception

Definition at line 189 of file Solver.java.

190  {
191  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
192  return assrts.ToBoolExprArray();
193  }

§ getHelp()

String getHelp ( )
inline

A string that describes all available solver parameters.

Definition at line 29 of file Solver.java.

30  {
31  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
32  }

§ 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

, or if model production is not enabled.

Exceptions
Z3Exception

Definition at line 245 of file Solver.java.

246  {
247  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
248  if (x == 0) {
249  return null;
250  } else {
251  return new Model(getContext(), x);
252  }
253  }

§ getNumAssertions()

int getNumAssertions ( )
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 178 of file Solver.java.

179  {
180  ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
181  return assrts.size();
182  }

§ getNumScopes()

int getNumScopes ( )
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  }

§ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for solver.

Exceptions
Z3Exception

Definition at line 51 of file Solver.java.

52  {
53  return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
54  getContext().nCtx(), getNativeObject()));
55  }

§ 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

, or if proof production is disabled.

Exceptions
Z3Exception

Definition at line 264 of file Solver.java.

265  {
266  long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
267  if (x == 0) {
268  return null;
269  } else {
270  return Expr.create(getContext(), x);
271  }
272  }

§ getReasonUnknown()

String getReasonUnknown ( )
inline

A brief justification of why the last call to

Check

returned

.

Definition at line 294 of file Solver.java.

295  {
296  return Native.solverGetReasonUnknown(getContext().nCtx(),
297  getNativeObject());
298  }

§ getStatistics()

Statistics getStatistics ( )
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 313 of file Solver.java.

314  {
315  return new Statistics(getContext(), Native.solverGetStatistics(
316  getContext().nCtx(), getNativeObject()));
317  }

§ 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

, or if core production is disabled.

Exceptions
Z3Exception

Definition at line 283 of file Solver.java.

284  {
285 
286  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
287  return core.ToBoolExprArray();
288  }

§ pop() [1/2]

void pop ( )
inline

Backtracks one backtracking point. Remarks: .

Definition at line 81 of file Solver.java.

82  {
83  pop(1);
84  }

§ 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 93 of file Solver.java.

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

§ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 72 of file Solver.java.

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

§ reset()

void reset ( )
inline

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

Definition at line 103 of file Solver.java.

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

§ setParameters()

void setParameters ( Params  value)
inline

Sets the solver parameters.

Exceptions
Z3Exception

Definition at line 39 of file Solver.java.

40  {
41  getContext().checkContextMatch(value);
42  Native.solverSetParams(getContext().nCtx(), getNativeObject(),
43  value.getNativeObject());
44  }

§ toString()

String toString ( )
inline

A string representation of the solver.

Definition at line 323 of file Solver.java.

324  {
325  return Native
326  .solverToString(getContext().nCtx(), getNativeObject());
327  }

§ translate()

Solver translate ( Context  ctx)
inline

Create a clone of the current solver with respect to

ctx

.

Definition at line 303 of file Solver.java.

304  {
305  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
306  }