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.

5 files changed, 143 insertions, 151 deletions

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
@@ -1141,6 +1160,83 @@ 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
   ${PROJECT_SOURCE_DIR}/src/theory/builtin/kinds
@@ -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
 }