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
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
add_subdirectory(base)
add_subdirectory(context)
add_subdirectory(expr)
-add_subdirectory(options)
if (NOT BUILD_LIB_ONLY)
add_subdirectory(parser)
endif()
+++ /dev/null
-###############################################################################
-# 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}
-)
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})
"""
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):
'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).
"""
'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')
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 = []
# 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__":
projects / cvc5.git / commitdiff