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 (BoolExpr... constraints)
 
void assertAndTrack (BoolExpr[] constraints, BoolExpr[] ps)
 
void assertAndTrack (BoolExpr constraint, BoolExpr 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 ()
 
Status check (Expr... assumptions)
 
Status check ()
 
Status getConsequences (BoolExpr[] assumptions, Expr[] variables, List< BoolExpr > 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 27 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 125 of file Solver.java.

126  {
127  getContext().checkContextMatch(constraints);
128  for (BoolExpr a : constraints)
129  {
130  Native.solverAssert(getContext().nCtx(), getNativeObject(),
131  a.getNativeObject());
132  }
133  }

◆ assertAndTrack() [1/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 177 of file Solver.java.

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

◆ assertAndTrack() [2/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 150 of file Solver.java.

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

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

254  {
255  return check((Expr[]) null);
256  }

◆ check() [2/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 232 of file Solver.java.

233  {
234  Z3_lbool r;
235  if (assumptions == null) {
236  r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
237  getNativeObject()));
238  } else {
239  r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
240  .nCtx(), getNativeObject(), assumptions.length, AST
241  .arrayToNative(assumptions)));
242  }
243  return lboolToStatus(r);
244  }

◆ fromFile()

void fromFile ( String  file)
inline

Load solver assertions from a file.

Definition at line 189 of file Solver.java.

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

◆ fromString()

void fromString ( String  str)
inline

Load solver assertions from a string.

Definition at line 197 of file Solver.java.

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

◆ getAssertions()

BoolExpr [] getAssertions ( )
inline

The set of asserted formulas.

Exceptions
Z3Exception

Definition at line 219 of file Solver.java.

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

◆ getConsequences()

Status getConsequences ( BoolExpr[]  assumptions,
Expr[]  variables,
List< BoolExpr 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 269 of file Solver.java.

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

◆ getHelp()

String getHelp ( )
inline

A string that describes all available solver parameters.

Definition at line 31 of file Solver.java.

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

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

292  {
293  long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
294  if (x == 0) {
295  return null;
296  } else {
297  return new Model(getContext(), x);
298  }
299  }

◆ getNumAssertions()

int getNumAssertions ( )
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 208 of file Solver.java.

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

◆ getNumScopes()

int getNumScopes ( )
inline

The current number of backtracking points (scopes).

See also
pop
push

Definition at line 64 of file Solver.java.

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

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for solver.

Exceptions
Z3Exception

Definition at line 53 of file Solver.java.

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

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

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

◆ getReasonUnknown()

String getReasonUnknown ( )
inline

A brief justification of why the last call to

Check

returned

UNKNOWN

.

Definition at line 340 of file Solver.java.

341  {
342  return Native.solverGetReasonUnknown(getContext().nCtx(),
343  getNativeObject());
344  }

◆ getStatistics()

Statistics getStatistics ( )
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 359 of file Solver.java.

360  {
361  return new Statistics(getContext(), Native.solverGetStatistics(
362  getContext().nCtx(), getNativeObject()));
363  }

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

330  {
331 
332  ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
333  return core.ToBoolExprArray();
334  }

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

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

◆ pop() [1/2]

void pop ( )
inline

Backtracks one backtracking point. Remarks: .

Definition at line 83 of file Solver.java.

84  {
85  pop(1);
86  }

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

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

◆ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 74 of file Solver.java.

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

◆ reset()

void reset ( )
inline

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

Definition at line 105 of file Solver.java.

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

◆ setParameters()

void setParameters ( Params  value)
inline

Sets the solver parameters.

Exceptions
Z3Exception

Definition at line 41 of file Solver.java.

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

◆ toString()

String toString ( )
inline

A string representation of the solver.

Definition at line 369 of file Solver.java.

370  {
371  return Native
372  .solverToString(getContext().nCtx(), getNativeObject());
373  }

◆ translate()

Solver translate ( Context  ctx)
inline

Create a clone of the current solver with respect to

ctx

.

Definition at line 349 of file Solver.java.

350  {
351  return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
352  }
com.microsoft.z3.Solver.check
Status check()
Definition: Solver.java:253
Z3_lbool
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
com.microsoft.z3.Solver.pop
void pop()
Definition: Solver.java:83
z3py.Model
def Model(ctx=None)
Definition: z3py.py:6259