From 902c683b92ce332a072cf75a644023f39de29c02 Mon Sep 17 00:00:00 2001 From: Nikolaj Bjorner Date: Mon, 29 Jul 2019 07:54:47 +0800 Subject: [PATCH] expose _get_ctx for scope semantics of newer versions of python #2441 Signed-off-by: Nikolaj Bjorner --- src/api/python/z3/z3.py | 3 +++ src/api/python/z3/z3rcf.py | 12 ++++++------ 2 files changed, 9 insertions(+), 6 deletions(-) diff --git a/src/api/python/z3/z3.py b/src/api/python/z3/z3.py index cd3253495..594d19d05 100644 --- a/src/api/python/z3/z3.py +++ b/src/api/python/z3/z3.py @@ -236,6 +236,9 @@ def _get_ctx(ctx): else: return ctx +def get_ctx(ctx): + return _get_ctx(ctx) + def set_param(*args, **kws): """Set Z3 global (or module) parameters. diff --git a/src/api/python/z3/z3rcf.py b/src/api/python/z3/z3rcf.py index 9d6f2f6ad..76d22bbca 100644 --- a/src/api/python/z3/z3rcf.py +++ b/src/api/python/z3/z3rcf.py @@ -21,21 +21,21 @@ def _to_rcfnum(num, ctx=None): return RCFNum(num, ctx) def Pi(ctx=None): - ctx = z3._get_ctx(ctx) + ctx = z3.get_ctx(ctx) return RCFNum(Z3_rcf_mk_pi(ctx.ref()), ctx) def E(ctx=None): - ctx = z3._get_ctx(ctx) + ctx = z3.get_ctx(ctx) return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx) def MkInfinitesimal(name="eps", ctx=None): # Todo: remove parameter name. # For now, we keep it for backward compatibility. - ctx = z3._get_ctx(ctx) + ctx = z3.get_ctx(ctx) return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx) def MkRoots(p, ctx=None): - ctx = z3._get_ctx(ctx) + ctx = z3.get_ctx(ctx) num = len(p) _tmp = [] _as = (RCFNumObj * num)() @@ -55,9 +55,9 @@ class RCFNum: # TODO: add support for converting AST numeral values into RCFNum if isinstance(num, RCFNumObj): self.num = num - self.ctx = z3._get_ctx(ctx) + self.ctx = z3.get_ctx(ctx) else: - self.ctx = z3._get_ctx(ctx) + self.ctx = z3.get_ctx(ctx) self.num = Z3_rcf_mk_rational(self.ctx_ref(), str(num)) def __del__(self):