Rename occurrences of CVC4 to CVC5. (#6351)

This renames everything but GitHub links and build system related
macros. Switching the build system to cvc5 will be the last step in the
renaming process.

17 files changed, 30 insertions, 30 deletions

diff --git a/src/expr/attribute.cpp b/src/expr/attribute.cpp
index 1cb8adad6..ce617079e 100644
--- a/src/expr/attribute.cpp
+++ b/src/expr/attribute.cpp
@@ -36,7 +36,7 @@ bool AttributeManager::inGarbageCollection() const {
 void AttributeManager::debugHook(int debugFlag) {
   /* DO NOT CHECK IN ANY CODE INTO THE DEBUG HOOKS!
    * debugHook() is an empty function for the purpose of debugging
-   * the AttributeManager without recompiling all of CVC4.
+   * the AttributeManager without recompiling all of cvc5.
    * Formally this is a nop.
    */
 }
diff --git a/src/expr/attribute.h b/src/expr/attribute.h
index e42338bbb..b58cd45a9 100644
--- a/src/expr/attribute.h
+++ b/src/expr/attribute.h
@@ -211,7 +211,7 @@ public:
 
   /**
    * debugHook() is an empty function for the purpose of debugging
-   * the AttributeManager without recompiling all of CVC4.
+   * the AttributeManager without recompiling all of cvc5.
    * Formally this is a nop.
    */
   void debugHook(int debugFlag);
diff --git a/src/expr/dtype.cpp b/src/expr/dtype.cpp
index 66331f5c7..07b8aa5f1 100644
--- a/src/expr/dtype.cpp
+++ b/src/expr/dtype.cpp
@@ -895,8 +895,8 @@ const std::vector<std::shared_ptr<DTypeConstructor> >& DType::getConstructors()
 
 std::ostream& operator<<(std::ostream& os, const DType& dt)
 {
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+  // can only output datatypes in the cvc5 native language
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
   dt.toStream(os);
   return os;
 }
diff --git a/src/expr/dtype.h b/src/expr/dtype.h
index da16729cc..6fd334e02 100644
--- a/src/expr/dtype.h
+++ b/src/expr/dtype.h
@@ -90,7 +90,7 @@ class DTypeConstructor;
  * allow the datatype to construct the necessary testers and selectors.
  *
  * An additional point to make is that we want to ease the burden on
- * both the parser AND the users of the CVC4 API, so this class takes
+ * both the parser AND the users of the cvc5 API, so this class takes
  * on the task of generating its own selectors and testers, for
  * instance.  That means that, after reifying the DType with the
  * NodeManager, the parser needs to go through the (now-resolved)
diff --git a/src/expr/dtype_cons.cpp b/src/expr/dtype_cons.cpp
index 8d6194b06..99e5ad8ac 100644
--- a/src/expr/dtype_cons.cpp
+++ b/src/expr/dtype_cons.cpp
@@ -678,8 +678,8 @@ void DTypeConstructor::toStream(std::ostream& out) const
 
 std::ostream& operator<<(std::ostream& os, const DTypeConstructor& ctor)
 {
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+  // can only output datatypes in the cvc5 native language
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
   ctor.toStream(os);
   return os;
 }
diff --git a/src/expr/dtype_selector.cpp b/src/expr/dtype_selector.cpp
index d6a3923df..98a07b2c9 100644
--- a/src/expr/dtype_selector.cpp
+++ b/src/expr/dtype_selector.cpp
@@ -78,8 +78,8 @@ void DTypeSelector::toStream(std::ostream& out) const
 
 std::ostream& operator<<(std::ostream& os, const DTypeSelector& arg)
 {
-  // can only output datatypes in the CVC4 native language
-  language::SetLanguage::Scope ls(os, language::output::LANG_CVC4);
+  // can only output datatypes in the cvc5 native language
+  language::SetLanguage::Scope ls(os, language::output::LANG_CVC);
   arg.toStream(os);
   return os;
 }
diff --git a/src/expr/kind_template.h b/src/expr/kind_template.h
index 5fa1d99ff..6e2362e84 100644
--- a/src/expr/kind_template.h
+++ b/src/expr/kind_template.h
@@ -36,7 +36,7 @@ enum Kind_t
 
 }  // namespace kind
 
-// import Kind into the "CVC4" namespace but keep the individual kind
+// import Kind into the "cvc5" namespace but keep the individual kind
 // constants under kind::
 typedef ::cvc5::kind::Kind_t Kind;
 
diff --git a/src/expr/metakind_template.h b/src/expr/metakind_template.h
index 0747b97fa..1271c2e64 100644
--- a/src/expr/metakind_template.h
+++ b/src/expr/metakind_template.h
@@ -33,7 +33,7 @@ namespace kind {
 namespace metakind {
 
 /**
- * Static, compile-time information about types T representing CVC4
+ * Static, compile-time information about types T representing cvc5
  * constants:
  *
  *   typename ConstantMap<T>::OwningTheory
@@ -51,7 +51,7 @@ struct ConstantMap;
 
 /**
  * Static, compile-time information about kinds k and what type their
- * corresponding CVC4 constants are:
+ * corresponding cvc5 constants are:
  *
  *   typename ConstantMapReverse<k>::T
  *
diff --git a/src/expr/mkexpr b/src/expr/mkexpr
index 0be51c71c..64a99d406 100755
--- a/src/expr/mkexpr
+++ b/src/expr/mkexpr
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
 # mkexpr
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2013  The CVC4 Project
+# Morgan Deters <mdeters@cs.nyu.edu> for cvc5
+# Copyright (c) 2010-2013  The cvc5 Project
 #
 # The purpose of this script is to create {expr,expr_manager}.{h,cpp}
 # from template files and a list of theory kinds.  Basically it just
diff --git a/src/expr/mkkind b/src/expr/mkkind
index 53e63af6e..117b3bb9e 100755
--- a/src/expr/mkkind
+++ b/src/expr/mkkind
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
 # mkkind
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2013  The CVC4 Project
+# Morgan Deters <mdeters@cs.nyu.edu> for cvc5
+# Copyright (c) 2010-2013  The cvc5 Project
 #
 # The purpose of this script is to create kind.h (and also
 # type_properties.h) from a template and a list of theory kinds.
diff --git a/src/expr/mkmetakind b/src/expr/mkmetakind
index 52fe070e6..a5801b9fe 100755
--- a/src/expr/mkmetakind
+++ b/src/expr/mkmetakind
@@ -1,8 +1,8 @@
 #!/usr/bin/env bash
 #
 # mkmetakind
-# Morgan Deters <mdeters@cs.nyu.edu> for CVC4
-# Copyright (c) 2010-2013  The CVC4 Project
+# Morgan Deters <mdeters@cs.nyu.edu> for cvc5
+# Copyright (c) 2010-2013  The cvc5 Project
 #
 # The purpose of this script is to create metakind.h from a template
 # and a list of theory kinds.
diff --git a/src/expr/node.h b/src/expr/node.h
index 181fc2e52..9014016b9 100644
--- a/src/expr/node.h
+++ b/src/expr/node.h
@@ -124,7 +124,7 @@ typedef NodeTemplate<true> Node;
  * creation.  If this is returned as a TNode rather than a Node, the
  * count drops to zero, marking the expression as eligible for reclamation.)
  *
- * More guidelines on when to use TNodes is available in the CVC4
+ * More guidelines on when to use TNodes is available in the cvc5
  * Developer's Guide:
  * http://cvc4.cs.stanford.edu/wiki/Developer%27s_Guide#Dealing_with_expressions_.28Nodes_and_TNodes.29
  */
@@ -395,7 +395,7 @@ public:
    * these functions, as they may only be needed in CNF conversion,
    * where it's pointless to do a lazy isAtomic determination by
    * searching through the DAG, and storing it, since the result will
-   * only be used once.  For more details see the 4/27/2010 CVC4
+   * only be used once.  For more details see the 4/27/2010 cvc5
    * developer's meeting notes at:
    *
    * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
diff --git a/src/expr/node_manager.h b/src/expr/node_manager.h
index 5ca6823d9..528cdcfc7 100644
--- a/src/expr/node_manager.h
+++ b/src/expr/node_manager.h
@@ -344,7 +344,7 @@ class NodeManager
    * these functions, as they may only be needed in CNF conversion,
    * where it's pointless to do a lazy isAtomic determination by
    * searching through the DAG, and storing it, since the result will
-   * only be used once.  For more details see the 4/27/2010 CVC4
+   * only be used once.  For more details see the 4/27/2010 cvc5
    * developer's meeting notes at:
    *
    * http://cvc4.cs.stanford.edu/wiki/Meeting_Minutes_-_April_27,_2010#isAtomic.28.29_and_isAtomicFormula.28.29
@@ -364,7 +364,7 @@ class NodeManager
    * lookup is done on the name.  If you mkVar("a", type) and then
    * mkVar("a", type) again, you have two variables.  The NodeManager
    * version of this is private to avoid internal uses of mkVar() from
-   * within CVC4.  Such uses should employ SkolemManager::mkSkolem() instead.
+   * within cvc5.  Such uses should employ SkolemManager::mkSkolem() instead.
    */
   Node mkVar(const std::string& name, const TypeNode& type);
   Node* mkVarPtr(const std::string& name, const TypeNode& type);
@@ -390,7 +390,7 @@ class NodeManager
   explicit NodeManager();
   ~NodeManager();
 
-  /** The node manager in the current public-facing CVC4 library context */
+  /** The node manager in the current public-facing cvc5 library context */
   static NodeManager* currentNM() { return s_current; }
   /** Get this node manager's skolem manager */
   SkolemManager* getSkolemManager() { return d_skManager.get(); }
@@ -1093,7 +1093,7 @@ class NodeManager
  * previous thread-global <code>NodeManager</code> when it is
  * destroyed, effectively maintaining a set of nested
  * <code>NodeManager</code> scopes.  This is especially useful on
- * public-interface calls into the CVC4 library, where CVC4's notion
+ * public-interface calls into the cvc5 library, where cvc5's notion
  * of the "current" <code>NodeManager</code> should be set to match
  * the calling context.  See, for example, the implementations of
  * public calls in the <code>SmtEngine</code> class.
diff --git a/src/expr/node_value.h b/src/expr/node_value.h
index 3aa927bdb..c45fadb5c 100644
--- a/src/expr/node_value.h
+++ b/src/expr/node_value.h
@@ -426,7 +426,7 @@ inline void NodeValue::inc() {
     ++d_rc;
     Assert(NodeManager::currentNM() != NULL)
         << "No current NodeManager on incrementing of NodeValue: "
-           "maybe a public CVC4 interface function is missing a "
+           "maybe a public cvc5 interface function is missing a "
            "NodeManagerScope ?";
     NodeManager::currentNM()->markRefCountMaxedOut(this);
   }
@@ -439,7 +439,7 @@ inline void NodeValue::dec() {
     if(__builtin_expect( ( d_rc == 0 ), false )) {
       Assert(NodeManager::currentNM() != NULL)
           << "No current NodeManager on destruction of NodeValue: "
-             "maybe a public CVC4 interface function is missing a "
+             "maybe a public cvc5 interface function is missing a "
              "NodeManagerScope ?";
       NodeManager::currentNM()->markForDeletion(this);
     }
diff --git a/src/expr/proof_node.h b/src/expr/proof_node.h
index 08d2a0245..f8d71f703 100644
--- a/src/expr/proof_node.h
+++ b/src/expr/proof_node.h
@@ -80,8 +80,8 @@ struct ProofNodeHashFunction
  * An external proof checker is expected to formalize the ProofNode only in
  * terms of *witness* forms.
  *
- * However, the rest of CVC4 sees only the *Skolem* form of arguments and
- * conclusions in ProofNode, since this is what is used throughout CVC4.
+ * However, the rest of cvc5 sees only the *Skolem* form of arguments and
+ * conclusions in ProofNode, since this is what is used throughout cvc5.
  */
 class ProofNode
 {
diff --git a/src/expr/sequence.h b/src/expr/sequence.h
index 40cadb858..8bf7abeea 100644
--- a/src/expr/sequence.h
+++ b/src/expr/sequence.h
@@ -28,7 +28,7 @@ class NodeTemplate;
 typedef NodeTemplate<true> Node;
 class TypeNode;
 
-/** The CVC4 sequence class
+/** The cvc5 sequence class
  *
  * This data structure is the domain of values for the sequence type.
  */
diff --git a/src/expr/type_node.h b/src/expr/type_node.h
index d1b5edf22..318d59613 100644
--- a/src/expr/type_node.h
+++ b/src/expr/type_node.h
@@ -420,7 +420,7 @@ public:
   /** is closed enumerable type
    *
    * This returns true if this type has an enumerator that produces constants
-   * that are fully handled by CVC4's quantifier-free theory solvers. Examples
+   * that are fully handled by cvc5's quantifier-free theory solvers. Examples
    * of types that are not closed enumerable are:
    * (1) uninterpreted sorts,
    * (2) arrays,