diff --git a/examples/python/visitor.py b/examples/python/visitor.py new file mode 100644 index 000000000..9255c6a80 --- /dev/null +++ b/examples/python/visitor.py @@ -0,0 +1,29 @@ +# Copyright (c) Microsoft Corporation 2015 + +from z3 import * + +def visitor(e, seen): + if e in seen: + return + seen[e] = True + yield e + if is_app(e): + for ch in e.children(): + for e in visitor(ch, seen): + yield e + return + if is_quantifier(e): + for e in visitor(e.body(), seen): + yield e + return + +x, y = Ints('x y') +fml = x + x + y > 2 +seen = {} +for e in visitor(fml, seen): + if is_const(e) and e.decl().kind() == Z3_OP_UNINTERPRETED: + print "Variable", e + else: + print e + + diff --git a/scripts/mk_project.py b/scripts/mk_project.py index 439843e08..a9aaa9791 100644 --- a/scripts/mk_project.py +++ b/scripts/mk_project.py @@ -91,6 +91,7 @@ def init_project_def(): add_ml_lib('ml', ['api_dll'], 'api/ml', lib_name='libz3ml') add_hlib('cpp', 'api/c++', includes2install=['z3++.h']) set_z3py_dir('api/python') + add_python_install() # Examples add_cpp_example('cpp_example', 'c++') add_cpp_example('z3_tptp', 'tptp') diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 83669472d..7e96f3b52 100644 --- a/scripts/mk_util.py +++ b/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 , --prefix= installation prefix (default: %s)." % PREFIX) else: print(" --parallel=num use cl option /MP with 'num' parallel processes") + print(" --pypkgdir= Force a particular Python package directory (default %s)" % PYTHON_PACKAGE_DIR) print(" -b , --build= 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 diff --git a/src/api/dotnet/Microsoft.Z3.Sharp.pc.in b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in new file mode 100644 index 000000000..8ca4e788b --- /dev/null +++ b/src/api/dotnet/Microsoft.Z3.Sharp.pc.in @@ -0,0 +1,7 @@ +prefix=@PREFIX@ +assemblies_dir=${prefix}/lib/mono/@GAC_PKG_NAME@ + +Name: @GAC_PKG_NAME@ +Description: .NET bindings for The Microsoft Z3 SMT solver +Version: @VERSION@ +Libs: -r:${assemblies_dir}/Microsoft.Z3.dll diff --git a/src/api/dotnet/Microsoft.Z3.mono.snk b/src/api/dotnet/Microsoft.Z3.mono.snk new file mode 100644 index 000000000..bfd0b3fce Binary files /dev/null and b/src/api/dotnet/Microsoft.Z3.mono.snk differ diff --git a/src/api/python/z3.py b/src/api/python/z3.py index f4e5d8941..27bfa6590 100644 --- a/src/api/python/z3.py +++ b/src/api/python/z3.py @@ -8189,7 +8189,7 @@ def is_fprm_value(a): class FPNumRef(FPRef): def isNaN(self): return self.decl().kind() == Z3_OP_FPA_NAN - + def isInf(self): return self.decl().kind() == Z3_OP_FPA_PLUS_INF or self.decl().kind() == Z3_OP_FPA_MINUS_INF @@ -8201,7 +8201,7 @@ class FPNumRef(FPRef): return (self.num_args() == 0 and (k == Z3_OP_FPA_MINUS_INF or k == Z3_OP_FPA_MINUS_ZERO)) or (self.sign() == True) """ - The sign of the numeral + The sign of the numeral. >>> x = FPNumRef(+1.0, FPSort(8, 24)) >>> x.sign() @@ -8215,30 +8215,32 @@ class FPNumRef(FPRef): if Z3_fpa_get_numeral_sign(self.ctx.ref(), self.as_ast(), byref(l)) == False: raise Z3Exception("error retrieving the sign of a numeral.") return l.value != 0 - + """ - The significand of the numeral + The significand of the numeral. >>> x = FPNumRef(2.5, FPSort(8, 24)) + >>> x.significand() 1.25 """ def significand(self): return Z3_fpa_get_numeral_significand_string(self.ctx.ref(), self.as_ast()) """ - The exponent of the numeral + The exponent of the numeral. >>> x = FPNumRef(2.5, FPSort(8, 24)) - >>> + >>> x.exponent() 1 """ def exponent(self): return Z3_fpa_get_numeral_exponent_string(self.ctx.ref(), self.as_ast()) """ - The exponent of the numeral as a long + The exponent of the numeral as a long. >>> x = FPNumRef(2.5, FPSort(8, 24)) + >>> x.exponent_as_long() 1 """ def exponent_as_long(self): @@ -8246,11 +8248,12 @@ class FPNumRef(FPRef): if not Z3_fpa_get_numeral_exponent_int64(self.ctx.ref(), self.as_ast(), ptr): raise Z3Exception("error retrieving the exponent of a numeral.") return ptr[0] - + """ - The string representation of the numeral + The string representation of the numeral. >>> x = FPNumRef(20, FPSort(8, 24)) + >>> x.as_string() 1.25*(2**4) """ def as_string(self): @@ -8378,7 +8381,7 @@ def FPVal(sig, exp=None, fps=None, ctx=None): val = val + 'p' val = val + _to_int_str(exp) return FPNumRef(Z3_mk_numeral(ctx.ref(), val, fps.ast), ctx) - + def FP(name, fpsort, ctx=None): """Return a floating-point constant named `name`. `fpsort` is the floating-point sort. @@ -8640,47 +8643,47 @@ def fpIsNaN(a): return FPRef(Z3_mk_fpa_is_nan(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsInfinite(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isInfinite expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_infinite(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsZero(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isZero expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_zero(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsNormal(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isNormal expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_normal(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsSubnormal(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isSubnormal expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_subnormal(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsNegative(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isNegative expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_negative(a.ctx_ref(), a.as_ast()), a.ctx) def fpIsPositive(a): - """Create a Z3 floating-point isNaN expression. + """Create a Z3 floating-point isPositive expression. """ if __debug__: _z3_assert(is_fp(a), "Argument must be Z3 floating-point expressions") return FPRef(Z3_mk_fpa_is_positive(a.ctx_ref(), a.as_ast()), a.ctx) - + def _check_fp_args(a, b): if __debug__: _z3_assert(is_fp(a) or is_fp(b), "At least one of the arguments must be a Z3 floating-point expression") diff --git a/src/ast/ast.h b/src/ast/ast.h index 8547675a8..e4e1b4d58 100644 --- a/src/ast/ast.h +++ b/src/ast/ast.h @@ -2013,6 +2013,7 @@ public: app * mk_distinct_expanded(unsigned num_args, expr * const * args); app * mk_true() { return m_true; } app * mk_false() { return m_false; } + app * mk_bool_val(bool b) { return b?m_true:m_false; } app * mk_interp(expr * arg) { return mk_app(m_basic_family_id, OP_INTERP, arg); } diff --git a/src/ast/ast_smt2_pp.cpp b/src/ast/ast_smt2_pp.cpp index c74b4f185..523d98a93 100644 --- a/src/ast/ast_smt2_pp.cpp +++ b/src/ast/ast_smt2_pp.cpp @@ -363,6 +363,23 @@ format * smt2_pp_environment::pp_arith_literal(app * t, bool decimal, unsigned d } } +format * smt2_pp_environment::pp_string_literal(app * t) { + std::string s; + VERIFY (get_sutil().str.is_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 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); } diff --git a/src/ast/ast_smt2_pp.h b/src/ast/ast_smt2_pp.h index 04c3b35d4..45d18ceff 100644 --- a/src/ast/ast_smt2_pp.h +++ b/src/ast/ast_smt2_pp.h @@ -29,6 +29,7 @@ Revision History: #include"array_decl_plugin.h" #include"fpa_decl_plugin.h" #include"dl_decl_plugin.h" +#include"seq_decl_plugin.h" #include"smt2_util.h" class smt2_pp_environment { @@ -47,6 +48,7 @@ public: virtual bv_util & get_bvutil() = 0; virtual array_util & get_arutil() = 0; virtual fpa_util & get_futil() = 0; + virtual seq_util & get_sutil() = 0; virtual datalog::dl_decl_util& get_dlutil() = 0; virtual bool uses(symbol const & s) const = 0; virtual format_ns::format * pp_fdecl(func_decl * f, unsigned & len); @@ -54,6 +56,7 @@ public: virtual format_ns::format * pp_arith_literal(app * t, bool decimal, unsigned prec); virtual format_ns::format * pp_float_literal(app * t, bool use_bv_lits, bool use_float_real_lits); virtual format_ns::format * pp_datalog_literal(app * t); + virtual format_ns::format * pp_string_literal(app * t); virtual format_ns::format * pp_sort(sort * s); virtual format_ns::format * pp_fdecl_ref(func_decl * f); format_ns::format * pp_fdecl_name(symbol const & fname, unsigned & len) const; @@ -70,12 +73,14 @@ class smt2_pp_environment_dbg : public smt2_pp_environment { bv_util m_bvutil; array_util m_arutil; fpa_util m_futil; + seq_util m_sutil; datalog::dl_decl_util m_dlutil; public: - smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_dlutil(m) {} + smt2_pp_environment_dbg(ast_manager & m):m_manager(m), m_autil(m), m_bvutil(m), m_arutil(m), m_futil(m), m_sutil(m), m_dlutil(m) {} virtual ast_manager & get_manager() const { return m_manager; } virtual arith_util & get_autil() { return m_autil; } virtual bv_util & get_bvutil() { return m_bvutil; } + virtual seq_util & get_sutil() { return m_sutil; } virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } diff --git a/src/ast/rewriter/seq_rewriter.cpp b/src/ast/rewriter/seq_rewriter.cpp new file mode 100644 index 000000000..96590a40a --- /dev/null +++ b/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; +} diff --git a/src/ast/rewriter/seq_rewriter.h b/src/ast/rewriter/seq_rewriter.h new file mode 100644 index 000000000..4674a7535 --- /dev/null +++ b/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 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 diff --git a/src/ast/rewriter/th_rewriter.cpp b/src/ast/rewriter/th_rewriter.cpp index b7197d239..a8aea47b6 100644 --- a/src/ast/rewriter/th_rewriter.cpp +++ b/src/ast/rewriter/th_rewriter.cpp @@ -26,6 +26,7 @@ Notes: #include"fpa_rewriter.h" #include"dl_rewriter.h" #include"pb_rewriter.h" +#include"seq_rewriter.h" #include"rewriter_def.h" #include"expr_substitution.h" #include"ast_smt2_pp.h" @@ -43,6 +44,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { fpa_rewriter m_f_rw; dl_rewriter m_dl_rw; pb_rewriter m_pb_rw; + seq_rewriter m_seq_rw; arith_util m_a_util; bv_util m_bv_util; unsigned long long m_max_memory; // in bytes @@ -76,6 +78,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_bv_rw.updt_params(p); m_ar_rw.updt_params(p); m_f_rw.updt_params(p); + m_seq_rw.updt_params(p); updt_local_params(p); } @@ -200,6 +203,8 @@ struct th_rewriter_cfg : public default_rewriter_cfg { return m_dl_rw.mk_app_core(f, num, args, result); if (fid == m_pb_rw.get_fid()) return m_pb_rw.mk_app_core(f, num, args, result); + if (fid == m_seq_rw.get_fid()) + return m_seq_rw.mk_app_core(f, num, args, result); return BR_FAILED; } @@ -650,6 +655,7 @@ struct th_rewriter_cfg : public default_rewriter_cfg { m_f_rw(m, p), m_dl_rw(m), m_pb_rw(m), + m_seq_rw(m), m_a_util(m), m_bv_util(m), m_used_dependencies(m), diff --git a/src/ast/seq_decl_plugin.cpp b/src/ast/seq_decl_plugin.cpp index 330227193..b47c4209d 100644 --- a/src/ast/seq_decl_plugin.cpp +++ b/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 -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& 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 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 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, ¶mA); sort* reA = m.mk_sort(m_family_id, RE_SORT, 1, ¶mA); - 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, ¶mS); 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, ¶m)); + 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 & 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 & 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, ¶m)); + 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& es) const { + expr* e1, *e2; + while (is_concat(e, e1, e2)) { + get_concat(e1, es); + e = e2; + } + es.push_back(e); } diff --git a/src/ast/seq_decl_plugin.h b/src/ast/seq_decl_plugin.h index c71c7317e..c61e3cc43 100644 --- a/src/ast/seq_decl_plugin.h +++ b/src/ast/seq_decl_plugin.h @@ -11,10 +11,12 @@ Abstract: Author: - Nikolaj Bjorner (nbjorner) 2011-14-11 + Nikolaj Bjorner (nbjorner) 2011-11-14 Revision History: + Updated to string sequences 2015-12-5 + --*/ #ifndef SEQ_DECL_PLUGIN_H_ #define SEQ_DECL_PLUGIN_H_ @@ -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 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& binding, sort* s, sort* sP); sort* apply_binding(ptr_vector 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& 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(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; } }; diff --git a/src/cmd_context/cmd_context.cpp b/src/cmd_context/cmd_context.cpp index 02b2b6525..1b5d9d470 100644 --- a/src/cmd_context/cmd_context.cpp +++ b/src/cmd_context/cmd_context.cpp @@ -245,6 +245,7 @@ protected: bv_util m_bvutil; array_util m_arutil; fpa_util m_futil; + seq_util m_sutil; datalog::dl_decl_util m_dlutil; format_ns::format * pp_fdecl_name(symbol const & s, func_decls const & fs, func_decl * f, unsigned & len) { @@ -265,13 +266,14 @@ protected: } public: - pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_dlutil(o.m()) {} + pp_env(cmd_context & o):m_owner(o), m_autil(o.m()), m_bvutil(o.m()), m_arutil(o.m()), m_futil(o.m()), m_sutil(o.m()), m_dlutil(o.m()) {} virtual ~pp_env() {} virtual ast_manager & get_manager() const { return m_owner.m(); } virtual arith_util & get_autil() { return m_autil; } virtual bv_util & get_bvutil() { return m_bvutil; } virtual array_util & get_arutil() { return m_arutil; } virtual fpa_util & get_futil() { return m_futil; } + virtual seq_util & get_sutil() { return m_sutil; } virtual datalog::dl_decl_util& get_dlutil() { return m_dlutil; } virtual bool uses(symbol const & s) const { return diff --git a/src/parsers/smt2/smt2parser.cpp b/src/parsers/smt2/smt2parser.cpp index b95be8ee5..404c04d3a 100644 --- a/src/parsers/smt2/smt2parser.cpp +++ b/src/parsers/smt2/smt2parser.cpp @@ -22,6 +22,7 @@ Revision History: #include"datatype_decl_plugin.h" #include"bv_decl_plugin.h" #include"arith_decl_plugin.h" +#include"seq_decl_plugin.h" #include"ast_pp.h" #include"well_sorted.h" #include"pattern_validation.h" @@ -65,6 +66,7 @@ namespace smt2 { scoped_ptr m_bv_util; scoped_ptr m_arith_util; + scoped_ptr m_seq_util; scoped_ptr m_pattern_validator; scoped_ptr 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; } diff --git a/src/parsers/smt2/smt2scanner.cpp b/src/parsers/smt2/smt2scanner.cpp index bc62c2646..ed16003c2 100644 --- a/src/parsers/smt2/smt2scanner.cpp +++ b/src/parsers/smt2/smt2scanner.cpp @@ -171,10 +171,7 @@ namespace smt2 { throw scanner_exception("unexpected end of string", m_line, m_spos); if (c == '\"') { next(); - if (curr() == '\"') { - m_string.push_back(c); - } - else { + if (curr() != '\"') { m_string.push_back(0); return STRING_TOKEN; } diff --git a/src/smt/theory_seq_empty.h b/src/smt/theory_seq_empty.h index 60350017f..e8e619bf8 100644 --- a/src/smt/theory_seq_empty.h +++ b/src/smt/theory_seq_empty.h @@ -20,8 +20,64 @@ Revision History: #define THEORY_SEQ_EMPTY_H_ #include "smt_theory.h" +#include "seq_decl_plugin.h" namespace smt { + class seq_factory : public value_factory { + typedef hashtable symbol_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())); + } + }; };