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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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/38] 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 75c935a4cb22ca6390a2a06e5612be73f87f4d7c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Dec 2015 12:09:15 -0800
Subject: [PATCH 15/38] add tokens to parse strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp     | 118 ++++++++++++++++++++++++++++----
 src/ast/seq_decl_plugin.h       |  53 +++++++++++++-
 src/parsers/smt2/smt2parser.cpp |  19 +++++
 3 files changed, 174 insertions(+), 16 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 330227193..612ffc9db 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -21,11 +21,14 @@ Revision History:
 #include "array_decl_plugin.h"
 #include <sstream>
 
-seq_decl_plugin::seq_decl_plugin(): m_init(false) {}
+seq_decl_plugin::seq_decl_plugin(): m_init(false), 
+                                    m_stringc_sym("String"),
+                                    m_string(0) {}
 
 void seq_decl_plugin::finalize() {
     for (unsigned i = 0; i < m_sigs.size(); ++i) 
         dealloc(m_sigs[i]);
+    m_manager->dec_ref(m_string);
 }
 
 bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
@@ -119,9 +122,17 @@ void seq_decl_plugin::init() {
     m_init = true;
     sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
     sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1));
+    sort* strT = m_string;
     parameter paramA(A);
+    parameter paramS(strT);
     sort* seqA = m.mk_sort(m_family_id, SEQ_SORT, 1, &paramA);
     sort* reA  = m.mk_sort(m_family_id, RE_SORT, 1, &paramA);
+    sort* reT  = m.mk_sort(m_family_id, RE_SORT, 1, &paramS);
+    sort* boolT = m.mk_bool_sort();
+    sort* intT  = arith_util(m).mk_int();
+    sort* predA = array_util(m).mk_array_sort(A, boolT);
+    sort* u16T = 0;
+    sort* u32T = 0;
     sort* seqAseqA[2] = { seqA, seqA };
     sort* seqAA[2] = { seqA, A };
     sort* seqAB[2] = { seqA, B };
@@ -130,9 +141,11 @@ void seq_decl_plugin::init() {
     sort* reAreA[2] = { reA, reA };
     sort* AA[2] = { A, A };
     sort* seqABB[3] = { seqA, B, B };
-    sort* boolT = m.mk_bool_sort();
-    sort* intT  = arith_util(m).mk_int();
-    sort* predA = array_util(m).mk_array_sort(A, boolT);
+    sort* str2T[2] = { strT, strT };
+    sort* str3T[3] = { strT, strT, strT };
+    sort* strTint2T[3] { strT, intT, intT };
+    sort* re2T[2] = { reT, reT };
+    sort* strTreT[2] = { strT, reT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq-unit",   1, 1, &A, seqA);
@@ -158,14 +171,46 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_UNION]      = alloc(psig, m, "re-union",   1, 2, reAreA, reA);
     m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re-intersect",   1, 2, reAreA, reA);
     m_sigs[OP_RE_DIFFERENCE] = alloc(psig, m, "re-difference",   1, 2, reAreA, reA);
-    m_sigs[OP_RE_COMPLEMENT] = alloc(psig, m, "re-complement",   1, 1, &reA, reA);
-    m_sigs[OP_RE_LOOP]       = alloc(psig, m, "re-loop",    1, 1, &reA, reA);
+    m_sigs[OP_RE_COMPLEMENT]     = alloc(psig, m, "re-complement",   1, 1, &reA, reA);
+    m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re-loop",    1, 1, &reA, reA);
     m_sigs[OP_RE_EMPTY_SEQ]      = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA);
-    m_sigs[OP_RE_EMPTY_SET]    = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
-    m_sigs[OP_RE_FULL_SET]    = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
-    m_sigs[OP_RE_OF_SEQ]     = alloc(psig, m, "re-of-seq",  1, 1, &seqA, reA);
-    m_sigs[OP_RE_OF_PRED]    = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
-    m_sigs[OP_RE_MEMBER]     = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
+    m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
+    m_sigs[OP_RE_FULL_SET]       = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
+    m_sigs[OP_RE_OF_SEQ]         = alloc(psig, m, "re-of-seq",  1, 1, &seqA, reA);
+    m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
+    m_sigs[OP_RE_MEMBER]         = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
+    m_sigs[OP_STRING_CONST]      = 0;
+    m_sigs[OP_STRING_CONCAT]     = alloc(psig, m, "str.++", 0, 2, str2T, strT);
+    m_sigs[OP_STRING_LENGTH]     = alloc(psig, m, "str.len", 0, 1, &strT, intT);
+    m_sigs[OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
+    m_sigs[OP_STRING_STRCTN]     = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
+    m_sigs[OP_STRING_CHARAT]     = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
+    m_sigs[OP_STRING_STRIDOF]    = alloc(psig, m, "str.indexof", 0, 2, str2T, intT);
+    m_sigs[OP_STRING_STRREPL]    = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
+    m_sigs[OP_STRING_PREFIX]     = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
+    m_sigs[OP_STRING_SUFFIX]     = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
+    m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
+    m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
+    //m_sigs[OP_STRING_U16TOS]   = alloc(psig, m, "u16.to.str", 0, 1, &intT, strT);
+    //m_sigs[OP_STRING_STOU16]   = alloc(psig, m, "str.to.u16", 0, 1, &strT, intT);
+    //m_sigs[OP_STRING_U32TOS]   = alloc(psig, m, "u32.to.str", 0, 1, &intT, strT);
+    //m_sigs[OP_STRING_STOU32]   = alloc(psig, m, "str.to.u32", 0, 1, &strT, intT);
+    m_sigs[OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
+    m_sigs[OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
+    m_sigs[OP_REGEXP_CONCAT]     = alloc(psig, m, "re.++", 0, 2, re2T, reT);
+    m_sigs[OP_REGEXP_UNION]      = alloc(psig, m, "re.union", 0, 2, re2T, reT);
+    m_sigs[OP_REGEXP_INTER]      = alloc(psig, m, "re.inter", 0, 2, re2T, reT);
+    m_sigs[OP_REGEXP_STAR]       = alloc(psig, m, "re.*", 0, 1, &reT, reT);
+    m_sigs[OP_REGEXP_PLUS]       = alloc(psig, m, "re.+", 0, 1, &reT, reT);
+    m_sigs[OP_REGEXP_OPT]        = alloc(psig, m, "re.opt", 0, 1, &reT, reT);
+    m_sigs[OP_REGEXP_RANGE]      = alloc(psig, m, "re.range", 0, 2, str2T, reT);
+    m_sigs[OP_REGEXP_LOOP]       = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
+}
+
+void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
+    decl_plugin::set_manager(m, id);
+    m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, STRING_SORT, 0, (parameter const*)0));
+    m->inc_ref(m_string);
 }
 
 sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
@@ -188,6 +233,8 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
             m.raise_exception("invalid regex sort, parameter is not a sort");
         }
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
+    case STRING_SORT:
+        return m_string;
     default:
         UNREACHABLE();
         return 0;
@@ -239,7 +286,38 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         if (num_parameters != 2 || !parameters[0].is_int() || !parameters[1].is_int()) {
             m.raise_exception("Expecting two numeral parameters to function re-loop");
         }
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));        
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k, num_parameters, parameters));   
+    case OP_STRING_CONST:
+        if (!(num_parameters == 1 && arity == 0 && parameters[0].is_symbol())) {
+            m.raise_exception("invalid string declaration");
+        } 
+        return m.mk_const_decl(m_stringc_sym, m_string,
+                               func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
+        
+    case OP_STRING_CONCAT:
+    case OP_STRING_LENGTH:
+    case OP_STRING_SUBSTR:
+    case OP_STRING_STRCTN:
+    case OP_STRING_CHARAT:
+    case OP_STRING_STRIDOF:
+    case OP_STRING_STRREPL:
+    case OP_STRING_PREFIX:
+    case OP_STRING_SUFFIX:
+    case OP_STRING_ITOS:
+    case OP_STRING_STOI:
+    case OP_STRING_IN_REGEXP:
+    case OP_STRING_TO_REGEXP:
+    case OP_REGEXP_CONCAT:
+    case OP_REGEXP_UNION:
+    case OP_REGEXP_INTER:
+    case OP_REGEXP_STAR:
+    case OP_REGEXP_PLUS:
+    case OP_REGEXP_OPT:
+    case OP_REGEXP_RANGE:
+    case OP_REGEXP_LOOP:
+        match(*m_sigs[k], arity, domain, range, rng);
+        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+
     default:
         UNREACHABLE();
         return 0;
@@ -249,7 +327,9 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
 void seq_decl_plugin::get_op_names(svector<builtin_name> & op_names, symbol const & logic) {
     init();
     for (unsigned i = 0; i < m_sigs.size(); ++i) {
-        op_names.push_back(builtin_name(m_sigs[i]->m_name.str().c_str(), i));
+        if (m_sigs[i]) {
+            op_names.push_back(builtin_name(m_sigs[i]->m_name.str().c_str(), i));
+        }
     }
 }
 
@@ -257,9 +337,21 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     init();
     sort_names.push_back(builtin_name("Seq",   SEQ_SORT));
     sort_names.push_back(builtin_name("RegEx", RE_SORT));
+    sort_names.push_back(builtin_name("String", STRING_SORT));
+}
+
+app* seq_decl_plugin::mk_string(symbol const& s) {
+    parameter param(s);
+    func_decl* f = m_manager->mk_const_decl(m_stringc_sym, m_string,
+                                   func_decl_info(m_family_id, OP_STRING_CONST, 1, &param));
+    return m_manager->mk_const(f);
 }
 
 bool seq_decl_plugin::is_value(app* e) const {
     // TBD: empty sequence is a value.
     return false;
 }
+
+app* seq_util::mk_string(symbol const& s) {
+    return seq.mk_string(s);
+}
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index c71c7317e..3d1faba42 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -24,7 +24,8 @@ Revision History:
 
 enum seq_sort_kind {
     SEQ_SORT,
-    RE_SORT
+    RE_SORT,
+    STRING_SORT
 };
 
 enum seq_op_kind {
@@ -60,6 +61,35 @@ enum seq_op_kind {
     OP_RE_OF_SEQ,
     OP_RE_OF_PRED,
     OP_RE_MEMBER,
+
+
+    // string specific operators.
+    OP_STRING_CONST,
+    OP_STRING_CONCAT, 
+    OP_STRING_LENGTH, 
+    OP_STRING_SUBSTR, 
+    OP_STRING_STRCTN, 
+    OP_STRING_CHARAT, 
+    OP_STRING_STRIDOF, 
+    OP_STRING_STRREPL, 
+    OP_STRING_PREFIX, 
+    OP_STRING_SUFFIX, 
+    OP_STRING_ITOS, 
+    OP_STRING_STOI, 
+    //OP_STRING_U16TOS, 
+    //OP_STRING_STOU16, 
+    //OP_STRING_U32TOS, 
+    //OP_STRING_STOU32, 
+    OP_STRING_IN_REGEXP, 
+    OP_STRING_TO_REGEXP, 
+    OP_REGEXP_CONCAT, 
+    OP_REGEXP_UNION, 
+    OP_REGEXP_INTER, 
+    OP_REGEXP_STAR, 
+    OP_REGEXP_PLUS, 
+    OP_REGEXP_OPT, 
+    OP_REGEXP_RANGE, 
+    OP_REGEXP_LOOP, 
     
     LAST_SEQ_OP
 };
@@ -83,7 +113,9 @@ class seq_decl_plugin : public decl_plugin {
     };
 
     ptr_vector<psig> m_sigs;
-    bool m_init;
+    bool             m_init;
+    symbol           m_stringc_sym;
+    sort*            m_string;
 
     void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
 
@@ -95,6 +127,8 @@ class seq_decl_plugin : public decl_plugin {
 
     void init();
 
+    virtual void set_manager(ast_manager * m, family_id id);
+
 public:
     seq_decl_plugin();
 
@@ -116,7 +150,20 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
-    
+    app* mk_string(symbol const& s);  
+};
+
+class seq_util {
+    ast_manager& m;
+    seq_decl_plugin& seq;
+public:
+    seq_util(ast_manager& m): 
+        m(m), 
+        seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))) {        
+    }
+    ~seq_util() {}
+
+    app* mk_string(symbol const& s);
 };
 
 #endif /* SEQ_DECL_PLUGIN_H_ */
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index b95be8ee5..62751c025 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -22,6 +22,7 @@ Revision History:
 #include"datatype_decl_plugin.h"
 #include"bv_decl_plugin.h"
 #include"arith_decl_plugin.h"
+#include"seq_decl_plugin.h"
 #include"ast_pp.h"
 #include"well_sorted.h"
 #include"pattern_validation.h"
@@ -65,6 +66,7 @@ namespace smt2 {
 
         scoped_ptr<bv_util>               m_bv_util;
         scoped_ptr<arith_util>            m_arith_util;
+        scoped_ptr<seq_util>              m_seq_util;
         scoped_ptr<pattern_validator>     m_pattern_validator;
         scoped_ptr<var_shifter>           m_var_shifter;
 
@@ -270,6 +272,12 @@ namespace smt2 {
             return *(m_arith_util.get());
         }
 
+        seq_util & sutil() {
+            if (m_seq_util.get() == 0)
+                m_seq_util = alloc(seq_util, m());
+            return *(m_seq_util.get());
+        }
+
         bv_util & butil() {
             if (m_bv_util.get() == 0)
                 m_bv_util = alloc(bv_util, m());
@@ -1059,6 +1067,13 @@ namespace smt2 {
             next();
         }
 
+        void parse_string_const() {
+            SASSERT(curr() == scanner::STRING_TOKEN);
+            expr_stack().push_back(sutil().mk_string(curr_id()));
+            TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
+            next();
+        }
+
         void push_pattern_frame() {
             // TODO: It seems the only reliable way to parse patterns is:
             // Parse as an S-Expr, then try to convert it to an useful pattern.
@@ -1723,6 +1738,9 @@ namespace smt2 {
                             break;
                         case scanner::KEYWORD_TOKEN:
                             throw parser_exception("invalid expression, unexpected keyword");
+                        case scanner::STRING_TOKEN:
+                            parse_string_const();
+                            break;
                         default:
                             throw parser_exception("invalid expression, unexpected input");
                         }
@@ -2609,6 +2627,7 @@ namespace smt2 {
             
             m_bv_util           = 0;
             m_arith_util        = 0;
+            m_seq_util          = 0;
             m_pattern_validator = 0;
             m_var_shifter       = 0;
         }

From a8e366aa246c2262523eacf09f89f14f7367f270 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Dec 2015 15:24:29 -0800
Subject: [PATCH 16/38] add basic string factory

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp     |  4 +-
 src/ast/seq_decl_plugin.h       | 89 ++++++++++++++++++++++++++++++++-
 src/parsers/smt2/smt2parser.cpp |  2 +-
 src/smt/theory_seq_empty.h      | 60 ++++++++++++++++++++++
 4 files changed, 150 insertions(+), 5 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 612ffc9db..65df99c5a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -352,6 +352,6 @@ bool seq_decl_plugin::is_value(app* e) const {
     return false;
 }
 
-app* seq_util::mk_string(symbol const& s) {
-    return seq.mk_string(s);
+app* seq_util::str::mk_string(symbol const& s) {
+    return u.seq.mk_string(s);
 }
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 3d1faba42..0cdfbd5a8 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -156,14 +156,99 @@ public:
 class seq_util {
     ast_manager& m;
     seq_decl_plugin& seq;
+    family_id m_fid;
 public:
+
+    class str {
+        seq_util&    u;
+        ast_manager& m;
+        family_id    m_fid;
+    public:
+        str(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
+
+        app* mk_string(symbol const& s);
+        app* mk_string(char const* s) { return mk_string(symbol(s)); }
+        app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_CONCAT, 2, es); }
+        app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
+        app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
+        app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); }
+
+        bool is_const(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
+        
+        bool is_const(expr const* n, std::string& s) const {
+            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
+        }
+        
+        bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); }
+        bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CONCAT); }
+        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_LENGTH); }
+        bool is_substr(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); }
+        bool is_strctn(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_STRCTN); }
+        bool is_charat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CHARAT); }
+        bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
+        bool is_repl(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
+        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_PREFIX); }
+        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUFFIX); }
+        bool is_itos(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
+        bool is_stoi(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STOI); }
+        bool is_in_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IN_REGEXP); }
+
+        
+        MATCH_BINARY(is_concat);
+        MATCH_UNARY(is_length);
+        MATCH_TERNARY(is_substr);
+        MATCH_BINARY(is_strctn);
+        MATCH_BINARY(is_charat);
+        MATCH_BINARY(is_stridof);
+        MATCH_BINARY(is_repl);
+        MATCH_BINARY(is_prefix);
+        MATCH_BINARY(is_suffix);
+        MATCH_UNARY(is_itos);
+        MATCH_UNARY(is_stoi);
+        MATCH_BINARY(is_in_regexp);        
+    };
+
+    class re {
+        seq_util&    u;
+        ast_manager& m;
+        family_id    m_fid;
+    public:
+        re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
+
+        bool is_to_regexp(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); }
+        bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_CONCAT); }
+        bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_UNION); }
+        bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_INTER); }
+        bool is_star(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_STAR); }
+        bool is_plus(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_PLUS); }
+        bool is_opt(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_OPT); }
+        bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_RANGE); }
+        bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
+       
+        MATCH_UNARY(is_to_regexp);
+        MATCH_BINARY(is_concat);
+        MATCH_BINARY(is_union);
+        MATCH_BINARY(is_inter);
+        MATCH_UNARY(is_star);
+        MATCH_UNARY(is_plus);
+        MATCH_UNARY(is_opt);
+        
+    };
+    str str;
+    re  re;
+
     seq_util(ast_manager& m): 
         m(m), 
-        seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))) {        
+        seq(*static_cast<seq_decl_plugin*>(m.get_plugin(m.mk_family_id("seq")))),
+        m_fid(seq.get_family_id()),
+        str(*this),
+        re(*this) {        
     }
+
     ~seq_util() {}
 
-    app* mk_string(symbol const& s);
+    family_id get_family_id() const { return m_fid; }
+    
 };
 
 #endif /* SEQ_DECL_PLUGIN_H_ */
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 62751c025..2f16f01d7 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1069,7 +1069,7 @@ namespace smt2 {
 
         void parse_string_const() {
             SASSERT(curr() == scanner::STRING_TOKEN);
-            expr_stack().push_back(sutil().mk_string(curr_id()));
+            expr_stack().push_back(sutil().str.mk_string(curr_id()));
             TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
             next();
         }
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 60350017f..b99336b29 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -20,8 +20,64 @@ Revision History:
 #define THEORY_SEQ_EMPTY_H_
 
 #include "smt_theory.h"
+#include "seq_decl_plugin.h"
 
 namespace smt {
+    class seq_factory : public value_factory {
+        typedef hashtable<symbol, symbol_hash_proc, symbol_eq_proc> symbol_set;
+        proto_model& m_model;
+        seq_util     u;
+        symbol_set   m_strings;
+        unsigned     m_next;
+    public:
+        seq_factory(ast_manager & m, family_id fid, proto_model & md):
+            value_factory(m, fid),
+            m_model(md),
+            u(m),
+            m_next(0)
+        {
+            m_strings.insert(symbol(""));
+            m_strings.insert(symbol("a"));
+            m_strings.insert(symbol("b"));
+        }
+
+        virtual expr* get_some_value(sort* s) { 
+            if (u.str.is_string(s)) 
+                return u.str.mk_string(symbol(""));            
+            NOT_IMPLEMENTED_YET();
+            return 0;
+        }
+        virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) { 
+            if (u.str.is_string(s)) {
+                v1 = u.str.mk_string("a");
+                v2 = u.str.mk_string("b");
+                return true;
+            }
+            NOT_IMPLEMENTED_YET();
+            return false; 
+        }
+        virtual expr* get_fresh_value(sort* s) { 
+            if (u.str.is_string(s)) {
+                while (true) {
+                    std::ostringstream strm;
+                    strm << "S" << m_next++;
+                    symbol sym(strm.str().c_str());
+                    if (m_strings.contains(sym)) continue;
+                    m_strings.insert(sym);
+                    return u.str.mk_string(sym);
+                }
+            }
+            NOT_IMPLEMENTED_YET();
+            return 0;
+        }
+        virtual void register_value(expr* n) {
+            std::string sym;
+            if (u.str.is_const(n, sym)) {
+                m_strings.insert(symbol(sym.c_str()));
+            }
+        }
+    };
+
     class theory_seq_empty : public theory {
         bool m_used;
         virtual final_check_status final_check_eh() { return m_used?FC_GIVEUP:FC_DONE; }
@@ -33,6 +89,10 @@ namespace smt {
         virtual char const * get_name() const { return "seq-empty"; }
     public:
         theory_seq_empty(ast_manager& m):theory(m.mk_family_id("seq")), m_used(false) {}
+        virtual void init_model(model_generator & mg) {
+            mg.register_factory(alloc(seq_factory, get_manager(), get_family_id(), mg.get_model()));
+        }
+
     };
 
 };

From b77e3872651555e4941958c5d07df3647ec5a14f Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Fri, 4 Dec 2015 15:26:53 -0800
Subject: [PATCH 17/38] value

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 3 +--
 1 file changed, 1 insertion(+), 2 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 65df99c5a..41aa7aa90 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -348,8 +348,7 @@ app* seq_decl_plugin::mk_string(symbol const& s) {
 }
 
 bool seq_decl_plugin::is_value(app* e) const {
-    // TBD: empty sequence is a value.
-    return false;
+    return is_app_of(e, m_family_id, OP_STRING_CONST);
 }
 
 app* seq_util::str::mk_string(symbol const& s) {

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 18/38] 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 19/38] 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 20/38] 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 c04f75cdbbcd3a0e384af4bba62e65d425ff694c Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Dec 2015 10:30:08 -0800
Subject: [PATCH 21/38] fix build

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 2 +-
 1 file changed, 1 insertion(+), 1 deletion(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 41aa7aa90..5962af658 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -143,7 +143,7 @@ void seq_decl_plugin::init() {
     sort* seqABB[3] = { seqA, B, B };
     sort* str2T[2] = { strT, strT };
     sort* str3T[3] = { strT, strT, strT };
-    sort* strTint2T[3] { strT, intT, intT };
+    sort* strTint2T[3] = { strT, intT, intT };
     sort* re2T[2] = { reT, reT };
     sort* strTreT[2] = { strT, reT };
     m_sigs.resize(LAST_SEQ_OP);

From 75359c580e1eb8a30565f88dd8c6caf4f25e57c1 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Dec 2015 12:02:33 -0800
Subject: [PATCH 22/38] add basic rewriting to strings

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast.h                     |   1 +
 src/ast/ast_smt2_pp.cpp           |  20 +++
 src/ast/ast_smt2_pp.h             |   7 +-
 src/ast/rewriter/seq_rewriter.cpp | 214 ++++++++++++++++++++++++++++++
 src/ast/rewriter/seq_rewriter.h   |  67 ++++++++++
 src/ast/rewriter/th_rewriter.cpp  |   6 +
 src/ast/seq_decl_plugin.h         |   5 +-
 src/cmd_context/cmd_context.cpp   |   4 +-
 src/parsers/smt2/smt2parser.cpp   |   2 +-
 src/parsers/smt2/smt2scanner.cpp  |   5 +-
 10 files changed, 323 insertions(+), 8 deletions(-)
 create mode 100644 src/ast/rewriter/seq_rewriter.cpp
 create mode 100644 src/ast/rewriter/seq_rewriter.h

diff --git a/src/ast/ast.h b/src/ast/ast.h
index 8547675a8..e4e1b4d58 100644
--- a/src/ast/ast.h
+++ b/src/ast/ast.h
@@ -2013,6 +2013,7 @@ public:
     app * mk_distinct_expanded(unsigned num_args, expr * const * args);
     app * mk_true() { return m_true; }
     app * mk_false() { return m_false; }
+    app * mk_bool_val(bool b) { return b?m_true:m_false; }
     app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); }
 
 
diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index c74b4f185..9ffbbd127 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -363,6 +363,23 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
     }
 }
 
+format * smt2_pp_environment::pp_string_literal(app * t) {
+    std::string s;
+    VERIFY (get_sutil().str.is_const(t, s));
+    std::ostringstream buffer;
+    buffer << "\"";
+    for (unsigned i = 0; i < s.length(); ++i) {
+        if (s[i] == '\"') {
+            buffer << "\"\"";
+        }
+        else {
+            buffer << s[i];
+        }
+    }
+    buffer << "\"";  
+    return mk_string(get_manager(), buffer.str().c_str());
+}
+
 format * smt2_pp_environment::pp_datalog_literal(app * t) {
     uint64 v;
     VERIFY (get_dlutil().is_numeral(t, v));
@@ -578,6 +595,9 @@ class smt2_printer {
         if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
             f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
         }
+        else if (m_env.get_sutil().str.is_const(c)) {
+            f = m_env.pp_string_literal(c);
+        }
         else if (m_env.get_bvutil().is_numeral(c)) {
             f = m_env.pp_bv_literal(c, m_pp_bv_lits, m_pp_bv_neg);
         }
diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h
index 04c3b35d4..45d18ceff 100644
--- a/src/ast/ast_smt2_pp.h
+++ b/src/ast/ast_smt2_pp.h
@@ -29,6 +29,7 @@ Revision History:
 #include"array_decl_plugin.h"
 #include"fpa_decl_plugin.h"
 #include"dl_decl_plugin.h"
+#include"seq_decl_plugin.h"
 #include"smt2_util.h"
 
 class smt2_pp_environment {
@@ -47,6 +48,7 @@ public:
     virtual bv_util & get_bvutil() = 0;
     virtual array_util & get_arutil() = 0;
     virtual fpa_util & get_futil() = 0;
+    virtual seq_util & get_sutil() = 0;
     virtual datalog::dl_decl_util& get_dlutil() = 0;
     virtual bool uses(symbol const & s) const = 0; 
     virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len);
@@ -54,6 +56,7 @@ public:
     virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec);
     virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits);
     virtual format_ns::format * pp_datalog_literal(app * t);
+    virtual format_ns::format * pp_string_literal(app * t);
     virtual format_ns::format * pp_sort(sort * s);
     virtual format_ns::format * pp_fdecl_ref(func_decl * f);
     format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const;
@@ -70,12 +73,14 @@ class smt2_pp_environment_dbg : public smt2_pp_environment {
     bv_util       m_bvutil;
     array_util    m_arutil;
     fpa_util      m_futil;
+    seq_util      m_sutil;
     datalog::dl_decl_util m_dlutil;
 public:
-    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_dlutil(m) {}
+    smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {}
     virtual ast_manager & get_manager() const { return m_manager; }
     virtual arith_util & get_autil() { return m_autil; }
     virtual bv_util & get_bvutil() { return m_bvutil; }
+    virtual seq_util & get_sutil() { return m_sutil; }
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
new file mode 100644
index 000000000..35f22d746
--- /dev/null
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -0,0 +1,214 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    seq_rewriter.cpp
+
+Abstract:
+
+    Basic rewriting rules for sequences constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-12-5
+
+Notes:
+
+--*/
+
+#include"seq_rewriter.h"
+#include"arith_decl_plugin.h"
+
+
+br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
+    SASSERT(f->get_family_id() == get_fid());
+    
+    switch(f->get_decl_kind()) {
+
+    case OP_SEQ_UNIT:
+    case OP_SEQ_EMPTY:
+    case OP_SEQ_CONCAT:
+    case OP_SEQ_CONS:
+    case OP_SEQ_REV_CONS:
+    case OP_SEQ_HEAD:
+    case OP_SEQ_TAIL:
+    case OP_SEQ_LAST:
+    case OP_SEQ_FIRST:
+    case OP_SEQ_PREFIX_OF:
+    case OP_SEQ_SUFFIX_OF:
+    case OP_SEQ_SUBSEQ_OF:
+    case OP_SEQ_EXTRACT:
+    case OP_SEQ_NTH:
+    case OP_SEQ_LENGTH:
+
+    case OP_RE_PLUS:
+    case OP_RE_STAR:
+    case OP_RE_OPTION:
+    case OP_RE_RANGE:
+    case OP_RE_CONCAT:
+    case OP_RE_UNION:
+    case OP_RE_INTERSECT:
+    case OP_RE_COMPLEMENT:
+    case OP_RE_DIFFERENCE:
+    case OP_RE_LOOP:
+    case OP_RE_EMPTY_SET:
+    case OP_RE_FULL_SET:
+    case OP_RE_EMPTY_SEQ:
+    case OP_RE_OF_SEQ:
+    case OP_RE_OF_PRED:
+    case OP_RE_MEMBER:
+        return BR_FAILED;
+
+    // string specific operators.
+    case OP_STRING_CONST:
+        return BR_FAILED;
+    case OP_STRING_CONCAT: 
+        SASSERT(num_args == 2);
+        return mk_str_concat(args[0], args[1], result);
+    case OP_STRING_LENGTH:
+        SASSERT(num_args == 1);
+        return mk_str_length(args[0], result);
+    case OP_STRING_SUBSTR: 
+        SASSERT(num_args == 3);
+        return mk_str_substr(args[0], args[1], args[2], result);
+    case OP_STRING_STRCTN: 
+        SASSERT(num_args == 2);
+        return mk_str_strctn(args[0], args[1], result);
+    case OP_STRING_CHARAT:
+        SASSERT(num_args == 2);
+        return mk_str_charat(args[0], args[1], result); 
+    case OP_STRING_STRIDOF: 
+        SASSERT(num_args == 2);
+        return mk_str_stridof(args[0], args[1], result);
+    case OP_STRING_STRREPL: 
+        SASSERT(num_args == 3);
+        return mk_str_strrepl(args[0], args[1], args[2], result);
+    case OP_STRING_PREFIX: 
+        SASSERT(num_args == 2);
+        return mk_str_prefix(args[0], args[1], result);
+    case OP_STRING_SUFFIX: 
+        SASSERT(num_args == 2);
+        return mk_str_suffix(args[0], args[1], result);
+    case OP_STRING_ITOS: 
+        SASSERT(num_args == 1);
+        return mk_str_itos(args[0], result);
+    case OP_STRING_STOI: 
+        SASSERT(num_args == 1);
+        return mk_str_stoi(args[0], result);
+    //case OP_STRING_U16TOS: 
+    //case OP_STRING_STOU16: 
+    //case OP_STRING_U32TOS: 
+    //case OP_STRING_STOU32: 
+    case OP_STRING_IN_REGEXP: 
+    case OP_STRING_TO_REGEXP: 
+    case OP_REGEXP_CONCAT: 
+    case OP_REGEXP_UNION: 
+    case OP_REGEXP_INTER: 
+    case OP_REGEXP_STAR: 
+    case OP_REGEXP_PLUS: 
+    case OP_REGEXP_OPT: 
+    case OP_REGEXP_RANGE: 
+    case OP_REGEXP_LOOP: 
+        return BR_FAILED;
+    }
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
+    std::string c, d;
+    if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
+        result = m_util.str.mk_string(c + d);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
+    std::string b;
+    if (m_util.str.is_const(a, b)) {
+        result = arith_util(m()).mk_numeral(rational(b.length()), true);
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
+    std::string c, d;
+    if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
+        result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
+    std::string s1, s2;
+    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) {
+        bool prefix = s1.length() <= s2.length();
+        for (unsigned i = 0; i < s1.length() && prefix; ++i) {
+            prefix = s1[i] == s2[i];
+        }
+        result = m().mk_bool_val(prefix);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
+    std::string s1, s2;
+    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) {
+        bool suffix = s1.length() <= s2.length();
+        for (unsigned i = 0; i < s1.length() && suffix; ++i) {
+            suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
+        }
+        result = m().mk_bool_val(suffix);
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
+    arith_util autil(m());
+    rational r;
+    if (autil.is_numeral(a, r)) {
+        result = m_util.str.mk_string(r.to_string());
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
+    arith_util autil(m());
+    std::string s;
+    if (m_util.str.is_const(a, s)) {
+        
+    }
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_in_regexp(expr* a, expr* b, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_str_to_regexp(expr* a, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_re_concat(expr* a, expr* b, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_re_union(expr* a, expr* b, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_re_star(expr* a, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_re_plus(expr* a, expr_ref& result) {
+    return BR_FAILED;
+}
+br_status seq_rewriter::mk_re_opt(expr* a, expr_ref& result) {
+    return BR_FAILED;
+}
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
new file mode 100644
index 000000000..62ef249a6
--- /dev/null
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -0,0 +1,67 @@
+/*++
+Copyright (c) 2015 Microsoft Corporation
+
+Module Name:
+
+    seq_rewriter.h
+
+Abstract:
+
+    Basic rewriting rules for sequences constraints.
+
+Author:
+
+    Nikolaj Bjorner (nbjorner) 2015-12-5
+
+Notes:
+
+--*/
+#ifndef SEQ_REWRITER_H_
+#define SEQ_REWRITER_H_
+
+#include"seq_decl_plugin.h"
+#include"rewriter_types.h"
+#include"params.h"
+#include"lbool.h"
+
+
+/**
+   \brief Cheap rewrite rules for seq constraints
+*/
+class seq_rewriter {
+    seq_util       m_util;
+
+    br_status mk_str_concat(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_length(expr* a, expr_ref& result);
+    br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_charat(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_stridof(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
+    br_status mk_str_prefix(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_suffix(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_itos(expr* a, expr_ref& result);
+    br_status mk_str_stoi(expr* a, expr_ref& result);
+    br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_to_regexp(expr* a, expr_ref& result);
+    br_status mk_re_concat(expr* a, expr* b, expr_ref& result);
+    br_status mk_re_union(expr* a, expr* b, expr_ref& result);
+    br_status mk_re_star(expr* a, expr_ref& result);
+    br_status mk_re_plus(expr* a, expr_ref& result);
+    br_status mk_re_opt(expr* a, expr_ref& result);
+
+public:    
+    seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
+        m_util(m) {
+    }
+    ast_manager & m() const { return m_util.get_manager(); }
+    family_id get_fid() const { return m_util.get_family_id(); }
+
+    void updt_params(params_ref const & p) {}
+    static void get_param_descrs(param_descrs & r) {}
+
+    br_status mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result);
+
+};
+
+#endif
diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp
index b7197d239..a8aea47b6 100644
--- a/src/ast/rewriter/th_rewriter.cpp
+++ b/src/ast/rewriter/th_rewriter.cpp
@@ -26,6 +26,7 @@ Notes:
 #include"fpa_rewriter.h"
 #include"dl_rewriter.h"
 #include"pb_rewriter.h"
+#include"seq_rewriter.h"
 #include"rewriter_def.h"
 #include"expr_substitution.h"
 #include"ast_smt2_pp.h"
@@ -43,6 +44,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
     fpa_rewriter        m_f_rw;
     dl_rewriter         m_dl_rw;
     pb_rewriter         m_pb_rw;
+    seq_rewriter        m_seq_rw;
     arith_util          m_a_util;
     bv_util             m_bv_util;
     unsigned long long  m_max_memory; // in bytes
@@ -76,6 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_bv_rw.updt_params(p);
         m_ar_rw.updt_params(p);
         m_f_rw.updt_params(p);
+        m_seq_rw.updt_params(p);
         updt_local_params(p);
     }
 
@@ -200,6 +203,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
             return m_dl_rw.mk_app_core(f, num, args, result);
         if (fid == m_pb_rw.get_fid())
             return m_pb_rw.mk_app_core(f, num, args, result);
+        if (fid == m_seq_rw.get_fid())
+            return m_seq_rw.mk_app_core(f, num, args, result);
         return BR_FAILED;
     }
 
@@ -650,6 +655,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg {
         m_f_rw(m, p),
         m_dl_rw(m),
         m_pb_rw(m),
+        m_seq_rw(m),
         m_a_util(m),
         m_bv_util(m),
         m_used_dependencies(m),
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 0cdfbd5a8..b81f87ec0 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -134,7 +134,7 @@ public:
 
     virtual ~seq_decl_plugin() {}
     virtual void finalize();
-    
+   
     virtual decl_plugin * mk_fresh() { return alloc(seq_decl_plugin); }
     
     virtual sort * mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters);
@@ -159,6 +159,8 @@ class seq_util {
     family_id m_fid;
 public:
 
+    ast_manager& get_manager() const { return m; }
+
     class str {
         seq_util&    u;
         ast_manager& m;
@@ -168,6 +170,7 @@ public:
 
         app* mk_string(symbol const& s);
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
+        app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
         app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_CONCAT, 2, es); }
         app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
         app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp
index 02b2b6525..1b5d9d470 100644
--- a/src/cmd_context/cmd_context.cpp
+++ b/src/cmd_context/cmd_context.cpp
@@ -245,6 +245,7 @@ protected:
     bv_util       m_bvutil;
     array_util    m_arutil;
     fpa_util      m_futil;
+    seq_util      m_sutil;
     datalog::dl_decl_util m_dlutil;
 
     format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) {
@@ -265,13 +266,14 @@ protected:
     }
 
 public:
-    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_dlutil(o.m()) {}
+    pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {}
     virtual ~pp_env() {}
     virtual ast_manager & get_manager() const { return m_owner.m(); }
     virtual arith_util & get_autil() { return m_autil; }
     virtual bv_util & get_bvutil() { return m_bvutil; }
     virtual array_util & get_arutil() { return m_arutil; }
     virtual fpa_util & get_futil() { return m_futil; }
+    virtual seq_util & get_sutil() { return m_sutil; }
     virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; }
     virtual bool uses(symbol const & s) const {
         return
diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp
index 2f16f01d7..404c04d3a 100644
--- a/src/parsers/smt2/smt2parser.cpp
+++ b/src/parsers/smt2/smt2parser.cpp
@@ -1069,7 +1069,7 @@ namespace smt2 {
 
         void parse_string_const() {
             SASSERT(curr() == scanner::STRING_TOKEN);
-            expr_stack().push_back(sutil().str.mk_string(curr_id()));
+            expr_stack().push_back(sutil().str.mk_string(m_scanner.get_string()));
             TRACE("smt2parser", tout << "new string: " << mk_pp(expr_stack().back(), m()) << "\n";);
             next();
         }
diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp
index bc62c2646..ed16003c2 100644
--- a/src/parsers/smt2/smt2scanner.cpp
+++ b/src/parsers/smt2/smt2scanner.cpp
@@ -171,10 +171,7 @@ namespace smt2 {
                 throw scanner_exception("unexpected end of string", m_line, m_spos);
             if (c == '\"') {
                 next();
-                if (curr() == '\"') {
-                    m_string.push_back(c);
-                }
-                else {
+                if (curr() != '\"') {
                     m_string.push_back(0);
                     return STRING_TOKEN;
                 }

From 5296009f460f7af793d29aad3a6d763e4a7454be Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Dec 2015 15:38:54 -0800
Subject: [PATCH 23/38] ground string rewriting

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 66 ++++++++++++++++++++++++++++---
 src/ast/rewriter/seq_rewriter.h   |  4 +-
 2 files changed, 64 insertions(+), 6 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 35f22d746..741e6077e 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -126,11 +126,21 @@ br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
 br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     std::string b;
     if (m_util.str.is_const(a, b)) {
-        result = arith_util(m()).mk_numeral(rational(b.length()), true);
+        result = m_autil.mk_numeral(rational(b.length()), true);
+        return BR_DONE;
     }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
+    std::string s;
+    rational pos, len;
+    if (m_util.str.is_const(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
+        pos.is_unsigned() && len.is_unsigned() && !pos.is_neg() && !len.is_neg() && pos.get_unsigned() <= s.length()) {
+        unsigned _pos = pos.get_unsigned();
+        unsigned _len = len.get_unsigned();
+        result = m_util.str.mk_string(s.substr(_pos, _len));
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
@@ -142,12 +152,45 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
+    std::string c;
+    rational r;
+    if (m_util.str.is_const(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
+        unsigned j = r.get_unsigned();
+        if (j < c.length()) {
+            char ch = c[j];
+            c[0] = ch;
+            c[1] = 0;
+            result = m_util.str.mk_string(c);
+            return BR_DONE;
+        }
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr_ref& result) {
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
+    std::string s1, s2, s3;
+    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_util.str.is_const(c, s3)) {
+        std::ostringstream buffer;
+        for (unsigned i = 0; i < s1.length(); ) {
+            if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
+                buffer << s3;
+                i += s2.length();
+            }
+            else {
+                buffer << s1[i];
+                ++i;
+            }
+        }
+        result = m_util.str.mk_string(buffer.str());
+        return BR_DONE;
+    }
+    if (b == c) {
+        result = a;
+        return BR_DONE;
+    }
+
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
@@ -160,6 +203,10 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(prefix);
         return BR_DONE;
     }
+    if (m_util.str.is_const(a, s1) && s1.length() == 0) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
@@ -172,22 +219,31 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(suffix);
         return BR_DONE;
     }
+    if (m_util.str.is_const(a, s1) && s1.length() == 0) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
-    arith_util autil(m());
     rational r;
-    if (autil.is_numeral(a, r)) {
+    if (m_autil.is_numeral(a, r)) {
         result = m_util.str.mk_string(r.to_string());
         return BR_DONE;
     }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
-    arith_util autil(m());
     std::string s;
     if (m_util.str.is_const(a, s)) {
-        
+        for (unsigned i = 0; i < s.length(); ++i) {
+            if (s[i] == '-') { if (i != 0) return BR_FAILED; }
+            else if ('0' <= s[i] && s[i] <= '9') continue;
+            return BR_FAILED;            
+        }
+        rational r(s.c_str());
+        result = m_autil.mk_numeral(r, true);
+        return BR_DONE;
     }
     return BR_FAILED;
 }
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 62ef249a6..04363c766 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -20,6 +20,7 @@ Notes:
 #define SEQ_REWRITER_H_
 
 #include"seq_decl_plugin.h"
+#include"arith_decl_plugin.h"
 #include"rewriter_types.h"
 #include"params.h"
 #include"lbool.h"
@@ -30,6 +31,7 @@ Notes:
 */
 class seq_rewriter {
     seq_util       m_util;
+    arith_util     m_autil;
 
     br_status mk_str_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_str_length(expr* a, expr_ref& result);
@@ -52,7 +54,7 @@ class seq_rewriter {
 
 public:    
     seq_rewriter(ast_manager & m, params_ref const & p = params_ref()):
-        m_util(m) {
+        m_util(m), m_autil(m) {
     }
     ast_manager & m() const { return m_util.get_manager(); }
     family_id get_fid() const { return m_util.get_family_id(); }

From 4fe0e07080bbc4aa006be03112892fe6007b22e0 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sat, 5 Dec 2015 16:36:11 -0800
Subject: [PATCH 24/38] indexof

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 24 ++++++++++++++++++++----
 src/ast/rewriter/seq_rewriter.h   |  2 +-
 src/ast/seq_decl_plugin.cpp       |  3 ++-
 3 files changed, 23 insertions(+), 6 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 741e6077e..2568639c3 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -79,8 +79,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
         SASSERT(num_args == 2);
         return mk_str_charat(args[0], args[1], result); 
     case OP_STRING_STRIDOF: 
-        SASSERT(num_args == 2);
-        return mk_str_stridof(args[0], args[1], result);
+        SASSERT(num_args == 3);
+        return mk_str_stridof(args[0], args[1], args[2], result);
     case OP_STRING_STRREPL: 
         SASSERT(num_args == 3);
         return mk_str_strrepl(args[0], args[1], args[2], result);
@@ -135,7 +135,7 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
     std::string s;
     rational pos, len;
     if (m_util.str.is_const(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
-        pos.is_unsigned() && len.is_unsigned() && !pos.is_neg() && !len.is_neg() && pos.get_unsigned() <= s.length()) {
+        pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
         unsigned _pos = pos.get_unsigned();
         unsigned _len = len.get_unsigned();
         result = m_util.str.mk_string(s.substr(_pos, _len));
@@ -166,7 +166,23 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
     }
     return BR_FAILED;
 }
-br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
+    std::string s1, s2;
+    rational r;
+    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_autil.is_numeral(c, r) && r.is_unsigned()) {
+        for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
+            if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
+                result = m_autil.mk_numeral(rational(i) - r, true);
+                return BR_DONE;
+            }
+        }
+        result = m_autil.mk_numeral(rational(-1), true);
+        return BR_DONE;
+    }
+    if (m_util.str.is_const(b, s2) && s2.length() == 0) {
+        result = c;
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
 br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 04363c766..f2a152640 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -38,7 +38,7 @@ class seq_rewriter {
     br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
     br_status mk_str_charat(expr* a, expr* b, expr_ref& result);
-    br_status mk_str_stridof(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_prefix(expr* a, expr* b, expr_ref& result);
     br_status mk_str_suffix(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 5962af658..19b5b3321 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -146,6 +146,7 @@ void seq_decl_plugin::init() {
     sort* strTint2T[3] = { strT, intT, intT };
     sort* re2T[2] = { reT, reT };
     sort* strTreT[2] = { strT, reT };
+    sort* str2TintT[3] = { strT, strT, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq-unit",   1, 1, &A, seqA);
@@ -185,7 +186,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
     m_sigs[OP_STRING_STRCTN]     = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_CHARAT]     = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
-    m_sigs[OP_STRING_STRIDOF]    = alloc(psig, m, "str.indexof", 0, 2, str2T, intT);
+    m_sigs[OP_STRING_STRIDOF]    = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[OP_STRING_STRREPL]    = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
     m_sigs[OP_STRING_PREFIX]     = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_SUFFIX]     = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);

From 40e9e4c7f85ba7e8387228e9180fb837f995eed2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 10:44:19 -0800
Subject: [PATCH 25/38] more rewrites

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 95 +++++++++++++++++++++++++++----
 src/ast/rewriter/seq_rewriter.h   |  1 +
 src/ast/seq_decl_plugin.cpp       |  9 +++
 src/ast/seq_decl_plugin.h         |  5 ++
 4 files changed, 98 insertions(+), 12 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 2568639c3..d9ed8f6e0 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -115,22 +115,75 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     return BR_FAILED;
 }
 
+/*
+   string + string = string
+   a + (b + c) = (a + b) + c
+   a + "" = a
+   "" + a = a
+   (a + string) + string = a + string
+*/
 br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
-    std::string c, d;
-    if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
-        result = m_util.str.mk_string(c + d);
+    std::string s1, s2;
+    expr* c, *d;
+    bool isc1 = m_util.str.is_const(a, s1);
+    bool isc2 = m_util.str.is_const(b, s2);
+    if (isc1 && isc2) {
+        result = m_util.str.mk_string(s1 + s2);
+        return BR_DONE;
+    }
+    if (m_util.str.is_concat(b, c, d)) {
+        result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
+        return BR_REWRITE2;
+    }
+    if (isc1 && s1.length() == 0) {
+        result = b;
+        return BR_DONE;
+    }
+    if (isc2 && s2.length() == 0) {
+        result = a;
+        return BR_DONE;
+    }
+    if (m_util.str.is_concat(a, c, d) && 
+        m_util.str.is_const(d, s1) && isc2) {
+        result = m_util.str.mk_string(s1 + s2);
         return BR_DONE;
     }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     std::string b;
-    if (m_util.str.is_const(a, b)) {
+    m_es.reset();
+    m_util.str.get_concat(a, m_es);
+    unsigned len = 0;
+    unsigned j = 0;
+    for (unsigned i = 0; i < m_es.size(); ++i) {
+        if (m_util.str.is_const(m_es[i], b)) {
+            len += b.length();
+        }
+        else {
+            m_es[j] = m_es[i];
+            ++j;
+        }
+    }
+    if (j == 0) {
         result = m_autil.mk_numeral(rational(b.length()), true);
         return BR_DONE;
     }
+    if (j != m_es.size()) {
+        expr_ref_vector es(m());        
+        for (unsigned i = 0; i < j; ++i) {
+            es.push_back(m_util.str.mk_length(m_es[i]));
+        }
+        if (len != 0) {
+            es.push_back(m_autil.mk_numeral(rational(len), true));
+        }
+        result = m_autil.mk_add(es.size(), es.c_ptr());
+        return BR_DONE;
+    }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s;
     rational pos, len;
@@ -151,6 +204,7 @@ br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
     }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
     std::string c;
     rational r;
@@ -166,10 +220,14 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
     }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2;
     rational r;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_autil.is_numeral(c, r) && r.is_unsigned()) {
+    bool isc1 = m_util.str.is_const(a, s1);
+    bool isc2 = m_util.str.is_const(b, s2);
+
+    if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
         for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
             if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
                 result = m_autil.mk_numeral(rational(i) - r, true);
@@ -179,15 +237,23 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
         result = m_autil.mk_numeral(rational(-1), true);
         return BR_DONE;
     }
-    if (m_util.str.is_const(b, s2) && s2.length() == 0) {
+    if (m_autil.is_numeral(c, r) && r.is_neg()) {
+        result = m_autil.mk_numeral(rational(-1), true);
+        return BR_DONE;
+    }
+    
+    if (isc2 && s2.length() == 0) {
         result = c;
         return BR_DONE;
     }
+    // Enhancement: walk segments of a, determine which segments must overlap, must not overlap, may overlap.
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2, s3;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && m_util.str.is_const(c, s3)) {
+    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && 
+        m_util.str.is_const(c, s3)) {
         std::ostringstream buffer;
         for (unsigned i = 0; i < s1.length(); ) {
             if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
@@ -206,12 +272,14 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
         result = a;
         return BR_DONE;
     }
-
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) {
+    bool isc1 = m_util.str.is_const(a, s1);
+    bool isc2 = m_util.str.is_const(b, s2);
+    if (isc1 && isc2) {
         bool prefix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && prefix; ++i) {
             prefix = s1[i] == s2[i];
@@ -219,15 +287,17 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(prefix);
         return BR_DONE;
     }
-    if (m_util.str.is_const(a, s1) && s1.length() == 0) {
+    if (isc1 && s1.length() == 0) {
         result = m().mk_true();
         return BR_DONE;
     }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2)) {
+    bool isc1 = m_util.str.is_const(a, s1);
+    if (isc1 && m_util.str.is_const(b, s2)) {
         bool suffix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && suffix; ++i) {
             suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
@@ -235,12 +305,13 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(suffix);
         return BR_DONE;
     }
-    if (m_util.str.is_const(a, s1) && s1.length() == 0) {
+    if (isc1 && s1.length() == 0) {
         result = m().mk_true();
         return BR_DONE;
     }
     return BR_FAILED;
 }
+
 br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
     rational r;
     if (m_autil.is_numeral(a, r)) {
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index f2a152640..cefa451fa 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -32,6 +32,7 @@ Notes:
 class seq_rewriter {
     seq_util       m_util;
     arith_util     m_autil;
+    ptr_vector<expr> m_es;
 
     br_status mk_str_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_str_length(expr* a, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 19b5b3321..4cd89285a 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -355,3 +355,12 @@ bool seq_decl_plugin::is_value(app* e) const {
 app* seq_util::str::mk_string(symbol const& s) {
     return u.seq.mk_string(s);
 }
+
+void seq_util::str::get_concat(expr* e, ptr_vector<expr>& es) const {
+    expr* e1, *e2;
+    while (is_concat(e, e1, e2)) {
+        get_concat(e1, es);
+        e = e2;
+    }    
+    es.push_back(e);
+}
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index b81f87ec0..4443b4bb2 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -181,6 +181,9 @@ public:
         bool is_const(expr const* n, std::string& s) const {
             return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
         }
+        bool is_const(expr const* n, symbol& s) const {
+            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
+        }
         
         bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); }
         bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CONCAT); }
@@ -209,6 +212,8 @@ public:
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
         MATCH_BINARY(is_in_regexp);        
+
+        void get_concat(expr* e, ptr_vector<expr>& es) const;
     };
 
     class re {

From 89fe24342ddf936b162680af4e5ff1e8c254f6d2 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 11:06:58 -0800
Subject: [PATCH 26/38] fix size_t mode

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index d9ed8f6e0..ac87bdb3d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -156,7 +156,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     m_es.reset();
     m_util.str.get_concat(a, m_es);
     unsigned len = 0;
-    unsigned j = 0;
+    size_t j = 0;
     for (unsigned i = 0; i < m_es.size(); ++i) {
         if (m_util.str.is_const(m_es[i], b)) {
             len += b.length();
@@ -167,7 +167,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
         }
     }
     if (j == 0) {
-        result = m_autil.mk_numeral(rational(b.length()), true);
+        result = m_autil.mk_numeral(rational(b.length(), rational::ui64()), true);
         return BR_DONE;
     }
     if (j != m_es.size()) {
@@ -176,7 +176,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
             es.push_back(m_util.str.mk_length(m_es[i]));
         }
         if (len != 0) {
-            es.push_back(m_autil.mk_numeral(rational(len), true));
+            es.push_back(m_autil.mk_numeral(rational(len, rational::ui64()), true));
         }
         result = m_autil.mk_add(es.size(), es.c_ptr());
         return BR_DONE;
@@ -255,7 +255,7 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
     if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && 
         m_util.str.is_const(c, s3)) {
         std::ostringstream buffer;
-        for (unsigned i = 0; i < s1.length(); ) {
+        for (size_t i = 0; i < s1.length(); ) {
             if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
                 buffer << s3;
                 i += s2.length();

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 27/38] 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 28/38] 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 aead45a2524994abffddea697c7829e3ccfcaa53 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 19:14:31 -0800
Subject: [PATCH 29/38] make dotnet optional and recover from python
 installation mismatch. Pull requests #338, #340

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/seq_decl_plugin.cpp | 46 ++++++++++++++++++++++++++++++-------
 src/ast/seq_decl_plugin.h   |  6 ++---
 2 files changed, 40 insertions(+), 12 deletions(-)

diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 4cd89285a..7a48d8efd 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -65,6 +65,34 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
     }
 }
 
+/*
+  \brief match left associative operator.
+*/
+void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
+    ptr_vector<sort> binding;
+    ast_manager& m = *m_manager;
+    if (dsz == 0) {
+        std::ostringstream strm;
+        strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
+        strm << "at least one argument expected " << dsz << " given";
+        m.raise_exception(strm.str().c_str());
+    }
+    bool is_match = true;
+    for (unsigned i = 0; is_match && i < dsz; ++i) {
+        is_match = match(binding, dom[i], sig.m_dom[0].get());
+    }
+    if (range && is_match) {
+        is_match = match(binding, range, sig.m_range);
+    }
+    if (!is_match) {
+        std::ostringstream strm;
+        strm << "Sort of function '" << sig.m_name << "' ";
+        strm << "does not match the declared type";
+        m.raise_exception(strm.str().c_str());
+    }
+    range_out = apply_binding(binding, sig.m_range);
+}
+
 void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
@@ -192,10 +220,6 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_SUFFIX]     = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
-    //m_sigs[OP_STRING_U16TOS]   = alloc(psig, m, "u16.to.str", 0, 1, &intT, strT);
-    //m_sigs[OP_STRING_STOU16]   = alloc(psig, m, "str.to.u16", 0, 1, &strT, intT);
-    //m_sigs[OP_STRING_U32TOS]   = alloc(psig, m, "u32.to.str", 0, 1, &intT, strT);
-    //m_sigs[OP_STRING_STOU32]   = alloc(psig, m, "str.to.u32", 0, 1, &strT, intT);
     m_sigs[OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
     m_sigs[OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
     m_sigs[OP_REGEXP_CONCAT]     = alloc(psig, m, "re.++", 0, 2, re2T, reT);
@@ -250,7 +274,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     switch(k) {
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_CONCAT:
     case OP_SEQ_CONS:
     case OP_SEQ_REV_CONS:
     case OP_SEQ_HEAD:
@@ -265,7 +288,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_STAR:
     case OP_RE_OPTION:
     case OP_RE_RANGE:
-    case OP_RE_CONCAT:
     case OP_RE_UNION:
     case OP_RE_INTERSECT:
     case OP_RE_DIFFERENCE:
@@ -295,7 +317,16 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_const_decl(m_stringc_sym, m_string,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
         
-    case OP_STRING_CONCAT:
+    case OP_SEQ_CONCAT:
+    case OP_RE_CONCAT:
+    case OP_REGEXP_CONCAT:
+    case OP_STRING_CONCAT: {
+        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
+        func_decl_info info(m_family_id, k);
+        info.set_left_associative();
+        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
+    }
+
     case OP_STRING_LENGTH:
     case OP_STRING_SUBSTR:
     case OP_STRING_STRCTN:
@@ -308,7 +339,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_STRING_STOI:
     case OP_STRING_IN_REGEXP:
     case OP_STRING_TO_REGEXP:
-    case OP_REGEXP_CONCAT:
     case OP_REGEXP_UNION:
     case OP_REGEXP_INTER:
     case OP_REGEXP_STAR:
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 4443b4bb2..35e2cbf8a 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -76,10 +76,6 @@ enum seq_op_kind {
     OP_STRING_SUFFIX, 
     OP_STRING_ITOS, 
     OP_STRING_STOI, 
-    //OP_STRING_U16TOS, 
-    //OP_STRING_STOU16, 
-    //OP_STRING_U32TOS, 
-    //OP_STRING_STOU32, 
     OP_STRING_IN_REGEXP, 
     OP_STRING_TO_REGEXP, 
     OP_REGEXP_CONCAT, 
@@ -119,6 +115,8 @@ class seq_decl_plugin : public decl_plugin {
 
     void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
 
+    void match_left_assoc(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
+
     bool match(ptr_vector<sort>& binding, sort* s, sort* sP);
 
     sort* apply_binding(ptr_vector<sort> const& binding, sort* s);

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 30/38] 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 31/38] 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 32/38] 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 33/38] 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 34/38] 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
+    
+

From 08bfd0841221833bf146a70f8fe9f5801eb1ee65 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 22:15:56 -0800
Subject: [PATCH 35/38] merging seq and string

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp           |   5 ++
 src/ast/rewriter/seq_rewriter.cpp |  30 ++------
 src/ast/rewriter/seq_rewriter.h   |   2 +-
 src/ast/seq_decl_plugin.cpp       | 119 +++++++++++++++---------------
 src/ast/seq_decl_plugin.h         |  45 +++++------
 src/smt/theory_seq_empty.h        |   6 +-
 6 files changed, 93 insertions(+), 114 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 9ffbbd127..62a6a586e 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -424,6 +424,11 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         fs.push_back(mk_unsigned(m, sbits));
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), "_");
     }
+    if (get_sutil().is_seq(s) && !get_sutil().is_string(s)) {
+        ptr_buffer<format> fs;
+        fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
+        return mk_seq1(m, fs.begin(), fs.end(), f2f(), "Seq");
+    }
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); 
 }
 
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index ac87bdb3d..00b94e60d 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -19,6 +19,7 @@ Notes:
 
 #include"seq_rewriter.h"
 #include"arith_decl_plugin.h"
+#include"ast_pp.h"
 
 
 br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * const * args, expr_ref & result) {
@@ -28,13 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_CONCAT:
-    case OP_SEQ_CONS:
-    case OP_SEQ_REV_CONS:
-    case OP_SEQ_HEAD:
-    case OP_SEQ_TAIL:
-    case OP_SEQ_LAST:
-    case OP_SEQ_FIRST:
     case OP_SEQ_PREFIX_OF:
     case OP_SEQ_SUFFIX_OF:
     case OP_SEQ_SUBSEQ_OF:
@@ -49,8 +43,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_CONCAT:
     case OP_RE_UNION:
     case OP_RE_INTERSECT:
-    case OP_RE_COMPLEMENT:
-    case OP_RE_DIFFERENCE:
     case OP_RE_LOOP:
     case OP_RE_EMPTY_SET:
     case OP_RE_FULL_SET:
@@ -63,9 +55,10 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     // string specific operators.
     case OP_STRING_CONST:
         return BR_FAILED;
-    case OP_STRING_CONCAT: 
+    case OP_SEQ_CONCAT: 
+    case _OP_STRING_CONCAT:
         SASSERT(num_args == 2);
-        return mk_str_concat(args[0], args[1], result);
+        return mk_seq_concat(args[0], args[1], result);
     case OP_STRING_LENGTH:
         SASSERT(num_args == 1);
         return mk_str_length(args[0], result);
@@ -96,19 +89,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_STRING_STOI: 
         SASSERT(num_args == 1);
         return mk_str_stoi(args[0], result);
-    //case OP_STRING_U16TOS: 
-    //case OP_STRING_STOU16: 
-    //case OP_STRING_U32TOS: 
-    //case OP_STRING_STOU32: 
     case OP_STRING_IN_REGEXP: 
     case OP_STRING_TO_REGEXP: 
-    case OP_REGEXP_CONCAT: 
-    case OP_REGEXP_UNION: 
-    case OP_REGEXP_INTER: 
-    case OP_REGEXP_STAR: 
-    case OP_REGEXP_PLUS: 
-    case OP_REGEXP_OPT: 
-    case OP_REGEXP_RANGE: 
     case OP_REGEXP_LOOP: 
         return BR_FAILED;
     }
@@ -122,7 +104,7 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
    "" + a = a
    (a + string) + string = a + string
 */
-br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
     expr* c, *d;
     bool isc1 = m_util.str.is_const(a, s1);
@@ -145,7 +127,7 @@ br_status seq_rewriter::mk_str_concat(expr* a, expr* b, expr_ref& result) {
     }
     if (m_util.str.is_concat(a, c, d) && 
         m_util.str.is_const(d, s1) && isc2) {
-        result = m_util.str.mk_string(s1 + s2);
+        result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
         return BR_DONE;
     }
     return BR_FAILED;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index cefa451fa..2d2909018 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -34,7 +34,7 @@ class seq_rewriter {
     arith_util     m_autil;
     ptr_vector<expr> m_es;
 
-    br_status mk_str_concat(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_concat(expr* a, expr* b, expr_ref& result);
     br_status mk_str_length(expr* a, expr_ref& result);
     br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 7a48d8efd..5fd8c0df7 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -19,16 +19,19 @@ Revision History:
 #include "seq_decl_plugin.h"
 #include "arith_decl_plugin.h"
 #include "array_decl_plugin.h"
+#include "ast_pp.h"
 #include <sstream>
 
 seq_decl_plugin::seq_decl_plugin(): m_init(false), 
                                     m_stringc_sym("String"),
-                                    m_string(0) {}
+                                    m_string(0),
+                                    m_char(0) {}
 
 void seq_decl_plugin::finalize() {
     for (unsigned i = 0; i < m_sigs.size(); ++i) 
         dealloc(m_sigs[i]);
     m_manager->dec_ref(m_string);
+    m_manager->dec_ref(m_char);
 }
 
 bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
@@ -38,29 +41,32 @@ bool seq_decl_plugin::is_sort_param(sort* s, unsigned& idx) {
 }
 
 bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
+    ast_manager& m = *m_manager;
     if (s == sP) return true;
     unsigned i;
     if (is_sort_param(sP, i)) {
         if (binding.size() <= i) binding.resize(i+1);
         if (binding[i] && (binding[i] != s)) return false;
+        TRACE("seq", tout << "setting binding @ " << i << " to " << mk_pp(s, m) << "\n";);
         binding[i] = s;
         return true;
     }
+
    
     if (s->get_family_id() == sP->get_family_id() &&
         s->get_decl_kind() == sP->get_decl_kind() &&
-        s->get_name() == sP->get_name()) {
-            SASSERT(s->get_num_parameters() == sP->get_num_parameters());
-            for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
-                parameter const& p = s->get_parameter(i);
-                if (p.is_ast() && is_sort(p.get_ast())) {
-                    parameter const& p2 = sP->get_parameter(i);
-                    if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
-                }
+        s->get_num_parameters() == sP->get_num_parameters()) {
+        for (unsigned i = 0; i < s->get_num_parameters(); ++i) {
+            parameter const& p = s->get_parameter(i);
+            if (p.is_ast() && is_sort(p.get_ast())) {
+                parameter const& p2 = sP->get_parameter(i);
+                if (!match(binding, to_sort(p.get_ast()), to_sort(p2.get_ast()))) return false;
             }
+        }
         return true;
     }
     else {
+        TRACE("seq", tout << "Could not match " << mk_pp(s, m) << " and " << mk_pp(sP, m) << "\n";);
         return false;
     }
 }
@@ -71,6 +77,11 @@ bool seq_decl_plugin::match(ptr_vector<sort>& binding, sort* s, sort* sP) {
 void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
+    TRACE("seq", 
+          tout << sig.m_name << ": ";
+          for (unsigned i = 0; i < dsz; ++i) tout << mk_pp(dom[i], m) << " ";
+          if (range) tout << " range: " << mk_pp(range, m);
+          tout << "\n";);
     if (dsz == 0) {
         std::ostringstream strm;
         strm << "Unexpected number of arguments to '" << sig.m_name << "' ";
@@ -91,6 +102,7 @@ void seq_decl_plugin::match_left_assoc(psig& sig, unsigned dsz, sort *const* dom
         m.raise_exception(strm.str().c_str());
     }
     range_out = apply_binding(binding, sig.m_range);
+    TRACE("seq", tout << mk_pp(range_out, m) << "\n";);
 }
 
 void seq_decl_plugin::match(psig& sig, unsigned dsz, sort *const* dom, sort* range, sort_ref& range_out) {
@@ -162,10 +174,8 @@ void seq_decl_plugin::init() {
     sort* u16T = 0;
     sort* u32T = 0;
     sort* seqAseqA[2] = { seqA, seqA };
-    sort* seqAA[2] = { seqA, A };
     sort* seqAB[2] = { seqA, B };
     sort* seqAreA[2] = { seqA, reA };
-    sort* AseqA[2] = { A, seqA };
     sort* reAreA[2] = { reA, reA };
     sort* AA[2] = { A, A };
     sort* seqABB[3] = { seqA, B, B };
@@ -177,30 +187,22 @@ void seq_decl_plugin::init() {
     sort* str2TintT[3] = { strT, strT, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
-    m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq-unit",   1, 1, &A, seqA);
-    m_sigs[OP_SEQ_EMPTY]     = alloc(psig, m, "seq-empty",  1, 0, 0, seqA); 
-    m_sigs[OP_SEQ_CONCAT]    = alloc(psig, m, "seq-concat", 1, 2, seqAseqA, seqA);
-    m_sigs[OP_SEQ_CONS]      = alloc(psig, m, "seq-cons",   1, 2, AseqA, seqA);
-    m_sigs[OP_SEQ_REV_CONS]  = alloc(psig, m, "seq-rev-cons",   1, 2, seqAA, seqA);
-    m_sigs[OP_SEQ_HEAD]      = alloc(psig, m, "seq-head",   1, 1, &seqA, A);
-    m_sigs[OP_SEQ_TAIL]      = alloc(psig, m, "seq-tail",   1, 1, &seqA, seqA);
-    m_sigs[OP_SEQ_LAST]      = alloc(psig, m, "seq-last",   1, 1, &seqA, A);
-    m_sigs[OP_SEQ_FIRST]     = alloc(psig, m, "seq-first",  1, 1, &seqA, seqA);
-    m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq-prefix-of", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq-suffix-of", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",   1, 1, &A, seqA);
+    m_sigs[OP_SEQ_EMPTY]     = alloc(psig, m, "seq.empty",  1, 0, 0, seqA); 
+    m_sigs[OP_SEQ_CONCAT]    = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA);
+    m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
     m_sigs[OP_SEQ_SUBSEQ_OF] = alloc(psig, m, "seq-subseq-of", 1, 2, seqAseqA, boolT);
     m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq-extract", 2, 3, seqABB, seqA);
     m_sigs[OP_SEQ_NTH]       = alloc(psig, m, "seq-nth", 2, 2, seqAB, A);
     m_sigs[OP_SEQ_LENGTH]    = alloc(psig, m, "seq-length", 1, 1, &seqA, intT);
-    m_sigs[OP_RE_PLUS]       = alloc(psig, m, "re-plus",    1, 1, &reA, reA);
-    m_sigs[OP_RE_STAR]       = alloc(psig, m, "re-star",    1, 1, &reA, reA);
-    m_sigs[OP_RE_OPTION]     = alloc(psig, m, "re-option",  1, 1, &reA, reA);
-    m_sigs[OP_RE_RANGE]      = alloc(psig, m, "re-range",   1, 2, AA,  reA);
-    m_sigs[OP_RE_CONCAT]     = alloc(psig, m, "re-concat",  1, 2, reAreA, reA);
-    m_sigs[OP_RE_UNION]      = alloc(psig, m, "re-union",   1, 2, reAreA, reA);
-    m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re-intersect",   1, 2, reAreA, reA);
-    m_sigs[OP_RE_DIFFERENCE] = alloc(psig, m, "re-difference",   1, 2, reAreA, reA);
-    m_sigs[OP_RE_COMPLEMENT]     = alloc(psig, m, "re-complement",   1, 1, &reA, reA);
+    m_sigs[OP_RE_PLUS]       = alloc(psig, m, "re.+",    1, 1, &reA, reA);
+    m_sigs[OP_RE_STAR]       = alloc(psig, m, "re.*",    1, 1, &reA, reA);
+    m_sigs[OP_RE_OPTION]     = alloc(psig, m, "re.opt",  1, 1, &reA, reA);
+    m_sigs[OP_RE_RANGE]      = alloc(psig, m, "re.range",   1, 2, seqAseqA,  reA);
+    m_sigs[OP_RE_CONCAT]     = alloc(psig, m, "re.++",  1, 2, reAreA, reA);
+    m_sigs[OP_RE_UNION]      = alloc(psig, m, "re.union",   1, 2, reAreA, reA);
+    m_sigs[OP_RE_INTERSECT]  = alloc(psig, m, "re.inter",   1, 2, reAreA, reA);
     m_sigs[OP_RE_LOOP]           = alloc(psig, m, "re-loop",    1, 1, &reA, reA);
     m_sigs[OP_RE_EMPTY_SEQ]      = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
@@ -209,7 +211,7 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
     m_sigs[OP_RE_MEMBER]         = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
     m_sigs[OP_STRING_CONST]      = 0;
-    m_sigs[OP_STRING_CONCAT]     = alloc(psig, m, "str.++", 0, 2, str2T, strT);
+    m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
     m_sigs[OP_STRING_LENGTH]     = alloc(psig, m, "str.len", 0, 1, &strT, intT);
     m_sigs[OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
     m_sigs[OP_STRING_STRCTN]     = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
@@ -222,19 +224,15 @@ void seq_decl_plugin::init() {
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
     m_sigs[OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
     m_sigs[OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
-    m_sigs[OP_REGEXP_CONCAT]     = alloc(psig, m, "re.++", 0, 2, re2T, reT);
-    m_sigs[OP_REGEXP_UNION]      = alloc(psig, m, "re.union", 0, 2, re2T, reT);
-    m_sigs[OP_REGEXP_INTER]      = alloc(psig, m, "re.inter", 0, 2, re2T, reT);
-    m_sigs[OP_REGEXP_STAR]       = alloc(psig, m, "re.*", 0, 1, &reT, reT);
-    m_sigs[OP_REGEXP_PLUS]       = alloc(psig, m, "re.+", 0, 1, &reT, reT);
-    m_sigs[OP_REGEXP_OPT]        = alloc(psig, m, "re.opt", 0, 1, &reT, reT);
-    m_sigs[OP_REGEXP_RANGE]      = alloc(psig, m, "re.range", 0, 2, str2T, reT);
     m_sigs[OP_REGEXP_LOOP]       = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
     decl_plugin::set_manager(m, id);
-    m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, STRING_SORT, 0, (parameter const*)0));
+    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, CHAR_SORT, 0, (parameter const*)0));
+    m->inc_ref(m_char);
+    parameter param(m_char);
+    m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
     m->inc_ref(m_string);
 }
 
@@ -249,6 +247,9 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
         if (!parameters[0].is_ast() || !is_sort(parameters[0].get_ast())) {
             m.raise_exception("invalid sequence sort, parameter is not a sort");
         }
+        if (parameters[0].get_ast() == m_char) {
+            return m_string;
+        }
         return m.mk_sort(symbol("Seq"), sort_info(m_family_id, SEQ_SORT, num_parameters, parameters));
     case RE_SORT:
         if (num_parameters != 1) {
@@ -260,6 +261,8 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
     case STRING_SORT:
         return m_string;
+    case CHAR_SORT:
+        return m_char;
     default:
         UNREACHABLE();
         return 0;
@@ -274,12 +277,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     switch(k) {
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_CONS:
-    case OP_SEQ_REV_CONS:
-    case OP_SEQ_HEAD:
-    case OP_SEQ_TAIL:
-    case OP_SEQ_LAST:
-    case OP_SEQ_FIRST:
     case OP_SEQ_PREFIX_OF:
     case OP_SEQ_SUFFIX_OF:
     case OP_SEQ_SUBSEQ_OF:
@@ -289,9 +286,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_OPTION:
     case OP_RE_RANGE:
     case OP_RE_UNION:
-    case OP_RE_INTERSECT:
-    case OP_RE_DIFFERENCE:
-    case OP_RE_COMPLEMENT:
     case OP_RE_EMPTY_SEQ:
     case OP_RE_EMPTY_SET:
     case OP_RE_OF_SEQ:   
@@ -317,15 +311,28 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         return m.mk_const_decl(m_stringc_sym, m_string,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
         
-    case OP_SEQ_CONCAT:
-    case OP_RE_CONCAT:
-    case OP_REGEXP_CONCAT:
-    case OP_STRING_CONCAT: {
+    case OP_SEQ_CONCAT: {
+        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
+        
+        func_decl_info info(m_family_id, k);
+        info.set_left_associative();
+        if (rng == m_string) {
+            return m.mk_func_decl(m_sigs[_OP_STRING_CONCAT]->m_name, rng, rng, rng, info);
+        }
+        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
+    } 
+    case OP_RE_CONCAT:  {
         match_left_assoc(*m_sigs[k], arity, domain, range, rng);
         func_decl_info info(m_family_id, k);
         info.set_left_associative();
         return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
     }
+    case _OP_STRING_CONCAT: {
+        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
+        func_decl_info info(m_family_id, OP_SEQ_CONCAT);
+        info.set_left_associative();
+        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
+    }
 
     case OP_STRING_LENGTH:
     case OP_STRING_SUBSTR:
@@ -339,12 +346,6 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_STRING_STOI:
     case OP_STRING_IN_REGEXP:
     case OP_STRING_TO_REGEXP:
-    case OP_REGEXP_UNION:
-    case OP_REGEXP_INTER:
-    case OP_REGEXP_STAR:
-    case OP_REGEXP_PLUS:
-    case OP_REGEXP_OPT:
-    case OP_REGEXP_RANGE:
     case OP_REGEXP_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index 35e2cbf8a..e85d01799 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -25,19 +25,14 @@ Revision History:
 enum seq_sort_kind {
     SEQ_SORT,
     RE_SORT,
-    STRING_SORT
+    STRING_SORT,
+    CHAR_SORT
 };
 
 enum seq_op_kind {
     OP_SEQ_UNIT,
     OP_SEQ_EMPTY,
     OP_SEQ_CONCAT,
-    OP_SEQ_CONS,
-    OP_SEQ_REV_CONS,
-    OP_SEQ_HEAD,
-    OP_SEQ_TAIL,
-    OP_SEQ_LAST,
-    OP_SEQ_FIRST,
     OP_SEQ_PREFIX_OF,
     OP_SEQ_SUFFIX_OF,
     OP_SEQ_SUBSEQ_OF,
@@ -52,8 +47,6 @@ enum seq_op_kind {
     OP_RE_CONCAT,
     OP_RE_UNION,
     OP_RE_INTERSECT,
-    OP_RE_COMPLEMENT,
-    OP_RE_DIFFERENCE,
     OP_RE_LOOP,
     OP_RE_EMPTY_SET,
     OP_RE_FULL_SET,
@@ -65,7 +58,7 @@ enum seq_op_kind {
 
     // string specific operators.
     OP_STRING_CONST,
-    OP_STRING_CONCAT, 
+    _OP_STRING_CONCAT, 
     OP_STRING_LENGTH, 
     OP_STRING_SUBSTR, 
     OP_STRING_STRCTN, 
@@ -78,13 +71,6 @@ enum seq_op_kind {
     OP_STRING_STOI, 
     OP_STRING_IN_REGEXP, 
     OP_STRING_TO_REGEXP, 
-    OP_REGEXP_CONCAT, 
-    OP_REGEXP_UNION, 
-    OP_REGEXP_INTER, 
-    OP_REGEXP_STAR, 
-    OP_REGEXP_PLUS, 
-    OP_REGEXP_OPT, 
-    OP_REGEXP_RANGE, 
     OP_REGEXP_LOOP, 
     
     LAST_SEQ_OP
@@ -112,6 +98,7 @@ class seq_decl_plugin : public decl_plugin {
     bool             m_init;
     symbol           m_stringc_sym;
     sort*            m_string;
+    sort*            m_char;
 
     void match(psig& sig, unsigned dsz, sort* const* dom, sort* range, sort_ref& rng);
 
@@ -148,6 +135,8 @@ public:
 
     virtual bool is_unique_value(app * e) const { return is_value(e); }
 
+    bool is_char(ast* a) const { return a == m_char; }
+
     app* mk_string(symbol const& s);  
 };
 
@@ -159,6 +148,9 @@ public:
 
     ast_manager& get_manager() const { return m; }
 
+    bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
+    bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
+
     class str {
         seq_util&    u;
         ast_manager& m;
@@ -169,7 +161,7 @@ public:
         app* mk_string(symbol const& s);
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
         app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
-        app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_CONCAT, 2, es); }
+        app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
         app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
         app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
         app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); }
@@ -183,8 +175,7 @@ public:
             return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
         }
         
-        bool is_string(sort* s) const { return is_sort_of(s, m_fid, STRING_SORT); }
-        bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CONCAT); }
+        bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
         bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_LENGTH); }
         bool is_substr(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); }
         bool is_strctn(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_STRCTN); }
@@ -222,13 +213,13 @@ public:
         re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
 
         bool is_to_regexp(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); }
-        bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_CONCAT); }
-        bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_UNION); }
-        bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_INTER); }
-        bool is_star(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_STAR); }
-        bool is_plus(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_PLUS); }
-        bool is_opt(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_OPT); }
-        bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_RANGE); }
+        bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
+        bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }
+        bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
+        bool is_star(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_STAR); }
+        bool is_plus(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_PLUS); }
+        bool is_opt(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_OPTION); }
+        bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_RANGE); }
         bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
        
         MATCH_UNARY(is_to_regexp);
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index b99336b29..03ea3edf8 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -42,13 +42,13 @@ namespace smt {
         }
 
         virtual expr* get_some_value(sort* s) { 
-            if (u.str.is_string(s)) 
+            if (u.is_string(s)) 
                 return u.str.mk_string(symbol(""));            
             NOT_IMPLEMENTED_YET();
             return 0;
         }
         virtual bool get_some_values(sort* s, expr_ref& v1, expr_ref& v2) { 
-            if (u.str.is_string(s)) {
+            if (u.is_string(s)) {
                 v1 = u.str.mk_string("a");
                 v2 = u.str.mk_string("b");
                 return true;
@@ -57,7 +57,7 @@ namespace smt {
             return false; 
         }
         virtual expr* get_fresh_value(sort* s) { 
-            if (u.str.is_string(s)) {
+            if (u.is_string(s)) {
                 while (true) {
                     std::ostringstream strm;
                     strm << "S" << m_next++;

From 70b10d53cf45da3351020e65a45a68946f18e644 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 22:17:36 -0800
Subject: [PATCH 36/38] fix build break - remove tabs

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 scripts/mk_util.py | 8 ++++----
 1 file changed, 4 insertions(+), 4 deletions(-)

diff --git a/scripts/mk_util.py b/scripts/mk_util.py
index a2e93d34c..7e96f3b52 100644
--- a/scripts/mk_util.py
+++ b/scripts/mk_util.py
@@ -411,10 +411,10 @@ def check_dotnet():
         monoCompilerExecutable = CSC
     monoCompilerPath = which(monoCompilerExecutable)
     if monoCompilerPath == None:
-	disable_dotnet()
-	print(("Could not find mono compiler ({}) in your PATH. Not building .NET bindings").format(
+        disable_dotnet()
+        print(("Could not find mono compiler ({}) in your PATH. Not building .NET bindings").format(
               monoCompilerExecutable))
-	return
+        return
     CSC = monoCompilerPath
 
     # Check for gacutil (needed to install the dotnet bindings)
@@ -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 is_python_install_enabled():
+            if not is_python_install_enabled():
                 return
             pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
             if IS_WINDOWS:

From 8bb73c8eae000c8d87aaec05e323ac3090e2e2e9 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 23:34:28 -0800
Subject: [PATCH 37/38] merge seq and string operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/ast_smt2_pp.cpp           |   8 +-
 src/ast/rewriter/seq_rewriter.cpp |  90 +++++++++++----------
 src/ast/rewriter/seq_rewriter.h   |   6 +-
 src/ast/seq_decl_plugin.cpp       | 128 +++++++++++++++++++-----------
 src/ast/seq_decl_plugin.h         |  93 ++++++++++++----------
 src/smt/theory_seq_empty.h        |   6 +-
 6 files changed, 186 insertions(+), 145 deletions(-)

diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp
index 62a6a586e..523d98a93 100644
--- a/src/ast/ast_smt2_pp.cpp
+++ b/src/ast/ast_smt2_pp.cpp
@@ -365,7 +365,7 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d
 
 format * smt2_pp_environment::pp_string_literal(app * t) {
     std::string s;
-    VERIFY (get_sutil().str.is_const(t, s));
+    VERIFY (get_sutil().str.is_string(t, s));
     std::ostringstream buffer;
     buffer << "\"";
     for (unsigned i = 0; i < s.length(); ++i) {
@@ -424,10 +424,10 @@ format_ns::format * smt2_pp_environment::pp_sort(sort * s) {
         fs.push_back(mk_unsigned(m, sbits));
         return mk_seq1(m, fs.begin(), fs.end(), f2f(), "_");
     }
-    if (get_sutil().is_seq(s) && !get_sutil().is_string(s)) {
+    if ((get_sutil().is_seq(s) || get_sutil().is_re(s)) && !get_sutil().is_string(s)) {
         ptr_buffer<format> fs;
         fs.push_back(pp_sort(to_sort(s->get_parameter(0).get_ast())));
-        return mk_seq1(m, fs.begin(), fs.end(), f2f(), "Seq");
+        return mk_seq1(m, fs.begin(), fs.end(), f2f(), get_sutil().is_seq(s)?"Seq":"Re");
     }
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); 
 }
@@ -600,7 +600,7 @@ class smt2_printer {
         if (m_env.get_autil().is_numeral(c) || m_env.get_autil().is_irrational_algebraic_numeral(c)) {
             f = m_env.pp_arith_literal(c, m_pp_decimal, m_pp_decimal_precision);
         }
-        else if (m_env.get_sutil().str.is_const(c)) {
+        else if (m_env.get_sutil().str.is_string(c)) {
             f = m_env.pp_string_literal(c);
         }
         else if (m_env.get_bvutil().is_numeral(c)) {
diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index 00b94e60d..fd370e425 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -29,12 +29,6 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_PREFIX_OF:
-    case OP_SEQ_SUFFIX_OF:
-    case OP_SEQ_SUBSEQ_OF:
-    case OP_SEQ_EXTRACT:
-    case OP_SEQ_NTH:
-    case OP_SEQ_LENGTH:
 
     case OP_RE_PLUS:
     case OP_RE_STAR:
@@ -47,52 +41,60 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
     case OP_RE_EMPTY_SET:
     case OP_RE_FULL_SET:
     case OP_RE_EMPTY_SEQ:
-    case OP_RE_OF_SEQ:
     case OP_RE_OF_PRED:
-    case OP_RE_MEMBER:
         return BR_FAILED;
 
     // string specific operators.
     case OP_STRING_CONST:
         return BR_FAILED;
     case OP_SEQ_CONCAT: 
-    case _OP_STRING_CONCAT:
         SASSERT(num_args == 2);
         return mk_seq_concat(args[0], args[1], result);
-    case OP_STRING_LENGTH:
+    case OP_SEQ_LENGTH:
         SASSERT(num_args == 1);
         return mk_str_length(args[0], result);
-    case OP_STRING_SUBSTR: 
+    case OP_SEQ_EXTRACT:
         SASSERT(num_args == 3);
         return mk_str_substr(args[0], args[1], args[2], result);
-    case OP_STRING_STRCTN: 
+    case OP_SEQ_CONTAINS: 
         SASSERT(num_args == 2);
         return mk_str_strctn(args[0], args[1], result);
-    case OP_STRING_CHARAT:
+    case OP_SEQ_AT:
         SASSERT(num_args == 2);
-        return mk_str_charat(args[0], args[1], result); 
+        return mk_str_at(args[0], args[1], result); 
     case OP_STRING_STRIDOF: 
         SASSERT(num_args == 3);
         return mk_str_stridof(args[0], args[1], args[2], result);
     case OP_STRING_STRREPL: 
         SASSERT(num_args == 3);
         return mk_str_strrepl(args[0], args[1], args[2], result);
-    case OP_STRING_PREFIX: 
+    case OP_SEQ_PREFIX: 
         SASSERT(num_args == 2);
-        return mk_str_prefix(args[0], args[1], result);
-    case OP_STRING_SUFFIX: 
+        return mk_seq_prefix(args[0], args[1], result);
+    case OP_SEQ_SUFFIX: 
         SASSERT(num_args == 2);
-        return mk_str_suffix(args[0], args[1], result);
+        return mk_seq_suffix(args[0], args[1], result);
     case OP_STRING_ITOS: 
         SASSERT(num_args == 1);
         return mk_str_itos(args[0], result);
     case OP_STRING_STOI: 
         SASSERT(num_args == 1);
         return mk_str_stoi(args[0], result);
-    case OP_STRING_IN_REGEXP: 
-    case OP_STRING_TO_REGEXP: 
+    case OP_SEQ_TO_RE:
+    case OP_SEQ_IN_RE:
     case OP_REGEXP_LOOP: 
         return BR_FAILED;
+    case _OP_STRING_CONCAT:
+    case _OP_STRING_PREFIX:
+    case _OP_STRING_SUFFIX:
+    case _OP_STRING_STRCTN:
+    case _OP_STRING_LENGTH:
+    case _OP_STRING_CHARAT:
+    case _OP_STRING_IN_REGEXP: 
+    case _OP_STRING_TO_REGEXP: 
+    case _OP_STRING_SUBSTR: 
+
+        UNREACHABLE();
     }
     return BR_FAILED;
 }
@@ -107,8 +109,8 @@ br_status seq_rewriter::mk_app_core(func_decl * f, unsigned num_args, expr * con
 br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
     expr* c, *d;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         result = m_util.str.mk_string(s1 + s2);
         return BR_DONE;
@@ -117,16 +119,16 @@ br_status seq_rewriter::mk_seq_concat(expr* a, expr* b, expr_ref& result) {
         result = m_util.str.mk_concat(m_util.str.mk_concat(a, c), d);
         return BR_REWRITE2;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = b;
         return BR_DONE;
     }
-    if (isc2 && s2.length() == 0) {
+    if (m_util.str.is_empty(b)) {
         result = a;
         return BR_DONE;
     }
     if (m_util.str.is_concat(a, c, d) && 
-        m_util.str.is_const(d, s1) && isc2) {
+        m_util.str.is_string(d, s1) && isc2) {
         result = m_util.str.mk_concat(c, m_util.str.mk_string(s1 + s2));
         return BR_DONE;
     }
@@ -140,7 +142,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     unsigned len = 0;
     size_t j = 0;
     for (unsigned i = 0; i < m_es.size(); ++i) {
-        if (m_util.str.is_const(m_es[i], b)) {
+        if (m_util.str.is_string(m_es[i], b)) {
             len += b.length();
         }
         else {
@@ -169,7 +171,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
 br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s;
     rational pos, len;
-    if (m_util.str.is_const(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
+    if (m_util.str.is_string(a, s) && m_autil.is_numeral(b, pos) && m_autil.is_numeral(c, len) &&
         pos.is_unsigned() && len.is_unsigned() && pos.get_unsigned() <= s.length()) {
         unsigned _pos = pos.get_unsigned();
         unsigned _len = len.get_unsigned();
@@ -180,17 +182,17 @@ br_status seq_rewriter::mk_str_substr(expr* a, expr* b, expr* c, expr_ref& resul
 }
 br_status seq_rewriter::mk_str_strctn(expr* a, expr* b, expr_ref& result) {
     std::string c, d;
-    if (m_util.str.is_const(a, c) && m_util.str.is_const(b, d)) {
+    if (m_util.str.is_string(a, c) && m_util.str.is_string(b, d)) {
         result = m().mk_bool_val(0 != strstr(d.c_str(), c.c_str()));
         return BR_DONE;
     }
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_str_at(expr* a, expr* b, expr_ref& result) {
     std::string c;
     rational r;
-    if (m_util.str.is_const(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
+    if (m_util.str.is_string(a, c) && m_autil.is_numeral(b, r) && r.is_unsigned()) {
         unsigned j = r.get_unsigned();
         if (j < c.length()) {
             char ch = c[j];
@@ -206,8 +208,8 @@ br_status seq_rewriter::mk_str_charat(expr* a, expr* b, expr_ref& result) {
 br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2;
     rational r;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
 
     if (isc1 && isc2 && m_autil.is_numeral(c, r) && r.is_unsigned()) {
         for (unsigned i = r.get_unsigned(); i < s1.length(); ++i) {
@@ -224,7 +226,7 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
         return BR_DONE;
     }
     
-    if (isc2 && s2.length() == 0) {
+    if (m_util.str.is_empty(b)) {
         result = c;
         return BR_DONE;
     }
@@ -234,8 +236,8 @@ br_status seq_rewriter::mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& resu
 
 br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result) {
     std::string s1, s2, s3;
-    if (m_util.str.is_const(a, s1) && m_util.str.is_const(b, s2) && 
-        m_util.str.is_const(c, s3)) {
+    if (m_util.str.is_string(a, s1) && m_util.str.is_string(b, s2) && 
+        m_util.str.is_string(c, s3)) {
         std::ostringstream buffer;
         for (size_t i = 0; i < s1.length(); ) {
             if (strncmp(s1.c_str() + i, s2.c_str(), s2.length()) == 0) {
@@ -257,10 +259,10 @@ br_status seq_rewriter::mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& resu
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_seq_prefix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    bool isc1 = m_util.str.is_const(a, s1);
-    bool isc2 = m_util.str.is_const(b, s2);
+    bool isc1 = m_util.str.is_string(a, s1);
+    bool isc2 = m_util.str.is_string(b, s2);
     if (isc1 && isc2) {
         bool prefix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && prefix; ++i) {
@@ -269,17 +271,17 @@ br_status seq_rewriter::mk_str_prefix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(prefix);
         return BR_DONE;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = m().mk_true();
         return BR_DONE;
     }
     return BR_FAILED;
 }
 
-br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
+br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
     std::string s1, s2;
-    bool isc1 = m_util.str.is_const(a, s1);
-    if (isc1 && m_util.str.is_const(b, s2)) {
+    bool isc1 = m_util.str.is_string(a, s1);
+    if (isc1 && m_util.str.is_string(b, s2)) {
         bool suffix = s1.length() <= s2.length();
         for (unsigned i = 0; i < s1.length() && suffix; ++i) {
             suffix = s1[s1.length() - i - 1] == s2[s2.length() - i - 1];
@@ -287,7 +289,7 @@ br_status seq_rewriter::mk_str_suffix(expr* a, expr* b, expr_ref& result) {
         result = m().mk_bool_val(suffix);
         return BR_DONE;
     }
-    if (isc1 && s1.length() == 0) {
+    if (m_util.str.is_empty(a)) {
         result = m().mk_true();
         return BR_DONE;
     }
@@ -304,7 +306,7 @@ br_status seq_rewriter::mk_str_itos(expr* a, expr_ref& result) {
 }
 br_status seq_rewriter::mk_str_stoi(expr* a, expr_ref& result) {
     std::string s;
-    if (m_util.str.is_const(a, s)) {
+    if (m_util.str.is_string(a, s)) {
         for (unsigned i = 0; i < s.length(); ++i) {
             if (s[i] == '-') { if (i != 0) return BR_FAILED; }
             else if ('0' <= s[i] && s[i] <= '9') continue;
diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h
index 2d2909018..4674a7535 100644
--- a/src/ast/rewriter/seq_rewriter.h
+++ b/src/ast/rewriter/seq_rewriter.h
@@ -38,11 +38,11 @@ class seq_rewriter {
     br_status mk_str_length(expr* a, expr_ref& result);
     br_status mk_str_substr(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strctn(expr* a, expr* b, expr_ref& result);
-    br_status mk_str_charat(expr* a, expr* b, expr_ref& result);
+    br_status mk_str_at(expr* a, expr* b, expr_ref& result);
     br_status mk_str_stridof(expr* a, expr* b, expr* c, expr_ref& result);
     br_status mk_str_strrepl(expr* a, expr* b, expr* c, expr_ref& result);
-    br_status mk_str_prefix(expr* a, expr* b, expr_ref& result);
-    br_status mk_str_suffix(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_prefix(expr* a, expr* b, expr_ref& result);
+    br_status mk_seq_suffix(expr* a, expr* b, expr_ref& result);
     br_status mk_str_itos(expr* a, expr_ref& result);
     br_status mk_str_stoi(expr* a, expr_ref& result);
     br_status mk_str_in_regexp(expr* a, expr* b, expr_ref& result);
diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp
index 5fd8c0df7..b47c4209d 100644
--- a/src/ast/seq_decl_plugin.cpp
+++ b/src/ast/seq_decl_plugin.cpp
@@ -161,7 +161,6 @@ void seq_decl_plugin::init() {
     ast_manager& m = *m_manager;
     m_init = true;
     sort* A = m.mk_uninterpreted_sort(symbol((unsigned)0));
-    sort* B = m.mk_uninterpreted_sort(symbol((unsigned)1));
     sort* strT = m_string;
     parameter paramA(A);
     parameter paramS(strT);
@@ -174,27 +173,27 @@ void seq_decl_plugin::init() {
     sort* u16T = 0;
     sort* u32T = 0;
     sort* seqAseqA[2] = { seqA, seqA };
-    sort* seqAB[2] = { seqA, B };
     sort* seqAreA[2] = { seqA, reA };
     sort* reAreA[2] = { reA, reA };
     sort* AA[2] = { A, A };
-    sort* seqABB[3] = { seqA, B, B };
+    sort* seqAint2T[3] = { seqA, intT, intT };
     sort* str2T[2] = { strT, strT };
     sort* str3T[3] = { strT, strT, strT };
     sort* strTint2T[3] = { strT, intT, intT };
     sort* re2T[2] = { reT, reT };
     sort* strTreT[2] = { strT, reT };
     sort* str2TintT[3] = { strT, strT, intT };
+    sort* seqAintT[2] = { seqA, intT };
     m_sigs.resize(LAST_SEQ_OP);
     // TBD: have (par ..) construct and load parameterized signature from premable.
     m_sigs[OP_SEQ_UNIT]      = alloc(psig, m, "seq.unit",   1, 1, &A, seqA);
     m_sigs[OP_SEQ_EMPTY]     = alloc(psig, m, "seq.empty",  1, 0, 0, seqA); 
     m_sigs[OP_SEQ_CONCAT]    = alloc(psig, m, "seq.++", 1, 2, seqAseqA, seqA);
-    m_sigs[OP_SEQ_PREFIX_OF] = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_SUFFIX_OF] = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_SUBSEQ_OF] = alloc(psig, m, "seq-subseq-of", 1, 2, seqAseqA, boolT);
-    m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq-extract", 2, 3, seqABB, seqA);
-    m_sigs[OP_SEQ_NTH]       = alloc(psig, m, "seq-nth", 2, 2, seqAB, A);
+    m_sigs[OP_SEQ_PREFIX]    = alloc(psig, m, "seq.prefixof", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_SUFFIX]    = alloc(psig, m, "seq.suffixof", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_CONTAINS]  = alloc(psig, m, "seq.contains", 1, 2, seqAseqA, boolT);
+    m_sigs[OP_SEQ_EXTRACT]   = alloc(psig, m, "seq.extract", 1, 3, seqAint2T, seqA);
+    m_sigs[OP_SEQ_AT]        = alloc(psig, m, "seq.at", 1, 2, seqAintT, seqA);
     m_sigs[OP_SEQ_LENGTH]    = alloc(psig, m, "seq-length", 1, 1, &seqA, intT);
     m_sigs[OP_RE_PLUS]       = alloc(psig, m, "re.+",    1, 1, &reA, reA);
     m_sigs[OP_RE_STAR]       = alloc(psig, m, "re.*",    1, 1, &reA, reA);
@@ -207,29 +206,29 @@ void seq_decl_plugin::init() {
     m_sigs[OP_RE_EMPTY_SEQ]      = alloc(psig, m, "re-empty-seq", 1, 0, 0, reA);
     m_sigs[OP_RE_EMPTY_SET]      = alloc(psig, m, "re-empty-set", 1, 0, 0, reA);
     m_sigs[OP_RE_FULL_SET]       = alloc(psig, m, "re-full-set", 1, 0, 0, reA);
-    m_sigs[OP_RE_OF_SEQ]         = alloc(psig, m, "re-of-seq",  1, 1, &seqA, reA);
+    m_sigs[OP_SEQ_TO_RE]         = alloc(psig, m, "seq.to.re",  1, 1, &seqA, reA);
     m_sigs[OP_RE_OF_PRED]        = alloc(psig, m, "re-of-pred", 1, 1, &predA, reA);
-    m_sigs[OP_RE_MEMBER]         = alloc(psig, m, "re-member", 1, 2, seqAreA, boolT);
+    m_sigs[OP_SEQ_IN_RE]         = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
     m_sigs[OP_STRING_CONST]      = 0;
-    m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
-    m_sigs[OP_STRING_LENGTH]     = alloc(psig, m, "str.len", 0, 1, &strT, intT);
-    m_sigs[OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
-    m_sigs[OP_STRING_STRCTN]     = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
-    m_sigs[OP_STRING_CHARAT]     = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
     m_sigs[OP_STRING_STRIDOF]    = alloc(psig, m, "str.indexof", 0, 3, str2TintT, intT);
     m_sigs[OP_STRING_STRREPL]    = alloc(psig, m, "str.replace", 0, 3, str3T, strT);
-    m_sigs[OP_STRING_PREFIX]     = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
-    m_sigs[OP_STRING_SUFFIX]     = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
     m_sigs[OP_STRING_ITOS]       = alloc(psig, m, "int.to.str", 0, 1, &intT, strT);
     m_sigs[OP_STRING_STOI]       = alloc(psig, m, "str.to.int", 0, 1, &strT, intT);
-    m_sigs[OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
-    m_sigs[OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
     m_sigs[OP_REGEXP_LOOP]       = alloc(psig, m, "re.loop", 0, 2, strTint2T, reT); // maybe 3 arguments.
+    m_sigs[_OP_STRING_CONCAT]    = alloc(psig, m, "str.++", 1, 2, str2T, strT);
+    m_sigs[_OP_STRING_LENGTH]    = alloc(psig, m, "str.len", 0, 1, &strT, intT);
+    m_sigs[_OP_STRING_STRCTN]    = alloc(psig, m, "str.contains", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_CHARAT]    = alloc(psig, m, "str.at", 0, 2, strTint2T, strT);
+    m_sigs[_OP_STRING_PREFIX]    = alloc(psig, m, "str.prefixof", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_SUFFIX]    = alloc(psig, m, "str.suffixof", 0, 2, str2T, boolT);
+    m_sigs[_OP_STRING_IN_REGEXP]  = alloc(psig, m, "str.in.re", 0, 2, strTreT, boolT);
+    m_sigs[_OP_STRING_TO_REGEXP]  = alloc(psig, m, "str.to.re", 0, 1, &strT, reT);
+    m_sigs[_OP_STRING_SUBSTR]     = alloc(psig, m, "str.substr", 0, 3, strTint2T, boolT);
 }
 
 void seq_decl_plugin::set_manager(ast_manager* m, family_id id) {
     decl_plugin::set_manager(m, id);
-    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, CHAR_SORT, 0, (parameter const*)0));
+    m_char = m->mk_sort(symbol("Char"), sort_info(m_family_id, _CHAR_SORT, 0, (parameter const*)0));
     m->inc_ref(m_char);
     parameter param(m_char);
     m_string = m->mk_sort(symbol("String"), sort_info(m_family_id, SEQ_SORT, 1, &param));
@@ -259,9 +258,9 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
             m.raise_exception("invalid regex sort, parameter is not a sort");
         }
         return m.mk_sort(symbol("RegEx"), sort_info(m_family_id, RE_SORT, num_parameters, parameters));
-    case STRING_SORT:
+    case _STRING_SORT:
         return m_string;
-    case CHAR_SORT:
+    case _CHAR_SORT:
         return m_char;
     default:
         UNREACHABLE();
@@ -269,6 +268,21 @@ sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter
     }
 }
 
+func_decl* seq_decl_plugin::mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string) {
+    ast_manager& m = *m_manager;
+    sort_ref rng(m);
+    match(*m_sigs[k], arity, domain, range, rng);
+    return m.mk_func_decl(m_sigs[(domain[0] == m_string)?k_string:k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
+}
+
+
+func_decl* seq_decl_plugin::mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq) {
+    ast_manager& m = *m_manager;
+    sort_ref rng(m);
+    match(*m_sigs[k], arity, domain, range, rng);
+    return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k_seq));
+}
+
 func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters, parameter const * parameters, 
                                           unsigned arity, sort * const * domain, sort * range) {
     init();
@@ -277,10 +291,7 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     switch(k) {
     case OP_SEQ_UNIT:
     case OP_SEQ_EMPTY:
-    case OP_SEQ_PREFIX_OF:
-    case OP_SEQ_SUFFIX_OF:
-    case OP_SEQ_SUBSEQ_OF:
-    case OP_SEQ_LENGTH:
+        
     case OP_RE_PLUS:
     case OP_RE_STAR:
     case OP_RE_OPTION:
@@ -288,14 +299,8 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
     case OP_RE_UNION:
     case OP_RE_EMPTY_SEQ:
     case OP_RE_EMPTY_SET:
-    case OP_RE_OF_SEQ:   
+
     case OP_RE_OF_PRED:
-    case OP_RE_MEMBER:
-        match(*m_sigs[k], arity, domain, range, rng);
-        return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
-    case OP_SEQ_EXTRACT:
-    case OP_SEQ_NTH:
-        // TBD check numeric arguments for being BVs or integers.
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
     case OP_RE_LOOP:
@@ -312,14 +317,10 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
                                func_decl_info(m_family_id, OP_STRING_CONST, num_parameters, parameters));
         
     case OP_SEQ_CONCAT: {
-        match_left_assoc(*m_sigs[k], arity, domain, range, rng);
-        
+        match_left_assoc(*m_sigs[k], arity, domain, range, rng);        
         func_decl_info info(m_family_id, k);
         info.set_left_associative();
-        if (rng == m_string) {
-            return m.mk_func_decl(m_sigs[_OP_STRING_CONCAT]->m_name, rng, rng, rng, info);
-        }
-        return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
+        return m.mk_func_decl(m_sigs[(rng == m_string)?_OP_STRING_CONCAT:k]->m_name, rng, rng, rng, info);
     } 
     case OP_RE_CONCAT:  {
         match_left_assoc(*m_sigs[k], arity, domain, range, rng);
@@ -333,19 +334,50 @@ func_decl * seq_decl_plugin::mk_func_decl(decl_kind k, unsigned num_parameters,
         info.set_left_associative();
         return m.mk_func_decl(m_sigs[k]->m_name, rng, rng, rng, info);
     }
+    case OP_SEQ_PREFIX:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_PREFIX);
+    case _OP_STRING_PREFIX:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_PREFIX);
+
+    case OP_SEQ_SUFFIX:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_SUFFIX);
+    case _OP_STRING_SUFFIX:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_SUFFIX);
+
+    case OP_SEQ_LENGTH:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_LENGTH);
+    case _OP_STRING_LENGTH:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_LENGTH);
+
+    case OP_SEQ_CONTAINS:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_STRCTN);
+    case _OP_STRING_STRCTN:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_CONTAINS);
+
+    case OP_SEQ_TO_RE:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_TO_REGEXP);
+    case _OP_STRING_TO_REGEXP:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_TO_RE);
+
+    case OP_SEQ_IN_RE:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_IN_REGEXP);
+    case _OP_STRING_IN_REGEXP:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_IN_RE);
+
+    case OP_SEQ_AT:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_CHARAT);
+    case _OP_STRING_CHARAT:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_AT);
+
+    case OP_SEQ_EXTRACT:
+        return mk_seq_fun(k, arity, domain, range, _OP_STRING_SUBSTR);
+    case _OP_STRING_SUBSTR:
+        return mk_str_fun(k, arity, domain, range, OP_SEQ_EXTRACT);
 
-    case OP_STRING_LENGTH:
-    case OP_STRING_SUBSTR:
-    case OP_STRING_STRCTN:
-    case OP_STRING_CHARAT:
     case OP_STRING_STRIDOF:
     case OP_STRING_STRREPL:
-    case OP_STRING_PREFIX:
-    case OP_STRING_SUFFIX:
     case OP_STRING_ITOS:
     case OP_STRING_STOI:
-    case OP_STRING_IN_REGEXP:
-    case OP_STRING_TO_REGEXP:
     case OP_REGEXP_LOOP:
         match(*m_sigs[k], arity, domain, range, rng);
         return m.mk_func_decl(m_sigs[k]->m_name, arity, domain, rng, func_decl_info(m_family_id, k));
@@ -369,7 +401,7 @@ void seq_decl_plugin::get_sort_names(svector<builtin_name> & sort_names, symbol
     init();
     sort_names.push_back(builtin_name("Seq",   SEQ_SORT));
     sort_names.push_back(builtin_name("RegEx", RE_SORT));
-    sort_names.push_back(builtin_name("String", STRING_SORT));
+    sort_names.push_back(builtin_name("String", _STRING_SORT));
 }
 
 app* seq_decl_plugin::mk_string(symbol const& s) {
diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h
index e85d01799..c61e3cc43 100644
--- a/src/ast/seq_decl_plugin.h
+++ b/src/ast/seq_decl_plugin.h
@@ -11,10 +11,12 @@ Abstract:
 
 Author:
 
-    Nikolaj Bjorner (nbjorner) 2011-14-11
+    Nikolaj Bjorner (nbjorner) 2011-11-14
 
 Revision History:
 
+    Updated to string sequences 2015-12-5
+
 --*/
 #ifndef SEQ_DECL_PLUGIN_H_
 #define SEQ_DECL_PLUGIN_H_
@@ -25,20 +27,22 @@ Revision History:
 enum seq_sort_kind {
     SEQ_SORT,
     RE_SORT,
-    STRING_SORT,
-    CHAR_SORT
+    _STRING_SORT,  // internal only
+    _CHAR_SORT     // internal only
 };
 
 enum seq_op_kind {
     OP_SEQ_UNIT,
     OP_SEQ_EMPTY,
     OP_SEQ_CONCAT,
-    OP_SEQ_PREFIX_OF,
-    OP_SEQ_SUFFIX_OF,
-    OP_SEQ_SUBSEQ_OF,
+    OP_SEQ_PREFIX,
+    OP_SEQ_SUFFIX,
+    OP_SEQ_CONTAINS,
     OP_SEQ_EXTRACT,
-    OP_SEQ_NTH,
+    OP_SEQ_AT,
     OP_SEQ_LENGTH,
+    OP_SEQ_TO_RE,
+    OP_SEQ_IN_RE,
 
     OP_RE_PLUS,
     OP_RE_STAR,
@@ -51,28 +55,26 @@ enum seq_op_kind {
     OP_RE_EMPTY_SET,
     OP_RE_FULL_SET,
     OP_RE_EMPTY_SEQ,
-    OP_RE_OF_SEQ,
     OP_RE_OF_PRED,
-    OP_RE_MEMBER,
 
 
     // string specific operators.
     OP_STRING_CONST,
-    _OP_STRING_CONCAT, 
-    OP_STRING_LENGTH, 
-    OP_STRING_SUBSTR, 
-    OP_STRING_STRCTN, 
-    OP_STRING_CHARAT, 
-    OP_STRING_STRIDOF, 
-    OP_STRING_STRREPL, 
-    OP_STRING_PREFIX, 
-    OP_STRING_SUFFIX, 
+    OP_STRING_STRIDOF, // TBD generalize
+    OP_STRING_STRREPL, // TBD generalize
     OP_STRING_ITOS, 
     OP_STRING_STOI, 
-    OP_STRING_IN_REGEXP, 
-    OP_STRING_TO_REGEXP, 
-    OP_REGEXP_LOOP, 
-    
+    OP_REGEXP_LOOP,    // TBD re-loop: integers as parameters or arguments?
+    // internal only operators. Converted to SEQ variants.
+    _OP_STRING_CONCAT, 
+    _OP_STRING_LENGTH, 
+    _OP_STRING_STRCTN,
+    _OP_STRING_PREFIX, 
+    _OP_STRING_SUFFIX, 
+    _OP_STRING_IN_REGEXP, 
+    _OP_STRING_TO_REGEXP, 
+    _OP_STRING_CHARAT, 
+    _OP_STRING_SUBSTR,      
     LAST_SEQ_OP
 };
 
@@ -110,6 +112,9 @@ class seq_decl_plugin : public decl_plugin {
 
     bool is_sort_param(sort* s, unsigned& idx);
 
+    func_decl* mk_seq_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_string);
+    func_decl* mk_str_fun(decl_kind k, unsigned arity, sort* const* domain, sort* range, decl_kind k_seq);
+
     void init();
 
     virtual void set_manager(ast_manager * m, family_id id);
@@ -150,6 +155,7 @@ public:
 
     bool is_string(sort* s) const { return is_seq(s) && seq.is_char(s->get_parameter(0).get_ast()); }
     bool is_seq(sort* s) const { return is_sort_of(s, m_fid, SEQ_SORT); }
+    bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
 
     class str {
         seq_util&    u;
@@ -162,45 +168,46 @@ public:
         app* mk_string(char const* s) { return mk_string(symbol(s)); }
         app* mk_string(std::string const& s) { return mk_string(symbol(s.c_str())); }
         app* mk_concat(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONCAT, 2, es); }
-        app* mk_length(expr* a) { return m.mk_app(m_fid, OP_STRING_LENGTH, 1, &a); }
-        app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_STRING_SUBSTR, 3, es); }
-        app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_STRING_STRCTN, 2, es); }
+        app* mk_length(expr* a) { return m.mk_app(m_fid, OP_SEQ_LENGTH, 1, &a); }
+        app* mk_substr(expr* a, expr* b, expr* c) { expr* es[3] = { a, b, c }; return m.mk_app(m_fid, OP_SEQ_EXTRACT, 3, es); }
+        app* mk_strctn(expr* a, expr* b) { expr* es[2] = { a, b }; return m.mk_app(m_fid, OP_SEQ_CONTAINS, 2, es); }
 
-        bool is_const(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
+        bool is_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
         
-        bool is_const(expr const* n, std::string& s) const {
-            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
+        bool is_string(expr const* n, std::string& s) const {
+            return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol().str(), true);
         }
-        bool is_const(expr const* n, symbol& s) const {
-            return is_const(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
+        bool is_string(expr const* n, symbol& s) const {
+            return is_string(n) && (s = to_app(n)->get_decl()->get_parameter(0).get_symbol(), true);
         }
         
+        bool is_empty(expr const* n) const { symbol s; return is_app_of(n, m_fid, OP_SEQ_EMPTY) || (is_string(n, s) && !s.is_numerical() && strcmp(s.bare_str(),"") == 0); }
         bool is_concat(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONCAT); }
-        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_LENGTH); }
-        bool is_substr(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUBSTR); }
-        bool is_strctn(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_STRCTN); }
-        bool is_charat(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_CHARAT); }
+        bool is_length(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_LENGTH); }
+        bool is_extract(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_EXTRACT); }
+        bool is_contains(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_CONTAINS); }
+        bool is_at(expr const* n)      const { return is_app_of(n, m_fid, OP_SEQ_AT); }
         bool is_stridof(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_STRIDOF); }
         bool is_repl(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STRREPL); }
-        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_PREFIX); }
-        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_STRING_SUFFIX); }
+        bool is_prefix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_PREFIX); }
+        bool is_suffix(expr const* n)  const { return is_app_of(n, m_fid, OP_SEQ_SUFFIX); }
         bool is_itos(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_ITOS); }
         bool is_stoi(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_STOI); }
-        bool is_in_regexp(expr const* n) const { return is_app_of(n, m_fid, OP_STRING_IN_REGEXP); }
+        bool is_in_re(expr const* n) const { return is_app_of(n, m_fid, OP_SEQ_IN_RE); }
 
         
         MATCH_BINARY(is_concat);
         MATCH_UNARY(is_length);
-        MATCH_TERNARY(is_substr);
-        MATCH_BINARY(is_strctn);
-        MATCH_BINARY(is_charat);
+        MATCH_TERNARY(is_extract);
+        MATCH_BINARY(is_contains);
+        MATCH_BINARY(is_at);
         MATCH_BINARY(is_stridof);
         MATCH_BINARY(is_repl);
         MATCH_BINARY(is_prefix);
         MATCH_BINARY(is_suffix);
         MATCH_UNARY(is_itos);
         MATCH_UNARY(is_stoi);
-        MATCH_BINARY(is_in_regexp);        
+        MATCH_BINARY(is_in_re);        
 
         void get_concat(expr* e, ptr_vector<expr>& es) const;
     };
@@ -212,7 +219,7 @@ public:
     public:
         re(seq_util& u):u(u), m(u.m), m_fid(u.m_fid) {}
 
-        bool is_to_regexp(expr const* n)    const { return is_app_of(n, m_fid, OP_STRING_TO_REGEXP); }
+        bool is_to_re(expr const* n)    const { return is_app_of(n, m_fid, OP_SEQ_TO_RE); }
         bool is_concat(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_CONCAT); }
         bool is_union(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_UNION); }
         bool is_inter(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_INTERSECT); }
@@ -222,7 +229,7 @@ public:
         bool is_range(expr const* n)    const { return is_app_of(n, m_fid, OP_RE_RANGE); }
         bool is_loop(expr const* n)    const { return is_app_of(n, m_fid, OP_REGEXP_LOOP); }
        
-        MATCH_UNARY(is_to_regexp);
+        MATCH_UNARY(is_to_re);
         MATCH_BINARY(is_concat);
         MATCH_BINARY(is_union);
         MATCH_BINARY(is_inter);
diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h
index 03ea3edf8..e8e619bf8 100644
--- a/src/smt/theory_seq_empty.h
+++ b/src/smt/theory_seq_empty.h
@@ -71,9 +71,9 @@ namespace smt {
             return 0;
         }
         virtual void register_value(expr* n) {
-            std::string sym;
-            if (u.str.is_const(n, sym)) {
-                m_strings.insert(symbol(sym.c_str()));
+            symbol sym;
+            if (u.str.is_string(n, sym)) {
+                m_strings.insert(sym);
             }
         }
     };

From 03d1391ded7ac0702f3749f669bd34ee41bba597 Mon Sep 17 00:00:00 2001
From: Nikolaj Bjorner <nbjorner@microsoft.com>
Date: Sun, 6 Dec 2015 23:37:37 -0800
Subject: [PATCH 38/38] merge seq and string operators

Signed-off-by: Nikolaj Bjorner <nbjorner@microsoft.com>
---
 src/ast/rewriter/seq_rewriter.cpp | 4 ++--
 1 file changed, 2 insertions(+), 2 deletions(-)

diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp
index fd370e425..96590a40a 100644
--- a/src/ast/rewriter/seq_rewriter.cpp
+++ b/src/ast/rewriter/seq_rewriter.cpp
@@ -139,7 +139,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
     std::string b;
     m_es.reset();
     m_util.str.get_concat(a, m_es);
-    unsigned len = 0;
+    size_t len = 0;
     size_t j = 0;
     for (unsigned i = 0; i < m_es.size(); ++i) {
         if (m_util.str.is_string(m_es[i], b)) {
@@ -151,7 +151,7 @@ br_status seq_rewriter::mk_str_length(expr* a, expr_ref& result) {
         }
     }
     if (j == 0) {
-        result = m_autil.mk_numeral(rational(b.length(), rational::ui64()), true);
+        result = m_autil.mk_numeral(rational(len, rational::ui64()), true);
         return BR_DONE;
     }
     if (j != m_es.size()) {