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 }

◆ 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
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 }
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 }

◆ 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 toctx.

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