Rename namespace CVC4 to CVC5. (#6249)

14 files changed, 30 insertions, 30 deletions

diff --git a/src/theory/arith/nl/cad/cdcac.cpp b/src/theory/arith/nl/cad/cdcac.cpp
index c4ecfbbfa..7fd22fb76 100644
--- a/src/theory/arith/nl/cad/cdcac.cpp
+++ b/src/theory/arith/nl/cad/cdcac.cpp
@@ -29,12 +29,12 @@ namespace std {
 template <typename T>
 std::ostream& operator<<(std::ostream& os, const std::vector<T>& v)
 {
-  CVC4::container_to_stream(os, v);
+  CVC5::container_to_stream(os, v);
   return os;
 }
 }  // namespace std
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -545,6 +545,6 @@ void CDCAC::pruneRedundantIntervals(std::vector<CACInterval>& intervals)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/cdcac.h b/src/theory/arith/nl/cad/cdcac.h
index 15230d14c..2b607ae78 100644
--- a/src/theory/arith/nl/cad/cdcac.h
+++ b/src/theory/arith/nl/cad/cdcac.h
@@ -31,7 +31,7 @@
 #include "theory/arith/nl/cad/proof_generator.h"
 #include "theory/arith/nl/cad/variable_ordering.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -210,7 +210,7 @@ class CDCAC
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/cdcac_utils.cpp b/src/theory/arith/nl/cad/cdcac_utils.cpp
index 24bad8d60..f40d528ff 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.cpp
+++ b/src/theory/arith/nl/cad/cdcac_utils.cpp
@@ -20,7 +20,7 @@
 
 #include "theory/arith/nl/cad/projections.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -370,6 +370,6 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/cdcac_utils.h b/src/theory/arith/nl/cad/cdcac_utils.h
index dad9bbd7a..3b3a3638b 100644
--- a/src/theory/arith/nl/cad/cdcac_utils.h
+++ b/src/theory/arith/nl/cad/cdcac_utils.h
@@ -28,7 +28,7 @@
 #include "expr/node.h"
 #include "theory/arith/nl/cad/projections.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -105,7 +105,7 @@ void makeFinestSquareFreeBasis(CACInterval& lhs, CACInterval& rhs);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/constraints.cpp b/src/theory/arith/nl/cad/constraints.cpp
index 028a61833..1ea172d11 100644
--- a/src/theory/arith/nl/cad/constraints.cpp
+++ b/src/theory/arith/nl/cad/constraints.cpp
@@ -23,7 +23,7 @@
 #include "theory/arith/nl/poly_conversion.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -79,6 +79,6 @@ void Constraints::sortConstraints()
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/constraints.h b/src/theory/arith/nl/cad/constraints.h
index 42f8920c8..70c52e85c 100644
--- a/src/theory/arith/nl/cad/constraints.h
+++ b/src/theory/arith/nl/cad/constraints.h
@@ -28,7 +28,7 @@
 
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -87,7 +87,7 @@ class Constraints
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/projections.cpp b/src/theory/arith/nl/cad/projections.cpp
index 5d72f5a2e..b9e17f844 100644
--- a/src/theory/arith/nl/cad/projections.cpp
+++ b/src/theory/arith/nl/cad/projections.cpp
@@ -20,7 +20,7 @@
 
 #include "base/check.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -106,6 +106,6 @@ PolyVector projection_mccallum(const std::vector<Polynomial>& polys)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/projections.h b/src/theory/arith/nl/cad/projections.h
index 33267cb7a..3b8eb412f 100644
--- a/src/theory/arith/nl/cad/projections.h
+++ b/src/theory/arith/nl/cad/projections.h
@@ -25,7 +25,7 @@
 
 #include <vector>
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -76,7 +76,7 @@ PolyVector projectionMcCallum(const std::vector<poly::Polynomial>& polys);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 
diff --git a/src/theory/arith/nl/cad/proof_checker.cpp b/src/theory/arith/nl/cad/proof_checker.cpp
index 45c43e2aa..f1ab2d6a9 100644
--- a/src/theory/arith/nl/cad/proof_checker.cpp
+++ b/src/theory/arith/nl/cad/proof_checker.cpp
@@ -17,9 +17,9 @@
 #include "expr/sequence.h"
 #include "theory/rewriter.h"
 
-using namespace CVC4::kind;
+using namespace CVC5::kind;
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -58,4 +58,4 @@ Node CADProofRuleChecker::checkInternal(PfRule id,
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/src/theory/arith/nl/cad/proof_checker.h b/src/theory/arith/nl/cad/proof_checker.h
index 5ebe0c6b7..26bbcc3a9 100644
--- a/src/theory/arith/nl/cad/proof_checker.h
+++ b/src/theory/arith/nl/cad/proof_checker.h
@@ -20,7 +20,7 @@
 #include "expr/node.h"
 #include "expr/proof_checker.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -53,6 +53,6 @@ class CADProofRuleChecker : public ProofRuleChecker
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif /* CVC4__THEORY__STRINGS__PROOF_CHECKER_H */
diff --git a/src/theory/arith/nl/cad/proof_generator.cpp b/src/theory/arith/nl/cad/proof_generator.cpp
index 9f0799e7c..fe3734dce 100644
--- a/src/theory/arith/nl/cad/proof_generator.cpp
+++ b/src/theory/arith/nl/cad/proof_generator.cpp
@@ -19,7 +19,7 @@
 #include "theory/lazy_tree_proof_generator.h"
 #include "theory/arith/nl/poly_conversion.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -230,6 +230,6 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof)
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/proof_generator.h b/src/theory/arith/nl/cad/proof_generator.h
index 4709b8e59..c1bb4be1e 100644
--- a/src/theory/arith/nl/cad/proof_generator.h
+++ b/src/theory/arith/nl/cad/proof_generator.h
@@ -28,7 +28,7 @@
 #include "theory/arith/nl/cad/cdcac_utils.h"
 #include "theory/lazy_tree_proof_generator.h"
 
-namespace CVC4 {
+namespace CVC5 {
 
 class ProofGenerator;
 
@@ -144,7 +144,7 @@ std::ostream& operator<<(std::ostream& os, const CADProofGenerator& proof);
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
 #endif
diff --git a/src/theory/arith/nl/cad/variable_ordering.cpp b/src/theory/arith/nl/cad/variable_ordering.cpp
index 958191fe1..63db35553 100644
--- a/src/theory/arith/nl/cad/variable_ordering.cpp
+++ b/src/theory/arith/nl/cad/variable_ordering.cpp
@@ -20,7 +20,7 @@
 
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -132,6 +132,6 @@ std::vector<poly::Variable> VariableOrdering::operator()(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif
diff --git a/src/theory/arith/nl/cad/variable_ordering.h b/src/theory/arith/nl/cad/variable_ordering.h
index 43e85b3cb..7fda3faa4 100644
--- a/src/theory/arith/nl/cad/variable_ordering.h
+++ b/src/theory/arith/nl/cad/variable_ordering.h
@@ -26,7 +26,7 @@
 #include "theory/arith/nl/cad/constraints.h"
 #include "util/poly_util.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace theory {
 namespace arith {
 namespace nl {
@@ -65,7 +65,7 @@ std::vector<poly_utils::VariableInformation> collectInformation(
 }  // namespace nl
 }  // namespace arith
 }  // namespace theory
-}  // namespace CVC4
+}  // namespace CVC5
 
 #endif