mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-12 12:08:18 +00:00
Code Activity

Add __enter__ and __exit__ methods on Optimize class (#7477)

Browse source 
This enables the use of the with statement for the Optimize class to
concisely call push() and pop(). This works similarly to the Solver
class.
This commit is contained in:
Oskar Haarklou Veileborg 2024-12-13 18:19:04 +01:00 committed by GitHub
parent 1e5c59a06f
commit b4295620b3
No known key found for this signature in database
GPG key ID: B5690EEEBB952194
1 changed files with 7 additions and 0 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

7
src/api/python/z3/z3.py
View file

@ -7991,6 +7991,13 @@ class Optimize(Z3PPObject):
if self._on_models_id is not None: if self._on_models_id is not None:
del _on_models[self._on_models_id] del _on_models[self._on_models_id]
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.