Fixed problems arising from unfortunate object destruction order in the Python API. Fixes #989.

scripts/update_api.py

@@ -311,8 +311,30 @@ def display_args_to_z3(params):
             core_py.write("a%s" % i)
         i = i + 1
 
+NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
+Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
+
 def mk_py_wrappers():
-    core_py.write("\n")
+    core_py.write("""
+class Elementaries:
+  def __init__(self, f):
+    self.f = f
+    self.get_error_code = _lib.Z3_get_error_code
+    self.get_error_message = _lib.Z3_get_error_msg
+    self.OK = Z3_OK
+    self.Exception = Z3Exception
+
+  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))
+  _elems.Check(ctx)
+
+""")
+
     for sig in _API2PY:
         name   = sig[0]
         result = sig[1]
@@ -320,25 +342,20 @@ def mk_py_wrappers():
         num    = len(params)
         core_py.write("def %s(" % name)
         display_args(num)
-        core_py.write("):\n")
+        comma = ", " if num != 0 else ""
-        core_py.write("  _lib = lib()\n")
+        core_py.write("%s_elems=Elementaries(_lib.%s)):\n" % (comma, name))
-        core_py.write("  if _lib is None or _lib.%s is None:\n" % name)
+        lval = "r = " if result != VOID else ""
-        core_py.write("     return\n")
+        core_py.write("  %s_elems.f(" % lval)
-        if result != VOID:
-            core_py.write("  r = _lib.%s(" % name)
-        else:
-            core_py.write("  _lib.%s(" % name)
         display_args_to_z3(params)
         core_py.write(")\n")
-        if len(params) > 0 and param_type(params[0]) == CONTEXT:
+        if len(params) > 0 and param_type(params[0]) == CONTEXT and not name in Unwrapped:
-            core_py.write("  err = _lib.Z3_get_error_code(a0)\n")
+            core_py.write("  _elems.Check(a0)\n")
-            core_py.write("  if err != Z3_OK:\n")
-            core_py.write("    raise Z3Exception(_lib.Z3_get_error_msg(a0, err))\n")
         if result == STRING:
             core_py.write("  return _to_pystr(r)\n")
         elif result != VOID:
             core_py.write("  return r\n")
         core_py.write("\n")
+    core_py
 
 
 ## .NET API native interface
@@ -391,10 +408,6 @@ def mk_dotnet(dotnet):
         dotnet.write(');\n\n')
     dotnet.write('        }\n')
 
-
-NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc', 'Z3_mk_interpolation_context' ]
-Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ]
-
 def mk_dotnet_wrappers(dotnet):
     global Type2Str
     dotnet.write("\n")
@@ -1605,35 +1618,71 @@ def write_exe_c_preamble(exe_c):
 
 def write_core_py_post(core_py):
   core_py.write("""
-
+# Clean up
+del _lib
+del _default_dirs
+del _all_dirs
+del _ext
 """)
     
 def write_core_py_preamble(core_py):
-  core_py.write('# Automatically generated file\n')
-  core_py.write('import sys, os\n')
-  core_py.write('import ctypes\n')
-  core_py.write('import pkg_resources\n')
-  core_py.write('from .z3types import *\n')
-  core_py.write('from .z3consts import *\n')
   core_py.write(
 """
+# Automatically generated file
+import sys, os
+import ctypes
+import pkg_resources
+from .z3types import *
+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'),                  
+                 None]
+_all_dirs = []
 
-def lib():
+if sys.version < '3':
-  global _lib
+  import __builtin__
-  if _lib is None:
+  if hasattr(__builtin__, "Z3_LIB_DIRS"):
-     _dirs = ['.', os.path.dirname(os.path.abspath(__file__)), pkg_resources.resource_filename('z3', 'lib'), os.path.join(sys.prefix, 'lib'), None]
+    _all_dirs = __builtin__.Z3_LIB_DIRS
-     for _dir in _dirs:
+else:
+  import builtins
+  if hasattr(builtins, "Z3_LIB_DIRS"):
+    _all_dirs = builtins.Z3_LIB_DIRS
+
+if 'Z3_LIBRARY_PATH' in os.environ:
+  lp = os.environ['Z3_LIBRARY_PATH'];
+  lds = lp.split(';') if sys.platform in ('win32') else lp.split(':')
+  _all_dirs.extend(lds)
+
+_all_dirs.extend(_default_dirs)
+
+for d in _all_dirs:
   try:
-          init(_dir)
+    d = os.path.realpath(d)
+    if os.path.isdir(d):
+      d = os.path.join(d, 'libz3.%s' % _ext)
+      if os.path.isfile(d):
+        _lib = ctypes.CDLL(d)              
         break
   except:
     pass
+
 if _lib is None:
-    raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python")
+  print("Could not find libz3.%s; consider adding the directory containing it to" % _ext)
-  return _lib
+  print("  - your system's PATH environment variable,")
+  print("  - the Z3_LIBRARY_PATH environment variable, or ")
+  print("  - to the custom Z3_LIBRARY_DIRS Python-builtin before importing the z3 module, e.g. via")
+  if sys.version < '3':
+    print("    import __builtin__")
+    print("    __builtin__.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+  else:
+    print("    import builtins")
+    print("    builtins.Z3_LIB_DIRS = [ '/path/to/libz3.%s' ] " % _ext)
+  raise Z3Exception("libz3.%s not found." % _ext)
 
 def _to_ascii(s):
   if isinstance(s, str):
@@ -1653,16 +1702,9 @@ else:
      else:
         return ""
 
-def init(PATH):
+_lib.Z3_set_error_handler.restype  = None
-  if PATH:
+_lib.Z3_set_error_handler.argtypes = [ContextObj, ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)]
-    PATH = os.path.realpath(PATH)
-    if os.path.isdir(PATH):
-      PATH = os.path.join(PATH, 'libz3.%s' % _ext)
-  else:
-    PATH = 'libz3.%s' % _ext
 
-  global _lib
-  _lib = ctypes.CDLL(PATH)
 """
   )
 

src/api/python/z3/z3.py

@@ -112,8 +112,6 @@ def _symbol2py(ctx, s):
     else:
         return Z3_get_symbol_string(ctx.ref(), s)
 
-_error_handler_fptr = ctypes.CFUNCTYPE(None, ctypes.c_void_p, ctypes.c_uint)
-
 # Hack for having nary functions that can receive one argument that is the
 # list of arguments.
 def _get_args(args):
@@ -127,13 +125,11 @@ def _get_args(args):
     except:  # len is not necessarily defined when args is not a sequence (use reflection?)
         return args
 
-def _Z3python_error_handler_core(c, e):
+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
 
-_Z3Python_error_handler = _error_handler_fptr(_Z3python_error_handler_core)
-
 def _to_param_value(val):
     if isinstance(val, bool):
         if val == True:
@@ -168,16 +164,13 @@ class Context:
             else:
                 Z3_set_param_value(conf, str(prev), _to_param_value(a))
                 prev = None
-        self.lib = lib()
         self.ctx = Z3_mk_context_rc(conf)
         Z3_set_ast_print_mode(self.ctx, Z3_PRINT_SMTLIB2_COMPLIANT)
-        lib().Z3_set_error_handler.restype  = None
+        Z3_set_error_handler(self.ctx, z3_error_handler)
-        lib().Z3_set_error_handler.argtypes = [ContextObj, _error_handler_fptr]
-        lib().Z3_set_error_handler(self.ctx, _Z3Python_error_handler)
         Z3_del_config(conf)
 
     def __del__(self):
-        self.lib.Z3_del_context(self.ctx)
+        Z3_del_context(self.ctx)
         self.ctx = None
 
     def ref(self):