Merge branch 'master' of https://github.com/Z3Prover/z3

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
+    
+

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') 

scripts/mk_util.py

@@ -34,6 +34,13 @@ 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")
+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']
@@ -67,9 +74,10 @@ ONLY_MAKEFILES = False
 Z3PY_SRC_DIR=None
 VS_PROJ = False
 TRACE = False
-DOTNET_ENABLED=False
+DOTNET_ENABLED=True
 JAVA_ENABLED=False
 ML_ENABLED=False
+PYTHON_INSTALL_ENABLED=True
 STATIC_LIB=False
 VER_MAJOR=None
 VER_MINOR=None
@@ -139,6 +147,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):
@@ -384,6 +393,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:
+        disable_dotnet()
+        print(("Could not find mono compiler ({}) in your PATH. Not building .NET bindings").format(
+              monoCompilerExecutable))
+        return
+    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";;')
@@ -528,8 +574,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
@@ -550,6 +594,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.")
@@ -561,8 +606,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.")
@@ -586,19 +630,25 @@ 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")
+    print("  Z3_INSTALL_PKGCONFIG_DIR Install directory for pkgconfig files relative to install prefix")
     exit(exit_code)
 
 # Parse configuration option for mk_make script
 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',
                                                ['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,10 +687,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')
-            mk_dir(PYTHON_PACKAGE_DIR)
-            if sys.version >= "3":
-                mk_dir(os.path.join(PYTHON_PACKAGE_DIR, '__pycache__'))
+        elif opt in ('--pypkgdir'):
+            PYTHON_PACKAGE_DIR = arg
         elif IS_WINDOWS and opt == '--parallel':
             VS_PAR = True
             VS_PAR_NUM = int(arg)
@@ -662,6 +710,17 @@ def parse_options():
         else:
             print("ERROR: Invalid command line option '%s'" % opt)
             display_help(1)
+    # Handle the Python package directory
+    if IS_WINDOWS:
+        PYTHON_INSTALL_ENABLED = True
+    else:
+        if not PYTHON_PACKAGE_DIR.startswith(PREFIX):
+            print(("Warning: The detected Python package directory (%s)"
+                   " does not live under the installation prefix (%s)"
+                   ". This would lead to a broken Python installation."
+                   "Use --pypkgdir= to change the Python package directory") %
+                  (PYTHON_PACKAGE_DIR, PREFIX))
+            PYTHON_INSTALL_ENABLED = False
 
 # Return a list containing a file names included using '#include' in
 # the given C/C++ file named fname.
@@ -749,6 +808,16 @@ def is_java_enabled():
 def is_ml_enabled():
     return 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
+
 def is_compiler(given, expected):
     """
     Return True if the 'given' compiler is the expected one.
@@ -992,17 +1061,21 @@ 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)))
+            MakeRuleCmd.install_files(
+                out,
+                os.path.join(self.to_src_dir, include),
+                os.path.join(INSTALL_INCLUDE_DIR, include)
+            )
 
     def mk_uninstall(self, out):
         for include in self.includes2install:
-            out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', '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)
@@ -1078,23 +1151,24 @@ 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)))
+            MakeRuleCmd.install_files(out, exefile, os.path.join(INSTALL_BIN_DIR, 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))
+        if self.install:
+            exefile = '%s$(EXE_EXT)' % self.exe_name
+            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):
@@ -1224,36 +1298,91 @@ 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(PYTHON_PACKAGE_DIR, dllfile)))
+            dllInstallPath = os.path.join(INSTALL_LIB_DIR, dllfile)
+            MakeRuleCmd.install_files(out, dllfile, dllInstallPath)
+            if not is_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))
+            else:
+                # Create symbolic link to save space.
+                # It's important that this symbolic link be relative (rather
+                # than absolute) so that the install is relocatable (needed for
+                # staged installs that use DESTDIR).
+                MakeRuleCmd.create_relative_symbolic_link(out, dllInstallPath, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
             if self.static:
                 libfile = '%s$(LIB_EXT)' % self.dll_name
-                out.write('\t@cp %s %s\n' % (libfile, os.path.join('$(PREFIX)', '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
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', 'lib', dllfile))
-        out.write('\t@rm -f %s\n' % os.path.join(PYTHON_PACKAGE_DIR, dllfile))
+        MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, dllfile))
+        if is_python_install_enabled():
+            pythonPkgDirWithoutPrefix = strip_path_prefix(PYTHON_PACKAGE_DIR, PREFIX)
+            MakeRuleCmd.remove_installed_files(out, os.path.join(pythonPkgDirWithoutPrefix, dllfile))
         libfile = '%s$(LIB_EXT)' % self.dll_name
-        out.write('\t@rm -f %s\n' % os.path.join('$(PREFIX)', '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 PythonInstallComponent(Component):
+    def __init__(self, name):
+        Component.__init__(self, name, None, [])
+
+    def main_component(self):
+        return is_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):
@@ -1265,37 +1394,113 @@ 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 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))
+
+        # Create pkg-config file
+        self.mk_pkg_config_file()
+        return
 
     def main_component(self):
         return DOTNET_ENABLED
@@ -1306,14 +1511,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))
 
 
 
@@ -1321,6 +1526,50 @@ class DotNetDLLComponent(Component):
         # Do nothing
         return
 
+    def mk_install_deps(self, out):
+        if not DOTNET_ENABLED:
+            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.gac_pkg_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)
+
+        # 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):
         Component.__init__(self, name, path, deps)
@@ -1383,34 +1632,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
-            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(INSTALL_LIB_DIR, dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            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
-            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(INSTALL_LIB_DIR, dllfile))
+            jarfile = '{}.jar'.format(self.package_name)
+            MakeRuleCmd.remove_installed_files(out, os.path.join(INSTALL_LIB_DIR, jarfile))
 
 class MLComponent(Component):
     def __init__(self, name, lib_name, path, deps):
@@ -1631,7 +1882,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:
@@ -1755,6 +2006,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)
@@ -1998,6 +2253,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()
 
@@ -2009,35 +2267,18 @@ 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'))
+    MakeRuleCmd.make_install_directory(out, INSTALL_BIN_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_INCLUDE_DIR)
+    MakeRuleCmd.make_install_directory(out, INSTALL_LIB_DIR)
     for c in get_components():
         c.mk_install(out)
-    out.write('\t@cp z3*.py %s\n' % PYTHON_PACKAGE_DIR)
-    if sys.version >= "3":
-        out.write('\t@cp %s*.pyc %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@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, 'lib'), 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)
-    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@echo Z3 was successfully uninstalled.\n')
     out.write('\n')
 
@@ -2060,7 +2301,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():
@@ -2566,7 +2809,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:
@@ -2582,6 +2824,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):
@@ -3175,7 +3420,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():
@@ -3183,8 +3428,183 @@ 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):
+    """
+        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_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(src_pattern, str)
+        assert not ' ' in src_pattern
+        assert isinstance(dest, str)
+        assert not ' ' in dest
+        assert not os.path.isabs(src_pattern)
+        assert not os.path.isabs(dest)
+        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):
+        assert len(pattern) > 0
+        assert isinstance(pattern, str)
+        assert not ' ' in pattern
+        assert not os.path.isabs(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):
+        assert len(dir) > 0
+        assert isinstance(dir, str)
+        assert not ' ' in dir
+        assert not os.path.isabs(dir)
+        cls.write_cmd(out, "mkdir -p {install_root}{dir}".format(
+            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)
+        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 cls._is_path_prefix_of(temp_path, targetAsAbs):
+            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 {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
+    # ``$(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))
+
+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
+
+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

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

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")

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); }
 
 

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_string(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));
@@ -407,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_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(), get_sutil().is_seq(s)?"Seq":"Re");
+    }
     return format_ns::mk_string(get_manager(), s->get_name().str().c_str()); 
 }
 
@@ -578,6 +600,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_string(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);
         }

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; }

src/ast/rewriter/seq_rewriter.cpp

@@ -0,0 +1,341 @@
+/*++
+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"
+#include"ast_pp.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_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_LOOP:
+    case OP_RE_EMPTY_SET:
+    case OP_RE_FULL_SET:
+    case OP_RE_EMPTY_SEQ:
+    case OP_RE_OF_PRED:
+        return BR_FAILED;
+
+    // string specific operators.
+    case OP_STRING_CONST:
+        return BR_FAILED;
+    case OP_SEQ_CONCAT: 
+        SASSERT(num_args == 2);
+        return mk_seq_concat(args[0], args[1], result);
+    case OP_SEQ_LENGTH:
+        SASSERT(num_args == 1);
+        return mk_str_length(args[0], result);
+    case OP_SEQ_EXTRACT:
+        SASSERT(num_args == 3);
+        return mk_str_substr(args[0], args[1], args[2], result);
+    case OP_SEQ_CONTAINS: 
+        SASSERT(num_args == 2);
+        return mk_str_strctn(args[0], args[1], result);
+    case OP_SEQ_AT:
+        SASSERT(num_args == 2);
+        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_SEQ_PREFIX: 
+        SASSERT(num_args == 2);
+        return mk_seq_prefix(args[0], args[1], result);
+    case OP_SEQ_SUFFIX: 
+        SASSERT(num_args == 2);
+        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_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;
+}
+
+/*
+   string + string = string
+   a + (b + c) = (a + b) + c
+   a + "" = a
+   "" + a = a
+   (a + string) + string = a + string
+*/
+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_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;
+    }
+    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 (m_util.str.is_empty(a)) {
+        result = b;
+        return BR_DONE;
+    }
+    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_string(d, s1) && isc2) {
+        result = m_util.str.mk_concat(c, 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;
+    m_es.reset();
+    m_util.str.get_concat(a, m_es);
+    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)) {
+            len += b.length();
+        }
+        else {
+            m_es[j] = m_es[i];
+            ++j;
+        }
+    }
+    if (j == 0) {
+        result = m_autil.mk_numeral(rational(len, rational::ui64()), 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, rational::ui64()), 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;
+    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();
+        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) {
+    std::string c, 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_at(expr* a, expr* b, expr_ref& result) {
+    std::string c;
+    rational r;
+    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];
+            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* c, expr_ref& result) {
+    std::string s1, s2;
+    rational r;
+    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) {
+            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_autil.is_numeral(c, r) && r.is_neg()) {
+        result = m_autil.mk_numeral(rational(-1), true);
+        return BR_DONE;
+    }
+    
+    if (m_util.str.is_empty(b)) {
+        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_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) {
+                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_seq_prefix(expr* a, expr* b, expr_ref& result) {
+    std::string s1, 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) {
+            prefix = s1[i] == s2[i];
+        }
+        result = m().mk_bool_val(prefix);
+        return BR_DONE;
+    }
+    if (m_util.str.is_empty(a)) {
+        result = m().mk_true();
+        return BR_DONE;
+    }
+    return BR_FAILED;
+}
+
+br_status seq_rewriter::mk_seq_suffix(expr* a, expr* b, expr_ref& result) {
+    std::string s1, 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];
+        }
+        result = m().mk_bool_val(suffix);
+        return BR_DONE;
+    }
+    if (m_util.str.is_empty(a)) {
+        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)) {
+        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) {
+    std::string 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;
+            return BR_FAILED;            
+        }
+        rational r(s.c_str());
+        result = m_autil.mk_numeral(r, true);
+        return BR_DONE;
+    }
+    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;
+}

src/ast/rewriter/seq_rewriter.h

@@ -0,0 +1,70 @@
+/*++
+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"arith_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;
+    arith_util     m_autil;
+    ptr_vector<expr> m_es;
+
+    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);
+    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_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);
+    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), m_autil(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

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),

src/ast/seq_decl_plugin.cpp

@@ -19,13 +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) {}
+seq_decl_plugin::seq_decl_plugin(): m_init(false), 
+                                    m_stringc_sym("String"),
+                                    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) {
@@ -35,33 +41,70 @@ 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;
     }
 }
 
+/*
+  \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;
+    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 << "' ";
+        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);
+    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) {
     ptr_vector<sort> binding;
     ast_manager& m = *m_manager;
@@ -118,54 +161,78 @@ 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);
     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* 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 };
+    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* seqAreA[2] = { seqA, reA };
+    sort* reAreA[2] = { reA, reA };
+    sort* AA[2] = { A, A };
+    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-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_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_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]    = 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-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_LOOP]       = alloc(psig, m, "re-loop",    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);
-    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_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_SEQ_IN_RE]         = alloc(psig, m, "seq.in.re", 1, 2, seqAreA, boolT);
+    m_sigs[OP_STRING_CONST]      = 0;
+    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_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_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->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);
 }
 
 sort * seq_decl_plugin::mk_sort(decl_kind k, unsigned num_parameters, parameter const * parameters) {
@@ -179,6 +246,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) {
@@ -188,12 +258,31 @@ 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;
+    case _CHAR_SORT:
+        return m_char;
     default:
         UNREACHABLE();
         return 0;
     }
 }
 
+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();
@@ -202,36 +291,16 @@ 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:
-    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_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_DIFFERENCE:
-    case OP_RE_COMPLEMENT:
     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:
@@ -239,7 +308,80 @@ 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_SEQ_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[(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);
+        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_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_STRIDOF:
+    case OP_STRING_STRREPL:
+    case OP_STRING_ITOS:
+    case OP_STRING_STOI:
+    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 +391,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 +401,29 @@ 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;
+    return is_app_of(e, m_family_id, OP_STRING_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);
 }

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_
@@ -24,25 +26,23 @@ Revision History:
 
 enum seq_sort_kind {
     SEQ_SORT,
-    RE_SORT
+    RE_SORT,
+    _STRING_SORT,  // internal only
+    _CHAR_SORT     // internal only
 };
 
 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,
+    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,16 +51,30 @@ 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,
     OP_RE_EMPTY_SEQ,
-    OP_RE_OF_SEQ,
     OP_RE_OF_PRED,
-    OP_RE_MEMBER,
-    
+
+
+    // string specific operators.
+    OP_STRING_CONST,
+    OP_STRING_STRIDOF, // TBD generalize
+    OP_STRING_STRREPL, // TBD generalize
+    OP_STRING_ITOS, 
+    OP_STRING_STOI, 
+    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
 };
 
@@ -83,24 +97,34 @@ 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;
+    sort*            m_char;
 
     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);
 
     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);
+
 public:
     seq_decl_plugin();
 
     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);
@@ -116,6 +140,118 @@ 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);  
+};
+
+class seq_util {
+    ast_manager& m;
+    seq_decl_plugin& seq;
+    family_id m_fid;
+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); }
+    bool is_re(sort* s) const { return is_sort_of(s, m_fid, RE_SORT); }
+
+    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_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_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_string(expr const * n) const { return is_app_of(n, m_fid, OP_STRING_CONST); }
+        
+        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_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_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_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_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_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_re);        
+
+        void get_concat(expr* e, ptr_vector<expr>& es) const;
+    };
+
+    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_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); }
+        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_re);
+        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")))),
+        m_fid(seq.get_family_id()),
+        str(*this),
+        re(*this) {        
+    }
+
+    ~seq_util() {}
+
+    family_id get_family_id() const { return m_fid; }
     
 };
 

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

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().str.mk_string(m_scanner.get_string()));
+            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;
         }

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;
                 }

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.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.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.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) {
+            symbol sym;
+            if (u.str.is_string(n, sym)) {
+                m_strings.insert(sym);
+            }
+        }
+    };
+
     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()));
+        }
+
     };
 
 };