Rename namespace CVC4 to CVC5. (#6249)

18 files changed, 70 insertions, 70 deletions

diff --git a/test/unit/util/array_store_all_white.cpp b/test/unit/util/array_store_all_white.cpp
index 540fca6f2..5be00263d 100644
--- a/test/unit/util/array_store_all_white.cpp
+++ b/test/unit/util/array_store_all_white.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::ArrayStoreAll
+ ** \brief Black box testing of CVC5::ArrayStoreAll
  **
- ** Black box testing of CVC4::ArrayStoreAll.
+ ** Black box testing of CVC5::ArrayStoreAll.
  **/
 
 #include "expr/array_store_all.h"
 #include "test_smt.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilWhiteArrayStoreAll : public TestSmt
@@ -75,4 +75,4 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error)
       IllegalArgumentException);
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index 0f1d5786e..a64bf275d 100644
--- a/test/unit/util/assert_white.cpp
+++ b/test/unit/util/assert_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC4::Configuration.
+ ** \brief White box testing of CVC5::Configuration.
  **
- ** White box testing of CVC4::Configuration.
+ ** White box testing of CVC5::Configuration.
  **/
 
 #include <cstring>
@@ -20,7 +20,7 @@
 #include "base/check.h"
 #include "test.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilWhite : public TestInternal
@@ -86,4 +86,4 @@ TEST_F(TestUtilWhite, CheckArgument)
   ASSERT_THROW(CheckArgument(false, "x"), IllegalArgumentException);
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index b35b8fa21..0b52b6d14 100644
--- a/test/unit/util/binary_heap_black.cpp
+++ b/test/unit/util/binary_heap_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::BinaryHeap
+ ** \brief Black box testing of CVC5::BinaryHeap
  **
- ** Black box testing of CVC4::BinaryHeap.
+ ** Black box testing of CVC5::BinaryHeap.
  **/
 
 #include <iostream>
@@ -20,7 +20,7 @@
 #include "test.h"
 #include "util/bin_heap.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackBinaryHeap : public TestInternal
@@ -230,4 +230,4 @@ TEST_F(TestUtilBlackBinaryHeap, large_heap)
   ASSERT_TRUE(heap.empty());
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index 3de70cfec..b26d8a1c6 100644
--- a/test/unit/util/bitvector_black.cpp
+++ b/test/unit/util/bitvector_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::BitVector
+ ** \brief Black box testing of CVC5::BitVector
  **
- ** Black box testing of CVC4::BitVector.
+ ** Black box testing of CVC5::BitVector.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/bitvector.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackBitVector : public TestInternal
@@ -203,4 +203,4 @@ TEST_F(TestUtilBlackBitVector, static_helpers)
   ASSERT_EQ(BitVector::mkMaxSigned(4).toSignedInteger(), Integer(7));
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index ef5ddadd6..cce2518c4 100644
--- a/test/unit/util/boolean_simplification_black.cpp
+++ b/test/unit/util/boolean_simplification_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::BooleanSimplification
+ ** \brief Black box testing of CVC5::BooleanSimplification
  **
- ** Black box testing of CVC4::BooleanSimplification.
+ ** Black box testing of CVC5::BooleanSimplification.
  **/
 
 #include <algorithm>
@@ -26,7 +26,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "test_node.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackBooleanSimplification : public TestNode
@@ -248,4 +248,4 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
 #endif
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index 9f5552037..b4b6ab6a5 100644
--- a/test/unit/util/cardinality_black.cpp
+++ b/test/unit/util/cardinality_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Public-box testing of CVC4::Cardinality
+ ** \brief Public-box testing of CVC5::Cardinality
  **
- ** Public-box testing of CVC4::Cardinality.
+ ** Public-box testing of CVC5::Cardinality.
  **/
 
 #include <sstream>
@@ -22,7 +22,7 @@
 #include "util/cardinality.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackCardinality : public TestInternal
@@ -270,4 +270,4 @@ TEST_F(TestUtilBlackCardinality, cardinalities)
   ASSERT_EQ((z ^ z).getBethNumber(), 3);
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 5ee0f42c4..4985bced3 100644
--- a/test/unit/util/check_white.cpp
+++ b/test/unit/util/check_white.cpp
@@ -20,7 +20,7 @@
 #include "base/check.h"
 #include "test.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilWhiteCheck : public TestInternal
@@ -63,4 +63,4 @@ TEST_F(TestUtilWhiteCheck, expect_abort)
   ASSERT_DEATH(AlwaysAssert(false), "false");
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index 44ae8c04b..a7c5c2703 100644
--- a/test/unit/util/configuration_black.cpp
+++ b/test/unit/util/configuration_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Configuration.
+ ** \brief Black box testing of CVC5::Configuration.
  **
- ** Black box testing of CVC4::Configuration.
+ ** Black box testing of CVC5::Configuration.
  **/
 
 #include "base/configuration.h"
 #include "test.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackConfiguration : public TestInternal
@@ -96,4 +96,4 @@ TEST_F(TestUtilBlackConfiguration, about)
   Configuration::about();
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index ef24d870d..b486d91e9 100644
--- a/test/unit/util/datatype_black.cpp
+++ b/test/unit/util/datatype_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::DType
+ ** \brief Black box testing of CVC5::DType
  **
- ** Black box testing of CVC4::DType.
+ ** Black box testing of CVC5::DType.
  **/
 
 #include <sstream>
@@ -21,7 +21,7 @@
 #include "expr/type_node.h"
 #include "test_smt.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackDatatype : public TestSmt
@@ -495,4 +495,4 @@ TEST_F(TestUtilBlackDatatype, parametric_DType)
   ASSERT_EQ(TypeNode::leastCommonTypeNode(pairIntInt, pairIntInt), pairIntInt);
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp
index d6ac7af67..7216c0b8c 100644
--- a/test/unit/util/exception_black.cpp
+++ b/test/unit/util/exception_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Exception.
+ ** \brief Black box testing of CVC5::Exception.
  **
- ** Black box testing of CVC4::Exception.
+ ** Black box testing of CVC5::Exception.
  **/
 
 #include <iostream>
@@ -20,14 +20,14 @@
 #include "base/exception.h"
 #include "test.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackException : public TestInternal
 {
 };
 
-// CVC4::Exception is a simple class, just test it all at once.
+// CVC5::Exception is a simple class, just test it all at once.
 TEST_F(TestUtilBlackException, exceptions)
 {
   Exception e1;
@@ -52,4 +52,4 @@ TEST_F(TestUtilBlackException, exceptions)
   ASSERT_EQ(s3.str(), std::string("three of 'em!"));
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp
index fd27268d1..391c656f3 100644
--- a/test/unit/util/floatingpoint_black.cpp
+++ b/test/unit/util/floatingpoint_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::FloatingPoint.
+ ** \brief Black box testing of CVC5::FloatingPoint.
  **
- ** Black box testing of CVC4::FloatingPoint.
+ ** Black box testing of CVC5::FloatingPoint.
  **/
 
 #include "test.h"
 #include "util/floatingpoint.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackFloatingPoint : public TestInternal
@@ -136,4 +136,4 @@ TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal)
   ASSERT_TRUE(mfp128.isNormal());
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index 29b971160..fc92fa0d2 100644
--- a/test/unit/util/integer_black.cpp
+++ b/test/unit/util/integer_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Integer.
+ ** \brief Black box testing of CVC5::Integer.
  **
- ** Black box testing of CVC4::Integer.
+ ** Black box testing of CVC5::Integer.
  **/
 
 #include <limits>
@@ -21,7 +21,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackInteger : public TestInternal
@@ -564,4 +564,4 @@ TEST_F(TestUtilBlackInteger, modInverse)
   }
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp
index 16e606d87..3b5363dda 100644
--- a/test/unit/util/integer_white.cpp
+++ b/test/unit/util/integer_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC4::Integer.
+ ** \brief White box testing of CVC5::Integer.
  **
- ** White box testing of CVC4::Integer.
+ ** White box testing of CVC5::Integer.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilWhiteInteger : public TestInternal
@@ -53,4 +53,4 @@ TEST_F(TestUtilWhiteInteger, construction)
   ASSERT_EQ(Integer(u), Integer(u));
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index 48b1d4087..f5c973849 100644
--- a/test/unit/util/output_black.cpp
+++ b/test/unit/util/output_black.cpp
@@ -20,7 +20,7 @@
 #include "base/output.h"
 #include "test.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackOutput : public TestInternal
@@ -241,4 +241,4 @@ TEST_F(TestUtilBlackOutput, simple_print)
 #endif /* CVC4_MUZZLE */
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp
index d3eaaf61e..e6dee5d55 100644
--- a/test/unit/util/rational_black.cpp
+++ b/test/unit/util/rational_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Rational.
+ ** \brief Black box testing of CVC5::Rational.
  **
- ** Black box testing of CVC4::Rational.
+ ** Black box testing of CVC5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackRational : public TestInternal
@@ -44,4 +44,4 @@ TEST_F(TestUtilBlackRational, fromDecimal)
   ASSERT_THROW(Rational::fromDecimal("Hello, world!");, std::invalid_argument);
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp
index df2dd1b17..542a43990 100644
--- a/test/unit/util/rational_white.cpp
+++ b/test/unit/util/rational_white.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief White box testing of CVC4::Rational.
+ ** \brief White box testing of CVC5::Rational.
  **
- ** White box testing of CVC4::Rational.
+ ** White box testing of CVC5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilWhiteRational : public TestInternal
@@ -416,4 +416,4 @@ TEST_F(TestUtilWhiteRational, constructrion)
   ASSERT_EQ(Rational(u), Rational(u));
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 97bbb438c..4300b709c 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -9,15 +9,15 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::RealAlgebraicNumber.
+ ** \brief Black box testing of CVC5::RealAlgebraicNumber.
  **
- ** Black box testing of CVC4::RealAlgebraicNumber.
+ ** Black box testing of CVC5::RealAlgebraicNumber.
  **/
 
 #include "test.h"
 #include "util/real_algebraic_number.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 #ifndef CVC4_POLY_IMP
@@ -81,4 +81,4 @@ TEST_F(TestUtilBlackRealAlgebraicNumber, arithmetic)
   ASSERT_EQ(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index 71cde7e5a..f8a14d9b2 100644
--- a/test/unit/util/stats_black.cpp
+++ b/test/unit/util/stats_black.cpp
@@ -9,9 +9,9 @@
  ** All rights reserved.  See the file COPYING in the top-level source
  ** directory for licensing information.\endverbatim
  **
- ** \brief Black box testing of CVC4::Stat and associated classes
+ ** \brief Black box testing of CVC5::Stat and associated classes
  **
- ** Black box testing of CVC4::Stat and associated classes.
+ ** Black box testing of CVC5::Stat and associated classes.
  **/
 
 #include <fcntl.h>
@@ -27,7 +27,7 @@
 #include "util/stats_histogram.h"
 #include "util/stats_timer.h"
 
-namespace CVC4 {
+namespace CVC5 {
 namespace test {
 
 class TestUtilBlackStats : public TestInternal
@@ -49,7 +49,7 @@ TEST_F(TestUtilBlackStats, stats)
   BackedStat<void*> backedAddr("backedDouble", (void*)0xDEADBEEF);
   IntegralHistogramStat<std::int64_t> histIntStat("hist-int");
   histIntStat << 15 << 16 << 15 << 14 << 16;
-  IntegralHistogramStat<CVC4::PfRule> histPfRuleStat("hist-pfrule");
+  IntegralHistogramStat<CVC5::PfRule> histPfRuleStat("hist-pfrule");
   histPfRuleStat << PfRule::ASSUME << PfRule::SCOPE << PfRule::ASSUME;
 
   // A statistic with no safe_print support
@@ -161,4 +161,4 @@ TEST_F(TestUtilBlackStats, stats)
 #endif
 }
 }  // namespace test
-}  // namespace CVC4
+}  // namespace CVC5