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

expose _get_ctx for scope semantics of newer versions of python #2441

Browse source 
Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
This commit is contained in:
Nikolaj Bjorner 2019-07-29 07:54:47 +08:00
parent 2bd8d3b485
commit 902c683b92
2 changed files with 9 additions and 6 deletions
Show stats Download patch file Download diff file Expand all files Collapse all files

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

@ -236,6 +236,9 @@ def _get_ctx(ctx):
else: else:
return ctx return ctx
def get_ctx(ctx):
return _get_ctx(ctx)
def set_param(*args, **kws): def set_param(*args, **kws):
"""Set Z3 global (or module) parameters. """Set Z3 global (or module) parameters.

12
src/api/python/z3/z3rcf.py
View file

@ -21,21 +21,21 @@ def _to_rcfnum(num, ctx=None):
return RCFNum(num, ctx) return RCFNum(num, ctx)
def Pi(ctx=None): def Pi(ctx=None):
ctx = z3._get_ctx(ctx) ctx = z3.get_ctx(ctx)
return RCFNum(Z3_rcf_mk_pi(ctx.ref()), ctx) return RCFNum(Z3_rcf_mk_pi(ctx.ref()), ctx)
def E(ctx=None): def E(ctx=None):
ctx = z3._get_ctx(ctx) ctx = z3.get_ctx(ctx)
return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx) return RCFNum(Z3_rcf_mk_e(ctx.ref()), ctx)
def MkInfinitesimal(name="eps", ctx=None): def MkInfinitesimal(name="eps", ctx=None):
# Todo: remove parameter name. # Todo: remove parameter name.
# For now, we keep it for backward compatibility. # 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) return RCFNum(Z3_rcf_mk_infinitesimal(ctx.ref()), ctx)
def MkRoots(p, ctx=None): def MkRoots(p, ctx=None):
ctx = z3._get_ctx(ctx) ctx = z3.get_ctx(ctx)
num = len(p) num = len(p)
_tmp = [] _tmp = []
_as = (RCFNumObj * num)() _as = (RCFNumObj * num)()
@ -55,9 +55,9 @@ class RCFNum:
# TODO: add support for converting AST numeral values into RCFNum # TODO: add support for converting AST numeral values into RCFNum
if isinstance(num, RCFNumObj): if isinstance(num, RCFNumObj):
self.num = num self.num = num
self.ctx = z3._get_ctx(ctx) self.ctx = z3.get_ctx(ctx)
else: else:
self.ctx = z3._get_ctx(ctx) self.ctx = z3.get_ctx(ctx)
self.num = Z3_rcf_mk_rational(self.ctx_ref(), str(num)) self.num = Z3_rcf_mk_rational(self.ctx_ref(), str(num))
def __del__(self): def __del__(self):