Z3
Data Structures | 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 30 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 128 of file Solver.java.

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

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

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

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

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

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

259  {
260  return check((Expr[]) null);
261  }

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

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

◆ fromFile()

void fromFile ( String  file)
inline

Load solver assertions from a file.

Definition at line 192 of file Solver.java.

193  {
194  Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
195  }

◆ fromString()

void fromString ( String  str)
inline

Load solver assertions from a string.

Definition at line 200 of file Solver.java.

201  {
202  Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
203  }

◆ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Exceptions
Z3Exception

Definition at line 222 of file Solver.java.

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

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

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

◆ getHelp()

String getHelp ( )
inline

A string that describes all available solver parameters.

Definition at line 34 of file Solver.java.

35  {
36  return Native.solverGetHelp(getContext().nCtx(), getNativeObject());
37  }

◆ 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
Used to signify a satisfiable status.

, or if model production is not enabled.

Exceptions
Z3Exception

Definition at line 296 of file Solver.java.

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

◆ getNumAssertions()

int getNumAssertions ( )
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 211 of file Solver.java.

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

◆ getNumScopes()

int getNumScopes ( )
inline

The current number of backtracking points (scopes).

See also
pop
push

Definition at line 67 of file Solver.java.

68  {
69  return Native
70  .solverGetNumScopes(getContext().nCtx(), getNativeObject());
71  }

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for solver.

Exceptions
Z3Exception

Definition at line 56 of file Solver.java.

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

◆ 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
Used to signify an unsatisfiable status.

, or if proof production is disabled.

Exceptions
Z3Exception

Definition at line 315 of file Solver.java.

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

◆ getReasonUnknown()

String getReasonUnknown ( )
inline

A brief justification of why the last call to

Check

returned

@ UNKNOWN
Used to signify an unknown status.

.

Definition at line 345 of file Solver.java.

346  {
347  return Native.solverGetReasonUnknown(getContext().nCtx(),
348  getNativeObject());
349  }

◆ getStatistics()

Statistics getStatistics ( )
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 364 of file Solver.java.

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

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

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

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

119  {
120  Native.solverInterrupt(getContext().nCtx(), getNativeObject());
121  }

◆ pop() [1/2]

void pop ( )
inline

Backtracks one backtracking point. Remarks: .

Definition at line 86 of file Solver.java.

87  {
88  pop(1);
89  }

Referenced by Solver.__exit__().

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

99  {
100  Native.solverPop(getContext().nCtx(), getNativeObject(), n);
101  }

Referenced by Solver.__exit__().

◆ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 77 of file Solver.java.

78  {
79  Native.solverPush(getContext().nCtx(), getNativeObject());
80  }

Referenced by Solver.__enter__().

◆ reset()

void reset ( )
inline

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

Definition at line 108 of file Solver.java.

109  {
110  Native.solverReset(getContext().nCtx(), getNativeObject());
111  }

◆ setParameters()

void setParameters ( Params  value)
inline

Sets the solver parameters.

Exceptions
Z3Exception

Definition at line 44 of file Solver.java.

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

◆ toString()

String toString ( )
inline

A string representation of the solver.

Definition at line 374 of file Solver.java.

375  {
376  return Native
377  .solverToString(getContext().nCtx(), getNativeObject());
378  }

◆ translate()

Solver translate ( Context  ctx)
inline

Create a clone of the current solver with respect to

ctx

.

Definition at line 354 of file Solver.java.

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

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__().