From d540d881ef3d0d701e91ae8d7170ed2d74b529fa Mon Sep 17 00:00:00 2001 From: Alper Altuntas Date: Thu, 30 Nov 2023 09:35:08 -0700 Subject: [PATCH] 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. --- src/api/python/z3/z3.py | 7 +++++++ 1 file changed, 7 insertions(+) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index d029769e064..7551d8a2024 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -6955,6 +6955,13 @@ def __del__(self): 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) + def __enter__(self): + self.push() + return self + + def __exit__(self, *exc_info): + self.pop() + def set(self, *args, **keys): """Set a configuration option. The method `help()` return a string containing all available options.