From 9558dc14fb88bcee3997cba6f42e0b5377861edb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 26 Feb 2016 18:24:57 +0000 Subject: [PATCH 01/42] Refactor ``exec_pyg_scripts()`` so that it is usable externally via a new ``pyg2hpp.py`` script. This will allow other build systems to take ``pyg`` files and generate the corresponding ``hpp`` files. --- scripts/mk_util.py | 14 +++++++------- scripts/pyg2hpp.py | 42 ++++++++++++++++++++++++++++++++++++++++++ 2 files changed, 49 insertions(+), 7 deletions(-) create mode 100755 scripts/pyg2hpp.py diff --git a/scripts/mk_util.py b/scripts/mk_util.py index a02a9b40fee..dbc83353f89 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2488,10 +2488,10 @@ def mk_auto_src(): STRING = 3 SYMBOL = 4 UINT_MAX = 4294967295 -CURR_PYG = None +CURRENT_PYG_HPP_DEST_DIR = None -def get_curr_pyg(): - return CURR_PYG +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' } @@ -2524,8 +2524,8 @@ def to_c_method(s): return s.replace('.', '_') def def_module_params(module_name, export, params, class_name=None, description=None): - pyg = get_curr_pyg() - dirname = os.path.split(get_curr_pyg())[0] + 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) @@ -2590,12 +2590,12 @@ def _execfile(file, globals=globals(), locals=locals()): # Execute python auxiliary scripts that generate extra code for Z3. def exec_pyg_scripts(): - global CURR_PYG + 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) - CURR_PYG = script + CURRENT_PYG_HPP_DEST_DIR = root _execfile(script, PYG_GLOBALS) # TODO: delete after src/ast/pattern/expr_pattern_match diff --git a/scripts/pyg2hpp.py b/scripts/pyg2hpp.py new file mode 100755 index 00000000000..f1ada2b84ae --- /dev/null +++ b/scripts/pyg2hpp.py @@ -0,0 +1,42 @@ +#!/usr/bin/env python +""" +Reads a pyg file and emits the corresponding +C++ header file into the specified destination +directory. +""" +import mk_util +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) + + 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 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 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + From ef5817946279cbfaacbd137e8ce061964914fe2d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 27 Feb 2016 22:31:19 +0000 Subject: [PATCH 02/42] Refactor ``mk_pat_db()`` so that it is usable externally via a new function ``mk_pat_db_internal()`` which is called by a new ``mk_pat_db.py`` script. This will allow other build systems to generate the ``database.h`` file. --- scripts/mk_pat_db.py | 34 ++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 21 ++++++++++++--------- 2 files changed, 46 insertions(+), 9 deletions(-) create mode 100755 scripts/mk_pat_db.py diff --git a/scripts/mk_pat_db.py b/scripts/mk_pat_db.py new file mode 100755 index 00000000000..3f2e7c50775 --- /dev/null +++ b/scripts/mk_pat_db.py @@ -0,0 +1,34 @@ +#!/usr/bin/env python +""" +Reads a pattern database and generates the corresponding +header file. +""" +import mk_util +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) + + 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 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index dbc83353f89..77a8df0e2ea 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2602,16 +2602,19 @@ def exec_pyg_scripts(): # database.smt ==> database.h def mk_pat_db(): c = get_component(PATTERN_COMPONENT) - fin = open(os.path.join(c.src_dir, 'database.smt2'), 'r') - fout = open(os.path.join(c.src_dir, 'database.h'), 'w') - fout.write('static char const g_pattern_database[] =\n') - for line in fin: - fout.write('"%s\\n"\n' % line.strip('\n')) - fout.write(';\n') - fin.close() - fout.close() + 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') if VERBOSE: - print("Generated '%s'" % os.path.join(c.src_dir, 'database.h')) + print("Generated '%s'" % outputFilePath) # Update version numbers def update_version(): From a13438818f31bc8fc5dae0cdefca47c6dea6c884 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Feb 2016 09:55:41 +0000 Subject: [PATCH 03/42] Refactor ``mk_install_tactic_cpp()`` so that it is usable externally via a new function ``mk_install_tactic_cpp_internal()`` which is called by a new ``mk_install_tactic_cpp.py`` script. This will allow other build systems to generate the ``install_tactic.cpp`` files. --- scripts/mk_install_tactic_cpp.py | 47 ++++++++++++++++++++++++++++++++ scripts/mk_util.py | 14 +++++++--- 2 files changed, 57 insertions(+), 4 deletions(-) create mode 100755 scripts/mk_install_tactic_cpp.py diff --git a/scripts/mk_install_tactic_cpp.py b/scripts/mk_install_tactic_cpp.py new file mode 100755 index 00000000000..f8323d73149 --- /dev/null +++ b/scripts/mk_install_tactic_cpp.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python +""" +Determines the available tactics +in header files in the list of source directions +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 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) + + if check_dir(pargs.destination_dir) != 0: + return 1 + + for source_dir in pargs.source_dirs: + if check_dir(source_dir) != 0: + return 1 + + mk_util.mk_install_tactic_cpp_internal(pargs.source_dirs, pargs.destination_dir) + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 77a8df0e2ea..9060d37fc1a 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2677,6 +2677,13 @@ def ADD_PROBE(name, descr, cmd): # 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 = [] @@ -2688,12 +2695,11 @@ def mk_install_tactic_cpp(cnames, path): fout.write('#include"cmd_context.h"\n') tactic_pat = re.compile('[ \t]*ADD_TACTIC\(.*\)') probe_pat = re.compile('[ \t]*ADD_PROBE\(.*\)') - for cname in cnames: - c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) + 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(c.src_dir, h_file), 'r') + fin = open(os.path.join(component_src_dir, h_file), 'r') for line in fin: if tactic_pat.match(line): if not added_include: From 2f7f02260522d00ca8b091f905e3e4a548b748e5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Feb 2016 13:31:23 +0000 Subject: [PATCH 04/42] Refactor ``mk_mem_initializer_cpp()`` so that it is usable externally via a new function ``mk_mem_initializer_cpp_internal()`` which is called by a new ``mk_mem_initializer_cpp.py`` script. This will allow other build systems to generate the ``mem_initializer.cpp`` files. --- scripts/mk_mem_initializer_cpp.py | 48 +++++++++++++++++++++++++++++++ scripts/mk_util.py | 14 ++++++--- 2 files changed, 58 insertions(+), 4 deletions(-) create mode 100755 scripts/mk_mem_initializer_cpp.py diff --git a/scripts/mk_mem_initializer_cpp.py b/scripts/mk_mem_initializer_cpp.py new file mode 100755 index 00000000000..c8b68049f1a --- /dev/null +++ b/scripts/mk_mem_initializer_cpp.py @@ -0,0 +1,48 @@ +#!/usr/bin/env python +""" +Scans the source directories for +memory initializers and finalizers and +emits and implementation of +``void mem_initialize()`` and +``void mem_finalize()`` into ``mem_initializer.cpp`` +in the destination directory. +""" +import mk_util +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) + + if check_dir(pargs.destination_dir) != 0: + return 1 + + for source_dir in pargs.source_dirs: + if check_dir(source_dir) != 0: + return 1 + + mk_util.mk_mem_initializer_cpp_internal(pargs.source_dirs, pargs.destination_dir) + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 9060d37fc1a..ef652eab30f 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2752,6 +2752,13 @@ def mk_all_install_tactic_cpps(): # 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') @@ -2761,12 +2768,11 @@ def mk_mem_initializer_cpp(cnames, path): # ADD_INITIALIZER with priority initializer_prio_pat = re.compile('[ \t]*ADD_INITIALIZER\(\'([^\']*)\',[ \t]*(-?[0-9]*)\)') finalizer_pat = re.compile('[ \t]*ADD_FINALIZER\(\'([^\']*)\'\)') - for cname in cnames: - c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) + 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(c.src_dir, h_file), 'r') + fin = open(os.path.join(component_src_dir, h_file), 'r') for line in fin: m = initializer_pat.match(line) if m: From 2b3fe3d02c6c215faad8ca309895bc2c90e406bd Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Feb 2016 16:27:05 +0000 Subject: [PATCH 05/42] Refactor ``mk_gparams_register_modules()`` so that it is usable externally via a new function ``mk_gparams_register_modules_internal()`` which is called by a new ``mk_gparams_register_modules_cpp.py`` script. This will allow other build systems to generate the ``gparams_register_modules.cpp`` files. --- scripts/mk_gparams_register_modules_cpp.py | 47 ++++++++++++++++++++++ scripts/mk_util.py | 16 +++++--- 2 files changed, 58 insertions(+), 5 deletions(-) create mode 100755 scripts/mk_gparams_register_modules_cpp.py diff --git a/scripts/mk_gparams_register_modules_cpp.py b/scripts/mk_gparams_register_modules_cpp.py new file mode 100755 index 00000000000..1c7e221ba41 --- /dev/null +++ b/scripts/mk_gparams_register_modules_cpp.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python +""" +Determines the available global parameters +in header files in the list of source directions +and generates a ``gparams_register_modules.cpp`` file in +the destination directory that defines a function +``void gparams_register_modules()``. +""" +import mk_util +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) + + if check_dir(pargs.destination_dir) != 0: + return 1 + + for source_dir in pargs.source_dirs: + if check_dir(source_dir) != 0: + return 1 + + mk_util.mk_gparams_register_modules_internal(pargs.source_dirs, pargs.destination_dir) + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index ef652eab30f..53a9b24fe69 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2817,11 +2817,18 @@ def mk_all_mem_initializer_cpps(): cnames.append(c.name) mk_mem_initializer_cpp(cnames, c.src_dir) -# Generate an mem_initializer.cpp at path. +# 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 = [] @@ -2832,12 +2839,11 @@ def mk_gparams_register_modules(cnames, path): 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 cname in cnames: - c = get_component(cname) - h_files = filter(lambda f: f.endswith('.h') or f.endswith('.hpp'), os.listdir(c.src_dir)) + 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(c.src_dir, h_file), 'r') + fin = open(os.path.join(component_src_dir, h_file), 'r') for line in fin: m = reg_pat.match(line) if m: From db34baa979cc63955b4a9a51a853d5337dd65b3f Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sun, 28 Feb 2016 21:45:35 +0000 Subject: [PATCH 06/42] Partially refactor the code in ``update_api.py`` so that it can be used as a script for other build systems and is callable via a new ``generate_files()`` function from ``mk_util.py``. This removes the horrible ``_execfile()`` hack that was previously in ``mk_util.py``. Unfortunately lots of bad code is still in ``update_api.py`` but fixing all of its problems is too much work right now. --- scripts/mk_util.py | 23 ++- scripts/update_api.py | 367 ++++++++++++++++++++++++++---------------- 2 files changed, 248 insertions(+), 142 deletions(-) mode change 100644 => 100755 scripts/update_api.py diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 53a9b24fe69..91952823250 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2957,7 +2957,28 @@ def mk_bindings(api_files): if is_java_enabled(): check_java() mk_z3consts_java(api_files) - _execfile(os.path.join('scripts', 'update_api.py'), g) # HACK + # Generate some of the bindings and "api" module files + import update_api + dotnet_output_dir = None + if is_dotnet_enabled(): + dotnet_output_dir = get_component('dotnet').src_dir + java_output_dir = None + java_package_name = None + if is_java_enabled(): + java_output_dir = get_component('java').src_dir + java_package_name = get_component('java').package_name + ml_output_dir = None + if is_ml_enabled(): + ml_output_dir = get_component('ml').src_dir + # Get the update_api module to do the work for us + update_api.generate_files(api_files=new_api_files, + api_output_dir=get_component('api').src_dir, + z3py_output_dir=get_z3py_dir(), + dotnet_output_dir=dotnet_output_dir, + java_output_dir=java_output_dir, + java_package_name=java_package_name, + ml_output_dir=ml_output_dir + ) cp_z3py_to_build() if is_ml_enabled(): check_ml() diff --git a/scripts/update_api.py b/scripts/update_api.py old mode 100644 new mode 100755 index badd960ccc6..8a389752f67 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,113 +1,35 @@ - ############################################ # Copyright (c) 2012 Microsoft Corporation -# -# Scripts for generating Makefiles and Visual +# +# Scripts for generating Makefiles and Visual # Studio project files. # # Author: Leonardo de Moura (leonardo) ############################################ -from mk_util import * -from mk_exception import * +""" +This script generates the ``api_log_macros.h``, +``api_log_macros.cpp`` and ``api_commands.cpp`` +files for the "api" module based on parsing +several API header files. It can also optionally +emit some of the files required for Z3's different +language bindings. +""" +import mk_util +import mk_exception +import argparse +import logging +import re +import os +import sys ########################################################## # TODO: rewrite this file without using global variables. # This file is a big HACK. # It started as small simple script. # Now, it is too big, and is invoked from mk_make.py -# The communication uses # ########################################################## -# -# Generate logging support and bindings -# -api_dir = get_component('api').src_dir -dotnet_dir = get_component('dotnet').src_dir - -log_h = open(os.path.join(api_dir, 'api_log_macros.h'), 'w') -log_c = open(os.path.join(api_dir, 'api_log_macros.cpp'), 'w') -exe_c = open(os.path.join(api_dir, 'api_commands.cpp'), 'w') -core_py = open(os.path.join(get_z3py_dir(), 'z3core.py'), 'w') -dotnet_fileout = os.path.join(dotnet_dir, 'Native.cs') -## -log_h.write('// Automatically generated file\n') -log_h.write('#include\"z3.h\"\n') -log_h.write('#ifdef __GNUC__\n') -log_h.write('#define _Z3_UNUSED __attribute__((unused))\n') -log_h.write('#else\n') -log_h.write('#define _Z3_UNUSED\n') -log_h.write('#endif\n') - -## -log_c.write('// Automatically generated file\n') -log_c.write('#include\n') -log_c.write('#include\"z3.h\"\n') -log_c.write('#include\"api_log_macros.h\"\n') -log_c.write('#include\"z3_logger.h\"\n') -## -exe_c.write('// Automatically generated file\n') -exe_c.write('#include\"z3.h\"\n') -exe_c.write('#include\"z3_replayer.h\"\n') -## -log_h.write('extern std::ostream * g_z3_log;\n') -log_h.write('extern bool g_z3_log_enabled;\n') -log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n') -log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n') -log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') -log_h.write('void _Z3_append_log(char const * msg);\n') -## -exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') -## -core_py.write('# Automatically generated file\n') -core_py.write('import sys, os\n') -core_py.write('import ctypes\n') -core_py.write('from z3types import *\n') -core_py.write('from z3consts import *\n') -core_py.write(""" -_lib = None -def lib(): - global _lib - if _lib == None: - _dir = os.path.dirname(os.path.abspath(__file__)) - for ext in ['dll', 'so', 'dylib']: - try: - init('libz3.%s' % ext) - break - except: - pass - try: - init(os.path.join(_dir, 'libz3.%s' % ext)) - break - except: - pass - if _lib == None: - raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") - return _lib - -def _to_ascii(s): - if isinstance(s, str): - return s.encode('ascii') - else: - return s - -if sys.version < '3': - def _to_pystr(s): - return s -else: - def _to_pystr(s): - if s != None: - enc = sys.stdout.encoding - if enc != None: return s.decode(enc) - else: return s.decode('ascii') - else: - return "" - -def init(PATH): - global _lib - _lib = ctypes.CDLL(PATH) -""") - IN = 0 OUT = 1 INOUT = 2 @@ -176,10 +98,9 @@ def def_Type(var, c_type, py_type): Type2PyStr[next_type_id] = py_type next_type_id = next_type_id + 1 -def def_Types(): - import re +def def_Types(api_files): pat1 = re.compile(" *def_Type\(\'(.*)\',[^\']*\'(.*)\',[^\']*\'(.*)\'\)[ \t]*") - for api_file in API_FILES: + for api_file in api_files: api = open(api_file, 'r') for line in api: m = pat1.match(line) @@ -418,10 +339,8 @@ def reg_dotnet(name, result, params): global _dotnet_decls _dotnet_decls.append((name, result, params)) -def mk_dotnet(): +def mk_dotnet(dotnet): global Type2Str - global dotnet_fileout - dotnet = open(dotnet_fileout, 'w') dotnet.write('// Automatically generated file\n') dotnet.write('using System;\n') dotnet.write('using System.Collections.Generic;\n') @@ -468,10 +387,8 @@ def mk_dotnet(): NULLWrapped = [ 'Z3_mk_context', 'Z3_mk_context_rc' ] Unwrapped = [ 'Z3_del_context', 'Z3_get_error_code' ] -def mk_dotnet_wrappers(): +def mk_dotnet_wrappers(dotnet): global Type2Str - global dotnet_fileout - dotnet = open(dotnet_fileout, 'a') dotnet.write("\n") dotnet.write(" public static void Z3_set_error_handler(Z3_context a0, Z3_error_handler a1) {\n") dotnet.write(" LIB.Z3_set_error_handler(a0, a1);\n") @@ -556,16 +473,13 @@ def java_array_element_type(p): else: return 'jlong' -def mk_java(): - if not is_java_enabled(): - return - java_dir = get_component('java').src_dir +def mk_java(java_dir, package_name): java_nativef = os.path.join(java_dir, 'Native.java') java_wrapperf = os.path.join(java_dir, 'Native.cpp') java_native = open(java_nativef, 'w') java_native.write('// Automatically generated file\n') - java_native.write('package %s;\n' % get_component('java').package_name) - java_native.write('import %s.enumerations.*;\n' % get_component('java').package_name) + java_native.write('package %s;\n' % package_name) + java_native.write('import %s.enumerations.*;\n' % package_name) java_native.write('public final class Native {\n') java_native.write(' public static class IntPtr { public int value; }\n') java_native.write(' public static class LongPtr { public long value; }\n') @@ -638,7 +552,7 @@ def mk_java(): java_native.write(' }\n\n') java_native.write('}\n') java_wrapper = open(java_wrapperf, 'w') - pkg_str = get_component('java').package_name.replace('.', '_') + pkg_str = package_name.replace('.', '_') java_wrapper.write('// Automatically generated file\n') java_wrapper.write('#ifdef _CYGWIN\n') java_wrapper.write('typedef long long __int64;\n') @@ -801,7 +715,7 @@ def mk_java(): java_wrapper.write('#ifdef __cplusplus\n') java_wrapper.write('}\n') java_wrapper.write('#endif\n') - if is_verbose(): + if mk_util.is_verbose(): print("Generated '%s'" % java_nativef) def mk_log_header(file, name, params): @@ -1076,7 +990,7 @@ def def_API(name, result, params): mk_log_result_macro(log_h, name, result, params) next_id = next_id + 1 -def mk_bindings(): +def mk_bindings(exe_c): exe_c.write("void register_z3_replayer_cmds(z3_replayer & in) {\n") for key, val in API2Id.items(): exe_c.write(" in.register_cmd(%s, exec_%s, \"%s\");\n" % (key, val, val)) @@ -1160,11 +1074,8 @@ def ml_set_wrap(t, d, n): ts = type2str(t) return d + ' = caml_alloc_custom(&default_custom_ops, sizeof(' + ts + '), 0, 1); memcpy( Data_custom_val(' + d + '), &' + n + ', sizeof(' + ts + '));' -def mk_ml(): +def mk_ml(ml_dir): global Type2Str - if not is_ml_enabled(): - return - ml_dir = get_component('ml').src_dir ml_nativef = os.path.join(ml_dir, 'z3native.ml') ml_nativefi = os.path.join(ml_dir, 'z3native.mli') ml_wrapperf = os.path.join(ml_dir, 'z3native_stubs.c') @@ -1534,14 +1445,14 @@ def mk_ml(): ml_wrapper.write('#ifdef __cplusplus\n') ml_wrapper.write('}\n') ml_wrapper.write('#endif\n') - if is_verbose(): + if mk_util.is_verbose(): print ('Generated "%s"' % ml_nativef) # Collect API(...) commands from -def def_APIs(): +def def_APIs(api_files): pat1 = re.compile(" *def_API.*") pat2 = re.compile(" *extra_API.*") - for api_file in API_FILES: + for api_file in api_files: api = open(api_file, 'r') for line in api: line = line.strip('\r\n\t ') @@ -1553,24 +1464,198 @@ def def_APIs(): if m: eval(line) except Exception: - raise MKException("Failed to process API definition: %s" % line) -def_Types() -def_APIs() -mk_bindings() -mk_py_wrappers() -mk_dotnet() -mk_dotnet_wrappers() -mk_java() -mk_ml() - -log_h.close() -log_c.close() -exe_c.close() -core_py.close() - -if is_verbose(): - print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.h')) - print("Generated '%s'" % os.path.join(api_dir, 'api_log_macros.cpp')) - print("Generated '%s'" % os.path.join(api_dir, 'api_commands.cpp')) - print("Generated '%s'" % os.path.join(get_z3py_dir(), 'z3core.py')) - print("Generated '%s'" % os.path.join(dotnet_dir, 'Native.cs')) + raise mk_exec_header.MKException("Failed to process API definition: %s" % line) + +def write_log_h_preamble(log_h): + log_h.write('// Automatically generated file\n') + log_h.write('#include\"z3.h\"\n') + log_h.write('#ifdef __GNUC__\n') + log_h.write('#define _Z3_UNUSED __attribute__((unused))\n') + log_h.write('#else\n') + log_h.write('#define _Z3_UNUSED\n') + log_h.write('#endif\n') + # + log_h.write('extern std::ostream * g_z3_log;\n') + log_h.write('extern bool g_z3_log_enabled;\n') + log_h.write('class z3_log_ctx { bool m_prev; public: z3_log_ctx():m_prev(g_z3_log_enabled) { g_z3_log_enabled = false; } ~z3_log_ctx() { g_z3_log_enabled = m_prev; } bool enabled() const { return m_prev; } };\n') + log_h.write('inline void SetR(void * obj) { *g_z3_log << "= " << obj << "\\n"; }\ninline void SetO(void * obj, unsigned pos) { *g_z3_log << "* " << obj << " " << pos << "\\n"; } \ninline void SetAO(void * obj, unsigned pos, unsigned idx) { *g_z3_log << "@ " << obj << " " << pos << " " << idx << "\\n"; }\n') + log_h.write('#define RETURN_Z3(Z3RES) if (_LOG_CTX.enabled()) { SetR(Z3RES); } return Z3RES\n') + log_h.write('void _Z3_append_log(char const * msg);\n') + + +def write_log_c_preamble(log_c): + log_c.write('// Automatically generated file\n') + log_c.write('#include\n') + log_c.write('#include\"z3.h\"\n') + log_c.write('#include\"api_log_macros.h\"\n') + log_c.write('#include\"z3_logger.h\"\n') + +def write_exe_c_preamble(exe_c): + exe_c.write('// Automatically generated file\n') + exe_c.write('#include\"z3.h\"\n') + exe_c.write('#include\"z3_replayer.h\"\n') + # + exe_c.write('void Z3_replayer_error_handler(Z3_context ctx, Z3_error_code c) { printf("[REPLAYER ERROR HANDLER]: %s\\n", Z3_get_error_msg(ctx, c)); }\n') + +def write_core_py_preamble(core_py): + core_py.write('# Automatically generated file\n') + core_py.write('import sys, os\n') + core_py.write('import ctypes\n') + core_py.write('from z3types import *\n') + core_py.write('from z3consts import *\n') + core_py.write( +""" +_lib = None +def lib(): + global _lib + if _lib == None: + _dir = os.path.dirname(os.path.abspath(__file__)) + for ext in ['dll', 'so', 'dylib']: + try: + init('libz3.%s' % ext) + break + except: + pass + try: + init(os.path.join(_dir, 'libz3.%s' % ext)) + break + except: + pass + if _lib == None: + raise Z3Exception("init(Z3_LIBRARY_PATH) must be invoked before using Z3-python") + return _lib + +def _to_ascii(s): + if isinstance(s, str): + return s.encode('ascii') + else: + return s + +if sys.version < '3': + def _to_pystr(s): + return s +else: + def _to_pystr(s): + if s != None: + enc = sys.stdout.encoding + if enc != None: return s.decode(enc) + else: return s.decode('ascii') + else: + return "" + +def init(PATH): + global _lib + _lib = ctypes.CDLL(PATH) +""" + ) + +log_h = None +log_c = None +exe_c = None +core_py = None + +# FIXME: This can only be called once from this module +# due to its use of global state! +def generate_files(api_files, + api_output_dir, + z3py_output_dir=None, + dotnet_output_dir=None, + java_output_dir=None, + java_package_name=None, + ml_output_dir=None): + """ + Scan the api files in ``api_files`` and emit + the relevant ``api_*.h`` and ``api_*.cpp`` files + for the api modules into the ``api_output_dir`` + directory. + + For the remaining arguments, if said argument is + not ``None`` the relevant files for that language + binding will be emitted to the specified directory. + """ + # FIXME: These should not be global + global log_h, log_c, exe_c, core_py + assert isinstance(api_files, list) + assert os.path.isdir(api_output_dir) + + # Hack to avoid emitting z3core.py when we don't want it + def mk_z3coredotpy_file_object(): + if z3py_output_dir: + assert os.path.isdir(z3py_output_dir) + return open(os.path.join(z3py_output_dir, 'z3core.py'), 'w') + else: + # Return a file that we can write to without caring + import tempfile + return tempfile.TemporaryFile(mode='w') + + with open(os.path.join(api_output_dir, 'api_log_macros.h'), 'w') as log_h: + with open(os.path.join(api_output_dir, 'api_log_macros.cpp'), 'w') as log_c: + with open(os.path.join(api_output_dir, 'api_commands.cpp'), 'w') as exe_c: + with mk_z3coredotpy_file_object() as core_py: + # Write preambles + write_log_h_preamble(log_h) + write_log_c_preamble(log_c) + write_exe_c_preamble(exe_c) + write_core_py_preamble(core_py) + + # FIXME: these functions are awful + def_Types(api_files) + def_APIs(api_files) + mk_bindings(exe_c) + mk_py_wrappers() + + if mk_util.is_verbose(): + print("Generated '{}'".format(log_h.name)) + print("Generated '{}'".format(log_c.name)) + print("Generated '{}'".format(exe_c.name)) + print("Generated '{}'".format(core_py.name)) + + if dotnet_output_dir: + with open(os.path.join(dotnet_output_dir, 'Native.cs'), 'w') as dotnet_file: + mk_dotnet(dotnet_file) + mk_dotnet_wrappers(dotnet_file) + if mk_util.is_verbose(): + print("Generated '{}'".format(dotnet_file.name)) + + if java_output_dir: + mk_java(java_output_dir, java_package_name) + if ml_output_dir: + mk_ml(ml_output_dir) + +def main(args): + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument("api_output_dir", help="Directory to emit files for api module") + parser.add_argument("api_files", nargs="+", help="API header files to generate files from") + parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) + parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None) + parser.add_argument("--java-output-dir", dest="java_output_dir", default=None) + parser.add_argument("--java-package-name", dest="java_package_name", default=None) + parser.add_argument("--ml-output-dir", dest="ml_output_dir", default=None) + pargs = parser.parse_args(args) + + if pargs.java_output_dir: + if pargs.java_package_name == None: + logging.error('--java-package-name must be specified') + return 1 + + 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 os.path.isdir(pargs.api_output_dir): + logging.error('"{}" is not a directory'.format(pargs.api_output_dir)) + return 1 + + generate_files(api_files=pargs.api_files, + api_output_dir=pargs.api_output_dir, + z3py_output_dir=pargs.z3py_output_dir, + dotnet_output_dir=pargs.dotnet_output_dir, + java_output_dir=pargs.java_output_dir, + java_package_name=pargs.java_package_name, + ml_output_dir=pargs.ml_output_dir) + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) From 251527603df01904f70ed884f8695fedab5caed9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 20 Feb 2016 23:21:00 +0000 Subject: [PATCH 07/42] Implement a CMake build system. This is a large rework of my first attempt at this (#459). This implementation calls into the recently implemented python scripts to generate the necessary generated ``.h`` and ``.cpp`` files but is independent from Python building system otherwise. Unlike the Python build system, the generated files are emitted into the build tree to avoid polluting the source tree. The build system is setup to refuse to configure if it detects generated files in the source tree. If your source tree is dirty you can run ``git clean -fx`` to clean your working directory. Currently the build succeeds on Linux using CMake 3.4.3 using the "Unix Makefiles" generator with gcc or clang. The following notable features are implemented: * Building of the C and C++ examples and the ``test-z3`` executable. These are included from the ``all`` target so you have to tell the build system (e.g. make) to build them manually. * Install (``make install``) and uninstall (``make uninstall``) of libz3 and its header files. This supports ``DESTDIR`` out of the box because CMake supports it. * An option (``BUILD_LIBZ3_SHARED``) to build libz3 as a static or dynamic library. * Support for using/not using OpenMP (``USE_OPENMP``) * Support for using/not using libgmp (``USE_LIB_GMP``) * Setting the SOVERSION for libz3. I'm not sure if I'm setting the * number correctly though. This is required by Linux distrubtions that wills ship libz3. This needs discussion. The following notable features are currently not implemented and are left for future work. * Support for ARM. * Support for the foci2 library. * Support for creating/installing/uninstalling the dotnet, java, python and ml bindings. * Full support for MSVC. Although I've tried to write the CMake code with MSVC in mind not all the correct flags are passed to it. * Support for using the git hash. This new build system has several advantages other the old build system. * It is easier for outside contributors to contribute to Z3 when the build system is something more standard. * Incremental builds work properly. With the old build system when new code is pulled down the old build directory would need to thrown out and a new fresh build had to be performed because the build system didn't know how to correctly rebuild the project (e.g. couldn't handle new sources being added/removed, compiler flags changing, generated files changing, etc...). This is a MASSIVE boost to productivity! * We now have access rich array of features that CMake provides for building C/C++ projects. This means less time spent implementing custom build system logic in Python that is already supported by CMake. * CMake supports many IDEs out of the box so it should be fairly straight forward to build Z3 with Visual Studio (once support for MSVC is added), Xcode, Eclipse CDT, CLion, ..etc. --- CMakeLists.txt | 300 ++++++++++++++++++ cmake/cmake_uninstall.cmake.in | 24 ++ cmake/compiler_flags_override.cmake | 30 ++ cmake/compiler_warnings.cmake | 38 +++ cmake/modules/FindGMP.cmake | 64 ++++ cmake/target_arch_detect.cmake | 22 ++ cmake/target_arch_detect.cpp | 10 + cmake/z3_add_component.cmake | 245 ++++++++++++++ cmake/z3_add_cxx_flag.cmake | 22 ++ examples/CMakeLists.txt | 2 + examples/c++/CMakeLists.txt | 4 + examples/c/CMakeLists.txt | 3 + src/CMakeLists.txt | 139 ++++++++ src/ackermannization/CMakeLists.txt | 20 ++ src/api/CMakeLists.txt | 86 +++++ src/api/dll/CMakeLists.txt | 13 + src/ast/CMakeLists.txt | 48 +++ src/ast/fpa/CMakeLists.txt | 10 + src/ast/macros/CMakeLists.txt | 9 + src/ast/normal_forms/CMakeLists.txt | 11 + src/ast/pattern/CMakeLists.txt | 36 +++ src/ast/proof_checker/CMakeLists.txt | 6 + src/ast/rewriter/CMakeLists.txt | 34 ++ src/ast/rewriter/bit_blaster/CMakeLists.txt | 8 + src/ast/simplifier/CMakeLists.txt | 30 ++ src/ast/substitution/CMakeLists.txt | 10 + src/cmd_context/CMakeLists.txt | 21 ++ src/cmd_context/extra_cmds/CMakeLists.txt | 10 + src/duality/CMakeLists.txt | 11 + src/interp/CMakeLists.txt | 19 ++ .../{iz3params.pyg => interp_params.pyg} | 0 src/math/automata/CMakeLists.txt | 6 + src/math/euclid/CMakeLists.txt | 6 + src/math/grobner/CMakeLists.txt | 6 + src/math/hilbert/CMakeLists.txt | 6 + src/math/interval/CMakeLists.txt | 6 + src/math/polynomial/CMakeLists.txt | 16 + .../{algebraic.pyg => algebraic_params.pyg} | 0 src/math/realclosure/CMakeLists.txt | 9 + .../realclosure/{rcf.pyg => rcf_params.pyg} | 0 src/math/simplex/CMakeLists.txt | 6 + src/math/subpaving/CMakeLists.txt | 11 + src/math/subpaving/tactic/CMakeLists.txt | 8 + src/model/CMakeLists.txt | 18 ++ src/muz/base/CMakeLists.txt | 23 ++ src/muz/bmc/CMakeLists.txt | 7 + src/muz/clp/CMakeLists.txt | 7 + src/muz/dataflow/CMakeLists.txt | 6 + src/muz/ddnf/CMakeLists.txt | 8 + src/muz/duality/CMakeLists.txt | 8 + src/muz/fp/CMakeLists.txt | 16 + src/muz/pdr/CMakeLists.txt | 20 ++ src/muz/rel/CMakeLists.txt | 32 ++ src/muz/tab/CMakeLists.txt | 7 + src/muz/transforms/CMakeLists.txt | 28 ++ src/nlsat/CMakeLists.txt | 14 + src/nlsat/tactic/CMakeLists.txt | 10 + src/opt/CMakeLists.txt | 26 ++ src/parsers/smt/CMakeLists.txt | 8 + src/parsers/smt2/CMakeLists.txt | 8 + src/parsers/util/CMakeLists.txt | 11 + src/qe/CMakeLists.txt | 21 ++ src/sat/CMakeLists.txt | 29 ++ src/sat/sat_solver/CMakeLists.txt | 11 + src/sat/tactic/CMakeLists.txt | 9 + src/shell/CMakeLists.txt | 47 +++ src/smt/CMakeLists.txt | 77 +++++ src/smt/params/CMakeLists.txt | 18 ++ src/smt/proto_model/CMakeLists.txt | 13 + src/smt/tactic/CMakeLists.txt | 8 + src/solver/CMakeLists.txt | 13 + src/tactic/CMakeLists.txt | 20 ++ src/tactic/aig/CMakeLists.txt | 7 + src/tactic/arith/CMakeLists.txt | 31 ++ src/tactic/bv/CMakeLists.txt | 16 + src/tactic/core/CMakeLists.txt | 25 ++ src/tactic/fpa/CMakeLists.txt | 14 + src/tactic/nlsat_smt/CMakeLists.txt | 7 + src/tactic/portfolio/CMakeLists.txt | 15 + src/tactic/sls/CMakeLists.txt | 13 + src/tactic/smtlogics/CMakeLists.txt | 31 ++ src/tactic/ufbv/CMakeLists.txt | 14 + src/test/CMakeLists.txt | 125 ++++++++ src/test/fuzzing/CMakeLists.txt | 8 + src/util/CMakeLists.txt | 60 ++++ src/util/version.h.in | 5 + 86 files changed, 2259 insertions(+) create mode 100644 CMakeLists.txt create mode 100644 cmake/cmake_uninstall.cmake.in create mode 100644 cmake/compiler_flags_override.cmake create mode 100644 cmake/compiler_warnings.cmake create mode 100644 cmake/modules/FindGMP.cmake create mode 100644 cmake/target_arch_detect.cmake create mode 100644 cmake/target_arch_detect.cpp create mode 100644 cmake/z3_add_component.cmake create mode 100644 cmake/z3_add_cxx_flag.cmake create mode 100644 examples/CMakeLists.txt create mode 100644 examples/c++/CMakeLists.txt create mode 100644 examples/c/CMakeLists.txt create mode 100644 src/CMakeLists.txt create mode 100644 src/ackermannization/CMakeLists.txt create mode 100644 src/api/CMakeLists.txt create mode 100644 src/api/dll/CMakeLists.txt create mode 100644 src/ast/CMakeLists.txt create mode 100644 src/ast/fpa/CMakeLists.txt create mode 100644 src/ast/macros/CMakeLists.txt create mode 100644 src/ast/normal_forms/CMakeLists.txt create mode 100644 src/ast/pattern/CMakeLists.txt create mode 100644 src/ast/proof_checker/CMakeLists.txt create mode 100644 src/ast/rewriter/CMakeLists.txt create mode 100644 src/ast/rewriter/bit_blaster/CMakeLists.txt create mode 100644 src/ast/simplifier/CMakeLists.txt create mode 100644 src/ast/substitution/CMakeLists.txt create mode 100644 src/cmd_context/CMakeLists.txt create mode 100644 src/cmd_context/extra_cmds/CMakeLists.txt create mode 100644 src/duality/CMakeLists.txt create mode 100644 src/interp/CMakeLists.txt rename src/interp/{iz3params.pyg => interp_params.pyg} (100%) create mode 100644 src/math/automata/CMakeLists.txt create mode 100644 src/math/euclid/CMakeLists.txt create mode 100644 src/math/grobner/CMakeLists.txt create mode 100644 src/math/hilbert/CMakeLists.txt create mode 100644 src/math/interval/CMakeLists.txt create mode 100644 src/math/polynomial/CMakeLists.txt rename src/math/polynomial/{algebraic.pyg => algebraic_params.pyg} (100%) create mode 100644 src/math/realclosure/CMakeLists.txt rename src/math/realclosure/{rcf.pyg => rcf_params.pyg} (100%) create mode 100644 src/math/simplex/CMakeLists.txt create mode 100644 src/math/subpaving/CMakeLists.txt create mode 100644 src/math/subpaving/tactic/CMakeLists.txt create mode 100644 src/model/CMakeLists.txt create mode 100644 src/muz/base/CMakeLists.txt create mode 100644 src/muz/bmc/CMakeLists.txt create mode 100644 src/muz/clp/CMakeLists.txt create mode 100644 src/muz/dataflow/CMakeLists.txt create mode 100644 src/muz/ddnf/CMakeLists.txt create mode 100644 src/muz/duality/CMakeLists.txt create mode 100644 src/muz/fp/CMakeLists.txt create mode 100644 src/muz/pdr/CMakeLists.txt create mode 100644 src/muz/rel/CMakeLists.txt create mode 100644 src/muz/tab/CMakeLists.txt create mode 100644 src/muz/transforms/CMakeLists.txt create mode 100644 src/nlsat/CMakeLists.txt create mode 100644 src/nlsat/tactic/CMakeLists.txt create mode 100644 src/opt/CMakeLists.txt create mode 100644 src/parsers/smt/CMakeLists.txt create mode 100644 src/parsers/smt2/CMakeLists.txt create mode 100644 src/parsers/util/CMakeLists.txt create mode 100644 src/qe/CMakeLists.txt create mode 100644 src/sat/CMakeLists.txt create mode 100644 src/sat/sat_solver/CMakeLists.txt create mode 100644 src/sat/tactic/CMakeLists.txt create mode 100644 src/shell/CMakeLists.txt create mode 100644 src/smt/CMakeLists.txt create mode 100644 src/smt/params/CMakeLists.txt create mode 100644 src/smt/proto_model/CMakeLists.txt create mode 100644 src/smt/tactic/CMakeLists.txt create mode 100644 src/solver/CMakeLists.txt create mode 100644 src/tactic/CMakeLists.txt create mode 100644 src/tactic/aig/CMakeLists.txt create mode 100644 src/tactic/arith/CMakeLists.txt create mode 100644 src/tactic/bv/CMakeLists.txt create mode 100644 src/tactic/core/CMakeLists.txt create mode 100644 src/tactic/fpa/CMakeLists.txt create mode 100644 src/tactic/nlsat_smt/CMakeLists.txt create mode 100644 src/tactic/portfolio/CMakeLists.txt create mode 100644 src/tactic/sls/CMakeLists.txt create mode 100644 src/tactic/smtlogics/CMakeLists.txt create mode 100644 src/tactic/ufbv/CMakeLists.txt create mode 100644 src/test/CMakeLists.txt create mode 100644 src/test/fuzzing/CMakeLists.txt create mode 100644 src/util/CMakeLists.txt create mode 100644 src/util/version.h.in diff --git a/CMakeLists.txt b/CMakeLists.txt new file mode 100644 index 00000000000..3c10b4f0aac --- /dev/null +++ b/CMakeLists.txt @@ -0,0 +1,300 @@ +# This overrides the default flags for the different CMAKE_BUILD_TYPEs +set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake") +project(Z3 LANGUAGES C CXX) +cmake_minimum_required(VERSION 2.8.12) + +################################################################################ +# Project version +################################################################################ +set(Z3_VERSION_MAJOR 4) +set(Z3_VERSION_MINOR 4) +set(Z3_VERSION_PATCH 2) +set(Z3_VERSION_TWEAK 0) +set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") +message(STATUS "Z3 version ${Z3_VERSION}") + +################################################################################ +# Message for polluted source tree sanity checks +################################################################################ +set(z3_polluted_tree_msg + " should not exist and is polluting the source tree." + " It is likely that this file came from the Python build system which" + " generates files inside the source tree. This is bad practice and the CMake" + " build system is setup to make sure that the source tree is clean during" + " its configure step. If you are using git you can remove all untracked files" + " using ``git clean -fx``. Be careful when doing this. You should probably use" + " this with ``-n`` first to check which file(s) would be removed." +) + +################################################################################ +# Add our CMake module directory to the list of module search directories +################################################################################ +list(APPEND CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/cmake/modules") + +################################################################################ +# Useful CMake functions/Macros +################################################################################ +include(CheckCXXSourceCompiles) + +################################################################################ +# Compiler flags for Z3 components. +# Subsequent commands will append to this +################################################################################ +set(Z3_COMPONENT_CXX_DEFINES "") +set(Z3_COMPONENT_CXX_FLAGS "") +set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "") +set(Z3_DEPENDENT_LIBS "") + +################################################################################ +# Build type +################################################################################ +message(STATUS "CMake generator: ${CMAKE_GENERATOR}") +if (DEFINED CMAKE_CONFIGURATION_TYPES) + # Multi-configuration build (e.g. Visual Studio and Xcode). Here + # CMAKE_BUILD_TYPE doesn't matter + message(STATUS "Available configurations: ${CMAKE_CONFIGURATION_TYPES}") +else() + # Single configuration generator (e.g. Unix Makefiles, Ninja) + set(available_build_types Debug Release RelWithDebInfo MinSizeRel) + if(NOT CMAKE_BUILD_TYPE) + message(STATUS "CMAKE_BUILD_TYPE is not set. Setting default") + message(STATUS "The available build types are: ${available_build_types}") + set(CMAKE_BUILD_TYPE RelWithDebInfo CACHE String + "Options are ${build_types}" + FORCE) + # Provide drop down menu options in cmake-gui + set_property(CACHE CMAKE_BUILD_TYPE PROPERTY STRINGS ${available_build_types}) + endif() + message(STATUS "Build type: ${CMAKE_BUILD_TYPE}") +endif() + +# CMAKE_BUILD_TYPE has no meaning for multi-configuration generators +# (e.g. Visual Studio) so use generator expressions instead to add +# the right definitions when doing a particular build type. +# +# Note for some reason we have to leave off ``-D`` here otherwise +# we get ``-D-DZ3DEBUG`` passed to the compiler +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:Z3DEBUG>) +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_EXTERNAL_RELEASE>) +list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_EXTERNAL_RELEASE>) + +################################################################################ +# Find Python +################################################################################ +find_package(PythonInterp REQUIRED) +message(STATUS "PYTHON_EXECUTABLE: ${PYTHON_EXECUTABLE}") + +################################################################################ +# Target architecture detection +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cmake) +detect_target_architecture(TARGET_ARCHITECTURE) +message(STATUS "Detected target architecture: ${TARGET_ARCHITECTURE}") +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_AMD64_") +endif() + + +################################################################################ +# Function for detecting C++ compiler flag support +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/z3_add_cxx_flag.cmake) + +################################################################################ +# Platform detection +################################################################################ +if ("${CMAKE_SYSTEM_NAME}" STREQUAL "Linux") + message(STATUS "Platform: Linux") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_LINUX_") + if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_USE_THREAD_LOCAL") + endif() + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) +elseif ("${CMAKE_SYSTEM_NAME}" STREQUAL "Darwin") + # Does OSX really not need any special flags? + message(STATUS "Platform: Darwin") +elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "FreeBSD") + message(STATUS "Platform: FreeBSD") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_FREEBSD_") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) +elseif ("${CMAKE_SYSTEM_NAME}" MATCHES "OpenBSD") + message(STATUS "Platform: OpenBSD") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_OPENBSD_") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) +elseif (CYGWIN) + message(STATUS "Platform: Cygwin") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_CYGWIN") + z3_add_cxx_flag("-fno-strict-aliasing" REQUIRED) +elseif (WIN32) + message(STATUS "Platform: Windows") + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_WINDOWS") +else() + message(FATAL_ERROR "Platform \"${CMAKE_SYSTEM_NAME}\" not recognised") +endif() + + +################################################################################ +# GNU multiple precision library support +################################################################################ +option(USE_LIB_GMP "Use GNU Multiple Precision Library" OFF) +if (USE_LIB_GMP) + # Because this is off by default we will make the configure fail if libgmp + # can't be found + find_package(GMP REQUIRED) + message(STATUS "Using libgmp") + list(APPEND Z3_DEPENDENT_LIBS ${GMP_C_LIBRARIES}) + list(APPEND Z3_COMPONENT_EXTRA_INCLUDE_DIRS ${GMP_INCLUDE_DIRS}) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_GMP") +else() + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_MP_INTERNAL") + message(STATUS "Not using libgmp") +endif() + +################################################################################ +# FOCI2 support +################################################################################ +# FIXME: What is this? +option(USE_FOCI2 "Use FOCI2" OFF) +if (USE_FOCI2) + message(FATAL_ERROR "TODO") + message(STATUS "Using FOCI2") +else() + message(STATUS "Not using FOCI2") +endif() + +################################################################################ +# OpenMP support +################################################################################ +option(USE_OPENMP "Use OpenMP" ON) +set(OPENMP_FOUND FALSE) +if (USE_OPENMP) + # Because this is on by default we make the configure succeed with a warning + # if OpenMP support is not detected. + find_package(OpenMP) + if (NOT OPENMP_FOUND) + message(WARNING "OpenMP support was requested but your compiler doesn't support it") + endif() +endif() +if (OPENMP_FOUND) + list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) + list(APPEND Z3_DEPENDENT_LIBS ${OpenMP_CXX_FLAGS}) + unset(CMAKE_REQUIRED_FLAGS) + message(STATUS "Using OpenMP") +else() + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_NO_OMP_") + message(STATUS "Not using OpenMP") +endif() + +################################################################################ +# FP math +################################################################################ +# FIXME: Support ARM "-mfpu=vfp -mfloat-abi=hard" +if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) + set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") + elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + set(SSE_FLAGS "/arch:SSE2") + else() + message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}") + endif() + CHECK_CXX_COMPILER_FLAG("${SSE_FLAGS}" HAS_SSE2) + if (HAS_SSE2) + list(APPEND Z3_COMPONENT_CXX_FLAGS ${SSE_FLAGS}) + endif() + unset(SSE_FLAGS) +endif() + +################################################################################ +# Compiler warnings +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/compiler_warnings.cmake) + +################################################################################ +# Option to control what type of library we build +################################################################################ +option(BUILD_LIBZ3_SHARED "Build libz3 as a shared library if true, otherwise build a static library" ON) + + +################################################################################ +# Symbol visibility +################################################################################ +if (NOT MSVC) + z3_add_cxx_flag("-fvisibility=hidden" REQUIRED) +endif() + +################################################################################ +# Tracing +################################################################################ +option(ENABLE_TRACING OFF "Enable tracing") +if (ENABLE_TRACING) + list(APPEND Z3_COMPONENT_CXX_DEFINES "-D_TRACE") +endif() +# Should we always enable tracing when doing a debug build? +#list(APPEND Z3_COMPONENT_CXX_DEFINES $<$:_TRACE>) + +################################################################################ +# Postion indepdent code +################################################################################ +# This is required because code built in the components will end up in a shared +# library. If not building a shared library ``-fPIC`` isn't needed and would add +# unnecessary overhead. +if (BUILD_LIBZ3_SHARED) + if (NOT MSVC) + z3_add_cxx_flag("-fPIC" REQUIRED) + endif() +endif() + +################################################################################ +# Report Z3_COMPONENT flags +################################################################################ +message(STATUS "Z3_COMPONENT_CXX_DEFINES: ${Z3_COMPONENT_CXX_DEFINES}") +message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}") +message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}") +message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}") + +################################################################################ +# Z3 installation locations +################################################################################ +set (Z3_INSTALL_LIB_DIR "lib") +set (Z3_INSTALL_BIN_DIR "bin") +set (Z3_INSTALL_INCLUDE_DIR "include") + +################################################################################ +# CMake build file locations +################################################################################ +# To mimic the python build system output these into the root of the build +# directory +set(CMAKE_LIBRARY_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") +set(CMAKE_ARCHIVE_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") +set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") + +################################################################################ +# Z3 components, library and executables +################################################################################ +include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake) +add_subdirectory(src) + +################################################################################ +# Examples +################################################################################ +option(ENABLE_EXAMPLE_TARGETS "Build Z3 api examples" ON) +if (ENABLE_EXAMPLE_TARGETS) + add_subdirectory(examples) +endif() + +################################################################################ +# Uninstall rule +################################################################################ +configure_file( + "${CMAKE_SOURCE_DIR}/cmake/cmake_uninstall.cmake.in" + "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" + @ONLY +) + +add_custom_target(uninstall + COMMAND + "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" + COMMENT "Uninstalling..." + USES_TERMINAL + VERBATIM +) diff --git a/cmake/cmake_uninstall.cmake.in b/cmake/cmake_uninstall.cmake.in new file mode 100644 index 00000000000..cbe8c274977 --- /dev/null +++ b/cmake/cmake_uninstall.cmake.in @@ -0,0 +1,24 @@ +if(NOT EXISTS "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt") + message(FATAL_ERROR "Cannot find install manifest: " + "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt") +endif() + +file(READ "@CMAKE_CURRENT_BINARY_DIR@/install_manifest.txt" files) +string(REGEX REPLACE "\n" ";" files "${files}") +foreach(file ${files}) + set(_full_file_path "$ENV{DESTDIR}${file}") + message(STATUS "Uninstalling ${_full_file_path}") + if(IS_SYMLINK "${_full_file_path}" OR EXISTS "${_full_file_path}") + # We could use ``file(REMOVE ...)`` here but then we wouldn't + # know if the removal failed. + execute_process(COMMAND + "@CMAKE_COMMAND@" "-E" "remove" "${_full_file_path}" + RESULT_VARIABLE rm_retval + ) + if(NOT "${rm_retval}" STREQUAL 0) + message(FATAL_ERROR "Problem when removing \"${_full_file_path}\"") + endif() + else() + message(STATUS "File \"${_full_file_path}\" does not exist.") + endif() +endforeach() diff --git a/cmake/compiler_flags_override.cmake b/cmake/compiler_flags_override.cmake new file mode 100644 index 00000000000..cb1f8dbc16f --- /dev/null +++ b/cmake/compiler_flags_override.cmake @@ -0,0 +1,30 @@ +# This file overrides the default compiler flags for CMake's built-in +# configurations (CMAKE_BUILD_TYPE). Most compiler flags should not be set here. +# The main purpose is to make sure ``-DNDEBUG`` is never set by default. +if (CMAKE_C_COMPILER_ID) + set(_lang C) +elseif(CMAKE_CXX_COMPILER_ID) + set(_lang CXX) +else() + message(FATAL_ERROR "Unknown language") +endif() + +if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU")) + # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed + set(CMAKE_${_lang}_FLAGS_INIT "") + # FIXME: should we have -D_DEBUG here to match MSVC build? + set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0") + set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os") + set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3") + set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") +elseif ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "MSVC") + # Not tested! + set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/D_DEBUG /MTd /Zi /Ob0 /Od /RTC1") + set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1") + set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2") + set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1") +else() + message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"") +endif() + +unset(_lang) diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake new file mode 100644 index 00000000000..e9910c2e4ea --- /dev/null +++ b/cmake/compiler_warnings.cmake @@ -0,0 +1,38 @@ +set(GCC_AND_CLANG_WARNINGS + "-Wall" +) +set(GCC_ONLY_WARNINGS "") +set(CLANG_ONLY_WARNINGS "") +set(MSVC_WARNINGS "/W3") + +set(WARNING_FLAGS_TO_CHECK "") +if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") + list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) + list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_ONLY_WARNINGS}) +elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") + list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) + list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) +elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) +else() + message(AUTHOR_WARNING "Unknown compiler") +endif() + +# Loop through flags and use the ones which the compiler supports +foreach (flag ${WARNING_FLAGS_TO_CHECK}) + z3_add_cxx_flag("${flag}") +endforeach() + +option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) +if (WARNINGS_AS_ERRORS) + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") + elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX") + else() + message(AUTHOR_WARNING "Unknown compiler") + endif() + message(STATUS "Treating compiler warnings as errors") +else() + message(STATUS "Not treating compiler warnings as errors") +endif() diff --git a/cmake/modules/FindGMP.cmake b/cmake/modules/FindGMP.cmake new file mode 100644 index 00000000000..b749750efc5 --- /dev/null +++ b/cmake/modules/FindGMP.cmake @@ -0,0 +1,64 @@ +# Tries to find an install of the GNU multiple precision library +# +# Once done this will define +# GMP_FOUND - BOOL: System has the GMP library installed +# GMP_INCLUDE_DIRS - LIST:The GMP include directories +# GMP_C_LIBRARIES - LIST:The libraries needed to use GMP via it's C interface +# GMP_CXX_LIBRARIES - LIST:The libraries needed to use GMP via it's C++ interface + +include(FindPackageHandleStandardArgs) + +# Try to find libraries +find_library(GMP_C_LIBRARIES + NAMES gmp + DOC "GMP C libraries" +) +if (GMP_C_LIBRARIES) + message(STATUS "Found GMP C library: \"${GMP_C_LIBRARIES}\"") +else() + message(STATUS "Could not find GMP C library") +endif() +find_library(GMP_CXX_LIBRARIES + NAMES gmpxx + DOC "GMP C++ libraries" +) +if (GMP_CXX_LIBRARIES) + message(STATUS "Found GMP C++ library: \"${GMP_CXX_LIBRARIES}\"") +else() + message(STATUS "Could not find GMP C++ library") +endif() + +# Try to find headers +find_path(GMP_C_INCLUDES + NAMES gmp.h + DOC "GMP C header" +) +if (GMP_C_INCLUDES) + message(STATUS "Found GMP C include path: \"${GMP_C_INCLUDES}\"") +else() + message(STATUS "Could not find GMP C include path") +endif() + +find_path(GMP_CXX_INCLUDES + NAMES gmpxx.h + DOC "GMP C++ header" +) +if (GMP_CXX_INCLUDES) + message(STATUS "Found GMP C++ include path: \"${GMP_CXX_INCLUDES}\"") +else() + message(STATUS "Could not find GMP C++ include path") +endif() + +if (GMP_C_LIBRARIES AND GMP_CXX_LIBRARIES AND GMP_C_INCLUDES AND GMP_CXX_INCLUDES) + set(GMP_INCLUDE_DIRS "${GMP_C_INCLUDES}" "${GMP_CXX_INCLUDES}") + list(REMOVE_DUPLICATES GMP_INCLUDE_DIRS) + message(STATUS "Found GMP") +else() + message(STATUS "Could not find GMP") +endif() + +# TODO: We should check we can link some simple code against libgmp and libgmpxx + +# Handle QUIET and REQUIRED and check the necessary variables were set and if so +# set ``GMP_FOUND`` +find_package_handle_standard_args(GMP DEFAULT_MSG GMP_INCLUDE_DIRS GMP_C_LIBRARIES GMP_CXX_LIBRARIES) diff --git a/cmake/target_arch_detect.cmake b/cmake/target_arch_detect.cmake new file mode 100644 index 00000000000..68194cfe47d --- /dev/null +++ b/cmake/target_arch_detect.cmake @@ -0,0 +1,22 @@ +############################################################################### +# Target detection +# +# We abuse the compiler preprocessor to work out what target the compiler is +# building for. The nice thing about this approach is that we'll detect the +# right target even if we are using a cross compiler. +############################################################################### +function(detect_target_architecture OUTPUT_VAR) + try_run(run_result + compile_result + "${CMAKE_BINARY_DIR}" + "${CMAKE_SOURCE_DIR}/cmake/target_arch_detect.cpp" + COMPILE_OUTPUT_VARIABLE compiler_output + ) + if (compile_result) + message(FATAL_ERROR "Expected compile to fail") + endif() + string(REGEX MATCH "CMAKE_TARGET_ARCH_([a-zA-Z0-9_]+)" arch "${compiler_output}") + # Strip out prefix + string(REPLACE "CMAKE_TARGET_ARCH_" "" arch "${arch}") + set(${OUTPUT_VAR} "${arch}" PARENT_SCOPE) +endfunction() diff --git a/cmake/target_arch_detect.cpp b/cmake/target_arch_detect.cpp new file mode 100644 index 00000000000..8053e3532e5 --- /dev/null +++ b/cmake/target_arch_detect.cpp @@ -0,0 +1,10 @@ +// This is used by the CMake build to detect +// what architecture the compiler is targeting. +// TODO: Add more targets here +#if defined(__i386__) || defined(_M_IX86) +#error CMAKE_TARGET_ARCH_i686 +#elif defined(__x86_64__) || defined(_M_X64) +#error CMAKE_TARGET_ARCH_x86_64 +#else +#error CMAKE_TARGET_ARCH_unknown +#endif diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake new file mode 100644 index 00000000000..56567405548 --- /dev/null +++ b/cmake/z3_add_component.cmake @@ -0,0 +1,245 @@ +include(CMakeParseArguments) +define_property(GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS + BRIEF_DOCS "List of Z3 components to use in libz3" + FULL_DOCS "List of Z3 components to use in libz3") + +function(z3_expand_dependencies output_var) + if (ARGC LESS 2) + message(FATAL_ERROR "Invalid number of arguments") + endif() + # Remaing args should be component names + set(_expanded_deps ${ARGN}) + set(_old_number_of_deps 0) + list(LENGTH _expanded_deps _number_of_deps) + while (_number_of_deps GREATER _old_number_of_deps) + set(_old_number_of_deps "${_number_of_deps}") + # Loop over the known dependencies and retrieve their dependencies + set(_old_expanded_deps ${_expanded_deps}) + foreach (dependency ${_old_expanded_deps}) + get_property(_depdeps GLOBAL PROPERTY Z3_${dependency}_DEPS) + list(APPEND _expanded_deps ${_depdeps}) + unset(_depdeps) + endforeach() + list(REMOVE_DUPLICATES _expanded_deps) + list(LENGTH _expanded_deps _number_of_deps) + endwhile() + set(${output_var} ${_expanded_deps} PARENT_SCOPE) +endfunction() + +function(z3_add_component_dependencies_to_target target_name) + if (ARGC LESS 2) + message(FATAL_ERROR "Invalid number of arguments") + endif() + if (NOT (TARGET ${target_name})) + message(FATAL_ERROR "Target \"${target_name}\" does not exist") + endif() + # Remaing args should be component names + set(_expanded_deps ${ARGN}) + foreach (dependency ${_expanded_deps}) + # FIXME: Adding these include paths wouldn't be necessary if the sources + # used include paths rooted in the ``src`` directory. + get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) + foreach (inc_dir ${_dep_include_dirs}) + target_include_directories(${target_name} PRIVATE "${inc_dir}") + endforeach() + unset(_dep_include_dirs) + # Ensure this component's dependencies are built before this component. + # This important because we might need the generated header files in + # other components. + add_dependencies(${target_name} ${dependency}) + endforeach() +endfunction() + +macro(z3_add_component component_name) + CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN}) + message(STATUS "Adding component ${component_name}") + # Note: We don't check the sources exist here because + # they might be generated files that don't exist yet. + + set(_list_generated_headers "") + foreach (pyg_file ${Z3_MOD_PYG_FILES}) + set(_full_pyg_file_path "${CMAKE_CURRENT_SOURCE_DIR}/${pyg_file}") + if (NOT (EXISTS "${_full_pyg_file_path}")) + message(FATAL_ERROR "\"${_full_pyg_file_path}\" does not exist") + endif() + string(REPLACE ".pyg" ".hpp" _output_file "${pyg_file}") + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${_output_file}\" " + ${z3_polluted_tree_msg} + ) + endif() + set(_full_output_file_path "${CMAKE_CURRENT_BINARY_DIR}/${_output_file}") + message(STATUS "Adding rule to generate \"${_output_file}\"") + 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" + COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\"" + WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" + USES_TERMINAL + VERBATIM + ) + list(APPEND _list_generated_headers "${_full_output_file_path}") + endforeach() + unset(_full_include_dir_path) + unset(_full_output_file_path) + unset(_output_file) + + # Using "object" libraries here means we have a convenient + # name to refer to a component in CMake but we don't actually + # create a static/library from them. This allows us to easily + # build a static or dynamic library from the object libraries + # on all platforms. Is this added flexibility worth the linking + # overhead it adds? + add_library(${component_name} OBJECT ${Z3_MOD_SOURCES} ${_list_generated_headers}) + unset(_list_generated_headers) + # Add definitions + foreach (define ${Z3_COMPONENT_CXX_DEFINES}) + target_compile_definitions(${component_name} PRIVATE ${define}) + endforeach() + # Add compiler flags + foreach (flag ${Z3_COMPONENT_CXX_FLAGS}) + target_compile_options(${component_name} PRIVATE ${flag}) + endforeach() + + # It's unfortunate that we have to manage the include directories and dependencies ourselves. + # + # If we weren't building "object" libraries we could use + # ``` + # target_include_directories(${component_name} INTERFACE "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + # target_link_libraries(${component_name} INTERFACE ${Z3_MOD_COMPONENT_DEPENDENCIES}) + # ``` + # but we can't do that with "object" libraries. + + # Record this component's include directories + set_property(GLOBAL PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_SOURCE_DIR}") + set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_INCLUDES "${CMAKE_CURRENT_BINARY_DIR}") + set_property(GLOBAL PROPERTY Z3_${component_name}_DEPS "") + # Record this component's dependencies + foreach (dependency ${Z3_MOD_COMPONENT_DEPENDENCIES}) + if (NOT (TARGET ${dependency})) + message(FATAL_ERROR "Component \"${component_name}\" depends on a non existant component \"${dependency}\"") + endif() + set_property(GLOBAL APPEND PROPERTY Z3_${component_name}_DEPS "${dependency}") + endforeach() + + # Determine all the components that this component depends on + set(_expanded_deps "") + if (DEFINED Z3_MOD_COMPONENT_DEPENDENCIES) + z3_expand_dependencies(_expanded_deps ${Z3_MOD_COMPONENT_DEPENDENCIES}) + z3_add_component_dependencies_to_target(${component_name} ${_expanded_deps}) + endif() + #message(STATUS "Component \"${component_name}\" has the following dependencies ${_expanded_deps}") + + # For any generated header files for this component + target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_BINARY_DIR}") + # So that any generated header files can refer to source files in the component's + # source tree + target_include_directories(${component_name} PRIVATE "${CMAKE_CURRENT_SOURCE_DIR}") + + # Add any extra include directories + foreach (extra_include ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) + target_include_directories(${component_name} PRIVATE "${extra_include}") + endforeach() + + if (NOT Z3_MOD_NOT_LIBZ3_COMPONENT) + # Add this component to the global list of Z3 components for libz3 + set_property(GLOBAL APPEND PROPERTY Z3_LIBZ3_COMPONENTS ${component_name}) + endif() +endmacro() + +macro(z3_add_install_tactic_rule) + # Arguments should be component names to use + if (ARGC LESS 1) + message(FATAL_ERROR "There should be at least one component") + endif() + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/install_tactic.cpp\"" + ${z3_polluted_tree_msg} + ) + endif() + z3_expand_dependencies(_expanded_components ${ARGN}) + # Get paths to search + set(_search_paths "") + foreach (dependency ${_expanded_components}) + get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) + list(APPEND _search_paths ${_dep_include_dirs}) + endforeach() + list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + add_custom_command(OUTPUT "install_tactic.cpp" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" + "${CMAKE_CURRENT_BINARY_DIR}" + ${_search_paths} + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_install_tactic_cpp.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${_expanded_components} + COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" + USES_TERMINAL + VERBATIM + ) +endmacro() + +macro(z3_add_memory_initializer_rule) + # Arguments should be component names to use + if (ARGC LESS 1) + message(FATAL_ERROR "There should be at least one component") + endif() + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/mem_initializer.cpp\"" + ${z3_polluted_tree_msg} + ) + endif() + z3_expand_dependencies(_expanded_components ${ARGN}) + # Get paths to search + set(_search_paths "") + foreach (dependency ${_expanded_components}) + get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) + list(APPEND _search_paths ${_dep_include_dirs}) + endforeach() + list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + add_custom_command(OUTPUT "mem_initializer.cpp" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" + "${CMAKE_CURRENT_BINARY_DIR}" + ${_search_paths} + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_mem_initializer_cpp.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${_expanded_components} + COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" + USES_TERMINAL + VERBATIM + ) +endmacro() + +macro(z3_add_gparams_register_modules_rule) + # Arguments should be component names to use + if (ARGC LESS 1) + message(FATAL_ERROR "There should be at least one component") + endif() + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/gparams_register_modules.cpp\"" + ${z3_polluted_tree_msg} + ) + endif() + z3_expand_dependencies(_expanded_components ${ARGN}) + # Get paths to search + set(_search_paths "") + foreach (dependency ${_expanded_components}) + get_property(_dep_include_dirs GLOBAL PROPERTY Z3_${dependency}_INCLUDES) + list(APPEND _search_paths ${_dep_include_dirs}) + endforeach() + list(APPEND _search_paths "${CMAKE_CURRENT_SOURCE_DIR}" "${CMAKE_CURRENT_BINARY_DIR}") + add_custom_command(OUTPUT "gparams_register_modules.cpp" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" + "${CMAKE_CURRENT_BINARY_DIR}" + ${_search_paths} + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_gparams_register_modules_cpp.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${_expanded_components} + COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" + USES_TERMINAL + VERBATIM + ) +endmacro() diff --git a/cmake/z3_add_cxx_flag.cmake b/cmake/z3_add_cxx_flag.cmake new file mode 100644 index 00000000000..0c56bb0f612 --- /dev/null +++ b/cmake/z3_add_cxx_flag.cmake @@ -0,0 +1,22 @@ +include(CheckCXXCompilerFlag) +include(CMakeParseArguments) + +function(z3_add_cxx_flag flag) + CMAKE_PARSE_ARGUMENTS(z3_add_flag "REQUIRED" "" "" ${ARGN}) + string(REPLACE "-" "_" SANITIZED_FLAG_NAME "${flag}") + string(REPLACE "/" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE "=" "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + string(REPLACE " " "_" SANITIZED_FLAG_NAME "${SANITIZED_FLAG_NAME}") + unset(HAS_${SANITIZED_FLAG_NAME}) + CHECK_CXX_COMPILER_FLAG("${flag}" HAS_${SANITIZED_FLAG_NAME}) + if (z3_add_flag_REQUIRED AND NOT HAS_${SANITIZED_FLAG_NAME}) + message(FATAL_ERROR "The flag \"${flag}\" is required but your C++ compiler doesn't support it") + endif() + if (HAS_${SANITIZED_FLAG_NAME}) + message(STATUS "C++ compiler supports ${flag}") + list(APPEND Z3_COMPONENT_CXX_FLAGS "${flag}") + set(Z3_COMPONENT_CXX_FLAGS "${Z3_COMPONENT_CXX_FLAGS}" PARENT_SCOPE) + else() + message(STATUS "C++ compiler does not support ${flag}") + endif() +endfunction() diff --git a/examples/CMakeLists.txt b/examples/CMakeLists.txt new file mode 100644 index 00000000000..b8cecbe631e --- /dev/null +++ b/examples/CMakeLists.txt @@ -0,0 +1,2 @@ +add_subdirectory(c) +add_subdirectory(c++) diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt new file mode 100644 index 00000000000..85bbd77c712 --- /dev/null +++ b/examples/c++/CMakeLists.txt @@ -0,0 +1,4 @@ +add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) +target_link_libraries(cpp_example PRIVATE libz3) +target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") +target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt new file mode 100644 index 00000000000..1a14573ac38 --- /dev/null +++ b/examples/c/CMakeLists.txt @@ -0,0 +1,3 @@ +add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) +target_link_libraries(c_example PRIVATE libz3) +target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt new file mode 100644 index 00000000000..4a41cccecc1 --- /dev/null +++ b/src/CMakeLists.txt @@ -0,0 +1,139 @@ +# I'm duplicating the order in ``mk_project.py`` for now to help us keep +# the build systems in sync. +# +# The components in these directory explicitly declare their dependencies so +# you may be able to re-order some of these directories but an error will be +# raised if you try to declare a component is depedent on another component +# that has not yet been declared. +add_subdirectory(util) +add_subdirectory(math/polynomial) +add_subdirectory(sat) +add_subdirectory(nlsat) +add_subdirectory(math/hilbert) +add_subdirectory(math/simplex) +add_subdirectory(math/automata) +add_subdirectory(math/interval) +add_subdirectory(math/realclosure) +add_subdirectory(math/subpaving) +add_subdirectory(ast) +add_subdirectory(ast/rewriter) +add_subdirectory(ast/normal_forms) +add_subdirectory(model) +add_subdirectory(tactic) +add_subdirectory(ast/substitution) +add_subdirectory(parsers/util) +add_subdirectory(math/grobner) +add_subdirectory(math/euclid) +add_subdirectory(tactic/core) +add_subdirectory(sat/tactic) +add_subdirectory(tactic/arith) +add_subdirectory(nlsat/tactic) +add_subdirectory(math/subpaving/tactic) +add_subdirectory(tactic/aig) +add_subdirectory(solver) +add_subdirectory(ackermannization) +add_subdirectory(interp) +add_subdirectory(cmd_context) +add_subdirectory(cmd_context/extra_cmds) +add_subdirectory(parsers/smt2) +add_subdirectory(ast/proof_checker) +## Simplifier module will be deleted in the future. +## It has been replaced with rewriter component. +add_subdirectory(ast/simplifier) +add_subdirectory(ast/fpa) +add_subdirectory(ast/macros) +add_subdirectory(ast/pattern) +add_subdirectory(ast/rewriter/bit_blaster) +add_subdirectory(smt/params) +add_subdirectory(smt/proto_model) +add_subdirectory(smt) +add_subdirectory(tactic/bv) +add_subdirectory(smt/tactic) +add_subdirectory(tactic/sls) +add_subdirectory(qe) +add_subdirectory(duality) +add_subdirectory(muz/base) +add_subdirectory(muz/dataflow) +add_subdirectory(muz/transforms) +add_subdirectory(muz/rel) +add_subdirectory(muz/pdr) +add_subdirectory(muz/clp) +add_subdirectory(muz/tab) +add_subdirectory(muz/bmc) +add_subdirectory(muz/ddnf) +add_subdirectory(muz/duality) +add_subdirectory(muz/fp) +add_subdirectory(tactic/nlsat_smt) +add_subdirectory(tactic/ufbv) +add_subdirectory(sat/sat_solver) +add_subdirectory(tactic/smtlogics) +add_subdirectory(tactic/fpa) +add_subdirectory(tactic/portfolio) +add_subdirectory(parsers/smt) +add_subdirectory(opt) +add_subdirectory(api) +add_subdirectory(api/dll) + +################################################################################ +# libz3 +################################################################################ +get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS) +set (object_files "") +foreach (component ${Z3_LIBZ3_COMPONENTS_LIST}) + list(APPEND object_files $) +endforeach() +if (BUILD_LIBZ3_SHARED) + set(lib_type "SHARED") +else() + set(lib_type "STATIC") +endif() +add_library(libz3 ${lib_type} ${object_files}) +# FIXME: Set "VERSION" and "SOVERSION" properly +set_target_properties(libz3 PROPERTIES + OUTPUT_NAME z3 + # FIXME: Should we be using ${Z3_VERSION} here? + # VERSION: Sets up symlinks, does it do anything else? + VERSION ${Z3_VERSION} + # SOVERSION: On platforms that use ELF this sets the API version + # and should be incremented everytime the API changes + SOVERSION ${Z3_VERSION}) + +# Using INTERFACE means that targets that try link against libz3 will +# automatically link against the libs in Z3_DEPENDENT_LIBS +target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) +# Declare which header file are the public header files of libz3 +# these will automatically installed when the libz3 target is installed +set (libz3_public_headers + z3_algebraic.h + z3_api.h + z3_ast_containers.h + z3_fixedpoint.h + z3_fpa.h + z3.h + c++/z3++.h + z3_interp.h + z3_macros.h + z3_optimization.h + z3_polynomial.h + z3_rcf.h + z3_v1.h +) +foreach (header ${libz3_public_headers}) + set_property(TARGET libz3 APPEND PROPERTY + PUBLIC_HEADER "${CMAKE_SOURCE_DIR}/src/api/${header}") +endforeach() + +install(TARGETS libz3 + LIBRARY DESTINATION "${Z3_INSTALL_LIB_DIR}" + ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}" + PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}" +) +################################################################################ +# Z3 executable +################################################################################ +add_subdirectory(shell) + +################################################################################ +# z3-test +################################################################################ +add_subdirectory(test) diff --git a/src/ackermannization/CMakeLists.txt b/src/ackermannization/CMakeLists.txt new file mode 100644 index 00000000000..93529ae1286 --- /dev/null +++ b/src/ackermannization/CMakeLists.txt @@ -0,0 +1,20 @@ +z3_add_component(ackermannization + SOURCES + ackermannize_bv_model_converter.cpp + ackermannize_bv_tactic.cpp + ackr_bound_probe.cpp + ackr_helper.cpp + ackr_model_converter.cpp + lackr.cpp + lackr_model_constructor.cpp + lackr_model_converter_lazy.cpp + COMPONENT_DEPENDENCIES + ast + model + rewriter + solver + tactic + PYG_FILES + ackermannization_params.pyg + ackermannize_bv_tactic_params.pyg +) diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt new file mode 100644 index 00000000000..506b28cb307 --- /dev/null +++ b/src/api/CMakeLists.txt @@ -0,0 +1,86 @@ +set(api_header_files_to_scan + z3_api.h + z3_ast_containers.h + z3_algebraic.h + z3_polynomial.h + z3_rcf.h + z3_fixedpoint.h + z3_optimization.h + z3_interp.h + z3_fpa.h +) +set(generated_files + api_commands.cpp + api_log_macros.cpp + api_log_macros.h +) + +# Sanity check +foreach (gen_file ${generated_files}) + if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/${gen_file}") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/${gen_files}\"" + ${z3_polluted_tree_msg}) + endif() +endforeach() + +set(full_path_api_header_files_to_scan "") +foreach (header_file ${api_header_files_to_scan}) + list(APPEND full_path_api_header_files_to_scan "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}") +endforeach() +set(full_path_generated_files "") +foreach (gen_file ${generated_files}) + list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}") +endforeach() + +add_custom_command(OUTPUT ${generated_files} + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + "${CMAKE_CURRENT_BINARY_DIR}" + ${full_path_api_header_files_to_scan} + DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + ${full_path_api_header_files_to_scan} + COMMENT "Generating ${generated_files}" + USES_TERMINAL + VERBATIM +) + +z3_add_component(api + SOURCES + api_algebraic.cpp + api_arith.cpp + api_array.cpp + api_ast.cpp + api_ast_map.cpp + api_ast_vector.cpp + api_bv.cpp + api_config_params.cpp + api_context.cpp + api_datalog.cpp + api_datatype.cpp + api_fpa.cpp + api_goal.cpp + api_interp.cpp + api_log.cpp + api_model.cpp + api_numeral.cpp + api_opt.cpp + api_params.cpp + api_parsers.cpp + api_pb.cpp + api_polynomial.cpp + api_quant.cpp + api_rcf.cpp + api_seq.cpp + api_solver.cpp + api_stats.cpp + api_tactic.cpp + z3_replayer.cpp + ${full_path_generated_files} + COMPONENT_DEPENDENCIES + interp + opt + portfolio + realclosure + smtparser +) diff --git a/src/api/dll/CMakeLists.txt b/src/api/dll/CMakeLists.txt new file mode 100644 index 00000000000..31b0fb576c6 --- /dev/null +++ b/src/api/dll/CMakeLists.txt @@ -0,0 +1,13 @@ +set(api_dll_deps api extra_cmds sat) +z3_add_component(api_dll + SOURCES + dll.cpp + "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp" + "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp" + "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp" + COMPONENT_DEPENDENCIES + ${api_dll_deps} +) +z3_add_install_tactic_rule(${api_dll_deps}) +z3_add_memory_initializer_rule(${api_dll_deps}) +z3_add_gparams_register_modules_rule(${api_dll_deps}) diff --git a/src/ast/CMakeLists.txt b/src/ast/CMakeLists.txt new file mode 100644 index 00000000000..de0e4bdaf7c --- /dev/null +++ b/src/ast/CMakeLists.txt @@ -0,0 +1,48 @@ +z3_add_component(ast + SOURCES + act_cache.cpp + arith_decl_plugin.cpp + array_decl_plugin.cpp + ast.cpp + ast_ll_pp.cpp + ast_lt.cpp + ast_pp_util.cpp + ast_printer.cpp + ast_smt2_pp.cpp + ast_smt_pp.cpp + ast_translation.cpp + ast_util.cpp + bv_decl_plugin.cpp + datatype_decl_plugin.cpp + decl_collector.cpp + dl_decl_plugin.cpp + expr2polynomial.cpp + expr2var.cpp + expr_abstract.cpp + expr_functors.cpp + expr_map.cpp + expr_stat.cpp + expr_substitution.cpp + for_each_ast.cpp + for_each_expr.cpp + format.cpp + fpa_decl_plugin.cpp + func_decl_dependencies.cpp + has_free_vars.cpp + macro_substitution.cpp + num_occurs.cpp + occurs.cpp + pb_decl_plugin.cpp + pp.cpp + reg_decl_plugins.cpp + seq_decl_plugin.cpp + shared_occs.cpp + static_features.cpp + used_vars.cpp + well_sorted.cpp + COMPONENT_DEPENDENCIES + polynomial + util # Unnecessary? polynomial already depends on util + PYG_FILES + pp_params.pyg +) diff --git a/src/ast/fpa/CMakeLists.txt b/src/ast/fpa/CMakeLists.txt new file mode 100644 index 00000000000..12298b573b4 --- /dev/null +++ b/src/ast/fpa/CMakeLists.txt @@ -0,0 +1,10 @@ +z3_add_component(fpa + SOURCES + fpa2bv_converter.cpp + COMPONENT_DEPENDENCIES + ast + simplifier + util + PYG_FILES + fpa2bv_rewriter_params.pyg +) diff --git a/src/ast/macros/CMakeLists.txt b/src/ast/macros/CMakeLists.txt new file mode 100644 index 00000000000..ca38b4759c8 --- /dev/null +++ b/src/ast/macros/CMakeLists.txt @@ -0,0 +1,9 @@ +z3_add_component(macros + SOURCES + macro_finder.cpp + macro_manager.cpp + macro_util.cpp + quasi_macros.cpp + COMPONENT_DEPENDENCIES + simplifier +) diff --git a/src/ast/normal_forms/CMakeLists.txt b/src/ast/normal_forms/CMakeLists.txt new file mode 100644 index 00000000000..30702cd8c0f --- /dev/null +++ b/src/ast/normal_forms/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(normal_forms + SOURCES + defined_names.cpp + name_exprs.cpp + nnf.cpp + pull_quant.cpp + COMPONENT_DEPENDENCIES + rewriter + PYG_FILES + nnf_params.pyg +) diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt new file mode 100644 index 00000000000..1f8d43b0b83 --- /dev/null +++ b/src/ast/pattern/CMakeLists.txt @@ -0,0 +1,36 @@ +# If this code for adding the rule to generate the database file is ever needed +# for other components then we should refactor this code into +# z3_add_component() +if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/database.h") + message(FATAL_ERROR "The generated file \"database.h\"" + ${z3_polluted_tree_msg}) +endif() + +add_custom_command(OUTPUT "database.h" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py" + "${CMAKE_CURRENT_SOURCE_DIR}/database.smt2" + "${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" + COMMENT "Generating \"database.h\"" + USES_TERMINAL + VERBATIM +) + +z3_add_component(pattern + SOURCES + expr_pattern_match.cpp + pattern_inference.cpp + pattern_inference_params.cpp + # Let CMake know this target depends on this generated + # header file + ${CMAKE_CURRENT_BINARY_DIR}/database.h + COMPONENT_DEPENDENCIES + normal_forms + simplifier + smt2parser + PYG_FILES + pattern_inference_params_helper.pyg +) diff --git a/src/ast/proof_checker/CMakeLists.txt b/src/ast/proof_checker/CMakeLists.txt new file mode 100644 index 00000000000..5c947adec48 --- /dev/null +++ b/src/ast/proof_checker/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(proof_checker + SOURCES + proof_checker.cpp + COMPONENT_DEPENDENCIES + rewriter +) diff --git a/src/ast/rewriter/CMakeLists.txt b/src/ast/rewriter/CMakeLists.txt new file mode 100644 index 00000000000..59834ea1316 --- /dev/null +++ b/src/ast/rewriter/CMakeLists.txt @@ -0,0 +1,34 @@ +z3_add_component(rewriter + SOURCES + arith_rewriter.cpp + array_rewriter.cpp + ast_counter.cpp + bool_rewriter.cpp + bv_rewriter.cpp + datatype_rewriter.cpp + der.cpp + dl_rewriter.cpp + expr_replacer.cpp + expr_safe_replace.cpp + factor_rewriter.cpp + fpa_rewriter.cpp + mk_simplified_app.cpp + pb_rewriter.cpp + quant_hoist.cpp + rewriter.cpp + seq_rewriter.cpp + th_rewriter.cpp + var_subst.cpp + COMPONENT_DEPENDENCIES + ast + automata + polynomial + PYG_FILES + arith_rewriter_params.pyg + array_rewriter_params.pyg + bool_rewriter_params.pyg + bv_rewriter_params.pyg + fpa_rewriter_params.pyg + poly_rewriter_params.pyg + rewriter_params.pyg +) diff --git a/src/ast/rewriter/bit_blaster/CMakeLists.txt b/src/ast/rewriter/bit_blaster/CMakeLists.txt new file mode 100644 index 00000000000..9eea1558ec7 --- /dev/null +++ b/src/ast/rewriter/bit_blaster/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(bit_blaster + SOURCES + bit_blaster.cpp + bit_blaster_rewriter.cpp + COMPONENT_DEPENDENCIES + rewriter + simplifier +) diff --git a/src/ast/simplifier/CMakeLists.txt b/src/ast/simplifier/CMakeLists.txt new file mode 100644 index 00000000000..7597374a614 --- /dev/null +++ b/src/ast/simplifier/CMakeLists.txt @@ -0,0 +1,30 @@ +z3_add_component(simplifier + SOURCES + arith_simplifier_params.cpp + arith_simplifier_plugin.cpp + array_simplifier_params.cpp + array_simplifier_plugin.cpp + basic_simplifier_plugin.cpp + bit2int.cpp + bv_elim.cpp + bv_simplifier_params.cpp + bv_simplifier_plugin.cpp + datatype_simplifier_plugin.cpp + distribute_forall.cpp + elim_bounds.cpp + fpa_simplifier_plugin.cpp + inj_axiom.cpp + maximise_ac_sharing.cpp + poly_simplifier_plugin.cpp + pull_ite_tree.cpp + push_app_ite.cpp + seq_simplifier_plugin.cpp + simplifier.cpp + simplifier_plugin.cpp + COMPONENT_DEPENDENCIES + rewriter + PYG_FILES + arith_simplifier_params_helper.pyg + array_simplifier_params_helper.pyg + bv_simplifier_params_helper.pyg +) diff --git a/src/ast/substitution/CMakeLists.txt b/src/ast/substitution/CMakeLists.txt new file mode 100644 index 00000000000..80e12c9953b --- /dev/null +++ b/src/ast/substitution/CMakeLists.txt @@ -0,0 +1,10 @@ +z3_add_component(substitution + SOURCES + matcher.cpp + substitution.cpp + substitution_tree.cpp + unifier.cpp + COMPONENT_DEPENDENCIES + ast + rewriter +) diff --git a/src/cmd_context/CMakeLists.txt b/src/cmd_context/CMakeLists.txt new file mode 100644 index 00000000000..8b2d10eec0e --- /dev/null +++ b/src/cmd_context/CMakeLists.txt @@ -0,0 +1,21 @@ +z3_add_component(cmd_context + SOURCES + basic_cmds.cpp + check_logic.cpp + cmd_context.cpp + cmd_context_to_goal.cpp + cmd_util.cpp + context_params.cpp + echo_tactic.cpp + eval_cmd.cpp + interpolant_cmds.cpp + parametric_cmd.cpp + pdecl.cpp + simplify_cmd.cpp + tactic_cmds.cpp + tactic_manager.cpp + COMPONENT_DEPENDENCIES + interp + rewriter + solver +) diff --git a/src/cmd_context/extra_cmds/CMakeLists.txt b/src/cmd_context/extra_cmds/CMakeLists.txt new file mode 100644 index 00000000000..3aef1a55396 --- /dev/null +++ b/src/cmd_context/extra_cmds/CMakeLists.txt @@ -0,0 +1,10 @@ +z3_add_component(extra_cmds + SOURCES + dbg_cmds.cpp + polynomial_cmds.cpp + subpaving_cmds.cpp + COMPONENT_DEPENDENCIES + arith_tactics + cmd_context + subpaving_tactic +) diff --git a/src/duality/CMakeLists.txt b/src/duality/CMakeLists.txt new file mode 100644 index 00000000000..eb2d5c4f287 --- /dev/null +++ b/src/duality/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(duality + SOURCES + duality_profiling.cpp + duality_rpfp.cpp + duality_solver.cpp + duality_wrapper.cpp + COMPONENT_DEPENDENCIES + interp + qe + smt +) diff --git a/src/interp/CMakeLists.txt b/src/interp/CMakeLists.txt new file mode 100644 index 00000000000..949811b93f2 --- /dev/null +++ b/src/interp/CMakeLists.txt @@ -0,0 +1,19 @@ +z3_add_component(interp + SOURCES + iz3base.cpp + iz3checker.cpp + iz3foci.cpp + iz3interp.cpp + iz3mgr.cpp + iz3pp.cpp + iz3profiling.cpp + iz3proof.cpp + iz3proof_itp.cpp + iz3scopes.cpp + iz3translate.cpp + iz3translate_direct.cpp + COMPONENT_DEPENDENCIES + solver + PYG_FILES + interp_params.pyg +) diff --git a/src/interp/iz3params.pyg b/src/interp/interp_params.pyg similarity index 100% rename from src/interp/iz3params.pyg rename to src/interp/interp_params.pyg diff --git a/src/math/automata/CMakeLists.txt b/src/math/automata/CMakeLists.txt new file mode 100644 index 00000000000..1fffd24a84f --- /dev/null +++ b/src/math/automata/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(automata + SOURCES + automaton.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/src/math/euclid/CMakeLists.txt b/src/math/euclid/CMakeLists.txt new file mode 100644 index 00000000000..a72f02b2809 --- /dev/null +++ b/src/math/euclid/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(euclid + SOURCES + euclidean_solver.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/src/math/grobner/CMakeLists.txt b/src/math/grobner/CMakeLists.txt new file mode 100644 index 00000000000..1b56c775fdb --- /dev/null +++ b/src/math/grobner/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(grobner + SOURCES + grobner.cpp + COMPONENT_DEPENDENCIES + ast +) diff --git a/src/math/hilbert/CMakeLists.txt b/src/math/hilbert/CMakeLists.txt new file mode 100644 index 00000000000..2e44140b8ad --- /dev/null +++ b/src/math/hilbert/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(hilbert + SOURCES + hilbert_basis.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/src/math/interval/CMakeLists.txt b/src/math/interval/CMakeLists.txt new file mode 100644 index 00000000000..390529b9dff --- /dev/null +++ b/src/math/interval/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(interval + SOURCES + interval_mpq.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/src/math/polynomial/CMakeLists.txt b/src/math/polynomial/CMakeLists.txt new file mode 100644 index 00000000000..1792f50aaa5 --- /dev/null +++ b/src/math/polynomial/CMakeLists.txt @@ -0,0 +1,16 @@ +z3_add_component(polynomial + SOURCES + algebraic_numbers.cpp + polynomial_cache.cpp + polynomial.cpp + polynomial_factorization.cpp + rpolynomial.cpp + sexpr2upolynomial.cpp + upolynomial.cpp + upolynomial_factorization.cpp + COMPONENT_DEPENDENCIES + util + PYG_FILES + algebraic_params.pyg +) + diff --git a/src/math/polynomial/algebraic.pyg b/src/math/polynomial/algebraic_params.pyg similarity index 100% rename from src/math/polynomial/algebraic.pyg rename to src/math/polynomial/algebraic_params.pyg diff --git a/src/math/realclosure/CMakeLists.txt b/src/math/realclosure/CMakeLists.txt new file mode 100644 index 00000000000..beb5f147b54 --- /dev/null +++ b/src/math/realclosure/CMakeLists.txt @@ -0,0 +1,9 @@ +z3_add_component(realclosure + SOURCES + mpz_matrix.cpp + realclosure.cpp + COMPONENT_DEPENDENCIES + interval + PYG_FILES + rcf_params.pyg +) diff --git a/src/math/realclosure/rcf.pyg b/src/math/realclosure/rcf_params.pyg similarity index 100% rename from src/math/realclosure/rcf.pyg rename to src/math/realclosure/rcf_params.pyg diff --git a/src/math/simplex/CMakeLists.txt b/src/math/simplex/CMakeLists.txt new file mode 100644 index 00000000000..6f965919d5a --- /dev/null +++ b/src/math/simplex/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(simplex + SOURCES + simplex.cpp + COMPONENT_DEPENDENCIES + util +) diff --git a/src/math/subpaving/CMakeLists.txt b/src/math/subpaving/CMakeLists.txt new file mode 100644 index 00000000000..be88f63cd1f --- /dev/null +++ b/src/math/subpaving/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(subpaving + SOURCES + subpaving.cpp + subpaving_hwf.cpp + subpaving_mpf.cpp + subpaving_mpff.cpp + subpaving_mpfx.cpp + subpaving_mpq.cpp + COMPONENT_DEPENDENCIES + interval +) diff --git a/src/math/subpaving/tactic/CMakeLists.txt b/src/math/subpaving/tactic/CMakeLists.txt new file mode 100644 index 00000000000..eedb0ed4da1 --- /dev/null +++ b/src/math/subpaving/tactic/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(subpaving_tactic + SOURCES + expr2subpaving.cpp + subpaving_tactic.cpp + COMPONENT_DEPENDENCIES + core_tactics + subpaving +) diff --git a/src/model/CMakeLists.txt b/src/model/CMakeLists.txt new file mode 100644 index 00000000000..0e685e07cf5 --- /dev/null +++ b/src/model/CMakeLists.txt @@ -0,0 +1,18 @@ +z3_add_component(model + SOURCES + func_interp.cpp + model2expr.cpp + model_core.cpp + model.cpp + model_evaluator.cpp + model_implicant.cpp + model_pp.cpp + model_smt2_pp.cpp + model_v2_pp.cpp + COMPONENT_DEPENDENCIES + rewriter + PYG_FILES + model_evaluator_params.pyg + model_params.pyg +) + diff --git a/src/muz/base/CMakeLists.txt b/src/muz/base/CMakeLists.txt new file mode 100644 index 00000000000..ec1ce47c301 --- /dev/null +++ b/src/muz/base/CMakeLists.txt @@ -0,0 +1,23 @@ +z3_add_component(muz + SOURCES + bind_variables.cpp + dl_boogie_proof.cpp + dl_context.cpp + dl_costs.cpp + dl_rule.cpp + dl_rule_set.cpp + dl_rule_subsumption_index.cpp + dl_rule_transformer.cpp + dl_util.cpp + hnf.cpp + proof_utils.cpp + rule_properties.cpp + COMPONENT_DEPENDENCIES + aig_tactic + qe + sat + smt + smt2parser + PYG_FILES + fixedpoint_params.pyg +) diff --git a/src/muz/bmc/CMakeLists.txt b/src/muz/bmc/CMakeLists.txt new file mode 100644 index 00000000000..dcd99898e85 --- /dev/null +++ b/src/muz/bmc/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(bmc + SOURCES + dl_bmc_engine.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/src/muz/clp/CMakeLists.txt b/src/muz/clp/CMakeLists.txt new file mode 100644 index 00000000000..32d9a928ebf --- /dev/null +++ b/src/muz/clp/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(clp + SOURCES + clp_context.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/src/muz/dataflow/CMakeLists.txt b/src/muz/dataflow/CMakeLists.txt new file mode 100644 index 00000000000..3fc1e1f1955 --- /dev/null +++ b/src/muz/dataflow/CMakeLists.txt @@ -0,0 +1,6 @@ +z3_add_component(dataflow + SOURCES + dataflow.cpp + COMPONENT_DEPENDENCIES + muz +) diff --git a/src/muz/ddnf/CMakeLists.txt b/src/muz/ddnf/CMakeLists.txt new file mode 100644 index 00000000000..55d6bae5d25 --- /dev/null +++ b/src/muz/ddnf/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(ddnf + SOURCES + ddnf.cpp + COMPONENT_DEPENDENCIES + muz + rel + transforms +) diff --git a/src/muz/duality/CMakeLists.txt b/src/muz/duality/CMakeLists.txt new file mode 100644 index 00000000000..f005b88b1c4 --- /dev/null +++ b/src/muz/duality/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(duality_intf + SOURCES + duality_dl_interface.cpp + COMPONENT_DEPENDENCIES + duality + muz + transforms +) diff --git a/src/muz/fp/CMakeLists.txt b/src/muz/fp/CMakeLists.txt new file mode 100644 index 00000000000..239c4df124b --- /dev/null +++ b/src/muz/fp/CMakeLists.txt @@ -0,0 +1,16 @@ +z3_add_component(fp + SOURCES + datalog_parser.cpp + dl_cmds.cpp + dl_register_engine.cpp + horn_tactic.cpp + COMPONENT_DEPENDENCIES + bmc + clp + ddnf + duality_intf + muz + pdr + rel + tab +) diff --git a/src/muz/pdr/CMakeLists.txt b/src/muz/pdr/CMakeLists.txt new file mode 100644 index 00000000000..ca2992b9792 --- /dev/null +++ b/src/muz/pdr/CMakeLists.txt @@ -0,0 +1,20 @@ +z3_add_component(pdr + SOURCES + pdr_closure.cpp + pdr_context.cpp + pdr_dl_interface.cpp + pdr_farkas_learner.cpp + pdr_generalizers.cpp + pdr_manager.cpp + pdr_prop_solver.cpp + pdr_reachable_cache.cpp + pdr_smt_context_manager.cpp + pdr_sym_mux.cpp + pdr_util.cpp + COMPONENT_DEPENDENCIES + arith_tactics + core_tactics + muz + smt_tactic + transforms +) diff --git a/src/muz/rel/CMakeLists.txt b/src/muz/rel/CMakeLists.txt new file mode 100644 index 00000000000..720714ed854 --- /dev/null +++ b/src/muz/rel/CMakeLists.txt @@ -0,0 +1,32 @@ +z3_add_component(rel + SOURCES + aig_exporter.cpp + check_relation.cpp + dl_base.cpp + dl_bound_relation.cpp + dl_check_table.cpp + dl_compiler.cpp + dl_external_relation.cpp + dl_finite_product_relation.cpp + dl_instruction.cpp + dl_interval_relation.cpp + dl_lazy_table.cpp + dl_mk_explanations.cpp + dl_mk_partial_equiv.cpp + dl_mk_similarity_compressor.cpp + dl_mk_simple_joins.cpp + dl_product_relation.cpp + dl_relation_manager.cpp + dl_sieve_relation.cpp + dl_sparse_table.cpp + dl_table.cpp + dl_table_relation.cpp + doc.cpp + karr_relation.cpp + rel_context.cpp + tbv.cpp + udoc_relation.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/src/muz/tab/CMakeLists.txt b/src/muz/tab/CMakeLists.txt new file mode 100644 index 00000000000..cfae51280a0 --- /dev/null +++ b/src/muz/tab/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(tab + SOURCES + tab_context.cpp + COMPONENT_DEPENDENCIES + muz + transforms +) diff --git a/src/muz/transforms/CMakeLists.txt b/src/muz/transforms/CMakeLists.txt new file mode 100644 index 00000000000..6a0a1ac9c23 --- /dev/null +++ b/src/muz/transforms/CMakeLists.txt @@ -0,0 +1,28 @@ +z3_add_component(transforms + SOURCES + dl_mk_array_blast.cpp + dl_mk_backwards.cpp + dl_mk_bit_blast.cpp + dl_mk_coalesce.cpp + dl_mk_coi_filter.cpp + dl_mk_filter_rules.cpp + dl_mk_interp_tail_simplifier.cpp + dl_mk_karr_invariants.cpp + dl_mk_loop_counter.cpp + dl_mk_magic_sets.cpp + dl_mk_magic_symbolic.cpp + dl_mk_quantifier_abstraction.cpp + dl_mk_quantifier_instantiation.cpp + dl_mk_rule_inliner.cpp + dl_mk_scale.cpp + dl_mk_separate_negated_tails.cpp + dl_mk_slice.cpp + dl_mk_subsumption_checker.cpp + dl_mk_unbound_compressor.cpp + dl_mk_unfold.cpp + dl_transforms.cpp + COMPONENT_DEPENDENCIES + dataflow + hilbert + muz +) diff --git a/src/nlsat/CMakeLists.txt b/src/nlsat/CMakeLists.txt new file mode 100644 index 00000000000..d0c1379e586 --- /dev/null +++ b/src/nlsat/CMakeLists.txt @@ -0,0 +1,14 @@ +z3_add_component(nlsat + SOURCES + nlsat_clause.cpp + nlsat_evaluator.cpp + nlsat_explain.cpp + nlsat_interval_set.cpp + nlsat_solver.cpp + nlsat_types.cpp + COMPONENT_DEPENDENCIES + polynomial + sat + PYG_FILES + nlsat_params.pyg +) diff --git a/src/nlsat/tactic/CMakeLists.txt b/src/nlsat/tactic/CMakeLists.txt new file mode 100644 index 00000000000..9ea26a0c586 --- /dev/null +++ b/src/nlsat/tactic/CMakeLists.txt @@ -0,0 +1,10 @@ +z3_add_component(nlsat_tactic + SOURCES + goal2nlsat.cpp + nlsat_tactic.cpp + qfnra_nlsat_tactic.cpp + COMPONENT_DEPENDENCIES + arith_tactics + nlsat + sat_tactic +) diff --git a/src/opt/CMakeLists.txt b/src/opt/CMakeLists.txt new file mode 100644 index 00000000000..c50f8be52bb --- /dev/null +++ b/src/opt/CMakeLists.txt @@ -0,0 +1,26 @@ +z3_add_component(opt + SOURCES + bcd2.cpp + fu_malik.cpp + hitting_sets.cpp + maxhs.cpp + maxres.cpp + maxsls.cpp + maxsmt.cpp + mss.cpp + mus.cpp + opt_cmds.cpp + opt_context.cpp + opt_pareto.cpp + optsmt.cpp + opt_solver.cpp + pb_sls.cpp + wmax.cpp + COMPONENT_DEPENDENCIES + sat_solver + sls_tactic + smt + smtlogic_tactics + PYG_FILES + opt_params.pyg +) diff --git a/src/parsers/smt/CMakeLists.txt b/src/parsers/smt/CMakeLists.txt new file mode 100644 index 00000000000..2edf7b6794d --- /dev/null +++ b/src/parsers/smt/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(smtparser + SOURCES + smtlib.cpp + smtlib_solver.cpp + smtparser.cpp + COMPONENT_DEPENDENCIES + portfolio +) diff --git a/src/parsers/smt2/CMakeLists.txt b/src/parsers/smt2/CMakeLists.txt new file mode 100644 index 00000000000..1467d95c6f1 --- /dev/null +++ b/src/parsers/smt2/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(smt2parser + SOURCES + smt2parser.cpp + smt2scanner.cpp + COMPONENT_DEPENDENCIES + cmd_context + parser_util +) diff --git a/src/parsers/util/CMakeLists.txt b/src/parsers/util/CMakeLists.txt new file mode 100644 index 00000000000..6ede4b77305 --- /dev/null +++ b/src/parsers/util/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(parser_util + SOURCES + cost_parser.cpp + pattern_validation.cpp + scanner.cpp + simple_parser.cpp + COMPONENT_DEPENDENCIES + ast + PYG_FILES + parser_params.pyg +) diff --git a/src/qe/CMakeLists.txt b/src/qe/CMakeLists.txt new file mode 100644 index 00000000000..9db253bd605 --- /dev/null +++ b/src/qe/CMakeLists.txt @@ -0,0 +1,21 @@ +z3_add_component(qe + SOURCES + nlarith_util.cpp + qe_arith.cpp + qe_arith_plugin.cpp + qe_array_plugin.cpp + qe_bool_plugin.cpp + qe_bv_plugin.cpp + qe_cmd.cpp + qe.cpp + qe_datatype_plugin.cpp + qe_dl_plugin.cpp + qe_lite.cpp + qe_sat_tactic.cpp + qe_tactic.cpp + qe_util.cpp + vsubst_tactic.cpp + COMPONENT_DEPENDENCIES + sat + smt +) diff --git a/src/sat/CMakeLists.txt b/src/sat/CMakeLists.txt new file mode 100644 index 00000000000..cfc3835c11b --- /dev/null +++ b/src/sat/CMakeLists.txt @@ -0,0 +1,29 @@ +z3_add_component(sat + SOURCES + dimacs.cpp + sat_asymm_branch.cpp + sat_bceq.cpp + sat_clause.cpp + sat_clause_set.cpp + sat_clause_use_list.cpp + sat_cleaner.cpp + sat_config.cpp + sat_elim_eqs.cpp + sat_iff3_finder.cpp + sat_integrity_checker.cpp + sat_model_converter.cpp + sat_mus.cpp + sat_probing.cpp + sat_scc.cpp + sat_simplifier.cpp + sat_sls.cpp + sat_solver.cpp + sat_watched.cpp + COMPONENT_DEPENDENCIES + util + PYG_FILES + sat_asymm_branch_params.pyg + sat_params.pyg + sat_scc_params.pyg + sat_simplifier_params.pyg +) diff --git a/src/sat/sat_solver/CMakeLists.txt b/src/sat/sat_solver/CMakeLists.txt new file mode 100644 index 00000000000..14eb4ac2550 --- /dev/null +++ b/src/sat/sat_solver/CMakeLists.txt @@ -0,0 +1,11 @@ +z3_add_component(sat_solver + SOURCES + inc_sat_solver.cpp + COMPONENT_DEPENDENCIES + aig_tactic + arith_tactics + bv_tactics + core_tactics + sat_tactic + solver +) diff --git a/src/sat/tactic/CMakeLists.txt b/src/sat/tactic/CMakeLists.txt new file mode 100644 index 00000000000..74aeba8b962 --- /dev/null +++ b/src/sat/tactic/CMakeLists.txt @@ -0,0 +1,9 @@ +z3_add_component(sat_tactic + SOURCES + atom2bool_var.cpp + goal2sat.cpp + sat_tactic.cpp + COMPONENT_DEPENDENCIES + sat + tactic +) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt new file mode 100644 index 00000000000..82113bbb7ab --- /dev/null +++ b/src/shell/CMakeLists.txt @@ -0,0 +1,47 @@ +set (shell_object_files "") +# FIXME: z3 should really link against libz3 and not the +# individual components. Several things prevent us from +# doing this +# * The api_dll component in libz3 shouldn't be used the +# the z3 executable. +# * The z3 executable uses symbols that are hidden in libz3 + +# We are only using these dependencies to enforce a build +# order. We don't use this list for actual linking. +set(shell_deps api extra_cmds opt sat) +z3_expand_dependencies(shell_expanded_deps ${shell_deps}) +get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS) +foreach (component ${Z3_LIBZ3_COMPONENTS_LIST}) + if ("${component}" STREQUAL "api_dll") + # We don't use the api_dll component in the Z3 executable + continue() + endif() + list(APPEND shell_object_files $) +endforeach() +add_executable(shell + datalog_frontend.cpp + dimacs_frontend.cpp + "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp" + "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp" + main.cpp + "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp" + opt_frontend.cpp + smtlib_frontend.cpp + z3_log_frontend.cpp +# FIXME: shell should really link against libz3 but it can't due to requiring +# use of some hidden symbols. Also libz3 has the ``api_dll`` component which +# we don't want (I think). + ${shell_object_files} +) +z3_add_install_tactic_rule(${shell_deps}) +z3_add_memory_initializer_rule(${shell_deps}) +z3_add_gparams_register_modules_rule(${shell_deps}) +set_target_properties(shell PROPERTIES OUTPUT_NAME z3) +target_compile_definitions(shell PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) +target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) +target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS}) +z3_add_component_dependencies_to_target(shell ${shell_expanded_deps}) +install(TARGETS shell + RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}" +) diff --git a/src/smt/CMakeLists.txt b/src/smt/CMakeLists.txt new file mode 100644 index 00000000000..e9306b2d693 --- /dev/null +++ b/src/smt/CMakeLists.txt @@ -0,0 +1,77 @@ +z3_add_component(smt + SOURCES + arith_eq_adapter.cpp + arith_eq_solver.cpp + asserted_formulas.cpp + cached_var_subst.cpp + cost_evaluator.cpp + dyn_ack.cpp + elim_term_ite.cpp + expr_context_simplifier.cpp + fingerprints.cpp + mam.cpp + old_interval.cpp + qi_queue.cpp + smt_almost_cg_table.cpp + smt_case_split_queue.cpp + smt_cg_table.cpp + smt_checker.cpp + smt_clause.cpp + smt_conflict_resolution.cpp + smt_context.cpp + smt_context_inv.cpp + smt_context_pp.cpp + smt_context_stat.cpp + smt_enode.cpp + smt_farkas_util.cpp + smt_for_each_relevant_expr.cpp + smt_implied_equalities.cpp + smt_internalizer.cpp + smt_justification.cpp + smt_kernel.cpp + smt_literal.cpp + smt_model_checker.cpp + smt_model_finder.cpp + smt_model_generator.cpp + smt_quantifier.cpp + smt_quantifier_stat.cpp + smt_quick_checker.cpp + smt_relevancy.cpp + smt_setup.cpp + smt_solver.cpp + smt_statistics.cpp + smt_theory.cpp + smt_value_sort.cpp + theory_arith.cpp + theory_array_base.cpp + theory_array.cpp + theory_array_full.cpp + theory_bv.cpp + theory_datatype.cpp + theory_dense_diff_logic.cpp + theory_diff_logic.cpp + theory_dl.cpp + theory_dummy.cpp + theory_fpa.cpp + theory_opt.cpp + theory_pb.cpp + theory_seq.cpp + theory_utvpi.cpp + theory_wmaxsat.cpp + uses_theory.cpp + watch_list.cpp + COMPONENT_DEPENDENCIES + bit_blaster + cmd_context + euclid + fpa + grobner + macros + normal_forms + parser_util + pattern + proof_checker + proto_model + simplex + substitution +) diff --git a/src/smt/params/CMakeLists.txt b/src/smt/params/CMakeLists.txt new file mode 100644 index 00000000000..67224a2876b --- /dev/null +++ b/src/smt/params/CMakeLists.txt @@ -0,0 +1,18 @@ +z3_add_component(smt_params + SOURCES + dyn_ack_params.cpp + preprocessor_params.cpp + qi_params.cpp + smt_params.cpp + theory_arith_params.cpp + theory_array_params.cpp + theory_bv_params.cpp + theory_pb_params.cpp + COMPONENT_DEPENDENCIES + ast + bit_blaster + pattern + simplifier + PYG_FILES + smt_params_helper.pyg +) diff --git a/src/smt/proto_model/CMakeLists.txt b/src/smt/proto_model/CMakeLists.txt new file mode 100644 index 00000000000..0539c0fb0c6 --- /dev/null +++ b/src/smt/proto_model/CMakeLists.txt @@ -0,0 +1,13 @@ +z3_add_component(proto_model + SOURCES + array_factory.cpp + datatype_factory.cpp + numeral_factory.cpp + proto_model.cpp + struct_factory.cpp + value_factory.cpp + COMPONENT_DEPENDENCIES + model + simplifier + smt_params +) diff --git a/src/smt/tactic/CMakeLists.txt b/src/smt/tactic/CMakeLists.txt new file mode 100644 index 00000000000..b7525bda846 --- /dev/null +++ b/src/smt/tactic/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(smt_tactic + SOURCES + ctx_solver_simplify_tactic.cpp + smt_tactic.cpp + unit_subsumption_tactic.cpp + COMPONENT_DEPENDENCIES + smt +) diff --git a/src/solver/CMakeLists.txt b/src/solver/CMakeLists.txt new file mode 100644 index 00000000000..5e76c91ce76 --- /dev/null +++ b/src/solver/CMakeLists.txt @@ -0,0 +1,13 @@ +z3_add_component(solver + SOURCES + check_sat_result.cpp + combined_solver.cpp + solver.cpp + solver_na2as.cpp + tactic2solver.cpp + COMPONENT_DEPENDENCIES + model + tactic + PYG_FILES + combined_solver_params.pyg +) diff --git a/src/tactic/CMakeLists.txt b/src/tactic/CMakeLists.txt new file mode 100644 index 00000000000..318803cd218 --- /dev/null +++ b/src/tactic/CMakeLists.txt @@ -0,0 +1,20 @@ +z3_add_component(tactic + SOURCES + equiv_proof_converter.cpp + extension_model_converter.cpp + filter_model_converter.cpp + goal.cpp + goal_num_occurs.cpp + goal_shared_occs.cpp + goal_util.cpp + horn_subsume_model_converter.cpp + model_converter.cpp + probe.cpp + proof_converter.cpp + replace_proof_converter.cpp + tactical.cpp + tactic.cpp + COMPONENT_DEPENDENCIES + ast + model +) diff --git a/src/tactic/aig/CMakeLists.txt b/src/tactic/aig/CMakeLists.txt new file mode 100644 index 00000000000..1e1a0d26690 --- /dev/null +++ b/src/tactic/aig/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(aig_tactic + SOURCES + aig.cpp + aig_tactic.cpp + COMPONENT_DEPENDENCIES + tactic +) diff --git a/src/tactic/arith/CMakeLists.txt b/src/tactic/arith/CMakeLists.txt new file mode 100644 index 00000000000..cdc42367a2b --- /dev/null +++ b/src/tactic/arith/CMakeLists.txt @@ -0,0 +1,31 @@ +z3_add_component(arith_tactics + SOURCES + add_bounds_tactic.cpp + arith_bounds_tactic.cpp + bound_manager.cpp + bound_propagator.cpp + bv2int_rewriter.cpp + bv2real_rewriter.cpp + card2bv_tactic.cpp + degree_shift_tactic.cpp + diff_neq_tactic.cpp + elim01_tactic.cpp + eq2bv_tactic.cpp + factor_tactic.cpp + fix_dl_var_tactic.cpp + fm_tactic.cpp + lia2card_tactic.cpp + lia2pb_tactic.cpp + linear_equation.cpp + nla2bv_tactic.cpp + normalize_bounds_tactic.cpp + pb2bv_model_converter.cpp + pb2bv_tactic.cpp + probe_arith.cpp + propagate_ineqs_tactic.cpp + purify_arith_tactic.cpp + recover_01_tactic.cpp + COMPONENT_DEPENDENCIES + core_tactics + sat +) diff --git a/src/tactic/bv/CMakeLists.txt b/src/tactic/bv/CMakeLists.txt new file mode 100644 index 00000000000..42cff2bfc33 --- /dev/null +++ b/src/tactic/bv/CMakeLists.txt @@ -0,0 +1,16 @@ +z3_add_component(bv_tactics + SOURCES + bit_blaster_model_converter.cpp + bit_blaster_tactic.cpp + bv1_blaster_tactic.cpp + bvarray2uf_rewriter.cpp + bvarray2uf_tactic.cpp + bv_bounds_tactic.cpp + bv_size_reduction_tactic.cpp + elim_small_bv_tactic.cpp + max_bv_sharing_tactic.cpp + COMPONENT_DEPENDENCIES + bit_blaster + core_tactics + tactic +) diff --git a/src/tactic/core/CMakeLists.txt b/src/tactic/core/CMakeLists.txt new file mode 100644 index 00000000000..d59265c5cda --- /dev/null +++ b/src/tactic/core/CMakeLists.txt @@ -0,0 +1,25 @@ +z3_add_component(core_tactics + SOURCES + blast_term_ite_tactic.cpp + cofactor_elim_term_ite.cpp + cofactor_term_ite_tactic.cpp + ctx_simplify_tactic.cpp + der_tactic.cpp + distribute_forall_tactic.cpp + elim_term_ite_tactic.cpp + elim_uncnstr_tactic.cpp + nnf_tactic.cpp + occf_tactic.cpp + pb_preprocess_tactic.cpp + propagate_values_tactic.cpp + reduce_args_tactic.cpp + simplify_tactic.cpp + solve_eqs_tactic.cpp + split_clause_tactic.cpp + symmetry_reduce_tactic.cpp + tseitin_cnf_tactic.cpp + COMPONENT_DEPENDENCIES + normal_forms + tactic +) + diff --git a/src/tactic/fpa/CMakeLists.txt b/src/tactic/fpa/CMakeLists.txt new file mode 100644 index 00000000000..d93cd5b821d --- /dev/null +++ b/src/tactic/fpa/CMakeLists.txt @@ -0,0 +1,14 @@ +z3_add_component(fpa_tactics + SOURCES + fpa2bv_model_converter.cpp + fpa2bv_tactic.cpp + qffp_tactic.cpp + COMPONENT_DEPENDENCIES + arith_tactics + bv_tactics + core_tactics + fpa + sat_tactic + smtlogic_tactics + smt_tactic +) diff --git a/src/tactic/nlsat_smt/CMakeLists.txt b/src/tactic/nlsat_smt/CMakeLists.txt new file mode 100644 index 00000000000..e28b1196651 --- /dev/null +++ b/src/tactic/nlsat_smt/CMakeLists.txt @@ -0,0 +1,7 @@ +z3_add_component(nlsat_smt_tactic + SOURCES + nl_purify_tactic.cpp + COMPONENT_DEPENDENCIES + nlsat_tactic + smt_tactic +) diff --git a/src/tactic/portfolio/CMakeLists.txt b/src/tactic/portfolio/CMakeLists.txt new file mode 100644 index 00000000000..d20af772b8b --- /dev/null +++ b/src/tactic/portfolio/CMakeLists.txt @@ -0,0 +1,15 @@ +z3_add_component(portfolio + SOURCES + default_tactic.cpp + smt_strategic_solver.cpp + COMPONENT_DEPENDENCIES + aig_tactic + fp + fpa_tactics + qe + sat_solver + sls_tactic + smtlogic_tactics + subpaving_tactic + ufbv_tactic +) diff --git a/src/tactic/sls/CMakeLists.txt b/src/tactic/sls/CMakeLists.txt new file mode 100644 index 00000000000..8b720b333dc --- /dev/null +++ b/src/tactic/sls/CMakeLists.txt @@ -0,0 +1,13 @@ +z3_add_component(sls_tactic + SOURCES + bvsls_opt_engine.cpp + sls_engine.cpp + sls_tactic.cpp + COMPONENT_DEPENDENCIES + bv_tactics + core_tactics + normal_forms + tactic + PYG_FILES + sls_params.pyg +) diff --git a/src/tactic/smtlogics/CMakeLists.txt b/src/tactic/smtlogics/CMakeLists.txt new file mode 100644 index 00000000000..840dd008a7c --- /dev/null +++ b/src/tactic/smtlogics/CMakeLists.txt @@ -0,0 +1,31 @@ +z3_add_component(smtlogic_tactics + SOURCES + nra_tactic.cpp + qfaufbv_tactic.cpp + qfauflia_tactic.cpp + qfbv_tactic.cpp + qfidl_tactic.cpp + qflia_tactic.cpp + qflra_tactic.cpp + qfnia_tactic.cpp + qfnra_tactic.cpp + qfufbv_ackr_model_converter.cpp + qfufbv_tactic.cpp + qfufnra_tactic.cpp + qfuf_tactic.cpp + quant_tactics.cpp + COMPONENT_DEPENDENCIES + ackermannization + aig_tactic + arith_tactics + bv_tactics + fp + muz + nlsat_tactic + nlsat_smt_tactic + qe + sat_solver + smt_tactic + PYG_FILES + qfufbv_tactic_params.pyg +) diff --git a/src/tactic/ufbv/CMakeLists.txt b/src/tactic/ufbv/CMakeLists.txt new file mode 100644 index 00000000000..c1d6daaaa18 --- /dev/null +++ b/src/tactic/ufbv/CMakeLists.txt @@ -0,0 +1,14 @@ +z3_add_component(ufbv_tactic + SOURCES + macro_finder_tactic.cpp + quasi_macros_tactic.cpp + ufbv_rewriter.cpp + ufbv_rewriter_tactic.cpp + ufbv_tactic.cpp + COMPONENT_DEPENDENCIES + core_tactics + macros + normal_forms + rewriter + smt_tactic +) diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt new file mode 100644 index 00000000000..0217e99b6bc --- /dev/null +++ b/src/test/CMakeLists.txt @@ -0,0 +1,125 @@ +add_subdirectory(fuzzing) +################################################################################ +# z3-test executable +################################################################################ +set(z3_test_deps api fuzzing simplex) +z3_expand_dependencies(z3_test_expanded_deps ${z3_test_deps}) +set (z3_test_extra_object_files "") +foreach (component ${z3_test_expanded_deps}) + list(APPEND z3_test_extra_object_files $) +endforeach() +add_executable(test-z3 + EXCLUDE_FROM_ALL + algebraic.cpp + api_bug.cpp + api.cpp + arith_rewriter.cpp + arith_simplifier_plugin.cpp + ast.cpp + bit_blaster.cpp + bits.cpp + bit_vector.cpp + buffer.cpp + bv_simplifier_plugin.cpp + chashtable.cpp + check_assumptions.cpp + datalog_parser.cpp + ddnf.cpp + diff_logic.cpp + dl_context.cpp + dl_product_relation.cpp + dl_query.cpp + dl_relation.cpp + dl_table.cpp + dl_util.cpp + doc.cpp + escaped.cpp + ex.cpp + expr_rand.cpp + expr_substitution.cpp + ext_numeral.cpp + f2n.cpp + factor_rewriter.cpp + fixed_bit_vector.cpp + for_each_file.cpp + get_implied_equalities.cpp + "${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp" + hashtable.cpp + heap.cpp + heap_trie.cpp + hilbert_basis.cpp + horn_subsume_model_converter.cpp + hwf.cpp + inf_rational.cpp + "${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp" + interval.cpp + karr.cpp + list.cpp + main.cpp + map.cpp + matcher.cpp + "${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp" + memory.cpp + model2expr.cpp + model_retrieval.cpp + mpbq.cpp + mpf.cpp + mpff.cpp + mpfx.cpp + mpq.cpp + mpz.cpp + nlarith_util.cpp + nlsat.cpp + no_overflow.cpp + object_allocator.cpp + old_interval.cpp + optional.cpp + parray.cpp + pdr.cpp + permutation.cpp + polynomial.cpp + polynomial_factorization.cpp + polynorm.cpp + prime_generator.cpp + proof_checker.cpp + qe_arith.cpp + quant_elim.cpp + quant_solve.cpp + random.cpp + rational.cpp + rcf.cpp + region.cpp + sat_user_scope.cpp + simple_parser.cpp + simplex.cpp + simplifier.cpp + small_object_allocator.cpp + smt2print_parse.cpp + smt_context.cpp + sorting_network.cpp + stack.cpp + string_buffer.cpp + substitution.cpp + symbol.cpp + symbol_table.cpp + tbv.cpp + theory_dl.cpp + theory_pb.cpp + timeout.cpp + total_order.cpp + trigo.cpp + udoc_relation.cpp + uint_set.cpp + upolynomial.cpp + var_subst.cpp + vector.cpp + ${z3_test_extra_object_files} +) +z3_add_install_tactic_rule(${z3_test_deps}) +z3_add_memory_initializer_rule(${z3_test_deps}) +z3_add_gparams_register_modules_rule(${z3_test_deps}) +target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) +target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) +target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS}) +target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps}) diff --git a/src/test/fuzzing/CMakeLists.txt b/src/test/fuzzing/CMakeLists.txt new file mode 100644 index 00000000000..c2bc61ed5cb --- /dev/null +++ b/src/test/fuzzing/CMakeLists.txt @@ -0,0 +1,8 @@ +z3_add_component(fuzzing + NOT_LIBZ3_COMPONENT # Don't put this component inside libz3 + SOURCES + expr_delta.cpp + expr_rand.cpp + COMPONENT_DEPENDENCIES + ast +) diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt new file mode 100644 index 00000000000..c8507653179 --- /dev/null +++ b/src/util/CMakeLists.txt @@ -0,0 +1,60 @@ +if (EXISTS "${CMAKE_CURRENT_SOURCE_DIR}/version.h") + message(FATAL_ERROR "\"${CMAKE_CURRENT_SOURCE_DIR}/version.h\"" + ${z3_polluted_tree_msg} + ) +endif() +configure_file(version.h.in ${CMAKE_CURRENT_BINARY_DIR}/version.h @ONLY) + +z3_add_component(util + SOURCES + approx_nat.cpp + approx_set.cpp + bit_util.cpp + bit_vector.cpp + cmd_context_types.cpp + common_msgs.cpp + cooperate.cpp + debug.cpp + env_params.cpp + fixed_bit_vector.cpp + gparams.cpp + hash.cpp + hwf.cpp + inf_int_rational.cpp + inf_rational.cpp + inf_s_integer.cpp + lbool.cpp + luby.cpp + memory_manager.cpp + mpbq.cpp + mpf.cpp + mpff.cpp + mpfx.cpp + mpn.cpp + mpq.cpp + mpq_inf.cpp + mpz.cpp + page.cpp + params.cpp + permutation.cpp + prime_generator.cpp + rational.cpp + region.cpp + rlimit.cpp + scoped_ctrl_c.cpp + scoped_timer.cpp + sexpr.cpp + s_integer.cpp + small_object_allocator.cpp + smt2_util.cpp + stack.cpp + statistics.cpp + symbol.cpp + timeit.cpp + timeout.cpp + timer.cpp + trace.cpp + util.cpp + warning.cpp + z3_exception.cpp +) diff --git a/src/util/version.h.in b/src/util/version.h.in new file mode 100644 index 00000000000..05b619f2d67 --- /dev/null +++ b/src/util/version.h.in @@ -0,0 +1,5 @@ +// automatically generated file. +#define Z3_MAJOR_VERSION @Z3_VERSION_MAJOR@ +#define Z3_MINOR_VERSION @Z3_VERSION_MINOR@ +#define Z3_BUILD_NUMBER @Z3_VERSION_PATCH@ +#define Z3_REVISION_NUMBER @Z3_VERSION_TWEAK@ From e1584cc9c7683ebb0a81022c43ebbce29f8b44cb Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 15:37:20 +0000 Subject: [PATCH 08/42] CMake 2.8.12 does not support the ``LANGUAGES`` argument. --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3c10b4f0aac..8652dc046d7 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,6 +1,6 @@ # This overrides the default flags for the different CMAKE_BUILD_TYPEs set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake") -project(Z3 LANGUAGES C CXX) +project(Z3 C CXX) cmake_minimum_required(VERSION 2.8.12) ################################################################################ From 9f5f8f128f92fd78409b5c7c89235217dc5d9ec8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 15:38:53 +0000 Subject: [PATCH 09/42] CMake 2.8.12 doesn't support the ``continue()`` command. --- src/shell/CMakeLists.txt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index 82113bbb7ab..c8d125ff670 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -12,11 +12,10 @@ set(shell_deps api extra_cmds opt sat) z3_expand_dependencies(shell_expanded_deps ${shell_deps}) get_property(Z3_LIBZ3_COMPONENTS_LIST GLOBAL PROPERTY Z3_LIBZ3_COMPONENTS) foreach (component ${Z3_LIBZ3_COMPONENTS_LIST}) - if ("${component}" STREQUAL "api_dll") + if (NOT ("${component}" STREQUAL "api_dll")) # We don't use the api_dll component in the Z3 executable - continue() + list(APPEND shell_object_files $) endif() - list(APPEND shell_object_files $) endforeach() add_executable(shell datalog_frontend.cpp From 32e51eda2e5591cad00a38637064eedc76c3bf6c Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 16:03:20 +0000 Subject: [PATCH 10/42] Only CMake >= 3.2 supports the ``USES_TERMINAL`` argument to add_custom_command() --- CMakeLists.txt | 12 +++++++++++- cmake/z3_add_component.cmake | 8 ++++---- src/ast/pattern/CMakeLists.txt | 2 +- 3 files changed, 16 insertions(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8652dc046d7..234b6da0f00 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -13,6 +13,16 @@ set(Z3_VERSION_TWEAK 0) set(Z3_VERSION "${Z3_VERSION_MAJOR}.${Z3_VERSION_MINOR}.${Z3_VERSION_PATCH}.${Z3_VERSION_TWEAK}") message(STATUS "Z3 version ${Z3_VERSION}") +################################################################################ +# Set various useful variables depending on CMake version +################################################################################ +if (("${CMAKE_VERSION}" VERSION_EQUAL "3.2") OR ("${CMAKE_VERSION}" VERSION_GREATER "3.2")) + # In CMake >= 3.2 add_custom_command() supports a ``USES_TERMINAL`` argument + set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "USES_TERMINAL") +else() + set(ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG "") +endif() + ################################################################################ # Message for polluted source tree sanity checks ################################################################################ @@ -295,6 +305,6 @@ add_custom_target(uninstall COMMAND "${CMAKE_COMMAND}" -P "${CMAKE_CURRENT_BINARY_DIR}/cmake_uninstall.cmake" COMMENT "Uninstalling..." - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) diff --git a/cmake/z3_add_component.cmake b/cmake/z3_add_component.cmake index 56567405548..bb2761181f0 100644 --- a/cmake/z3_add_component.cmake +++ b/cmake/z3_add_component.cmake @@ -76,7 +76,7 @@ macro(z3_add_component component_name) DEPENDS "${CMAKE_SOURCE_DIR}/scripts/pyg2hpp.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating \"${_full_output_file_path}\" from \"${pyg_file}\"" WORKING_DIRECTORY "${CMAKE_CURRENT_BINARY_DIR}" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) list(APPEND _list_generated_headers "${_full_output_file_path}") @@ -175,7 +175,7 @@ macro(z3_add_install_tactic_rule) "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/install_tactic.cpp\"" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) endmacro() @@ -207,7 +207,7 @@ macro(z3_add_memory_initializer_rule) "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/mem_initializer.cpp\"" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) endmacro() @@ -239,7 +239,7 @@ macro(z3_add_gparams_register_modules_rule) "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" ${_expanded_components} COMMENT "Generating \"${CMAKE_CURRENT_BINARY_DIR}/gparams_register_modules.cpp\"" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) endmacro() diff --git a/src/ast/pattern/CMakeLists.txt b/src/ast/pattern/CMakeLists.txt index 1f8d43b0b83..8cff3e739d5 100644 --- a/src/ast/pattern/CMakeLists.txt +++ b/src/ast/pattern/CMakeLists.txt @@ -15,7 +15,7 @@ add_custom_command(OUTPUT "database.h" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/mk_pat_db.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" COMMENT "Generating \"database.h\"" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) From e8a9209577d4622a4dbfa3e617fbaa8ee3db9c74 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 16:28:53 +0000 Subject: [PATCH 11/42] Add sanity check to make sure in-source CMake builds are disallowed. --- CMakeLists.txt | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 234b6da0f00..389c317a4d6 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -36,6 +36,14 @@ set(z3_polluted_tree_msg " this with ``-n`` first to check which file(s) would be removed." ) +################################################################################ +# Sanity check - Disallow building in source +################################################################################ +if ("${CMAKE_SOURCE_DIR}" STREQUAL "${CMAKE_BINARY_DIR}") + message(FATAL_ERROR "In source builds are not allowed. You should invoke " + "CMake from a different directory.") +endif() + ################################################################################ # Add our CMake module directory to the list of module search directories ################################################################################ From 7ac9172600dc09976b9216a5391648e5c784a712 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 18:18:58 +0000 Subject: [PATCH 12/42] Fix CMake configure under CMake 3.1 with MSVC under Windows. --- CMakeLists.txt | 20 ++++++++++++++++++-- cmake/compiler_flags_override.cmake | 4 ++-- cmake/compiler_warnings.cmake | 6 ++++-- 3 files changed, 24 insertions(+), 6 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 389c317a4d6..3f864c55bff 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -1,7 +1,22 @@ +# Enforce some CMake policies +cmake_minimum_required(VERSION 2.8.12) +if (POLICY CMP0054) + # FIXME: This is horrible. With the old behaviour, + # quoted strings like "MSVC" in if() conditionals + # get implicitly dereferenced. The NEW behaviour + # doesn't do this but CMP0054 was only introduced + # in CMake 3.1 and we support lower versions as the + # minimum. We could set NEW here but it would be very + # confusing to use NEW for some builds and OLD for others + # which could lead to some subtle bugs. Instead when the + # minimum version is 3.1 change this policy to NEW and remove + # the hacks in place to work around it. + cmake_policy(SET CMP0054 OLD) +endif() + # This overrides the default flags for the different CMAKE_BUILD_TYPEs set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake") project(Z3 C CXX) -cmake_minimum_required(VERSION 2.8.12) ################################################################################ # Project version @@ -210,7 +225,8 @@ endif() if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang")) set(SSE_FLAGS "-mfpmath=sse" "-msse" "-msse2") - elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + # FIXME: Remove "x.." when CMP0054 is set to NEW + elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") set(SSE_FLAGS "/arch:SSE2") else() message(FATAL_ERROR "Unknown compiler ${CMAKE_CXX_COMPILER_ID}") diff --git a/cmake/compiler_flags_override.cmake b/cmake/compiler_flags_override.cmake index cb1f8dbc16f..d78b9060188 100644 --- a/cmake/compiler_flags_override.cmake +++ b/cmake/compiler_flags_override.cmake @@ -17,8 +17,8 @@ if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMP set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os") set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3") set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") -elseif ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "MSVC") - # Not tested! + # FIXME: Remove "x.." when CMP0054 is set to NEW +elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/D_DEBUG /MTd /Zi /Ob0 /Od /RTC1") set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1") set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2") diff --git a/cmake/compiler_warnings.cmake b/cmake/compiler_warnings.cmake index e9910c2e4ea..c214e446466 100644 --- a/cmake/compiler_warnings.cmake +++ b/cmake/compiler_warnings.cmake @@ -12,7 +12,8 @@ if ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU") elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") list(APPEND WARNING_FLAGS_TO_CHECK ${GCC_AND_CLANG_WARNINGS}) list(APPEND WARNING_FLAGS_TO_CHECK ${CLANG_ONLY_WARNINGS}) -elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + # FIXME: Remove "x.." when CMP0054 is set to NEW +elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND WARNING_FLAGS_TO_CHECK ${MSVC_WARNINGS}) else() message(AUTHOR_WARNING "Unknown compiler") @@ -27,7 +28,8 @@ option(WARNINGS_AS_ERRORS "Treat compiler warnings as errors" OFF) if (WARNINGS_AS_ERRORS) if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) list(APPEND Z3_COMPONENT_CXX_FLAGS "-Werror") - elseif ("${CMAKE_CXX_COMPILER_ID}" MATCHES "MSVC") + # FIXME: Remove "x.." when CMP0054 is set to NEW + elseif ("x${CMAKE_CXX_COMPILER_ID}" STREQUAL "xMSVC") list(APPEND Z3_COMPONENT_CXX_FLAGS "/WX") else() message(AUTHOR_WARNING "Unknown compiler") From ca6c41e4116f2a09b629c52de2661fc7c471caca Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 20:53:57 +0000 Subject: [PATCH 13/42] Don't append ${OpenMP_CXX_FLAGS} to Z3_DEPENDENT_LIBS. This is wrong because this is passed to ``target_link_libraries()``. It just so happens that ``target_link_libraries()`` will interpret arguments starting with a dash as a flag to pass to the linker (i.e. in this case ``-fopenmp``). However in the case of MSVC that flag is ``/openmp`` which is the interpreted as a file path which will lead to a linker failure later because the linker can't find the file ``\openmp.obj``. --- CMakeLists.txt | 9 ++++++++- examples/c++/CMakeLists.txt | 1 + examples/c/CMakeLists.txt | 1 + src/CMakeLists.txt | 1 + src/shell/CMakeLists.txt | 1 + src/test/CMakeLists.txt | 1 + 6 files changed, 13 insertions(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 3f864c55bff..8fb92004064 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -77,6 +77,8 @@ set(Z3_COMPONENT_CXX_DEFINES "") set(Z3_COMPONENT_CXX_FLAGS "") set(Z3_COMPONENT_EXTRA_INCLUDE_DIRS "") set(Z3_DEPENDENT_LIBS "") +set(Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS "") +set(Z3_DEPENDENT_EXTRA_C_LINK_FLAGS "") ################################################################################ # Build type @@ -210,7 +212,10 @@ if (USE_OPENMP) endif() if (OPENMP_FOUND) list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) - list(APPEND Z3_DEPENDENT_LIBS ${OpenMP_CXX_FLAGS}) + # Targets linking against libz3 (or its individual components) + # will need to add these flags + list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) + list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS}) unset(CMAKE_REQUIRED_FLAGS) message(STATUS "Using OpenMP") else() @@ -285,6 +290,8 @@ message(STATUS "Z3_COMPONENT_CXX_DEFINES: ${Z3_COMPONENT_CXX_DEFINES}") message(STATUS "Z3_COMPONENT_CXX_FLAGS: ${Z3_COMPONENT_CXX_FLAGS}") message(STATUS "Z3_DEPENDENT_LIBS: ${Z3_DEPENDENT_LIBS}") message(STATUS "Z3_COMPONENT_EXTRA_INCLUDE_DIRS: ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}") +message(STATUS "Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}") +message(STATUS "Z3_DEPENDENT_EXTRA_C_LINK_FLAGS: ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}") ################################################################################ # Z3 installation locations diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt index 85bbd77c712..9e8483ac819 100644 --- a/examples/c++/CMakeLists.txt +++ b/examples/c++/CMakeLists.txt @@ -2,3 +2,4 @@ add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) target_link_libraries(cpp_example PRIVATE libz3) target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") +set_property(TARGET cpp_example APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt index 1a14573ac38..3257729aab4 100644 --- a/examples/c/CMakeLists.txt +++ b/examples/c/CMakeLists.txt @@ -1,3 +1,4 @@ add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) target_link_libraries(c_example PRIVATE libz3) target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") +set_property(TARGET c_example APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 4a41cccecc1..e8edf8b5e71 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -101,6 +101,7 @@ set_target_properties(libz3 PROPERTIES # Using INTERFACE means that targets that try link against libz3 will # automatically link against the libs in Z3_DEPENDENT_LIBS target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) + # Declare which header file are the public header files of libz3 # these will automatically installed when the libz3 target is installed set (libz3_public_headers diff --git a/src/shell/CMakeLists.txt b/src/shell/CMakeLists.txt index c8d125ff670..d4dff6f817a 100644 --- a/src/shell/CMakeLists.txt +++ b/src/shell/CMakeLists.txt @@ -41,6 +41,7 @@ target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS}) z3_add_component_dependencies_to_target(shell ${shell_expanded_deps}) +set_property(TARGET shell APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) install(TARGETS shell RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}" ) diff --git a/src/test/CMakeLists.txt b/src/test/CMakeLists.txt index 0217e99b6bc..6a42b79d2af 100644 --- a/src/test/CMakeLists.txt +++ b/src/test/CMakeLists.txt @@ -122,4 +122,5 @@ target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS}) target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +set_property(TARGET test-z3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps}) From 246a1050063893cf82602f28f2827628e668e7e3 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 22:43:18 +0000 Subject: [PATCH 14/42] Force incremental linking to be off for MSVC. Whilst I'm here copy the stacksize flag used in the Python building system. This was an effort to try and stop the Visual Studio build from emitting the error message ``` 70>LINK : fatal error LNK1104: cannot open file 'C:\Users\dan\dev\z3-1\build_console\Debug\z3.ilk' ``` Unfortunately this has not fixed the issue. --- cmake/compiler_flags_override.cmake | 8 ++++++++ 1 file changed, 8 insertions(+) diff --git a/cmake/compiler_flags_override.cmake b/cmake/compiler_flags_override.cmake index d78b9060188..26785a614f5 100644 --- a/cmake/compiler_flags_override.cmake +++ b/cmake/compiler_flags_override.cmake @@ -23,6 +23,14 @@ elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1") set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2") set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1") + # Override linker flags (see Windows-MSVC.cmake for CMake's defaults) + # The stack size comes from the Python build system. + set(_msvc_stack_size "8388608") + set(CMAKE_EXE_LINKER_FLAGS_DEBUG_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}") + set(CMAKE_EXE_LINKER_FLAGS_RELWITHDEBINFO_INIT "/debug /INCREMENTAL:NO /STACK:${_msvc_stack_size}") + set(CMAKE_EXE_LINKER_FLAGS_MINSIZEREL_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}") + set(CMAKE_EXE_LINKER_FLAGS_RELEASE_INIT "/INCREMENTAL:NO /STACK:${_msvc_stack_size}") + unset(_msvc_stack_size) else() message(FATAL_ERROR "Overrides not set for ${_lang} compiler \"${CMAKE_${_lang}_COMPILER_ID}\"") endif() From ce54f6d9570eb2b5c80379e8a3849025f4ef183e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 23:06:35 +0000 Subject: [PATCH 15/42] Fix racing MSVC CMake build. The ``libz3`` target must have a different OUTPUT_NAME than the ``shell`` target to avoid conflicting file names. --- src/CMakeLists.txt | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index e8edf8b5e71..a85e025c32e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -90,7 +90,6 @@ endif() add_library(libz3 ${lib_type} ${object_files}) # FIXME: Set "VERSION" and "SOVERSION" properly set_target_properties(libz3 PROPERTIES - OUTPUT_NAME z3 # FIXME: Should we be using ${Z3_VERSION} here? # VERSION: Sets up symlinks, does it do anything else? VERSION ${Z3_VERSION} @@ -98,6 +97,16 @@ set_target_properties(libz3 PROPERTIES # and should be incremented everytime the API changes SOVERSION ${Z3_VERSION}) +if (NOT MSVC) + # On UNIX like platforms if we don't change the OUTPUT_NAME + # the library gets a name like ``liblibz3.so`` so we change it + # here. We don't do a rename with MSVC because we get file naming + # conflicts (the z3 executable also has this OUTPUT_NAME) with + # ``.ilk``, ``.pdb``, ``.lib`` and ``.exp`` files sharing the same + # prefix. + set_target_properties(libz3 PROPERTIES OUTPUT_NAME z3) +endif() + # Using INTERFACE means that targets that try link against libz3 will # automatically link against the libs in Z3_DEPENDENT_LIBS target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) From 46ac368f866405b680917c8e62cdf8b2b8c56af1 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Mon, 29 Feb 2016 23:44:33 +0000 Subject: [PATCH 16/42] Refactor ``mk_def_file()`` so that it is usable externally via a new function ``mk_def_file_internal()`` which is called by a new ``mk_def_file.py`` script. This will allow other build systems to generate the ``api_dll.def`` file. --- scripts/mk_def_file.py | 36 ++++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 18 +++++++++++++----- 2 files changed, 49 insertions(+), 5 deletions(-) create mode 100755 scripts/mk_def_file.py diff --git a/scripts/mk_def_file.py b/scripts/mk_def_file.py new file mode 100755 index 00000000000..2b9b5a0716c --- /dev/null +++ b/scripts/mk_def_file.py @@ -0,0 +1,36 @@ +#!/usr/bin/env python +""" +Reads a list of Z3 API header files and +generate a ``.def`` file to define the +exported symbols of a dll. This file +can be passed to the ``/DEF`` to the +linker used by MSVC. +""" +import mk_util +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) + + for api_file in pargs.api_files: + if not os.path.exists(api_file): + logging.error('"{}" does not exist'.format(api_file)) + return 1 + + mk_util.mk_def_file_internal( + pargs.output_file, + pargs.dllname, + pargs.api_files) + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 91952823250..f7a51b4da61 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2884,14 +2884,22 @@ def mk_all_gparams_register_modules(): # Generate a .def based on the files at c.export_files slot. def mk_def_file(c): - pat1 = re.compile(".*Z3_API.*") defname = '%s.def' % os.path.join(c.src_dir, c.name) - fout = open(defname, 'w') - fout.write('LIBRARY "%s"\nEXPORTS\n' % c.dll_name) - num = 1 + dll_name = c.dll_name + export_header_files = [] for dot_h in c.export_files: dot_h_c = c.find_file(dot_h, c.name) - api = open(os.path.join(dot_h_c.src_dir, dot_h), 'r') + 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: From beb21126e203ccc8c09caa3149e12d44a8a3b617 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 10:27:39 +0000 Subject: [PATCH 17/42] Move where the Z3 API header files to be scanned by the Python scripts is declared out of ``src/api/CMakeLists.txt`` and into ``src/CMakeLists.txt``. We will need this list to generate the ``api_dll.def`` module definition file for MSVC. Whilst I'm here also fix a stray use of ``USES_TERMINAL`` in ``add_custom_command()``. --- src/CMakeLists.txt | 32 +++++++++++++++++++++++++++++++- src/api/CMakeLists.txt | 21 +++------------------ 2 files changed, 34 insertions(+), 19 deletions(-) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index a85e025c32e..0e6e3cde1c7 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -1,9 +1,38 @@ +################################################################################ +# API header files +################################################################################ +# This lists the API header files that are scanned by +# some of the build rules to generate some files needed +# by the build +set(Z3_API_HEADER_FILES_TO_SCAN + z3_api.h + z3_ast_containers.h + z3_algebraic.h + z3_polynomial.h + z3_rcf.h + z3_fixedpoint.h + z3_optimization.h + z3_interp.h + z3_fpa.h +) +set(Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "") +foreach (header_file ${Z3_API_HEADER_FILES_TO_SCAN}) + set(full_path_api_header_file "${CMAKE_CURRENT_SOURCE_DIR}/api/${header_file}") + list(APPEND Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN "${full_path_api_header_file}") + if (NOT EXISTS "${full_path_api_header_file}") + message(FATAL_ERROR "API header file \"${full_path_api_header_file}\" does not exist") + endif() +endforeach() + +################################################################################ +# Traverse directories each adding a Z3 component +################################################################################ # I'm duplicating the order in ``mk_project.py`` for now to help us keep # the build systems in sync. # # The components in these directory explicitly declare their dependencies so # you may be able to re-order some of these directories but an error will be -# raised if you try to declare a component is depedent on another component +# raised if you try to declare a component is dependent on another component # that has not yet been declared. add_subdirectory(util) add_subdirectory(math/polynomial) @@ -138,6 +167,7 @@ install(TARGETS libz3 ARCHIVE DESTINATION "${Z3_INSTALL_LIB_DIR}" PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}" ) + ################################################################################ # Z3 executable ################################################################################ diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index 506b28cb307..b5a111a2525 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -1,14 +1,3 @@ -set(api_header_files_to_scan - z3_api.h - z3_ast_containers.h - z3_algebraic.h - z3_polynomial.h - z3_rcf.h - z3_fixedpoint.h - z3_optimization.h - z3_interp.h - z3_fpa.h -) set(generated_files api_commands.cpp api_log_macros.cpp @@ -23,10 +12,6 @@ foreach (gen_file ${generated_files}) endif() endforeach() -set(full_path_api_header_files_to_scan "") -foreach (header_file ${api_header_files_to_scan}) - list(APPEND full_path_api_header_files_to_scan "${CMAKE_CURRENT_SOURCE_DIR}/${header_file}") -endforeach() set(full_path_generated_files "") foreach (gen_file ${generated_files}) list(APPEND full_path_generated_files "${CMAKE_CURRENT_BINARY_DIR}/${gen_file}") @@ -36,12 +21,12 @@ add_custom_command(OUTPUT ${generated_files} COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/update_api.py" "${CMAKE_CURRENT_BINARY_DIR}" - ${full_path_api_header_files_to_scan} + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" - ${full_path_api_header_files_to_scan} + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} COMMENT "Generating ${generated_files}" - USES_TERMINAL + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} VERBATIM ) From c9e3332019140cd13cfd4742f35f362962c76759 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 11:08:30 +0000 Subject: [PATCH 18/42] Teach the CMake build system to generate the module exports file ``api_dll.def`` and append the necessary flag to the linker when using MSVC. The MSVC build with CMake now succeeds and both the ``c_example`` and ``cpp_example`` work :) --- src/CMakeLists.txt | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 0e6e3cde1c7..32a6ffa9e7e 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -168,6 +168,37 @@ install(TARGETS libz3 PUBLIC_HEADER DESTINATION "${Z3_INSTALL_INCLUDE_DIR}" ) +if (MSVC) + # Handle settings dll exports when using MSVC + # FIXME: This seems unnecessarily complicated but I'm doing + # this because this is what the python build system does. + # CMake has a much more elegant (see ``GenerateExportHeader.cmake``) + # way of handling this. + set(dll_module_exports_file "${CMAKE_CURRENT_BINARY_DIR}/api_dll.def") + add_custom_command(OUTPUT "${dll_module_exports_file}" + COMMAND + "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_def_file.py" + "${dll_module_exports_file}" + "libz3" + ${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_FULL_PATH_API_HEADER_FILES_TO_SCAN} + COMMENT "Generating \"${dll_module_exports_file}\"" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} + VERBATIM + ) + add_custom_target(libz3_extra_depends + DEPENDS "${dll_module_exports_file}" + ) + add_dependencies(libz3 libz3_extra_depends) + set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS + "/DEF:${dll_module_exports_file}" + ) +endif() + ################################################################################ # Z3 executable ################################################################################ From 0aa86c22aa72a87f7dbfa0f2ad615153d6ecfff5 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 16:04:27 +0000 Subject: [PATCH 19/42] Add documentation on CMake build system. --- README-CMake.md | 279 ++++++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 279 insertions(+) create mode 100644 README-CMake.md diff --git a/README-CMake.md b/README-CMake.md new file mode 100644 index 00000000000..2fa99ef5f35 --- /dev/null +++ b/README-CMake.md @@ -0,0 +1,279 @@ +# Z3's CMake build system + +[CMake](https://cmake.org/) is a "meta build system" that reads a description +of the project written in the ``CMakeLists.txt`` files and emits a build +system for that project of your choice using one of CMake's "generators". +This allows CMake to support many different platforms and build tools. +You can run ``cmake --help`` to see the list of supported "generators" +on your platform. Example generators include "UNIX Makfiles" and "Visual Studio +12 2013". + +## Getting started + +The general workflow when using CMake is the following + +1. Create a new build directory +2. Configure the project +3. Generate the build system +4. Invoke the build system to build the project + +To perform steps 2 and 3 you can choose from three different tools + +* cmake +* ccmake +* cmake-gui + +``cmake`` is a command line tool and is what you should use if you are +writing a script to build Z3. This tool performs steps 1 and 2 in one +go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are +more interactive and allow you to change various options. In both these +tools the basic steps to follow are: + +1. Configure. +2. Change any options you wish. Everytime you change a set of options + You should configure again. This may cause new options to appear +3. Generate. + +For information see https://cmake.org/runningcmake/ + +Note when invoking CMake you give it the path to the source directory. +This is the top-level directory in the Z3 repository containing a +``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``. +If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory) +the configure step will fail. + +What follows is a brief walk through of how to build Z3 using various generators. + +### Unix Makefiles + +Run the following in the top level directory of the Z3 repository. + +``` +mkdir build +cd build +cmake -G "Unix Makefiles" ../ +make -j4 +``` + +Note that on some platforms "Unix Makesfiles" is the default generator so on those +platforms you don't need to pass ``-G "Unix Makefiles"`` command line option to +``cmake``. + +Note there is nothing special about the ``build`` directory name here. You can call +it whatever you like. + +Note the "Unix Makefile" generator is a "single" configuration generator which +means you pick the build type (e.g. ``Debug``, ``Release``) when you invoke CMake. +You can set the build type by passing it to the ``cmake`` invocation like so: + +``` +cmake -G "Unix Makefiles" -DCMAKE_BUILD_TYPE=Release ../ +``` + +See the section on "Build Types" for the different CMake build types. + +If you wish to use a different compiler set the CXX and CC environment variables +passed to cmake. This must be done at the very first invocation to ``cmake`` +in the build directory because once configuration has happened the compiler +is fixed. If you want to use a different compiler to the one you have already +configured you either need to make a new build directory or delete the contents +of the current build directory and start again. + +For example to use clang the ``cmake `` line would be + +``` +CC=clang CXX=clang++ cmake ../ +``` + +Note that CMake build will detect the target architecture that compiler is set up +to build for and the generated build system will build for that architecture. +If there is a way to tell your compiler to build for a different architecture via +compiler flags then you can set the ``CFLAGS`` and ``CXXFLAGS`` environment variables +to have the build target that architecture. + +For example if you are on a x86_64 machine and you want to do a 32-bit build and have +a multilib version of GCC you can run ``cmake`` like this + +``` +CFLAGS="-m32" CXXFLAGS="-m32" CC=gcc CXX=g++ cmake ../ +``` + +Note like with the ``CC`` and ``CXX`` flags this must be done on the very first invocation +to CMake in the build directory. + +### Ninja + +[Ninja](https://ninja-build.org/) is a simple build system that is built for speed. +It can be significantly faster than "UNIX Makefile"s because it is not a recursive +build system and thus doesn't create a new process everytime it traverses into a directory. +Ninja is particularly appropriate if you want fast incremental building. + +Basic usage is as follows: + +``` +mkdir build +cd build +cmake -G "Ninja" ../ +ninja +``` + +Note the discussion of the ``CC``, ``CXX``, ``CFLAGS`` and ``CXXFLAGS`` for "Unix Makefiles" +also applies here. + +Note also that like the "Unix Makefiles" generator, the "Ninja" generator is a single configuration +generator so you pick the build type when you invoke ``cmake`` by passing ``CMAKE_BUILD_TYPE=`` +to ``cmake``. See the section on "Build Types". + +Note that Ninja runs in parallel by default. Use the ``-j`` flag to change this. + +### Visual Studio + +For the Visual Studio generators you need to know which version of Visual Studio you wish +to use and also what architecture you want to build for. + +We'll use the ``cmake-gui`` here as it is easier to pick the right generator but this can +be scripted if need be. + +Here are the basic steps: + +1. Create an empty build directory +2. Start the cmake-gui program +3. Set "where is the source code" to the root of the Z3 project repository. You can do this by pressing + the "Browse Source..." button and picking the directory. +4. Set "where to build the binaries" to the empty build directory you just created. You can do this + by pressing the "Browse build..." button and picking the directory. +5. Press the "Configure" button +6. A window will appear asking you to pick the generator to use. Pick the + generator that matches the version of Visual Studio you are using. Note also + that some of the generator names contain ``Win64`` (e.g. ``Visual Studio 12 + 2013 Win64``) this indicates a x86 64-bit build. Generator names without + this (e.g. ``Visual Studio 12 2013``) are x86 32-bit build. +7. Press the "Finish" button and wait for CMake to finish it's first configure. +8. A set of configuration options will appear which will affect various aspects of the build. + Change them as you desire. If you change a set of options press the "Configure" + again. Additional options may appear when you do this. +9. When you have finished changing configuration options press the "Generate" button. +10. When generation is done close cmake-gui. +11. In the build directory open the generated ``Z3.sln`` solution file created by CMake with + Visual Studio. +12. In Visual Studio pick the build type (e.g. ``Debug``, ``Release``) you want. +13. Click "BUILD > Build Solution". + +Note that unlike the "Unix Makefile" and "Ninja" generators the Visual Studio generators +are multi-configuration generators which means you don't set the build type when invoking +CMake. Instead you set the build type inside Visual Studio. See the "Build Type" section +for more information. + +## Build Types + +Several build types are supported. + +* Release +* Debug +* RelWithDebInfo +* MinSizeRel + +For the single configuration generators (e.g. "Unix Makefile" and "Ninja") you set the +build type when invoking ``cmake`` by passing ``-DCMAKE_BUILD_TYPE=`` where +```` is one of the build types specified above. + +For multi-configuration generators (e.g. Visual Studio) you don't set the build type +when invoking CMake and instead set the build type within Visual Studio itself. + +## Useful options + +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/``) +* ``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. +* ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support. +* ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation. + +On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. + +## Developer/packager notes + +These notes are help developers and packagers of Z3. + +### Install/Uninstall + +Install and uninstall targets are supported. Use ``CMAKE_INSTALL_PREFIX`` to set the install +prefix. + +To install + +``` +make install +``` + +To uninstall + +``` +make uninstall +``` + +Note that ``DESTDIR`` is supported for [staged installs](https://www.gnu.org/prep/standards/html_node/DESTDIR.html). + +To install + +``` +mkdir staged +make install DESTDIR=/full/path/to/staged/ +``` + +to uninstall + +``` +make uninstall DESTDIR=/full/path/to/staged +``` + +The above also works for Ninja but ``DESTDIR`` must be an environment variable instead. + +### Examining invoked commands + +If you are using the "UNIX Makefiles" generator and want to see exactly the commands that are +being run you can pass ``VERBOSE=1`` to make. + +``` +make VERBOSE=1 +``` + +If you are using Ninja you can use the ``-v`` flag. + +### Additional targets + +To see the list of targets run + +``` +make help +``` + +There are a few special targets: + +* ``clean`` all the built targets in the current directory and below +* ``edit_cache`` will invoke one of the CMake tools (depending on which is available) to let you change configuration options. +* ``rebuild_cache`` will reinvoke ``cmake`` for the project. + +### Setting build type specific flags + +The build system supports single configuration and multi-configuration generators. This means +it is not possible to know the build type at configure time and therefore ``${CMAKE_BUILD_TYPE}`` +should not be conditionally used to set compiler flags or definitions. Instead you should use Generator expressions which are evaluated by the generator. + +For example + +``` +$<$:Z3DEBUG> +``` + +If the build type at build time is ``Debug`` this evaluates to ``Z3DEBUG`` but evaluates to nothing for all other configurations. You can see examples of this in the ``CMakeLists.txt`` files. + +### File-globbing + +It is tempting use file-globbing in ``CMakeLists.txt`` to find a set for files matching a pattern and +use them as the sources to build a target. This however is a bad idea because it prevents CMake from knowing when it needs to rerun itself. This is why source file names are explicitly listed in the ``CMakeLists.txt`` so that when changes are made the source files used to build a target automatically triggers a rerun of CMake. + +Long story short. Don't use file globbing. From 346f66d6569986fb33f70305eecf63829cd39d80 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 16:06:58 +0000 Subject: [PATCH 20/42] Don't set the ``_DEBUG`` define. This is related to issue #463 --- cmake/compiler_flags_override.cmake | 3 +-- 1 file changed, 1 insertion(+), 2 deletions(-) diff --git a/cmake/compiler_flags_override.cmake b/cmake/compiler_flags_override.cmake index 26785a614f5..d951805deb6 100644 --- a/cmake/compiler_flags_override.cmake +++ b/cmake/compiler_flags_override.cmake @@ -12,14 +12,13 @@ endif() if (("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "Clang") OR ("${CMAKE_${_lang}_COMPILER_ID}" MATCHES "GNU")) # Taken from Modules/Compiler/GNU.cmake but -DNDEBUG is removed set(CMAKE_${_lang}_FLAGS_INIT "") - # FIXME: should we have -D_DEBUG here to match MSVC build? set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "-g -O0") set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "-Os") set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "-O3") set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "-O2 -g") # FIXME: Remove "x.." when CMP0054 is set to NEW elseif ("x${CMAKE_${_lang}_COMPILER_ID}" STREQUAL "xMSVC") - set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/D_DEBUG /MTd /Zi /Ob0 /Od /RTC1") + set(CMAKE_${_lang}_FLAGS_DEBUG_INIT "/MTd /Zi /Ob0 /Od /RTC1") set(CMAKE_${_lang}_FLAGS_MINSIZEREL_INIT "/MT /O1 /Ob1") set(CMAKE_${_lang}_FLAGS_RELEASE_INIT "/MT /O2 /Ob2") set(CMAKE_${_lang}_FLAGS_RELWITHDEBINFO_INIT "/MT /Zi /O2 /Ob1") From 2b9bdf3947d98cfdad4cad42afa92b2fac53faca Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 16:17:21 +0000 Subject: [PATCH 21/42] Only pass OpenMP flags to the linker when using GCC or Clang. Passing those flags to the linker when MSVC results in a warning about an unused flag. --- CMakeLists.txt | 16 ++++++++++++---- 1 file changed, 12 insertions(+), 4 deletions(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 8fb92004064..7a1937f8eb0 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -212,10 +212,18 @@ if (USE_OPENMP) endif() if (OPENMP_FOUND) list(APPEND Z3_COMPONENT_CXX_FLAGS ${OpenMP_CXX_FLAGS}) - # Targets linking against libz3 (or its individual components) - # will need to add these flags - list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_CXX_FLAGS}) - list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_C_FLAGS}) + # GCC and Clang need to have additional flags passed to the linker. + # We can't do ``target_link_libraries(libz3 INTERFACE ${OpenMP_CXX_FLAGS})`` + # because ``/openmp`` is interpreted as file name rather than a linker + # flag by MSVC and breaks the build + if (("${CMAKE_CXX_COMPILER_ID}" MATCHES "Clang") OR + ("${CMAKE_CXX_COMPILER_ID}" MATCHES "GNU")) + list(APPEND Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS ${OpenMP_C_FLAGS}) + endif() + if (("${CMAKE_C_COMPILER_ID}" MATCHES "Clang") OR + ("${CMAKE_C_COMPILER_ID}" MATCHES "GNU")) + list(APPEND Z3_DEPENDENT_EXTRA_C_LINK_FLAGS ${OpenMP_CXX_FLAGS}) + endif() unset(CMAKE_REQUIRED_FLAGS) message(STATUS "Using OpenMP") else() From 1a914eb9b5e3df5c3b26ad44599056eba5ae4251 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Tue, 1 Mar 2016 17:46:50 +0000 Subject: [PATCH 22/42] Improve CMake build system documentation * Mention NMake * Mention Ninja works on Windows * Give example of passing configuration options to ``cmake`` --- README-CMake.md | 31 +++++++++++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/README-CMake.md b/README-CMake.md index 2fa99ef5f35..2550d8c6caa 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -126,6 +126,31 @@ to ``cmake``. See the section on "Build Types". Note that Ninja runs in parallel by default. Use the ``-j`` flag to change this. +Note that Ninja also runs on Windows. You just need to run ``cmake`` in an +environment where the compiler can be found. If you have Visual Studio +installed it typically ships with a "Developer Command Prompt Window" that you +can use which has the environment variables setup for you. + +## NMake + +NMake is a build system that ships with Visual Studio. You are advised to use +Ninja instead which is significantly faster due to supporting concurrent +builds. However CMake does support NMake if you wish to use it. Note that +NMake is a single configuration generator so you must set ``CMAKE_BUILD_TYPE`` +to set the build type. + +Basic usage: + +1. Launch the "Developer Command Prompt Windows" +2. Change to the root of the Z3 repository + +``` +mkdir build +cd build +cmake -G "NMake Makefiles" ../ +nmake +``` + ### Visual Studio For the Visual Studio generators you need to know which version of Visual Studio you wish @@ -194,6 +219,12 @@ The following useful options can be passed to CMake whilst configuring. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. +Example + +``` +cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../ +``` + ## Developer/packager notes These notes are help developers and packagers of Z3. From f6e946443ea39323d8a300fdf666e413b43d5d36 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 08:13:28 +0000 Subject: [PATCH 23/42] Made emission of the API module files ``api_log_macros.h``, ``api_log_macros.cpp`` and ``api_commands.cpp`` optional in ``update_api.py``. This is required to implement support for building and installing Z3's API bindings with CMake. --- scripts/update_api.py | 38 ++++++++++++++++++++------------------ src/api/CMakeLists.txt | 3 ++- 2 files changed, 22 insertions(+), 19 deletions(-) diff --git a/scripts/update_api.py b/scripts/update_api.py index 8a389752f67..9358ec6dd7a 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1557,7 +1557,7 @@ def init(PATH): # FIXME: This can only be called once from this module # due to its use of global state! def generate_files(api_files, - api_output_dir, + api_output_dir=None, z3py_output_dir=None, dotnet_output_dir=None, java_output_dir=None, @@ -1576,22 +1576,25 @@ def generate_files(api_files, # FIXME: These should not be global global log_h, log_c, exe_c, core_py assert isinstance(api_files, list) - assert os.path.isdir(api_output_dir) - # Hack to avoid emitting z3core.py when we don't want it - def mk_z3coredotpy_file_object(): - if z3py_output_dir: - assert os.path.isdir(z3py_output_dir) - return open(os.path.join(z3py_output_dir, 'z3core.py'), 'w') + # Hack: Avoid emitting files when we don't want them + # by writing to temporary files that get deleted when + # closed. This allows us to work around the fact that + # existing code is designed to always emit these files. + def mk_file_or_temp(output_dir, file_name, mode='w'): + if output_dir != None: + assert os.path.exists(output_dir) and os.path.isdir(output_dir) + return open(os.path.join(output_dir, file_name), mode) else: # Return a file that we can write to without caring + print("Faking emission of '{}'".format(file_name)) import tempfile - return tempfile.TemporaryFile(mode='w') + return tempfile.TemporaryFile(mode=mode) - with open(os.path.join(api_output_dir, 'api_log_macros.h'), 'w') as log_h: - with open(os.path.join(api_output_dir, 'api_log_macros.cpp'), 'w') as log_c: - with open(os.path.join(api_output_dir, 'api_commands.cpp'), 'w') as exe_c: - with mk_z3coredotpy_file_object() as core_py: + with mk_file_or_temp(api_output_dir, 'api_log_macros.h') as log_h: + with mk_file_or_temp(api_output_dir, 'api_log_macros.cpp') as log_c: + with mk_file_or_temp(api_output_dir, 'api_commands.cpp') as exe_c: + with mk_file_or_temp(z3py_output_dir, 'z3core.py') as core_py: # Write preambles write_log_h_preamble(log_h) write_log_c_preamble(log_c) @@ -1625,8 +1628,11 @@ def mk_z3coredotpy_file_object(): def main(args): logging.basicConfig(level=logging.INFO) parser = argparse.ArgumentParser(description=__doc__) - parser.add_argument("api_output_dir", help="Directory to emit files for api module") - parser.add_argument("api_files", nargs="+", help="API header files to generate files from") + parser.add_argument("api_files", nargs="+", + help="API header files to generate files from") + parser.add_argument("--api_output_dir", + help="Directory to emit files for api module", + default=None) parser.add_argument("--z3py-output-dir", dest="z3py_output_dir", default=None) parser.add_argument("--dotnet-output-dir", dest="dotnet_output_dir", default=None) parser.add_argument("--java-output-dir", dest="java_output_dir", default=None) @@ -1644,10 +1650,6 @@ def main(args): logging.error('"{}" does not exist'.format(api_file)) return 1 - if not os.path.isdir(pargs.api_output_dir): - logging.error('"{}" is not a directory'.format(pargs.api_output_dir)) - return 1 - generate_files(api_files=pargs.api_files, api_output_dir=pargs.api_output_dir, z3py_output_dir=pargs.z3py_output_dir, diff --git a/src/api/CMakeLists.txt b/src/api/CMakeLists.txt index b5a111a2525..0fd012b87bd 100644 --- a/src/api/CMakeLists.txt +++ b/src/api/CMakeLists.txt @@ -20,8 +20,9 @@ endforeach() add_custom_command(OUTPUT ${generated_files} COMMAND "${PYTHON_EXECUTABLE}" "${CMAKE_SOURCE_DIR}/scripts/update_api.py" - "${CMAKE_CURRENT_BINARY_DIR}" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--api_output_dir" + "${CMAKE_CURRENT_BINARY_DIR}" DEPENDS "${CMAKE_SOURCE_DIR}/scripts/update_api.py" "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} From 8bc7d319c7ec1e5e3421a791e9c985db7433bf26 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 11:59:48 +0000 Subject: [PATCH 24/42] Refactor ``mk_z3consts_py()`` to that is usable externally via a new function ``mk_z3consts_py_internal()`` which called by a new ``mk_consts_files.py`` script. This will script will allow the const declarations for the different Z3 language bindings to be generated. Right now only support for python is implemented but more can be added in the future. --- scripts/mk_consts_files.py | 47 ++++++++++++++++++++++++++++++++++++++ scripts/mk_util.py | 20 ++++++++++------ 2 files changed, 60 insertions(+), 7 deletions(-) create mode 100755 scripts/mk_consts_files.py diff --git a/scripts/mk_consts_files.py b/scripts/mk_consts_files.py new file mode 100755 index 00000000000..543c56e0e0d --- /dev/null +++ b/scripts/mk_consts_files.py @@ -0,0 +1,47 @@ +#!/usr/bin/env python +""" +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 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) + + for api_file in pargs.api_files: + if not os.path.exists(api_file): + logging.error('"{}" does not exist'.format(api_file)) + return 1 + + 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 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:])) + diff --git a/scripts/mk_util.py b/scripts/mk_util.py index f7a51b4da61..56726b1cc4c 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2999,6 +2999,17 @@ def mk_bindings(api_files): def mk_z3consts_py(api_files): if Z3PY_SRC_DIR is None: raise MKException("You must invoke set_z3py_dir(path):") + full_path_api_files = [] + api_dll = get_component(Z3_DLL_COMPONENT) + for api_file in 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("^ *//.*$") @@ -3007,14 +3018,9 @@ def mk_z3consts_py(api_files): openbrace_pat = re.compile("{ *") closebrace_pat = re.compile("}.*;") - z3consts = open(os.path.join(Z3PY_SRC_DIR, 'z3consts.py'), 'w') + z3consts = open(os.path.join(output_dir, 'z3consts.py'), 'w') z3consts.write('# Automatically generated file\n\n') - - api_dll = get_component(Z3_DLL_COMPONENT) - for api_file in 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) api = open(api_file, 'r') SEARCHING = 0 @@ -3075,7 +3081,7 @@ def mk_z3consts_py(api_files): api.close() z3consts.close() if VERBOSE: - print("Generated '%s'" % os.path.join(Z3PY_SRC_DIR, 'z3consts.py')) + print("Generated '%s'" % os.path.join(output_dir, 'z3consts.py')) # Extract enumeration types from z3_api.h, and add .Net definitions From fb449517e331dc2160c5fcc856f0b41173066939 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 09:10:32 +0000 Subject: [PATCH 25/42] Teach the CMake build system to build and install the python bindings The new ``BUILD_PYTHON_BINDINGS`` option (off by default) will enable building the bindings and the new ``INSTALL_PYTHON_BINDINGS`` option enables installing them. --- README-CMake.md | 2 + src/CMakeLists.txt | 11 ++++ src/api/python/CMakeLists.txt | 108 ++++++++++++++++++++++++++++++++++ 3 files changed, 121 insertions(+) create mode 100644 src/api/python/CMakeLists.txt diff --git a/README-CMake.md b/README-CMake.md index 2550d8c6caa..a7b96c65967 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -216,6 +216,8 @@ The following useful options can be passed to CMake whilst configuring. * ``ENABLE_EXAMPLE_TARGETS`` - BOOL. If set to ``TRUE`` add the build targets for building the API examples. * ``USE_OPENMP`` - BOOL. If set to ``TRUE`` and OpenMP support is detected build with OpenMP support. * ``USE_LIB_GMP`` - BOOL. If set to ``TRUE`` use the GNU multiple precision library. If set to ``FALSE`` use an internal implementation. +* ``BUILD_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` then Z3's python bindings will be built. +* ``INSTALL_PYTHON_BINDINGS`` - BOOL. If set to ``TRUE`` and ``BUILD_PYTHON_BINDINGS`` is ``TRUE`` then running the ``install`` target will install Z3's Python bindings. On the command line these can be passed to ``cmake`` using the ``-D`` option. In ``ccmake`` and ``cmake-gui`` these can be set in the user interface. diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 32a6ffa9e7e..8fb48af00f2 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -208,3 +208,14 @@ add_subdirectory(shell) # z3-test ################################################################################ add_subdirectory(test) + + +################################################################################ +# Z3 API bindings +################################################################################ +option(BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF) +if (BUILD_PYTHON_BINDINGS) + add_subdirectory(api/python) +endif() + +# TODO: Implement support for other bindigns diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt new file mode 100644 index 00000000000..16cd3d6dedb --- /dev/null +++ b/src/api/python/CMakeLists.txt @@ -0,0 +1,108 @@ +message(STATUS "Emitting rules to build Z3 python bindings") +############################################################################### +# Add target to build python bindings for the build directory +############################################################################### +# This allows the python bindings to be used directly from the build directory +set(z3py_files + z3.py + z3num.py + z3poly.py + z3printer.py + z3rcf.py + z3test.py + z3types.py + z3util.py +) + +set(z3py_bindings_build_dest "${CMAKE_BINARY_DIR}") + +set(build_z3_python_bindings_target_depends "") +foreach (z3py_file ${z3py_files}) + add_custom_command(OUTPUT "${z3py_bindings_build_dest}/${z3py_file}" + COMMAND "${CMAKE_COMMAND}" "-E" "copy" + "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" + "${z3py_bindings_build_dest}" + DEPENDS "${CMAKE_CURRENT_SOURCE_DIR}/${z3py_file}" + COMMENT "Copying \"${z3py_file}\" to ${z3py_bindings_build_dest}" + ) + list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/${z3py_file}") +endforeach() + +# Generate z3core.py +add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3core.py" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--z3py-output-dir" + "${z3py_bindings_build_dest}" + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${CMAKE_SOURCE_DIR}/scripts/update_api.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + COMMENT "Generating z3core.py" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) +list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3core.py") + +# Generate z3consts.py +add_custom_command(OUTPUT "${z3py_bindings_build_dest}/z3consts.py" + COMMAND "${PYTHON_EXECUTABLE}" + "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "--z3py-output-dir" + "${z3py_bindings_build_dest}" + DEPENDS + ${Z3_FULL_PATH_API_HEADER_FILES_TO_SCAN} + "${CMAKE_SOURCE_DIR}/scripts/mk_consts_files.py" + "${CMAKE_SOURCE_DIR}/scripts/mk_util.py" + COMMENT "Generating z3consts.py" + ${ADD_CUSTOM_COMMAND_USES_TERMINAL_ARG} +) +list(APPEND build_z3_python_bindings_target_depends "${z3py_bindings_build_dest}/z3consts.py") + +# Convenient top-level target +add_custom_target(build_z3_python_bindings + ALL + DEPENDS + ${build_z3_python_bindings_target_depends} +) + +############################################################################### +# Install +############################################################################### +option(INSTALL_PYTHON_BINDINGS "Install Python bindings when invoking install target" ON) +if (INSTALL_PYTHON_BINDINGS) + # Determine the installation path for the bindings + message(STATUS "Emitting rules to install Z3 python bindings") + execute_process( + COMMAND "${PYTHON_EXECUTABLE}" "-c" + "import distutils.sysconfig; print(distutils.sysconfig.get_python_lib())" + RESULT_VARIABLE exit_code + OUTPUT_VARIABLE python_pkg_dir + OUTPUT_STRIP_TRAILING_WHITESPACE + ) + + if (NOT ("${exit_code}" EQUAL 0)) + message(FATAL_ERROR "Failed to determine your Python package directory") + endif() + message(STATUS "Detected Python package directory: \"${python_pkg_dir}\"") + + # Check if path exists under the install prefix + set(python_install_dir "") + string(FIND "${python_pkg_dir}" "${CMAKE_INSTALL_PREFIX}" position) + if (NOT ("${position}" EQUAL 0)) + message(WARNING "The detected Python package directory \"${python_pkg_dir}\" " + "does not exist under the install prefix \"${CMAKE_INSTALL_PREFIX}\"." + " Running the install target may lead to a broken installation." + ) + set(python_install_dir "${python_pkg_dir}") + else() + string(REPLACE "${CMAKE_INSTALL_PREFIX}" "" python_install_dir "${python_pkg_dir}") + endif() + message(STATUS "Python bindings will be installed to \"${python_install_dir}\"") + install(FILES ${build_z3_python_bindings_target_depends} + DESTINATION "${python_install_dir}" + ) +else() + message(STATUS "Not emitting rules to install Z3 python bindings") +endif() From 9b48b5ca831590e5d9926c60a5cea759ebb77780 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 14:45:01 +0000 Subject: [PATCH 26/42] When building with OpenMP make sure libz3 passes extra linker flags. This is necessary for libz3 to be usable from the Python bindings when libz3 is built with gcc or clang. --- examples/c++/CMakeLists.txt | 1 - examples/c/CMakeLists.txt | 1 - src/CMakeLists.txt | 2 ++ 3 files changed, 2 insertions(+), 2 deletions(-) diff --git a/examples/c++/CMakeLists.txt b/examples/c++/CMakeLists.txt index 9e8483ac819..85bbd77c712 100644 --- a/examples/c++/CMakeLists.txt +++ b/examples/c++/CMakeLists.txt @@ -2,4 +2,3 @@ add_executable(cpp_example EXCLUDE_FROM_ALL example.cpp) target_link_libraries(cpp_example PRIVATE libz3) target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") target_include_directories(cpp_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api/c++") -set_property(TARGET cpp_example APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) diff --git a/examples/c/CMakeLists.txt b/examples/c/CMakeLists.txt index 3257729aab4..1a14573ac38 100644 --- a/examples/c/CMakeLists.txt +++ b/examples/c/CMakeLists.txt @@ -1,4 +1,3 @@ add_executable(c_example EXCLUDE_FROM_ALL test_capi.c) target_link_libraries(c_example PRIVATE libz3) target_include_directories(c_example PRIVATE "${CMAKE_SOURCE_DIR}/src/api") -set_property(TARGET c_example APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_C_LINK_FLAGS}) diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 8fb48af00f2..c4f6b3334db 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -140,6 +140,8 @@ endif() # automatically link against the libs in Z3_DEPENDENT_LIBS target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) +set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) + # Declare which header file are the public header files of libz3 # these will automatically installed when the libz3 target is installed set (libz3_public_headers From 849c16c4fc37a8fb9dc3dac845c59fd3f9c86684 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 15:47:14 +0000 Subject: [PATCH 27/42] Don't try to remove the CMAKE_INSTALL_PREFIX from the ``python_install_dir``. The implementation was broken because we would strip off ``/usr`` and then install into ``/lib/python-3.5/site-packages``. We could remove the leading slash to make sure we install into the CMAKE_INSTALL_PREFIX but doing so seems unnecessarily complicated given that DESTDIR still seems to be respected even when given absolute paths to the CMake ``install()``. --- src/api/python/CMakeLists.txt | 5 ++--- 1 file changed, 2 insertions(+), 3 deletions(-) diff --git a/src/api/python/CMakeLists.txt b/src/api/python/CMakeLists.txt index 16cd3d6dedb..2279be716b3 100644 --- a/src/api/python/CMakeLists.txt +++ b/src/api/python/CMakeLists.txt @@ -95,10 +95,9 @@ if (INSTALL_PYTHON_BINDINGS) "does not exist under the install prefix \"${CMAKE_INSTALL_PREFIX}\"." " Running the install target may lead to a broken installation." ) - set(python_install_dir "${python_pkg_dir}") - else() - string(REPLACE "${CMAKE_INSTALL_PREFIX}" "" python_install_dir "${python_pkg_dir}") endif() + # Using DESTDIR still seems to work even if we use an absolute path + set(python_install_dir "${python_pkg_dir}") message(STATUS "Python bindings will be installed to \"${python_install_dir}\"") install(FILES ${build_z3_python_bindings_target_depends} DESTINATION "${python_install_dir}" From d54d6b50f0a2d1f6a4f8cfc8d5861012de4e1e30 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 23:17:34 +0000 Subject: [PATCH 28/42] Teach the Python build system to use the ``version.h.in`` template file used by the CMake build and use the existing ``configre_file()`` function to generate the ``version.h`` file needed by the build. --- scripts/mk_util.py | 21 +++++++++++++-------- 1 file changed, 13 insertions(+), 8 deletions(-) diff --git a/scripts/mk_util.py b/scripts/mk_util.py index 56726b1cc4c..1185217edf8 100644 --- a/scripts/mk_util.py +++ b/scripts/mk_util.py @@ -2632,15 +2632,20 @@ def update_version(): # Update files with the version number def mk_version_dot_h(major, minor, build, revision): c = get_component(UTIL_COMPONENT) - fout = open(os.path.join(c.src_dir, 'version.h'), 'w') - fout.write('// automatically generated file.\n') - fout.write('#define Z3_MAJOR_VERSION %s\n' % major) - fout.write('#define Z3_MINOR_VERSION %s\n' % minor) - fout.write('#define Z3_BUILD_NUMBER %s\n' % build) - fout.write('#define Z3_REVISION_NUMBER %s\n' % revision) - fout.close() + version_template = os.path.join(c.src_dir, 'version.h.in') + version_header_output = os.path.join(c.src_dir, 'version.h') + # Note the substitution names are what is used by the CMake + # builds system. If you change these you should change them + # in the CMake build too + configure_file(version_template, version_header_output, + { 'Z3_VERSION_MAJOR': str(major), + 'Z3_VERSION_MINOR': str(minor), + 'Z3_VERSION_PATCH': str(build), + 'Z3_VERSION_TWEAK': str(revision), + } + ) if VERBOSE: - print("Generated '%s'" % os.path.join(c.src_dir, 'version.h')) + print("Generated '%s'" % version_header_output) # Generate AssemblyInfo.cs files with the right version numbers by using ``AssemblyInfo.cs.in`` files as a template def mk_all_assembly_infos(major, minor, build, revision): From a3e0eae9ec1a6bcfdf8a1ddde647606892c9431e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Wed, 2 Mar 2016 23:39:03 +0000 Subject: [PATCH 29/42] Move CMakeLists.txt files (other than the one in the repository root) and the cmake directory into a new directory ``contrib/cmake`` that mirrors the directory structure of the root. This is a comprimise between me and Christoph Wintersteiger that was suggested by Arie Gurfinkel that allows the CMake build system to live in the Z3 repository but not impact the Z3 developers that want to avoid the CMake build system. The build system will not work in its new location and a bootstrap script will soon be provided that allows a developer to copy the files back to their correct location. --- {cmake => contrib/cmake/cmake}/cmake_uninstall.cmake.in | 0 {cmake => contrib/cmake/cmake}/compiler_flags_override.cmake | 0 {cmake => contrib/cmake/cmake}/compiler_warnings.cmake | 0 {cmake => contrib/cmake/cmake}/modules/FindGMP.cmake | 0 {cmake => contrib/cmake/cmake}/target_arch_detect.cmake | 0 {cmake => contrib/cmake/cmake}/target_arch_detect.cpp | 0 {cmake => contrib/cmake/cmake}/z3_add_component.cmake | 0 {cmake => contrib/cmake/cmake}/z3_add_cxx_flag.cmake | 0 {examples => contrib/cmake/examples}/CMakeLists.txt | 0 {examples => contrib/cmake/examples}/c++/CMakeLists.txt | 0 {examples => contrib/cmake/examples}/c/CMakeLists.txt | 0 {src => contrib/cmake/src}/CMakeLists.txt | 0 {src => contrib/cmake/src}/ackermannization/CMakeLists.txt | 0 {src => contrib/cmake/src}/api/CMakeLists.txt | 0 {src => contrib/cmake/src}/api/dll/CMakeLists.txt | 0 {src => contrib/cmake/src}/api/python/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/fpa/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/macros/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/normal_forms/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/pattern/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/proof_checker/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/rewriter/CMakeLists.txt | 0 .../cmake/src}/ast/rewriter/bit_blaster/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/simplifier/CMakeLists.txt | 0 {src => contrib/cmake/src}/ast/substitution/CMakeLists.txt | 0 {src => contrib/cmake/src}/cmd_context/CMakeLists.txt | 0 {src => contrib/cmake/src}/cmd_context/extra_cmds/CMakeLists.txt | 0 {src => contrib/cmake/src}/duality/CMakeLists.txt | 0 {src => contrib/cmake/src}/interp/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/automata/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/euclid/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/grobner/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/hilbert/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/interval/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/polynomial/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/realclosure/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/simplex/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/subpaving/CMakeLists.txt | 0 {src => contrib/cmake/src}/math/subpaving/tactic/CMakeLists.txt | 0 {src => contrib/cmake/src}/model/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/base/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/bmc/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/clp/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/dataflow/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/ddnf/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/duality/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/fp/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/pdr/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/rel/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/tab/CMakeLists.txt | 0 {src => contrib/cmake/src}/muz/transforms/CMakeLists.txt | 0 {src => contrib/cmake/src}/nlsat/CMakeLists.txt | 0 {src => contrib/cmake/src}/nlsat/tactic/CMakeLists.txt | 0 {src => contrib/cmake/src}/opt/CMakeLists.txt | 0 {src => contrib/cmake/src}/parsers/smt/CMakeLists.txt | 0 {src => contrib/cmake/src}/parsers/smt2/CMakeLists.txt | 0 {src => contrib/cmake/src}/parsers/util/CMakeLists.txt | 0 {src => contrib/cmake/src}/qe/CMakeLists.txt | 0 {src => contrib/cmake/src}/sat/CMakeLists.txt | 0 {src => contrib/cmake/src}/sat/sat_solver/CMakeLists.txt | 0 {src => contrib/cmake/src}/sat/tactic/CMakeLists.txt | 0 {src => contrib/cmake/src}/shell/CMakeLists.txt | 0 {src => contrib/cmake/src}/smt/CMakeLists.txt | 0 {src => contrib/cmake/src}/smt/params/CMakeLists.txt | 0 {src => contrib/cmake/src}/smt/proto_model/CMakeLists.txt | 0 {src => contrib/cmake/src}/smt/tactic/CMakeLists.txt | 0 {src => contrib/cmake/src}/solver/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/aig/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/arith/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/bv/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/core/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/fpa/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/nlsat_smt/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/portfolio/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/sls/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/smtlogics/CMakeLists.txt | 0 {src => contrib/cmake/src}/tactic/ufbv/CMakeLists.txt | 0 {src => contrib/cmake/src}/test/CMakeLists.txt | 0 {src => contrib/cmake/src}/test/fuzzing/CMakeLists.txt | 0 {src => contrib/cmake/src}/util/CMakeLists.txt | 0 82 files changed, 0 insertions(+), 0 deletions(-) rename {cmake => contrib/cmake/cmake}/cmake_uninstall.cmake.in (100%) rename {cmake => contrib/cmake/cmake}/compiler_flags_override.cmake (100%) rename {cmake => contrib/cmake/cmake}/compiler_warnings.cmake (100%) rename {cmake => contrib/cmake/cmake}/modules/FindGMP.cmake (100%) rename {cmake => contrib/cmake/cmake}/target_arch_detect.cmake (100%) rename {cmake => contrib/cmake/cmake}/target_arch_detect.cpp (100%) rename {cmake => contrib/cmake/cmake}/z3_add_component.cmake (100%) rename {cmake => contrib/cmake/cmake}/z3_add_cxx_flag.cmake (100%) rename {examples => contrib/cmake/examples}/CMakeLists.txt (100%) rename {examples => contrib/cmake/examples}/c++/CMakeLists.txt (100%) rename {examples => contrib/cmake/examples}/c/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ackermannization/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/api/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/api/dll/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/api/python/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/fpa/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/macros/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/normal_forms/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/pattern/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/proof_checker/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/rewriter/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/rewriter/bit_blaster/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/simplifier/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/ast/substitution/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/cmd_context/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/cmd_context/extra_cmds/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/duality/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/interp/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/automata/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/euclid/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/grobner/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/hilbert/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/interval/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/polynomial/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/realclosure/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/simplex/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/subpaving/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/math/subpaving/tactic/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/model/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/base/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/bmc/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/clp/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/dataflow/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/ddnf/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/duality/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/fp/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/pdr/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/rel/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/tab/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/muz/transforms/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/nlsat/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/nlsat/tactic/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/opt/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/parsers/smt/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/parsers/smt2/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/parsers/util/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/qe/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/sat/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/sat/sat_solver/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/sat/tactic/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/shell/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/smt/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/smt/params/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/smt/proto_model/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/smt/tactic/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/solver/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/aig/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/arith/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/bv/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/core/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/fpa/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/nlsat_smt/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/portfolio/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/sls/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/smtlogics/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/tactic/ufbv/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/test/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/test/fuzzing/CMakeLists.txt (100%) rename {src => contrib/cmake/src}/util/CMakeLists.txt (100%) diff --git a/cmake/cmake_uninstall.cmake.in b/contrib/cmake/cmake/cmake_uninstall.cmake.in similarity index 100% rename from cmake/cmake_uninstall.cmake.in rename to contrib/cmake/cmake/cmake_uninstall.cmake.in diff --git a/cmake/compiler_flags_override.cmake b/contrib/cmake/cmake/compiler_flags_override.cmake similarity index 100% rename from cmake/compiler_flags_override.cmake rename to contrib/cmake/cmake/compiler_flags_override.cmake diff --git a/cmake/compiler_warnings.cmake b/contrib/cmake/cmake/compiler_warnings.cmake similarity index 100% rename from cmake/compiler_warnings.cmake rename to contrib/cmake/cmake/compiler_warnings.cmake diff --git a/cmake/modules/FindGMP.cmake b/contrib/cmake/cmake/modules/FindGMP.cmake similarity index 100% rename from cmake/modules/FindGMP.cmake rename to contrib/cmake/cmake/modules/FindGMP.cmake diff --git a/cmake/target_arch_detect.cmake b/contrib/cmake/cmake/target_arch_detect.cmake similarity index 100% rename from cmake/target_arch_detect.cmake rename to contrib/cmake/cmake/target_arch_detect.cmake diff --git a/cmake/target_arch_detect.cpp b/contrib/cmake/cmake/target_arch_detect.cpp similarity index 100% rename from cmake/target_arch_detect.cpp rename to contrib/cmake/cmake/target_arch_detect.cpp diff --git a/cmake/z3_add_component.cmake b/contrib/cmake/cmake/z3_add_component.cmake similarity index 100% rename from cmake/z3_add_component.cmake rename to contrib/cmake/cmake/z3_add_component.cmake diff --git a/cmake/z3_add_cxx_flag.cmake b/contrib/cmake/cmake/z3_add_cxx_flag.cmake similarity index 100% rename from cmake/z3_add_cxx_flag.cmake rename to contrib/cmake/cmake/z3_add_cxx_flag.cmake diff --git a/examples/CMakeLists.txt b/contrib/cmake/examples/CMakeLists.txt similarity index 100% rename from examples/CMakeLists.txt rename to contrib/cmake/examples/CMakeLists.txt diff --git a/examples/c++/CMakeLists.txt b/contrib/cmake/examples/c++/CMakeLists.txt similarity index 100% rename from examples/c++/CMakeLists.txt rename to contrib/cmake/examples/c++/CMakeLists.txt diff --git a/examples/c/CMakeLists.txt b/contrib/cmake/examples/c/CMakeLists.txt similarity index 100% rename from examples/c/CMakeLists.txt rename to contrib/cmake/examples/c/CMakeLists.txt diff --git a/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt similarity index 100% rename from src/CMakeLists.txt rename to contrib/cmake/src/CMakeLists.txt diff --git a/src/ackermannization/CMakeLists.txt b/contrib/cmake/src/ackermannization/CMakeLists.txt similarity index 100% rename from src/ackermannization/CMakeLists.txt rename to contrib/cmake/src/ackermannization/CMakeLists.txt diff --git a/src/api/CMakeLists.txt b/contrib/cmake/src/api/CMakeLists.txt similarity index 100% rename from src/api/CMakeLists.txt rename to contrib/cmake/src/api/CMakeLists.txt diff --git a/src/api/dll/CMakeLists.txt b/contrib/cmake/src/api/dll/CMakeLists.txt similarity index 100% rename from src/api/dll/CMakeLists.txt rename to contrib/cmake/src/api/dll/CMakeLists.txt diff --git a/src/api/python/CMakeLists.txt b/contrib/cmake/src/api/python/CMakeLists.txt similarity index 100% rename from src/api/python/CMakeLists.txt rename to contrib/cmake/src/api/python/CMakeLists.txt diff --git a/src/ast/CMakeLists.txt b/contrib/cmake/src/ast/CMakeLists.txt similarity index 100% rename from src/ast/CMakeLists.txt rename to contrib/cmake/src/ast/CMakeLists.txt diff --git a/src/ast/fpa/CMakeLists.txt b/contrib/cmake/src/ast/fpa/CMakeLists.txt similarity index 100% rename from src/ast/fpa/CMakeLists.txt rename to contrib/cmake/src/ast/fpa/CMakeLists.txt diff --git a/src/ast/macros/CMakeLists.txt b/contrib/cmake/src/ast/macros/CMakeLists.txt similarity index 100% rename from src/ast/macros/CMakeLists.txt rename to contrib/cmake/src/ast/macros/CMakeLists.txt diff --git a/src/ast/normal_forms/CMakeLists.txt b/contrib/cmake/src/ast/normal_forms/CMakeLists.txt similarity index 100% rename from src/ast/normal_forms/CMakeLists.txt rename to contrib/cmake/src/ast/normal_forms/CMakeLists.txt diff --git a/src/ast/pattern/CMakeLists.txt b/contrib/cmake/src/ast/pattern/CMakeLists.txt similarity index 100% rename from src/ast/pattern/CMakeLists.txt rename to contrib/cmake/src/ast/pattern/CMakeLists.txt diff --git a/src/ast/proof_checker/CMakeLists.txt b/contrib/cmake/src/ast/proof_checker/CMakeLists.txt similarity index 100% rename from src/ast/proof_checker/CMakeLists.txt rename to contrib/cmake/src/ast/proof_checker/CMakeLists.txt diff --git a/src/ast/rewriter/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/CMakeLists.txt similarity index 100% rename from src/ast/rewriter/CMakeLists.txt rename to contrib/cmake/src/ast/rewriter/CMakeLists.txt diff --git a/src/ast/rewriter/bit_blaster/CMakeLists.txt b/contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt similarity index 100% rename from src/ast/rewriter/bit_blaster/CMakeLists.txt rename to contrib/cmake/src/ast/rewriter/bit_blaster/CMakeLists.txt diff --git a/src/ast/simplifier/CMakeLists.txt b/contrib/cmake/src/ast/simplifier/CMakeLists.txt similarity index 100% rename from src/ast/simplifier/CMakeLists.txt rename to contrib/cmake/src/ast/simplifier/CMakeLists.txt diff --git a/src/ast/substitution/CMakeLists.txt b/contrib/cmake/src/ast/substitution/CMakeLists.txt similarity index 100% rename from src/ast/substitution/CMakeLists.txt rename to contrib/cmake/src/ast/substitution/CMakeLists.txt diff --git a/src/cmd_context/CMakeLists.txt b/contrib/cmake/src/cmd_context/CMakeLists.txt similarity index 100% rename from src/cmd_context/CMakeLists.txt rename to contrib/cmake/src/cmd_context/CMakeLists.txt diff --git a/src/cmd_context/extra_cmds/CMakeLists.txt b/contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt similarity index 100% rename from src/cmd_context/extra_cmds/CMakeLists.txt rename to contrib/cmake/src/cmd_context/extra_cmds/CMakeLists.txt diff --git a/src/duality/CMakeLists.txt b/contrib/cmake/src/duality/CMakeLists.txt similarity index 100% rename from src/duality/CMakeLists.txt rename to contrib/cmake/src/duality/CMakeLists.txt diff --git a/src/interp/CMakeLists.txt b/contrib/cmake/src/interp/CMakeLists.txt similarity index 100% rename from src/interp/CMakeLists.txt rename to contrib/cmake/src/interp/CMakeLists.txt diff --git a/src/math/automata/CMakeLists.txt b/contrib/cmake/src/math/automata/CMakeLists.txt similarity index 100% rename from src/math/automata/CMakeLists.txt rename to contrib/cmake/src/math/automata/CMakeLists.txt diff --git a/src/math/euclid/CMakeLists.txt b/contrib/cmake/src/math/euclid/CMakeLists.txt similarity index 100% rename from src/math/euclid/CMakeLists.txt rename to contrib/cmake/src/math/euclid/CMakeLists.txt diff --git a/src/math/grobner/CMakeLists.txt b/contrib/cmake/src/math/grobner/CMakeLists.txt similarity index 100% rename from src/math/grobner/CMakeLists.txt rename to contrib/cmake/src/math/grobner/CMakeLists.txt diff --git a/src/math/hilbert/CMakeLists.txt b/contrib/cmake/src/math/hilbert/CMakeLists.txt similarity index 100% rename from src/math/hilbert/CMakeLists.txt rename to contrib/cmake/src/math/hilbert/CMakeLists.txt diff --git a/src/math/interval/CMakeLists.txt b/contrib/cmake/src/math/interval/CMakeLists.txt similarity index 100% rename from src/math/interval/CMakeLists.txt rename to contrib/cmake/src/math/interval/CMakeLists.txt diff --git a/src/math/polynomial/CMakeLists.txt b/contrib/cmake/src/math/polynomial/CMakeLists.txt similarity index 100% rename from src/math/polynomial/CMakeLists.txt rename to contrib/cmake/src/math/polynomial/CMakeLists.txt diff --git a/src/math/realclosure/CMakeLists.txt b/contrib/cmake/src/math/realclosure/CMakeLists.txt similarity index 100% rename from src/math/realclosure/CMakeLists.txt rename to contrib/cmake/src/math/realclosure/CMakeLists.txt diff --git a/src/math/simplex/CMakeLists.txt b/contrib/cmake/src/math/simplex/CMakeLists.txt similarity index 100% rename from src/math/simplex/CMakeLists.txt rename to contrib/cmake/src/math/simplex/CMakeLists.txt diff --git a/src/math/subpaving/CMakeLists.txt b/contrib/cmake/src/math/subpaving/CMakeLists.txt similarity index 100% rename from src/math/subpaving/CMakeLists.txt rename to contrib/cmake/src/math/subpaving/CMakeLists.txt diff --git a/src/math/subpaving/tactic/CMakeLists.txt b/contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt similarity index 100% rename from src/math/subpaving/tactic/CMakeLists.txt rename to contrib/cmake/src/math/subpaving/tactic/CMakeLists.txt diff --git a/src/model/CMakeLists.txt b/contrib/cmake/src/model/CMakeLists.txt similarity index 100% rename from src/model/CMakeLists.txt rename to contrib/cmake/src/model/CMakeLists.txt diff --git a/src/muz/base/CMakeLists.txt b/contrib/cmake/src/muz/base/CMakeLists.txt similarity index 100% rename from src/muz/base/CMakeLists.txt rename to contrib/cmake/src/muz/base/CMakeLists.txt diff --git a/src/muz/bmc/CMakeLists.txt b/contrib/cmake/src/muz/bmc/CMakeLists.txt similarity index 100% rename from src/muz/bmc/CMakeLists.txt rename to contrib/cmake/src/muz/bmc/CMakeLists.txt diff --git a/src/muz/clp/CMakeLists.txt b/contrib/cmake/src/muz/clp/CMakeLists.txt similarity index 100% rename from src/muz/clp/CMakeLists.txt rename to contrib/cmake/src/muz/clp/CMakeLists.txt diff --git a/src/muz/dataflow/CMakeLists.txt b/contrib/cmake/src/muz/dataflow/CMakeLists.txt similarity index 100% rename from src/muz/dataflow/CMakeLists.txt rename to contrib/cmake/src/muz/dataflow/CMakeLists.txt diff --git a/src/muz/ddnf/CMakeLists.txt b/contrib/cmake/src/muz/ddnf/CMakeLists.txt similarity index 100% rename from src/muz/ddnf/CMakeLists.txt rename to contrib/cmake/src/muz/ddnf/CMakeLists.txt diff --git a/src/muz/duality/CMakeLists.txt b/contrib/cmake/src/muz/duality/CMakeLists.txt similarity index 100% rename from src/muz/duality/CMakeLists.txt rename to contrib/cmake/src/muz/duality/CMakeLists.txt diff --git a/src/muz/fp/CMakeLists.txt b/contrib/cmake/src/muz/fp/CMakeLists.txt similarity index 100% rename from src/muz/fp/CMakeLists.txt rename to contrib/cmake/src/muz/fp/CMakeLists.txt diff --git a/src/muz/pdr/CMakeLists.txt b/contrib/cmake/src/muz/pdr/CMakeLists.txt similarity index 100% rename from src/muz/pdr/CMakeLists.txt rename to contrib/cmake/src/muz/pdr/CMakeLists.txt diff --git a/src/muz/rel/CMakeLists.txt b/contrib/cmake/src/muz/rel/CMakeLists.txt similarity index 100% rename from src/muz/rel/CMakeLists.txt rename to contrib/cmake/src/muz/rel/CMakeLists.txt diff --git a/src/muz/tab/CMakeLists.txt b/contrib/cmake/src/muz/tab/CMakeLists.txt similarity index 100% rename from src/muz/tab/CMakeLists.txt rename to contrib/cmake/src/muz/tab/CMakeLists.txt diff --git a/src/muz/transforms/CMakeLists.txt b/contrib/cmake/src/muz/transforms/CMakeLists.txt similarity index 100% rename from src/muz/transforms/CMakeLists.txt rename to contrib/cmake/src/muz/transforms/CMakeLists.txt diff --git a/src/nlsat/CMakeLists.txt b/contrib/cmake/src/nlsat/CMakeLists.txt similarity index 100% rename from src/nlsat/CMakeLists.txt rename to contrib/cmake/src/nlsat/CMakeLists.txt diff --git a/src/nlsat/tactic/CMakeLists.txt b/contrib/cmake/src/nlsat/tactic/CMakeLists.txt similarity index 100% rename from src/nlsat/tactic/CMakeLists.txt rename to contrib/cmake/src/nlsat/tactic/CMakeLists.txt diff --git a/src/opt/CMakeLists.txt b/contrib/cmake/src/opt/CMakeLists.txt similarity index 100% rename from src/opt/CMakeLists.txt rename to contrib/cmake/src/opt/CMakeLists.txt diff --git a/src/parsers/smt/CMakeLists.txt b/contrib/cmake/src/parsers/smt/CMakeLists.txt similarity index 100% rename from src/parsers/smt/CMakeLists.txt rename to contrib/cmake/src/parsers/smt/CMakeLists.txt diff --git a/src/parsers/smt2/CMakeLists.txt b/contrib/cmake/src/parsers/smt2/CMakeLists.txt similarity index 100% rename from src/parsers/smt2/CMakeLists.txt rename to contrib/cmake/src/parsers/smt2/CMakeLists.txt diff --git a/src/parsers/util/CMakeLists.txt b/contrib/cmake/src/parsers/util/CMakeLists.txt similarity index 100% rename from src/parsers/util/CMakeLists.txt rename to contrib/cmake/src/parsers/util/CMakeLists.txt diff --git a/src/qe/CMakeLists.txt b/contrib/cmake/src/qe/CMakeLists.txt similarity index 100% rename from src/qe/CMakeLists.txt rename to contrib/cmake/src/qe/CMakeLists.txt diff --git a/src/sat/CMakeLists.txt b/contrib/cmake/src/sat/CMakeLists.txt similarity index 100% rename from src/sat/CMakeLists.txt rename to contrib/cmake/src/sat/CMakeLists.txt diff --git a/src/sat/sat_solver/CMakeLists.txt b/contrib/cmake/src/sat/sat_solver/CMakeLists.txt similarity index 100% rename from src/sat/sat_solver/CMakeLists.txt rename to contrib/cmake/src/sat/sat_solver/CMakeLists.txt diff --git a/src/sat/tactic/CMakeLists.txt b/contrib/cmake/src/sat/tactic/CMakeLists.txt similarity index 100% rename from src/sat/tactic/CMakeLists.txt rename to contrib/cmake/src/sat/tactic/CMakeLists.txt diff --git a/src/shell/CMakeLists.txt b/contrib/cmake/src/shell/CMakeLists.txt similarity index 100% rename from src/shell/CMakeLists.txt rename to contrib/cmake/src/shell/CMakeLists.txt diff --git a/src/smt/CMakeLists.txt b/contrib/cmake/src/smt/CMakeLists.txt similarity index 100% rename from src/smt/CMakeLists.txt rename to contrib/cmake/src/smt/CMakeLists.txt diff --git a/src/smt/params/CMakeLists.txt b/contrib/cmake/src/smt/params/CMakeLists.txt similarity index 100% rename from src/smt/params/CMakeLists.txt rename to contrib/cmake/src/smt/params/CMakeLists.txt diff --git a/src/smt/proto_model/CMakeLists.txt b/contrib/cmake/src/smt/proto_model/CMakeLists.txt similarity index 100% rename from src/smt/proto_model/CMakeLists.txt rename to contrib/cmake/src/smt/proto_model/CMakeLists.txt diff --git a/src/smt/tactic/CMakeLists.txt b/contrib/cmake/src/smt/tactic/CMakeLists.txt similarity index 100% rename from src/smt/tactic/CMakeLists.txt rename to contrib/cmake/src/smt/tactic/CMakeLists.txt diff --git a/src/solver/CMakeLists.txt b/contrib/cmake/src/solver/CMakeLists.txt similarity index 100% rename from src/solver/CMakeLists.txt rename to contrib/cmake/src/solver/CMakeLists.txt diff --git a/src/tactic/CMakeLists.txt b/contrib/cmake/src/tactic/CMakeLists.txt similarity index 100% rename from src/tactic/CMakeLists.txt rename to contrib/cmake/src/tactic/CMakeLists.txt diff --git a/src/tactic/aig/CMakeLists.txt b/contrib/cmake/src/tactic/aig/CMakeLists.txt similarity index 100% rename from src/tactic/aig/CMakeLists.txt rename to contrib/cmake/src/tactic/aig/CMakeLists.txt diff --git a/src/tactic/arith/CMakeLists.txt b/contrib/cmake/src/tactic/arith/CMakeLists.txt similarity index 100% rename from src/tactic/arith/CMakeLists.txt rename to contrib/cmake/src/tactic/arith/CMakeLists.txt diff --git a/src/tactic/bv/CMakeLists.txt b/contrib/cmake/src/tactic/bv/CMakeLists.txt similarity index 100% rename from src/tactic/bv/CMakeLists.txt rename to contrib/cmake/src/tactic/bv/CMakeLists.txt diff --git a/src/tactic/core/CMakeLists.txt b/contrib/cmake/src/tactic/core/CMakeLists.txt similarity index 100% rename from src/tactic/core/CMakeLists.txt rename to contrib/cmake/src/tactic/core/CMakeLists.txt diff --git a/src/tactic/fpa/CMakeLists.txt b/contrib/cmake/src/tactic/fpa/CMakeLists.txt similarity index 100% rename from src/tactic/fpa/CMakeLists.txt rename to contrib/cmake/src/tactic/fpa/CMakeLists.txt diff --git a/src/tactic/nlsat_smt/CMakeLists.txt b/contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt similarity index 100% rename from src/tactic/nlsat_smt/CMakeLists.txt rename to contrib/cmake/src/tactic/nlsat_smt/CMakeLists.txt diff --git a/src/tactic/portfolio/CMakeLists.txt b/contrib/cmake/src/tactic/portfolio/CMakeLists.txt similarity index 100% rename from src/tactic/portfolio/CMakeLists.txt rename to contrib/cmake/src/tactic/portfolio/CMakeLists.txt diff --git a/src/tactic/sls/CMakeLists.txt b/contrib/cmake/src/tactic/sls/CMakeLists.txt similarity index 100% rename from src/tactic/sls/CMakeLists.txt rename to contrib/cmake/src/tactic/sls/CMakeLists.txt diff --git a/src/tactic/smtlogics/CMakeLists.txt b/contrib/cmake/src/tactic/smtlogics/CMakeLists.txt similarity index 100% rename from src/tactic/smtlogics/CMakeLists.txt rename to contrib/cmake/src/tactic/smtlogics/CMakeLists.txt diff --git a/src/tactic/ufbv/CMakeLists.txt b/contrib/cmake/src/tactic/ufbv/CMakeLists.txt similarity index 100% rename from src/tactic/ufbv/CMakeLists.txt rename to contrib/cmake/src/tactic/ufbv/CMakeLists.txt diff --git a/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt similarity index 100% rename from src/test/CMakeLists.txt rename to contrib/cmake/src/test/CMakeLists.txt diff --git a/src/test/fuzzing/CMakeLists.txt b/contrib/cmake/src/test/fuzzing/CMakeLists.txt similarity index 100% rename from src/test/fuzzing/CMakeLists.txt rename to contrib/cmake/src/test/fuzzing/CMakeLists.txt diff --git a/src/util/CMakeLists.txt b/contrib/cmake/src/util/CMakeLists.txt similarity index 100% rename from src/util/CMakeLists.txt rename to contrib/cmake/src/util/CMakeLists.txt From 875acfc2103d3bcb189fa805da4eed3751887035 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 18:28:16 +0000 Subject: [PATCH 30/42] Add bootstrap.py script to copy CMake files into their correct location on a user's machine and add documentation for this. Also add a ``maintainers.txt`` file. --- README-CMake.md | 147 ++++++++++++++++---- contrib/cmake/bootstrap.py | 254 ++++++++++++++++++++++++++++++++++ contrib/cmake/maintainers.txt | 3 + 3 files changed, 375 insertions(+), 29 deletions(-) create mode 100755 contrib/cmake/bootstrap.py create mode 100644 contrib/cmake/maintainers.txt diff --git a/README-CMake.md b/README-CMake.md index a7b96c65967..cbdcbd158ef 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -10,39 +10,56 @@ on your platform. Example generators include "UNIX Makfiles" and "Visual Studio ## Getting started -The general workflow when using CMake is the following +### Fixing a polluted source tree -1. Create a new build directory -2. Configure the project -3. Generate the build system -4. Invoke the build system to build the project +If you have never used the python build system you can skip this step. -To perform steps 2 and 3 you can choose from three different tools +The existing Python build system creates generated source files in +the build tree. The CMake build system will refuse to work if it +detects this so you need to clean your build tree first. -* cmake -* ccmake -* cmake-gui +To do this run the following in the root of the repository -``cmake`` is a command line tool and is what you should use if you are -writing a script to build Z3. This tool performs steps 1 and 2 in one -go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are -more interactive and allow you to change various options. In both these -tools the basic steps to follow are: +``` +git clean -nx src +``` -1. Configure. -2. Change any options you wish. Everytime you change a set of options - You should configure again. This may cause new options to appear -3. Generate. +This will list everything that will be removed. If you are happy +with this then run. -For information see https://cmake.org/runningcmake/ +``` +git clean -fx src +``` -Note when invoking CMake you give it the path to the source directory. -This is the top-level directory in the Z3 repository containing a -``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``. -If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory) -the configure step will fail. +which will remove the generated source files. + +### Bootstrapping + +Most of Z3's CMake files do not live in their correct location. Instead those +files live in the ``contrib/cmake`` folder and a script is provided that will +copy (or hard link) the files into their correct location. + +To copy the files run + +``` +python contrib/cmake/bootstrap.py create +``` + +in the root of the repository. Once you have done this you can now build Z3 using CMake. +Remember to rerun this command if you pull down new code or change branch so +that the CMake files are up to date. + +To remove the copied files run + +``` +python contrib/cmake/bootstrap.py remove +``` -What follows is a brief walk through of how to build Z3 using various generators. +Note if you plan to do development on Z3 you should read the developer +notes on bootstrapping in this document. + +What follows is a brief walk through of how to build Z3 using some +of the more commonly used CMake generators. ### Unix Makefiles @@ -52,7 +69,7 @@ Run the following in the top level directory of the Z3 repository. mkdir build cd build cmake -G "Unix Makefiles" ../ -make -j4 +make -j4 # Replace 4 with an appropriate number ``` Note that on some platforms "Unix Makesfiles" is the default generator so on those @@ -131,7 +148,7 @@ environment where the compiler can be found. If you have Visual Studio installed it typically ships with a "Developer Command Prompt Window" that you can use which has the environment variables setup for you. -## NMake +### NMake NMake is a build system that ships with Visual Studio. You are advised to use Ninja instead which is significantly faster due to supporting concurrent @@ -189,6 +206,40 @@ are multi-configuration generators which means you don't set the build type when CMake. Instead you set the build type inside Visual Studio. See the "Build Type" section for more information. +### General workflow + +The general workflow when using CMake is the following + +1. Create a new build directory +2. Configure the project +3. Generate the build system +4. Invoke the build system to build the project + +To perform steps 2 and 3 you can choose from three different tools + +* cmake +* ccmake +* cmake-gui + +``cmake`` is a command line tool and is what you should use if you are +writing a script to build Z3. This tool performs steps 1 and 2 in one +go without user interaction. The ``ccmake`` and ``cmake-gui`` tools are +more interactive and allow you to change various options. In both these +tools the basic steps to follow are: + +1. Configure. +2. Change any options you wish. Everytime you change a set of options + You should configure again. This may cause new options to appear +3. Generate. + +For information see https://cmake.org/runningcmake/ + +Note when invoking CMake you give it the path to the source directory. +This is the top-level directory in the Z3 repository containing a +``CMakeLists.txt``. That file should contain the line ``project(Z3 C CXX)``. +If you give it a path deeper into the Z3 repository (e.g. the ``src`` directory) +the configure step will fail. + ## Build Types Several build types are supported. @@ -231,18 +282,56 @@ cmake -DCMAKE_BUILD_TYPE=Release -DENABLE_TRACING=FALSE ../ These notes are help developers and packagers of Z3. +### Boostrapping the CMake build + +Z3's CMake system is experimental and not officially supported. Consequently +Z3's developers have decided that they do not want the CMake files in the +``src/`` and ``examples/`` folders. Instead the ``contrib/cmake/bootstrap.py`` +script copies or hard links them into the correct locations. For context +on this decision see https://github.com/Z3Prover/z3/pull/461 . + +The ``contrib/cmake/bootstrap.py create`` command just copies over files which makes +development harder because you have to copy your modifications over to the +files in ``contrib/cmake`` for your changes to committed to git. If you are on a UNIX like +platform you can create hard links instead by running + +``` +contrib/cmake/boostrap.py create --hard-link +``` + +Using hard links means that modifying any of the "copied" files also modifies the +file under version control. Using hard links also means that the file modification time +will appear correct (i.e. the hard-linked "copies" have the same file modification time +as the corresponding file under version control) which means CMake will correctly reconfigure +when invoked. This is why using symbolic links is not an option because the file modification +time of a symbolic link is not the same as the file modification of the file being pointed to. + +Unfortunately a downside to using hard links (or just plain copies) is that if +you pull down new code (i.e. ``git pull``) then some of the CMake files under +version control may change but the corresponding hard-linked "copies" will not. + +This mean that (regardless of whether or not you use hard links) every time you +pull down new code or change branch or do an interactive rebase you must run +(with or without ``--hard-link``): + +``` +contrb/cmake/boostrap.py create +``` + +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. -To install +To install run ``` make install ``` -To uninstall +To uninstall run ``` make uninstall diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py new file mode 100755 index 00000000000..e9524dad71e --- /dev/null +++ b/contrib/cmake/bootstrap.py @@ -0,0 +1,254 @@ +#!/usr/bin/env python +""" +This script is used to copy or delete the +CMake build system files from the contrib/cmake +folder into the their correct location in the Z3 +repository. + +It offers two modes + +* create - This will symlink the ``cmake`` directory and copy (or hard link) +the appropriate files into their correct locations in the repository. + +* remove - This will remove the symlinked ``cmake`` +directory and remove the files added by the above +methods. + +This has the advantage +that editing the hard link edits the underlying file +(making development easier because copying files is +not neccessary) and CMake will regenerate correctly +because the modification time stamps will be correct. + +""" +import argparse +import logging +import os +import pprint +import shutil +import sys + +def get_full_path_to_script(): + return os.path.abspath(__file__) + +def get_cmake_contrib_dir(): + return os.path.dirname(get_full_path_to_script()) + +def get_repo_root_dir(): + r = os.path.dirname(os.path.dirname(get_cmake_contrib_dir())) + assert os.path.isdir(r) + return r + +# These are paths that should be ignored when checking if a folder +# in the ``contrib/cmake`` exists in the root of the repository +verificationExceptions = { + os.path.join(get_repo_root_dir(), 'cmake'), + os.path.join(get_repo_root_dir(), 'cmake', 'modules') +} + +def contribPathToRepoPath(path): + assert path.startswith(get_cmake_contrib_dir()) + stripped = path[len(get_cmake_contrib_dir()) + 1:] # Plus one is to remove leading slash + assert not os.path.isabs(stripped) + logging.debug('stripped:{}'.format(stripped)) + r = os.path.join(get_repo_root_dir(), stripped) + assert os.path.isabs(r) + logging.debug('Converted contrib path "{}" to repo path "{}"'.format(path, r)) + return r + +def verify_mirrored_directory_struture(): + """ + Check that the directories contained in ``contrib/cmake`` exist + in the root of the repo. + """ + for (dirpath, _, _) in os.walk(get_cmake_contrib_dir()): + expectedDir = contribPathToRepoPath(dirpath) + logging.debug('expectedDir:{}'.format(expectedDir)) + if (not (os.path.exists(expectedDir) and os.path.isdir(expectedDir)) and + expectedDir not in verificationExceptions): + logging.error(('Expected to find directory "{}" but it does not exist' + ' or is not a directory').format(expectedDir)) + return 1 + + return 0 + +def mk_sym_link(target, linkName): + logging.info('Making symbolic link target="{}", linkName="{}"'.format(target, linkName)) + if os.path.exists(linkName): + logging.info('Removing existing link "{}"'.format(linkName)) + if not os.path.islink(linkName): + logging.warning('"{}" overwriting file that is not a symlink'.format(linkName)) + delete_path(linkName) + if os.name == 'posix': + os.symlink(src=target, dst=linkName) + else: + # TODO: Windows does support symlinks but the implementation to do that + # from python is a little complicated so for now lets just copy everyting + logging.warning('Creating symbolic links is not supported. Just making a copy instead') + if os.path.isdir(target): + # Recursively copy directory + shutil.copytree(src=target, dst=linkName, symlinks=False, ignore=False) + else: + # Copy file + assert os.path.isfile(target) + shutil.copy2(src=target, dst=linkName) + +def delete_path(path): + logging.info('Removing "{}"'.format(path)) + if not os.path.exists(path): + logging.warning('"{}" does not exist'.format(path)) + return + if os.path.isdir(path) and not os.path.islink(path): + # FIXME: If we can get symbolic link support on Windows we + # can disallow this completely. + assert os.name == 'nt' + shutil.rmtree(path) + else: + os.remove(path) + +def shouldSkipFile(path): + # Skip this script + if path == get_full_path_to_script(): + return True + # Skip the maintainers file + if path == os.path.join(get_cmake_contrib_dir(), 'maintainers.txt'): + return True + # Skip Vim temporary files + if os.path.basename(path).startswith('.') and path.endswith('.swp'): + return True + return False + + +def create(useHardLinks): + """ + Copy or hard link files in the CMake contrib directory + into the repository where they are intended to live. + + Note that symbolic links for the CMakeLists.txt files + are not appropriate because they won't have the right + file modification time when the files they point to + are modified. This would prevent CMake from correctly + reconfiguring when it detects this is required. + """ + + # Make the ``cmake`` directory a symbolic link. + # We treat this one specially as it is the only directory + # that doesn't already exist in the repository root so + # we can just use a symlink here + linkName = os.path.join(get_repo_root_dir(), 'cmake') + target = os.path.join(get_cmake_contrib_dir(), 'cmake') + specialDir = target + mk_sym_link(target, linkName) + + for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): + # Skip the special directory and its children + if dirPath.startswith(specialDir): + logging.info('Skipping directory "{}"'.format(dirPath)) + continue + + for fileName in fileNames: + fileInContrib = os.path.join(dirPath, fileName) + # Skip files + if shouldSkipFile(fileInContrib): + logging.info('Skipping "{}"'.format(fileInContrib)) + continue + fileInRepo = contribPathToRepoPath(fileInContrib) + logging.info('"{}" => "{}"'.format(fileInContrib, fileInRepo)) + if useHardLinks: + if not os.name == 'posix': + logging.error('Hard links are not supported on your platform') + return False + if os.path.exists(fileInRepo): + delete_path(fileInRepo) + os.link(src=fileInContrib, dst=fileInRepo) + else: + try: + shutil.copy2(src=fileInContrib, dst=fileInRepo) + except shutil.SameFileError as e: + # Can hit this if used created hard links first and then run again without + # wanting hard links + logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( + fileInContrib, fileInRepo)) + logging.error('You should remove the files using the "remove" mode ' + 'and try to create again. You probably are mixing the ' + 'hard-link and non-hard-link create modes') + return False + return True + +def remove(): + """ + Remove the CMake files from their intended location in + the repository. This is used to remove + the files created by the ``create()`` function. + """ + # This directory is treated specially as it is normally + # a symlink. + linkName = os.path.join(get_repo_root_dir(), 'cmake') + delete_path(linkName) + specialDir = os.path.join(get_cmake_contrib_dir(), 'cmake') + + for (dirPath,_ , fileNames) in os.walk(get_cmake_contrib_dir()): + # Skip the special directory and its children + if dirPath.startswith(specialDir): + logging.info('Skipping directory "{}"'.format(dirPath)) + continue + for fileName in fileNames: + fileInContrib = os.path.join(dirPath, fileName) + # Skip files + if shouldSkipFile(fileInContrib): + logging.info('Skipping "{}"'.format(fileInContrib)) + continue + fileInRepo = contribPathToRepoPath(fileInContrib) + if os.path.exists(fileInRepo): + logging.info('Removing "{}"'.format(fileInRepo)) + delete_path(fileInRepo) + return True + +def main(args): + logging.basicConfig(level=logging.INFO) + parser = argparse.ArgumentParser(description=__doc__) + parser.add_argument('mode', + choices=['create', 'remove'], + help='The mode to use') + parser.add_argument("-l","--log-level", + type=str, + default="info", + dest="log_level", + choices=['debug','info','warning','error'] + ) + parser.add_argument("-H", "--hard-link", + action='store_true', + default=False, + dest='hard_link', + help='When using the create mode create hard links instead of copies' + ) + pargs = parser.parse_args(args) + + logLevel = getattr(logging, pargs.log_level.upper(),None) + logging.basicConfig(level=logLevel) + + # Before we start make sure we can transplant the CMake files on to + # repository + if verify_mirrored_directory_struture() != 0: + logging.error('"{}" does not mirror "{}"'.format(get_cmake_contrib_dir(), get_repo_root_dir())) + return 1 + + if pargs.mode == "create": + if not create(useHardLinks=pargs.hard_link): + logging.error("Failed to create") + return 1 + elif pargs.mode == "create_hard_link": + if not create(useHardLinks=True): + logging.error("Failed to create_hard_link") + return 1 + elif pargs.mode == "remove": + if not remove(): + logging.error("Failed to remove") + return 1 + else: + logging.error('Unknown mode "{}"'.format(pargs.mode)) + + return 0 + +if __name__ == '__main__': + sys.exit(main(sys.argv[1:])) diff --git a/contrib/cmake/maintainers.txt b/contrib/cmake/maintainers.txt new file mode 100644 index 00000000000..caa6798c66d --- /dev/null +++ b/contrib/cmake/maintainers.txt @@ -0,0 +1,3 @@ +# Maintainers + +- Dan Liew (@delcypher) From b76ce607b8fc3c2e191b648798fe6c609478c01a Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 18:34:13 +0000 Subject: [PATCH 31/42] Provide a friendly error message if someone tries to use the CMake build without invoking the ``contrib/cmake/boostrap.py`` script. --- CMakeLists.txt | 10 ++++++++++ 1 file changed, 10 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 7a1937f8eb0..331c7a17d4b 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -14,6 +14,16 @@ if (POLICY CMP0054) cmake_policy(SET CMP0054 OLD) endif() +# Provide a friendly message if the user hasn't run the bootstrap script +# to copy all the CMake files into their correct location. +# It is unfortunate that we have to do this, see #461 for the discussion +# on this. +if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) + message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\"" + ". This probably means you need to run" + "``python contrib/cmake/boostrap.py create``") +endif() + # This overrides the default flags for the different CMAKE_BUILD_TYPEs set(CMAKE_USER_MAKE_RULES_OVERRIDE "${CMAKE_CURRENT_SOURCE_DIR}/cmake/compiler_flags_override.cmake") project(Z3 C CXX) From a5f8ceaa489ce133ba3831e1d62a06e86d101ef8 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 18:38:21 +0000 Subject: [PATCH 32/42] Add globbing patterns to ``.gitignore`` so the files copied over by the ``contrib/cmake/bootstrap.py`` script are ignored and so don't get accidently commited. --- .gitignore | 9 +++++++++ 1 file changed, 9 insertions(+) diff --git a/.gitignore b/.gitignore index 58abdcf7379..80a50ea9f14 100644 --- a/.gitignore +++ b/.gitignore @@ -75,3 +75,12 @@ src/api/ml/z3.mllib *.bak doc/api doc/code + +# CMake files copied over by the ``contrib/cmake/boostrap.py`` script +# See #461 +examples/CMakeLists.txt +examples/*/CMakeLists.txt +src/CMakeLists.txt +src/*/CMakeLists.txt +src/*/*/CMakeLists.txt +src/*/*/*/CMakeLists.txt From e67ed6be5d0f8c7f1017c0953cfe763cf0c18cf9 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 18:44:44 +0000 Subject: [PATCH 33/42] Note in the README the experimental CMake build system. --- README.md | 5 +++++ 1 file changed, 5 insertions(+) diff --git a/README.md b/README.md index 534c6c378da..6052e2f9129 100644 --- a/README.md +++ b/README.md @@ -74,6 +74,11 @@ sudo make uninstall To clean Z3 you can delete the build directory and run the ``mk_make.py`` script again. +## Building Z3 using CMake + +Z3 has an unofficial build system using CMake. Read the [README-CMake.md](README-CMake.md) +file for details. + ## Z3 bindings Z3 has bindings for various programming languages. From 786362a4233fc9397c91fee54f9fefc1502bcd1e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 18:55:12 +0000 Subject: [PATCH 34/42] Fix bug in CMake bootstrap script when running under Windows. --- contrib/cmake/bootstrap.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py index e9524dad71e..3df17f1770d 100755 --- a/contrib/cmake/bootstrap.py +++ b/contrib/cmake/bootstrap.py @@ -87,7 +87,7 @@ def mk_sym_link(target, linkName): logging.warning('Creating symbolic links is not supported. Just making a copy instead') if os.path.isdir(target): # Recursively copy directory - shutil.copytree(src=target, dst=linkName, symlinks=False, ignore=False) + shutil.copytree(src=target, dst=linkName, symlinks=False) else: # Copy file assert os.path.isfile(target) From 017e9a24617669a45bb4ec904414795582cce98b Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 19:30:18 +0000 Subject: [PATCH 35/42] Try to fix the freebsd build by linking against the system's threading library. --- CMakeLists.txt | 6 ++++++ 1 file changed, 6 insertions(+) diff --git a/CMakeLists.txt b/CMakeLists.txt index 331c7a17d4b..320c5664204 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -261,6 +261,12 @@ if ("${TARGET_ARCHITECTURE}" STREQUAL "x86_64") unset(SSE_FLAGS) endif() +################################################################################ +# Threading support +################################################################################ +find_package(Threads) +list(APPEND Z3_DEPENDENT_LIBS ${CMAKE_THREAD_LIBS_INIT}) + ################################################################################ # Compiler warnings ################################################################################ From d12b558bea66fc416a132b71faa0c1a9da1fc580 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 20:52:08 +0000 Subject: [PATCH 36/42] Fix typo spotted by @arrowd --- CMakeLists.txt | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/CMakeLists.txt b/CMakeLists.txt index 320c5664204..8b32b0108f1 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -21,7 +21,7 @@ endif() if (NOT (EXISTS "${CMAKE_SOURCE_DIR}/src/CMakeLists.txt")) message(FATAL_ERROR "Cannot find \"${CMAKE_SOURCE_DIR}/src/CMakeLists.txt\"" ". This probably means you need to run" - "``python contrib/cmake/boostrap.py create``") + "``python contrib/cmake/bootstrap.py create``") endif() # This overrides the default flags for the different CMAKE_BUILD_TYPEs From 7033ebe6b5fb5c2eba40efb20675ce70b08e797e Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 21:08:39 +0000 Subject: [PATCH 37/42] Fix running the CMake bootstrap script under Python 2.7 --- contrib/cmake/bootstrap.py | 17 ++++++++++++----- 1 file changed, 12 insertions(+), 5 deletions(-) diff --git a/contrib/cmake/bootstrap.py b/contrib/cmake/bootstrap.py index 3df17f1770d..a3c81fb250c 100755 --- a/contrib/cmake/bootstrap.py +++ b/contrib/cmake/bootstrap.py @@ -80,7 +80,7 @@ def mk_sym_link(target, linkName): logging.warning('"{}" overwriting file that is not a symlink'.format(linkName)) delete_path(linkName) if os.name == 'posix': - os.symlink(src=target, dst=linkName) + os.symlink(target, linkName) else: # TODO: Windows does support symlinks but the implementation to do that # from python is a little complicated so for now lets just copy everyting @@ -160,15 +160,22 @@ def create(useHardLinks): return False if os.path.exists(fileInRepo): delete_path(fileInRepo) - os.link(src=fileInContrib, dst=fileInRepo) + os.link(fileInContrib, fileInRepo) else: try: shutil.copy2(src=fileInContrib, dst=fileInRepo) - except shutil.SameFileError as e: + except shutil.Error as e: # Can hit this if used created hard links first and then run again without # wanting hard links - logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( - fileInContrib, fileInRepo)) + if sys.version_info.major <= 2: + logging.error(e.message) + else: + # Python >= 3 + if isinstance(e, shutil.SameFileError): + logging.error('Trying to copy "{}" to "{}" but they are the same file'.format( + fileInContrib, fileInRepo)) + else: + logging.error(e) logging.error('You should remove the files using the "remove" mode ' 'and try to create again. You probably are mixing the ' 'hard-link and non-hard-link create modes') From a2cc6d256ac420d4662e725fd7d4d0cbc42cfdea Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Thu, 3 Mar 2016 21:15:53 +0000 Subject: [PATCH 38/42] Emit an error message if building the Python bindings is enabled but libz3 is built statically. This build combination doesn't work because the Python bindings need a dynamic libz3. --- contrib/cmake/src/CMakeLists.txt | 4 ++++ 1 file changed, 4 insertions(+) diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index c4f6b3334db..5e60d7e9deb 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -217,6 +217,10 @@ add_subdirectory(test) ################################################################################ option(BUILD_PYTHON_BINDINGS "Build Python bindings for Z3" OFF) if (BUILD_PYTHON_BINDINGS) + if (NOT BUILD_LIBZ3_SHARED) + message(FATAL_ERROR "The python bindings will not work with a static libz3. " + "You either need to disable BUILD_PYTHON_BINDINGS or enable BUILD_LIBZ3_SHARED") + endif() add_subdirectory(api/python) endif() From 29901e79e1e7b7e91a161dfb94a3a0eb6126c6d6 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 4 Mar 2016 11:19:35 +0000 Subject: [PATCH 39/42] Fix how the list of linker flags ``Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`` is applied to targets. The ``LINK_FLAGS`` property of a target is a string and not a list and so if ``Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS`` contained more than one flag the linker line would end up being ``-flag1;flag2;flag3;...`` which would not work. Now we use a new function ``z3_append_linker_flag_list_to_target()`` to iterate through the list and update the ``LINK_FLAGS`` property of the specified target correctly. --- CMakeLists.txt | 1 + .../z3_append_linker_flag_list_to_target.cmake | 17 +++++++++++++++++ contrib/cmake/src/CMakeLists.txt | 6 ++---- contrib/cmake/src/shell/CMakeLists.txt | 2 +- contrib/cmake/src/test/CMakeLists.txt | 4 ++-- 5 files changed, 23 insertions(+), 7 deletions(-) create mode 100644 contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake diff --git a/CMakeLists.txt b/CMakeLists.txt index 8b32b0108f1..0e95cb65a4e 100644 --- a/CMakeLists.txt +++ b/CMakeLists.txt @@ -337,6 +337,7 @@ set(CMAKE_RUNTIME_OUTPUT_DIRECTORY "${CMAKE_BINARY_DIR}") # Z3 components, library and executables ################################################################################ include(${CMAKE_SOURCE_DIR}/cmake/z3_add_component.cmake) +include(${CMAKE_SOURCE_DIR}/cmake/z3_append_linker_flag_list_to_target.cmake) add_subdirectory(src) ################################################################################ diff --git a/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake b/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake new file mode 100644 index 00000000000..3eb1e2d340d --- /dev/null +++ b/contrib/cmake/cmake/z3_append_linker_flag_list_to_target.cmake @@ -0,0 +1,17 @@ +# The LINK_FLAGS property of a target in CMake is unfortunately a string and +# not a list. This function takes a list of linker flags and iterates through +# them to append them as strings to the ``LINK_FLAGS`` property of +# the specified target. +# E.g. +# z3_append_linker_flag_list_to_target(mytarget "-fopenmp" "-static") +function(z3_append_linker_flag_list_to_target target) + if (NOT (TARGET "${target}")) + message(FATAL_ERROR "Specified target \"${target}\" is not a target") + endif() + foreach(flag ${ARGN}) + #message(STATUS "Appending link flag \"${flag}\" to target ${target}") + # Note that space inside the quoted string is required so that the flags + # are space separated. + set_property(TARGET ${target} APPEND_STRING PROPERTY LINK_FLAGS " ${flag}") + endforeach() +endfunction() diff --git a/contrib/cmake/src/CMakeLists.txt b/contrib/cmake/src/CMakeLists.txt index 5e60d7e9deb..6708f505e27 100644 --- a/contrib/cmake/src/CMakeLists.txt +++ b/contrib/cmake/src/CMakeLists.txt @@ -140,7 +140,7 @@ endif() # automatically link against the libs in Z3_DEPENDENT_LIBS target_link_libraries(libz3 INTERFACE ${Z3_DEPENDENT_LIBS}) -set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +z3_append_linker_flag_list_to_target(libz3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) # Declare which header file are the public header files of libz3 # these will automatically installed when the libz3 target is installed @@ -196,9 +196,7 @@ if (MSVC) DEPENDS "${dll_module_exports_file}" ) add_dependencies(libz3 libz3_extra_depends) - set_property(TARGET libz3 APPEND PROPERTY LINK_FLAGS - "/DEF:${dll_module_exports_file}" - ) + z3_append_linker_flag_list_to_target(libz3 "/DEF:${dll_module_exports_file}") endif() ################################################################################ diff --git a/contrib/cmake/src/shell/CMakeLists.txt b/contrib/cmake/src/shell/CMakeLists.txt index d4dff6f817a..65b97aaafc0 100644 --- a/contrib/cmake/src/shell/CMakeLists.txt +++ b/contrib/cmake/src/shell/CMakeLists.txt @@ -41,7 +41,7 @@ target_compile_options(shell PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) target_link_libraries(shell PRIVATE ${Z3_DEPENDENT_LIBS}) z3_add_component_dependencies_to_target(shell ${shell_expanded_deps}) -set_property(TARGET shell APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +z3_append_linker_flag_list_to_target(shell ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) install(TARGETS shell RUNTIME DESTINATION "${Z3_INSTALL_BIN_DIR}" ) diff --git a/contrib/cmake/src/test/CMakeLists.txt b/contrib/cmake/src/test/CMakeLists.txt index 6a42b79d2af..b6166b3f8b8 100644 --- a/contrib/cmake/src/test/CMakeLists.txt +++ b/contrib/cmake/src/test/CMakeLists.txt @@ -121,6 +121,6 @@ z3_add_gparams_register_modules_rule(${z3_test_deps}) target_compile_definitions(test-z3 PRIVATE ${Z3_COMPONENT_CXX_DEFINES}) target_compile_options(test-z3 PRIVATE ${Z3_COMPONENT_CXX_FLAGS}) target_link_libraries(test-z3 PRIVATE ${Z3_DEPENDENT_LIBS}) -target_include_directories(shell PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) -set_property(TARGET test-z3 APPEND PROPERTY LINK_FLAGS ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) +target_include_directories(test-z3 PRIVATE ${Z3_COMPONENT_EXTRA_INCLUDE_DIRS}) +z3_append_linker_flag_list_to_target(test-z3 ${Z3_DEPENDENT_EXTRA_CXX_LINK_FLAGS}) z3_add_component_dependencies_to_target(test-z3 ${z3_test_expanded_deps}) From a52d81ef3ec4e888508c003f40aa4041e41ea1f7 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 4 Mar 2016 13:43:25 +0000 Subject: [PATCH 40/42] Document ``z3_add_component()``. --- contrib/cmake/cmake/z3_add_component.cmake | 31 ++++++++++++++++++++++ 1 file changed, 31 insertions(+) diff --git a/contrib/cmake/cmake/z3_add_component.cmake b/contrib/cmake/cmake/z3_add_component.cmake index bb2761181f0..eebc0c8d96f 100644 --- a/contrib/cmake/cmake/z3_add_component.cmake +++ b/contrib/cmake/cmake/z3_add_component.cmake @@ -50,6 +50,37 @@ function(z3_add_component_dependencies_to_target target_name) endforeach() endfunction() +# z3_add_component(component_name +# [NOT_LIBZ3_COMPONENT] +# SOURCES source1 [source2...] +# [COMPONENT_DEPENDENCIES component1 [component2...]] +# [PYG_FILES pygfile1 [pygfile2...]] +# ) +# +# Declares a Z3 component (as a CMake "object library") with target name +# ``component_name``. +# +# The option ``NOT_LIBZ3_COMPONENT`` declares that the +# component should not be included in libz3. If this is not specified +# the component will be included in libz3. +# +# The mandatory ``SOURCES`` keyword should be followed by the source files +# (including any files generated at build or configure time) that are should be +# included in the component. It is not necessary to list header files here as +# CMake infers header file dependencies unless that header file is generated at +# build time. +# +# The optional ``COMPONENT_DEPENDENCIES`` keyword should be followed by a list of +# components that ``component_name`` should depend on. The components listed here +# must have already been declared using ``z3_add_component()``. Listing components +# here causes them to be built before ``component_name``. It also currently causes +# the include directories used by the transistive closure of the dependencies +# to be added to the list of include directories used to build ``component_name``. +# +# The optional ``PYG_FILES`` keyword should be followed by a list of one or +# more ``.pyg`` files that should used to be generate +# ``_params.hpp`` header files used by the ``component_name``. +# macro(z3_add_component component_name) CMAKE_PARSE_ARGUMENTS("Z3_MOD" "NOT_LIBZ3_COMPONENT" "" "SOURCES;COMPONENT_DEPENDENCIES;PYG_FILES" ${ARGN}) message(STATUS "Adding component ${component_name}") From 1d9a7dcf475f9638bb27b973611aa42e739a8f5d Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Fri, 4 Mar 2016 15:31:56 +0000 Subject: [PATCH 41/42] Add missing shebang in ``scripts/update_api.py``. The script was already marked as executable but it wasn't possible to execute from a shell due to the missing shebang. --- scripts/update_api.py | 1 + 1 file changed, 1 insertion(+) diff --git a/scripts/update_api.py b/scripts/update_api.py index 9358ec6dd7a..d5cc92a7f72 100755 --- a/scripts/update_api.py +++ b/scripts/update_api.py @@ -1,3 +1,4 @@ +#!/usr/bin/env python ############################################ # Copyright (c) 2012 Microsoft Corporation # From 7fd5042ff39d5b17f872263380be1267a9f6e385 Mon Sep 17 00:00:00 2001 From: Dan Liew Date: Sat, 5 Mar 2016 16:53:29 +0000 Subject: [PATCH 42/42] Minor tweaks to ``README-CMake.md``. --- README-CMake.md | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/README-CMake.md b/README-CMake.md index cbdcbd158ef..28f49cf2716 100644 --- a/README-CMake.md +++ b/README-CMake.md @@ -15,8 +15,8 @@ on your platform. Example generators include "UNIX Makfiles" and "Visual Studio If you have never used the python build system you can skip this step. The existing Python build system creates generated source files in -the build tree. The CMake build system will refuse to work if it -detects this so you need to clean your build tree first. +the source tree. The CMake build system will refuse to work if it +detects this so you need to clean your source tree first. To do this run the following in the root of the repository @@ -46,8 +46,8 @@ python contrib/cmake/bootstrap.py create ``` in the root of the repository. Once you have done this you can now build Z3 using CMake. -Remember to rerun this command if you pull down new code or change branch so -that the CMake files are up to date. +Make sure you remember to rerun this command if you pull down new code/rebase/change branch so +that the copied CMake files are up to date. To remove the copied files run