mirrors/z3
3
0
Fork 0
mirror of https://github.com/Z3Prover/z3 synced 2025-04-27 02:45:51 +00:00
Code Activity

Fixed error handlers in Python API.

Browse source
This commit is contained in:
Christoph M. Wintersteiger 2017-11-08 20:09:09 +00:00
parent bec6c3f9e2
commit 17bcb37cf1
2 changed files with 20 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

20
scripts/update_api.py
View file

@ -324,14 +324,16 @@ class Elementaries:
self.OK = Z3_OK
self.Exception = Z3Exception
def Check(self, ctx):
def Check(self, ctx):
err = self.get_error_code(ctx)
if err != self.OK:
raise self.Exception(self.get_error_message(ctx, err))
def Z3_set_error_handler(ctx, hndlr, _elems=Elementaries(_lib.Z3_set_error_handler)):
_elems.f(ctx, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)(hndlr))
ceh = _error_handler_type(hndlr)
_elems.f(ctx, ceh)
_elems.Check(ctx)
return ceh
""")
@ -1637,10 +1639,10 @@ from .z3consts import *
_ext = 'dll' if sys.platform in ('win32', 'cygwin') else 'dylib' if sys.platform == 'darwin' else 'so'
_lib = None
_default_dirs = ['.',
os.path.dirname(os.path.abspath(__file__)),
pkg_resources.resource_filename('z3', 'lib'),
os.path.join(sys.prefix, 'lib'),
_default_dirs = ['.',
os.path.dirname(os.path.abspath(__file__)),
pkg_resources.resource_filename('z3', 'lib'),
os.path.join(sys.prefix, 'lib'),
None]
_all_dirs = []
@ -1667,7 +1669,7 @@ for d in _all_dirs:
if os.path.isdir(d):
d = os.path.join(d, 'libz3.%s' % _ext)
if os.path.isfile(d):
_lib = ctypes.CDLL(d)
_lib = ctypes.CDLL(d)
break
except:
pass
@ -1710,8 +1712,10 @@ else:
else:
return ""
_error_handler_type = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
_lib.Z3_set_error_handler.restype = None
_lib.Z3_set_error_handler.argtypes = [ContextObj, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)]
_lib.Z3_set_error_handler.argtypes = [ContextObj, _error_handler_type]
"""
)

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

@ -125,11 +125,6 @@ def _get_args(args):
except: # len is not necessarily defined when args is not a sequence (use reflection?)
return args
def z3_error_handler(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
def _to_param_value(val):
if isinstance(val, bool):
if val == True:
@ -139,6 +134,11 @@ def _to_param_value(val):
else:
return str(val)
def z3_error_handler(c, e):
# Do nothing error handler, just avoid exit(0)
# The wrappers in z3core.py will raise a Z3Exception if an error is detected
return
class Context:
"""A Context manages all other Z3 objects, global configuration options, etc.
@ -165,13 +165,14 @@ class Context:
Z3_set_param_value(conf, str(prev), _to_param_value(a))
prev = None
self.ctx = Z3_mk_context_rc(conf)
self.eh = Z3_set_error_handler(self.ctx, z3_error_handler)
Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
Z3_set_error_handler(self.ctx, z3_error_handler)
Z3_del_config(conf)
def __del__(self):
Z3_del_context(self.ctx)
Z3_del_context(self.ctx)
self.ctx = None
self.eh = None
def ref(self):
"""Return a reference to the actual C pointer to the Z3 context."""