From e2546d2b95820bea9071f2f1235a019c99507a45 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 7 Dec 2015 06:51:00 +0000 Subject: [PATCH 1/8] Refactor references to ``pythonPkgDirWithoutPrefix`` to a object attribute. --- scripts/mk_util.py | 20 +++++++++----------- 1 file changed, 9 insertions(+), 11 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8c109136d..100199156 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1344,27 +1344,26 @@ class DLLComponent(Component): class PythonInstallComponent(Component): def __init__(self, name): Component.__init__(self, name, None, []) + self.pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) def main_component(self): return False def install_deps(self, out): if not is_python_install_enabled(): - return - pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) - MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix) + return + MakeRuleCmd.make_install_directory(out, self.pythonPkgDirWithoutPrefix) def mk_install(self, out): if not is_python_install_enabled(): return - pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) - MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix) + MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDirWithoutPrefix) if sys.version >= "3": - pythonPycacheDir = os.path.join(pythonPkgDirWithoutPrefix, '__pycache__') + pythonPycacheDir = os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__') MakeRuleCmd.make_install_directory(out, pythonPycacheDir) MakeRuleCmd.install_files(out, '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), pythonPycacheDir) else: - MakeRuleCmd.install_files(out, 'z3*.pyc', pythonPkgDirWithoutPrefix) + MakeRuleCmd.install_files(out, 'z3*.pyc', self.pythonPkgDirWithoutPrefix) if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): if os.uname()[0] == 'Darwin': LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH" @@ -1377,10 +1376,9 @@ class PythonInstallComponent(Component): def mk_uninstall(self, out): if not is_python_install_enabled(): return - pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) - MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3'))) - MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, 'z3'))) - MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(pythonPkgDirWithoutPrefix, '__pycache__', 'z3'))) + MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) + MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) + MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__', 'z3'))) def mk_makefile(self, out): return From 38b45919b55617801d6297e1f32d60523479e71d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 7 Dec 2015 07:38:24 +0000 Subject: [PATCH 2/8] Unbreak running ``make install``. The python ``site-package`` directory was not created before trying to create files in it. The ``install_deps()`` method was also dead. It looks like that should have been named ``mk_install_deps()`` but even if we give it the right name it does the wrong thing. That method is supposed emit target names (i.e. dependencies) not commands. --- scripts/mk_util.py | 10 +++++----- 1 file changed, 5 insertions(+), 5 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 100199156..9c3bae270 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1300,9 +1300,13 @@ class DLLComponent(Component): dllfile = '%s$(SO_EXT)' % self.dll_name dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile) MakeRuleCmd.install_files(out, dllfile, dllInstallPath) + # FIXME: This belongs in ``PythonInstallComponent`` but + # it currently doesn't have access to this component so + # it can't emit these rules if not is_python_install_enabled(): return pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) + MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix) if IS_WINDOWS: MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile)) else: @@ -1349,14 +1353,10 @@ class PythonInstallComponent(Component): def main_component(self): return False - def install_deps(self, out): - if not is_python_install_enabled(): - return - MakeRuleCmd.make_install_directory(out, self.pythonPkgDirWithoutPrefix) - def mk_install(self, out): if not is_python_install_enabled(): return + MakeRuleCmd.make_install_directory(out, self.pythonPkgDirWithoutPrefix) MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDirWithoutPrefix) if sys.version >= "3": pythonPycacheDir = os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__') From 0a8cd3ae191e30c9335cbd7cd7d88cb3b9f4b6f0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 7 Dec 2015 11:03:08 +0000 Subject: [PATCH 3/8] Refactor the install and uninstall commands for the python bindings out of ``DLLComponent`` and into ``PythonInstallComponent`` where they belong. --- scripts/mk_project.py | 12 +++---- scripts/mk_util.py | 78 ++++++++++++++++++++++++++----------------- 2 files changed, 53 insertions(+), 37 deletions(-) diff --git a/scripts/mk_project.py b/scripts/mk_project.py index a9aaa9791..eb7218d4b 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -81,17 +81,17 @@ def init_project_def(): includes2install=['z3.h', 'z3_v1.h', 'z3_macros.h'] + API_files) add_exe('shell', ['api', 'sat', 'extra_cmds','opt'], exe_name='z3') add_exe('test', ['api', 'fuzzing', 'simplex'], exe_name='test-z3', install=False) - add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', - reexports=['api'], - dll_name='libz3', - static=build_static_lib(), - export_files=API_files) + _libz3Component = add_dll('api_dll', ['api', 'sat', 'extra_cmds'], 'api/dll', + reexports=['api'], + dll_name='libz3', + static=build_static_lib(), + export_files=API_files) add_dot_net_dll('dotnet', ['api_dll'], 'api/dotnet', dll_name='Microsoft.Z3', assembly_info_dir='Properties') add_java_dll('java', ['api_dll'], 'api/java', dll_name='libz3java', package_name="com.microsoft.z3", manifest_file='manifest') add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') - add_python_install() + add_python_install(_libz3Component) # Examples add_cpp_example('cpp_example', 'c++') add_cpp_example('z3_tptp', 'tptp') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9c3bae270..ca08c7804 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1210,11 +1210,23 @@ class DLLComponent(Component): else: return self.name + '$(SO_EXT)' + def dll_file(self): + """ + Return file name of component suitable for use in a Makefile + """ + return '%s$(SO_EXT)' % self.dll_name + + def install_path(self): + """ + Return install location of component (relative to prefix) + suitable for use in a Makefile + """ + return os.path.join(INSTALL_LIB_DIR, self.dll_file()) + def mk_makefile(self, out): Component.mk_makefile(self, out) # generate rule for (SO_EXT) - dllfile = '%s$(SO_EXT)' % self.dll_name - out.write('%s:' % dllfile) + out.write('%s:' % self.dll_file()) deps = sort_components(self.deps) objs = [] for cppfile in get_cpp_files(self.src_dir): @@ -1234,7 +1246,7 @@ class DLLComponent(Component): c_dep = get_component(dep) out.write(' ' + c_dep.get_link_name()) out.write('\n') - out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % dllfile) + out.write('\t$(LINK) $(SLINK_OUT_FLAG)%s $(SLINK_FLAGS)' % self.dll_file()) for obj in objs: out.write(' ') out.write(obj) @@ -1250,9 +1262,9 @@ class DLLComponent(Component): if self.static: self.mk_static(out) libfile = '%s$(LIB_EXT)' % self.dll_name - out.write('%s: %s %s\n\n' % (self.name, dllfile, libfile)) + out.write('%s: %s %s\n\n' % (self.name, self.dll_file(), libfile)) else: - out.write('%s: %s\n\n' % (self.name, dllfile)) + out.write('%s: %s\n\n' % (self.name, self.dll_file())) def mk_static(self, out): # generate rule for lib @@ -1297,34 +1309,13 @@ class DLLComponent(Component): def mk_install(self, out): if self.install: - dllfile = '%s$(SO_EXT)' % self.dll_name - dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile) - MakeRuleCmd.install_files(out, dllfile, dllInstallPath) - # FIXME: This belongs in ``PythonInstallComponent`` but - # it currently doesn't have access to this component so - # it can't emit these rules - if not is_python_install_enabled(): - return - pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) - MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix) - if IS_WINDOWS: - MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile)) - else: - # Create symbolic link to save space. - # It's important that this symbolic link be relative (rather - # than absolute) so that the install is relocatable (needed for - # staged installs that use DESTDIR). - MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile)) + MakeRuleCmd.install_files(out, self.dll_file(), self.install_path()) if self.static: libfile = '%s$(LIB_EXT)' % self.dll_name MakeRuleCmd.install_files(out, libfile, os.path.join(INSTALL_LIB_DIR, libfile)) def mk_uninstall(self, out): - dllfile = '%s$(SO_EXT)' % self.dll_name - MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile)) - if is_python_install_enabled(): - pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) - MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile)) + MakeRuleCmd.remove_installed_files(out, self.install_path()) libfile = '%s$(LIB_EXT)' % self.dll_name MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile)) @@ -1346,9 +1337,11 @@ class DLLComponent(Component): '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name)) class PythonInstallComponent(Component): - def __init__(self, name): + def __init__(self, name, libz3Component): + assert isinstance(libz3Component, DLLComponent) Component.__init__(self, name, None, []) self.pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) + self.libz3Component = libz3Component def main_component(self): return False @@ -1357,6 +1350,26 @@ class PythonInstallComponent(Component): if not is_python_install_enabled(): return MakeRuleCmd.make_install_directory(out, self.pythonPkgDirWithoutPrefix) + + # Sym-link or copy libz3 into python package directory + if IS_WINDOWS: + MakeRuleCmd.install_files(out, + self.libz3Component.dll_file(), + os.path.join(pythonPkgDirWithoutPrefix, + self.libz3Component.dll_file()) + ) + else: + # Create symbolic link to save space. + # It's important that this symbolic link be relative (rather + # than absolute) so that the install is relocatable (needed for + # staged installs that use DESTDIR). + MakeRuleCmd.create_relative_symbolic_link(out, + self.libz3Component.install_path(), + os.path.join(self.pythonPkgDirWithoutPrefix, + self.libz3Component.dll_file() + ) + ) + MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDirWithoutPrefix) if sys.version >= "3": pythonPycacheDir = os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__') @@ -1376,6 +1389,8 @@ class PythonInstallComponent(Component): def mk_uninstall(self, out): if not is_python_install_enabled(): return + MakeRuleCmd.remove_installed_files(out, os.path.join(self.pythonPkgDirWithoutPrefix, + self.libz3Component.dll_file())) MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__', 'z3'))) @@ -2007,6 +2022,7 @@ def add_extra_exe(name, deps=[], path=None, exe_name=None, install=True): def add_dll(name, deps=[], path=None, dll_name=None, export_files=[], reexports=[], install=True, static=False): c = DLLComponent(name, dll_name, path, deps, export_files, reexports, install, static) reg_component(name, c) + return c def add_dot_net_dll(name, deps=[], path=None, dll_name=None, assembly_info_dir=None): c = DotNetDLLComponent(name, dll_name, path, deps, assembly_info_dir) @@ -2016,9 +2032,9 @@ def add_java_dll(name, deps=[], path=None, dll_name=None, package_name=None, man c = JavaDLLComponent(name, dll_name, package_name, manifest_file, path, deps) reg_component(name, c) -def add_python_install(): +def add_python_install(libz3Component): name = 'python_install' - reg_component(name, PythonInstallComponent(name)) + reg_component(name, PythonInstallComponent(name, libz3Component)) def add_ml_lib(name, deps=[], path=None, lib_name=None): c = MLComponent(name, lib_name, path, deps) From d98d392aac860a98f71d7706291db7244e5d4ba4 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 7 Dec 2015 12:58:40 +0000 Subject: [PATCH 4/8] Try unbreak OSX build when Python installation doesn't live under PREFIX. In this case it is not safe to call ``strip_path_prefix()`` due to the assertion error it will raise. --- scripts/mk_util.py | 7 ++++++- 1 file changed, 6 insertions(+), 1 deletion(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ca08c7804..acaff3b78 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1340,8 +1340,13 @@ class PythonInstallComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) Component.__init__(self, name, None, []) - self.pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) + self.pythonPkgDirWithoutPrefix = None self.libz3Component = libz3Component + if PYTHON_INSTALL_ENABLED: + # Only safe to call this if we know that PYTHON_PACKAGE_DIR lives under PREFIX. + # Other parts of the code enforce that this is the case when ``PYTHON_INSTALL_ENABLED`` + # is True. + self.pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) def main_component(self): return False From edf5ed27dfd95c07aa6dc0c267e5bf2fa96398f8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Dec 2015 22:52:33 +0000 Subject: [PATCH 5/8] Attempt to allow (but warn about) installation of Python bindings under OSX when the Python ``site-packages`` directory doesn't live under the install prefix. Also disallow installing under Windows as it doesn't really make sense. --- scripts/mk_util.py | 134 +++++++++++++++++++++++++++++++++------------ 1 file changed, 98 insertions(+), 36 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index acaff3b78..183e70003 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -712,7 +712,9 @@ def parse_options(): display_help(1) # Handle the Python package directory if IS_WINDOWS: - PYTHON_INSTALL_ENABLED = True + # Installing under Windows doesn't make sense as the install prefix is used + # but that doesn't make sense under Windows + PYTHON_INSTALL_ENABLED = False else: if not PYTHON_PACKAGE_DIR.startswith(PREFIX): print(("Warning: The detected Python package directory (%s)" @@ -720,7 +722,14 @@ def parse_options(): ". This would lead to a broken Python installation." "Use --pypkgdir= to change the Python package directory") % (PYTHON_PACKAGE_DIR, PREFIX)) - PYTHON_INSTALL_ENABLED = False + if IS_OSX and PYTHON_PACKAGE_DIR.startswith('/Library/'): + print("Using hack to install Python bindings, this might lead to a broken system") + PYTHON_INSTALL_ENABLED = True + else: + print("Disabling install of Python bindings") + PYTHON_INSTALL_ENABLED = False + else: + PYTHON_INSTALL_ENABLED = True # Return a list containing a file names included using '#include' in # the given C/C++ file named fname. @@ -1340,13 +1349,26 @@ class PythonInstallComponent(Component): def __init__(self, name, libz3Component): assert isinstance(libz3Component, DLLComponent) Component.__init__(self, name, None, []) - self.pythonPkgDirWithoutPrefix = None + self.pythonPkgDir = None + self.in_prefix_install = True self.libz3Component = libz3Component - if PYTHON_INSTALL_ENABLED: - # Only safe to call this if we know that PYTHON_PACKAGE_DIR lives under PREFIX. - # Other parts of the code enforce that this is the case when ``PYTHON_INSTALL_ENABLED`` - # is True. - self.pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) + if not PYTHON_INSTALL_ENABLED: + return + + if self.is_osx_hack(): + # Use full path that is outside of install prefix + self.pythonPkgDir = PYTHON_PACKAGE_DIR + self.in_prefix_install = False + assert os.path.isabs(self.pythonPkgDir) + else: + # Use path inside the prefix (should be the normal case) + assert PYTHON_PACKAGE_DIR.startswith(PREFIX) + self.pythonPkgDir = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX) + assert not os.path.isabs(self.pythonPkgDir) + assert self.in_prefix_install + + def is_osx_hack(self): + return IS_OSX and not PYTHON_PACKAGE_DIR.startswith(PREFIX) def main_component(self): return False @@ -1354,14 +1376,15 @@ class PythonInstallComponent(Component): def mk_install(self, out): if not is_python_install_enabled(): return - MakeRuleCmd.make_install_directory(out, self.pythonPkgDirWithoutPrefix) + MakeRuleCmd.make_install_directory(out, self.pythonPkgDir, in_prefix=self.in_prefix_install) # Sym-link or copy libz3 into python package directory - if IS_WINDOWS: + if IS_WINDOWS or self.is_osx_hack(): MakeRuleCmd.install_files(out, self.libz3Component.dll_file(), - os.path.join(pythonPkgDirWithoutPrefix, - self.libz3Component.dll_file()) + os.path.join(self.pythonPkgDir, + self.libz3Component.dll_file()), + in_prefix=self.in_prefix_install ) else: # Create symbolic link to save space. @@ -1370,18 +1393,27 @@ class PythonInstallComponent(Component): # staged installs that use DESTDIR). MakeRuleCmd.create_relative_symbolic_link(out, self.libz3Component.install_path(), - os.path.join(self.pythonPkgDirWithoutPrefix, + os.path.join(self.pythonPkgDir, self.libz3Component.dll_file() - ) + ), ) - MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDirWithoutPrefix) + MakeRuleCmd.install_files(out, 'z3*.py', self.pythonPkgDir, + in_prefix=self.in_prefix_install) if sys.version >= "3": - pythonPycacheDir = os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__') - MakeRuleCmd.make_install_directory(out, pythonPycacheDir) - MakeRuleCmd.install_files(out, '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), pythonPycacheDir) + pythonPycacheDir = os.path.join(self.pythonPkgDir, '__pycache__') + MakeRuleCmd.make_install_directory(out, + pythonPycacheDir, + in_prefix=self.in_prefix_install) + MakeRuleCmd.install_files(out, + '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), + pythonPycacheDir, + in_prefix=self.in_prefix_install) else: - MakeRuleCmd.install_files(out, 'z3*.pyc', self.pythonPkgDirWithoutPrefix) + MakeRuleCmd.install_files(out, + 'z3*.pyc', + self.pythonPkgDir, + in_prefix=self.in_prefix_install) if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib(): if os.uname()[0] == 'Darwin': LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH" @@ -1394,11 +1426,21 @@ class PythonInstallComponent(Component): def mk_uninstall(self, out): if not is_python_install_enabled(): return - MakeRuleCmd.remove_installed_files(out, os.path.join(self.pythonPkgDirWithoutPrefix, - self.libz3Component.dll_file())) - MakeRuleCmd.remove_installed_files(out, '{}*.py'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) - MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, 'z3'))) - MakeRuleCmd.remove_installed_files(out, '{}*.pyc'.format(os.path.join(self.pythonPkgDirWithoutPrefix, '__pycache__', 'z3'))) + MakeRuleCmd.remove_installed_files(out, + os.path.join(self.pythonPkgDir, + self.libz3Component.dll_file()), + in_prefix=self.in_prefix_install + ) + MakeRuleCmd.remove_installed_files(out, + '{}*.py'.format(os.path.join(self.pythonPkgDir, 'z3')), + in_prefix=self.in_prefix_install) + MakeRuleCmd.remove_installed_files(out, + '{}*.pyc'.format(os.path.join(self.pythonPkgDir, 'z3')), + in_prefix=self.in_prefix_install) + MakeRuleCmd.remove_installed_files(out, + '{}*.pyc'.format(os.path.join(self.pythonPkgDir, '__pycache__', 'z3')), + in_prefix=self.in_prefix_install + ) def mk_makefile(self, out): return @@ -3479,37 +3521,56 @@ class MakeRuleCmd(object): return "$(DESTDIR)$(PREFIX)/" @classmethod - def install_files(cls, out, src_pattern, dest): + def _install_root(cls, path, in_prefix, out): + if in_prefix: + assert not os.path.isabs(path) + install_root = cls.install_root() + else: + # This hack only exists for the Python bindings on OSX + # which are sometimes not installed inside the prefix. + # In all other cases installing outside the prefix is + # misleading and dangerous! + assert IS_OSX + assert os.path.isabs(path) + install_root = "$(DESTDIR)" + cls.write_cmd(out, 'echo "WARNING: {} is not in the install prefix. This will likely lead to a broken installation."'.format(path)) + return install_root + + @classmethod + def install_files(cls, out, src_pattern, dest, in_prefix=True): assert len(dest) > 0 assert isinstance(src_pattern, str) assert not ' ' in src_pattern assert isinstance(dest, str) assert not ' ' in dest assert not os.path.isabs(src_pattern) - assert not os.path.isabs(dest) + install_root = cls._install_root(dest, in_prefix, out) + cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format( src_pattern=src_pattern, - install_root=cls.install_root(), + install_root=install_root, dest=dest)) @classmethod - def remove_installed_files(cls, out, pattern): + def remove_installed_files(cls, out, pattern, in_prefix=True): assert len(pattern) > 0 assert isinstance(pattern, str) assert not ' ' in pattern - assert not os.path.isabs(pattern) + install_root = cls._install_root(pattern, in_prefix, out) + cls.write_cmd(out, "rm -f {install_root}{pattern}".format( - install_root=cls.install_root(), + install_root=install_root, pattern=pattern)) @classmethod - def make_install_directory(cls, out, dir): + def make_install_directory(cls, out, dir, in_prefix=True): assert len(dir) > 0 assert isinstance(dir, str) assert not ' ' in dir - assert not os.path.isabs(dir) + install_root = cls._install_root(dir, in_prefix, out) + cls.write_cmd(out, "mkdir -p {install_root}{dir}".format( - install_root=cls.install_root(), + install_root=install_root, dir=dir)) @classmethod @@ -3548,10 +3609,11 @@ class MakeRuleCmd(object): # it's a file if link_name[-1] != '/': # link_name is a file - temp_path = '/' + os.path.dirname(link_name) + temp_path = os.path.dirname(link_name) else: # link_name is a directory - temp_path = '/' + link_name[:-1] + temp_path = link_name[:-1] + temp_path = '/' + temp_path relative_path = "" targetAsAbs = '/' + target assert os.path.isabs(targetAsAbs) @@ -3575,7 +3637,7 @@ class MakeRuleCmd(object): assert isinstance(target, str) assert isinstance(link_name, str) assert not os.path.isabs(target) - assert not os.path.isabs(link_name) + cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format( target=target, install_root=cls.install_root(), From 0a1c645b5ebec12ccefa13f055b61a0705e5f245 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Dec 2015 23:20:39 +0000 Subject: [PATCH 6/8] Don't emit install commands and dependencies if ML bindings are disabled! --- scripts/mk_util.py | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 183e70003..fb1a3141e 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1843,12 +1843,16 @@ class MLComponent(Component): self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, self.sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) def mk_install_deps(self, out): + if not is_ml_enabled(): + return if OCAMLFIND != '': out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') out.write(os.path.join(self.sub_dir, 'z3ml.cmxa ')) out.write(os.path.join(self.sub_dir, 'META ')) def mk_install(self, out): + if not is_ml_enabled(): + return if OCAMLFIND != '': out.write('\t@%s remove Z3\n' % (OCAMLFIND)) out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META')))) @@ -1875,6 +1879,8 @@ class MLComponent(Component): out.write('\n') def mk_uninstall(self, out): + if not is_ml_enabled(): + return if OCAMLFIND != '': out.write('\t@%s remove Z3\n' % (OCAMLFIND)) From d9cd01f3f7973ca167e4263bba383c566b4db062 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Wed, 9 Dec 2015 09:28:17 +0000 Subject: [PATCH 7/8] remove a few leftovers from min aggregation cleanup Signed-off-by: Nuno Lopes --- src/muz/rel/dl_base.cpp | 122 ---------------------------- src/muz/rel/dl_base.h | 28 ------- src/muz/rel/dl_compiler.cpp | 3 - src/muz/rel/dl_instruction.cpp | 55 ------------- src/muz/rel/dl_relation_manager.cpp | 6 -- src/muz/rel/dl_relation_manager.h | 3 - src/muz/rel/rel_context.cpp | 8 -- src/test/dl_table.cpp | 70 ---------------- 8 files changed, 295 deletions(-) diff --git a/src/muz/rel/dl_base.cpp b/src/muz/rel/dl_base.cpp index 6dc7f2f6e..b7f4d6cef 100644 --- a/src/muz/rel/dl_base.cpp +++ b/src/muz/rel/dl_base.cpp @@ -484,126 +484,4 @@ namespace datalog { } brw.mk_or(disjs.size(), disjs.c_ptr(), fml); } - - class table_plugin::min_fn : public table_min_fn{ - table_signature m_sig; - const unsigned_vector m_group_by_cols; - const unsigned m_col; - public: - min_fn(const table_signature & t_sig, const unsigned_vector& group_by_cols, const unsigned col) - : m_sig(t_sig), - m_group_by_cols(group_by_cols), - m_col(col) {} - - virtual table_base* operator()(table_base const& t) { - //return reference_implementation(t); - return reference_implementation_with_hash(t); - } - - private: - - /** - Reference implementation with negation: - - T1 = join(T, T) by group_cols - T2 = { (t1,t2) in T1 | t1[col] > t2[col] } - T3 = { t1 | (t1,t2) in T2 } - T4 = T \ T3 - - The point of this reference implementation is to show - that the minimum requires negation (set difference). - This is relevant for fixed point computations. - */ - virtual table_base * reference_implementation(const table_base & t) { - relation_manager & manager = t.get_manager(); - scoped_ptr join_fn = manager.mk_join_fn(t, t, m_group_by_cols, m_group_by_cols); - scoped_rel join_table = (*join_fn)(t, t); - - table_base::iterator join_table_it = join_table->begin(); - table_base::iterator join_table_end = join_table->end(); - table_fact row; - - table_element i, j; - - for (; join_table_it != join_table_end; ++join_table_it) { - join_table_it->get_fact(row); - i = row[m_col]; - j = row[t.num_columns() + m_col]; - - if (i > j) { - continue; - } - - join_table->remove_fact(row); - } - - unsigned_vector cols(t.num_columns()); - for (unsigned k = 0; k < cols.size(); ++k) { - cols[k] = cols.size() + k; - SASSERT(cols[k] < join_table->num_columns()); - } - - scoped_ptr project_fn = manager.mk_project_fn(*join_table, cols); - scoped_rel gt_table = (*project_fn)(*join_table); - - for (unsigned k = 0; k < cols.size(); ++k) { - cols[k] = k; - SASSERT(cols[k] < t.num_columns()); - SASSERT(cols[k] < gt_table->num_columns()); - } - - table_base * result = t.clone(); - scoped_ptr diff_fn = manager.mk_filter_by_negation_fn(*result, *gt_table, cols, cols); - (*diff_fn)(*result, *gt_table); - return result; - } - - typedef map < table_fact, table_element, svector_hash_proc, - vector_eq_proc > group_map; - - // Thanks to Nikolaj who kindly helped with the second reference implementation! - virtual table_base * reference_implementation_with_hash(const table_base & t) { - group_map group; - table_base::iterator it = t.begin(); - table_base::iterator end = t.end(); - table_fact row, row2; - table_element current_value, min_value; - for (; it != end; ++it) { - it->get_fact(row); - current_value = row[m_col]; - group_by(row, row2); - group_map::entry* entry = group.find_core(row2); - if (!entry) { - group.insert(row2, current_value); - } - else if (entry->get_data().m_value > current_value) { - entry->get_data().m_value = current_value; - } - } - table_base* result = t.get_plugin().mk_empty(m_sig); - table_base::iterator it2 = t.begin(); - for (; it2 != end; ++it2) { - it2->get_fact(row); - current_value = row[m_col]; - group_by(row, row2); - VERIFY(group.find(row2, min_value)); - if (min_value == current_value) { - result->add_fact(row); - } - } - return result; - } - - void group_by(table_fact const& in, table_fact& out) { - out.reset(); - for (unsigned i = 0; i < m_group_by_cols.size(); ++i) { - out.push_back(in[m_group_by_cols[i]]); - } - } - }; - - table_min_fn * table_plugin::mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col) { - return alloc(table_plugin::min_fn, t.get_signature(), group_by_cols, col); - } } diff --git a/src/muz/rel/dl_base.h b/src/muz/rel/dl_base.h index c26623737..7b6210850 100644 --- a/src/muz/rel/dl_base.h +++ b/src/muz/rel/dl_base.h @@ -192,29 +192,6 @@ namespace datalog { virtual base_object * operator()(const base_object & t1, const base_object & t2) = 0; }; - /** - \brief Aggregate minimum value - - Informally, we want to group rows in a table \c t by \c group_by_cols and - return the minimum value in column \c col among each group. - - Let \c t be a table with N columns. - Let \c group_by_cols be a set of column identifers for table \c t such that |group_by_cols| < N. - Let \c col be a column identifier for table \c t such that \c col is not in \c group_by_cols. - - Let R_col be a set of rows in table \c t such that, for all rows r_i, r_j in R_col - and column identifiers k in \c group_by_cols, r_i[k] = r_j[k]. - - For each R_col, we want to restrict R_col to those rows whose value in column \c col is minimal. - - min_fn(R, group_by_cols, col) = - { row in R | forall row' in R . row'[group_by_cols] = row[group_by_cols] => row'[col] >= row[col] } - */ - class min_fn : public base_fn { - public: - virtual base_object * operator()(const base_object & t) = 0; - }; - class transformer_fn : public base_fn { public: virtual base_object * operator()(const base_object & t) = 0; @@ -879,7 +856,6 @@ namespace datalog { typedef table_infrastructure::base_fn base_table_fn; typedef table_infrastructure::join_fn table_join_fn; - typedef table_infrastructure::min_fn table_min_fn; typedef table_infrastructure::transformer_fn table_transformer_fn; typedef table_infrastructure::union_fn table_union_fn; typedef table_infrastructure::mutator_fn table_mutator_fn; @@ -1044,7 +1020,6 @@ namespace datalog { class table_plugin : public table_infrastructure::plugin_object { friend class relation_manager; - class min_fn; protected: table_plugin(symbol const& n, relation_manager & manager) : plugin_object(n, manager) {} public: @@ -1052,9 +1027,6 @@ namespace datalog { virtual bool can_handle_signature(const table_signature & s) { return s.functional_columns()==0; } protected: - virtual table_min_fn * mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col); - /** If the returned value is non-zero, the returned object must take ownership of \c mapper. Otherwise \c mapper must remain unmodified. diff --git a/src/muz/rel/dl_compiler.cpp b/src/muz/rel/dl_compiler.cpp index 7b26f19c7..67227e7d9 100644 --- a/src/muz/rel/dl_compiler.cpp +++ b/src/muz/rel/dl_compiler.cpp @@ -467,9 +467,6 @@ namespace datalog { // whether to dealloc the previous result bool dealloc = true; - // setup information for min aggregation - unsigned_vector group_by_cols; - if(pt_len == 2) { reg_idx t1_reg=tail_regs[0]; reg_idx t2_reg=tail_regs[1]; diff --git a/src/muz/rel/dl_instruction.cpp b/src/muz/rel/dl_instruction.cpp index fb7bb9281..2c1850bf4 100644 --- a/src/muz/rel/dl_instruction.cpp +++ b/src/muz/rel/dl_instruction.cpp @@ -25,7 +25,6 @@ Revision History: #include"rel_context.h" #include"debug.h" #include"warning.h" -#include"dl_table_relation.h" namespace datalog { @@ -886,60 +885,6 @@ namespace datalog { removed_cols, result); } - class instr_min : public instruction { - reg_idx m_source_reg; - reg_idx m_target_reg; - unsigned_vector m_group_by_cols; - unsigned m_min_col; - public: - instr_min(reg_idx source_reg, reg_idx target_reg, const unsigned_vector & group_by_cols, unsigned min_col) - : m_source_reg(source_reg), - m_target_reg(target_reg), - m_group_by_cols(group_by_cols), - m_min_col(min_col) { - } - virtual bool perform(execution_context & ctx) { - log_verbose(ctx); - if (!ctx.reg(m_source_reg)) { - ctx.make_empty(m_target_reg); - return true; - } - - const relation_base & s = *ctx.reg(m_source_reg); - if (!s.from_table()) { - throw default_exception(default_exception::fmt(), "relation is not a table %s", - s.get_plugin().get_name().bare_str()); - } - ++ctx.m_stats.m_min; - const table_relation & tr = static_cast(s); - const table_base & source_t = tr.get_table(); - relation_manager & r_manager = s.get_manager(); - - const relation_signature & r_sig = s.get_signature(); - scoped_ptr fn = r_manager.mk_min_fn(source_t, m_group_by_cols, m_min_col); - table_base * target_t = (*fn)(source_t); - - TRACE("dl", - tout << "% "; - target_t->display(tout); - tout << "\n";); - - relation_base * target_r = r_manager.mk_table_relation(r_sig, target_t); - ctx.set_reg(m_target_reg, target_r); - return true; - } - virtual void display_head_impl(execution_context const& ctx, std::ostream & out) const { - out << " MIN AGGR "; - } - virtual void make_annotations(execution_context & ctx) { - } - }; - - instruction * instruction::mk_min(reg_idx source, reg_idx target, const unsigned_vector & group_by_cols, - const unsigned min_col) { - return alloc(instr_min, source, target, group_by_cols, min_col); - } - class instr_select_equal_and_project : public instruction { reg_idx m_src; reg_idx m_result; diff --git a/src/muz/rel/dl_relation_manager.cpp b/src/muz/rel/dl_relation_manager.cpp index 2b78baf05..ddcdf7ae2 100644 --- a/src/muz/rel/dl_relation_manager.cpp +++ b/src/muz/rel/dl_relation_manager.cpp @@ -1023,12 +1023,6 @@ namespace datalog { return res; } - table_min_fn * relation_manager::mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col) - { - return t.get_plugin().mk_min_fn(t, group_by_cols, col); - } - class relation_manager::auxiliary_table_transformer_fn { table_fact m_row; public: diff --git a/src/muz/rel/dl_relation_manager.h b/src/muz/rel/dl_relation_manager.h index cda6373d3..6e1b5737e 100644 --- a/src/muz/rel/dl_relation_manager.h +++ b/src/muz/rel/dl_relation_manager.h @@ -251,9 +251,6 @@ namespace datalog { return mk_join_fn(t1, t2, cols1.size(), cols1.c_ptr(), cols2.c_ptr(), allow_product_relation); } - table_min_fn * mk_min_fn(const table_base & t, - unsigned_vector & group_by_cols, const unsigned col); - /** \brief Return functor that transforms a table into one that lacks columns listed in \c removed_cols array. diff --git a/src/muz/rel/rel_context.cpp b/src/muz/rel/rel_context.cpp index c6b47f1ed..52dd10202 100644 --- a/src/muz/rel/rel_context.cpp +++ b/src/muz/rel/rel_context.cpp @@ -291,27 +291,19 @@ namespace datalog { return res; } -#define _MIN_DONE_ 1 - void rel_context::transform_rules() { rule_transformer transf(m_context); -#ifdef _MIN_DONE_ transf.register_plugin(alloc(mk_coi_filter, m_context)); -#endif transf.register_plugin(alloc(mk_filter_rules, m_context)); transf.register_plugin(alloc(mk_simple_joins, m_context)); if (m_context.unbound_compressor()) { transf.register_plugin(alloc(mk_unbound_compressor, m_context)); } -#ifdef _MIN_DONE_ if (m_context.similarity_compressor()) { transf.register_plugin(alloc(mk_similarity_compressor, m_context)); } -#endif transf.register_plugin(alloc(mk_partial_equivalence_transformer, m_context)); -#ifdef _MIN_DONE_ transf.register_plugin(alloc(mk_rule_inliner, m_context)); -#endif transf.register_plugin(alloc(mk_interp_tail_simplifier, m_context)); transf.register_plugin(alloc(mk_separate_negated_tails, m_context)); diff --git a/src/test/dl_table.cpp b/src/test/dl_table.cpp index b14988f11..62eec34bc 100644 --- a/src/test/dl_table.cpp +++ b/src/test/dl_table.cpp @@ -95,78 +95,8 @@ void test_dl_bitvector_table() { test_table(mk_bv_table); } -void test_table_min() { - std::cout << "----- test_table_min -----\n"; - datalog::table_signature sig; - sig.push_back(2); - sig.push_back(4); - sig.push_back(8); - smt_params params; - ast_manager ast_m; - datalog::register_engine re; - datalog::context ctx(ast_m, re, params); - datalog::relation_manager & m = ctx.get_rel_context()->get_rmanager(); - - m.register_plugin(alloc(datalog::bitvector_table_plugin, m)); - - datalog::table_base* tbl = mk_bv_table(m, sig); - datalog::table_base& table = *tbl; - - datalog::table_fact row, row1, row2, row3; - row.push_back(1); - row.push_back(2); - row.push_back(5); - - // Group (1,2,*) - row1 = row; - row[2] = 6; - row2 = row; - row[2] = 5; - row3 = row; - - table.add_fact(row1); - table.add_fact(row2); - table.add_fact(row3); - - // Group (1,3,*) - row[1] = 3; - row1 = row; - row[2] = 7; - row2 = row; - row[2] = 4; - row3 = row; - - table.add_fact(row1); - table.add_fact(row2); - table.add_fact(row3); - - table.display(std::cout); - - unsigned_vector group_by(2); - group_by[0] = 0; - group_by[1] = 1; - - datalog::table_min_fn * min_fn = m.mk_min_fn(table, group_by, 2); - datalog::table_base * min_tbl = (*min_fn)(table); - - min_tbl->display(std::cout); - - row[1] = 2; - row[2] = 5; - SASSERT(min_tbl->contains_fact(row)); - - row[1] = 3; - row[2] = 4; - SASSERT(min_tbl->contains_fact(row)); - - dealloc(min_fn); - min_tbl->deallocate(); - tbl->deallocate(); -} - void tst_dl_table() { test_dl_bitvector_table(); - test_table_min(); } #else void tst_dl_table() { From a0f9f461f8ec5f9d3bacf671ffca07aa41ddcbe8 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Wed, 9 Dec 2015 13:01:42 +0000 Subject: [PATCH 8/8] Build fix --- scripts/mk_util.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 8c109136d..96325bd47 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -1783,13 +1783,13 @@ class MLComponent(Component): self.mk_ml_meta(os.path.join('src/api/ml/META'), os.path.join(BUILD_DIR, self.sub_dir, 'META'), VER_MAJOR, VER_MINOR, VER_BUILD, VER_REVISION) def mk_install_deps(self, out): - if OCAMLFIND != '': + if is_ml_enabled() and OCAMLFIND != '': out.write(get_component(Z3_DLL_COMPONENT).dll_name + '$(SO_EXT) ') out.write(os.path.join(self.sub_dir, 'z3ml.cmxa ')) out.write(os.path.join(self.sub_dir, 'META ')) def mk_install(self, out): - if OCAMLFIND != '': + if is_ml_enabled() and OCAMLFIND != '': out.write('\t@%s remove Z3\n' % (OCAMLFIND)) out.write('\t@%s install Z3 %s' % (OCAMLFIND, (os.path.join(self.sub_dir, 'META')))) for m in self.modules: @@ -1815,7 +1815,7 @@ class MLComponent(Component): out.write('\n') def mk_uninstall(self, out): - if OCAMLFIND != '': + if is_ml_enabled() and OCAMLFIND != '': out.write('\t@%s remove Z3\n' % (OCAMLFIND)) def main_component(self):