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 | interrupt ()
void | add (Expr< BoolSort >... constraints)
void | assertAndTrack (Expr< BoolSort >[] constraints, Expr< BoolSort >[] ps)
void | assertAndTrack (Expr< BoolSort > constraint, Expr< BoolSort > p)
void | fromFile (String file)
| Load solver assertions from a file. More...
void | fromString (String str)
| Load solver assertions from a string. More...
int | getNumAssertions ()
BoolExpr[] | getAssertions ()
final Status | check (Expr< BoolSort >... assumptions)
Status | check ()
Status | getConsequences (Expr< BoolSort >[] assumptions, Expr<?>[] variables, List< Expr< BoolSort > > consequences)
Model | getModel ()
Expr<?> | getProof ()
BoolExpr[] | getUnsatCore ()
String | getReasonUnknown ()
Solver | translate (Context ctx)
Statistics | getStatistics ()
String | toString ()

## Additional Inherited Members
Static Public Member Functions inherited from Z3Object
static long[] | arrayToNative (Z3Object[] a)
static int | arrayLength (Z3Object[] a)

## Detailed Description

Solvers.

Definition at line 28 of file Solver.java.

## Member Function Documentation

## ◆ add()

void add | ( | Expr< BoolSort >... | constraints | ) |
| inline

Assert a multiple constraints into the solver.

Exceptions

  Z3Exception |

Definition at line 126 of file Solver.java.

127 {
128 getContext().checkContextMatch(constraints);
129 for (Expr<BoolSort> a : constraints)
130 {
131 Native.solverAssert(getContext().nCtx(), getNativeObject(),
132 a.getNativeObject());
133 }
134 }

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

## ◆ assertAndTrack() [1/2]

void assertAndTrack | ( | Expr< BoolSort > | constraint,
|  | Expr< BoolSort > | 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 178 of file Solver.java.

179 {
180 getContext().checkContextMatch(constraint);
181 getContext().checkContextMatch(p);
182
183 Native.solverAssertAndTrack(getContext().nCtx(), getNativeObject(),
184 constraint.getNativeObject(), p.getNativeObject());
185 }

## ◆ assertAndTrack() [2/2]

void assertAndTrack | ( | Expr< BoolSort >[] | constraints,
|  | Expr< BoolSort >[] | 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 151 of file Solver.java.

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

## ◆ check() [1/2]

Status check | ( |  | ) |
| inline

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

See also
  getModel
  getUnsatCore
  getProof

Definition at line 256 of file Solver.java.

257 {
258 return check((Expr[]) null);
259 }
com.microsoft.z3.Solver.check
Status check()
Definition: Solver.java:256

## ◆ check() [2/2]

final Status check | ( | Expr< BoolSort >... | assumptions | ) |
| inline

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

See also
  getModel
  getUnsatCore
  getProof

Definition at line 234 of file Solver.java.

235 {
236 Z3_lbool r;
237 if (assumptions == null) {
238 r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
239 getNativeObject()));
240 } else {
241 r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
242 .nCtx(), getNativeObject(), assumptions.length, AST
243 .arrayToNative(assumptions)));
244 }
245 return lboolToStatus(r);
246 }
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:102

## ◆ fromFile()

void fromFile | ( | String | file | ) |
| inline

Load solver assertions from a file.

Definition at line 190 of file Solver.java.

191 {
192 Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
193 }

## ◆ fromString()

void fromString | ( | String | str | ) |
| inline

Load solver assertions from a string.

Definition at line 198 of file Solver.java.

199 {
200 Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
201 }

## ◆ getAssertions()

BoolExpr[] getAssertions | ( |  | ) |
| inline

The set of asserted formulas.

Exceptions

  Z3Exception |

Definition at line 220 of file Solver.java.

221 {
222 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
223 return assrts.ToBoolExprArray();
224 }

## ◆ getConsequences()

Status getConsequences | ( | Expr< BoolSort >[] | assumptions,
|  | Expr<?>[] | variables,
|  | List< Expr< BoolSort > > | consequences
| ) |  |
| inline

Retrieve fixed assignments to the set of variables in the form of consequences. Each consequence is an implication of the form

      relevant-assumptions Implies variable = value

where the relevant assumptions is a subset of the assumptions that are passed in and the equality on the right side of the implication indicates how a variable is fixed.

Definition at line 272 of file Solver.java.

273 {
274 ASTVector result = new ASTVector(getContext());
275 ASTVector asms = new ASTVector(getContext());
276 ASTVector vars = new ASTVector(getContext());
277 for (Expr<BoolSort> asm : assumptions) asms.push(asm);
278 for (Expr<?> v : variables) vars.push(v);
279 int r = Native.solverGetConsequences(getContext().nCtx(), getNativeObject(), asms.getNativeObject(), vars.getNativeObject(), result.getNativeObject());
280 for (int i = 0; i < result.size(); ++i) consequences.add((BoolExpr) Expr.create(getContext(), result.get(i).getNativeObject()));
281 return lboolToStatus(Z3_lbool.fromInt(r));
282 }

## ◆ getHelp()

String getHelp | ( |  | ) |
| inline

A string that describes all available solver parameters.

Definition at line 32 of file Solver.java.

33 {
34 return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
35 }

## ◆ 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 294 of file Solver.java.

295 {
296 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
297 if (x == 0) {
298 return null;
299 } else {
300 return new Model(getContext(), x);
301 }
302 }
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6579

## ◆ getNumAssertions()

int getNumAssertions | ( |  | ) |
| inline

The number of assertions in the solver.

Exceptions

  Z3Exception |

Definition at line 209 of file Solver.java.

210 {
211 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
212 return assrts.size();
213 }

## ◆ getNumScopes()

int getNumScopes | ( |  | ) |
| inline

The current number of backtracking points (scopes).

See also
  pop
  push

Definition at line 65 of file Solver.java.

66 {
67 return Native
68 .solverGetNumScopes(getContext().nCtx(), getNativeObject());
69 }

## ◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions | ( |  | ) |
| inline

Retrieves parameter descriptions for solver.

Exceptions

  Z3Exception |

Definition at line 54 of file Solver.java.

55 {
56 return new ParamDescrs(getContext(), Native.solverGetParamDescrs(
57 getContext().nCtx(), getNativeObject()));
58 }

## ◆ 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 313 of file Solver.java.

314 {
315 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
316 if (x == 0) {
317 return null;
318 } else {
319 return Expr.create(getContext(), x);
320 }
321 }

## ◆ getReasonUnknown()

String getReasonUnknown | ( |  | ) |
| inline

A brief justification of why the last call to `Check` returned `UNKNOWN`.

Definition at line 343 of file Solver.java.

344 {
345 return Native.solverGetReasonUnknown(getContext().nCtx(),
346 getNativeObject());
347 }

## ◆ getStatistics()

Statistics getStatistics | ( |  | ) |
| inline

Solver statistics.

Exceptions

  Z3Exception |

Definition at line 362 of file Solver.java.

363 {
364 return new Statistics(getContext(), Native.solverGetStatistics(
365 getContext().nCtx(), getNativeObject()));
366 }

## ◆ 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 332 of file Solver.java.

333 {
334
335 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
336 return core.ToBoolExprArray();
337 }

## ◆ interrupt()

void interrupt | ( |  | ) |
| inline

Interrupt the execution of the solver object. Remarks: This ensures that the interrupt applies only to the given solver object and it applies only if it is running.

Definition at line 116 of file Solver.java.

117 {
118 Native.solverInterrupt(getContext().nCtx(), getNativeObject());
119 }

## ◆ pop() [1/2]

void pop | ( |  | ) |
| inline

Backtracks one backtracking point. Remarks: .

Definition at line 84 of file Solver.java.

85 {
86 pop(1);
87 }
com.microsoft.z3.Solver.pop
void pop()
Definition: Solver.java: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 96 of file Solver.java.

97 {
98 Native.solverPop(getContext().nCtx(), getNativeObject(), n);
99 }

## ◆ push()

void push | ( |  | ) |
| inline

Creates a backtracking point.

See also
  pop

Definition at line 75 of file Solver.java.

76 {
77 Native.solverPush(getContext().nCtx(), getNativeObject());
78 }

## ◆ reset()

void reset | ( |  | ) |
| inline

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

Definition at line 106 of file Solver.java.

107 {
108 Native.solverReset(getContext().nCtx(), getNativeObject());
109 }

## ◆ setParameters()

void setParameters | ( | Params | value | ) |
| inline

Sets the solver parameters.

Exceptions

  Z3Exception |

Definition at line 42 of file Solver.java.

43 {
44 getContext().checkContextMatch(value);
45 Native.solverSetParams(getContext().nCtx(), getNativeObject(),
46 value.getNativeObject());
47 }

## ◆ toString()

String toString | ( |  | ) |
| inline

A string representation of the solver.

Definition at line 372 of file Solver.java.

373 {
374 return Native
375 .solverToString(getContext().nCtx(), getNativeObject());
376 }

## ◆ translate()

Solver translate | ( | Context | ctx | ) |
| inline

Create a clone of the current solver with respect to`ctx`.

Definition at line 352 of file Solver.java.

353 {
354 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
355 }

Referenced by AstRef.__copy__(), Goal.__copy__(), AstVector.__copy__(), FuncInterp.__copy__(), ModelRef.__copy__(), Solver.__copy__(), Goal.__deepcopy__(), AstVector.__deepcopy__(), FuncInterp.__deepcopy__(), ModelRef.__deepcopy__(), and Solver.__deepcopy__().