From a2e3788a2095706e663312b418e3c3dad3e30c50 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 18:23:51 +0000 Subject: [PATCH 01/22] [CMake] Refactor the dependency on ``scripts/mk_util.py`` into a list ``Z3_GENERATED_FILE_EXTRA_DEPENDENCIES`` that is used by the ``add_custom_command()`` declarations. This will let us easily change the common dependencies for generating build files in the future. --- CMakeLists.txt | 12 ++++++++++++ contrib/cmake/cmake/z3_add_component.cmake | 9 +++++---- contrib/cmake/src/CMakeLists.txt | 2 +- contrib/cmake/src/api/CMakeLists.txt | 2 +- contrib/cmake/src/api/python/CMakeLists.txt | 4 ++-- contrib/cmake/src/ast/pattern/CMakeLists.txt | 2 +- 6 files changed, 22 insertions(+), 9 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 0e95cb65a..8ed9f5201 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -333,6 +333,18 @@ 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. +# FIXME: We should drop the dependency on ``mk_util.py`` +set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" +) + ################################################################################ # Z3 components, library and executables ################################################################################ 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..36b524f0a 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -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..78837c001 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -24,7 +24,7 @@ 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} COMMENT "Generating ${generated_files}" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} diff --git a/contrib/cmake/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt index 2279be716..05d04e552 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -38,7 +38,7 @@ 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" - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${Z3_GENERATED_FILE_EXTRA_DEPENDENCIES} COMMENT "Generating z3core.py" ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} ) @@ -54,7 +54,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 From 2b64729b2174bbae9d87d28a5e26afebafc6fce0 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 16:54:22 +0000 Subject: [PATCH 02/22] Move ``mk_z3consts_py_internal()`` out of ``mk_util.py`` into ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_consts_files.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_z3consts_py_internal()`` now returns the path to the generated file. The motivation behind this is so that clients of the function know the path to the generated file. Whilst I'm here also reindent ``mk_consts_files.py`` and move some of its code into ``mk_genfile_common.py`` so it can be shared. Also update Z3_GENERATED_FILE_EXTRA_DEPENDENCIES in the CMake build so it knows about ``mk_genfile_common.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- CMakeLists.txt | 1 + scripts/mk_consts_files.py | 50 ++++++-------- scripts/mk_genfile_common.py | 126 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 79 +--------------------- 4 files changed, 152 insertions(+), 104 deletions(-) create mode 100644 scripts/mk_genfile_common.py diff --git a/CMakeLists.txt b/CMakeLists.txt index 8ed9f5201..5cdf06120 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -343,6 +343,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") # FIXME: We should drop the dependency on ``mk_util.py`` set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" ) ################################################################################ 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_genfile_common.py b/scripts/mk_genfile_common.py new file mode 100644 index 000000000..abe10a0d1 --- /dev/null +++ b/scripts/mk_genfile_common.py @@ -0,0 +1,126 @@ +# 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 diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 188dad7a4..da3c6eef9 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 @@ -3026,83 +3027,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 From 8a35f744c7b285d5087107debc22e4274c8f39d8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 19:08:47 +0000 Subject: [PATCH 03/22] Move ``mk_def_file_internal()`` out of ``mk_util.py`` into ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_def_file.py`` to use the code at its new location. Whilst I'm here also reindent ``mk_def_file.py`` and make it use some of the code in ``mk_genfile_common.py`` to avoid code duplication. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_def_file.py | 34 +++++++++++++++++----------------- scripts/mk_genfile_common.py | 33 +++++++++++++++++++++++++++++++++ scripts/mk_util.py | 23 +---------------------- 3 files changed, 51 insertions(+), 39 deletions(-) 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 index abe10a0d1..e0b9bce48 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -124,3 +124,36 @@ def mk_z3consts_py_internal(api_files, output_dir): 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() diff --git a/scripts/mk_util.py b/scripts/mk_util.py index da3c6eef9..f9d639daf 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2913,28 +2913,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) From 404aa2a5a0355db1bbe546be138d3ea0477738cb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 20:29:20 +0000 Subject: [PATCH 04/22] Move ``mk_gparams_register_modules_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_gparams_register_modules_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_gparams_register_modules_internal()`` now returns the path to the generated file. The motivation behind this so that clients of the function know the path to the generated file. Whilst I'm here reindent ``mk_gparams_register_modules_cpp.py`` and the relevant code in ``mk_util.py``. Also remove duplicated code that is now available in ``mk_genfile_common.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 61 ++++++++++++++++++++++ scripts/mk_gparams_register_modules_cpp.py | 46 +++++++--------- scripts/mk_util.py | 59 +++------------------ 3 files changed, 86 insertions(+), 80 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index e0b9bce48..71db2518a 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -157,3 +157,64 @@ def mk_def_file_internal(defname, dll_name, export_header_files): 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 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_util.py b/scripts/mk_util.py index f9d639daf..260625ec4 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2839,61 +2839,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: From f4e98a4fe521e6b3fa4e5cf79fcf66fed859e4b8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 21:56:42 +0000 Subject: [PATCH 05/22] Move ``mk_install_tactic_cpp_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_install_tactic_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_install_tactic_cpp_internal()`` now returns the path the generated file. The motivation behind this is so that clients of the function know the path of the generated file. Whilst I'm here reindent ``mk_install_tactic_cpp.py`` and the relevant code in ``mk_util.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 90 ++++++++++++++++++++++++++++++++ scripts/mk_install_tactic_cpp.py | 47 +++++++---------- scripts/mk_util.py | 80 +++------------------------- 3 files changed, 115 insertions(+), 102 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 71db2518a..05bf21f36 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -218,3 +218,93 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): fout.write('}\n') fout.close() return fullname + +############################################################################### +# Functions/data structures for generating ``install_tactics.cpp`` +############################################################################### + +# FIXME: Remove use of global data structures +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)) + + +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. + """ + global ADD_TACTIC_DATA, ADD_PROBE_DATA + ADD_TACTIC_DATA = [] + ADD_PROBE_DATA = [] + 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 '), 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 '), 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 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_util.py b/scripts/mk_util.py index 260625ec4..b823ba327 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2682,82 +2682,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: From 114e165fadf2f8ae3ffd079dfeb98f3a1445c6cd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 22:21:56 +0000 Subject: [PATCH 06/22] Move ``mk_mem_initializer_cpp_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_mem_initializer_cpp.py`` to use the code at its new location. The interface has been changed slightly so that ``mk_mem_initializer_cpp_internal()`` now returns the path the generated file. The motivation behind this is so that clients of the function know the path of the generated file. Whilst I'm here reindent ``mk_mem_initializer_cpp.py`` and the relevant code in ``mk_util.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 68 +++++++++++++++++++++++++++++++ scripts/mk_mem_initializer_cpp.py | 46 +++++++++------------ scripts/mk_util.py | 65 +++-------------------------- 3 files changed, 93 insertions(+), 86 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 05bf21f36..4c7565dac 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -308,3 +308,71 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): 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 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_util.py b/scripts/mk_util.py index b823ba327..913914fef 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2700,67 +2700,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: From 8840e5a00f52dd087fb1d3253efdfc927052991a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 8 Mar 2016 23:21:09 +0000 Subject: [PATCH 07/22] Move ``mk_pat_db_internal()`` from ``mk_util.py`` to ``mk_genfile_common.py`` and adapt ``mk_util.py`` and ``mk_pat_db.py`` to use the code at its new location. Whilst I'm here reindent ``mk_mem_initializer_cpp.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. --- scripts/mk_genfile_common.py | 15 +++++++++++++++ scripts/mk_pat_db.py | 31 +++++++++++++------------------ scripts/mk_util.py | 12 ++---------- 3 files changed, 30 insertions(+), 28 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 4c7565dac..943d4052a 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -376,3 +376,18 @@ def mk_mem_initializer_cpp_internal(component_src_dirs, path): 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') 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 913914fef..47afa2251 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2621,17 +2621,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(): From 87e99cd7342ec293f9ec1f39b57ebed817710232 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 00:42:20 +0000 Subject: [PATCH 08/22] Move the code for generating ``*.hpp`` files from ``*.pyg`` from ``mk_util.py`` to ``mk_genfile_common.py``. A new function ``mk_hpp_from_pyg()`` has been added which provides a more sensible interface (hides the nasty ``exec()`` stuff) to create the ``*.hpp`` files from ``*.pyg`` files. Both ``mk_util.py`` and ``pyg2hpp.py`` have been modified to use the new interface. Whilst I'm here reindent ``pyg2hpp.py``. The purpose of this change is to have Python code common to the Python and CMake build systems separate from Python code that is only used for the Python build system. I've tested this change by making sure that the all the ``*.hpp`` files generated from ``*.pyg`` files match the files generated before this change. --- scripts/mk_genfile_common.py | 129 +++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 104 +--------------------------- scripts/pyg2hpp.py | 42 +++++------- 3 files changed, 150 insertions(+), 125 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 943d4052a..8b4b26313 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -391,3 +391,132 @@ def mk_pat_db_internal(inputFilePath, outputFilePath): 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_util.py b/scripts/mk_util.py index 47afa2251..1c7ee4ab5 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2499,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": @@ -2607,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 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:])) From b3f6a3c4af0d157140a1a537927b9c086bef9b22 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 01:20:08 +0000 Subject: [PATCH 09/22] Remove use of global data structures in ``mk_install_tactic_cpp_internal()`` --- scripts/mk_genfile_common.py | 29 +++++++++++++---------------- 1 file changed, 13 insertions(+), 16 deletions(-) diff --git a/scripts/mk_genfile_common.py b/scripts/mk_genfile_common.py index 8b4b26313..790ce7205 100644 --- a/scripts/mk_genfile_common.py +++ b/scripts/mk_genfile_common.py @@ -223,19 +223,6 @@ def mk_gparams_register_modules_internal(component_src_dirs, path): # Functions/data structures for generating ``install_tactics.cpp`` ############################################################################### -# FIXME: Remove use of global data structures -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)) - - def mk_install_tactic_cpp_internal(component_src_dirs, path): """ Generate a ``install_tactics.cpp`` file in the directory ``path``. @@ -251,9 +238,19 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): ``component_src_dirs`` The procedure looks for ``ADD_TACTIC`` commands in the ``.h`` and ``.hpp`` files of these components. """ - global ADD_TACTIC_DATA, ADD_PROBE_DATA 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') @@ -275,7 +272,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), globals()) + exec(line.strip('\n '), exec_globals) except Exception as e: _logger.error("Failed processing ADD_TACTIC command at '{}'\n{}".format( fullname, line)) @@ -285,7 +282,7 @@ def mk_install_tactic_cpp_internal(component_src_dirs, path): added_include = True fout.write('#include"%s"\n' % h_file) try: - exec(line.strip('\n '), globals()) + exec(line.strip('\n '), exec_globals) except Exception as e: _logger.error("Failed processing ADD_PROBE command at '{}'\n{}".format( fullname, line)) From 98244ac9a97c4f5e641024657d0a4cd82e0ff9ab Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 01:26:06 +0000 Subject: [PATCH 10/22] [CMake] Remove global "generated file" dependency on ``mk_util.py``. Most file generation scripts don't depend on it anymore. The exceptions are uses of ``update_api.py``. An explicit dependency has been added here and a ``FIXME`` has been left to indicate that this should be removed once ``update_api.py`` is completly independent of ``mk_util.py``. --- CMakeLists.txt | 2 -- contrib/cmake/src/api/CMakeLists.txt | 2 ++ contrib/cmake/src/api/python/CMakeLists.txt | 2 ++ 3 files changed, 4 insertions(+), 2 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 5cdf06120..0204a8a44 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -340,9 +340,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") ################################################################################ # 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. -# FIXME: We should drop the dependency on ``mk_util.py`` set(Z3_GENERATED_FILE_EXTRA_DEPENDENCIES - "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" "${CMAKE_SOURCE_DIR}/scripts/mk_genfile_common.py" ) diff --git a/contrib/cmake/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt index 78837c001..8e796168f 100644 --- a/contrib/cmake/src/api/CMakeLists.txt +++ b/contrib/cmake/src/api/CMakeLists.txt @@ -26,6 +26,8 @@ add_custom_command(OUTPUT ${generated_files} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.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 05d04e552..6e4096057 100644 --- a/contrib/cmake/src/api/python/CMakeLists.txt +++ b/contrib/cmake/src/api/python/CMakeLists.txt @@ -39,6 +39,8 @@ add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" ${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} ) From 04ca873abb03462bd1250133dcea6683caeb422e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 9 Mar 2016 14:09:29 +0000 Subject: [PATCH 11/22] [CMake] Provide a way to customise the install directories used for executables, include files and libraries. We use ``GNUInstallDirs.cmake`` which ships with CMake to do the difficult work of setting a sensible default and setting up CMake cache variables. These can be overriden when running CMake by setting the ``CMAKE_INSTALL_BINDIR``, ``CMAKE_INSTALL_INCLUDEDIR`` and ``CMAKE_INSTALL_LIBDIR`` cache variables. --- CMakeLists.txt | 7 ++++--- README-CMake.md | 10 +++++++--- contrib/cmake/src/CMakeLists.txt | 6 +++--- contrib/cmake/src/shell/CMakeLists.txt | 2 +- 4 files changed, 15 insertions(+), 10 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3cc29780d..97c8b1862 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 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/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 6708f505e..2bf7442ab 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) 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}" ) From 0b1b5a4328fece4af9e5213ff7e2b244c356b1bf Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 10 Mar 2016 09:03:24 +0000 Subject: [PATCH 12/22] fix VS x64 warning --- src/muz/pdr/pdr_sym_mux.cpp | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) 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); From d6c3260db7a18cdcb3092eea7f2b3493c5426376 Mon Sep 17 00:00:00 2001 From: Nuno Lopes Date: Thu, 10 Mar 2016 10:15:09 +0000 Subject: [PATCH 13/22] reduce_args_tactic: make it aware that 'a + const' may be a unique value in bv theory it allows us to remove UFs that are of the form f(a + 1), f(a + 2), etc.. --- src/tactic/core/reduce_args_tactic.cpp | 159 ++++++++++--------------- 1 file changed, 65 insertions(+), 94 deletions(-) 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);); From 6a2f27476ca579b4b3efe25e93c83067fe0967cc Mon Sep 17 00:00:00 2001 From: hongjiawu Date: Thu, 10 Mar 2016 18:10:59 +0100 Subject: [PATCH 14/22] Update README.md --- README.md | 2 ++ 1 file changed, 2 insertions(+) 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]. From 2f8465552cd05e7f8fd66885c01f40bf9f9b8094 Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Thu, 18 Feb 2016 17:08:54 +0000 Subject: [PATCH 15/22] additional logging --- src/ackermannization/ackermannize_bv_tactic.cpp | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) 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()); } From a2140085d6197716fe69d94ed78ce5c5715fa8e2 Mon Sep 17 00:00:00 2001 From: mikolas Date: Fri, 26 Feb 2016 13:02:59 +0000 Subject: [PATCH 16/22] In lazy ackermannization, collect all conflicting terms in one iteration. --- .../lackr_model_constructor.cpp | 35 ++++++++++++------- 1 file changed, 22 insertions(+), 13 deletions(-) diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 09034fa36..3ff7d2c10 100644 --- a/src/ackermannization/lackr_model_constructor.cpp +++ b/src/ackermannization/lackr_model_constructor.cpp @@ -60,15 +60,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; } @@ -144,6 +146,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 +155,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 +182,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; } From ae9f369574e6a94d0d008a38c8205160fe5b3f8b Mon Sep 17 00:00:00 2001 From: Mikolas Janota Date: Fri, 26 Feb 2016 14:48:00 +0000 Subject: [PATCH 17/22] Fix in lackr_model_constructor. --- src/ackermannization/lackr_model_constructor.cpp | 10 ++++++++-- 1 file changed, 8 insertions(+), 2 deletions(-) diff --git a/src/ackermannization/lackr_model_constructor.cpp b/src/ackermannization/lackr_model_constructor.cpp index 3ff7d2c10..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(); @@ -136,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; }; @@ -221,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'; ); From 419e2c4899a55ea8e698a00cd6abff5638de7032 Mon Sep 17 00:00:00 2001 From: mikolas Date: Mon, 29 Feb 2016 11:39:52 +0000 Subject: [PATCH 18/22] Inc sat for ackr. --- src/tactic/smtlogics/qfufbv_tactic.cpp | 12 ++++++++++-- src/tactic/smtlogics/qfufbv_tactic_params.pyg | 1 + 2 files changed, 11 insertions(+), 2 deletions(-) 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'), )) From 9dd53c091a716abd35248a648be2c2200572b154 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Mar 2016 12:02:49 +0000 Subject: [PATCH 19/22] guard on m_preprocess in inc_sat_solver --- src/sat/sat_solver/inc_sat_solver.cpp | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) 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"; From b5279d1da89ba77d8dddbed6927491cc1416b970 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Mar 2016 12:35:41 +0000 Subject: [PATCH 20/22] Bugfix for fp.to_ieee_bv. Fixes #507. --- src/ast/fpa_decl_plugin.cpp | 10 +++++----- src/ast/rewriter/fpa_rewriter.cpp | 6 ++---- 2 files changed, 7 insertions(+), 9 deletions(-) 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); From 3e61ee233154121d113790445f2c9bb531fea738 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Mar 2016 12:51:37 +0000 Subject: [PATCH 21/22] disabled "hardware interpretation" of fp.min/fp.max because the unspecified, standard-compliant behaviour is cheap anyways. --- src/ast/fpa/fpa2bv_converter.cpp | 108 ++++++++++++++----------------- 1 file changed, 50 insertions(+), 58 deletions(-) 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; } From badf9e6e67ccfe97de0e725c706f040345ab3eb5 Mon Sep 17 00:00:00 2001 From: "Christoph M. Wintersteiger" Date: Fri, 11 Mar 2016 14:05:32 +0000 Subject: [PATCH 22/22] whitespace --- src/ast/fpa/fpa2bv_rewriter.cpp | 72 ++++++++++++++++----------------- 1 file changed, 36 insertions(+), 36 deletions(-) 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; }