Add guards to disable clang-format around placeholders in templates. (#6375)

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<k, pool>::constHash(
   return nv->getConst<T>().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<TypeConstant>());
+    // 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<TypeConstant>());
+    // 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<TypeConstant>());
+      // 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<std::string> Options::suggestSmtOptions(
     const std::string& optionName)
@@ -557,15 +569,16 @@ std::vector<std::string> Options::suggestSmtOptions(
   return suggestions;
 }
 
+// clang-format off
 std::vector<std::vector<std::string> > Options::getOptions() const
 {
   std::vector< std::vector<std::string> > 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<AttributeUniqueId> preids;
-  ${pre_rewrite_attribute_ids}
+  // clang-format off
+  ${pre_rewrite_attribute_ids}  // clang-format on
 
-  std::vector<AttributeUniqueId> postids;
-  ${post_rewrite_attribute_ids}
+  std::vector<AttributeUniqueId>
+      postids;
+  // clang-format off
+  ${post_rewrite_attribute_ids}  // clang-format on
 
-  std::vector<const AttributeUniqueId*> allids;
-  for(unsigned i = 0; i < preids.size(); ++i){
+  std::vector<const AttributeUniqueId*>
+      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 <TheoryId theoryId>
 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<TypeConstant>())
       {
+        // 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();