diff --git a/CMakeLists.txt b/CMakeLists.txt index 3cc29780d..d33f352e1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -321,9 +321,10 @@ message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLA ################################################################################ # Z3 installation locations ################################################################################ -set (Z3_INSTALL_LIB_DIR "lib") -set (Z3_INSTALL_BIN_DIR "bin") -set (Z3_INSTALL_INCLUDE_DIR "include") +include(GNUInstallDirs) +message(STATUS "CMAKE_INSTALL_LIBDIR: \"${CMAKE_INSTALL_LIBDIR}\"") +message(STATUS "CMAKE_INSTALL_BINDIR: \"${CMAKE_INSTALL_BINDIR}\"") +message(STATUS "CMAKE_INSTALL_INCLUDEDIR: \"${CMAKE_INSTALL_INCLUDEDIR}\"") ################################################################################ # CMake build file locations @@ -334,6 +335,17 @@ set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") +################################################################################ +# Extra dependencies for build rules that use the Python infrastructure to +# generate files used for Z3's build. Changes to these files will trigger +# a rebuild of all the generated files. +################################################################################ +# Note: ``update_api.py`` is deliberately not here because it not used +# to generate every generated file. The targets that need it list it explicitly. +set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES + "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" +) + ################################################################################ # Z3 components, library and executables ################################################################################ diff --git a/README-CMake.md b/README-CMake.md index 28f49cf27..cdedb8374 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -261,7 +261,10 @@ when invoking CMake and instead set the build type within Visual Studio itself. The following useful options can be passed to CMake whilst configuring. * ``CMAKE_BUILD_TYPE`` - STRING. The build type to use. Only relevant for single configuration generators (e.g. "Unix Makefile" and "Ninja"). -* ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``) +* ``CMAKE_INSTALL_BINDIR`` - STRING. The path to install z3 binaries (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``bin``. +* ``CMAKE_INSTALL_INCLUDEDIR`` - STRING. The path to install z3 include files (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``include``. +* ``CMAKE_INSTALL_LIBDIR`` - STRING. The path to install z3 libraries (relative to ``CMAKE_INSTALL_PREFIX``), e.g. ``lib``. +* ``CMAKE_INSTALL_PREFIX`` - STRING. The install prefix to use (e.g. ``/usr/local/``). * ``ENABLE_TRACING`` - BOOL. If set to ``TRUE`` enable tracing, if set to ``FALSE`` disable tracing. * ``BUILD_LIBZ3_SHARED`` - BOOL. If set to ``TRUE`` build libz3 as a shared library otherwise build as a static library. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. @@ -322,8 +325,9 @@ in order to be sure that the copied CMake files are not out of date. ### Install/Uninstall -Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to set the install -prefix. +Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to +set the install prefix. If you also need need to control which directories are +used for install set the documented ``CMAKE_INSTALL_*`` options. To install run diff --git a/README.md b/README.md index 6052e2f91..a3ba1ff24 100644 --- a/README.md +++ b/README.md @@ -3,6 +3,8 @@ Z3 is a theorem prover from Microsoft Research. It is licensed under the [MIT license](LICENSE.txt). +If you are not familiar with Z3, you can start [here](https://github.com/Z3Prover/z3/wiki#background). + Z3 can be built using [Visual Studio][1] or a [Makefile][2]. It provides [bindings for several programming languages][3]. diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/contrib/cmake/cmake/z3_add_component.cmake index eebc0c8d9..b90aa2fe7 100644 --- a/contrib/cmake/cmake/z3_add_component.cmake +++ b/contrib/cmake/cmake/z3_add_component.cmake @@ -104,7 +104,8 @@ macro(z3_add_component component_name) add_custom_command(OUTPUT "${_output_file}" COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${_full_pyg_file_path}" "${CMAKE_CURRENT_BINARY_DIR}" MAIN_DEPENDENCY "${_full_pyg_file_path}" - DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\"" WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -203,7 +204,7 @@ macro(z3_add_install_tactic_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -235,7 +236,7 @@ macro(z3_add_memory_initializer_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -267,7 +268,7 @@ macro(z3_add_gparams_register_modules_rule) "${CMAKE_CURRENT_BINARY_DIR}" ${_search_paths} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 6708f505e..00dd01627 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -165,9 +165,9 @@ foreach (header ${libz3_public_headers}) endforeach() install(TARGETS libz3 - LIBRARY DESTINATION "${Z3_INSTALL_LIB_DIR}" - ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}" - PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}" + LIBRARY DESTINATION "${CMAKE_INSTALL_LIBDIR}" + ARCHIVE DESTINATION "${CMAKE_INSTALL_LIBDIR}" + PUBLIC_HEADER DESTINATION "${CMAKE_INSTALL_INCLUDEDIR}" ) if (MSVC) @@ -186,7 +186,7 @@ if (MSVC) ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} COMMENT "Generating \"${dll_module_exports_file}\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt index 0fd012b87..8e796168f 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -24,8 +24,10 @@ add_custom_command(OUTPUT ${generated_files} "--api_output_dir" "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating ${generated_files}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 2279be716..6e4096057 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -38,6 +38,8 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" DEPENDS ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} + # FIXME: When update_api.py no longer uses ``mk_util`` drop this dependency "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} @@ -54,7 +56,7 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py" DEPENDS ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3consts.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) diff --git a/contrib/cmake/src/ast/pattern/CMakeLists.txt b/contrib/cmake/src/ast/pattern/CMakeLists.txt index 8cff3e739..59e0545a1 100644 --- a/contrib/cmake/src/ast/pattern/CMakeLists.txt +++ b/contrib/cmake/src/ast/pattern/CMakeLists.txt @@ -13,7 +13,7 @@ add_custom_command(OUTPUT "database.h" "${CMAKE_CURRENT_BINARY_DIR}/database.h" MAIN_DEPENDENCY "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating \"database.h\"" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/contrib/cmake/src/shell/CMakeLists.txt index 65b97aaaf..c5d5ca880 100644 --- a/contrib/cmake/src/shell/CMakeLists.txt +++ b/contrib/cmake/src/shell/CMakeLists.txt @@ -43,5 +43,5 @@ target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS}) z3_add_component_dependencies_to_target(shell ${shell_expanded_deps}) z3_append_linker_flag_list_to_target(shell ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) install(TARGETS shell - RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}" + RUNTIME DESTINATION "${CMAKE_INSTALL_BINDIR}" ) diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py index 543c56e0e..2c017bd2c 100755 --- a/scripts/mk_consts_files.py +++ b/scripts/mk_consts_files.py @@ -4,44 +4,38 @@ Reads a list of Z3 API header files and generate the constant declarations need by one or more Z3 language bindings """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(output_dir): - if not os.path.isdir(output_dir): - logging.error('"{}" is not an existing directory'.format(output_dir)) - return 1 - return 0 def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("api_files", nargs="+") - parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("api_files", nargs="+") + parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + pargs = parser.parse_args(args) - for api_file in pargs.api_files: - if not os.path.exists(api_file): - logging.error('"{}" does not exist'.format(api_file)) - return 1 + if not mk_genfile_common.check_files_exist(pargs.api_files): + logging.error('One or more API files do not exist') + return 1 - count = 0 + count = 0 - if pargs.z3py_output_dir: - if check_dir(pargs.z3py_output_dir) != 0: - return 1 - mk_util.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) - count += 1 + if pargs.z3py_output_dir: + if not mk_genfile_common.check_dir_exists(pargs.z3py_output_dir): + return 1 + output = mk_genfile_common.mk_z3consts_py_internal(pargs.api_files, pargs.z3py_output_dir) + logging.info('Generated "{}"'.format(output)) + count += 1 - if count == 0: - logging.info('No files generated. You need to specific an output directory' - ' for the relevant langauge bindings') - # TODO: Add support for other bindings - return 0 + if count == 0: + logging.info('No files generated. You need to specific an output directory' + ' for the relevant langauge bindings') + # TODO: Add support for other bindings + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) - + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py index 2b9b5a071..07418a975 100755 --- a/scripts/mk_def_file.py +++ b/scripts/mk_def_file.py @@ -6,31 +6,31 @@ exported symbols of a dll. This file can be passed to the ``/DEF`` to the linker used by MSVC. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("output_file", help="output def file path") - parser.add_argument("dllname", help="dllname to use in def file") - parser.add_argument("api_files", nargs="+") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("output_file", help="output def file path") + parser.add_argument("dllname", help="dllname to use in def file") + parser.add_argument("api_files", nargs="+") + pargs = parser.parse_args(args) - for api_file in pargs.api_files: - if not os.path.exists(api_file): - logging.error('"{}" does not exist'.format(api_file)) - return 1 + if not mk_genfile_common.check_files_exist(pargs.api_files): + logging.error('One or more api files do not exist') + return 1 - mk_util.mk_def_file_internal( - pargs.output_file, - pargs.dllname, - pargs.api_files) - return 0 + mk_genfile_common.mk_def_file_internal( + pargs.output_file, + pargs.dllname, + pargs.api_files) + logging.info('Generated "{}"'.format(pargs.output_file)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py new file mode 100644 index 000000000..790ce7205 --- /dev/null +++ b/scripts/mk_genfile_common.py @@ -0,0 +1,519 @@ +# This file contains code that is common to +# both the Python build system and the CMake +# build system. +# +# The code here generally is involved in +# generating files needed by Z3 at build time. +# +# You should **not** import ``mk_util`` here +# to avoid having this code depend on the +# of the Python build system. +import os +import logging +import re +import sys + +# Logger for this module +_logger = logging.getLogger(__name__) + + +############################################################################### +# Utility functions +############################################################################### +def check_dir_exists(output_dir): + """ + Returns ``True`` if ``output_dir`` exists, otherwise + returns ``False``. + """ + if not os.path.isdir(output_dir): + _logger.error('"{}" is not an existing directory'.format(output_dir)) + return False + return True + +def check_files_exist(files): + assert isinstance(files, list) + for f in files: + if not os.path.exists(f): + _logger.error('"{}" does not exist'.format(f)) + return False + return True + +############################################################################### +# Functions for generating constant declarations for language bindings +############################################################################### + +def mk_z3consts_py_internal(api_files, output_dir): + """ + Generate ``z3consts.py`` from the list of API header files + in ``api_files`` and write the output file into + the ``output_dir`` directory + + Returns the path to the generated file. + """ + assert os.path.isdir(output_dir) + assert isinstance(api_files, list) + + blank_pat = re.compile("^ *\r?$") + comment_pat = re.compile("^ *//.*$") + typedef_pat = re.compile("typedef enum *") + typedef2_pat = re.compile("typedef enum { *") + openbrace_pat = re.compile("{ *") + closebrace_pat = re.compile("}.*;") + + z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') + z3consts_output_path = z3consts.name + z3consts.write('# Automatically generated file\n\n') + for api_file in api_files: + api = open(api_file, 'r') + + SEARCHING = 0 + FOUND_ENUM = 1 + IN_ENUM = 2 + + mode = SEARCHING + decls = {} + idx = 0 + + linenum = 1 + for line in api: + m1 = blank_pat.match(line) + m2 = comment_pat.match(line) + if m1 or m2: + # skip blank lines and comments + linenum = linenum + 1 + elif mode == SEARCHING: + m = typedef_pat.match(line) + if m: + mode = FOUND_ENUM + m = typedef2_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + elif mode == FOUND_ENUM: + m = openbrace_pat.match(line) + if m: + mode = IN_ENUM + decls = {} + idx = 0 + else: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + assert mode == IN_ENUM + words = re.split('[^\-a-zA-Z0-9_]+', line) + m = closebrace_pat.match(line) + if m: + name = words[1] + z3consts.write('# enum %s\n' % name) + for k in decls: + i = decls[k] + z3consts.write('%s = %s\n' % (k, i)) + z3consts.write('\n') + mode = SEARCHING + elif len(words) <= 2: + assert False, "Invalid %s, line: %s" % (api_file, linenum) + else: + if words[2] != '': + if len(words[2]) > 1 and words[2][1] == 'x': + idx = int(words[2], 16) + else: + idx = int(words[2]) + decls[words[1]] = idx + idx = idx + 1 + linenum = linenum + 1 + api.close() + z3consts.close() + return z3consts_output_path + +############################################################################### +# Functions for generating a "module definition file" for MSVC +############################################################################### + +def mk_def_file_internal(defname, dll_name, export_header_files): + """ + Writes to a module definition file to a file named ``defname``. + + ``dll_name`` is the name of the dll (without the ``.dll`` suffix). + ``export_header_file`` is a list of header files to scan for symbols + to include in the module definition file. + """ + assert isinstance(export_header_files, list) + pat1 = re.compile(".*Z3_API.*") + fout = open(defname, 'w') + fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name) + num = 1 + for export_header_file in export_header_files: + api = open(export_header_file, 'r') + for line in api: + m = pat1.match(line) + if m: + words = re.split('\W+', line) + i = 0 + for w in words: + if w == 'Z3_API': + f = words[i+1] + fout.write('\t%s @%s\n' % (f, num)) + i = i + 1 + num = num + 1 + api.close() + fout.close() + +############################################################################### +# Functions for generating ``gparams_register_modules.cpp`` +############################################################################### +def mk_gparams_register_modules_internal(component_src_dirs, path): + """ + Generate a ``gparams_register_modules.cpp`` file in the directory ``path``. + Returns the path to the generated file. + + This file implements the procedure + + ``` + void gparams_register_modules() + ``` + + This procedure is invoked by gparams::init() + """ + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + cmds = [] + mod_cmds = [] + mod_descrs = [] + fullname = os.path.join(path, 'gparams_register_modules.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include"gparams.h"\n') + reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') + reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') + reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') + for component_src_dir in component_src_dirs: + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + m = reg_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + cmds.append((m.group(1))) + m = reg_mod_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + mod_cmds.append((m.group(1), m.group(2))) + m = reg_mod_descr_pat.match(line) + if m: + mod_descrs.append((m.group(1), m.group(2))) + fin.close() + fout.write('void gparams_register_modules() {\n') + for code in cmds: + fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) + for (mod, code) in mod_cmds: + fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod)) + for (mod, descr) in mod_descrs: + fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) + fout.write('}\n') + fout.close() + return fullname + +############################################################################### +# Functions/data structures for generating ``install_tactics.cpp`` +############################################################################### + +def mk_install_tactic_cpp_internal(component_src_dirs, path): + """ + Generate a ``install_tactics.cpp`` file in the directory ``path``. + Returns the path the generated file. + + This file implements the procedure + + ``` + void install_tactics(tactic_manager & ctx) + ``` + + It installs all tactics found in the given component directories + ``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands + in the ``.h`` and ``.hpp`` files of these components. + """ + ADD_TACTIC_DATA = [] + ADD_PROBE_DATA = [] + def ADD_TACTIC(name, descr, cmd): + ADD_TACTIC_DATA.append((name, descr, cmd)) + + def ADD_PROBE(name, descr, cmd): + ADD_PROBE_DATA.append((name, descr, cmd)) + + exec_globals = { + 'ADD_TACTIC': ADD_TACTIC, + 'ADD_PROBE': ADD_PROBE, + } + + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + fullname = os.path.join(path, 'install_tactic.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + fout.write('#include"tactic.h"\n') + fout.write('#include"tactic_cmds.h"\n') + fout.write('#include"cmd_context.h"\n') + tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') + probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') + for component_src_dir in component_src_dirs: + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + if tactic_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + try: + exec(line.strip('\n '), exec_globals) + except Exception as e: + _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( + fullname, line)) + raise e + if probe_pat.match(line): + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + try: + exec(line.strip('\n '), exec_globals) + except Exception as e: + _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( + fullname, line)) + raise e + fin.close() + # First pass will just generate the tactic factories + idx = 0 + for data in ADD_TACTIC_DATA: + fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) + idx = idx + 1 + fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') + fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') + fout.write('void install_tactics(tactic_manager & ctx) {\n') + idx = 0 + for data in ADD_TACTIC_DATA: + fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) + idx = idx + 1 + for data in ADD_PROBE_DATA: + fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) + fout.write('}\n') + fout.close() + return fullname + +############################################################################### +# Functions for generating ``mem_initializer.cpp`` +############################################################################### + +def mk_mem_initializer_cpp_internal(component_src_dirs, path): + """ + Generate a ``mem_initializer.cpp`` file in the directory ``path``. + Returns the path to the generated file. + + This file implements the procedures + + ``` + void mem_initialize() + void mem_finalize() + ``` + + These procedures are invoked by the Z3 memory_manager + """ + assert isinstance(component_src_dirs, list) + assert check_dir_exists(path) + initializer_cmds = [] + finalizer_cmds = [] + fullname = os.path.join(path, 'mem_initializer.cpp') + fout = open(fullname, 'w') + fout.write('// Automatically generated file.\n') + initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') + # ADD_INITIALIZER with priority + initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') + finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') + for component_src_dir in component_src_dirs: + h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) + for h_file in h_files: + added_include = False + fin = open(os.path.join(component_src_dir, h_file), 'r') + for line in fin: + m = initializer_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + initializer_cmds.append((m.group(1), 0)) + m = initializer_prio_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + initializer_cmds.append((m.group(1), int(m.group(2)))) + m = finalizer_pat.match(line) + if m: + if not added_include: + added_include = True + fout.write('#include"%s"\n' % h_file) + finalizer_cmds.append(m.group(1)) + fin.close() + initializer_cmds.sort(key=lambda tup: tup[1]) + fout.write('void mem_initialize() {\n') + for (cmd, prio) in initializer_cmds: + fout.write(cmd) + fout.write('\n') + fout.write('}\n') + fout.write('void mem_finalize() {\n') + for cmd in finalizer_cmds: + fout.write(cmd) + fout.write('\n') + fout.write('}\n') + fout.close() + return fullname + +############################################################################### +# Functions for generating ``database.h`` +############################################################################### + +def mk_pat_db_internal(inputFilePath, outputFilePath): + """ + Generate ``g_pattern_database[]`` declaration header file. + """ + with open(inputFilePath, 'r') as fin: + with open(outputFilePath, 'w') as fout: + fout.write('static char const g_pattern_database[] =\n') + for line in fin: + fout.write('"%s\\n"\n' % line.strip('\n')) + fout.write(';\n') + +############################################################################### +# Functions and data structures for generating ``*_params.hpp`` files from +# ``*.pyg`` files +############################################################################### + +UINT = 0 +BOOL = 1 +DOUBLE = 2 +STRING = 3 +SYMBOL = 4 +UINT_MAX = 4294967295 + +TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } +TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } +TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' } + +def pyg_default(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + return p[2] + +def pyg_default_as_c_literal(p): + if p[1] == BOOL: + if p[2]: + return "true" + else: + return "false" + elif p[1] == STRING: + return '"%s"' % p[2] + elif p[1] == SYMBOL: + return 'symbol("%s")' % p[2] + elif p[1] == UINT: + return '%su' % p[2] + else: + return p[2] + +def to_c_method(s): + return s.replace('.', '_') + + +def max_memory_param(): + return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') + +def max_steps_param(): + return ('max_steps', UINT, UINT_MAX, 'maximum number of steps') + +def mk_hpp_from_pyg(pyg_file, output_dir): + """ + Generates the corresponding header file for the input pyg file + at the path ``pyg_file``. The file is emitted into the directory + ``output_dir``. + + Returns the path to the generated file + """ + CURRENT_PYG_HPP_DEST_DIR = output_dir + # Note OUTPUT_HPP_FILE cannot be a string as we need a mutable variable + # for the nested function to modify + OUTPUT_HPP_FILE = [ ] + # The function below has been nested so that it can use closure to capture + # the above variables that aren't global but instead local to this + # function. This avoids use of global state which makes this function safer. + def def_module_params(module_name, export, params, class_name=None, description=None): + dirname = CURRENT_PYG_HPP_DEST_DIR + assert(os.path.exists(dirname)) + if class_name is None: + class_name = '%s_params' % module_name + hpp = os.path.join(dirname, '%s.hpp' % class_name) + out = open(hpp, 'w') + out.write('// Automatically generated file\n') + out.write('#ifndef __%s_HPP_\n' % class_name.upper()) + out.write('#define __%s_HPP_\n' % class_name.upper()) + out.write('#include"params.h"\n') + if export: + out.write('#include"gparams.h"\n') + out.write('struct %s {\n' % class_name) + out.write(' params_ref const & p;\n') + if export: + out.write(' params_ref g;\n') + out.write(' %s(params_ref const & _p = params_ref::get_empty()):\n' % class_name) + out.write(' p(_p)') + if export: + out.write(', g(gparams::get_module("%s"))' % module_name) + out.write(' {}\n') + out.write(' static void collect_param_descrs(param_descrs & d) {\n') + for param in params: + out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name)) + out.write(' }\n') + if export: + out.write(' /*\n') + out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name)) + if description is not None: + out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description)) + out.write(' */\n') + # Generated accessors + for param in params: + if export: + out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + else: + out.write(' %s %s() const { return p.%s("%s", %s); }\n' % + (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) + out.write('};\n') + out.write('#endif\n') + out.close() + OUTPUT_HPP_FILE.append(hpp) + + # Globals to use when executing the ``.pyg`` file. + pyg_globals = { + 'UINT' : UINT, + 'BOOL' : BOOL, + 'DOUBLE' : DOUBLE, + 'STRING' : STRING, + 'SYMBOL' : SYMBOL, + 'UINT_MAX' : UINT_MAX, + 'max_memory_param' : max_memory_param, + 'max_steps_param' : max_steps_param, + # Note that once this function is enterred that function + # executes with respect to the globals of this module and + # not the globals defined here + 'def_module_params' : def_module_params, + } + with open(pyg_file, 'r') as fh: + exec(fh.read() + "\n", pyg_globals, None) + assert len(OUTPUT_HPP_FILE) == 1 + return OUTPUT_HPP_FILE[0] diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py index 1c7e221ba..cf6e8da96 100755 --- a/scripts/mk_gparams_register_modules_cpp.py +++ b/scripts/mk_gparams_register_modules_cpp.py @@ -6,42 +6,34 @@ and generates a ``gparams_register_modules.cpp`` file in the destination directory that defines a function ``void gparams_register_modules()``. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("destination_dir", help="destination directory") - parser.add_argument("source_dirs", nargs="+", - help="One or more source directories to search") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("destination_dir", help="destination directory") + parser.add_argument("source_dirs", nargs="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_gparams_register_modules_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_gparams_register_modules_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py index f8323d731..21e66b3ab 100755 --- a/scripts/mk_install_tactic_cpp.py +++ b/scripts/mk_install_tactic_cpp.py @@ -6,42 +6,33 @@ and generates a ``install_tactic.cpp`` file in the destination directory that defines a function ``void install_tactics(tactic_manager& ctx)``. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("destination_dir", help="destination directory") - parser.add_argument("source_dirs", nargs="+", - help="One or more source directories to search") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("destination_dir", help="destination directory") + parser.add_argument("source_dirs", nargs="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_install_tactic_cpp_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_install_tactic_cpp_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) - + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py index c8b68049f..b56fcbced 100755 --- a/scripts/mk_mem_initializer_cpp.py +++ b/scripts/mk_mem_initializer_cpp.py @@ -7,42 +7,34 @@ emits and implementation of ``void mem_finalize()`` into ``mem_initializer.cpp`` in the destination directory. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys -def check_dir(path): - if not os.path.exists(path): - logging.error('"{}" does not exist'.format(path)) - return 1 - - if not os.path.isdir(path): - logging.error('"{}" is not a directory'.format(path)) - return 1 - - return 0 - - def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("destination_dir", help="destination directory") - parser.add_argument("source_dirs", nargs="+", - help="One or more source directories to search") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("destination_dir", help="destination directory") + parser.add_argument("source_dirs", nargs="+", + help="One or more source directories to search") + pargs = parser.parse_args(args) - if check_dir(pargs.destination_dir) != 0: - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - for source_dir in pargs.source_dirs: - if check_dir(source_dir) != 0: - return 1 + for source_dir in pargs.source_dirs: + if not mk_genfile_common.check_dir_exists(source_dir): + return 1 - mk_util.mk_mem_initializer_cpp_internal(pargs.source_dirs, pargs.destination_dir) - return 0 + output = mk_genfile_common.mk_mem_initializer_cpp_internal( + pargs.source_dirs, + pargs.destination_dir + ) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py index 3f2e7c507..76dc7ba48 100755 --- a/scripts/mk_pat_db.py +++ b/scripts/mk_pat_db.py @@ -3,32 +3,27 @@ Reads a pattern database and generates the corresponding header file. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("db_file", help="pattern database file") - parser.add_argument("output_file", help="output header file path") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("db_file", help="pattern database file") + parser.add_argument("output_file", help="output header file path") + pargs = parser.parse_args(args) - if not os.path.exists(pargs.db_file): - logging.error('"{}" does not exist'.format(pargs.db_file)) - return 1 + if not os.path.exists(pargs.db_file): + logging.error('"{}" does not exist'.format(pargs.db_file)) + return 1 - if (os.path.exists(pargs.output_file) and - not os.path.isfile(pargs.output_file)): - logging.error('Refusing to overwrite "{}"'.format( - pargs.output_file)) - return 1 - - mk_util.mk_pat_db_internal(pargs.db_file, pargs.output_file) - return 0 + mk_genfile_common.mk_pat_db_internal(pargs.db_file, pargs.output_file) + logging.info('Generated "{}"'.format(pargs.output_file)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 188dad7a4..1c7ee4ab5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -12,6 +12,7 @@ import re import getopt import shutil from mk_exception import * +import mk_genfile_common from fnmatch import fnmatch import distutils.sysconfig import compileall @@ -2498,104 +2499,6 @@ def mk_auto_src(): mk_all_mem_initializer_cpps() mk_all_gparams_register_modules() -UINT = 0 -BOOL = 1 -DOUBLE = 2 -STRING = 3 -SYMBOL = 4 -UINT_MAX = 4294967295 -CURRENT_PYG_HPP_DEST_DIR = None - -def get_current_pyg_hpp_dest_dir(): - return CURRENT_PYG_HPP_DEST_DIR - -TYPE2CPK = { UINT : 'CPK_UINT', BOOL : 'CPK_BOOL', DOUBLE : 'CPK_DOUBLE', STRING : 'CPK_STRING', SYMBOL : 'CPK_SYMBOL' } -TYPE2CTYPE = { UINT : 'unsigned', BOOL : 'bool', DOUBLE : 'double', STRING : 'char const *', SYMBOL : 'symbol' } -TYPE2GETTER = { UINT : 'get_uint', BOOL : 'get_bool', DOUBLE : 'get_double', STRING : 'get_str', SYMBOL : 'get_sym' } - -def pyg_default(p): - if p[1] == BOOL: - if p[2]: - return "true" - else: - return "false" - return p[2] - -def pyg_default_as_c_literal(p): - if p[1] == BOOL: - if p[2]: - return "true" - else: - return "false" - elif p[1] == STRING: - return '"%s"' % p[2] - elif p[1] == SYMBOL: - return 'symbol("%s")' % p[2] - elif p[1] == UINT: - return '%su' % p[2] - else: - return p[2] - -def to_c_method(s): - return s.replace('.', '_') - -def def_module_params(module_name, export, params, class_name=None, description=None): - dirname = get_current_pyg_hpp_dest_dir() - assert(os.path.exists(dirname)) - if class_name is None: - class_name = '%s_params' % module_name - hpp = os.path.join(dirname, '%s.hpp' % class_name) - out = open(hpp, 'w') - out.write('// Automatically generated file\n') - out.write('#ifndef __%s_HPP_\n' % class_name.upper()) - out.write('#define __%s_HPP_\n' % class_name.upper()) - out.write('#include"params.h"\n') - if export: - out.write('#include"gparams.h"\n') - out.write('struct %s {\n' % class_name) - out.write(' params_ref const & p;\n') - if export: - out.write(' params_ref g;\n') - out.write(' %s(params_ref const & _p = params_ref::get_empty()):\n' % class_name) - out.write(' p(_p)') - if export: - out.write(', g(gparams::get_module("%s"))' % module_name) - out.write(' {}\n') - out.write(' static void collect_param_descrs(param_descrs & d) {\n') - for param in params: - out.write(' d.insert("%s", %s, "%s", "%s","%s");\n' % (param[0], TYPE2CPK[param[1]], param[3], pyg_default(param), module_name)) - out.write(' }\n') - if export: - out.write(' /*\n') - out.write(" REG_MODULE_PARAMS('%s', '%s::collect_param_descrs')\n" % (module_name, class_name)) - if description is not None: - out.write(" REG_MODULE_DESCRIPTION('%s', '%s')\n" % (module_name, description)) - out.write(' */\n') - # Generated accessors - for param in params: - if export: - out.write(' %s %s() const { return p.%s("%s", g, %s); }\n' % - (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) - else: - out.write(' %s %s() const { return p.%s("%s", %s); }\n' % - (TYPE2CTYPE[param[1]], to_c_method(param[0]), TYPE2GETTER[param[1]], param[0], pyg_default_as_c_literal(param))) - out.write('};\n') - out.write('#endif\n') - out.close() - if is_verbose(): - print("Generated '%s'" % hpp) - -def max_memory_param(): - return ('max_memory', UINT, UINT_MAX, 'maximum amount of memory in megabytes') - -def max_steps_param(): - return ('max_steps', UINT, UINT_MAX, 'maximum number of steps') - -PYG_GLOBALS = { 'UINT' : UINT, 'BOOL' : BOOL, 'DOUBLE' : DOUBLE, 'STRING' : STRING, 'SYMBOL' : SYMBOL, - 'UINT_MAX' : UINT_MAX, - 'max_memory_param' : max_memory_param, - 'max_steps_param' : max_steps_param, - 'def_module_params' : def_module_params } def _execfile(file, globals=globals(), locals=locals()): if sys.version < "2.7": @@ -2606,13 +2509,13 @@ def _execfile(file, globals=globals(), locals=locals()): # Execute python auxiliary scripts that generate extra code for Z3. def exec_pyg_scripts(): - global CURRENT_PYG_HPP_DEST_DIR for root, dirs, files in os.walk('src'): for f in files: if f.endswith('.pyg'): script = os.path.join(root, f) - CURRENT_PYG_HPP_DEST_DIR = root - _execfile(script, PYG_GLOBALS) + generated_file = mk_genfile_common.mk_hpp_from_pyg(script, root) + if is_verbose(): + print("Generated '{}'".format(generated_file)) # TODO: delete after src/ast/pattern/expr_pattern_match # database.smt ==> database.h @@ -2620,17 +2523,9 @@ def mk_pat_db(): c = get_component(PATTERN_COMPONENT) fin = os.path.join(c.src_dir, 'database.smt2') fout = os.path.join(c.src_dir, 'database.h') - mk_pat_db_internal(fin, fout) - -def mk_pat_db_internal(inputFilePath, outputFilePath): - with open(inputFilePath, 'r') as fin: - with open(outputFilePath, 'w') as fout: - fout.write('static char const g_pattern_database[] =\n') - for line in fin: - fout.write('"%s\\n"\n' % line.strip('\n')) - fout.write(';\n') + mk_genfile_common.mk_pat_db_internal(fin, fout) if VERBOSE: - print("Generated '%s'" % outputFilePath) + print("Generated '{}'".format(fout)) # Update version numbers def update_version(): @@ -2681,82 +2576,14 @@ def mk_all_assembly_infos(major, minor, build, revision): else: raise MKException("Failed to find assembly template info file '%s'" % assembly_info_template) -ADD_TACTIC_DATA=[] -ADD_PROBE_DATA=[] - -def ADD_TACTIC(name, descr, cmd): - global ADD_TACTIC_DATA - ADD_TACTIC_DATA.append((name, descr, cmd)) - -def ADD_PROBE(name, descr, cmd): - global ADD_PROBE_DATA - ADD_PROBE_DATA.append((name, descr, cmd)) - -# Generate an install_tactics.cpp at path. -# This file implements the procedure -# void install_tactics(tactic_manager & ctx) -# It installs all tactics in the given component (name) list cnames -# The procedure looks for ADD_TACTIC commands in the .h files of these components. def mk_install_tactic_cpp(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_install_tactic_cpp_internal(component_src_dirs, path) - -def mk_install_tactic_cpp_internal(component_src_dirs, path): - global ADD_TACTIC_DATA, ADD_PROBE_DATA - ADD_TACTIC_DATA = [] - ADD_PROBE_DATA = [] - fullname = os.path.join(path, 'install_tactic.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include"tactic.h"\n') - fout.write('#include"tactic_cmds.h"\n') - fout.write('#include"cmd_context.h"\n') - tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') - probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - for component_src_dir in component_src_dirs: - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - if tactic_pat.match(line): - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - try: - exec(line.strip('\n '), globals()) - except: - raise MKException("Failed processing ADD_TACTIC command at '%s'\n%s" % (fullname, line)) - if probe_pat.match(line): - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - try: - exec(line.strip('\n '), globals()) - except: - raise MKException("Failed processing ADD_PROBE command at '%s'\n%s" % (fullname, line)) - fin.close() - # First pass will just generate the tactic factories - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write('MK_SIMPLE_TACTIC_FACTORY(__Z3_local_factory_%s, %s);\n' % (idx, data[2])) - idx = idx + 1 - fout.write('#define ADD_TACTIC_CMD(NAME, DESCR, FACTORY) ctx.insert(alloc(tactic_cmd, symbol(NAME), DESCR, alloc(FACTORY)))\n') - fout.write('#define ADD_PROBE(NAME, DESCR, PROBE) ctx.insert(alloc(probe_info, symbol(NAME), DESCR, PROBE))\n') - fout.write('void install_tactics(tactic_manager & ctx) {\n') - idx = 0 - for data in ADD_TACTIC_DATA: - fout.write(' ADD_TACTIC_CMD("%s", "%s", __Z3_local_factory_%s);\n' % (data[0], data[1], idx)) - idx = idx + 1 - for data in ADD_PROBE_DATA: - fout.write(' ADD_PROBE("%s", "%s", %s);\n' % data) - fout.write('}\n') - fout.close() + component_src_dirs = [] + for cname in cnames: + c = get_component(cname) + component_src_dirs.append(c.src_dir) + generated_file = mk_genfile_common.mk_install_tactic_cpp_internal(component_src_dirs, path) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_install_tactic_cpps(): if not ONLY_MAKEFILES: @@ -2767,67 +2594,14 @@ def mk_all_install_tactic_cpps(): cnames.append(c.name) mk_install_tactic_cpp(cnames, c.src_dir) -# Generate an mem_initializer.cpp at path. -# This file implements the procedures -# void mem_initialize() -# void mem_finalize() -# These procedures are invoked by the Z3 memory_manager def mk_mem_initializer_cpp(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_mem_initializer_cpp_internal(component_src_dirs, path) - -def mk_mem_initializer_cpp_internal(component_src_dirs, path): - initializer_cmds = [] - finalizer_cmds = [] - fullname = os.path.join(path, 'mem_initializer.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - initializer_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\'\)') - # ADD_INITIALIZER with priority - initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') - finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for component_src_dir in component_src_dirs: - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - m = initializer_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - initializer_cmds.append((m.group(1), 0)) - m = initializer_prio_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - initializer_cmds.append((m.group(1), int(m.group(2)))) - m = finalizer_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - finalizer_cmds.append(m.group(1)) - fin.close() - initializer_cmds.sort(key=lambda tup: tup[1]) - fout.write('void mem_initialize() {\n') - for (cmd, prio) in initializer_cmds: - fout.write(cmd) - fout.write('\n') - fout.write('}\n') - fout.write('void mem_finalize() {\n') - for cmd in finalizer_cmds: - fout.write(cmd) - fout.write('\n') - fout.write('}\n') - fout.close() + component_src_dirs = [] + for cname in cnames: + c = get_component(cname) + component_src_dirs.append(c.src_dir) + generated_file = mk_genfile_common.mk_mem_initializer_cpp_internal(component_src_dirs, path) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_mem_initializer_cpps(): if not ONLY_MAKEFILES: @@ -2838,61 +2612,14 @@ def mk_all_mem_initializer_cpps(): cnames.append(c.name) mk_mem_initializer_cpp(cnames, c.src_dir) -# Generate an ``gparams_register_modules.cpp`` at path. -# This file implements the procedure -# void gparams_register_modules() -# This procedure is invoked by gparams::init() def mk_gparams_register_modules(cnames, path): - component_src_dirs = [] - for cname in cnames: - c = get_component(cname) - component_src_dirs.append(c.src_dir) - mk_gparams_register_modules_internal(component_src_dirs, path) - -def mk_gparams_register_modules_internal(component_src_dirs, path): - cmds = [] - mod_cmds = [] - mod_descrs = [] - fullname = os.path.join(path, 'gparams_register_modules.cpp') - fout = open(fullname, 'w') - fout.write('// Automatically generated file.\n') - fout.write('#include"gparams.h"\n') - reg_pat = re.compile('[ \t]*REG_PARAMS\(\'([^\']*)\'\)') - reg_mod_pat = re.compile('[ \t]*REG_MODULE_PARAMS\(\'([^\']*)\', *\'([^\']*)\'\)') - reg_mod_descr_pat = re.compile('[ \t]*REG_MODULE_DESCRIPTION\(\'([^\']*)\', *\'([^\']*)\'\)') - for component_src_dir in component_src_dirs: - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(component_src_dir)) - for h_file in h_files: - added_include = False - fin = open(os.path.join(component_src_dir, h_file), 'r') - for line in fin: - m = reg_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - cmds.append((m.group(1))) - m = reg_mod_pat.match(line) - if m: - if not added_include: - added_include = True - fout.write('#include"%s"\n' % h_file) - mod_cmds.append((m.group(1), m.group(2))) - m = reg_mod_descr_pat.match(line) - if m: - mod_descrs.append((m.group(1), m.group(2))) - fin.close() - fout.write('void gparams_register_modules() {\n') - for code in cmds: - fout.write('{ param_descrs d; %s(d); gparams::register_global(d); }\n' % code) - for (mod, code) in mod_cmds: - fout.write('{ param_descrs * d = alloc(param_descrs); %s(*d); gparams::register_module("%s", d); }\n' % (code, mod)) - for (mod, descr) in mod_descrs: - fout.write('gparams::register_module_descr("%s", "%s");\n' % (mod, descr)) - fout.write('}\n') - fout.close() + component_src_dirs = [] + for cname in cnames: + c = get_component(cname) + component_src_dirs.append(c.src_dir) + generated_file = mk_genfile_common.mk_gparams_register_modules_internal(component_src_dirs, path) if VERBOSE: - print("Generated '%s'" % fullname) + print("Generated '{}'".format(generated_file)) def mk_all_gparams_register_modules(): if not ONLY_MAKEFILES: @@ -2912,28 +2639,7 @@ def mk_def_file(c): dot_h_c = c.find_file(dot_h, c.name) api = os.path.join(dot_h_c.src_dir, dot_h) export_header_files.append(api) - mk_def_file_internal(defname, dll_name, export_header_files) - -def mk_def_file_internal(defname, dll_name, export_header_files): - pat1 = re.compile(".*Z3_API.*") - fout = open(defname, 'w') - fout.write('LIBRARY "%s"\nEXPORTS\n' % dll_name) - num = 1 - for export_header_file in export_header_files: - api = open(export_header_file, 'r') - for line in api: - m = pat1.match(line) - if m: - words = re.split('\W+', line) - i = 0 - for w in words: - if w == 'Z3_API': - f = words[i+1] - fout.write('\t%s @%s\n' % (f, num)) - i = i + 1 - num = num + 1 - api.close() - fout.close() + mk_genfile_common.mk_def_file_internal(defname, dll_name, export_header_files) if VERBOSE: print("Generated '%s'" % defname) @@ -3026,83 +2732,9 @@ def mk_z3consts_py(api_files): api_file_c = api_dll.find_file(api_file, api_dll.name) api_file = os.path.join(api_file_c.src_dir, api_file) full_path_api_files.append(api_file) - mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) - -def mk_z3consts_py_internal(api_files, output_dir): - assert os.path.isdir(output_dir) - assert isinstance(api_files, list) - - blank_pat = re.compile("^ *\r?$") - comment_pat = re.compile("^ *//.*$") - typedef_pat = re.compile("typedef enum *") - typedef2_pat = re.compile("typedef enum { *") - openbrace_pat = re.compile("{ *") - closebrace_pat = re.compile("}.*;") - - z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') - z3consts.write('# Automatically generated file\n\n') - for api_file in api_files: - api = open(api_file, 'r') - - SEARCHING = 0 - FOUND_ENUM = 1 - IN_ENUM = 2 - - mode = SEARCHING - decls = {} - idx = 0 - - linenum = 1 - for line in api: - m1 = blank_pat.match(line) - m2 = comment_pat.match(line) - if m1 or m2: - # skip blank lines and comments - linenum = linenum + 1 - elif mode == SEARCHING: - m = typedef_pat.match(line) - if m: - mode = FOUND_ENUM - m = typedef2_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - elif mode == FOUND_ENUM: - m = openbrace_pat.match(line) - if m: - mode = IN_ENUM - decls = {} - idx = 0 - else: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - assert mode == IN_ENUM - words = re.split('[^\-a-zA-Z0-9_]+', line) - m = closebrace_pat.match(line) - if m: - name = words[1] - z3consts.write('# enum %s\n' % name) - for k in decls: - i = decls[k] - z3consts.write('%s = %s\n' % (k, i)) - z3consts.write('\n') - mode = SEARCHING - elif len(words) <= 2: - assert False, "Invalid %s, line: %s" % (api_file, linenum) - else: - if words[2] != '': - if len(words[2]) > 1 and words[2][1] == 'x': - idx = int(words[2], 16) - else: - idx = int(words[2]) - decls[words[1]] = idx - idx = idx + 1 - linenum = linenum + 1 - api.close() - z3consts.close() + generated_file = mk_genfile_common.mk_z3consts_py_internal(full_path_api_files, Z3PY_SRC_DIR) if VERBOSE: - print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py')) + print("Generated '{}".format(generated_file)) # Extract enumeration types from z3_api.h, and add .Net definitions diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py index f1ada2b84..b1af3edc9 100755 --- a/scripts/pyg2hpp.py +++ b/scripts/pyg2hpp.py @@ -4,39 +4,33 @@ Reads a pyg file and emits the corresponding C++ header file into the specified destination directory. """ -import mk_util +import mk_genfile_common import argparse import logging import os import sys def main(args): - logging.basicConfig(level=logging.INFO) - parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("pyg_file", help="pyg file") - parser.add_argument("destination_dir", help="destination directory") - pargs = parser.parse_args(args) + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("pyg_file", help="pyg file") + parser.add_argument("destination_dir", help="destination directory") + pargs = parser.parse_args(args) - if not os.path.exists(pargs.pyg_file): - logging.error('"{}" does not exist'.format(pargs.pyg_file)) - return 1 + if not os.path.exists(pargs.pyg_file): + logging.error('"{}" does not exist'.format(pargs.pyg_file)) + return 1 - if not os.path.exists(pargs.destination_dir): - logging.error('"{}" does not exist'.format(pargs.destination_dir)) - return 1 + if not mk_genfile_common.check_dir_exists(pargs.destination_dir): + return 1 - if not os.path.isdir(pargs.destination_dir): - logging.error('"{}" is not a directory'.format(pargs.destination_dir)) - return 1 - - pyg_full_path = os.path.abspath(pargs.pyg_file) - destination_dir_full_path = os.path.abspath(pargs.destination_dir) - logging.info('Using {}'.format(pyg_full_path)) - # Use the existing infrastructure to do this - mk_util.CURRENT_PYG_HPP_DEST_DIR = destination_dir_full_path - mk_util._execfile(pyg_full_path, mk_util.PYG_GLOBALS) - return 0 + pyg_full_path = os.path.abspath(pargs.pyg_file) + destination_dir_full_path = os.path.abspath(pargs.destination_dir) + logging.info('Using {}'.format(pyg_full_path)) + output = mk_genfile_common.mk_hpp_from_pyg(pyg_full_path, destination_dir_full_path) + logging.info('Generated "{}"'.format(output)) + return 0 if __name__ == '__main__': - sys.exit(main(sys.argv[1:])) + sys.exit(main(sys.argv[1:])) diff --git a/src/ackermannization/ackermannize_bv_tactic.cpp b/src/ackermannization/ackermannize_bv_tactic.cpp index 123b496a1..f9c48c2bd 100644 --- a/src/ackermannization/ackermannize_bv_tactic.cpp +++ b/src/ackermannization/ackermannize_bv_tactic.cpp @@ -38,6 +38,7 @@ public: tactic_report report("ackermannize", *g); fail_if_unsat_core_generation("ackermannize", g); fail_if_proof_generation("ackermannize", g); + TRACE("ackermannize", g->display(tout << "in\n");); expr_ref_vector flas(m); const unsigned sz = g->size(); @@ -48,6 +49,7 @@ public: goal_ref resg(alloc(goal, *g, true)); const bool success = lackr.mk_ackermann(resg, m_lemma_limit); if (!success) { // Just pass on the input unchanged + TRACE("ackermannize", tout << "ackermannize not run due to limit" << std::endl;); result.reset(); result.push_back(g.get()); mc = 0; @@ -62,7 +64,7 @@ public: } resg->inc_depth(); - TRACE("ackermannize", resg->display(tout);); + TRACE("ackermannize", resg->display(tout << "out\n");); SASSERT(resg->is_well_sorted()); } diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 09034fa36..8e99fe2a2 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -34,11 +34,13 @@ struct lackr_model_constructor::imp { , m_conflicts(conflicts) , m_b_rw(m) , m_bv_rw(m) + , m_evaluator(NULL) , m_empty_model(m) , m_ackr_helper(m) {} ~imp() { + if (m_evaluator) dealloc(m_evaluator); { values2val_t::iterator i = m_values2val.begin(); const values2val_t::iterator e = m_values2val.end(); @@ -60,15 +62,17 @@ struct lackr_model_constructor::imp { // // Returns true iff model was successfully constructed. + // Conflicts are saved as a side effect. // bool check() { + bool retv = true; for (unsigned i = 0; i < m_abstr_model->get_num_constants(); i++) { func_decl * const c = m_abstr_model->get_constant(i); - app * const term = m_info->find_term(c); - if (term) m_stack.push_back(term); - else m_stack.push_back(m_m.mk_const(c)); + app * const _term = m_info->find_term(c); + expr * const term = _term ? _term : m_m.mk_const(c); + if (!check_term(term)) retv = false; } - return run(); + return retv; } @@ -134,7 +138,7 @@ struct lackr_model_constructor::imp { conflict_list& m_conflicts; bool_rewriter m_b_rw; bv_rewriter m_bv_rw; - scoped_ptr m_evaluator; + model_evaluator * m_evaluator; model m_empty_model; private: struct val_info { expr * value; app * source_term; }; @@ -144,6 +148,7 @@ struct lackr_model_constructor::imp { app2val_t m_app2val; ptr_vector m_stack; ackr_helper m_ackr_helper; + expr_mark m_visited; static inline val_info mk_val_info(expr* value, app* source_term) { val_info rv; @@ -152,17 +157,23 @@ struct lackr_model_constructor::imp { return rv; } - // + // Performs congruence check on a given term. + bool check_term(expr * term) { + m_stack.push_back(term); + const bool rv = _check_stack(); + m_stack.reset(); + return rv; + } + // Performs congruence check on terms on the stack. - // (Currently stops upon the first failure). - // Returns true if and only if congruence check succeeded. - bool run() { - m_evaluator = alloc(model_evaluator, m_empty_model); - expr_mark visited; + // Stops upon the first failure. + // Returns true if and only if all congruence checks succeeded. + bool _check_stack() { + if (m_evaluator == NULL) m_evaluator = alloc(model_evaluator, m_empty_model); expr * curr; while (!m_stack.empty()) { curr = m_stack.back(); - if (visited.is_marked(curr)) { + if (m_visited.is_marked(curr)) { m_stack.pop_back(); continue; } @@ -173,8 +184,8 @@ struct lackr_model_constructor::imp { return false; case AST_APP: { app * a = to_app(curr); - if (for_each_expr_args(m_stack, visited, a->get_num_args(), a->get_args())) { - visited.mark(a, true); + if (for_each_expr_args(m_stack, m_visited, a->get_num_args(), a->get_args())) { + m_visited.mark(a, true); m_stack.pop_back(); if (!mk_value(a)) return false; } @@ -212,7 +223,11 @@ struct lackr_model_constructor::imp { for (unsigned i = 0; i < num; ++i) { expr * val; const bool b = eval_cached(to_app(args[i]), val); // TODO: OK conversion to_app? - CTRACE("model_constructor", !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2); ); + CTRACE("model_constructor", m_conflicts.empty() && !b, tout << "fail arg val(\n" << mk_ismt2_pp(args[i], m_m, 2) << '\n'; ); + if (!b) { + // bailing out because args eval failed previously + return false; + } TRACE("model_constructor", tout << "arg val " << i << "(\n" << mk_ismt2_pp(args[i], m_m, 2) << " : " << mk_ismt2_pp(val, m_m, 2) << '\n'; ); diff --git a/src/ast/fpa/fpa2bv_converter.cpp b/src/ast/fpa/fpa2bv_converter.cpp index 0d90e1c5a..4a3ec7553 100644 --- a/src/ast/fpa/fpa2bv_converter.cpp +++ b/src/ast/fpa/fpa2bv_converter.cpp @@ -1155,38 +1155,34 @@ expr_ref fpa2bv_converter::mk_min_unspecified(func_decl * f, expr * x, expr * y) expr_ref res(m); // The only cases in which min is unspecified for is when the arguments are +0.0 and -0.0. + // There is no "hardware interpretation" for fp.min. - if (m_hi_fp_unspecified) - // The hardware interpretation is -0.0. - mk_nzero(f, res); - else { - std::pair decls(0, 0); - if (!m_specials.find(f, decls)) { - decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_specials.insert(f, decls); - m.inc_ref(f); - m.inc_ref(decls.first); - m.inc_ref(decls.second); - } - - expr_ref pn(m), np(m); - mk_fp(decls.first, - m_bv_util.mk_numeral(0, ebits), - m_bv_util.mk_numeral(0, sbits - 1), - pn); - mk_fp(decls.second, - m_bv_util.mk_numeral(0, ebits), - m_bv_util.mk_numeral(0, sbits - 1), - np); - - expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); - mk_is_pzero(x, x_is_pzero); - mk_is_nzero(y, x_is_nzero); - m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); - mk_ite(xyzero, pn, np, res); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } + expr_ref pn(m), np(m); + mk_fp(decls.first, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + pn); + mk_fp(decls.second, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + np); + + expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); + mk_is_pzero(x, x_is_pzero); + mk_is_nzero(y, x_is_nzero); + m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); + mk_ite(xyzero, pn, np, res); + return res; } @@ -1244,38 +1240,34 @@ expr_ref fpa2bv_converter::mk_max_unspecified(func_decl * f, expr * x, expr * y) expr_ref res(m); // The only cases in which max is unspecified for is when the arguments are +0.0 and -0.0. + // There is no "hardware interpretation" for fp.max. - if (m_hi_fp_unspecified) - // The hardware interpretation is +0.0. - mk_pzero(f, res); - else { - std::pair decls(0, 0); - if (!m_specials.find(f, decls)) { - decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); - m_specials.insert(f, decls); - m.inc_ref(f); - m.inc_ref(decls.first); - m.inc_ref(decls.second); - } - - expr_ref pn(m), np(m); - mk_fp(decls.first, - m_bv_util.mk_numeral(0, ebits), - m_bv_util.mk_numeral(0, sbits - 1), - pn); - mk_fp(decls.second, - m_bv_util.mk_numeral(0, ebits), - m_bv_util.mk_numeral(0, sbits - 1), - np); - - expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); - mk_is_pzero(x, x_is_pzero); - mk_is_nzero(y, x_is_nzero); - m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); - mk_ite(xyzero, pn, np, res); + std::pair decls(0, 0); + if (!m_specials.find(f, decls)) { + decls.first = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + decls.second = m.mk_fresh_const(0, m_bv_util.mk_sort(1)); + m_specials.insert(f, decls); + m.inc_ref(f); + m.inc_ref(decls.first); + m.inc_ref(decls.second); } + expr_ref pn(m), np(m); + mk_fp(decls.first, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + pn); + mk_fp(decls.second, + m_bv_util.mk_numeral(0, ebits), + m_bv_util.mk_numeral(0, sbits - 1), + np); + + expr_ref x_is_pzero(m), x_is_nzero(m), xyzero(m); + mk_is_pzero(x, x_is_pzero); + mk_is_nzero(y, x_is_nzero); + m_simp.mk_and(x_is_pzero, x_is_nzero, xyzero); + mk_ite(xyzero, pn, np, res); + return res; } diff --git a/src/ast/fpa/fpa2bv_rewriter.cpp b/src/ast/fpa/fpa2bv_rewriter.cpp index 188a73e95..710faf447 100644 --- a/src/ast/fpa/fpa2bv_rewriter.cpp +++ b/src/ast/fpa/fpa2bv_rewriter.cpp @@ -28,7 +28,7 @@ fpa2bv_rewriter_cfg::fpa2bv_rewriter_cfg(ast_manager & m, fpa2bv_converter & c, m_manager(m), m_out(m), m_conv(c), - m_bindings(m) + m_bindings(m) { updt_params(p); // We need to make sure that the mananger has the BV plugin loaded. @@ -49,7 +49,7 @@ void fpa2bv_rewriter_cfg::updt_params(params_ref const & p) { updt_local_params(p); } -bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const { +bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const { cooperate("fpa2bv"); return num_steps > m_max_steps; } @@ -57,22 +57,22 @@ bool fpa2bv_rewriter_cfg::max_steps_exceeded(unsigned num_steps) const { br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * const * args, expr_ref & result, proof_ref & result_pr) { TRACE("fpa2bv_rw", tout << "APP: " << f->get_name() << std::endl; ); - + if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_float(f->get_range())) { m_conv.mk_const(f, result); return BR_DONE; } - + if (num == 0 && f->get_family_id() == null_family_id && m_conv.is_rm(f->get_range())) { m_conv.mk_rm_const(f, result); return BR_DONE; } - + if (m().is_eq(f)) { SASSERT(num == 2); - TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << + TRACE("fpa2bv_rw", tout << "(= " << mk_ismt2_pp(args[0], m()) << " " << mk_ismt2_pp(args[1], m()) << ")" << std::endl;); - SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); + SASSERT(m().get_sort(args[0]) == m().get_sort(args[1])); sort * ds = f->get_domain()[0]; if (m_conv.is_float(ds)) { m_conv.mk_eq(args[0], args[1], result); @@ -100,7 +100,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co } return BR_FAILED; } - + if (m_conv.is_float_family(f)) { switch (f->get_decl_kind()) { case OP_FPA_RM_NEAREST_TIES_TO_AWAY: @@ -108,7 +108,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_RM_TOWARD_NEGATIVE: case OP_FPA_RM_TOWARD_POSITIVE: case OP_FPA_RM_TOWARD_ZERO: m_conv.mk_rounding_mode(f, result); return BR_DONE; - case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; + case OP_FPA_NUM: m_conv.mk_numeral(f, num, args, result); return BR_DONE; case OP_FPA_PLUS_INF: m_conv.mk_pinf(f, result); return BR_DONE; case OP_FPA_MINUS_INF: m_conv.mk_ninf(f, result); return BR_DONE; case OP_FPA_PLUS_ZERO: m_conv.mk_pzero(f, result); return BR_DONE; @@ -120,7 +120,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_MUL: m_conv.mk_mul(f, num, args, result); return BR_DONE; case OP_FPA_DIV: m_conv.mk_div(f, num, args, result); return BR_DONE; case OP_FPA_REM: m_conv.mk_rem(f, num, args, result); return BR_DONE; - case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; + case OP_FPA_ABS: m_conv.mk_abs(f, num, args, result); return BR_DONE; case OP_FPA_FMA: m_conv.mk_fma(f, num, args, result); return BR_DONE; case OP_FPA_SQRT: m_conv.mk_sqrt(f, num, args, result); return BR_DONE; case OP_FPA_ROUND_TO_INTEGRAL: m_conv.mk_round_to_integral(f, num, args, result); return BR_DONE; @@ -129,7 +129,7 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_GT: m_conv.mk_float_gt(f, num, args, result); return BR_DONE; case OP_FPA_LE: m_conv.mk_float_le(f, num, args, result); return BR_DONE; case OP_FPA_GE: m_conv.mk_float_ge(f, num, args, result); return BR_DONE; - case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; + case OP_FPA_IS_ZERO: m_conv.mk_is_zero(f, num, args, result); return BR_DONE; case OP_FPA_IS_NAN: m_conv.mk_is_nan(f, num, args, result); return BR_DONE; case OP_FPA_IS_INF: m_conv.mk_is_inf(f, num, args, result); return BR_DONE; case OP_FPA_IS_NORMAL: m_conv.mk_is_normal(f, num, args, result); return BR_DONE; @@ -143,20 +143,20 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co case OP_FPA_TO_SBV: m_conv.mk_to_sbv(f, num, args, result); return BR_DONE; case OP_FPA_TO_REAL: m_conv.mk_to_real(f, num, args, result); return BR_DONE; case OP_FPA_TO_IEEE_BV: m_conv.mk_to_ieee_bv(f, num, args, result); return BR_DONE; - + case OP_FPA_MIN: m_conv.mk_min(f, num, args, result); return BR_REWRITE_FULL; case OP_FPA_MAX: m_conv.mk_max(f, num, args, result); return BR_REWRITE_FULL; - + case OP_FPA_INTERNAL_MIN_UNSPECIFIED: result = m_conv.mk_min_unspecified(f, args[0], args[1]); return BR_DONE; case OP_FPA_INTERNAL_MAX_UNSPECIFIED: result = m_conv.mk_max_unspecified(f, args[0], args[1]); return BR_DONE; case OP_FPA_INTERNAL_MIN_I: m_conv.mk_min_i(f, num, args, result); return BR_DONE; case OP_FPA_INTERNAL_MAX_I: m_conv.mk_max_i(f, num, args, result); return BR_DONE; - + case OP_FPA_INTERNAL_RM: - case OP_FPA_INTERNAL_BVWRAP: - case OP_FPA_INTERNAL_BVUNWRAP: + case OP_FPA_INTERNAL_BVWRAP: + case OP_FPA_INTERNAL_BVUNWRAP: case OP_FPA_INTERNAL_TO_REAL_UNSPECIFIED: - case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: + case OP_FPA_INTERNAL_TO_UBV_UNSPECIFIED: case OP_FPA_INTERNAL_TO_SBV_UNSPECIFIED: return BR_FAILED; default: TRACE("fpa2bv", tout << "unsupported operator: " << f->get_name() << "\n"; @@ -167,27 +167,27 @@ br_status fpa2bv_rewriter_cfg::reduce_app(func_decl * f, unsigned num, expr * co else { SASSERT(!m_conv.is_float_family(f)); bool is_float_uf = m_conv.is_float(f->get_range()) || m_conv.is_rm(f->get_range()); - + for (unsigned i = 0; i < f->get_arity(); i++) { sort * di = f->get_domain()[i]; is_float_uf |= m_conv.is_float(di) || m_conv.is_rm(di); } - + if (is_float_uf) { m_conv.mk_uninterpreted_function(f, num, args, result); return BR_DONE; } } - + return BR_FAILED; } bool fpa2bv_rewriter_cfg::pre_visit(expr * t) { TRACE("fpa2bv", tout << "pre_visit: " << mk_ismt2_pp(t, m()) << std::endl;); - - if (is_quantifier(t)) { - quantifier * q = to_quantifier(t); + + if (is_quantifier(t)) { + quantifier * q = to_quantifier(t); TRACE("fpa2bv", tout << "pre_visit quantifier [" << q->get_id() << "]: " << mk_ismt2_pp(q->get_expr(), m()) << std::endl;); sort_ref_vector new_bindings(m_manager); for (unsigned i = 0 ; i < q->get_num_decls(); i++) @@ -199,9 +199,9 @@ bool fpa2bv_rewriter_cfg::pre_visit(expr * t) } -bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, - expr * new_body, - expr * const * new_patterns, +bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, + expr * new_body, + expr * const * new_patterns, expr * const * new_no_patterns, expr_ref & result, proof_ref & result_pr) { @@ -221,7 +221,7 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, name_buffer.reset(); name_buffer << n << ".bv"; new_decl_names.push_back(symbol(name_buffer.c_str())); - new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); + new_decl_sorts.push_back(m_conv.bu().mk_sort(sbits+ebits)); } else { new_decl_sorts.push_back(s); @@ -232,19 +232,19 @@ bool fpa2bv_rewriter_cfg::reduce_quantifier(quantifier * old_q, new_body, old_q->get_weight(), old_q->get_qid(), old_q->get_skid(), old_q->get_num_patterns(), new_patterns, old_q->get_num_no_patterns(), new_no_patterns); result_pr = 0; - m_bindings.shrink(old_sz); - TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << + m_bindings.shrink(old_sz); + TRACE("fpa2bv", tout << "reduce_quantifier[" << old_q->get_depth() << "]: " << mk_ismt2_pp(old_q->get_expr(), m()) << std::endl << " new body: " << mk_ismt2_pp(new_body, m()) << std::endl; - tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); + tout << "result = " << mk_ismt2_pp(result, m()) << std::endl;); return true; } -bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { +bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & result_pr) { if (t->get_idx() >= m_bindings.size()) return false; - // unsigned inx = m_bindings.size() - t->get_idx() - 1; - + // unsigned inx = m_bindings.size() - t->get_idx() - 1; + expr_ref new_exp(m()); sort * s = t->get_sort(); if (m_conv.is_float(s)) @@ -255,14 +255,14 @@ bool fpa2bv_rewriter_cfg::reduce_var(var * t, expr_ref & result, proof_ref & res new_var = m().mk_var(t->get_idx(), m_conv.bu().mk_sort(sbits+ebits)); m_conv.mk_fp(m_conv.bu().mk_extract(sbits+ebits-1, sbits+ebits-1, new_var), m_conv.bu().mk_extract(ebits - 1, 0, new_var), - m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), + m_conv.bu().mk_extract(sbits+ebits-2, ebits, new_var), new_exp); } else new_exp = m().mk_var(t->get_idx(), s); - + result = new_exp; - result_pr = 0; + result_pr = 0; TRACE("fpa2bv", tout << "reduce_var: " << mk_ismt2_pp(t, m()) << " -> " << mk_ismt2_pp(result, m()) << std::endl;); return true; } diff --git a/src/ast/fpa_decl_plugin.cpp b/src/ast/fpa_decl_plugin.cpp index 317112cae..7d0126d06 100644 --- a/src/ast/fpa_decl_plugin.cpp +++ b/src/ast/fpa_decl_plugin.cpp @@ -593,7 +593,7 @@ func_decl * fpa_decl_plugin::mk_to_fp_unsigned(decl_kind k, unsigned num_paramet } func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { if (arity != 3) m_manager->raise_exception("invalid number of arguments to fp"); if (!is_sort_of(domain[0], m_bv_fid, BV_SORT) || @@ -610,7 +610,7 @@ func_decl * fpa_decl_plugin::mk_fp(decl_kind k, unsigned num_parameters, paramet } func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { SASSERT(m_bv_plugin); if (arity != 2) m_manager->raise_exception("invalid number of arguments to fp.to_ubv"); @@ -631,7 +631,7 @@ func_decl * fpa_decl_plugin::mk_to_ubv(decl_kind k, unsigned num_parameters, par } func_decl * fpa_decl_plugin::mk_to_sbv(decl_kind k, unsigned num_parameters, parameter const * parameters, - unsigned arity, sort * const * domain, sort * range) { + unsigned arity, sort * const * domain, sort * range) { SASSERT(m_bv_plugin); if (arity != 2) m_manager->raise_exception("invalid number of arguments to fp.to_sbv"); @@ -671,9 +671,9 @@ func_decl * fpa_decl_plugin::mk_to_ieee_bv(decl_kind k, unsigned num_parameters, unsigned float_sz = domain[0]->get_parameter(0).get_int() + domain[0]->get_parameter(1).get_int(); parameter ps[] = { parameter(float_sz) }; - sort * bv_srt = m_bv_plugin->mk_sort(m_bv_fid, 1, ps); + sort * bv_srt = m_bv_plugin->mk_sort(BV_SORT, 1, ps); symbol name("to_ieee_bv"); - return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k, num_parameters, parameters)); + return m_manager->mk_func_decl(name, 1, domain, bv_srt, func_decl_info(m_family_id, k)); } func_decl * fpa_decl_plugin::mk_internal_rm(decl_kind k, unsigned num_parameters, parameter const * parameters, diff --git a/src/ast/rewriter/fpa_rewriter.cpp b/src/ast/rewriter/fpa_rewriter.cpp index bc3f8c25e..57fb606ba 100644 --- a/src/ast/rewriter/fpa_rewriter.cpp +++ b/src/ast/rewriter/fpa_rewriter.cpp @@ -150,11 +150,9 @@ br_status fpa_rewriter::mk_to_sbv_unspecified(func_decl * f, expr_ref & result) } br_status fpa_rewriter::mk_to_ieee_bv_unspecified(func_decl * f, expr_ref & result) { - SASSERT(f->get_num_parameters() == 1); - SASSERT(f->get_parameter(0).is_int()); - unsigned bv_sz = f->get_parameter(0).get_int(); - bv_util bu(m()); + unsigned bv_sz = bu.get_bv_size(f->get_range()); + if (m_hi_fp_unspecified) // The "hardware interpretation" is 0. result = bu.mk_numeral(0, bv_sz); diff --git a/src/muz/pdr/pdr_sym_mux.cpp b/src/muz/pdr/pdr_sym_mux.cpp index 198752846..a68b57e9c 100644 --- a/src/muz/pdr/pdr_sym_mux.cpp +++ b/src/muz/pdr/pdr_sym_mux.cpp @@ -32,7 +32,7 @@ sym_mux::sym_mux(ast_manager & m) : m(m), m_ref_holder(m), m_next_sym_suffix_idx(0) { m_suffixes.push_back("_n"); - unsigned suf_sz = m_suffixes.size(); + size_t suf_sz = m_suffixes.size(); for(unsigned i = 0; i < suf_sz; ++i) { symbol suff_sym = symbol(m_suffixes[i].c_str()); m_used_suffixes.insert(suff_sym); diff --git a/src/sat/sat_solver/inc_sat_solver.cpp b/src/sat/sat_solver/inc_sat_solver.cpp index b5617098e..355c52f1e 100644 --- a/src/sat/sat_solver/inc_sat_solver.cpp +++ b/src/sat/sat_solver/inc_sat_solver.cpp @@ -72,7 +72,7 @@ public: m_asmsf(m), m_fmls_head(0), m_core(m), - m_map(m), + m_map(m), m_num_scopes(0), m_dep_core(m), m_unknown("no reason given") { @@ -214,7 +214,7 @@ public: m_optimize_model = m_params.get_bool("optimize_model", false); } virtual void collect_statistics(statistics & st) const { - m_preprocess->collect_statistics(st); + if (m_preprocess) m_preprocess->collect_statistics(st); m_solver.collect_statistics(st); } virtual void get_unsat_core(ptr_vector & r) { @@ -440,7 +440,7 @@ private: DEBUG_CODE( for (unsigned i = 0; i < m_fmls.size(); ++i) { expr_ref tmp(m); - if (m_model->eval(m_fmls[i].get(), tmp, true)) { + if (m_model->eval(m_fmls[i].get(), tmp, true)) { CTRACE("sat", !m.is_true(tmp), tout << "Evaluation failed: " << mk_pp(m_fmls[i].get(), m) << " to " << tmp << "\n"; diff --git a/src/tactic/core/reduce_args_tactic.cpp b/src/tactic/core/reduce_args_tactic.cpp index cf83a5a10..4f6f4c3d7 100644 --- a/src/tactic/core/reduce_args_tactic.cpp +++ b/src/tactic/core/reduce_args_tactic.cpp @@ -83,14 +83,34 @@ tactic * mk_reduce_args_tactic(ast_manager & m, params_ref const & p) { struct reduce_args_tactic::imp { ast_manager & m_manager; - bool m_produce_models; + bv_util m_bv; ast_manager & m() const { return m_manager; } imp(ast_manager & m): - m_manager(m) { + m_manager(m), + m_bv(m) { } + static bool is_var_plus_offset(ast_manager& m, bv_util& bv, expr* e, expr*& base) { + expr *lhs, *rhs; + if (bv.is_bv_add(e, lhs, rhs) && bv.is_numeral(lhs)) { + base = rhs; + } else { + base = e; + } + return true; + } + + static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e, expr*& base) { + base = 0; + return m.is_unique_value(e) || is_var_plus_offset(m, bv, e, base); + } + + static bool may_be_unique(ast_manager& m, bv_util& bv, expr* e) { + expr* base; + return may_be_unique(m, bv, e, base); + } void checkpoint() { if (m_manager.canceled()) @@ -100,10 +120,12 @@ struct reduce_args_tactic::imp { struct find_non_candidates_proc { ast_manager & m_manager; + bv_util & m_bv; obj_hashtable & m_non_cadidates; - find_non_candidates_proc(ast_manager & m, obj_hashtable & non_cadidates): + find_non_candidates_proc(ast_manager & m, bv_util & bv, obj_hashtable & non_cadidates): m_manager(m), + m_bv(bv), m_non_cadidates(non_cadidates) { } @@ -122,7 +144,7 @@ struct reduce_args_tactic::imp { unsigned j = n->get_num_args(); while (j > 0) { --j; - if (m_manager.is_unique_value(n->get_arg(j))) + if (may_be_unique(m_manager, m_bv, n->get_arg(j))) return; } m_non_cadidates.insert(d); @@ -135,7 +157,7 @@ struct reduce_args_tactic::imp { */ void find_non_candidates(goal const & g, obj_hashtable & non_candidates) { non_candidates.reset(); - find_non_candidates_proc proc(m_manager, non_candidates); + find_non_candidates_proc proc(m_manager, m_bv, non_candidates); expr_fast_mark1 visited; unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { @@ -154,11 +176,13 @@ struct reduce_args_tactic::imp { struct populate_decl2args_proc { ast_manager & m_manager; + bv_util & m_bv; obj_hashtable & m_non_cadidates; obj_map & m_decl2args; - - populate_decl2args_proc(ast_manager & m, obj_hashtable & nc, obj_map & d): - m_manager(m), m_non_cadidates(nc), m_decl2args(d) {} + obj_map > m_decl2base; // for args = base + offset + + populate_decl2args_proc(ast_manager & m, bv_util & bv, obj_hashtable & nc, obj_map & d): + m_manager(m), m_bv(bv), m_non_cadidates(nc), m_decl2args(d) {} void operator()(var * n) {} void operator()(quantifier * n) {} @@ -172,20 +196,25 @@ struct reduce_args_tactic::imp { return; // declaration is not a candidate unsigned j = n->get_num_args(); obj_map::iterator it = m_decl2args.find_iterator(d); + expr* base; if (it == m_decl2args.end()) { m_decl2args.insert(d, bit_vector()); + svector& bases = m_decl2base.insert_if_not_there2(d, svector())->get_data().m_value; + bases.resize(j); it = m_decl2args.find_iterator(d); SASSERT(it != m_decl2args.end()); it->m_value.reserve(j); while (j > 0) { --j; - it->m_value.set(j, m_manager.is_unique_value(n->get_arg(j))); + it->m_value.set(j, may_be_unique(m_manager, m_bv, n->get_arg(j), base)); + bases[j] = base; } } else { + svector& bases = m_decl2base[d]; SASSERT(j == it->m_value.size()); while (j > 0) { --j; - it->m_value.set(j, it->m_value.get(j) && m_manager.is_unique_value(n->get_arg(j))); + it->m_value.set(j, it->m_value.get(j) && may_be_unique(m_manager, m_bv, n->get_arg(j), base) && bases[j] == base); } } } @@ -196,7 +225,7 @@ struct reduce_args_tactic::imp { obj_map & decl2args) { expr_fast_mark1 visited; decl2args.reset(); - populate_decl2args_proc proc(m_manager, non_candidates, decl2args); + populate_decl2args_proc proc(m_manager, m_bv, non_candidates, decl2args); unsigned sz = g.size(); for (unsigned i = 0; i < sz; i++) { checkpoint(); @@ -291,67 +320,6 @@ struct reduce_args_tactic::imp { } } }; - - struct populate_decl2arg_set_proc { - ast_manager & m_manager; - obj_map & m_decl2args; - decl2arg2func_map & m_decl2arg2funcs; - - populate_decl2arg_set_proc(ast_manager & m, - obj_map & d, - decl2arg2func_map & ds): - m_manager(m), m_decl2args(d), m_decl2arg2funcs(ds) {} - - void operator()(var * n) {} - void operator()(quantifier * n) {} - - void operator()(app * n) { - if (n->get_num_args() == 0) - return; // ignore constants - func_decl * d = n->get_decl(); - if (d->get_family_id() != null_family_id) - return; // ignore interpreted symbols - obj_map::iterator it = m_decl2args.find_iterator(d); - if (it == m_decl2args.end()) - return; // not reducing the arguments of this declaration - bit_vector & bv = it->m_value; - arg2func * map = 0; - decl2arg2func_map::iterator it2 = m_decl2arg2funcs.find_iterator(d); - if (it2 == m_decl2arg2funcs.end()) { - map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv)); - m_decl2arg2funcs.insert(d, map); - } - else { - map = it2->m_value; - } - if (!map->contains(n)) { - // create fresh symbol... - ptr_buffer domain; - unsigned arity = d->get_arity(); - for (unsigned i = 0; i < arity; i++) { - if (!bv.get(i)) - domain.push_back(d->get_domain(i)); - } - func_decl * new_d = m_manager.mk_fresh_func_decl(d->get_name(), symbol::null, domain.size(), domain.c_ptr(), d->get_range()); - map->insert(n, new_d); - m_manager.inc_ref(n); - m_manager.inc_ref(new_d); - } - } - }; - - void populate_decl2arg_set(goal const & g, - obj_map & decl2args, - decl2arg2func_map & decl2arg2funcs) { - expr_fast_mark1 visited; - - populate_decl2arg_set_proc proc(m_manager, decl2args, decl2arg2funcs); - unsigned sz = g.size(); - for (unsigned i = 0; i < sz; i++) { - checkpoint(); - quick_for_each_expr(proc, visited, g.form(i)); - } - } struct reduce_args_rw_cfg : public default_rewriter_cfg { ast_manager & m; @@ -377,24 +345,31 @@ struct reduce_args_tactic::imp { return BR_FAILED; // ignore constants if (f->get_family_id() != null_family_id) return BR_FAILED; // ignore interpreted symbols - decl2arg2func_map::iterator it = m_decl2arg2funcs.find_iterator(f); - if (it == m_decl2arg2funcs.end()) + obj_map::iterator it = m_decl2args.find_iterator(f); + if (it == m_decl2args.end()) return BR_FAILED; - SASSERT(m_decl2args.contains(f)); - bit_vector & bv = m_decl2args.find(f); - arg2func * map = it->m_value; - app_ref tmp(m); - tmp = m.mk_app(f, num, args); - CTRACE("reduce_args", !map->contains(tmp), - tout << "map does not contain tmp f: " << f->get_name() << "\n"; - tout << mk_ismt2_pp(tmp, m) << "\n"; - arg2func::iterator it = map->begin(); - arg2func::iterator end = map->end(); - for (; it != end; ++it) { - tout << mk_ismt2_pp(it->m_key, m) << "\n---> " << it->m_value->get_name() << "\n"; - }); - SASSERT(map->contains(tmp)); - func_decl * new_f = map->find(tmp); + + bit_vector & bv = it->m_value; + arg2func *& map = m_decl2arg2funcs.insert_if_not_there2(f, 0)->get_data().m_value; + if (!map) { + map = alloc(arg2func, arg2func_hash_proc(bv), arg2func_eq_proc(bv)); + } + + app_ref tmp(m.mk_app(f, num, args), m); + func_decl *& new_f = map->insert_if_not_there2(tmp, 0)->get_data().m_value; + if (!new_f) { + // create fresh symbol + ptr_buffer domain; + unsigned arity = f->get_arity(); + for (unsigned i = 0; i < arity; ++i) { + if (!bv.get(i)) + domain.push_back(f->get_domain(i)); + } + new_f = m.mk_fresh_func_decl(f->get_name(), symbol::null, domain.size(), domain.c_ptr(), f->get_range()); + m.inc_ref(tmp); + m.inc_ref(new_f); + } + ptr_buffer new_args; for (unsigned i = 0; i < num; i++) { if (!bv.get(i)) @@ -470,7 +445,6 @@ struct reduce_args_tactic::imp { void operator()(goal & g, model_converter_ref & mc) { if (g.inconsistent()) return; - m_produce_models = g.models_enabled(); TRACE("reduce_args", g.display(tout);); tactic_report report("reduce-args", g); obj_hashtable non_candidates; @@ -481,10 +455,7 @@ struct reduce_args_tactic::imp { if (decl2args.empty()) return; - ptr_vector arg2funcs; reduce_args_ctx ctx(m_manager); - populate_decl2arg_set(g, decl2args, ctx.m_decl2arg2funcs); - reduce_args_rw rw(*this, decl2args, ctx.m_decl2arg2funcs); unsigned sz = g.size(); @@ -499,7 +470,7 @@ struct reduce_args_tactic::imp { report_tactic_progress(":reduced-funcs", decl2args.size()); - if (m_produce_models) + if (g.models_enabled()) mc = mk_mc(decl2args, ctx.m_decl2arg2funcs); TRACE("reduce_args", g.display(tout); if (mc) mc->display(tout);); diff --git a/src/tactic/smtlogics/qfufbv_tactic.cpp b/src/tactic/smtlogics/qfufbv_tactic.cpp index 421a76cc7..3ee97308a 100644 --- a/src/tactic/smtlogics/qfufbv_tactic.cpp +++ b/src/tactic/smtlogics/qfufbv_tactic.cpp @@ -47,6 +47,7 @@ public: : m_m(m) , m_p(p) , m_use_sat(false) + , m_inc_use_sat(false) {} virtual ~qfufbv_ackr_tactic() { } @@ -85,6 +86,7 @@ public: void updt_params(params_ref const & _p) { qfufbv_tactic_params p(_p); m_use_sat = p.sat_backend(); + m_inc_use_sat = p.inc_sat_backend(); } virtual void collect_statistics(statistics & st) const { @@ -105,12 +107,18 @@ private: params_ref m_p; lackr_stats m_st; bool m_use_sat; + bool m_inc_use_sat; solver* setup_sat() { solver * sat(NULL); if (m_use_sat) { - tactic_ref t = mk_qfbv_tactic(m_m, m_p); - sat = mk_tactic2solver(m_m, t.get(), m_p); + if (m_inc_use_sat) { + sat = mk_inc_sat_solver(m_m, m_p); + } + else { + tactic_ref t = mk_qfbv_tactic(m_m, m_p); + sat = mk_tactic2solver(m_m, t.get(), m_p); + } } else { tactic_ref t = mk_qfaufbv_tactic(m_m, m_p); diff --git a/src/tactic/smtlogics/qfufbv_tactic_params.pyg b/src/tactic/smtlogics/qfufbv_tactic_params.pyg index 6c4bd5b8e..b7640538d 100644 --- a/src/tactic/smtlogics/qfufbv_tactic_params.pyg +++ b/src/tactic/smtlogics/qfufbv_tactic_params.pyg @@ -4,5 +4,6 @@ def_module_params('ackermannization', export=True, params=( ('sat_backend', BOOL, False, 'use SAT rather than SMT in qfufbv_ackr_tactic'), + ('inc_sat_backend', BOOL, False, 'use incremental SAT'), ))