Rename CVC4_ macros to CVC5_. (#6327)

10 files changed, 60 insertions, 42 deletions

diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index 9f2301d7e..df621d860 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -28,9 +28,9 @@
 #include "expr/attribute_unique_id.h"
 
 // include supporting templates
-#define CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#define CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 #include "expr/attribute_internals.h"
-#undef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#undef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 
 namespace cvc5 {
 namespace expr {
diff --git a/src/expr/attribute_internals.h b/src/expr/attribute_internals.h
index 2293e4b5a..a0ef6ea02 100644
--- a/src/expr/attribute_internals.h
+++ b/src/expr/attribute_internals.h
@@ -16,9 +16,9 @@
 
 #include "cvc4_private.h"
 
-#ifndef CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
+#ifndef CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H
 #  error expr/attribute_internals.h should only be included by expr/attribute.h
-#endif /* CVC4_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
+#endif /* CVC5_ATTRIBUTE_H__INCLUDING__ATTRIBUTE_INTERNALS_H */
 
 #ifndef CVC5__EXPR__ATTRIBUTE_INTERNALS_H
 #define CVC5__EXPR__ATTRIBUTE_INTERNALS_H
diff --git a/src/expr/metakind_template.cpp b/src/expr/metakind_template.cpp
index 52502cbcd..451464d17 100644
--- a/src/expr/metakind_template.cpp
+++ b/src/expr/metakind_template.cpp
@@ -29,7 +29,9 @@ 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[] */
 
@@ -45,7 +47,9 @@ ${metakind_kinds}
 
 namespace expr {
 
+// clang-format off
 ${metakind_constantMaps}
+// clang-format on
 
 }  // namespace expr
 
@@ -58,7 +62,9 @@ size_t NodeValueCompare::constHash(const ::cvc5::expr::NodeValue* nv)
 
   switch (nv->d_kind)
   {
+// clang-format off
 ${metakind_constHashes}
+// clang-format on
 default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
@@ -75,7 +81,9 @@ bool NodeValueCompare::compare(const ::cvc5::expr::NodeValue* nv1,
   {
     switch (nv1->d_kind)
     {
+// clang-format off
 ${metakind_compares}
+// clang-format on
 default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv1->d_kind);
     }
   }
@@ -111,7 +119,9 @@ void NodeValueConstPrinter::toStream(std::ostream& out,
 
   switch (nv->d_kind)
   {
+// clang-format off
 ${metakind_constPrinters}
+// clang-format on
 default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
@@ -142,7 +152,9 @@ void deleteNodeValueConstant(::cvc5::expr::NodeValue* nv)
 
   switch (nv->d_kind)
   {
+// clang-format off
 ${metakind_constDeleters}
+// clang-format on
 default: Unhandled() << ::cvc5::expr::NodeValue::dKindToKind(nv->d_kind);
   }
 }
@@ -154,7 +166,9 @@ uint32_t getMinArityForKind(::cvc5::Kind k)
 {
   static const unsigned lbs[] = {
     0, /* NULL_EXPR */
+// clang-format off
 ${metakind_lbchildren}
+// clang-format on
 
     0 /* LAST_KIND */
   };
@@ -166,7 +180,9 @@ uint32_t getMaxArityForKind(::cvc5::Kind k)
 {
   static const unsigned ubs[] = {
     0, /* NULL_EXPR */
+// clang-format off
 ${metakind_ubchildren}
+// clang-format on
 
     0, /* LAST_KIND */
   };
@@ -188,11 +204,13 @@ Kind operatorToKind(::cvc5::expr::NodeValue* nv)
     return kind::APPLY_UF;
   }
 
-  switch(Kind k CVC4_UNUSED = nv->getKind()) {
-${metakind_operatorKinds}
+  switch (Kind k CVC5_UNUSED = nv->getKind())
+  {
+// clang-format off
+    ${metakind_operatorKinds}
+// clang-format on
 
-  default:
-    return kind::UNDEFINED_KIND;  /* LAST_KIND */
+    default: return kind::UNDEFINED_KIND; /* LAST_KIND */
   };
 }
 
diff --git a/src/expr/node.cpp b/src/expr/node.cpp
index 90d29f1eb..ec6b7c6fb 100644
--- a/src/expr/node.cpp
+++ b/src/expr/node.cpp
@@ -32,7 +32,7 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
                                                            std::string message)
     : Exception(message), d_node(new Node(node))
 {
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   std::stringstream ss;
   LastExceptionBuffer* current = LastExceptionBuffer::getCurrent();
   if(current != NULL){
@@ -48,7 +48,7 @@ TypeCheckingExceptionPrivate::TypeCheckingExceptionPrivate(TNode node,
     string ssstring = ss.str();
     current->setContents(ssstring.c_str());
   }
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 }
 
 TypeCheckingExceptionPrivate::~TypeCheckingExceptionPrivate() { delete d_node; }
diff --git a/src/expr/node.h b/src/expr/node.h
index b8e44a4cb..4554c1ee8 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -1435,7 +1435,7 @@ NodeTemplate<ref_count>::substitute(Iterator substitutionsBegin,
   }
 }
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
  * outside of gdb.  This writes to the Warning() stream and immediately
@@ -1488,7 +1488,7 @@ static void __attribute__((used)) debugPrintRawTNode(const NodeTemplate<false>&
   n.printAst(Warning(), 0);
   Warning().flush();
 }
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
 }  // namespace cvc5
 
diff --git a/src/expr/node_builder.cpp b/src/expr/node_builder.cpp
index 8c3e8d077..307c3aaf8 100644
--- a/src/expr/node_builder.cpp
+++ b/src/expr/node_builder.cpp
@@ -77,11 +77,11 @@ NodeBuilder::NodeBuilder(const NodeBuilder& nb)
 
 NodeBuilder::~NodeBuilder()
 {
-  if (CVC4_PREDICT_FALSE(nvIsAllocated()))
+  if (CVC5_PREDICT_FALSE(nvIsAllocated()))
   {
     dealloc();
   }
-  else if (CVC4_PREDICT_FALSE(!isUsed()))
+  else if (CVC5_PREDICT_FALSE(!isUsed()))
   {
     decrRefCounts();
   }
@@ -146,11 +146,11 @@ void NodeBuilder::clear(Kind k)
 {
   Assert(k != kind::NULL_EXPR) << "illegal Node-building clear kind";
 
-  if (CVC4_PREDICT_FALSE(nvIsAllocated()))
+  if (CVC5_PREDICT_FALSE(nvIsAllocated()))
   {
     dealloc();
   }
-  else if (CVC4_PREDICT_FALSE(!isUsed()))
+  else if (CVC5_PREDICT_FALSE(!isUsed()))
   {
     decrRefCounts();
   }
@@ -187,7 +187,7 @@ NodeBuilder& NodeBuilder::operator<<(const Kind& k)
   // NodeBuilder construction or at the last clear()), but we do
   // now.  That means we appended a Kind with operator<<(Kind),
   // which now (lazily) we'll collapse.
-  if (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+  if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
   {
     Node n2 = operator Node();
     clear();
@@ -209,7 +209,7 @@ NodeBuilder& NodeBuilder::operator<<(TNode n)
   // NodeBuilder construction or at the last clear()), but we do
   // now.  That means we appended a Kind with operator<<(Kind),
   // which now (lazily) we'll collapse.
-  if (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+  if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
   {
     Node n2 = operator Node();
     clear();
@@ -226,7 +226,7 @@ NodeBuilder& NodeBuilder::operator<<(TypeNode n)
   // NodeBuilder construction or at the last clear()), but we do
   // now.  That means we appended a Kind with operator<<(Kind),
   // which now (lazily) we'll collapse.
-  if (CVC4_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
+  if (CVC5_PREDICT_FALSE(d_nv->d_id == 0 && getKind() != kind::UNDEFINED_KIND))
   {
     Node n2 = operator Node();
     clear();
@@ -280,7 +280,7 @@ void NodeBuilder::realloc(size_t toSize)
       << "attempt to realloc() a NodeBuilder to size " << toSize
       << " (beyond hard limit of " << expr::NodeValue::MAX_CHILDREN << ")";
 
-  if (CVC4_PREDICT_FALSE(nvIsAllocated()))
+  if (CVC5_PREDICT_FALSE(nvIsAllocated()))
   {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
@@ -447,7 +447,7 @@ expr::NodeValue* NodeBuilder::constructNV()
   // NodeManager pool of Nodes.  See implementation notes at the top
   // of this file.
 
-  if (CVC4_PREDICT_TRUE(!nvIsAllocated()))
+  if (CVC5_PREDICT_TRUE(!nvIsAllocated()))
   {
     /** Case 1.  d_nv points to d_inlineNv: it is the backing store
      ** allocated "inline" in this NodeBuilder. **/
@@ -578,7 +578,7 @@ void NodeBuilder::internalCopy(const NodeBuilder& nb)
     return;
   }
 
-  bool realloced CVC4_UNUSED = false;
+  bool realloced CVC5_UNUSED = false;
   if (nb.d_nvMaxChildren > d_nvMaxChildren)
   {
     realloced = true;
@@ -603,7 +603,7 @@ void NodeBuilder::internalCopy(const NodeBuilder& nb)
   }
 }
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
 inline void NodeBuilder::maybeCheckType(const TNode n) const
 {
   /* force an immediate type check, if early type checking is
@@ -615,9 +615,9 @@ inline void NodeBuilder::maybeCheckType(const TNode n) const
     d_nm->getType(n, true);
   }
 }
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
-bool NodeBuilder::isUsed() const { return CVC4_PREDICT_FALSE(d_nv == nullptr); }
+bool NodeBuilder::isUsed() const { return CVC5_PREDICT_FALSE(d_nv == nullptr); }
 
 void NodeBuilder::setUsed()
 {
@@ -639,25 +639,25 @@ void NodeBuilder::setUnused()
 
 bool NodeBuilder::nvIsAllocated() const
 {
-  return CVC4_PREDICT_FALSE(d_nv != &d_inlineNv)
-         && CVC4_PREDICT_TRUE(d_nv != nullptr);
+  return CVC5_PREDICT_FALSE(d_nv != &d_inlineNv)
+         && CVC5_PREDICT_TRUE(d_nv != nullptr);
 }
 
 bool NodeBuilder::nvNeedsToBeAllocated() const
 {
-  return CVC4_PREDICT_FALSE(d_nv->d_nchildren == d_nvMaxChildren);
+  return CVC5_PREDICT_FALSE(d_nv->d_nchildren == d_nvMaxChildren);
 }
 
 void NodeBuilder::realloc()
 {
   size_t newSize = 2 * size_t(d_nvMaxChildren);
   size_t hardLimit = expr::NodeValue::MAX_CHILDREN;
-  realloc(CVC4_PREDICT_FALSE(newSize > hardLimit) ? hardLimit : newSize);
+  realloc(CVC5_PREDICT_FALSE(newSize > hardLimit) ? hardLimit : newSize);
 }
 
 void NodeBuilder::allocateNvIfNecessaryForAppend()
 {
-  if (CVC4_PREDICT_FALSE(nvNeedsToBeAllocated()))
+  if (CVC5_PREDICT_FALSE(nvNeedsToBeAllocated()))
   {
     realloc();
   }
@@ -665,8 +665,8 @@ void NodeBuilder::allocateNvIfNecessaryForAppend()
 
 void NodeBuilder::crop()
 {
-  if (CVC4_PREDICT_FALSE(nvIsAllocated())
-      && CVC4_PREDICT_TRUE(d_nvMaxChildren > d_nv->d_nchildren))
+  if (CVC5_PREDICT_FALSE(nvIsAllocated())
+      && CVC5_PREDICT_TRUE(d_nvMaxChildren > d_nv->d_nchildren))
   {
     // Ensure d_nv is not modified on allocation failure
     expr::NodeValue* newBlock = (expr::NodeValue*)std::realloc(
diff --git a/src/expr/node_builder.h b/src/expr/node_builder.h
index 271a217dc..95e91bb52 100644
--- a/src/expr/node_builder.h
+++ b/src/expr/node_builder.h
@@ -363,13 +363,13 @@ class NodeBuilder {
   /** Construct the node value out of the node builder */
   expr::NodeValue* constructNV();
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   // Throws a TypeCheckingExceptionPrivate on a failure.
   void maybeCheckType(const TNode n) const;
-#else  /* CVC4_DEBUG */
+#else  /* CVC5_DEBUG */
   // Do nothing if not in debug mode.
   inline void maybeCheckType(const TNode n) const {}
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
   // used by convenience node builders
   NodeBuilder& collapseTo(Kind k);
diff --git a/src/expr/node_manager.cpp b/src/expr/node_manager.cpp
index dd372a81d..072685e09 100644
--- a/src/expr/node_manager.cpp
+++ b/src/expr/node_manager.cpp
@@ -448,7 +448,7 @@ TypeNode NodeManager::getType(TNode n, bool check)
 
   Debug("getType") << this << " getting type for " << &n << " " << n << ", check=" << check << ", needsCheck = " << needsCheck << ", hasType = " << hasType << endl;
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
   // already did type check eagerly upon creation in node builder
   bool doTypeCheck = false;
 #else
@@ -664,10 +664,10 @@ std::vector<TypeNode> NodeManager::mkMutualDatatypeTypes(
     for (size_t i = 0, ncons = dt.getNumConstructors(); i < ncons; i++)
     {
       const DTypeConstructor& c = dt[i];
-      TypeNode testerType CVC4_UNUSED = c.getTester().getType();
+      TypeNode testerType CVC5_UNUSED = c.getTester().getType();
       Assert(c.isResolved() && testerType.isTester() && testerType[0] == ut)
           << "malformed tester in datatype post-resolution";
-      TypeNode ctorType CVC4_UNUSED = c.getConstructor().getType();
+      TypeNode ctorType CVC5_UNUSED = c.getConstructor().getType();
       Assert(ctorType.isConstructor()
             && ctorType.getNumChildren() == c.getNumArgs() + 1
             && ctorType.getRangeType() == ut)
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 3e1ccd67e..57eef062b 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -518,7 +518,7 @@ inline std::ostream& operator<<(std::ostream& out, const NodeValue& nv) {
 
 }  // namespace expr
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
  * outside of gdb.  This writes to the Warning() stream and immediately
@@ -542,7 +542,7 @@ static void __attribute__((used)) debugPrintRawNodeValue(const expr::NodeValue*
   nv->printAst(Warning(), 0);
   Warning().flush();
 }
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
 }  // namespace cvc5
 
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index 41f9afe6f..a1c4fa92b 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -1032,7 +1032,7 @@ inline unsigned TypeNode::getBitVectorSize() const {
   return getConst<BitVectorSize>();
 }
 
-#ifdef CVC4_DEBUG
+#ifdef CVC5_DEBUG
 /**
  * Pretty printer for use within gdb.  This is not intended to be used
  * outside of gdb.  This writes to the Warning() stream and immediately
@@ -1066,7 +1066,7 @@ static void __attribute__((used)) debugPrintRawTypeNode(const TypeNode& n) {
   n.printAst(Warning(), 0);
   Warning().flush();
 }
-#endif /* CVC4_DEBUG */
+#endif /* CVC5_DEBUG */
 
 }  // namespace cvc5