From c8bc4881d4f3bf54258b0f01280fbda23a1dd651 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Fri, 6 Aug 2021 11:55:18 -0700 Subject: [PATCH] Merge options cmake into general cmake file (#6989) This PR removes options/CMakeLists.txt and merges its contents into src/CMakeLists.txt and does some generalization in the mkoptions.py script. This prepares the whole setup so that we can also generate options code in other directories than options/ easily in the future: parts of the options code will be moved to the main folder. --- src/CMakeLists.txt | 97 +++++++++++++++++++++++++++- src/options/CMakeLists.txt | 111 -------------------------------- src/options/mkoptions.py | 78 ++++++++++++---------- src/options/module_template.cpp | 4 +- src/options/module_template.h | 4 +- 5 files changed, 143 insertions(+), 151 deletions(-) delete mode 100644 src/options/CMakeLists.txt diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt index 5ea99144b..d3f4a0e6a 100644 --- a/src/CMakeLists.txt +++ b/src/CMakeLists.txt @@ -50,6 +50,25 @@ libcvc5_add_sources( omt/integer_optimizer.h omt/omt_optimizer.cpp omt/omt_optimizer.h + options/decision_weight.h + options/didyoumean.cpp + options/didyoumean.h + options/language.cpp + options/language.h + options/managed_streams.cpp + options/managed_streams.h + options/option_exception.cpp + options/option_exception.h + options/options_handler.cpp + options/options_handler.h + options/options_listener.h + options/options_public.h + options/outputc.cpp + options/outputc.h + options/printer_modes.cpp + options/printer_modes.h + options/set_language.cpp + options/set_language.h preprocessing/assertion_pipeline.cpp preprocessing/assertion_pipeline.h preprocessing/learned_literal_manager.cpp @@ -1140,6 +1159,83 @@ libcvc5_add_sources( include_directories(include) include_directories(. ${CMAKE_CURRENT_BINARY_DIR}) +#-----------------------------------------------------------------------------# +# Take care of options + +check_python_module("toml") + +set(options_toml_files + options/arith_options.toml + options/arrays_options.toml + options/base_options.toml + options/booleans_options.toml + options/builtin_options.toml + options/bv_options.toml + options/datatypes_options.toml + options/decision_options.toml + options/expr_options.toml + options/fp_options.toml + options/main_options.toml + options/parser_options.toml + options/printer_options.toml + options/proof_options.toml + options/prop_options.toml + options/quantifiers_options.toml + options/sep_options.toml + options/sets_options.toml + options/smt_options.toml + options/strings_options.toml + options/theory_options.toml + options/uf_options.toml +) +string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files}) +string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files}) +list(PREPEND options_gen_cpp_files "options/options.cpp" "options/options_public.cpp") +list(PREPEND options_gen_h_files "options/options.h") + +libcvc5_add_sources(GENERATED ${options_gen_cpp_files} ${options_gen_h_files}) + +list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files) + +set(options_gen_doc_files "") +if (BUILD_DOCS) + list( + APPEND + options_gen_doc_files + "${CMAKE_BINARY_DIR}/docs/options_generated.rst" + ) +endif() + +add_custom_command( + OUTPUT + ${options_gen_cpp_files} ${options_gen_h_files} + ${options_gen_doc_files} + COMMAND + ${CMAKE_COMMAND} -E make_directory ${CMAKE_CURRENT_BINARY_DIR}/options + COMMAND + ${PYTHON_EXECUTABLE} + ${CMAKE_CURRENT_LIST_DIR}/options/mkoptions.py + ${CMAKE_CURRENT_LIST_DIR} + ${CMAKE_BINARY_DIR} + ${CMAKE_CURRENT_BINARY_DIR} + ${abs_toml_files} + DEPENDS + options/mkoptions.py + ${options_toml_files} + options/module_template.h + options/module_template.cpp + options/options_public_template.cpp + options/options_template.h + options/options_template.cpp +) + +add_custom_target(gen-options + DEPENDS + ${options_gen_cpp_files} + ${options_gen_h_files} +) + + #-----------------------------------------------------------------------------# set(KINDS_FILES @@ -1163,7 +1259,6 @@ set(KINDS_FILES add_subdirectory(base) add_subdirectory(context) add_subdirectory(expr) -add_subdirectory(options) if (NOT BUILD_LIB_ONLY) add_subdirectory(parser) endif() diff --git a/src/options/CMakeLists.txt b/src/options/CMakeLists.txt deleted file mode 100644 index a75806504..000000000 --- a/src/options/CMakeLists.txt +++ /dev/null @@ -1,111 +0,0 @@ -############################################################################### -# Top contributors (to current version): -# Mathias Preiner, Aina Niemetz, Andrew Reynolds -# -# This file is part of the cvc5 project. -# -# Copyright (c) 2009-2021 by the authors listed in the file AUTHORS -# in the top-level source directory and their institutional affiliations. -# All rights reserved. See the file COPYING in the top-level source -# directory for licensing information. -# ############################################################################# -# -# The build system configuration. -## - -# Check if the toml Python module is installed. -check_python_module("toml") - -libcvc5_add_sources( - decision_weight.h - didyoumean.cpp - didyoumean.h - language.cpp - language.h - managed_streams.cpp - managed_streams.h - option_exception.cpp - option_exception.h - options_handler.cpp - options_handler.h - options_listener.h - options_public.h - outputc.cpp - outputc.h - printer_modes.cpp - printer_modes.h - set_language.cpp - set_language.h -) - -set(options_toml_files - arith_options.toml - arrays_options.toml - base_options.toml - booleans_options.toml - builtin_options.toml - bv_options.toml - datatypes_options.toml - decision_options.toml - expr_options.toml - fp_options.toml - main_options.toml - parser_options.toml - printer_options.toml - proof_options.toml - prop_options.toml - quantifiers_options.toml - sep_options.toml - sets_options.toml - smt_options.toml - strings_options.toml - theory_options.toml - uf_options.toml -) - -string(REPLACE "toml" "cpp;" options_gen_cpp_files ${options_toml_files}) -string(REPLACE "toml" "h;" options_gen_h_files ${options_toml_files}) - -libcvc5_add_sources(GENERATED options.h options.cpp options_public.cpp ${options_gen_cpp_files}) - -list_prepend(options_toml_files "${CMAKE_CURRENT_LIST_DIR}/" abs_toml_files) - -set(options_gen_doc_files "") -if (BUILD_DOCS) - list( - APPEND - options_gen_doc_files - "${CMAKE_BINARY_DIR}/docs/options_generated.rst" - ) -endif() - -add_custom_command( - OUTPUT - options.h options.cpp options_public.cpp - ${options_gen_cpp_files} ${options_gen_h_files} - ${options_gen_doc_files} - COMMAND - ${PYTHON_EXECUTABLE} - ${CMAKE_CURRENT_LIST_DIR}/mkoptions.py - ${CMAKE_CURRENT_LIST_DIR} - ${CMAKE_BINARY_DIR} - ${CMAKE_CURRENT_BINARY_DIR} - ${abs_toml_files} - DEPENDS - mkoptions.py - ${options_toml_files} - module_template.h - module_template.cpp - options_public_template.cpp - options_template.h - options_template.cpp -) - -add_custom_target(gen-options - DEPENDS - options.h - options.cpp - options_public.cpp - ${options_gen_cpp_files} - ${options_gen_h_files} -) diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py index 15f319e9c..ec5eda17e 100644 --- a/src/options/mkoptions.py +++ b/src/options/mkoptions.py @@ -551,7 +551,7 @@ def help_mode_format(option): return '\n '.join('"{}\\n"'.format(x) for x in text) -def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): +def codegen_module(module, dst_dir, tpls): """ Generate code for each option module (*_options.{h,cpp}) """ @@ -663,28 +663,29 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp): visibility_include = '#include "cvc5_public.h"' else: visibility_include = '#include "cvc5_private.h"' + + data = { + 'visibility_include': visibility_include, + 'id_cap': module.id_cap, + 'id': module.id, + 'includes': '\n'.join(sorted(list(includes))), + 'holder_spec': '\n'.join(holder_specs), + 'decls': '\n'.join(decls), + 'specs': '\n'.join(specs), + 'option_names': '\n'.join(option_names), + 'inls': '\n'.join(inls), + 'defaults_decl': '\n'.join(default_decl), + 'modes_decl': '\n'.join(mode_decl), + 'header': module.header, + 'accs': '\n'.join(accs), + 'defaults_impl': '\n'.join(default_impl), + 'defs': '\n'.join(defs), + 'modes_impl': '\n'.join(mode_impl), + } - filename = os.path.splitext(os.path.split(module.header)[1])[0] - write_file(dst_dir, '{}.h'.format(filename), tpl_module_h.format( - visibility_include=visibility_include, - id_cap=module.id_cap, - id=module.id, - includes='\n'.join(sorted(list(includes))), - holder_spec='\n'.join(holder_specs), - decls='\n'.join(decls), - specs='\n'.join(specs), - option_names='\n'.join(option_names), - inls='\n'.join(inls), - defaults='\n'.join(default_decl), - modes=''.join(mode_decl))) - - write_file(dst_dir, '{}.cpp'.format(filename), tpl_module_cpp.format( - header=module.header, - id=module.id, - accs='\n'.join(accs), - defaults='\n'.join(default_impl), - defs='\n'.join(defs), - modes=''.join(mode_impl))) + for tpl in tpls: + filename = tpl['output'].replace('module', module.filename) + write_file(dst_dir, filename, tpl['content'].format(**data)) def docgen_option(option, help_common, help_others): @@ -729,8 +730,7 @@ def add_getopt_long(long_name, argument_req, getopt_long): 'required' if argument_req else 'no', value)) -def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, - tpl_options_cpp, tpl_options_public): +def codegen_all_modules(modules, build_dir, dst_dir, tpls): """ Generate code for all option modules (options.cpp). """ @@ -953,9 +953,9 @@ def codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, 'getoption_handlers': '\n'.join(getoption_handlers), 'setoption_handlers': '\n'.join(setoption_handlers), } - write_file(dst_dir, 'options.h', tpl_options_h.format(**data)) - write_file(dst_dir, 'options.cpp', tpl_options_cpp.format(**data)) - write_file(dst_dir, 'options_public.cpp', tpl_options_public.format(**data)) + for tpl in tpls: + write_file(dst_dir, tpl['output'], tpl['content'].format(**data)) + if os.path.isdir('{}/docs/'.format(build_dir)): sphinxgen.render('{}/docs/'.format(build_dir), 'options_generated.rst') @@ -1091,13 +1091,21 @@ def mkoptions_main(): for file in filenames: if not os.path.exists(file): die("configuration file '{}' does not exist".format(file)) + + module_tpls = [ + {'input': 'options/module_template.h'}, + {'input': 'options/module_template.cpp'}, + ] + global_tpls = [ + {'input': 'options/options_template.h'}, + {'input': 'options/options_template.cpp'}, + {'input': 'options/options_public_template.cpp'}, + ] + + for tpl in module_tpls + global_tpls: + tpl['output'] = tpl['input'].replace('_template', '') + tpl['content'] = read_tpl(src_dir, tpl['input']) - # Read source code template files from source directory. - tpl_module_h = read_tpl(src_dir, 'module_template.h') - tpl_module_cpp = read_tpl(src_dir, 'module_template.cpp') - tpl_options_public = read_tpl(src_dir, 'options_public_template.cpp') - tpl_options_h = read_tpl(src_dir, 'options_template.h') - tpl_options_cpp = read_tpl(src_dir, 'options_template.cpp') # Parse files, check attributes and create module/option objects modules = [] @@ -1113,10 +1121,10 @@ def mkoptions_main(): # Create *_options.{h,cpp} in destination directory for module in modules: - codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp) + codegen_module(module, dst_dir, module_tpls) # Create options.cpp in destination directory - codegen_all_modules(modules, build_dir, dst_dir, tpl_options_h, tpl_options_cpp, tpl_options_public) + codegen_all_modules(modules, build_dir, dst_dir, global_tpls) if __name__ == "__main__": diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp index bc953b952..0d5e2d4ee 100644 --- a/src/options/module_template.cpp +++ b/src/options/module_template.cpp @@ -31,13 +31,13 @@ namespace options { ${defs}$ -${modes}$ +${modes_impl}$ namespace ${id}$ { // clang-format off -${defaults}$ +${defaults_impl}$ // clang-format on } diff --git a/src/options/module_template.h b/src/options/module_template.h index a74d3c49d..a0719ea32 100644 --- a/src/options/module_template.h +++ b/src/options/module_template.h @@ -31,7 +31,7 @@ namespace cvc5 { namespace options { // clang-format off -${modes}$ +${modes_decl}$ // clang-format on #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) @@ -74,7 +74,7 @@ ${inls}$ namespace ${id}$ { // clang-format off -${defaults}$ +${defaults_decl}$ // clang-format on } -- 2.30.2