From 92fa57d6ec03ea19cf5ef177905ee59f29231e8f Mon Sep 17 00:00:00 2001 From: Aina Niemetz Date: Tue, 20 Apr 2021 11:58:46 -0700 Subject: [PATCH] Add guards to disable clang-format around placeholders in templates. (#6375) --- src/expr/kind_template.cpp | 20 ++++-- src/expr/kind_template.h | 22 +++--- src/expr/metakind_template.cpp | 20 +++--- src/expr/metakind_template.h | 9 ++- src/expr/type_checker_template.cpp | 34 +++++---- src/expr/type_properties_template.h | 20 +++++- src/options/options_template.cpp | 59 +++++++++------ src/theory/rewriter_tables_template.h | 95 ++++++++++++++++--------- src/theory/theory_traits_template.h | 20 ++++-- src/theory/type_enumerator_template.cpp | 7 +- 10 files changed, 201 insertions(+), 105 deletions(-) diff --git a/src/expr/kind_template.cpp b/src/expr/kind_template.cpp index da1a75499..49f815b68 100644 --- a/src/expr/kind_template.cpp +++ b/src/expr/kind_template.cpp @@ -32,7 +32,9 @@ const char* toString(cvc5::Kind k) /* special cases */ case UNDEFINED_KIND: return "UNDEFINED_KIND"; case NULL_EXPR: return "NULL"; + // clang-format off ${kind_printers} + // clang-format on case LAST_KIND: return "LAST_KIND"; default: return "?"; } @@ -70,7 +72,9 @@ const char* toString(TypeConstant tc) { switch (tc) { + // clang-format off ${type_constant_descriptions} + // clang-format on default: return "UNKNOWN_TYPE_CONSTANT"; } } @@ -83,13 +87,15 @@ namespace theory { TheoryId kindToTheoryId(::cvc5::Kind k) { - switch(k) { - case kind::UNDEFINED_KIND: - case kind::NULL_EXPR: - break; + switch (k) + { + case kind::UNDEFINED_KIND: + case kind::NULL_EXPR: + break; + // clang-format off ${kind_to_theory_id} - case kind::LAST_KIND: - break; + // clang-format on + case kind::LAST_KIND: break; } throw IllegalArgumentException("", "k", __PRETTY_FUNCTION__, "bad kind"); } @@ -98,7 +104,9 @@ TheoryId typeConstantToTheoryId(::cvc5::TypeConstant typeConstant) { switch (typeConstant) { + // clang-format off ${type_constant_to_theory_id} + // clang-format on case LAST_TYPE: break; } throw IllegalArgumentException( diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h index 6e2362e84..cc4286d25 100644 --- a/src/expr/kind_template.h +++ b/src/expr/kind_template.h @@ -28,9 +28,11 @@ namespace kind { enum Kind_t { - UNDEFINED_KIND = -1, /**< undefined */ - NULL_EXPR, /**< Null kind */ + UNDEFINED_KIND = -1, /**< undefined */ + NULL_EXPR, /**< Null kind */ + // clang-format off ${kind_decls} LAST_KIND /**< marks the upper-bound of this enumeration */ + // clang-format on }; /* enum Kind_t */ @@ -69,9 +71,10 @@ std::ostream& operator<<(std::ostream&, cvc5::Kind); bool isAssociative(::cvc5::Kind k); std::string kindToString(::cvc5::Kind k); -struct KindHashFunction { +struct KindHashFunction +{ inline size_t operator()(::cvc5::Kind k) const { return k; } -};/* struct KindHashFunction */ +}; /* struct KindHashFunction */ } // namespace kind @@ -80,17 +83,18 @@ struct KindHashFunction { */ enum TypeConstant { + // clang-format off ${type_constant_list} LAST_TYPE + // clang-format on }; /* enum TypeConstant */ /** * We hash the constants with their values. */ -struct TypeConstantHashFunction { - inline size_t operator()(TypeConstant tc) const { - return tc; - } -};/* struct TypeConstantHashFunction */ +struct TypeConstantHashFunction +{ + inline size_t operator()(TypeConstant tc) const { return tc; } +}; /* struct TypeConstantHashFunction */ const char* toString(TypeConstant tc); std::ostream& operator<<(std::ostream& out, TypeConstant typeConstant); diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp index 01b0c01a8..1b05815d8 100644 --- a/src/expr/metakind_template.cpp +++ b/src/expr/metakind_template.cpp @@ -26,15 +26,15 @@ namespace kind { /** * Get the metakind for a particular kind. */ -MetaKind metaKindOf(Kind k) { +MetaKind metaKindOf(Kind k) +{ static const MetaKind metaKinds[] = { - metakind::INVALID, /* UNDEFINED_KIND */ - metakind::INVALID, /* NULL_EXPR */ -// clang-format off -${metakind_kinds} -// clang-format on - metakind::INVALID /* LAST_KIND */ - };/* metaKinds[] */ + metakind::INVALID, /* UNDEFINED_KIND */ + metakind::INVALID, /* NULL_EXPR */ + // clang-format off +${metakind_kinds} // clang-format on + metakind::INVALID /* LAST_KIND */ + }; /* metaKinds[] */ Assert(k >= kind::NULL_EXPR && k < kind::LAST_KIND); @@ -42,7 +42,7 @@ ${metakind_kinds} // handle the UNDEFINED_KIND (-1) case. If we don't, the compiler // emits warnings for non-assertion builds, since the check isn't done. return metaKinds[k + 1]; -}/* metaKindOf(k) */ +} /* metaKindOf(k) */ } // namespace kind @@ -64,7 +64,7 @@ size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv) switch (nv->d_kind) { // clang-format off -${metakind_constHashes} + ${metakind_constHashes} // clang-format on default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind); } diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h index 1271c2e64..760cda981 100644 --- a/src/expr/metakind_template.h +++ b/src/expr/metakind_template.h @@ -129,14 +129,18 @@ struct NodeValuePoolEq { #endif /* CVC5__KIND__METAKIND_H */ +// clang-format off ${metakind_includes} +// clang-format on #ifdef CVC5__NODE_MANAGER_NEEDS_CONSTANT_MAP namespace cvc5 { namespace expr { +// clang-format off ${metakind_getConst_decls} +// clang-format on } // namespace expr namespace kind { @@ -170,9 +174,12 @@ inline size_t NodeValueConstCompare::constHash( return nv->getConst().hash(); } +// clang-format off ${metakind_constantMaps_decls} +// clang-format on -struct NodeValueConstPrinter { +struct NodeValueConstPrinter +{ static void toStream(std::ostream& out, const ::cvc5::expr::NodeValue* nv); static void toStream(std::ostream& out, TNode n); }; diff --git a/src/expr/type_checker_template.cpp b/src/expr/type_checker_template.cpp index 3944fac11..af9b9b876 100644 --- a/src/expr/type_checker_template.cpp +++ b/src/expr/type_checker_template.cpp @@ -20,7 +20,9 @@ #include "expr/type_checker.h" #include "expr/type_checker_util.h" +// clang-format off ${typechecker_includes} +// clang-format on namespace cvc5 { namespace expr { @@ -30,20 +32,23 @@ TypeNode TypeChecker::computeType(NodeManager* nodeManager, TNode n, bool check) TypeNode typeNode; // Infer the type - switch(n.getKind()) { - case kind::VARIABLE: - case kind::SKOLEM: - typeNode = nodeManager->getAttribute(n, TypeAttr()); - break; - case kind::BUILTIN: - typeNode = nodeManager->builtinOperatorType(); - break; - + switch (n.getKind()) + { + case kind::VARIABLE: + case kind::SKOLEM: + typeNode = nodeManager->getAttribute(n, TypeAttr()); + break; + case kind::BUILTIN: + typeNode = nodeManager->builtinOperatorType(); + break; + + // clang-format off ${typerules} + // clang-format on - default: - Debug("getType") << "FAILURE" << std::endl; - Unhandled() << " " << n.getKind(); + default: + Debug("getType") << "FAILURE" << std::endl; + Unhandled() << " " << n.getKind(); } nodeManager->setAttribute(n, TypeAttr(), typeNode); @@ -60,8 +65,11 @@ bool TypeChecker::computeIsConst(NodeManager* nodeManager, TNode n) || n.getMetaKind() == kind::metakind::PARAMETERIZED || n.getMetaKind() == kind::metakind::NULLARY_OPERATOR); - switch(n.getKind()) { + switch (n.getKind()) + { + // clang-format off ${construles} + // clang-format on default:; } diff --git a/src/expr/type_properties_template.h b/src/expr/type_properties_template.h index 77a671a68..40ead9a5e 100644 --- a/src/expr/type_properties_template.h +++ b/src/expr/type_properties_template.h @@ -26,7 +26,9 @@ #include "expr/type_node.h" #include "options/language.h" +// clang-format off ${type_properties_includes} +// clang-format on namespace cvc5 { namespace kind { @@ -41,7 +43,9 @@ inline Cardinality getCardinality(TypeConstant tc) { switch (tc) { + // clang-format off ${type_constant_cardinalities} + // clang-format on default: InternalError() << "No cardinality known for type constant " << tc; } } /* getCardinality(TypeConstant) */ @@ -57,7 +61,9 @@ inline Cardinality getCardinality(TypeNode typeNode) { switch(Kind k = typeNode.getKind()) { case TYPE_CONSTANT: return getCardinality(typeNode.getConst()); + // clang-format off ${type_cardinalities} + // clang-format on default: InternalError() << "A theory kinds file did not provide a cardinality " << "or cardinality computer for type:\n" @@ -67,10 +73,12 @@ ${type_cardinalities} inline bool isWellFounded(TypeConstant tc) { switch(tc) { + // clang-format off ${type_constant_wellfoundednesses} -default: - InternalError() << "No well-foundedness status known for type constant: " - << tc; + // clang-format on + default: + InternalError() << "No well-foundedness status known for type constant: " + << tc; } }/* isWellFounded(TypeConstant) */ @@ -79,7 +87,9 @@ inline bool isWellFounded(TypeNode typeNode) { switch(Kind k = typeNode.getKind()) { case TYPE_CONSTANT: return isWellFounded(typeNode.getConst()); + // clang-format off ${type_wellfoundednesses} + // clang-format on default: InternalError() << "A theory kinds file did not provide a well-foundedness " << "or well-foundedness computer for type:\n" @@ -91,7 +101,9 @@ inline Node mkGroundTerm(TypeConstant tc) { switch (tc) { + // clang-format off ${type_constant_groundterms} + // clang-format on default: InternalError() << "No ground term known for type constant: " << tc; } @@ -104,7 +116,9 @@ inline Node mkGroundTerm(TypeNode typeNode) { case TYPE_CONSTANT: return mkGroundTerm(typeNode.getConst()); + // clang-format off ${type_groundterms} + // clang-format on default: InternalError() << "A theory kinds file did not provide a ground term " << "or ground term computer for type:\n" diff --git a/src/options/options_template.cpp b/src/options/options_template.cpp index b9b80aa7e..c06a7aab3 100644 --- a/src/options/options_template.cpp +++ b/src/options/options_template.cpp @@ -65,6 +65,7 @@ ${headers_handler}$ using namespace cvc5; using namespace cvc5::options; +// clang-format on namespace cvc5 { @@ -249,7 +250,9 @@ std::string Options::formatThreadOptionException(const std::string& option) { void Options::setListener(OptionsListener* ol) { d_olisten = ol; } +// clang-format off ${custom_handlers}$ +// clang-format on #if defined(CVC5_MUZZLED) || defined(CVC5_COMPETITION_MODE) # define DO_SEMANTIC_CHECKS_BY_DEFAULT false @@ -257,22 +260,26 @@ ${custom_handlers}$ # define DO_SEMANTIC_CHECKS_BY_DEFAULT true #endif /* CVC5_MUZZLED || CVC5_COMPETITION_MODE */ +// clang-format off options::OptionsHolder::OptionsHolder() : ${module_defaults}$ { } +// clang-format on - -static const std::string mostCommonOptionsDescription = "\ +static const std::string mostCommonOptionsDescription = + "\ Most commonly-used cvc5 options:\n" -${help_common}$; - + // clang-format off +${help_common}$ + // clang-format on + ; -static const std::string optionsDescription = mostCommonOptionsDescription + "\n\ -\n\ -Additional cvc5 options:\n" +// clang-format off +static const std::string optionsDescription = + mostCommonOptionsDescription + "\n\nAdditional cvc5 options:\n" ${help_others}$; - +// clang-format on static const std::string optionsFootnote = "\n\ [*] Each of these options has a --no-OPTIONNAME variant, which reverses the\n\ @@ -343,10 +350,11 @@ void Options::printLanguageHelp(std::ostream& out) { * If you add something that has a short option equivalent, you should * add it to the getopt_long() call in parseOptions(). */ +// clang-format off static struct option cmdlineOptions[] = { ${cmdline_options}$ - { NULL, no_argument, NULL, '\0' } -};/* cmdlineOptions */ + {nullptr, no_argument, nullptr, '\0'}}; +// clang-format on namespace options { @@ -469,9 +477,11 @@ void Options::parseOptionsRecursive(Options* options, Debug("options") << "[ before, optind == " << optind << " ]" << std::endl; Debug("options") << "[ argc == " << argc << ", argv == " << argv << " ]" << std::endl; + // clang-format off int c = getopt_long(argc, argv, "+:${options_short}$", cmdlineOptions, NULL); + // clang-format on main_optind = optind; @@ -503,23 +513,24 @@ void Options::parseOptionsRecursive(Options* options, Debug("preemptGetopt") << "processing option " << c << " (`" << char(c) << "'), " << option << std::endl; + // clang-format off switch(c) { ${options_handler}$ - - case ':': + case ':' : // This can be a long or short option, and the way to get at the // name of it is different. - throw OptionException(std::string("option `") + option + - "' missing its required argument"); + throw OptionException(std::string("option `") + option + + "' missing its required argument"); - case '?': - default: - throw OptionException(std::string("can't understand option `") + option + - "'" + suggestCommandLineOptions(option)); + case '?': + default: + throw OptionException(std::string("can't understand option `") + option + + "'" + suggestCommandLineOptions(option)); } } + // clang-format on Debug("options") << "got " << nonoptions->size() << " non-option arguments." << std::endl; @@ -537,10 +548,11 @@ std::string Options::suggestCommandLineOptions(const std::string& optionName) return didYouMean.getMatchAsString(optionName.substr(0, optionName.find('='))); } +// clang-format off static const char* smtOptions[] = { ${options_smt}$ - NULL -};/* smtOptions[] */ + nullptr}; +// clang-format on std::vector Options::suggestSmtOptions( const std::string& optionName) @@ -557,15 +569,16 @@ std::vector Options::suggestSmtOptions( return suggestions; } +// clang-format off std::vector > Options::getOptions() const { std::vector< std::vector > opts; ${options_getoptions}$ - return opts; } +// clang-format on void Options::setOption(const std::string& key, const std::string& optionarg) { @@ -580,6 +593,7 @@ void Options::setOption(const std::string& key, const std::string& optionarg) } } +// clang-format off void Options::setOptionInternal(const std::string& key, const std::string& optionarg) { @@ -588,7 +602,9 @@ void Options::setOptionInternal(const std::string& key, ${setoption_handlers}$ throw UnrecognizedOptionException(key); } +// clang-format on +// clang-format off std::string Options::getOption(const std::string& key) const { Trace("options") << "Options::getOption(" << key << ")" << std::endl; @@ -596,6 +612,7 @@ std::string Options::getOption(const std::string& key) const throw UnrecognizedOptionException(key); } +// clang-format on #undef USE_EARLY_TYPE_CHECKING_BY_DEFAULT #undef DO_SEMANTIC_CHECKS_BY_DEFAULT diff --git a/src/theory/rewriter_tables_template.h b/src/theory/rewriter_tables_template.h index 5c52e79b5..c549f8cfb 100644 --- a/src/theory/rewriter_tables_template.h +++ b/src/theory/rewriter_tables_template.h @@ -20,76 +20,101 @@ #pragma once +#include "expr/attribute.h" +#include "expr/attribute_unique_id.h" #include "theory/rewriter.h" #include "theory/rewriter_attributes.h" -#include "expr/attribute_unique_id.h" -#include "expr/attribute.h" +// clang-format off ${rewriter_includes} +// clang-format on namespace cvc5 { namespace theory { -Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) { - switch(theoryId) { +Node Rewriter::getPreRewriteCache(theory::TheoryId theoryId, TNode node) +{ + switch (theoryId) + { + // clang-format off ${pre_rewrite_get_cache} - default: - Unreachable(); + // clang-format on + default: Unreachable(); } } -Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) { - switch(theoryId) { +Node Rewriter::getPostRewriteCache(theory::TheoryId theoryId, TNode node) +{ + switch (theoryId) + { + // clang-format off ${post_rewrite_get_cache} - default: - Unreachable(); + // clang-format on + default: Unreachable(); } } -void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) { - switch(theoryId) { +void Rewriter::setPreRewriteCache(theory::TheoryId theoryId, + TNode node, + TNode cache) +{ + switch (theoryId) + { + // clang-format off ${pre_rewrite_set_cache} - default: - Unreachable(); + // clang-format on + default: Unreachable(); } } -void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, TNode node, TNode cache) { - switch(theoryId) { +void Rewriter::setPostRewriteCache(theory::TheoryId theoryId, + TNode node, + TNode cache) +{ + switch (theoryId) + { + // clang-format off ${post_rewrite_set_cache} - default: - Unreachable(); + // clang-format on + default: Unreachable(); } } Rewriter::Rewriter() : d_tpg(nullptr) { -for (size_t i = 0; i < kind::LAST_KIND; ++i) -{ - d_preRewriters[i] = nullptr; - d_postRewriters[i] = nullptr; -} + for (size_t i = 0; i < kind::LAST_KIND; ++i) + { + d_preRewriters[i] = nullptr; + d_postRewriters[i] = nullptr; + } -for (size_t i = 0; i < theory::THEORY_LAST; ++i) -{ - d_preRewritersEqual[i] = nullptr; - d_postRewritersEqual[i] = nullptr; -} + for (size_t i = 0; i < theory::THEORY_LAST; ++i) + { + d_preRewritersEqual[i] = nullptr; + d_postRewritersEqual[i] = nullptr; + } } -void Rewriter::clearCachesInternal() { +void Rewriter::clearCachesInternal() +{ typedef cvc5::expr::attr::AttributeUniqueId AttributeUniqueId; std::vector preids; - ${pre_rewrite_attribute_ids} + // clang-format off + ${pre_rewrite_attribute_ids} // clang-format on - std::vector postids; - ${post_rewrite_attribute_ids} + std::vector + postids; + // clang-format off + ${post_rewrite_attribute_ids} // clang-format on - std::vector allids; - for(unsigned i = 0; i < preids.size(); ++i){ + std::vector + allids; + for (size_t i = 0, size = preids.size(); i < size; ++i) + { allids.push_back(&preids[i]); } - for(unsigned i = 0; i < postids.size(); ++i){ + for (size_t i = 0, size = postids.size(); i < size; ++i) + { allids.push_back(&postids[i]); } NodeManager::currentNM()->deleteAttributes(allids); diff --git a/src/theory/theory_traits_template.h b/src/theory/theory_traits_template.h index 75a922096..fa6552be1 100644 --- a/src/theory/theory_traits_template.h +++ b/src/theory/theory_traits_template.h @@ -25,7 +25,9 @@ #include "options/theory_options.h" #include "theory/theory.h" +// clang-format off ${theory_includes} +// clang-format on namespace cvc5 { namespace theory { @@ -33,15 +35,21 @@ namespace theory { template struct TheoryTraits; +// clang-format off ${theory_traits} - -struct TheoryConstructor { - static void addTheory(TheoryEngine* engine, TheoryId id) { - switch(id) { - +// clang-format on + +struct TheoryConstructor +{ + static void addTheory(TheoryEngine* engine, TheoryId id) + { + switch (id) + { + // clang-format off ${theory_constructors} + // clang-format on -default: Unhandled() << id; + default: Unhandled() << id; } } }; /* struct cvc5::theory::TheoryConstructor */ diff --git a/src/theory/type_enumerator_template.cpp b/src/theory/type_enumerator_template.cpp index a8ffc8b2d..4f942d6c6 100644 --- a/src/theory/type_enumerator_template.cpp +++ b/src/theory/type_enumerator_template.cpp @@ -19,8 +19,9 @@ #include "expr/kind.h" #include "theory/type_enumerator.h" - +// clang-format off ${type_enumerator_includes} +// clang-format on using namespace std; @@ -35,11 +36,15 @@ TypeEnumeratorInterface* TypeEnumerator::mkTypeEnumerator( case kind::TYPE_CONSTANT: switch (type.getConst()) { + // clang-format off ${mk_type_enumerator_type_constant_cases} + // clang-format on default: Unhandled() << "No type enumerator for type `" << type << "'"; } Unreachable(); + // clang-format off ${mk_type_enumerator_cases} + // clang-format on default: Unhandled() << "No type enumerator for type `" << type << "'"; } Unreachable(); -- 2.30.2