From cd1f1c3f308b67fc4b8f006196e5bc1f366cc10d Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Tue, 11 May 2021 00:22:24 +0200 Subject: [PATCH] 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. --- src/options/arith_options.toml | 1 - src/options/arrays_options.toml | 1 - src/options/base_options.toml | 1 - src/options/booleans_options.toml | 2 +- src/options/builtin_options.toml | 2 +- src/options/bv_options.toml | 1 - src/options/datatypes_options.toml | 1 - src/options/decision_options.toml | 1 - src/options/expr_options.toml | 1 - src/options/fp_options.toml | 1 - src/options/main_options.toml | 1 - src/options/mkoptions.py | 19 ++++++++++--------- src/options/module_template.cpp | 1 + src/options/module_template.h | 6 +++--- src/options/parser_options.toml | 1 - src/options/printer_options.toml | 1 - src/options/proof_options.toml | 1 - src/options/prop_options.toml | 1 - src/options/quantifiers_options.toml | 1 - src/options/resource_manager_options.toml | 1 - src/options/sep_options.toml | 1 - src/options/sets_options.toml | 1 - src/options/smt_options.toml | 1 - src/options/strings_options.toml | 1 - src/options/theory_options.toml | 1 - src/options/uf_options.toml | 1 - 26 files changed, 16 insertions(+), 35 deletions(-) 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 _options.toml configuration file, mkoptions.py * expands this template and generates a _options.cpp file. */ +#include "${header}$" #include 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" -- 2.30.2