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)
 
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 ()
 
Model getModel ()
 
Expr getProof ()
 
BoolExpr[] getUnsatCore ()
 
String getReasonUnknown ()
 
Solver translate (Context ctx)
 
Statistics getStatistics ()
 
String toString ()
 

Detailed Description

Solvers.

Definition at line 26 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 114 of file Solver.java.

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

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

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

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

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

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

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

251 {
252 return check((Expr[]) null);
253 }

Referenced by Solver.check().

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

222 {
223 Z3_lbool r;
224 if (assumptions == null) {
225 r = Z3_lbool.fromInt(Native.solverCheck(getContext().nCtx(),
226 getNativeObject()));
227 } else {
228 r = Z3_lbool.fromInt(Native.solverCheckAssumptions(getContext()
229 .nCtx(), getNativeObject(), assumptions.length, AST
230 .arrayToNative(assumptions)));
231 }
232 switch (r)
233 {
234 case Z3_L_TRUE:
235 return Status.SATISFIABLE;
236 case Z3_L_FALSE:
237 return Status.UNSATISFIABLE;
238 default:
239 return Status.UNKNOWN;
240 }
241 }
Z3_lbool
Lifted Boolean type: false, undefined, true.
Definition: z3_api.h:100
@ Z3_L_TRUE
Definition: z3_api.h:103
@ Z3_L_FALSE
Definition: z3_api.h:101

◆ fromFile()

void fromFile ( String  file)
inline

Load solver assertions from a file.

Definition at line 178 of file Solver.java.

179 {
180 Native.solverFromFile(getContext().nCtx(), getNativeObject(), file);
181 }

◆ fromString()

void fromString ( String  str)
inline

Load solver assertions from a string.

Definition at line 186 of file Solver.java.

187 {
188 Native.solverFromString(getContext().nCtx(), getNativeObject(), str);
189 }

◆ getAssertions()

BoolExpr[] getAssertions ( )
inline

The set of asserted formulas.

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.ToBoolExprArray();
212 }

◆ getHelp()

String getHelp ( )
inline

A string that describes all available solver parameters.

Definition at line 30 of file Solver.java.

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

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

265 {
266 long x = Native.solverGetModel(getContext().nCtx(), getNativeObject());
267 if (x == 0) {
268 return null;
269 } else {
270 return new Model(getContext(), x);
271 }
272 }
def Model(ctx=None)
Definition: z3py.py:6236

◆ getNumAssertions()

int getNumAssertions ( )
inline

The number of assertions in the solver.

Exceptions
Z3Exception

Definition at line 197 of file Solver.java.

198 {
199 ASTVector assrts = new ASTVector(getContext(), Native.solverGetAssertions(getContext().nCtx(), getNativeObject()));
200 return assrts.size();
201 }

◆ getNumScopes()

int getNumScopes ( )
inline

The current number of backtracking points (scopes).

See also
pop
push

Definition at line 63 of file Solver.java.

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

◆ getParameterDescriptions()

ParamDescrs getParameterDescriptions ( )
inline

Retrieves parameter descriptions for solver.

Exceptions
Z3Exception

Definition at line 52 of file Solver.java.

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

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

284 {
285 long x = Native.solverGetProof(getContext().nCtx(), getNativeObject());
286 if (x == 0) {
287 return null;
288 } else {
289 return Expr.create(getContext(), x);
290 }
291 }

◆ getReasonUnknown()

String getReasonUnknown ( )
inline

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

Definition at line 313 of file Solver.java.

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

◆ getStatistics()

Statistics getStatistics ( )
inline

Solver statistics.

Exceptions
Z3Exception

Definition at line 332 of file Solver.java.

333 {
334 return new Statistics(getContext(), Native.solverGetStatistics(
335 getContext().nCtx(), getNativeObject()));
336 }

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

303 {
304
305 ASTVector core = new ASTVector(getContext(), Native.solverGetUnsatCore(getContext().nCtx(), getNativeObject()));
306 return core.ToBoolExprArray();
307 }

◆ pop() [1/2]

void pop ( )
inline

Backtracks one backtracking point. Remarks: .

Definition at line 82 of file Solver.java.

83 {
84 pop(1);
85 }

Referenced by Solver.pop().

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

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

◆ push()

void push ( )
inline

Creates a backtracking point.

See also
pop

Definition at line 73 of file Solver.java.

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

◆ reset()

void reset ( )
inline

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

Definition at line 104 of file Solver.java.

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

◆ setParameters()

void setParameters ( Params  value)
inline

Sets the solver parameters.

Exceptions
Z3Exception

Definition at line 40 of file Solver.java.

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

◆ toString()

String toString ( )
inline

A string representation of the solver.

Definition at line 342 of file Solver.java.

343 {
344 return Native
345 .solverToString(getContext().nCtx(), getNativeObject());
346 }

◆ translate()

Solver translate ( Context  ctx)
inline

Create a clone of the current solver with respect toctx.

Definition at line 322 of file Solver.java.

323 {
324 return new Solver(ctx, Native.solverTranslate(getContext().nCtx(), getNativeObject(), ctx.nCtx()));
325 }

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