Rename namespace CVC5 to cvc5. (#6258)

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 5be00263d..b82807835 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 CVC5::ArrayStoreAll
+ ** \brief Black box testing of cvc5::ArrayStoreAll
  **
- ** Black box testing of CVC5::ArrayStoreAll.
+ ** Black box testing of cvc5::ArrayStoreAll.
  **/
 
 #include "expr/array_store_all.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilWhiteArrayStoreAll : public TestSmt
@@ -75,4 +75,4 @@ TEST_F(TestUtilWhiteArrayStoreAll, const_error)
       IllegalArgumentException);
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/assert_white.cpp b/test/unit/util/assert_white.cpp
index a64bf275d..bab612b62 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 CVC5::Configuration.
+ ** \brief White box testing of cvc5::Configuration.
  **
- ** White box testing of CVC5::Configuration.
+ ** White box testing of cvc5::Configuration.
  **/
 
 #include <cstring>
@@ -20,7 +20,7 @@
 #include "base/check.h"
 #include "test.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/binary_heap_black.cpp b/test/unit/util/binary_heap_black.cpp
index 0b52b6d14..c00aeaeb2 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 CVC5::BinaryHeap
+ ** \brief Black box testing of cvc5::BinaryHeap
  **
- ** Black box testing of CVC5::BinaryHeap.
+ ** Black box testing of cvc5::BinaryHeap.
  **/
 
 #include <iostream>
@@ -20,7 +20,7 @@
 #include "test.h"
 #include "util/bin_heap.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackBinaryHeap : public TestInternal
@@ -230,4 +230,4 @@ TEST_F(TestUtilBlackBinaryHeap, large_heap)
   ASSERT_TRUE(heap.empty());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/bitvector_black.cpp b/test/unit/util/bitvector_black.cpp
index b26d8a1c6..61dfa8101 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 CVC5::BitVector
+ ** \brief Black box testing of cvc5::BitVector
  **
- ** Black box testing of CVC5::BitVector.
+ ** Black box testing of cvc5::BitVector.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/bitvector.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/boolean_simplification_black.cpp b/test/unit/util/boolean_simplification_black.cpp
index cce2518c4..baacbce5a 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 CVC5::BooleanSimplification
+ ** \brief Black box testing of cvc5::BooleanSimplification
  **
- ** Black box testing of CVC5::BooleanSimplification.
+ ** Black box testing of cvc5::BooleanSimplification.
  **/
 
 #include <algorithm>
@@ -26,7 +26,7 @@
 #include "smt_util/boolean_simplification.h"
 #include "test_node.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackBooleanSimplification : public TestNode
@@ -248,4 +248,4 @@ TEST_F(TestUtilBlackBooleanSimplification, simplifyConflict)
 #endif
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/cardinality_black.cpp b/test/unit/util/cardinality_black.cpp
index b4b6ab6a5..f4b2f3ac4 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 CVC5::Cardinality
+ ** \brief Public-box testing of cvc5::Cardinality
  **
- ** Public-box testing of CVC5::Cardinality.
+ ** Public-box testing of cvc5::Cardinality.
  **/
 
 #include <sstream>
@@ -22,7 +22,7 @@
 #include "util/cardinality.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/check_white.cpp b/test/unit/util/check_white.cpp
index 4985bced3..4909e3a58 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 CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/configuration_black.cpp b/test/unit/util/configuration_black.cpp
index a7c5c2703..35bfd4d78 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 CVC5::Configuration.
+ ** \brief Black box testing of cvc5::Configuration.
  **
- ** Black box testing of CVC5::Configuration.
+ ** Black box testing of cvc5::Configuration.
  **/
 
 #include "base/configuration.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackConfiguration : public TestInternal
@@ -96,4 +96,4 @@ TEST_F(TestUtilBlackConfiguration, about)
   Configuration::about();
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/datatype_black.cpp b/test/unit/util/datatype_black.cpp
index b486d91e9..37cfe0cfa 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 CVC5::DType
+ ** \brief Black box testing of cvc5::DType
  **
- ** Black box testing of CVC5::DType.
+ ** Black box testing of cvc5::DType.
  **/
 
 #include <sstream>
@@ -21,7 +21,7 @@
 #include "expr/type_node.h"
 #include "test_smt.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/exception_black.cpp b/test/unit/util/exception_black.cpp
index 7216c0b8c..2884dbfb8 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 CVC5::Exception.
+ ** \brief Black box testing of cvc5::Exception.
  **
- ** Black box testing of CVC5::Exception.
+ ** Black box testing of cvc5::Exception.
  **/
 
 #include <iostream>
@@ -20,14 +20,14 @@
 #include "base/exception.h"
 #include "test.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackException : public TestInternal
 {
 };
 
-// CVC5::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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/floatingpoint_black.cpp b/test/unit/util/floatingpoint_black.cpp
index 391c656f3..0fe48928f 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 CVC5::FloatingPoint.
+ ** \brief Black box testing of cvc5::FloatingPoint.
  **
- ** Black box testing of CVC5::FloatingPoint.
+ ** Black box testing of cvc5::FloatingPoint.
  **/
 
 #include "test.h"
 #include "util/floatingpoint.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackFloatingPoint : public TestInternal
@@ -136,4 +136,4 @@ TEST_F(TestUtilBlackFloatingPoint, makeMaxNormal)
   ASSERT_TRUE(mfp128.isNormal());
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/integer_black.cpp b/test/unit/util/integer_black.cpp
index fc92fa0d2..1a3e75256 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 CVC5::Integer.
+ ** \brief Black box testing of cvc5::Integer.
  **
- ** Black box testing of CVC5::Integer.
+ ** Black box testing of cvc5::Integer.
  **/
 
 #include <limits>
@@ -21,7 +21,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackInteger : public TestInternal
@@ -564,4 +564,4 @@ TEST_F(TestUtilBlackInteger, modInverse)
   }
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/integer_white.cpp b/test/unit/util/integer_white.cpp
index 3b5363dda..117f82195 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 CVC5::Integer.
+ ** \brief White box testing of cvc5::Integer.
  **
- ** White box testing of CVC5::Integer.
+ ** White box testing of cvc5::Integer.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/integer.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/output_black.cpp b/test/unit/util/output_black.cpp
index f5c973849..e951dd114 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 CVC5 {
+namespace cvc5 {
 namespace test {
 
 class TestUtilBlackOutput : public TestInternal
@@ -241,4 +241,4 @@ TEST_F(TestUtilBlackOutput, simple_print)
 #endif /* CVC4_MUZZLE */
 }
 }  // namespace test
-}  // namespace CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/rational_black.cpp b/test/unit/util/rational_black.cpp
index e6dee5d55..d3b116d26 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 CVC5::Rational.
+ ** \brief Black box testing of cvc5::Rational.
  **
- ** Black box testing of CVC5::Rational.
+ ** Black box testing of cvc5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/rational_white.cpp b/test/unit/util/rational_white.cpp
index 542a43990..c5b52e3c8 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 CVC5::Rational.
+ ** \brief White box testing of cvc5::Rational.
  **
- ** White box testing of CVC5::Rational.
+ ** White box testing of cvc5::Rational.
  **/
 
 #include <sstream>
@@ -19,7 +19,7 @@
 #include "test.h"
 #include "util/rational.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 4300b709c..507be5ea0 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 CVC5::RealAlgebraicNumber.
+ ** \brief Black box testing of cvc5::RealAlgebraicNumber.
  **
- ** Black box testing of CVC5::RealAlgebraicNumber.
+ ** Black box testing of cvc5::RealAlgebraicNumber.
  **/
 
 #include "test.h"
 #include "util/real_algebraic_number.h"
 
-namespace CVC5 {
+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 CVC5
+}  // namespace cvc5
diff --git a/test/unit/util/stats_black.cpp b/test/unit/util/stats_black.cpp
index f8a14d9b2..2ee64ab33 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 CVC5::Stat and associated classes
+ ** \brief Black box testing of cvc5::Stat and associated classes
  **
- ** Black box testing of CVC5::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 CVC5 {
+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<CVC5::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 CVC5
+}  // namespace cvc5