From: Gereon Kremer <nafur42@gmail.com>
Date: Mon, 10 May 2021 22:22:24 +0000 (+0200)
Subject: Remove header for option modules (#6514)
X-Git-Tag: cvc5-1.0.0~1774
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=cd1f1c3f308b67fc4b8f006196e5bc1f366cc10d;p=cvc5.git

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 2afe92ccd..c472bad3f 100644
--- 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 309370163..6017edfd5 100644
--- 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 eb3a13778..2c61e057c 100644
--- 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 811e0fdd2..52725bb8e 100644
--- 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 6ef79cd0b..b5f2ed593 100644
--- 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 e6ef18311..3172f8d5f 100644
--- 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 cf1ac5f49..107c7dd94 100644
--- 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 68698b3a1..d8c8a15b6 100644
--- 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 34a4fb979..52f351348 100644
--- 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 af8d044f7..d726cec3b 100644
--- 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 f014068f3..ccbf2e6ae 100644
--- 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 b632b3384..74e8d690d 100644
--- 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 e0b3f79d1..0a4d594b2 100644
--- 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 559f4a5e4..b668a1e3f 100644
--- 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 56568bc0c..4b3d01b99 100644
--- 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 d72279f95..433e6f613 100644
--- 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 177307918..f0875455f 100644
--- 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 0670bb7da..9cddc9470 100644
--- 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 ce2e1ab32..20376c053 100644
--- 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 8f1c28ca5..85cdf1bef 100644
--- 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 9e808df98..f45e78c98 100644
--- 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 0f206f980..db9cfa480 100644
--- 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 3d0cb6d8d..7328c44ad 100644
--- 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 4672bbb6e..44c9c191f 100644
--- 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 a0f769684..0c4fa7aca 100644
--- 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 bd0027fb4..8b99493e1 100644
--- 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"