mirror of
https://github.com/Z3Prover/z3
synced 2025-04-12 12:08:18 +00:00
Add __enter__ and __exit__ methods to Solver class (#7025)
To enable the usage of the with statement for the Solver class instances, this commit adds __enter__ and __exit__ methods. The with statement should offer a more concise and safer alternative to explicit usage of push() and pop() methods.
This commit is contained in:
parent
26440ed3d8
commit
d540d881ef
|
@ -6955,6 +6955,13 @@ class Solver(Z3PPObject):
|
||||||
if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
|
if self.solver is not None and self.ctx.ref() is not None and Z3_solver_dec_ref is not None:
|
||||||
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
|
Z3_solver_dec_ref(self.ctx.ref(), self.solver)
|
||||||
|
|
||||||
|
def __enter__(self):
|
||||||
|
self.push()
|
||||||
|
return self
|
||||||
|
|
||||||
|
def __exit__(self, *exc_info):
|
||||||
|
self.pop()
|
||||||
|
|
||||||
def set(self, *args, **keys):
|
def set(self, *args, **keys):
|
||||||
"""Set a configuration option.
|
"""Set a configuration option.
|
||||||
The method `help()` return a string containing all available options.
|
The method `help()` return a string containing all available options.
|
||||||
|
|
Loading…
Reference in a new issue