diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-04-01 09:56:14 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-04-01 16:56:14 +0000 |
commit | 05a53a2ac405bcd18a84024247145f161809c3b0 (patch) | |
tree | 34241c0a82f79d717ddbfbb0c294f9a09c7edb0c /test/unit/util | |
parent | afaf4413775ff7d6054a5893f1397ad908e0773c (diff) |
Rename namespace CVC5 to cvc5. (#6258)
Diffstat (limited to 'test/unit/util')
-rw-r--r-- | test/unit/util/array_store_all_white.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/assert_white.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/binary_heap_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/bitvector_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/boolean_simplification_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/cardinality_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/check_white.cpp | 4 | ||||
-rw-r--r-- | test/unit/util/configuration_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/datatype_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/exception_black.cpp | 10 | ||||
-rw-r--r-- | test/unit/util/floatingpoint_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/integer_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/integer_white.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/output_black.cpp | 4 | ||||
-rw-r--r-- | test/unit/util/rational_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/rational_white.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/real_algebraic_number_black.cpp | 8 | ||||
-rw-r--r-- | test/unit/util/stats_black.cpp | 10 |
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 |