Rename namespace CVC4 to CVC5. (#6249)

11 files changed, 59 insertions, 59 deletions

diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index cf68e060c..48ceaf103 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -196,7 +196,7 @@
 #     is with your type checker:
 #
 #       cardinality MY_TYPE \
-#           ::CVC4::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
+#           ::CVC5::theory::foo::TheoryFoo::CardinalityComputer(%TYPE%) \
 #           "theory/foo/theory_foo_type_rules.h"
 #
 #   well-founded K wellfoundedness-computer ground-term-computer [header]
@@ -240,13 +240,13 @@
 # commands.
 #
 
-theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
+theory THEORY_BUILTIN ::CVC5::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
 typechecker "theory/builtin/theory_builtin_type_rules.h"
 
 properties stable-infinite
 
 # Rewriter responsible for all the terms of the theory
-rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
+rewriter ::CVC5::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
 
 sort BUILTIN_OPERATOR_TYPE \
     Cardinality::INTEGERS \
@@ -259,33 +259,33 @@ parameterized SORT_TYPE SORT_TAG 0: "specifies types of user-declared 'uninterpr
 # enough (for now) ?
 cardinality SORT_TYPE "Cardinality(Cardinality::INTEGERS)"
 well-founded SORT_TYPE \
-    "::CVC4::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
+    "::CVC5::theory::builtin::SortProperties::isWellFounded(%TYPE%)" \
+    "::CVC5::theory::builtin::SortProperties::mkGroundTerm(%TYPE%)"
 
 constant UNINTERPRETED_CONSTANT \
-    ::CVC4::UninterpretedConstant \
-    ::CVC4::UninterpretedConstantHashFunction \
+    ::CVC5::UninterpretedConstant \
+    ::CVC5::UninterpretedConstantHashFunction \
     "expr/uninterpreted_constant.h" \
-    "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC4::UninterpretedConstant class (used in models)"
-typerule UNINTERPRETED_CONSTANT ::CVC4::theory::builtin::UninterpretedConstantTypeRule
+    "the kind of expressions representing uninterpreted constants; payload is an instance of the CVC5::UninterpretedConstant class (used in models)"
+typerule UNINTERPRETED_CONSTANT ::CVC5::theory::builtin::UninterpretedConstantTypeRule
 enumerator SORT_TYPE \
-    ::CVC4::theory::builtin::UninterpretedSortEnumerator \
+    ::CVC5::theory::builtin::UninterpretedSortEnumerator \
     "theory/builtin/type_enumerator.h"
 
 constant ABSTRACT_VALUE \
-    ::CVC4::AbstractValue \
-    ::CVC4::AbstractValueHashFunction \
+    ::CVC5::AbstractValue \
+    ::CVC5::AbstractValueHashFunction \
     "util/abstract_value.h" \
-    "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC4::AbstractValue class (used in models)"
-typerule ABSTRACT_VALUE ::CVC4::theory::builtin::AbstractValueTypeRule
+    "the kind of expressions representing abstract values (other than uninterpreted sort constants); payload is an instance of the CVC5::AbstractValue class (used in models)"
+typerule ABSTRACT_VALUE ::CVC5::theory::builtin::AbstractValueTypeRule
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
 # not stored that way.  If you ask for the operator of (EQUAL a b),
 # you'll get a special, singleton (BUILTIN EQUAL) Node.
 constant BUILTIN \
-    ::CVC4::Kind \
-    ::CVC4::kind::KindHashFunction \
+    ::CVC5::Kind \
+    ::CVC5::kind::KindHashFunction \
     "expr/kind.h" \
     "the kind of expressions representing built-in operators"
 
@@ -301,33 +301,33 @@ operator LAMBDA 2 "a lambda expression; first parameter is a BOUND_VAR_LIST, sec
 operator WITNESS 2 "a witness expression; first parameter is a BOUND_VAR_LIST, second is the witness body"
 
 constant TYPE_CONSTANT \
-    ::CVC4::TypeConstant \
-    ::CVC4::TypeConstantHashFunction \
+    ::CVC5::TypeConstant \
+    ::CVC5::TypeConstantHashFunction \
     "expr/kind.h" \
     "a representation for basic types"
 operator FUNCTION_TYPE 2: "a function type"
 cardinality FUNCTION_TYPE \
-    "::CVC4::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
+    "::CVC5::theory::builtin::FunctionProperties::computeCardinality(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 well-founded FUNCTION_TYPE \
-    "::CVC4::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
-    "::CVC4::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
+    "::CVC5::theory::builtin::FunctionProperties::isWellFounded(%TYPE%)" \
+    "::CVC5::theory::builtin::FunctionProperties::mkGroundTerm(%TYPE%)" \
     "theory/builtin/theory_builtin_type_rules.h"
 enumerator FUNCTION_TYPE \
-    ::CVC4::theory::builtin::FunctionEnumerator \
+    ::CVC5::theory::builtin::FunctionEnumerator \
     "theory/builtin/type_enumerator.h"
 sort SEXPR_TYPE \
     Cardinality::INTEGERS \
     not-well-founded \
     "the type of a symbolic expression"
 
-typerule EQUAL ::CVC4::theory::builtin::EqualityTypeRule
-typerule DISTINCT ::CVC4::theory::builtin::DistinctTypeRule
-typerule SEXPR ::CVC4::theory::builtin::SExprTypeRule
-typerule LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
-typerule WITNESS ::CVC4::theory::builtin::WitnessTypeRule
+typerule EQUAL ::CVC5::theory::builtin::EqualityTypeRule
+typerule DISTINCT ::CVC5::theory::builtin::DistinctTypeRule
+typerule SEXPR ::CVC5::theory::builtin::SExprTypeRule
+typerule LAMBDA ::CVC5::theory::builtin::LambdaTypeRule
+typerule WITNESS ::CVC5::theory::builtin::WitnessTypeRule
 
 # lambda expressions that are isomorphic to array constants can be considered constants
-construle LAMBDA ::CVC4::theory::builtin::LambdaTypeRule
+construle LAMBDA ::CVC5::theory::builtin::LambdaTypeRule
 
 endtheory
diff --git a/src/theory/builtin/proof_checker.cpp b/src/theory/builtin/proof_checker.cpp
index 3e0eca128..62f0f1b9a 100644
--- a/src/theory/builtin/proof_checker.cpp
+++ b/src/theory/builtin/proof_checker.cpp
@@ -20,9 +20,9 @@
 #include "theory/rewriter.h"
 #include "theory/theory.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 
 const char* toString(MethodId id)
@@ -497,4 +497,4 @@ Node BuiltinProofRuleChecker::mkTheoryIdNode(TheoryId tid)
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/builtin/proof_checker.h b/src/theory/builtin/proof_checker.h
index 77cb2593a..ed68f1215 100644
--- a/src/theory/builtin/proof_checker.h
+++ b/src/theory/builtin/proof_checker.h
@@ -22,7 +22,7 @@
 #include "expr/proof_node.h"
 #include "theory/quantifiers/extended_rewrite.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 
 /**
@@ -179,6 +179,6 @@ class BuiltinProofRuleChecker : public ProofRuleChecker
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BUILTIN__PROOF_CHECKER_H */
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 13162960c..83e9d3fed 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -24,7 +24,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -62,4 +62,4 @@ void TheoryBuiltin::finishInit()
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 94a00b7e3..449282ae6 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -23,7 +23,7 @@
 #include "theory/builtin/theory_builtin_rewriter.h"
 #include "theory/theory.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -53,6 +53,6 @@ class TheoryBuiltin : public Theory
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_H */
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
index 16e454e04..16fc59a5a 100644
--- a/src/theory/builtin/theory_builtin_rewriter.cpp
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -23,7 +23,7 @@
 
 using namespace std;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -502,6 +502,6 @@ Node TheoryBuiltinRewriter::getArrayRepresentationForLambda(TNode n)
   return Rewriter::rewrite(anode);
 }
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
index bf84d543b..c419abdb3 100644
--- a/src/theory/builtin/theory_builtin_rewriter.h
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -22,7 +22,7 @@
 
 #include "theory/theory_rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -117,8 +117,8 @@ class TheoryBuiltinRewriter : public TheoryRewriter
   static Node getArrayRepresentationForLambda(TNode n);
 }; /* class TheoryBuiltinRewriter */
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_REWRITER_H */
diff --git a/src/theory/builtin/theory_builtin_type_rules.cpp b/src/theory/builtin/theory_builtin_type_rules.cpp
index 3abdbd48f..d5a5c9ab7 100644
--- a/src/theory/builtin/theory_builtin_type_rules.cpp
+++ b/src/theory/builtin/theory_builtin_type_rules.cpp
@@ -18,7 +18,7 @@
 
 #include "expr/attribute.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -47,4 +47,4 @@ Node SortProperties::mkGroundTerm(TypeNode type)
 
 }  // namespace builtin
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/builtin/theory_builtin_type_rules.h b/src/theory/builtin/theory_builtin_type_rules.h
index e0c68aa0f..815483507 100644
--- a/src/theory/builtin/theory_builtin_type_rules.h
+++ b/src/theory/builtin/theory_builtin_type_rules.h
@@ -25,7 +25,7 @@
 
 #include <sstream>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -246,8 +246,8 @@ class FunctionProperties {
   }
 };/* class FuctionProperties */
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BUILTIN__THEORY_BUILTIN_TYPE_RULES_H */
diff --git a/src/theory/builtin/type_enumerator.cpp b/src/theory/builtin/type_enumerator.cpp
index 6f7082191..4dda11070 100644
--- a/src/theory/builtin/type_enumerator.cpp
+++ b/src/theory/builtin/type_enumerator.cpp
@@ -18,7 +18,7 @@
 
 #include "theory/builtin/theory_builtin_rewriter.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -47,6 +47,6 @@ FunctionEnumerator& FunctionEnumerator::operator++()
   return *this;
 }
 
-} /* CVC4::theory::builtin namespace */
-} /* CVC4::theory namespace */
-} /* CVC4 namespace */
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC5
diff --git a/src/theory/builtin/type_enumerator.h b/src/theory/builtin/type_enumerator.h
index 7b4b09f84..50cd50dda 100644
--- a/src/theory/builtin/type_enumerator.h
+++ b/src/theory/builtin/type_enumerator.h
@@ -25,7 +25,7 @@
 #include "theory/type_enumerator.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace builtin {
 
@@ -104,8 +104,8 @@ class FunctionEnumerator : public TypeEnumeratorBase<FunctionEnumerator>
   Node d_bvl;
 }; /* class FunctionEnumerator */
 
-}/* CVC4::theory::builtin namespace */
-}/* CVC4::theory namespace */
-}/* CVC4 namespace */
+}  // namespace builtin
+}  // namespace theory
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__BUILTIN_TYPE_ENUMERATOR_H */