Remove header for option modules (#6514)

This PR further simplifies the option declaration by removing the header attribute from module options.
Instead of specifying it manually, it is now automatically generated from the filename of the toml file. The header files and the toml files use matching names already, so this PR simply removes another mechanism that is not used anyway.
This PR also does a minor cleanup of the Options class in the mkoptions.py script.

diff --git a/src/options/arith_options.toml b/src/options/arith_options.toml
index 2afe92ccd5af49cdf5b9d968d495f032a604ca80..c472bad3f180914ba5f469e42ee0c67689196815 100644 (file)
--- a/src/options/arith_options.toml
+++ b/src/options/arith_options.toml
@@ -1,6 +1,5 @@
 id     = "ARITH"
 name   = "Arithmetic theory"
-header = "options/arith_options.h"
 
 [[option]]
   name       = "arithUnateLemmaMode"

diff --git a/src/options/arrays_options.toml b/src/options/arrays_options.toml
index 309370163236cb4a888b9576457c160e0c813b12..6017edfd55406d671826309eaf2349111c969631 100644 (file)
--- a/src/options/arrays_options.toml
+++ b/src/options/arrays_options.toml
@@ -1,6 +1,5 @@
 id     = "ARRAYS"
 name   = "Arrays theory"
-header = "options/arrays_options.h"
 
 [[option]]
   name       = "arraysOptimizeLinear"

diff --git a/src/options/base_options.toml b/src/options/base_options.toml
index eb3a13778434bc4ecc7a7bc70ff3a9392d53d589..2c61e057c5abd51c9ba190eac75dc5602866696e 100644 (file)
--- a/src/options/base_options.toml
+++ b/src/options/base_options.toml
@@ -1,6 +1,5 @@
 id     = "BASE"
 name   = "Base"
-header = "options/base_options.h"
 
 [[option]]
   name       = "binary_name"

diff --git a/src/options/booleans_options.toml b/src/options/booleans_options.toml
index 811e0fdd2a765ed7185cac8b75a79ca790c72373..52725bb8e60fd8f4af204849cbbfe1aae2d7f04a 100644 (file)
--- a/src/options/booleans_options.toml
+++ b/src/options/booleans_options.toml
@@ -1,3 +1,3 @@
 id     = "BOOLEANS"
 name   = "Boolean theory"
-header = "options/booleans_options.h"
+

diff --git a/src/options/builtin_options.toml b/src/options/builtin_options.toml
index 6ef79cd0bd5181b867ae0130a9423a0a6bdacd2f..b5f2ed593d6aaa2ba4ca0a69302c081def1585b0 100644 (file)
--- a/src/options/builtin_options.toml
+++ b/src/options/builtin_options.toml
@@ -1,3 +1,3 @@
 id     = "BUILTIN"
 name   = "Builtin theory"
-header = "options/builtin_options.h"
+

diff --git a/src/options/bv_options.toml b/src/options/bv_options.toml
index e6ef18311cb986db1ff2526cea24c6a9c3217a5b..3172f8d5f2a19a653d09749398f477154f8dee7e 100644 (file)
--- a/src/options/bv_options.toml
+++ b/src/options/bv_options.toml
@@ -1,6 +1,5 @@
 id     = "BV"
 name   = "Bitvector theory"
-header = "options/bv_options.h"
 
 [[option]]
   name       = "bvSatSolver"

diff --git a/src/options/datatypes_options.toml b/src/options/datatypes_options.toml
index cf1ac5f49412923c848173b0f04518c25a915d51..107c7dd94c22439a46de5b214a4bc163e24ce88a 100644 (file)
--- a/src/options/datatypes_options.toml
+++ b/src/options/datatypes_options.toml
@@ -1,6 +1,5 @@
 id     = "DATATYPES"
 name   = "Datatypes theory"
-header = "options/datatypes_options.h"
 
 # How to handle selectors applied to incorrect constructors.  If this option is set,
 # then we do not rewrite such a selector term to an arbitrary ground term.  

diff --git a/src/options/decision_options.toml b/src/options/decision_options.toml
index 68698b3a1581deec5bee6b54e6ccbfe2310de2ba..d8c8a15b6c3dbb0669b2e14be1d5beef49b94772 100644 (file)
--- a/src/options/decision_options.toml
+++ b/src/options/decision_options.toml
@@ -1,6 +1,5 @@
 id     = "DECISION"
 name   = "Decision heuristics"
-header = "options/decision_options.h"
 
 [[option]]
   name       = "decisionMode"

diff --git a/src/options/expr_options.toml b/src/options/expr_options.toml
index 34a4fb979982537b8a79faf2a8bb787c394be0b8..52f3513488ac3ffa30d1e34783640badb907bff1 100644 (file)
--- a/src/options/expr_options.toml
+++ b/src/options/expr_options.toml
@@ -1,6 +1,5 @@
 id     = "EXPR"
 name   = "Expression package"
-header = "options/expr_options.h"
 
 [[option]]
   name       = "defaultExprDepth"

diff --git a/src/options/fp_options.toml b/src/options/fp_options.toml
index af8d044f7516f0cb562c92cd1f9f03d9da2df236..d726cec3b2451613802e64cbad903644d5ddad63 100644 (file)
--- a/src/options/fp_options.toml
+++ b/src/options/fp_options.toml
@@ -1,6 +1,5 @@
 id     = "FP"
 name   = "Fp"
-header = "options/fp_options.h"
 
 [[option]]
   name       = "fpExp"

diff --git a/src/options/main_options.toml b/src/options/main_options.toml
index f014068f35976765d649b742451c46b2223d2741..ccbf2e6aebb01f5d3257dc1d455d777b821bfdb4 100644 (file)
--- a/src/options/main_options.toml
+++ b/src/options/main_options.toml
@@ -1,6 +1,5 @@
 id     = "DRIVER"
 name   = "Driver"
-header = "options/main_options.h"
 
 [[option]]
   name       = "version"

diff --git a/src/options/mkoptions.py b/src/options/mkoptions.py
index b632b338498871f332a0fbe8454b8fc6d6685d21..74e8d690d29f9ec9b94b018b33efb9b437680cda 100644 (file)
--- a/src/options/mkoptions.py
+++ b/src/options/mkoptions.py
@@ -50,7 +50,7 @@ import toml
 
 ### Allowed attributes for module/option
 
-MODULE_ATTR_REQ = ['id', 'name', 'header']
+MODULE_ATTR_REQ = ['id', 'name']
 MODULE_ATTR_ALL = MODULE_ATTR_REQ + ['option']
 
 OPTION_ATTR_REQ = ['category', 'type']
@@ -232,13 +232,13 @@ class Module(object):
     An options module represents a MODULE_options.toml option configuration
     file and contains lists of options.
     """
-    def __init__(self, d):
-        self.__dict__ = dict((k, None) for k in MODULE_ATTR_ALL)
+    def __init__(self, d, filename):
+        self.__dict__ = {k: d.get(k, None) for k in MODULE_ATTR_ALL}
         self.options = []
-        for (attr, val) in d.items():
-            assert attr in self.__dict__
-            if val:
-                self.__dict__[attr] = val
+        self.id = self.id.lower()
+        self.id_cap = self.id.upper()
+        self.filename = os.path.splitext(os.path.split(filename)[-1])[0]
+        self.header = os.path.join('options', '{}.h'.format(self.filename))
 
 
 class Option(object):
@@ -526,6 +526,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
     write_file(dst_dir, '{}.h'.format(filename), tpl_module_h.format(
         filename=filename,
         header=module.header,
+        id_cap=module.id_cap,
         id=module.id,
         includes='\n'.join(sorted(list(includes))),
         holder_spec=' \\\n'.join(holder_specs),
@@ -535,7 +536,7 @@ def codegen_module(module, dst_dir, tpl_module_h, tpl_module_cpp):
         modes=''.join(mode_decl)))
 
     write_file(dst_dir, '{}.cpp'.format(filename), tpl_module_cpp.format(
-        filename=filename,
+        header=module.header,
         accs='\n'.join(accs),
         defs='\n'.join(defs),
         modes=''.join(mode_impl)))
@@ -909,7 +910,7 @@ def parse_module(filename, module):
     # attributes are defined.
     check_attribs(filename,
                   MODULE_ATTR_REQ, MODULE_ATTR_ALL, module, 'module')
-    res = Module(module)
+    res = Module(module, filename)
 
     if 'option' in module:
         for attribs in module['option']:

diff --git a/src/options/module_template.cpp b/src/options/module_template.cpp
index e0b3f79d18b7eebae5b3f4259929d49b060badcd..0a4d594b2be3b927071c3d818381cafc2da005c5 100644 (file)
--- a/src/options/module_template.cpp
+++ b/src/options/module_template.cpp
@@ -15,6 +15,7 @@
  * For each <module>_options.toml configuration file, mkoptions.py
  * expands this template and generates a <module>_options.cpp file.
  */
+#include "${header}$"
 
 #include <iostream>
 

diff --git a/src/options/module_template.h b/src/options/module_template.h
index 559f4a5e4db594cf93cb5cb0453492ea62f71a0f..b668a1e3f31cf22b1f6d2b3fcbd228a522d9ef9f 100644 (file)
--- a/src/options/module_template.h
+++ b/src/options/module_template.h
@@ -18,8 +18,8 @@
 
 #include "cvc5_private.h"
 
-#ifndef CVC5__OPTIONS__${id}$_H
-#define CVC5__OPTIONS__${id}$_H
+#ifndef CVC5__OPTIONS__${id_cap}$_H
+#define CVC5__OPTIONS__${id_cap}$_H
 
 #include "options/options.h"
 
@@ -45,5 +45,5 @@ ${inls}$
 }  // namespace options
 }  // namespace cvc5
 
-#endif /* CVC5__OPTIONS__${id}$_H */
+#endif /* CVC5__OPTIONS__${id_cap}$_H */
 //clang-format on

diff --git a/src/options/parser_options.toml b/src/options/parser_options.toml
index 56568bc0c8ebb0e4f779b828495e4f1cc527ff53..4b3d01b9972615d25a40a2b5f3335ab18df5d382 100644 (file)
--- a/src/options/parser_options.toml
+++ b/src/options/parser_options.toml
@@ -1,6 +1,5 @@
 id     = "PARSER"
 name   = "Parser"
-header = "options/parser_options.h"
 
 [[option]]
   name       = "strictParsing"

diff --git a/src/options/printer_options.toml b/src/options/printer_options.toml
index d72279f95e067db5bb4fa9dbbe81fc09e57ee376..433e6f613b77ce39bfeeae4ee38f2cdf667d7117 100644 (file)
--- a/src/options/printer_options.toml
+++ b/src/options/printer_options.toml
@@ -1,6 +1,5 @@
 id     = "PRINTER"
 name   = "Printing"
-header = "options/printer_options.h"
 
 [[option]]
   name       = "modelFormatMode"

diff --git a/src/options/proof_options.toml b/src/options/proof_options.toml
index 177307918a132a1107e1e74d98559cc5cfd735d7..f0875455fbfdede152c57ff4087efcbe7ea9f4f4 100644 (file)
--- a/src/options/proof_options.toml
+++ b/src/options/proof_options.toml
@@ -1,6 +1,5 @@
 id     = "PROOF"
 name   = "Proof"
-header = "options/proof_options.h"
 
 [[option]]
   name       = "proofFormatMode"

diff --git a/src/options/prop_options.toml b/src/options/prop_options.toml
index 0670bb7da00a037125bc91d60ef0bda549203f78..9cddc94701b8123571eaa9c864695475ed936b0c 100644 (file)
--- a/src/options/prop_options.toml
+++ b/src/options/prop_options.toml
@@ -1,6 +1,5 @@
 id     = "PROP"
 name   = "SAT layer"
-header = "options/prop_options.h"
 
 [[option]]
   name       = "satRandomFreq"

diff --git a/src/options/quantifiers_options.toml b/src/options/quantifiers_options.toml
index ce2e1ab321e27f2e12e38ecf605cbafe2666cb53..20376c0530667f506fe30d40f5736cd52ef9700e 100644 (file)
--- a/src/options/quantifiers_options.toml
+++ b/src/options/quantifiers_options.toml
@@ -1,6 +1,5 @@
 id     = "QUANTIFIERS"
 name   = "Quantifiers"
-header = "options/quantifiers_options.h"
 
 # Whether to mini-scope quantifiers.
 # For example, forall x. ( P( x ) ^ Q( x ) ) will be rewritten to

diff --git a/src/options/resource_manager_options.toml b/src/options/resource_manager_options.toml
index 8f1c28ca521deb7daadb9032f15259cb61196856..85cdf1befb05ac87b213b9870145e6e12ba3754d 100644 (file)
--- a/src/options/resource_manager_options.toml
+++ b/src/options/resource_manager_options.toml
@@ -1,6 +1,5 @@
 id     = "resource_manager"
 name   = "Resource Manager options"
-header = "options/resource_manager_options.h"
 
 [[option]]
   name       = "cumulativeMillisecondLimit"

diff --git a/src/options/sep_options.toml b/src/options/sep_options.toml
index 9e808df98475a489be90e8939d1a625fd23e0b44..f45e78c980c029d205f1b97e20e65dd2e6b643c5 100644 (file)
--- a/src/options/sep_options.toml
+++ b/src/options/sep_options.toml
@@ -1,6 +1,5 @@
 id     = "SEP"
 name   = "Sep"
-header = "options/sep_options.h"
 
 [[option]]
   name       = "sepCheckNeg"

diff --git a/src/options/sets_options.toml b/src/options/sets_options.toml
index 0f206f980862604056d4cb4f9f60bcf77df29a0c..db9cfa480329ef6d4e693760101008ac21424693 100644 (file)
--- a/src/options/sets_options.toml
+++ b/src/options/sets_options.toml
@@ -1,6 +1,5 @@
 id     = "SETS"
 name   = "Sets"
-header = "options/sets_options.h"
 
 [[option]]
   name       = "setsProxyLemmas"

diff --git a/src/options/smt_options.toml b/src/options/smt_options.toml
index 3d0cb6d8d41b503542356849f6b2b995b25e849b..7328c44ad0a2451e618b341a51c59a077b7b576b 100644 (file)
--- a/src/options/smt_options.toml
+++ b/src/options/smt_options.toml
@@ -1,6 +1,5 @@
 id     = "SMT"
 name   = "SMT layer"
-header = "options/smt_options.h"
 
 [[option]]
   name       = "dumpModeString"

diff --git a/src/options/strings_options.toml b/src/options/strings_options.toml
index 4672bbb6e9224fa04d3e451c38af367e7da1ab72..44c9c191fe3b835f4c21cff2f3d02a9ca76b45c2 100644 (file)
--- a/src/options/strings_options.toml
+++ b/src/options/strings_options.toml
@@ -1,6 +1,5 @@
 id     = "STRINGS"
 name   = "Strings theory"
-header = "options/strings_options.h"
 
 [[option]]
   name       = "stringExp"

diff --git a/src/options/theory_options.toml b/src/options/theory_options.toml
index a0f769684a412a28e8ab2103f6c950260dccbff3..0c4fa7aca1ccac13b211ba804e5020e7f325b708 100644 (file)
--- a/src/options/theory_options.toml
+++ b/src/options/theory_options.toml
@@ -1,6 +1,5 @@
 id     = "THEORY"
 name   = "Theory layer"
-header = "options/theory_options.h"
 
 [[option]]
   name       = "theoryOfMode"

diff --git a/src/options/uf_options.toml b/src/options/uf_options.toml
index bd0027fb487ff7a144c88731ed4f652b41e9c040..8b99493e1d49784207b9d9c11a5ca98c0c1f42ff 100644 (file)
--- a/src/options/uf_options.toml
+++ b/src/options/uf_options.toml
@@ -1,6 +1,5 @@
 id     = "UF"
 name   = "Uninterpreted functions theory"
-header = "options/uf_options.h"
 
 [[option]]
   name       = "ufSymmetryBreaker"