From 9489665ddcc35dc99fc0367ab073ba15d9854043 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Mon, 23 Nov 2015 22:47:46 +0000
Subject: [PATCH 01/24] Partially fix not being able to do a staged package
 install of Z3 using the DESTDIR make file variable
 (https://www.gnu.org/prep/standards/html_node/DESTDIR.html) for ``install``
 and ``uninstall`` targets.

Typically packagers build packages like so

```
$ ./configure --prefix=/usr/
$ make
$ make DESTDIR=/some/path/ install
```

Doing this installs the files into a directory ``/some/path`` but places
files inside that directory using the layout in ``--prefix`` (e.g.
``/some/path/usr/bin/z3``).  The ``/some/path`` directory can then be
packaged (e.g. tarballed) for later installation.

The ``DESTDIR`` is not set in the Makefile and thus is empty by default
which maintains the existing ``make install`` behaviour.

Unfortunately this situation isn't fixed for the Python bindings (and
possibly others) yet as more invasive changes are needed here. I'll fix
this in later commits.
---
 scripts/mk_util.py | 22 +++++++++++-----------
 1 file changed, 11 insertions(+), 11 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 83669472d..0a3745a2f 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -992,11 +992,11 @@ class LibComponent(Component):
 
     def mk_install(self, out):
         for include in self.includes2install:
-            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(PREFIX)', 'include', include)))
+            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(DESTDIR)$(PREFIX)', 'include', include)))
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'include', include))
+            out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include', include))
 
     def mk_win_dist(self, build_path, dist_path):
         mk_dir(os.path.join(dist_path, 'include'))
@@ -1078,11 +1078,11 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(PREFIX)', 'bin', exefile)))
+            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile)))
 
     def mk_uninstall(self, out):
         exefile = '%s$(EXE_EXT)' % self.exe_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'bin', exefile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1224,19 +1224,19 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
+            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
             out.write('\t@cp %s %s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', 'lib', libfile)))
+                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
 
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'lib', dllfile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
         out.write('\t@rm -f %s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'lib', libfile))
+        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -2009,9 +2009,9 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'bin'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'include'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(PREFIX)', 'lib'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
+    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
     for c in get_components():
         c.mk_install(out)
     out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)

From b285ce7ceeba659596feb66aacf1140fc7abbc71 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 09:14:08 +0000
Subject: [PATCH 02/24] Partially fix not being able to do a staged install
 (using ``DESTDIR``) when installing the Python bindings.

If ``DESTDIR`` is set the bindings will now be installed under this
path but ``$(PREFIX)`` only appears in the ``Makefile`` if ``--prefix``
was set which seems a little broken (we'll fix this soon).

The creation of the Python ``site-packages`` (and ``__pycache__`` for Python
3) directories has been moved to build time instead of configure time
because we don't know what ``DESTDIR`` will be set to at configure time.
---
 scripts/mk_util.py | 23 +++++++++++------------
 1 file changed, 11 insertions(+), 12 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0a3745a2f..0cad588dc 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -637,10 +637,7 @@ def parse_options():
             SLOW_OPTIMIZE = True
         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
             PREFIX = arg
-            PYTHON_PACKAGE_DIR = os.path.join(PREFIX, 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
-            mk_dir(PYTHON_PACKAGE_DIR)
-            if sys.version >= "3":
-                mk_dir(os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
+            PYTHON_PACKAGE_DIR = os.path.join('$(PREFIX)', 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -1225,7 +1222,7 @@ class DLLComponent(Component):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
             out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
@@ -1234,7 +1231,7 @@ class DLLComponent(Component):
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
         out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
-        out.write('\t@rm -f %s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
+        out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
 
@@ -2012,14 +2009,16 @@ def mk_install(out):
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
     out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
+    out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     for c in get_components():
         c.mk_install(out)
-    out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)
+    out.write('\t@cp z3*.py $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     if sys.version >= "3":
-        out.write('\t@cp %s*.pyc %s\n' % (os.path.join('__pycache__', 'z3'),
+        out.write('\t@mkdir -p $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
+        out.write('\t@cp %s*.pyc $(DESTDIR)%s\n' % (os.path.join('__pycache__', 'z3'),
                                           os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))
     else:
-        out.write('\t@cp z3*.pyc %s\n' % PYTHON_PACKAGE_DIR)
+        out.write('\t@cp z3*.pyc $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     out.write('\t@echo Z3 was successfully installed.\n')
     if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
         if os.uname()[0] == 'Darwin':
@@ -2035,9 +2034,9 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
-    out.write('\t@rm -f %s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f %s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
+    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 

From 4c11037d70db1ef8c533395cf298aaf1e1505255 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 12:10:01 +0000
Subject: [PATCH 03/24] Fix setting the path to the Python package directory.

There were several problems with the existing implementation.

* When specifying ``--prefix`` the implementation would assume the
  path was ``$(PREFIX)/lib/python-<VERSION>/dist-packages``. This
  is incorrect. ``dist-packages`` is Debian (and its derivatives,
  i.e Ubuntu) specific and won't work on other Linux distributions
  such as Arch Linux.

* When generating the ``Makefile``, ``$(PREFIX)`` was only emitted
  during the Python installation when ``--prefix`` was passed on
  the command line. When ``--prefix`` was not passed the absolute
  path to the Python package directory was emitted. This is not
  very consistent.

This patch checks that the detected Python package directory lives
under the install prefix and emits an error if it does not as this
indicates that the installation will be broken. If the Python package
directory does live under the install prefix it replaces that prefix
with the ``$(PREFIX)`` variable when emitting the ``Makefile`` for
consistency with the other install commands.

If a user really wants to install to a particular Python package
directory they can force it with the newly added ``--pypkgdir=``
flag.
---
 scripts/mk_util.py | 32 ++++++++++++++++++++++++++++++--
 1 file changed, 30 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 0cad588dc..44779ebb1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -550,6 +550,7 @@ def display_help(exit_code):
         print("  -p <dir>, --prefix=<dir>      installation prefix (default: %s)." % PREFIX)
     else:
         print("  --parallel=num                use cl option /MP with 'num' parallel processes")
+    print("  --pypkgdir=<dir>              Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR)
     print("  -b <sudir>, --build=<subdir>  subdirectory where Z3 will be built (default: build).")
     print("  --githash=hash                include the given hash in the binaries.")
     print("  -d, --debug                   compile Z3 in debug mode.")
@@ -593,12 +594,13 @@ def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
+    pythonPkgDir=None
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
                                                ['build=', 'debug', 'silent', 'x64', 'help', 'makefiles', 'showcpp', 'vsproj',
                                                 'trace', 'nodotnet', 'staticlib', 'prefix=', 'gmp', 'foci2=', 'java', 'parallel=', 'gprof',
-                                                'githash=', 'x86', 'ml', 'optimize', 'noomp'])
+                                                'githash=', 'x86', 'ml', 'optimize', 'noomp', 'pypkgdir='])
     except:
         print("ERROR: Invalid command line option")
         display_help(1)
@@ -637,7 +639,8 @@ def parse_options():
             SLOW_OPTIMIZE = True
         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
             PREFIX = arg
-            PYTHON_PACKAGE_DIR = os.path.join('$(PREFIX)', 'lib', 'python%s' % distutils.sysconfig.get_python_version(), 'dist-packages')
+        elif opt in ('--pypkgdir'):
+            pythonPkgDir = arg
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -659,6 +662,31 @@ def parse_options():
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
+    # Handle the Python package directory
+    def printPythonPackageMessage(errorType):
+        msg = (("%s: The detected Python package directory (%s)"
+               " does not live under the installation prefix (%s)"
+               ". This will most likely lead to a broken installation.") %
+               (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+        if errorType == "ERROR":
+            msg += (" However if you are confident you want to use that"
+                   " Python package directory use --pypkgdir=%s to force"
+                   " it.") % PYTHON_PACKAGE_DIR
+        print(msg)
+    if pythonPkgDir == None:
+        if not IS_WINDOWS:
+            # Try to use the default if it makes sense
+            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+                printPythonPackageMessage("ERROR")
+                sys.exit(1)
+            # Do replacement to use $(PREFIX) in the Makefile
+            PYTHON_PACKAGE_DIR = PYTHON_PACKAGE_DIR.replace(PREFIX, "$(PREFIX)", 1)
+    else:
+        PYTHON_PACKAGE_DIR = pythonPkgDir
+        if not os.path.exists(PYTHON_PACKAGE_DIR):
+            print("WARNING: PYTHON_PACKAGE_DIR (%s) does not exist." % PYTHON_PACKAGE_DIR)
+        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+            printPythonPackageMessage("WARNING")
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.

From e8822b18065cd162634720c8a9aef7dbde837d99 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 17:27:54 +0000
Subject: [PATCH 04/24] Add a note about using DESTDIR when building Z3
 completes.

---
 scripts/mk_util.py | 4 +++-
 1 file changed, 3 insertions(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 44779ebb1..f146cd2e5 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -2087,7 +2087,9 @@ def mk_makefile():
     out.write("\t@echo \"Z3Py scripts stored in arbitrary directories can be also executed if \'%s\' directory is added to the PYTHONPATH environment variable.\"\n" % BUILD_DIR)
     if not IS_WINDOWS:
         out.write("\t@echo Use the following command to install Z3 at prefix $(PREFIX).\n")
-        out.write('\t@echo "    sudo make install"\n')
+        out.write('\t@echo "    sudo make install"\n\n')
+        out.write("\t@echo If you are doing a staged install you can use DESTDIR.\n")
+        out.write('\t@echo "    make DESTDIR=/some/temp/directory install"\n')
     # Generate :examples rule
     out.write('examples:')
     for c in get_components():

From 53f0addb6bf86b7a3a03d3ba817019dc3b043cfa Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 18:15:11 +0000
Subject: [PATCH 05/24] Avoid making a copy of libz3 on non Windows platforms
 for the Python bindings (provided they both exist within the same install
 prefix) by creating a relative symbolic link. This saves space when packaging
 Z3.

---
 scripts/mk_util.py | 50 ++++++++++++++++++++++++++++++++++++++++++++--
 1 file changed, 48 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index f146cd2e5..766347b16 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1246,11 +1246,57 @@ class DLLComponent(Component):
         if self.static:
             out.write(' %s$(LIB_EXT)' % self.dll_name)
 
+    def _compute_relative_path(self, link_dir, target):
+        """
+        Compute the relative path to ``target`` from a directory
+        ``link_dir``.
+
+        e.g.
+        ```
+        self._compute_relative_path("/usr/lib/python3.5/site-packages",
+                                         "/usr/lib/libz3.so")
+
+             ==
+
+             "../../libz3.so"
+        ```
+        """
+        assert os.path.isabs(link_dir)
+        assert os.path.isabs(target)
+        relative_path =""
+
+        temp_path = link_dir
+        # Keep walking up the directory tree until temp_path
+        # is a prefix of target.
+        while not target.startswith(temp_path):
+            assert temp_path != '/'
+            temp_path = os.path.dirname(temp_path)
+            relative_path += '../'
+
+        # Now get the path from the common prefix to the target
+        target_from_prefix = target.replace(temp_path,'',1)
+        relative_path += target_from_prefix
+        # Remove any double slashes
+        relativePath = relative_path.replace('//','/')
+        return relativePath
+
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
+            pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
+            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, dllInstallPath))
+            if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
+                out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            else:
+                # Create symbolic link to save space.
+                # Compute the relative path from the python package directory
+                # to libz3. It's important that this symlink be relative
+                # (rather than absolute) so that the install is relocatable.
+                dllInstallPathSubst = dllInstallPath.replace('$(PREFIX)', PREFIX,1)
+                relativePath = self._compute_relative_path(pythonPkgDirSubst,
+                                                           dllInstallPathSubst)
+                out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))

From 23cf7e86a92621af13676cce08c28ade4901b263 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Tue, 24 Nov 2015 23:03:18 +0000
Subject: [PATCH 06/24] Start to address @wintersteiger 's comments aboug
 ``$(DESTDIR)`` being duplicated in too many places and being worried that
 someone might forget to use it when installing additional components.

To acheive this the new ``MakeRuleCmd`` class provides
several class methods to generate commonly needed commands used in
make file rules.

Most of the build system has been changed to use these helper methods
apart from stuff related to the Python bindings. This can't be changed
until we fix how PYTHON_PACKAGE_DIR is handled. Right it not guaranteed
to live under the install prefix but this is a requirement when using
the ``MakeRuleCmd`` methods.
---
 scripts/mk_util.py | 88 +++++++++++++++++++++++++++++++++++++---------
 1 file changed, 72 insertions(+), 16 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 766347b16..691633eb2 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1017,11 +1017,15 @@ class LibComponent(Component):
 
     def mk_install(self, out):
         for include in self.includes2install:
-            out.write('\t@cp %s %s\n' % (os.path.join(self.to_src_dir, include), os.path.join('$(DESTDIR)$(PREFIX)', 'include', include)))
+            MakeRuleCmd.install_files(
+                out,
+                os.path.join(self.to_src_dir, include),
+                os.path.join('include', include)
+            )
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include', include))
+            MakeRuleCmd.remove_installed_files(out, os.path.join('include', include))
 
     def mk_win_dist(self, build_path, dist_path):
         mk_dir(os.path.join(dist_path, 'include'))
@@ -1103,11 +1107,11 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            out.write('\t@cp %s %s\n' % (exefile, os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile)))
+            MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
 
     def mk_uninstall(self, out):
         exefile = '%s$(EXE_EXT)' % self.exe_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin', exefile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1283,9 +1287,11 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
+            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            # FIXME: All this stuff to do with the Python bindings needs to
+            # be refactored to use MakeRuleCmd.
             dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
             pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
-            out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, dllInstallPath))
             if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
                 out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             else:
@@ -1299,15 +1305,15 @@ class DLLComponent(Component):
                 out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile)))
-
+                MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
 
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', dllfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+        # FIXME: Use MakeRuleCmd
         out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib', libfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
@@ -1474,14 +1480,16 @@ class JavaDLLComponent(Component):
     def mk_install(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@cp %s %s\n' % (dllfile, os.path.join('$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@cp %s.jar %s.jar\n' % (self.package_name, os.path.join('$(PREFIX)', 'lib', self.package_name)))
+            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            MakeRuleCmd.install_files(out, jarfile, os.path.join('lib', jarfile))
 
     def mk_uninstall(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            out.write('\t@rm %s\n' % (os.path.join('$(PREFIX)', 'lib', dllfile)))
-            out.write('\t@rm %s.jar\n' % (os.path.join('$(PREFIX)', 'lib', self.package_name)))
+            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', jarfile))
 
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
@@ -2080,9 +2088,10 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'bin'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'include'))
-    out.write('\t@mkdir -p %s\n' % os.path.join('$(DESTDIR)$(PREFIX)', 'lib'))
+    MakeRuleCmd.make_install_directory(out, 'bin')
+    MakeRuleCmd.make_install_directory(out, 'include')
+    MakeRuleCmd.make_install_directory(out, 'lib')
+    # FIXME: use MakeRuleCmd for the Python stuff
     out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
     for c in get_components():
         c.mk_install(out)
@@ -2108,6 +2117,7 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
+    # FIXME: use MakeRuleCmd for the Python stuff
     out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
     out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
     out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
@@ -3260,6 +3270,52 @@ def mk_unix_dist(build_path, dist_path):
         shutil.copy(os.path.join(build_path, pyc),
                     os.path.join(dist_path, 'bin', pyc))
 
+class MakeRuleCmd(object):
+    """
+        These class methods provide a convenient way to emit frequently
+        needed commands used in Makefile rules
+
+        Note that several of the method are meant for use during ``make
+        install`` and ``make uninstall``.  These methods correctly use
+        ``$(PREFIX)`` and ``$(DESTDIR)`` and therefore are preferrable
+        to writing commands manually which can be error prone.
+    """
+    @classmethod
+    def install_files(cls, out, srcPattern, dest):
+        assert len(dest) > 0
+        assert isinstance(srcPattern, str)
+        assert not ' ' in srcPattern
+        assert isinstance(dest, str)
+        assert not ' ' in dest
+        assert not os.path.isabs(srcPattern)
+        assert not os.path.isabs(dest)
+        cls.write_cmd(out, "cp {} $(DESTDIR)$(PREFIX)/{}".format(srcPattern, dest))
+
+    @classmethod
+    def remove_installed_files(cls, out, pattern):
+        assert len(pattern) > 0
+        assert isinstance(pattern, str)
+        assert not ' ' in pattern
+        assert not os.path.isabs(pattern)
+        cls.write_cmd(out, "rm -f $(DESTDIR)$(PREFIX)/{}".format(pattern))
+
+    @classmethod
+    def make_install_directory(cls, out, dir):
+        assert len(dir) > 0
+        assert isinstance(dir, str)
+        assert not ' ' in dir
+        assert not os.path.isabs(dir)
+        cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
+
+    # TODO: Refactor all of the build system to emit commands using this
+    # helper to simplify code. This will also let us replace ``@`` with
+    # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
+    # a variable (e.g. ``VERBOSE``) passed to the ``make`` invocation. This
+    # would be very helpful for debugging.
+    @classmethod
+    def write_cmd(cls, out, line):
+        out.write("\t@{}\n".format(line))
+
 
 if __name__ == '__main__':
     import doctest

From 041c02feb7aa682ecc887a2a1064b5729c68a5b4 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 10:46:56 +0000
Subject: [PATCH 07/24] Finish addressing @wintersteiger comments on
 ``$(DESTDIR)`` being duplicated in too many places by refactoring the
 installation and removal of the Python bindings to use the ``MakeRuleCmd``
 class.

In order to make this change:

* ``PYTHON_PACKAGE_DIR`` no longer contains the text ``$(PREFIX)``
* ``PYTHON_PACKAGE_DIR`` **MUST BE** inside the installation prefix
---
 scripts/mk_util.py | 166 ++++++++++++++++++++++-----------------------
 1 file changed, 83 insertions(+), 83 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 691633eb2..7bc68e193 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -594,7 +594,6 @@ def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
     global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
-    pythonPkgDir=None
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
@@ -640,7 +639,7 @@ def parse_options():
         elif not IS_WINDOWS and opt in ('-p', '--prefix'):
             PREFIX = arg
         elif opt in ('--pypkgdir'):
-            pythonPkgDir = arg
+            PYTHON_PACKAGE_DIR = arg
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -663,30 +662,15 @@ def parse_options():
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
     # Handle the Python package directory
-    def printPythonPackageMessage(errorType):
-        msg = (("%s: The detected Python package directory (%s)"
-               " does not live under the installation prefix (%s)"
-               ". This will most likely lead to a broken installation.") %
-               (errorType, PYTHON_PACKAGE_DIR, PREFIX))
-        if errorType == "ERROR":
-            msg += (" However if you are confident you want to use that"
-                   " Python package directory use --pypkgdir=%s to force"
-                   " it.") % PYTHON_PACKAGE_DIR
-        print(msg)
-    if pythonPkgDir == None:
-        if not IS_WINDOWS:
-            # Try to use the default if it makes sense
-            if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-                printPythonPackageMessage("ERROR")
-                sys.exit(1)
-            # Do replacement to use $(PREFIX) in the Makefile
-            PYTHON_PACKAGE_DIR = PYTHON_PACKAGE_DIR.replace(PREFIX, "$(PREFIX)", 1)
-    else:
-        PYTHON_PACKAGE_DIR = pythonPkgDir
-        if not os.path.exists(PYTHON_PACKAGE_DIR):
-            print("WARNING: PYTHON_PACKAGE_DIR (%s) does not exist." % PYTHON_PACKAGE_DIR)
+    if not IS_WINDOWS:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            printPythonPackageMessage("WARNING")
+            printPythonPackageMessage("ERROR")
+            print(("ERROR: The detected Python package directory (%s)"
+                   " does not live under the installation prefix (%s)"
+                   ". This would lead to a broken installation."
+                   "Use --pypkgdir= to change the Python package directory") %
+                  (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+            sys.exit(1)
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -1250,59 +1234,21 @@ class DLLComponent(Component):
         if self.static:
             out.write(' %s$(LIB_EXT)' % self.dll_name)
 
-    def _compute_relative_path(self, link_dir, target):
-        """
-        Compute the relative path to ``target`` from a directory
-        ``link_dir``.
-
-        e.g.
-        ```
-        self._compute_relative_path("/usr/lib/python3.5/site-packages",
-                                         "/usr/lib/libz3.so")
-
-             ==
-
-             "../../libz3.so"
-        ```
-        """
-        assert os.path.isabs(link_dir)
-        assert os.path.isabs(target)
-        relative_path =""
-
-        temp_path = link_dir
-        # Keep walking up the directory tree until temp_path
-        # is a prefix of target.
-        while not target.startswith(temp_path):
-            assert temp_path != '/'
-            temp_path = os.path.dirname(temp_path)
-            relative_path += '../'
-
-        # Now get the path from the common prefix to the target
-        target_from_prefix = target.replace(temp_path,'',1)
-        relative_path += target_from_prefix
-        # Remove any double slashes
-        relativePath = relative_path.replace('//','/')
-        return relativePath
-
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
-            # FIXME: All this stuff to do with the Python bindings needs to
-            # be refactored to use MakeRuleCmd.
-            dllInstallPath = os.path.join('$(PREFIX)', 'lib', dllfile)
-            pythonPkgDirSubst = PYTHON_PACKAGE_DIR.replace('$(PREFIX)', PREFIX, 1)
-            if IS_WINDOWS or not pythonPkgDirSubst.startswith(PREFIX):
-                out.write('\t@cp %s $(DESTDIR)%s\n' % (dllfile, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+            dllInstallPath = os.path.join('lib', dllfile)
+            MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
+            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            if IS_WINDOWS:
+                MakeRuleCmd.install_files(dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
                 # Compute the relative path from the python package directory
                 # to libz3. It's important that this symlink be relative
                 # (rather than absolute) so that the install is relocatable.
-                dllInstallPathSubst = dllInstallPath.replace('$(PREFIX)', PREFIX,1)
-                relativePath = self._compute_relative_path(pythonPkgDirSubst,
-                                                           dllInstallPathSubst)
-                out.write('\t@ln -s %s $(DESTDIR)%s\n' % (relativePath, os.path.join(PYTHON_PACKAGE_DIR, dllfile)))
+                dllInstallPathAbs = os.path.join(PREFIX, dllInstallPath)
+                MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
                 MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
@@ -1310,8 +1256,8 @@ class DLLComponent(Component):
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
-        # FIXME: Use MakeRuleCmd
-        out.write('\t@rm -f $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
+        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+        MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
 
@@ -2091,17 +2037,17 @@ def mk_install(out):
     MakeRuleCmd.make_install_directory(out, 'bin')
     MakeRuleCmd.make_install_directory(out, 'include')
     MakeRuleCmd.make_install_directory(out, 'lib')
-    # FIXME: use MakeRuleCmd for the Python stuff
-    out.write('\t@mkdir -p $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+    pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+    MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
     for c in get_components():
         c.mk_install(out)
-    out.write('\t@cp z3*.py $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+    MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
     if sys.version >= "3":
-        out.write('\t@mkdir -p $(DESTDIR)%s\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
-        out.write('\t@cp %s*.pyc $(DESTDIR)%s\n' % (os.path.join('__pycache__', 'z3'),
-                                          os.path.join(PYTHON_PACKAGE_DIR, '__pycache__')))
+        pythonPycacheDir = os.path.join(pythonPkgDirWithoutPrefix, '__pycache__')
+        MakeRuleCmd.make_install_directory(out, pythonPycacheDir)
+        MakeRuleCmd.install_files(out, '{}*.pyc'.format(os.path.join('__pycache__', 'z3')), pythonPycacheDir)
     else:
-        out.write('\t@cp z3*.pyc $(DESTDIR)%s\n' % PYTHON_PACKAGE_DIR)
+        MakeRuleCmd.install_files(out, 'z3*.pyc', pythonPkgDirWithoutPrefix)
     out.write('\t@echo Z3 was successfully installed.\n')
     if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
         if os.uname()[0] == 'Darwin':
@@ -2117,10 +2063,10 @@ def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
-    # FIXME: use MakeRuleCmd for the Python stuff
-    out.write('\t@rm -f $(DESTDIR)%s*.py\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, 'z3'))
-    out.write('\t@rm -f $(DESTDIR)%s*.pyc\n' % os.path.join(PYTHON_PACKAGE_DIR, '__pycache__', 'z3'))
+    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')))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 
@@ -3307,6 +3253,51 @@ class MakeRuleCmd(object):
         assert not os.path.isabs(dir)
         cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
 
+    @classmethod
+    def create_relative_symbolic_link(cls, out, target, link_name):
+        assert isinstance(target, str)
+        assert isinstance(link_name, str)
+        assert len(target) > 0
+        assert len(link_name) > 0
+        assert not os.path.isabs(target)
+        assert not os.path.isabs(link_name)
+
+        # We can't test to see if link_name is a file or directory
+        # because it may not exist yet. Instead follow the convention
+        # that if there is a leading slash target is a directory otherwise
+        # it's a file
+        if link_name[-1] != '/':
+            # link_name is a file
+            temp_path = '/' + os.path.dirname(link_name)
+        else:
+            # link_name is a directory
+            temp_path = '/' + link_name[:-1]
+        relative_path = ""
+        targetAsAbs = '/' + target
+        assert os.path.isabs(targetAsAbs)
+        assert os.path.isabs(temp_path)
+        # Keep walking up the directory tree until temp_path
+        # is a prefix of targetAsAbs
+        while not targetAsAbs.startswith(temp_path):
+            assert temp_path != '/'
+            temp_path = os.path.dirname(temp_path)
+            relative_path += '../'
+
+        # Now get the path from the common prefix directory to the target
+        target_from_prefix = targetAsAbs[len(temp_path):]
+        relative_path += target_from_prefix
+        # Remove any double slashes
+        relative_path = relative_path.replace('//','/')
+        cls.create_symbolic_link(out, relative_path, link_name)
+
+    @classmethod
+    def create_symbolic_link(cls, out, target, link_name):
+        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 {} $(DESTDIR)$(PREFIX)/{}'.format(target, link_name))
+
     # TODO: Refactor all of the build system to emit commands using this
     # helper to simplify code. This will also let us replace ``@`` with
     # ``$(Verb)`` and have it set to ``@`` or empty at build time depending on
@@ -3316,6 +3307,15 @@ class MakeRuleCmd(object):
     def write_cmd(cls, out, line):
         out.write("\t@{}\n".format(line))
 
+def strip_path_prefix(path, prefix):
+    assert path.startswith(prefix)
+    stripped_path = path[len(prefix):]
+    stripped_path.replace('//','/')
+    if stripped_path[0] == '/':
+        stripped_path = stripped_path[1:]
+
+    assert not os.path.isabs(stripped_path)
+    return stripped_path
 
 if __name__ == '__main__':
     import doctest

From d6fa0583abee1a1030a3faef0169cebbbebafced Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:02:59 +0000
Subject: [PATCH 08/24] Fix bug in ``ExeComponent.mk_uninstall()`` in the build
 system which would try to uninstall components that were never installed.

This bug would cause the following line to be emitted in the
``Makefile`` under the ``uninstall`` rule even though there was
no corresponding rule to install the file under the ``install`` rule.

```
@rm -f $(DESTDIR)$(PREFIX)/bin/test-z3$(EXE_EXT)
```
---
 scripts/mk_util.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 7bc68e193..8b75761fe 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1094,8 +1094,9 @@ class ExeComponent(Component):
             MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
 
     def mk_uninstall(self, out):
-        exefile = '%s$(EXE_EXT)' % self.exe_name
-        MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
+        if self.install:
+            exefile = '%s$(EXE_EXT)' % self.exe_name
+            MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:

From 6984070b3a742e9bccd65f9e2e2d447c3eecfe84 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:28:51 +0000
Subject: [PATCH 09/24] Fix typo (missing argument) that I missed that didn't
 fire because I did not test on Windows.

---
 scripts/mk_util.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 8b75761fe..5563c29a3 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1242,7 +1242,7 @@ class DLLComponent(Component):
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
-                MakeRuleCmd.install_files(dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
+                MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
                 # Compute the relative path from the python package directory

From 684318149b2112b0644473cb96f64024aedf8957 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 11:31:49 +0000
Subject: [PATCH 10/24] Remove dead code that I accidently left behind.

---
 scripts/mk_util.py | 1 -
 1 file changed, 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 5563c29a3..cd1dd9bd1 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1248,7 +1248,6 @@ class DLLComponent(Component):
                 # Compute the relative path from the python package directory
                 # to libz3. It's important that this symlink be relative
                 # (rather than absolute) so that the install is relocatable.
-                dllInstallPathAbs = os.path.join(PREFIX, dllInstallPath)
                 MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name

From 32c4384d4834c56f532386d2b133a92b57acd072 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 16:00:35 +0000
Subject: [PATCH 11/24] Fix dead comment and expand on the reasons for making a
 symbolic link slightly.

---
 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 cd1dd9bd1..fd8c713d4 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1245,9 +1245,9 @@ class DLLComponent(Component):
                 MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             else:
                 # Create symbolic link to save space.
-                # Compute the relative path from the python package directory
-                # to libz3. It's important that this symlink be relative
-                # (rather than absolute) so that the install is relocatable.
+                # 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))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name

From f1d4f36ddf3c1ec51cc5949a130231b77ba75648 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 18:50:02 +0000
Subject: [PATCH 12/24] Refactor the use of ``$(DESTDIR)$(PREFIX)`` in
 ``MakeRuleCmd`` class so that it is exposed via a public method
 (``install_root()``) so that is can be used externally. Also refactor the
 existing methods to use it.

---
 scripts/mk_util.py | 35 +++++++++++++++++++++++++++--------
 1 file changed, 27 insertions(+), 8 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index fd8c713d4..c6aedf6ff 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3227,15 +3227,27 @@ class MakeRuleCmd(object):
         to writing commands manually which can be error prone.
     """
     @classmethod
-    def install_files(cls, out, srcPattern, dest):
+    def install_root(cls):
+        """
+            Returns a string that will expand to the
+            install location when used in a makefile rule.
+        """
+        # Note: DESTDIR is to support staged installs
+        return "$(DESTDIR)$(PREFIX)/"
+
+    @classmethod
+    def install_files(cls, out, src_pattern, dest):
         assert len(dest) > 0
-        assert isinstance(srcPattern, str)
-        assert not ' ' in srcPattern
+        assert isinstance(src_pattern, str)
+        assert not ' ' in src_pattern
         assert isinstance(dest, str)
         assert not ' ' in dest
-        assert not os.path.isabs(srcPattern)
+        assert not os.path.isabs(src_pattern)
         assert not os.path.isabs(dest)
-        cls.write_cmd(out, "cp {} $(DESTDIR)$(PREFIX)/{}".format(srcPattern, dest))
+        cls.write_cmd(out, "cp {src_pattern} {install_root}{dest}".format(
+            src_pattern=src_pattern,
+            install_root=cls.install_root(),
+            dest=dest))
 
     @classmethod
     def remove_installed_files(cls, out, pattern):
@@ -3243,7 +3255,9 @@ class MakeRuleCmd(object):
         assert isinstance(pattern, str)
         assert not ' ' in pattern
         assert not os.path.isabs(pattern)
-        cls.write_cmd(out, "rm -f $(DESTDIR)$(PREFIX)/{}".format(pattern))
+        cls.write_cmd(out, "rm -f {install_root}{pattern}".format(
+            install_root=cls.install_root(),
+            pattern=pattern))
 
     @classmethod
     def make_install_directory(cls, out, dir):
@@ -3251,7 +3265,9 @@ class MakeRuleCmd(object):
         assert isinstance(dir, str)
         assert not ' ' in dir
         assert not os.path.isabs(dir)
-        cls.write_cmd(out, "mkdir -p $(DESTDIR)$(PREFIX)/{}".format(dir))
+        cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
+            install_root=cls.install_root(),
+            dir=dir))
 
     @classmethod
     def create_relative_symbolic_link(cls, out, target, link_name):
@@ -3296,7 +3312,10 @@ class MakeRuleCmd(object):
         assert isinstance(link_name, str)
         assert not os.path.isabs(target)
         assert not os.path.isabs(link_name)
-        cls.write_cmd(out, 'ln -s {} $(DESTDIR)$(PREFIX)/{}'.format(target, link_name))
+        cls.write_cmd(out, 'ln -s {target} {install_root}{link_name}'.format(
+            target=target,
+            install_root=cls.install_root(),
+            link_name=link_name))
 
     # TODO: Refactor all of the build system to emit commands using this
     # helper to simplify code. This will also let us replace ``@`` with

From d205b176e8bb725b6e14ef2482fd5873c378ed86 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 28 Nov 2015 18:53:42 +0000
Subject: [PATCH 13/24] Bug fix for
 ``MakeRuleCmd.create_relative_symbolic_link()``.

create_relative_symbolic_link(out, '/usr/lib64/libz3.so',
'/usr/lib/python3.5/site-package/libz3.so') would create an incorrect relative
path because it would consider ``/usr/lib`` to a be a path prefix of
``/usr/lib64``.
---
 scripts/mk_util.py | 23 ++++++++++++++++++++++-
 1 file changed, 22 insertions(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index c6aedf6ff..e166e8010 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -3269,6 +3269,27 @@ class MakeRuleCmd(object):
             install_root=cls.install_root(),
             dir=dir))
 
+    @classmethod
+    def _is_path_prefix_of(cls, temp_path, target_as_abs):
+        """
+            Returns True iff ``temp_path`` is a path prefix
+            of ``target_as_abs``
+        """
+        assert isinstance(temp_path, str)
+        assert isinstance(target_as_abs, str)
+        assert len(temp_path) > 0
+        assert len(target_as_abs) > 0
+        assert os.path.isabs(temp_path)
+        assert os.path.isabs(target_as_abs)
+
+        # Need to stick extra slash in front otherwise we might think that
+        # ``/lib`` is a prefix of ``/lib64``.  Of course if ``temp_path ==
+        # '/'`` then we shouldn't else we would check if ``//`` (rather than
+        # ``/``) is a prefix of ``/lib64``, which would fail.
+        if len(temp_path) > 1:
+            temp_path += os.sep
+        return target_as_abs.startswith(temp_path)
+
     @classmethod
     def create_relative_symbolic_link(cls, out, target, link_name):
         assert isinstance(target, str)
@@ -3294,7 +3315,7 @@ class MakeRuleCmd(object):
         assert os.path.isabs(temp_path)
         # Keep walking up the directory tree until temp_path
         # is a prefix of targetAsAbs
-        while not targetAsAbs.startswith(temp_path):
+        while not cls._is_path_prefix_of(temp_path, targetAsAbs):
             assert temp_path != '/'
             temp_path = os.path.dirname(temp_path)
             relative_path += '../'

From d2ba6f0ebfc4d4d5713926f00604ec39424463bb Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 28 Nov 2015 17:48:49 +0000
Subject: [PATCH 14/24] Provide a way to customise the install directories via
 environment variables:

Z3_INSTALL_BIN_DIR - defaults to "bin"
Z3_INSTALL_LIB_DIR - defaults to "lib"
Z3_INSTALL_INCLUDE_DIR - defaults to "include"

This has two advantages

* We no longer hard code strings like "bin" all over the place
* Packagers can easily control where things get installed.
---
 scripts/mk_util.py | 89 +++++++++++++++++++++++++---------------------
 1 file changed, 48 insertions(+), 41 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index e166e8010..d7021b570 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -34,6 +34,10 @@ OCAMLC=getenv("OCAMLC", "ocamlc")
 OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
 OCAML_LIB=getenv("OCAML_LIB", None)
 OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
+# Standard install directories relative to PREFIX
+INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
+INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
+INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
 
 CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
@@ -587,6 +591,9 @@ def display_help(exit_code):
     print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
     print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
     print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
+    print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
+    print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
+    print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
     exit(exit_code)
 
 # Parse configuration option for mk_make script
@@ -1004,18 +1011,18 @@ class LibComponent(Component):
             MakeRuleCmd.install_files(
                 out,
                 os.path.join(self.to_src_dir, include),
-                os.path.join('include', include)
+                os.path.join(INSTALL_INCLUDE_DIR, include)
             )
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            MakeRuleCmd.remove_installed_files(out, os.path.join('include', include))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_INCLUDE_DIR, include))
 
     def mk_win_dist(self, build_path, dist_path):
-        mk_dir(os.path.join(dist_path, 'include'))
+        mk_dir(os.path.join(dist_path, INSTALL_INCLUDE_DIR))
         for include in self.includes2install:
             shutil.copy(os.path.join(self.src_dir, include),
-                        os.path.join(dist_path, 'include', include))
+                        os.path.join(dist_path, INSTALL_INCLUDE_DIR, include))
 
     def mk_unix_dist(self, build_path, dist_path):
         self.mk_win_dist(build_path, dist_path)
@@ -1091,24 +1098,24 @@ class ExeComponent(Component):
     def mk_install(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            MakeRuleCmd.install_files(out, exefile, os.path.join('bin', exefile))
+            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, exefile))
 
     def mk_uninstall(self, out):
         if self.install:
             exefile = '%s$(EXE_EXT)' % self.exe_name
-            MakeRuleCmd.remove_installed_files(out, os.path.join('bin', exefile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_BIN_DIR, exefile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.exe' % os.path.join(build_path, self.exe_name),
-                        '%s.exe' % os.path.join(dist_path, 'bin', self.exe_name))
+                        '%s.exe' % os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
 
     def mk_unix_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy(os.path.join(build_path, self.exe_name),
-                        os.path.join(dist_path, 'bin', self.exe_name))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, self.exe_name))
 
 
 class ExtraExeComponent(ExeComponent):
@@ -1238,7 +1245,7 @@ class DLLComponent(Component):
     def mk_install(self, out):
         if self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            dllInstallPath = os.path.join('lib', dllfile)
+            dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
@@ -1251,32 +1258,32 @@ class DLLComponent(Component):
                 MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                MakeRuleCmd.install_files(out, libfile, os.path.join('lib', libfile))
+                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('lib', dllfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
         pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
         MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        MakeRuleCmd.remove_installed_files(out, os.path.join('lib', libfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
 
     def mk_win_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
-                        '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
             shutil.copy('%s.lib' % os.path.join(build_path, self.dll_name),
-                        '%s.lib' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.lib' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
     def mk_unix_dist(self, build_path, dist_path):
         if self.install:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             so = get_so_ext()
             shutil.copy('%s.%s' % (os.path.join(build_path, self.dll_name), so),
-                        '%s.%s' % (os.path.join(dist_path, 'bin', self.dll_name), so))
+                        '%s.%s' % (os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name), so))
             shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
-                        '%s.a' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
 class DotNetDLLComponent(Component):
     def __init__(self, name, dll_name, path, deps, assembly_info_dir):
@@ -1329,14 +1336,14 @@ class DotNetDLLComponent(Component):
     def mk_win_dist(self, build_path, dist_path):
         if DOTNET_ENABLED:
             # Assuming all DotNET dll should be in the distribution
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.dll' % os.path.join(build_path, self.dll_name),
-                        '%s.dll' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.dll' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
             shutil.copy('%s.xml' % os.path.join(build_path, self.dll_name),
-                        '%s.xml' % os.path.join(dist_path, 'bin', self.dll_name))
+                        '%s.xml' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
             if DEBUG_MODE:
                 shutil.copy('%s.pdb' % os.path.join(build_path, self.dll_name),
-                            '%s.pdb' % os.path.join(dist_path, 'bin', self.dll_name))
+                            '%s.pdb' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
 
 
@@ -1406,36 +1413,36 @@ class JavaDLLComponent(Component):
 
     def mk_win_dist(self, build_path, dist_path):
         if JAVA_ENABLED:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
-                        '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
+                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
             shutil.copy(os.path.join(build_path, 'libz3java.dll'),
-                        os.path.join(dist_path, 'bin', 'libz3java.dll'))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.dll'))
             shutil.copy(os.path.join(build_path, 'libz3java.lib'),
-                        os.path.join(dist_path, 'bin', 'libz3java.lib'))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.lib'))
 
     def mk_unix_dist(self, build_path, dist_path):
         if JAVA_ENABLED:
-            mk_dir(os.path.join(dist_path, 'bin'))
+            mk_dir(os.path.join(dist_path, INSTALL_BIN_DIR))
             shutil.copy('%s.jar' % os.path.join(build_path, self.package_name),
-                        '%s.jar' % os.path.join(dist_path, 'bin', self.package_name))
+                        '%s.jar' % os.path.join(dist_path, INSTALL_BIN_DIR, self.package_name))
             so = get_so_ext()
             shutil.copy(os.path.join(build_path, 'libz3java.%s' % so),
-                        os.path.join(dist_path, 'bin', 'libz3java.%s' % so))
+                        os.path.join(dist_path, INSTALL_BIN_DIR, 'libz3java.%s' % so))
 
     def mk_install(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.install_files(out, dllfile, os.path.join('lib', dllfile))
+            MakeRuleCmd.install_files(out, dllfile, os.path.join(INSTALL_LIB_DIR, dllfile))
             jarfile = '{}.jar'.format(self.package_name)
-            MakeRuleCmd.install_files(out, jarfile, os.path.join('lib', jarfile))
+            MakeRuleCmd.install_files(out, jarfile, os.path.join(INSTALL_LIB_DIR, jarfile))
 
     def mk_uninstall(self, out):
         if is_java_enabled() and self.install:
             dllfile = '%s$(SO_EXT)' % self.dll_name
-            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', dllfile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
             jarfile = '{}.jar'.format(self.package_name)
-            MakeRuleCmd.remove_installed_files(out, os.path.join('lib', jarfile))
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))
 
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
@@ -2034,9 +2041,9 @@ def mk_install(out):
     if is_ml_enabled() and OCAMLFIND != '':
         out.write('ocamlfind_install')
     out.write('\n')
-    MakeRuleCmd.make_install_directory(out, 'bin')
-    MakeRuleCmd.make_install_directory(out, 'include')
-    MakeRuleCmd.make_install_directory(out, 'lib')
+    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
     pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
     MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
     for c in get_components():
@@ -2055,7 +2062,7 @@ def mk_install(out):
         else:
             LD_LIBRARY_PATH = "LD_LIBRARY_PATH"
         out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
-                  (os.path.join(PREFIX, 'lib'), LD_LIBRARY_PATH))
+                  (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH))
         out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
     out.write('\n')
 
@@ -3206,7 +3213,7 @@ def mk_win_dist(build_path, dist_path):
     print("Adding to %s\n" % dist_path)
     for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
         shutil.copy(os.path.join(build_path, pyc),
-                    os.path.join(dist_path, 'bin', pyc))
+                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
 
 def mk_unix_dist(build_path, dist_path):
     for c in get_components():
@@ -3214,7 +3221,7 @@ def mk_unix_dist(build_path, dist_path):
     # Add Z3Py to bin directory
     for pyc in filter(lambda f: f.endswith('.pyc') or f.endswith('.py'), os.listdir(build_path)):
         shutil.copy(os.path.join(build_path, pyc),
-                    os.path.join(dist_path, 'bin', pyc))
+                    os.path.join(dist_path, INSTALL_BIN_DIR, pyc))
 
 class MakeRuleCmd(object):
     """

From 6884d3a245d59e7f8c02133c1ffa1fc2b60061b3 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Sat, 5 Dec 2015 07:50:33 +0000
Subject: [PATCH 15/24] Fix references to non existent function and variable
 due to a refactor in 041c02feb7aa682ecc887a2a1064b5729c68a5b4. Spotted by
 @NikolajBjorner

---
 scripts/mk_util.py | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index d7021b570..3e5590d5e 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -671,12 +671,11 @@ def parse_options():
     # Handle the Python package directory
     if not IS_WINDOWS:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            printPythonPackageMessage("ERROR")
             print(("ERROR: The detected Python package directory (%s)"
                    " does not live under the installation prefix (%s)"
                    ". This would lead to a broken installation."
                    "Use --pypkgdir= to change the Python package directory") %
-                  (errorType, PYTHON_PACKAGE_DIR, PREFIX))
+                  (PYTHON_PACKAGE_DIR, PREFIX))
             sys.exit(1)
 
 # Return a list containing a file names included using '#include' in

From 61d1cd524ea1cfd73b0554071ebdb7b891701b4a Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Wed, 25 Nov 2015 18:33:59 +0000
Subject: [PATCH 16/24] Teach the build system to build and install the ".NET
 bindings" under non Windows systems (i.e. Using mono).

Building these bindings is unfortunately on by default because
I didn't want to change the command line interface (i.e. ``--nodotnet``)
which people might be relying on. This should really be changed to
match the other binding flags (e.g. ``--java``) but I will leave
this for now.

To perform the build a C# compiler and the GAC utility are required.
The script will try to automatically detect them but the user can
override this by setting the ``CSC`` and ``GACUTIL`` environment
variables.

In order for the ".NET bindings" to be installed the assembly
(``Microsoft.Z3.dll``) needs to have a strong name which means
we need a Strong name key file which is what the
``Microsoft.Z3.mono.snk`` is for. This is the public and private
key so this key **must never** be used for checking integrity. Instead its
only purpose is to avoid any name clashes in the GAC.

It is also worth noting that slightly different flags needs to
be passed to the C# compiler on non Windows platforms. I don't
understand why some of the flags are being used on Windows but I left
a comment there that hopefully someone can fix...
---
 scripts/mk_util.py                   | 203 ++++++++++++++++++++++-----
 src/api/dotnet/Microsoft.Z3.mono.snk | Bin 0 -> 596 bytes
 2 files changed, 167 insertions(+), 36 deletions(-)
 create mode 100644 src/api/dotnet/Microsoft.Z3.mono.snk

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 3e5590d5e..4c959d0af 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -34,6 +34,8 @@ OCAMLC=getenv("OCAMLC", "ocamlc")
 OCAMLOPT=getenv("OCAMLOPT", "ocamlopt")
 OCAML_LIB=getenv("OCAML_LIB", None)
 OCAMLFIND=getenv("OCAMLFIND", "ocamlfind")
+CSC=getenv("CSC", None)
+GACUTIL=getenv("GACUTIL", None)
 # Standard install directories relative to PREFIX
 INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
 INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
@@ -71,7 +73,7 @@ ONLY_MAKEFILES = False
 Z3PY_SRC_DIR=None
 VS_PROJ = False
 TRACE = False
-DOTNET_ENABLED=False
+DOTNET_ENABLED=True
 JAVA_ENABLED=False
 ML_ENABLED=False
 STATIC_LIB=False
@@ -143,6 +145,7 @@ def which(program):
             exe_file = os.path.join(path, program)
             if is_exe(exe_file):
                 return exe_file
+    return None
 
 class TempFile:
     def __init__(self, name):
@@ -388,6 +391,43 @@ def check_java():
         if JNI_HOME is None:
             raise MKException("Failed to detect jni.h. Possible solution: set JNI_HOME with the path to JDK.")
 
+def check_dotnet():
+    global CSC, GACUTIL
+    if IS_WINDOWS:
+        # Apparently building the dotnet bindings worked fine before
+        # so don't bother to try to detect anything
+        # FIXME: Shouldn't we be checking the supported version of .NET
+        # or something!?
+        if CSC == None:
+            CSC='csc.exe'
+        return
+
+    # Check for the mono compiler
+    if CSC == None:
+        monoCompilerExecutable = 'mcs'
+    else:
+        monoCompilerExecutable = CSC
+    monoCompilerPath = which(monoCompilerExecutable)
+    if monoCompilerPath == None:
+        print(("ERROR: Could not find mono compiler ({}) in your PATH. "
+              "Either install it or disable building the dotnet bindings.").format(
+              monoCompilerExecutable))
+        sys.exit(1)
+    CSC = monoCompilerPath
+
+    # Check for gacutil (needed to install the dotnet bindings)
+    if GACUTIL == None:
+        gacutilExecutable = 'gacutil'
+    else:
+        gacutilExecutable = GACUTIL
+    gacutilPath = which(gacutilExecutable)
+    if gacutilPath == None:
+        print(("ERROR: Could not find the gacutil ({}) in your PATH. "
+               "Either install it or disable building the dotnet bindings.").format(
+               gacutilExecutable))
+        sys.exit(1)
+    GACUTIL = gacutilPath
+
 def check_ml():
     t = TempFile('hello.ml')
     t.add('print_string "Hello world!\n";;')
@@ -532,8 +572,6 @@ if os.name == 'nt':
     IS_WINDOWS=True
     # Visual Studio already displays the files being compiled
     SHOW_CPPS=False
-    # Enable .Net bindings by default on windows
-    DOTNET_ENABLED=True
 elif os.name == 'posix':
     if os.uname()[0] == 'Darwin':
         IS_OSX=True
@@ -566,8 +604,7 @@ def display_help(exit_code):
     print("  -m, --makefiles               generate only makefiles.")
     if IS_WINDOWS:
         print("  -v, --vsproj                  generate Visual Studio Project Files.")
-    if IS_WINDOWS:
-        print("  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules.")
+    print("  -n, --nodotnet                do not generate Microsoft.Z3.dll make rules.")
     if IS_WINDOWS:
         print("  --optimize                    generate optimized code during linking.")
     print("  -j, --java                    generate Java bindings.")
@@ -591,6 +628,8 @@ def display_help(exit_code):
     print("  OCAMLC     Ocaml byte-code compiler (only relevant with --ml)")
     print("  OCAMLOPT   Ocaml native compiler (only relevant with --ml)")
     print("  OCAML_LIB  Ocaml library directory (only relevant with --ml)")
+    print("  CSC        C# Compiler (only relevant if dotnet bindings are enabled)")
+    print("  GACUTIL    GAC Utility (only relevant if dotnet bindings are enabled)")
     print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
     print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
     print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
@@ -764,6 +803,9 @@ def is_java_enabled():
 def is_ml_enabled():
     return ML_ENABLED
 
+def is_dotnet_enabled():
+    return DOTNET_ENABLED
+
 def is_compiler(given, expected):
     """
     Return True if the 'given' compiler is the expected one.
@@ -1295,36 +1337,86 @@ class DotNetDLLComponent(Component):
         self.assembly_info_dir = assembly_info_dir
 
     def mk_makefile(self, out):
-        if DOTNET_ENABLED:
-            cs_fp_files = []
-            cs_files    = []
-            for cs_file in get_cs_files(self.src_dir):
-                cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
-                cs_files.append(cs_file)
-            if self.assembly_info_dir != '.':
-                for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
-                    cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
-                    cs_files.append(os.path.join(self.assembly_info_dir, cs_file))
-            dllfile = '%s.dll' % self.dll_name
-            out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
-            for cs_file in cs_fp_files:
-                out.write(' ')
-                out.write(cs_file)
-            out.write('\n')
-            out.write('  csc /noconfig /unsafe+ /nowarn:1701,1702 /nostdlib+ /errorreport:prompt /warn:4 /reference:mscorlib.dll /reference:System.Core.dll /reference:System.dll /reference:System.Numerics.dll /filealign:512 /linkresource:%s.dll /out:%s.dll /target:library /doc:%s.xml' % (get_component(Z3_DLL_COMPONENT).dll_name, self.dll_name, self.dll_name))
-            if DEBUG_MODE:
-                out.write(' /define:DEBUG;TRACE /debug+ /debug:full /optimize-')
-            else:
-                out.write(' /optimize+')
-            if VS_X64:
-                out.write(' /platform:x64')
-            else:
-                out.write(' /platform:x86')
-            for cs_file in cs_files:
-                out.write(' %s' % os.path.join(self.to_src_dir, cs_file))
-            out.write('\n')
-            out.write('%s: %s\n\n' % (self.name, dllfile))
+        if not DOTNET_ENABLED:
             return
+        cs_fp_files = []
+        cs_files    = []
+        for cs_file in get_cs_files(self.src_dir):
+            cs_fp_files.append(os.path.join(self.to_src_dir, cs_file))
+            cs_files.append(cs_file)
+        if self.assembly_info_dir != '.':
+            for cs_file in get_cs_files(os.path.join(self.src_dir, self.assembly_info_dir)):
+                cs_fp_files.append(os.path.join(self.to_src_dir, self.assembly_info_dir, cs_file))
+                cs_files.append(os.path.join(self.assembly_info_dir, cs_file))
+        dllfile = '%s.dll' % self.dll_name
+        out.write('%s: %s$(SO_EXT)' % (dllfile, get_component(Z3_DLL_COMPONENT).dll_name))
+        for cs_file in cs_fp_files:
+            out.write(' ')
+            out.write(cs_file)
+        out.write('\n')
+
+        cscCmdLine = [CSC]
+        if IS_WINDOWS:
+            # Using these flags under the mono compiler results in build errors.
+            cscCmdLine.extend( [# What is the motivation for this?
+                                '/noconfig+',
+                                '/nostdlib+',
+                                '/reference:mscorlib.dll',
+                                # Under mono this isn't neccessary as mono will search the system
+                                # library paths for libz3.so
+                                '/linkresource:{}.dll'.format(get_component(Z3_DLL_COMPONENT).dll_name),
+                               ]
+                             )
+        else:
+            # We need to give the assembly a strong name so that it
+            # can be installed into the GAC with ``make install``
+            pathToSnk = os.path.join(self.to_src_dir, 'Microsoft.Z3.mono.snk')
+            cscCmdLine.append('/keyfile:{}'.format(pathToSnk))
+
+        cscCmdLine.extend( ['/unsafe+',
+                            '/nowarn:1701,1702',
+                            '/errorreport:prompt',
+                            '/warn:4',
+                            '/reference:System.Core.dll',
+                            '/reference:System.dll',
+                            '/reference:System.Numerics.dll',
+                            '/filealign:512', # Why!?
+                            '/out:{}.dll'.format(self.dll_name),
+                            '/target:library',
+                            '/doc:{}.xml'.format(self.dll_name),
+                           ]
+                         )
+        if DEBUG_MODE:
+            cscCmdLine.extend( ['/define:DEBUG;TRACE',
+                                '/debug+',
+                                '/debug:full',
+                                '/optimize-'
+                               ]
+                             )
+        else:
+            cscCmdLine.extend(['/optimize+'])
+        if IS_WINDOWS:
+            if VS_X64:
+                cscCmdLine.extend(['/platform:x64'])
+            else:
+                cscCmdLine.extend(['/platform:x86'])
+        else:
+            # Just use default platform for now.
+            # If the dlls are run using mono then it
+            # ignores what the platform is set to anyway.
+            pass
+
+        for cs_file in cs_files:
+            cscCmdLine.append('{}'.format(os.path.join(self.to_src_dir, cs_file)))
+
+        # Now emit the command line
+        MakeRuleCmd.write_cmd(out, ' '.join(cscCmdLine))
+
+        # State that the high-level "dotnet" target depends on the .NET bindings
+        # dll we just created the build rule for
+        out.write('\n')
+        out.write('%s: %s\n\n' % (self.name, dllfile))
+        return
 
     def main_component(self):
         return DOTNET_ENABLED
@@ -1350,6 +1442,40 @@ class DotNetDLLComponent(Component):
         # Do nothing
         return
 
+    def mk_install_deps(self, out):
+        if not DOTNET_ENABLED:
+            return
+        out.write('%s' % self.name)
+
+    def _install_or_uninstall_to_gac(self, out, install):
+        gacUtilFlags = ['/package {}'.format(self.dll_name),
+                        '/root',
+                        '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR)
+                       ]
+        if install:
+            install_or_uninstall_flag = '-i'
+        else:
+            # Note need use ``-us`` here which takes an assembly file name
+            # rather than ``-u`` which takes an assembly display name (e.g.
+            #  )
+            install_or_uninstall_flag = '-us'
+        MakeRuleCmd.write_cmd(out, '{gacutil} {install_or_uninstall_flag} {assembly_name}.dll -f {flags}'.format(
+            gacutil=GACUTIL,
+            install_or_uninstall_flag=install_or_uninstall_flag,
+            assembly_name=self.dll_name,
+            flags=' '.join(gacUtilFlags)))
+
+    def mk_install(self, out):
+        if not DOTNET_ENABLED or IS_WINDOWS:
+            return
+        self._install_or_uninstall_to_gac(out, install=True)
+
+
+    def mk_uninstall(self, out):
+        if not DOTNET_ENABLED or IS_WINDOWS:
+            return
+        self._install_or_uninstall_to_gac(out, install=False)
+
 class JavaDLLComponent(Component):
     def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
         Component.__init__(self, name, path, deps)
@@ -1662,7 +1788,7 @@ class DotNetExampleComponent(ExampleComponent):
                 out.write(' ')
                 out.write(os.path.join(self.to_ex_dir, csfile))
             out.write('\n')
-            out.write('\tcsc /out:%s /reference:%s /debug:full /reference:System.Numerics.dll' % (exefile, dll))
+            out.write('\t%s /out:%s /reference:%s /debug:full /reference:System.Numerics.dll' % (CSC, exefile, dll))
             if VS_X64:
                 out.write(' /platform:x64')
             else:
@@ -2029,6 +2155,9 @@ def mk_config():
                 print('OCaml Compiler: %s' % OCAMLC)
                 print('OCaml Native:   %s' % OCAMLOPT)
                 print('OCaml Library:  %s' % OCAML_LIB)
+            if is_dotnet_enabled():
+                print('C# Compiler:    %s' % CSC)
+                print('GAC utility:    %s' % GACUTIL)
 
     config.close()
 
@@ -2603,7 +2732,6 @@ def cp_z3py_to_build():
 def mk_bindings(api_files):
     if not ONLY_MAKEFILES:
         mk_z3consts_py(api_files)
-        mk_z3consts_dotnet(api_files)
         new_api_files = []
         api = get_component(API_COMPONENT)
         for api_file in api_files:
@@ -2619,6 +2747,9 @@ def mk_bindings(api_files):
         if is_ml_enabled():
             check_ml()
             mk_z3consts_ml(api_files)
+        if is_dotnet_enabled():
+            check_dotnet()
+            mk_z3consts_dotnet(api_files)
 
 # Extract enumeration types from API files, and add python definitions.
 def mk_z3consts_py(api_files):
diff --git a/src/api/dotnet/Microsoft.Z3.mono.snk b/src/api/dotnet/Microsoft.Z3.mono.snk
new file mode 100644
index 0000000000000000000000000000000000000000..bfd0b3fce33b18365bd122d6a0d62ff6d3009d9c
GIT binary patch
literal 596
zcmV-a0;~N80ssI2Bme+XQ$aES1ONaL0001Y34hdwvy+iiZ#CZ+ujhi)%r=<6Q8y{p
zWd(E&Kd0wt3Gt#xDja-EY{bN8$?%f*Rp`ZE>13cTF5+QMo#08Lf2%cIGKqZ`K@4-+
zTsjW>z5Q=C!`0b2I^O^9xuwZgq@m6o0~CGwC7U}EXF#LI{aB?AFSD)=GNImE@n47~
zNfnUXCH#^;ihK;ZpH4gXY6$99SG%}$g$X)=M29Z?DsM9Xid1^sFniHkOAny+!WZU5
zv@$Vn;aJ~QDk_p|YrCkbZcQ|OhS7JHvo?JOn~$4$*ben1%g8fHQm<11=P#P?n8HL%
zCbebljs}XZIdt6+=HHQtn)3I<dfM(~_qv4U&hOuf3XbJtn2#^PYV%_3RdZA#2|qq!
zP_GRvlma|>zxpGLJ0!*4%1>)`S7G?b_#L!sU{>e8SN$prW{{PZI%Uww-Cr=*B1%Hm
z6<bm<2{rnBTzM*xE4P*65YB!ie&3vAGOGyKcmp~w#CfsId1rd=Z-BpNs&js3rI|~F
zGv(Cf%05+#Ic4?n0KZ~A8hNO1O&e*E_h<oZVSG2JhXrhqPxN21_Fr9CiUCvACj!fh
z!Z>HcqPj(4hdqKzWmY)bnL<rB^IkZ$&HHa-br-X5_yX1H!Y6*b!0(m;#sQ93>Dd!j
zMNM!Wwmxd*8!TNDY;m|h{ih0qrCNLuT_OLx+KU-Ys3Rlb72$ziy_Ny1G7=uXUmQ5K
i?izOc;@RNPcI)<yQLRXGJMz$~A0f7k^G5@>+#xXX8XY(Q

literal 0
HcmV?d00001


From c8a2b6645a96ca20fe38cf80f1550a008640db20 Mon Sep 17 00:00:00 2001
From: Dan Liew <daniel.liew@imperial.ac.uk>
Date: Thu, 26 Nov 2015 17:34:02 +0000
Subject: [PATCH 17/24] Teach the build system to generate and install a
 pkg-config file for the ".NET" bindings. This file is required for
 Monodevelop to find the bindings because Monodevelop uses pkg-config to find
 packages (it doesn't use the GAC).

For lack of a better name the GAC (and pkg-config) package name is now
``Microsoft.Z3.Sharp``. I don't want to call it ``Microsoft.Z3`` because
someone may want to create a ``Microsoft.Z3.pc`` file in the future for
the native Z3 library (i.e. C++ or C bindings).

In addition there is a new utility function ``configure_file()``
which reads a template file, applies some substitutions and writes
the result to another file. This very similar to what CMake does.

There is a new environment variable ``Z3_INSTALL_PKGCONFIG_DIR``
which allows pkgconfig directory to be controlled for the install.
---
 scripts/mk_util.py                      | 75 ++++++++++++++++++++++++-
 src/api/dotnet/Microsoft.Z3.Sharp.pc.in |  7 +++
 2 files changed, 81 insertions(+), 1 deletion(-)
 create mode 100644 src/api/dotnet/Microsoft.Z3.Sharp.pc.in

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 4c959d0af..e882e4a39 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -40,6 +40,7 @@ GACUTIL=getenv("GACUTIL", None)
 INSTALL_BIN_DIR=getenv("Z3_INSTALL_BIN_DIR", "bin")
 INSTALL_LIB_DIR=getenv("Z3_INSTALL_LIB_DIR", "lib")
 INSTALL_INCLUDE_DIR=getenv("Z3_INSTALL_INCLUDE_DIR", "include")
+INSTALL_PKGCONFIG_DIR=getenv("Z3_INSTALL_PKGCONFIG_DIR", os.path.join(INSTALL_LIB_DIR, 'pkgconfig'))
 
 CXX_COMPILERS=['g++', 'clang++']
 C_COMPILERS=['gcc', 'clang']
@@ -633,6 +634,7 @@ def display_help(exit_code):
     print("  Z3_INSTALL_BIN_DIR Install directory for binaries relative to install prefix")
     print("  Z3_INSTALL_LIB_DIR Install directory for libraries relative to install prefix")
     print("  Z3_INSTALL_INCLUDE_DIR Install directory for header files relative to install prefix")
+    print("  Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
     exit(exit_code)
 
 # Parse configuration option for mk_make script
@@ -1336,6 +1338,29 @@ class DotNetDLLComponent(Component):
         self.dll_name          = dll_name
         self.assembly_info_dir = assembly_info_dir
 
+    def mk_pkg_config_file(self):
+        """
+            Create pkgconfig file for the dot net bindings. These
+            are needed by Monodevelop.
+        """
+        pkg_config_template = os.path.join(self.src_dir, '{}.pc.in'.format(self.gac_pkg_name()))
+        substitutions = { 'PREFIX': PREFIX,
+                          'GAC_PKG_NAME': self.gac_pkg_name(),
+                          'VERSION': "{}.{}.{}.{}".format(
+                              VER_MAJOR,
+                              VER_MINOR,
+                              VER_BUILD,
+                              VER_REVISION)
+                        }
+        pkg_config_output = os.path.join(BUILD_DIR,
+                                       self.build_dir,
+                                       '{}.pc'.format(self.gac_pkg_name()))
+
+        # FIXME: Why isn't the build directory available?
+        mk_dir(os.path.dirname(pkg_config_output))
+        # Configure file that will be installed by ``make install``.
+        configure_file(pkg_config_template, pkg_config_output, substitutions)
+
     def mk_makefile(self, out):
         if not DOTNET_ENABLED:
             return
@@ -1416,6 +1441,9 @@ class DotNetDLLComponent(Component):
         # dll we just created the build rule for
         out.write('\n')
         out.write('%s: %s\n\n' % (self.name, dllfile))
+
+        # Create pkg-config file
+        self.mk_pkg_config_file()
         return
 
     def main_component(self):
@@ -1447,8 +1475,11 @@ class DotNetDLLComponent(Component):
             return
         out.write('%s' % self.name)
 
+    def gac_pkg_name(self):
+        return "{}.Sharp".format(self.dll_name)
+
     def _install_or_uninstall_to_gac(self, out, install):
-        gacUtilFlags = ['/package {}'.format(self.dll_name),
+        gacUtilFlags = ['/package {}'.format(self.gac_pkg_name()),
                         '/root',
                         '{}{}'.format(MakeRuleCmd.install_root(), INSTALL_LIB_DIR)
                        ]
@@ -1470,11 +1501,18 @@ class DotNetDLLComponent(Component):
             return
         self._install_or_uninstall_to_gac(out, install=True)
 
+        # Install pkg-config file. Monodevelop needs this to find Z3
+        pkg_config_output = os.path.join(self.build_dir,
+                                         '{}.pc'.format(self.gac_pkg_name()))
+        MakeRuleCmd.make_install_directory(out, INSTALL_PKGCONFIG_DIR)
+        MakeRuleCmd.install_files(out, pkg_config_output, INSTALL_PKGCONFIG_DIR)
 
     def mk_uninstall(self, out):
         if not DOTNET_ENABLED or IS_WINDOWS:
             return
         self._install_or_uninstall_to_gac(out, install=False)
+        pkg_config_file = os.path.join('lib','pkgconfig','{}.pc'.format(self.gac_pkg_name()))
+        MakeRuleCmd.remove_installed_files(out, pkg_config_file)
 
 class JavaDLLComponent(Component):
     def __init__(self, name, dll_name, package_name, manifest_file, path, deps):
@@ -3494,6 +3532,41 @@ def strip_path_prefix(path, prefix):
     assert not os.path.isabs(stripped_path)
     return stripped_path
 
+def configure_file(template_file_path, output_file_path, substitutions):
+    """
+        Read a template file ``template_file_path``, perform substitutions
+        found in the ``substitutions`` dictionary and write the result to
+        the output file ``output_file_path``.
+
+        The template file should contain zero or more template strings of the
+        form ``@NAME@``.
+
+        The substitutions dictionary maps old strings (without the ``@``
+        symbols) to their replacements.
+    """
+    assert isinstance(template_file_path, str)
+    assert isinstance(output_file_path, str)
+    assert isinstance(substitutions, dict)
+    assert len(template_file_path) > 0
+    assert len(output_file_path) > 0
+    print("Generating {} from {}".format(output_file_path, template_file_path))
+
+    if not os.path.exists(template_file_path):
+        raise MKException('Could not find template file "{}"'.format(template_file_path))
+
+    # Read whole template file into string
+    template_string = None
+    with open(template_file_path, 'r') as f:
+        template_string = f.read()
+
+    # Do replacements
+    for (old_string, replacement) in substitutions.items():
+        template_string = template_string.replace('@{}@'.format(old_string), replacement)
+
+    # Write the string to the file
+    with open(output_file_path, 'w') as f:
+        f.write(template_string)
+
 if __name__ == '__main__':
     import doctest
     doctest.testmod()
diff --git a/src/api/dotnet/Microsoft.Z3.Sharp.pc.in b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in
new file mode 100644
index 000000000..8ca4e788b
--- /dev/null
+++ b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in
@@ -0,0 +1,7 @@
+prefix=@PREFIX@
+assemblies_dir=${prefix}/lib/mono/@GAC_PKG_NAME@
+
+Name: @GAC_PKG_NAME@
+Description: .NET bindings for The Microsoft Z3 SMT solver
+Version: @VERSION@
+Libs: -r:${assemblies_dir}/Microsoft.Z3.dll

From ced9ba17e98cecbe574bcc92978e765f3269c7ab Mon Sep 17 00:00:00 2001
From: Andres Notzli <andres.noetzli@gmail.com>
Date: Sun, 6 Dec 2015 19:00:17 -0800
Subject: [PATCH 18/24] Fix misc issues in Python API docstrings

---
 src/api/python/z3.py | 37 ++++++++++++++++++++-----------------
 1 file changed, 20 insertions(+), 17 deletions(-)

diff --git a/src/api/python/z3.py b/src/api/python/z3.py
index f4e5d8941..27bfa6590 100644
--- a/src/api/python/z3.py
+++ b/src/api/python/z3.py
@@ -8189,7 +8189,7 @@ def is_fprm_value(a):
 class FPNumRef(FPRef):
     def isNaN(self):
         return self.decl().kind() == Z3_OP_FPA_NAN
-    
+
     def isInf(self):
         return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF
 
@@ -8201,7 +8201,7 @@ class FPNumRef(FPRef):
         return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True)
 
     """
-    The sign of the numeral
+    The sign of the numeral.
 
     >>> x = FPNumRef(+1.0, FPSort(8, 24))
     >>> x.sign()
@@ -8215,30 +8215,32 @@ class FPNumRef(FPRef):
         if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False:
             raise Z3Exception("error retrieving the sign of a numeral.")
         return l.value != 0
-    
+
     """
-    The significand of the numeral
+    The significand of the numeral.
 
     >>> x = FPNumRef(2.5, FPSort(8, 24))
+    >>> x.significand()
     1.25
     """
     def significand(self):
         return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast())
 
     """
-    The exponent of the numeral
+    The exponent of the numeral.
 
     >>> x = FPNumRef(2.5, FPSort(8, 24))
-    >>> 
+    >>> x.exponent()
     1
     """
     def exponent(self):
         return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast())
 
     """
-    The exponent of the numeral as a long
+    The exponent of the numeral as a long.
 
     >>> x = FPNumRef(2.5, FPSort(8, 24))
+    >>> x.exponent_as_long()
     1
     """
     def exponent_as_long(self):
@@ -8246,11 +8248,12 @@ class FPNumRef(FPRef):
         if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr):
             raise Z3Exception("error retrieving the exponent of a numeral.") 
         return ptr[0]
-    
+
     """
-    The string representation of the numeral
+    The string representation of the numeral.
 
     >>> x = FPNumRef(20, FPSort(8, 24))
+    >>> x.as_string()
     1.25*(2**4)
     """
     def as_string(self):
@@ -8378,7 +8381,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None):
     val = val + 'p'
     val = val + _to_int_str(exp)
     return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx)
-        
+
 def FP(name, fpsort, ctx=None):
     """Return a floating-point constant named `name`. 
     `fpsort` is the floating-point sort.
@@ -8640,47 +8643,47 @@ def fpIsNaN(a):
     return FPRef(Z3_mk_fpa_is_nan(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsInfinite(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isInfinite expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_infinite(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsZero(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isZero expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_zero(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsNormal(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isNormal expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_normal(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsSubnormal(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isSubnormal expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_subnormal(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsNegative(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isNegative expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_negative(a.ctx_ref(), a.as_ast()), a.ctx) 
 
 def fpIsPositive(a):
-    """Create a Z3 floating-point isNaN expression.
+    """Create a Z3 floating-point isPositive expression.
     """
     if __debug__:        
         _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions")
     return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) 
-    
+
 def _check_fp_args(a, b):
     if __debug__:
         _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression")

From 6c73c176b31dc08787900b15fbf08fd60c38c1e0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 19:10:11 -0800
Subject: [PATCH 19/24] make dotnet optional and recover from python
 installation mismatch. Pull requests #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_project.py |  1 +
 scripts/mk_util.py    | 91 +++++++++++++++++++++++++++++--------------
 2 files changed, 63 insertions(+), 29 deletions(-)

diff --git a/scripts/mk_project.py b/scripts/mk_project.py
index 439843e08..a9aaa9791 100644
--- a/scripts/mk_project.py
+++ b/scripts/mk_project.py
@@ -91,6 +91,7 @@ def init_project_def():
     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()
     # 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 e882e4a39..00db88d30 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -77,6 +77,7 @@ TRACE = False
 DOTNET_ENABLED=True
 JAVA_ENABLED=False
 ML_ENABLED=False
+PYTHON_INSTALL_ENABLED=True
 STATIC_LIB=False
 VER_MAJOR=None
 VER_MINOR=None
@@ -410,10 +411,10 @@ def check_dotnet():
         monoCompilerExecutable = CSC
     monoCompilerPath = which(monoCompilerExecutable)
     if monoCompilerPath == None:
-        print(("ERROR: Could not find mono compiler ({}) in your PATH. "
-              "Either install it or disable building the dotnet bindings.").format(
+	disable_dotnet()
+	print(("Could not find mono compiler ({}) in your PATH. Not building .NET bindings").format(
               monoCompilerExecutable))
-        sys.exit(1)
+	return
     CSC = monoCompilerPath
 
     # Check for gacutil (needed to install the dotnet bindings)
@@ -641,7 +642,7 @@ def display_help(exit_code):
 def parse_options():
     global VERBOSE, DEBUG_MODE, IS_WINDOWS, VS_X64, ONLY_MAKEFILES, SHOW_CPPS, VS_PROJ, TRACE, VS_PAR, VS_PAR_NUM
     global DOTNET_ENABLED, JAVA_ENABLED, ML_ENABLED, STATIC_LIB, PREFIX, GMP, FOCI2, FOCI2LIB, PYTHON_PACKAGE_DIR, GPROF, GIT_HASH
-    global LINUX_X64, SLOW_OPTIMIZE, USE_OMP
+    global LINUX_X64, SLOW_OPTIMIZE, USE_OMP, PYTHON_INSTALL_ENABLED
     try:
         options, remainder = getopt.gnu_getopt(sys.argv[1:],
                                                'b:df:sxhmcvtnp:gj',
@@ -710,14 +711,16 @@ def parse_options():
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
     # Handle the Python package directory
-    if not IS_WINDOWS:
+    if IS_WINDOWS:
+        PYTHON_INSTALL_ENABLED = False
+    else:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
-            print(("ERROR: The detected Python package directory (%s)"
+            print(("Warning: The detected Python package directory (%s)"
                    " does not live under the installation prefix (%s)"
-                   ". This would lead to a broken installation."
+                   ". This would lead to a broken Python installation."
                    "Use --pypkgdir= to change the Python package directory") %
                   (PYTHON_PACKAGE_DIR, PREFIX))
-            sys.exit(1)
+            PYTHON_INSTALL_ENABLED = False
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -808,6 +811,10 @@ def is_ml_enabled():
 def is_dotnet_enabled():
     return DOTNET_ENABLED
 
+def disable_dotnet():
+    global DOTNET_ENABLED
+    DOTNET_ENABLED = False
+
 def is_compiler(given, expected):
     """
     Return True if the 'given' compiler is the expected one.
@@ -1328,6 +1335,49 @@ class DLLComponent(Component):
             shutil.copy('%s.a' % os.path.join(build_path, self.dll_name),
                         '%s.a' % os.path.join(dist_path, INSTALL_BIN_DIR, self.dll_name))
 
+class PythonInstallComponent(Component):
+    def __init__(self, name):
+        Component.__init__(self, name, None, [])
+
+    def main_component(self):
+        return PYTHON_INSTALL_ENABLED
+
+    def install_deps(self, out):
+        if not self.main_component():
+             return
+        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+        MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
+
+    def mk_install(self, out):
+        if not self.main_component():
+            return
+        MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
+        if sys.version >= "3":
+            pythonPycacheDir = os.path.join(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)
+        if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
+            if os.uname()[0] == 'Darwin':
+                LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH"
+            else:
+                LD_LIBRARY_PATH = "LD_LIBRARY_PATH"
+            out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
+                      (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH))
+            out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
+
+    def mk_uninstall(self, out):
+        if not self.main_component():
+            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')))
+
+    def mk_makefile(self, out):
+        return
+
 class DotNetDLLComponent(Component):
     def __init__(self, name, dll_name, path, deps, assembly_info_dir):
         Component.__init__(self, name, path, deps)
@@ -1950,6 +2000,10 @@ 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():
+    name = 'python_install'
+    reg_component(name, PythonInstallComponent(name))
+
 def add_ml_lib(name, deps=[], path=None, lib_name=None):
     c = MLComponent(name, lib_name, path, deps)
     reg_component(name, c)
@@ -2210,36 +2264,15 @@ def mk_install(out):
     MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
     MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
     MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
-    pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
-    MakeRuleCmd.make_install_directory(out, pythonPkgDirWithoutPrefix)
     for c in get_components():
         c.mk_install(out)
-    MakeRuleCmd.install_files(out, 'z3*.py', pythonPkgDirWithoutPrefix)
-    if sys.version >= "3":
-        pythonPycacheDir = os.path.join(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)
     out.write('\t@echo Z3 was successfully installed.\n')
-    if PYTHON_PACKAGE_DIR != distutils.sysconfig.get_python_lib():
-        if os.uname()[0] == 'Darwin':
-            LD_LIBRARY_PATH = "DYLD_LIBRARY_PATH"
-        else:
-            LD_LIBRARY_PATH = "LD_LIBRARY_PATH"
-        out.write('\t@echo Z3 shared libraries were installed at \'%s\', make sure this directory is in your %s environment variable.\n' %
-                  (os.path.join(PREFIX, INSTALL_LIB_DIR), LD_LIBRARY_PATH))
-        out.write('\t@echo Z3Py was installed at \'%s\', make sure this directory is in your PYTHONPATH environment variable.' % PYTHON_PACKAGE_DIR)
     out.write('\n')
 
 def mk_uninstall(out):
     out.write('uninstall:\n')
     for c in get_components():
         c.mk_uninstall(out)
-    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')))
     out.write('\t@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 

From a9402303017052abc8b84fed6ff14641c42c8532 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 19:14:53 -0800
Subject: [PATCH 20/24] make dotnet optional and recover from python
 installation mismatch. Pull requests #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_util.py | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 00db88d30..47d60b2b3 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1434,7 +1434,7 @@ class DotNetDLLComponent(Component):
         if IS_WINDOWS:
             # Using these flags under the mono compiler results in build errors.
             cscCmdLine.extend( [# What is the motivation for this?
-                                '/noconfig+',
+                                '/noconfig',
                                 '/nostdlib+',
                                 '/reference:mscorlib.dll',
                                 # Under mono this isn't neccessary as mono will search the system

From febd83912e697e652a63722c4e762af433739018 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 19:25:18 -0800
Subject: [PATCH 21/24] make dotnet optional and recover from python
 installation mismatch. Pull requests #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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 47d60b2b3..21ebb3819 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -712,7 +712,7 @@ def parse_options():
             display_help(1)
     # Handle the Python package directory
     if IS_WINDOWS:
-        PYTHON_INSTALL_ENABLED = False
+        PYTHON_INSTALL_ENABLED = True
     else:
         if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
             print(("Warning: The detected Python package directory (%s)"
@@ -811,6 +811,9 @@ def is_ml_enabled():
 def is_dotnet_enabled():
     return DOTNET_ENABLED
 
+def is_python_install_enabled():
+    return PYTHON_INSTALL_ENABLED
+
 def disable_dotnet():
     global DOTNET_ENABLED
     DOTNET_ENABLED = False
@@ -1297,6 +1300,8 @@ class DLLComponent(Component):
             dllfile = '%s$(SO_EXT)' % self.dll_name
             dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
+	    if not python_install_enabled():
+                return
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
                 MakeRuleCmd.install_files(out, dllfile, os.path.join(pythonPkgDirWithoutPrefix, dllfile))

From 92a4ac9eb7b28a014f9f34f3c6d2e8e9463892a2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 19:28:39 -0800
Subject: [PATCH 22/24] make dotnet optional and recover from python
 installation mismatch. Pull requests #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 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 21ebb3819..51e76a148 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1300,7 +1300,7 @@ class DLLComponent(Component):
             dllfile = '%s$(SO_EXT)' % self.dll_name
             dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
             MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
-	    if not python_install_enabled():
+	    if not is_python_install_enabled():
                 return
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:
@@ -1345,8 +1345,8 @@ class PythonInstallComponent(Component):
         Component.__init__(self, name, None, [])
 
     def main_component(self):
-        return PYTHON_INSTALL_ENABLED
-
+        return is_python_install_enabled()
+    
     def install_deps(self, out):
         if not self.main_component():
              return

From e1ab2370e12469436120e72d9fa0ccaf3774114c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@z3-mac.local>
Date: Mon, 7 Dec 2015 03:32:58 +0000
Subject: [PATCH 23/24] fix python w.o. proper intallation, #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@z3-mac.local>
---
 scripts/mk_util.py | 5 +++--
 1 file changed, 3 insertions(+), 2 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index 51e76a148..a2e93d34c 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -1318,8 +1318,9 @@ class DLLComponent(Component):
     def mk_uninstall(self, out):
         dllfile = '%s$(SO_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
-        pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
-        MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
+        if is_python_install_enabled():
+            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
         MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, libfile))
 

From 64b9a301ed88782de519a9c4bb3dcdbbadcc0ae0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 20:09:13 -0800
Subject: [PATCH 24/24] add python visitor example in response to Stackoverflow
 question

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 examples/python/visitor.py | 29 +++++++++++++++++++++++++++++
 1 file changed, 29 insertions(+)
 create mode 100644 examples/python/visitor.py

diff --git a/examples/python/visitor.py b/examples/python/visitor.py
new file mode 100644
index 000000000..9255c6a80
--- /dev/null
+++ b/examples/python/visitor.py
@@ -0,0 +1,29 @@
+# Copyright (c) Microsoft Corporation 2015
+
+from z3 import *
+
+def visitor(e, seen):
+    if e in seen:
+        return
+    seen[e] = True
+    yield e
+    if is_app(e):
+        for ch in e.children():
+            for e in visitor(ch, seen):
+                yield e
+        return
+    if is_quantifier(e):
+        for e in visitor(e.body(), seen):
+            yield e
+        return
+
+x, y = Ints('x y')
+fml = x + x + y > 2 
+seen = {}
+for e in visitor(fml, seen):
+    if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED:
+        print "Variable", e
+    else:
+        print e
+    
+