diff options
Diffstat (limited to 'src/options')
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 <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" |