diff options
author | Aina Niemetz <aina.niemetz@gmail.com> | 2021-03-31 15:23:17 -0700 |
---|---|---|
committer | GitHub <noreply@github.com> | 2021-03-31 22:23:17 +0000 |
commit | a1466978fbc328507406d4a121dab4d1a1047e1d (patch) | |
tree | 12b40f161bb4d7a6ee40c20c78a15d6cda3c1995 /src/util | |
parent | f9a9af855fb65804ff0b36e764ccd9d0fa9f87f8 (diff) |
Rename namespace CVC4 to CVC5. (#6249)
Diffstat (limited to 'src/util')
72 files changed, 204 insertions, 200 deletions
diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 2c82b98e9..4f6cadde4 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { std::ostream& operator<<(std::ostream& out, const AbstractValue& val) { return out << "@" << val.getIndex(); @@ -38,4 +38,4 @@ AbstractValue::AbstractValue(Integer index) : d_index(index) index.toString().c_str()); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index 5d28d355a..ddd1018a2 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -22,7 +22,7 @@ #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { class AbstractValue { @@ -61,4 +61,4 @@ struct AbstractValueHashFunction } }; /* struct AbstractValueHashFunction */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index c51600122..40f2da045 100644 --- a/src/util/bin_heap.h +++ b/src/util/bin_heap.h @@ -29,7 +29,7 @@ #include "base/check.h" #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { /** * BinaryHeap that orders its elements greatest-first (i.e., in the opposite @@ -363,6 +363,6 @@ private: template <class Elem, class CmpFcn> const size_t BinaryHeap<Elem,CmpFcn>::MAX_SIZE = (std::numeric_limits<size_t>::max()-2)/2; -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__BIN_HEAP_H */ diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 3d907150d..85b373886 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -20,7 +20,7 @@ #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { unsigned BitVector::getSize() const { return d_size; } @@ -375,4 +375,4 @@ BitVector BitVector::mkMaxSigned(unsigned size) return ~BitVector::mkMinSigned(size); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/bitvector.h b/src/util/bitvector.h index c5a690c03..fbb91b8e3 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -25,7 +25,7 @@ #include "base/exception.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { class BitVector { @@ -442,6 +442,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv) return os << "[" << bv.d_size << "]"; } -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__BITVECTOR_H */ diff --git a/src/util/bool.h b/src/util/bool.h index 0dd179d6a..d1f57fcd4 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -19,7 +19,7 @@ #ifndef CVC4__BOOL_H #define CVC4__BOOL_H -namespace CVC4 { +namespace CVC5 { struct BoolHashFunction { inline size_t operator()(bool b) const { @@ -27,6 +27,6 @@ struct BoolHashFunction { } };/* struct BoolHashFunction */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__BOOL_H */ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 3ab44d6f8..027c3d2db 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -22,7 +22,7 @@ #include "base/check.h" #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { const Integer Cardinality::s_unknownCard(0); const Integer Cardinality::s_intCard(-1); @@ -263,4 +263,4 @@ std::ostream& operator<<(std::ostream& out, const Cardinality& c) { return out; } -} /* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 6c48b44a8..2ab2fdd63 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -24,7 +24,7 @@ #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { /** * Representation for a Beth number, used only to construct @@ -225,6 +225,6 @@ std::ostream& operator<<(std::ostream& out, CardinalityBeth b); /** Print a cardinality in a human-readable fashion. */ std::ostream& operator<<(std::ostream& out, const Cardinality& c); -} /* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__CARDINALITY_H */ diff --git a/src/util/dense_map.h b/src/util/dense_map.h index 7a3421281..e6fed6916 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -35,8 +35,7 @@ #include "base/check.h" #include "util/index.h" - -namespace CVC4 { +namespace CVC5 { template <class T> class DenseMap { @@ -339,4 +338,4 @@ public: void pop_back() { d_map.pop_back(); } }; /* class DenseMultiset */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index b3c823e06..45b1f6c27 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -22,10 +22,10 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { Divisible::Divisible(const Integer& n) : k(n) { PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/divisible.h b/src/util/divisible.h index 2de81c52b..5b3506ee8 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -26,7 +26,7 @@ #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { /** * The structure representing the divisibility-by-k predicate. @@ -61,6 +61,6 @@ inline std::ostream& operator <<(std::ostream& os, const Divisible& d) { return os << "divisible-by-" << d.k; } -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__DIVISIBLE_H */ diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index 26bdb65f4..be5f6a496 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -28,7 +28,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC4 { +namespace CVC5 { /* -------------------------------------------------------------------------- */ @@ -512,4 +512,4 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs) return os << "(_ to_fp " << fpcs.getSize().exponentWidth() << " " << fpcs.getSize().significandWidth() << ")"; } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index b6c1bfb53..060d1de99 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -29,7 +29,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC4 { +namespace CVC5 { /* -------------------------------------------------------------------------- */ @@ -514,7 +514,7 @@ struct FloatingPointToBVHashFunction { inline size_t operator()(const FloatingPointToBV& fptbv) const { - UnsignedHashFunction< ::CVC4::BitVectorSize> f; + UnsignedHashFunction< ::CVC5::BitVectorSize> f; return (key ^ 0x46504256) ^ f(fptbv.d_bv_size); } }; /* struct FloatingPointToBVHashFunction */ @@ -533,6 +533,6 @@ std::ostream& operator<<(std::ostream& os, const FloatingPointSize& fps); std::ostream& operator<<(std::ostream& os, const FloatingPointConvertSort& fpcs); -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__FLOATINGPOINT_H */ diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index 1d40292f7..efd3e2399 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -39,9 +39,9 @@ namespace symfpu { #define CVC4_LIT_ITE_DFN(T) \ template <> \ - struct ite<::CVC4::symfpuLiteral::CVC4Prop, T> \ + struct ite<::CVC5::symfpuLiteral::CVC4Prop, T> \ { \ - static const T& iteOp(const ::CVC4::symfpuLiteral::CVC4Prop& cond, \ + static const T& iteOp(const ::CVC5::symfpuLiteral::CVC4Prop& cond, \ const T& l, \ const T& r) \ { \ @@ -49,10 +49,10 @@ namespace symfpu { } \ } -CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::rm); -CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::prop); -CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::sbv); -CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); +CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::rm); +CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::prop); +CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::sbv); +CVC4_LIT_ITE_DFN(::CVC5::symfpuLiteral::traits::ubv); #undef CVC4_LIT_ITE_DFN } // namespace symfpu @@ -60,7 +60,7 @@ CVC4_LIT_ITE_DFN(::CVC4::symfpuLiteral::traits::ubv); /* -------------------------------------------------------------------------- */ -namespace CVC4 { +namespace CVC5 { uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) { @@ -881,11 +881,11 @@ wrappedBitVector<isSigned> wrappedBitVector<isSigned>::extract( template class wrappedBitVector<true>; template class wrappedBitVector<false>; -traits::rm traits::RNE(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_EVEN; }; -traits::rm traits::RNA(void) { return ::CVC4::ROUND_NEAREST_TIES_TO_AWAY; }; -traits::rm traits::RTP(void) { return ::CVC4::ROUND_TOWARD_POSITIVE; }; -traits::rm traits::RTN(void) { return ::CVC4::ROUND_TOWARD_NEGATIVE; }; -traits::rm traits::RTZ(void) { return ::CVC4::ROUND_TOWARD_ZERO; }; +traits::rm traits::RNE(void) { return ::CVC5::ROUND_NEAREST_TIES_TO_EVEN; }; +traits::rm traits::RNA(void) { return ::CVC5::ROUND_NEAREST_TIES_TO_AWAY; }; +traits::rm traits::RTP(void) { return ::CVC5::ROUND_TOWARD_POSITIVE; }; +traits::rm traits::RTN(void) { return ::CVC5::ROUND_TOWARD_NEGATIVE; }; +traits::rm traits::RTZ(void) { return ::CVC5::ROUND_TOWARD_ZERO; }; // This is a literal back-end so props are actually bools // so these can be handled in the same way as the internal assertions above @@ -906,4 +906,4 @@ void traits::invariant(const traits::prop& p) } } // namespace symfpuLiteral -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index 8857728ce..d01bf6a9d 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -30,7 +30,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC4 { +namespace CVC5 { class FloatingPointSize; class FloatingPointLiteral; @@ -56,8 +56,8 @@ class wrappedBitVector; using CVC4BitWidth = uint32_t; using CVC4Prop = bool; -using CVC4RM = ::CVC4::RoundingMode; -using CVC4FPSize = ::CVC4::FloatingPointSize; +using CVC4RM = ::CVC5::RoundingMode; +using CVC4FPSize = ::CVC5::FloatingPointSize; using CVC4UnsignedBitVector = wrappedBitVector<false>; using CVC4SignedBitVector = wrappedBitVector<true>; @@ -106,7 +106,7 @@ struct signedToLiteralType<false> }; /** - * This extends the interface for CVC4::BitVector for compatibility with symFPU. + * This extends the interface for CVC5::BitVector for compatibility with symFPU. * The template parameter distinguishes signed and unsigned bit-vectors, a * distinction symfpu uses. */ @@ -159,7 +159,7 @@ class wrappedBitVector : public BitVector /** * Inherited but ... * *sigh* if we use the inherited version then it will return a - * CVC4::BitVector which can be converted back to a + * CVC5::BitVector which can be converted back to a * wrappedBitVector<isSigned> but isn't done automatically when working * out types for templates instantiation. ITE is a particular * problem as expressions and constants no longer derive the @@ -502,6 +502,6 @@ class FloatingPointLiteral /* -------------------------------------------------------------------------- */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp index 9b14db699..78558ab27 100644 --- a/src/util/floatingpoint_size.cpp +++ b/src/util/floatingpoint_size.cpp @@ -15,7 +15,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { FloatingPointSize::FloatingPointSize(uint32_t exp_size, uint32_t sig_size) : d_exp_size(exp_size), d_sig_size(sig_size) @@ -31,4 +31,4 @@ FloatingPointSize::FloatingPointSize(const FloatingPointSize& old) Assert(validSignificandSize(d_sig_size)); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h index be00e0987..ed5dccc4f 100644 --- a/src/util/floatingpoint_size.h +++ b/src/util/floatingpoint_size.h @@ -16,7 +16,7 @@ #ifndef CVC4__FLOATINGPOINT_SIZE_H #define CVC4__FLOATINGPOINT_SIZE_H -namespace CVC4 { +namespace CVC5 { // Inline these! inline bool validExponentSize(uint32_t e) { return e >= 2; } @@ -92,6 +92,6 @@ struct FloatingPointSizeHashFunction | t.significandWidth()); } }; /* struct FloatingPointSizeHashFunction */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index bf13669d3..0ecc6485d 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -22,7 +22,7 @@ #include <gmpxx.h> -namespace CVC4 { +namespace CVC5 { /** Hashes the gmp integer primitive in a word by word fashion. */ inline size_t gmpz_hash(const mpz_t toHash) { @@ -35,6 +35,6 @@ inline size_t gmpz_hash(const mpz_t toHash) { return hash; }/* gmpz_hash() */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__GMP_UTIL_H */ diff --git a/src/util/hash.h b/src/util/hash.h index 8adb4b473..066e01aad 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -38,7 +38,7 @@ struct hash<uint64_t> { }/* std namespace */ -namespace CVC4 { +namespace CVC5 { namespace fnv1a { @@ -64,6 +64,6 @@ struct PairHashFunction { } };/* struct PairHashFunction */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__HASH_H */ diff --git a/src/util/iand.h b/src/util/iand.h index e5f1a5af7..a50c4aeb7 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -22,7 +22,7 @@ #include "base/exception.h" #include "util/integer.h" -namespace CVC4 { +namespace CVC5 { struct IntAnd { @@ -41,6 +41,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) return os << "[" << ia.d_size << "]"; } -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__IAND_H */ diff --git a/src/util/index.cpp b/src/util/index.cpp index f3b3df29d..7c9f3c57f 100644 --- a/src/util/index.cpp +++ b/src/util/index.cpp @@ -19,7 +19,7 @@ #include <limits> -namespace CVC4 { +namespace CVC5 { static_assert(sizeof(Index) <= sizeof(size_t), "Index cannot be larger than size_t"); @@ -34,4 +34,4 @@ static_assert(!std::numeric_limits<Index>::is_signed, * (Limited testing suggests a ~1/16 of running time.) Interestingly, * uint_fast32_t also has a sizeof == 8 on x86_64. */ -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/index.h b/src/util/index.h index 6a050f4f9..1fa881eb6 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -19,11 +19,11 @@ #ifndef CVC4__INDEX_H #define CVC4__INDEX_H -namespace CVC4 { +namespace CVC5 { /** Index is a standardized unsigned integer used for efficient indexing. */ using Index = uint32_t; -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__INDEX_H */ diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h index 3c36a6a97..b201630c0 100644 --- a/src/util/indexed_root_predicate.h +++ b/src/util/indexed_root_predicate.h @@ -19,7 +19,7 @@ #ifndef CVC4__UTIL__INDEXED_ROOT_PREDICATE_H #define CVC4__UTIL__INDEXED_ROOT_PREDICATE_H -namespace CVC4 { +namespace CVC5 { /** * The structure representing the index of a root predicate. @@ -69,6 +69,6 @@ struct IndexedRootPredicateHashFunction } }; /* struct IndexedRootPredicateHashFunction */ -} // namespace CVC4 +} // namespace CVC5 #endif
\ No newline at end of file diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index a4035165e..0f02f03e5 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { signed int Integer::s_fastSignedIntMin = -(1 << 29); signed int Integer::s_fastSignedIntMax = (1 << 29) - 1; @@ -568,4 +568,4 @@ std::ostream& operator<<(std::ostream& os, const Integer& n) { return os << n.toString(); } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index db1e5068f..7d7b002f2 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -33,13 +33,13 @@ #include "base/exception.h" #include "cvc4_export.h" // remove when Cvc language support is removed -namespace CVC4 { +namespace CVC5 { class Rational; class CVC4_EXPORT Integer { - friend class CVC4::Rational; + friend class CVC5::Rational; public: /** @@ -380,11 +380,11 @@ class CVC4_EXPORT Integer struct IntegerHashFunction { - size_t operator()(const CVC4::Integer& i) const { return i.hash(); } + size_t operator()(const CVC5::Integer& i) const { return i.hash(); } }; /* struct IntegerHashFunction */ std::ostream& operator<<(std::ostream& os, const Integer& n); -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 89f6dc308..d1e0d7108 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -31,7 +31,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { Integer::Integer(const char* s, unsigned base) : d_value(s, base) @@ -483,4 +483,4 @@ const Integer& Integer::max(const Integer& a, const Integer& b) return (a >= b) ? a : b; } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 616408b42..fa206d08f 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -27,13 +27,13 @@ #include "cvc4_export.h" // remove when Cvc language support is removed -namespace CVC4 { +namespace CVC5 { class Rational; class CVC4_EXPORT Integer { - friend class CVC4::Rational; + friend class CVC5::Rational; public: /** @@ -330,7 +330,7 @@ class CVC4_EXPORT Integer struct IntegerHashFunction { - inline size_t operator()(const CVC4::Integer& i) const { return i.hash(); } + inline size_t operator()(const CVC5::Integer& i) const { return i.hash(); } }; /* struct IntegerHashFunction */ inline std::ostream& operator<<(std::ostream& os, const Integer& n) @@ -338,6 +338,6 @@ inline std::ostream& operator<<(std::ostream& os, const Integer& n) return os << n.toString(); } -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/maybe.h b/src/util/maybe.h index a74a42a17..35c0efd68 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -31,7 +31,7 @@ #include "base/exception.h" -namespace CVC4 { +namespace CVC5 { template <class T> class Maybe @@ -84,6 +84,6 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){ return out; } -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__UTIL__MAYBE_H */ diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp index dd9d3bf92..37fa0d892 100644 --- a/src/util/ostream_util.cpp +++ b/src/util/ostream_util.cpp @@ -17,7 +17,7 @@ #include <ostream> -namespace CVC4 { +namespace CVC5 { StreamFormatScope::StreamFormatScope(std::ostream& out) : d_out(out), d_format_flags(out.flags()), d_precision(out.precision()) @@ -30,4 +30,4 @@ StreamFormatScope::~StreamFormatScope() d_out.flags(d_format_flags); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index 1f70e33ad..c5e1e2797 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -22,7 +22,7 @@ #include <ios> #include <iosfwd> -namespace CVC4 { +namespace CVC5 { // Saves the formatting of an ostream and restores the previous settings on // destruction. Example usage: @@ -44,6 +44,6 @@ class StreamFormatScope std::streamsize d_precision; }; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__UTIL__OSTREAM_UTIL_H */ diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp index e9f80bf77..9dbb24872 100644 --- a/src/util/poly_util.cpp +++ b/src/util/poly_util.cpp @@ -35,7 +35,7 @@ #include "util/rational.h" #include "util/real_algebraic_number.h" -namespace CVC4 { +namespace CVC5 { namespace poly_utils { namespace { @@ -361,6 +361,6 @@ void getVariableInformation(VariableInformation& vi, } } // namespace poly_utils -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/poly_util.h b/src/util/poly_util.h index 203aec618..efb185932 100644 --- a/src/util/poly_util.h +++ b/src/util/poly_util.h @@ -36,7 +36,7 @@ #include <poly/polyxx.h> -namespace CVC4 { +namespace CVC5 { /** * Utilities for working with libpoly. * This namespace contains various basic conversion routines necessary for the @@ -49,28 +49,28 @@ namespace CVC4 { */ namespace poly_utils { -/** Converts a poly::Integer to a CVC4::Integer. */ +/** Converts a poly::Integer to a CVC5::Integer. */ Integer toInteger(const poly::Integer& i); -/** Converts a poly::Integer to a CVC4::Rational. */ +/** Converts a poly::Integer to a CVC5::Rational. */ Rational toRational(const poly::Integer& r); -/** Converts a poly::Rational to a CVC4::Rational. */ +/** Converts a poly::Rational to a CVC5::Rational. */ Rational toRational(const poly::Rational& r); -/** Converts a poly::DyadicRational to a CVC4::Rational. */ +/** Converts a poly::DyadicRational to a CVC5::Rational. */ Rational toRational(const poly::DyadicRational& dr); -/** Converts a poly::Value to a CVC4::Rational (that may be a bit above). */ +/** Converts a poly::Value to a CVC5::Rational (that may be a bit above). */ Rational toRationalAbove(const poly::Value& v); -/** Converts a poly::Value to a CVC4::Rational (that may be a bit below). */ +/** Converts a poly::Value to a CVC5::Rational (that may be a bit below). */ Rational toRationalBelow(const poly::Value& v); -/** Converts a CVC4::Integer to a poly::Integer. */ +/** Converts a CVC5::Integer to a poly::Integer. */ poly::Integer toInteger(const Integer& i); -/** Converts a vector of CVC4::Integers to a vector of poly::Integers. */ +/** Converts a vector of CVC5::Integers to a vector of poly::Integers. */ std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi); -/** Converts a CVC4::Rational to a poly::Rational. */ +/** Converts a CVC5::Rational to a poly::Rational. */ poly::Rational toRational(const Rational& r); /** - * Converts a CVC4::Rational to a poly::DyadicRational. If the input is not + * Converts a CVC5::Rational to a poly::DyadicRational. If the input is not * dyadic, no result is produced. */ Maybe<poly::DyadicRational> toDyadicRational(const Rational& r); @@ -91,7 +91,7 @@ poly::Rational approximateToDyadic(const poly::Rational& r, /** * Constructs a poly::AlgebraicNumber, allowing for refinement of the - * CVC4::Rational bounds. As a poly::AlgebraicNumber works on + * CVC5::Rational bounds. As a poly::AlgebraicNumber works on * poly::DyadicRationals internally, the bounds are iteratively refined using * approximateToDyadic until the respective interval is isolating. If the * provided rational bounds are already dyadic, the refinement is skipped. @@ -101,7 +101,7 @@ poly::AlgebraicNumber toPolyRanWithRefinement(poly::UPolynomial&& p, const Rational& upper); /** - * Constructs a CVC4::RealAlgebraicNumber, simply wrapping + * Constructs a CVC5::RealAlgebraicNumber, simply wrapping * toPolyRanWithRefinement. */ RealAlgebraicNumber toRanWithRefinement(poly::UPolynomial&& p, @@ -138,7 +138,7 @@ void getVariableInformation(VariableInformation& vi, const poly::Polynomial& poly); } // namespace poly_utils -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/random.cpp b/src/util/random.cpp index 9d94ff624..ab35bd389 100644 --- a/src/util/random.cpp +++ b/src/util/random.cpp @@ -21,7 +21,7 @@ #include <cfloat> #include "base/check.h" -namespace CVC4 { +namespace CVC5 { Random::Random(uint64_t seed) { setSeed(seed); } @@ -66,4 +66,4 @@ bool Random::pickWithProb(double probability) return r < p; } -} +} // namespace CVC5 diff --git a/src/util/random.h b/src/util/random.h index 31d93a643..67d4e052d 100644 --- a/src/util/random.h +++ b/src/util/random.h @@ -21,7 +21,7 @@ #ifndef CVC4__UTIL__RANDOM_H #define CVC4__UTIL__RANDOM_H -namespace CVC4 { +namespace CVC5 { class Random { @@ -69,5 +69,5 @@ class Random uint64_t d_state; }; -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index 4d948415f..a974a6155 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { /* Computes a rational given a decimal string. The rational * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>. @@ -117,4 +117,4 @@ Maybe<Rational> Rational::fromDouble(double d) } } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index bd48ad851..d2c57e90d 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -37,7 +37,7 @@ #include "util/integer.h" #include "util/maybe.h" -namespace CVC4 { +namespace CVC5 { /** ** A multi-precision rational constant. @@ -336,11 +336,11 @@ class CVC4_EXPORT Rational struct RationalHashFunction { - inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } + inline size_t operator()(const CVC5::Rational& r) const { return r.hash(); } }; /* struct RationalHashFunction */ std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__RATIONAL_H */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 2fbe45d80..0762e17c1 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -27,7 +27,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { std::ostream& operator<<(std::ostream& os, const Rational& q){ return os << q.toString(); @@ -98,4 +98,4 @@ Maybe<Rational> Rational::fromDouble(double d) return Maybe<Rational>(); } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 490211001..0d7569b21 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -29,7 +29,7 @@ #include "util/integer.h" #include "util/maybe.h" -namespace CVC4 { +namespace CVC5 { /** ** A multi-precision rational constant. @@ -326,11 +326,11 @@ class CVC4_EXPORT Rational struct RationalHashFunction { - inline size_t operator()(const CVC4::Rational& r) const { return r.hash(); } + inline size_t operator()(const CVC5::Rational& r) const { return r.hash(); } }; /* struct RationalHashFunction */ std::ostream& operator<<(std::ostream& os, const Rational& n) CVC4_EXPORT; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__RATIONAL_H */ diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index b4730c1b1..6a8111b55 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -28,7 +28,7 @@ #include "base/check.h" #include "util/poly_util.h" -namespace CVC4 { +namespace CVC5 { RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an) : d_value(std::move(an)) @@ -174,4 +174,4 @@ int sgn(const RealAlgebraicNumber& ran) { return sgn(ran.getValue()); } bool isZero(const RealAlgebraicNumber& ran) { return is_zero(ran.getValue()); } bool isOne(const RealAlgebraicNumber& ran) { return is_one(ran.getValue()); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index ef5ff16f1..4819e8866 100644 --- a/src/util/real_algebraic_number_poly_imp.h +++ b/src/util/real_algebraic_number_poly_imp.h @@ -26,7 +26,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { /** * Represents a real algebraic number based on poly::AlgebraicNumber. @@ -148,6 +148,6 @@ bool isZero(const RealAlgebraicNumber& ran); /** Check whether a real algebraic number is one. */ bool isOne(const RealAlgebraicNumber& ran); -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__REAL_ALGEBRAIC_NUMBER_H */ diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index eabafeb37..5df83b1ce 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -16,7 +16,7 @@ #include <ostream> -namespace CVC4 { +namespace CVC5 { RegExpRepeat::RegExpRepeat(uint32_t repeatAmount) : d_repeatAmount(repeatAmount) { @@ -57,4 +57,4 @@ std::ostream& operator<<(std::ostream& os, const RegExpLoop& r) return os << "[" << r.d_loopMinOcc << ".." << r.d_loopMaxOcc << "]"; } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/regexp.h b/src/util/regexp.h index b08065a25..c28f121c0 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC4 { +namespace CVC5 { struct RegExpRepeat { @@ -69,6 +69,6 @@ std::ostream& operator<<(std::ostream& os, const RegExpRepeat& bv); std::ostream& operator<<(std::ostream& os, const RegExpLoop& bv); -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__UTIL__REGEXP_H */ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index c31300077..00395178c 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { bool WallClockTimer::on() const { @@ -420,4 +420,4 @@ void ResourceManager::registerListener(Listener* listener) return d_listeners.push_back(listener); } -} /* namespace CVC4 */ +} // namespace CVC5 diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index a8a7edb75..3a6269e99 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -26,7 +26,7 @@ #include <memory> #include <vector> -namespace CVC4 { +namespace CVC5 { class Listener; class Options; @@ -206,6 +206,6 @@ class ResourceManager }; /* class ResourceManager */ -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__RESOURCE_MANAGER_H */ diff --git a/src/util/result.cpp b/src/util/result.cpp index 6e83953a3..f9fa94266 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { Result::Result() : d_sat(SAT_UNKNOWN), @@ -374,4 +374,4 @@ void Result::toStream(std::ostream& out, OutputLanguage language) const { }; } -} /* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/result.h b/src/util/result.h index b5c5451ea..e2a3a268a 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -24,7 +24,7 @@ #include "options/language.h" -namespace CVC4 { +namespace CVC5 { class Result; @@ -160,6 +160,6 @@ bool operator==(enum Result::Entailment e, const Result& r); bool operator!=(enum Result::Sat s, const Result& r); bool operator!=(enum Result::Entailment e, const Result& r); -} /* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__RESULT_H */ diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 485bbf847..e58689df6 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -18,7 +18,7 @@ #include <fenv.h> -namespace CVC4 { +namespace CVC5 { #define CVC4_NUM_ROUNDING_MODES 5 @@ -45,6 +45,6 @@ struct RoundingModeHashFunction inline size_t operator()(const RoundingMode& rm) const { return size_t(rm); } }; /* struct RoundingModeHashFunction */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp index adb051d70..c70119822 100644 --- a/src/util/safe_print.cpp +++ b/src/util/safe_print.cpp @@ -28,7 +28,7 @@ /* Size of buffers used */ #define BUFFER_SIZE 20 -namespace CVC4 { +namespace CVC5 { template <> void safe_print(int fd, const std::string& msg) { @@ -214,4 +214,4 @@ void safe_print_right_aligned(int fd, uint64_t i, ssize_t width) { } } -} /* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/safe_print.h b/src/util/safe_print.h index dd66ed41b..553f78bb7 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -44,7 +44,7 @@ #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { /** * Prints arrays of chars (e.g. string literals) of length N. Safe to use in a @@ -136,6 +136,6 @@ void safe_print_hex(int fd, uint64_t i); */ void safe_print_right_aligned(int fd, uint64_t i, ssize_t width); -} /* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__SAFE_PRINT_H */ diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index 05f617aa5..a39aebc63 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -23,7 +23,7 @@ #include "util/bitvector.h" #include "util/random.h" -namespace CVC4 { +namespace CVC5 { BitVector Sampler::pickBvUniform(unsigned sz) { @@ -172,4 +172,4 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) return FloatingPoint(e, s, bv); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/sampler.h b/src/util/sampler.h index 449ef96f9..f715536bc 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -22,7 +22,7 @@ #include "util/floatingpoint.h" -namespace CVC4 { +namespace CVC5 { class Sampler { @@ -52,6 +52,6 @@ class Sampler static constexpr double probSpecial = 0.2; }; -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */ diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 91ef8a271..3c93ef5ae 100644 --- a/src/util/sexpr.cpp +++ b/src/util/sexpr.cpp @@ -33,7 +33,7 @@ #include "util/ostream_util.h" #include "util/smt2_quote_string.h" -namespace CVC4 { +namespace CVC5 { const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); @@ -90,12 +90,14 @@ SExpr::SExpr(const SExpr& other) Assert((d_children == NULL) == isAtom()); } -SExpr::SExpr(const CVC4::Integer& value) +SExpr::SExpr(const CVC5::Integer& value) : d_sexprType(SEXPR_INTEGER), d_integerValue(value), d_rationalValue(0), d_stringValue(""), - d_children(NULL) {} + d_children(NULL) +{ +} SExpr::SExpr(int value) : d_sexprType(SEXPR_INTEGER), @@ -125,12 +127,14 @@ SExpr::SExpr(unsigned long int value) d_stringValue(""), d_children(NULL) {} -SExpr::SExpr(const CVC4::Rational& value) +SExpr::SExpr(const CVC5::Rational& value) : d_sexprType(SEXPR_RATIONAL), d_integerValue(0), d_rationalValue(value), d_stringValue(""), - d_children(NULL) {} + d_children(NULL) +{ +} SExpr::SExpr(const std::string& value) : d_sexprType(SEXPR_STRING), @@ -304,12 +308,14 @@ std::string SExpr::getValue() const { return std::string(); } -const CVC4::Integer& SExpr::getIntegerValue() const { +const CVC5::Integer& SExpr::getIntegerValue() const +{ PrettyCheckArgument(isInteger(), this); return d_integerValue; } -const CVC4::Rational& SExpr::getRationalValue() const { +const CVC5::Rational& SExpr::getRationalValue() const +{ PrettyCheckArgument(isRational(), this); return d_rationalValue; } @@ -377,4 +383,4 @@ SExpr SExpr::parseListOfListOfAtoms( return SExpr(parsedListsOfAtoms); } -} /* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/sexpr.h b/src/util/sexpr.h index aabbf473d..f4eaca663 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -35,7 +35,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { class SExprKeyword { @@ -61,14 +61,14 @@ class CVC4_EXPORT SExpr SExpr& operator=(const SExpr& other); ~SExpr(); - SExpr(const CVC4::Integer& value); + SExpr(const CVC5::Integer& value); SExpr(int value); SExpr(long int value); SExpr(unsigned int value); SExpr(unsigned long int value); - SExpr(const CVC4::Rational& value); + SExpr(const CVC5::Rational& value); SExpr(const std::string& value); @@ -120,13 +120,13 @@ class CVC4_EXPORT SExpr * Get the integer value of this S-expression. This will cause an * error if this S-expression is not an integer. */ - const CVC4::Integer& getIntegerValue() const; + const CVC5::Integer& getIntegerValue() const; /** * Get the rational value of this S-expression. This will cause an * error if this S-expression is not a rational. */ - const CVC4::Rational& getRationalValue() const; + const CVC5::Rational& getRationalValue() const; /** * Get the children of this S-expression. This will cause an error @@ -211,10 +211,10 @@ class CVC4_EXPORT SExpr } d_sexprType; /** The value of an atomic integer-valued S-expression. */ - CVC4::Integer d_integerValue; + CVC5::Integer d_integerValue; /** The value of an atomic rational-valued S-expression. */ - CVC4::Rational d_rationalValue; + CVC5::Rational d_rationalValue; /** The value of an atomic S-expression. */ std::string d_stringValue; @@ -301,6 +301,6 @@ class CVC4_EXPORT PrettySExprs */ std::ostream& operator<<(std::ostream& out, PrettySExprs ps); -} /* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__SEXPR_H */ diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index e06e5dc93..7d255c6f1 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -19,7 +19,7 @@ #include <sstream> #include <string> -namespace CVC4 { +namespace CVC5 { /** * SMT-LIB 2 quoting for symbols @@ -43,4 +43,4 @@ std::string quoteSymbol(const std::string& s){ return s; } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index 911faae42..b9e6592df 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -21,13 +21,13 @@ #include <string> -namespace CVC4 { +namespace CVC5 { /** * SMT-LIB 2 quoting for symbols */ std::string quoteSymbol(const std::string& s); -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */ diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index d824e0f21..3c7ac6731 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -20,8 +20,7 @@ #include "util/safe_print.h" #include "util/statistics_registry.h" // for details about class Stat - -namespace CVC4 { +namespace CVC5 { bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { return s1->getName() < s2->getName(); @@ -131,4 +130,4 @@ SExpr StatisticsBase::getStatistic(std::string name) const { } } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/statistics.h b/src/util/statistics.h index 7b5400aaf..0c52cfe8e 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -29,7 +29,7 @@ #include "cvc4_export.h" #include "util/sexpr.h" -namespace CVC4 { +namespace CVC5 { class Stat; @@ -127,6 +127,6 @@ public: }; /* class Statistics */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__STATISTICS_H */ diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index b439daba8..bbd98ffaf 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -34,7 +34,7 @@ /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ -namespace CVC4 { +namespace CVC5 { void StatisticsRegistry::registerStat(Stat* s) { @@ -89,4 +89,4 @@ RegisterStatistic::~RegisterStatistic() { d_reg->unregisterStat(d_stat); } -}/* CVC4 namespace */ +} // namespace CVC5 diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index a55aec282..b8c83436f 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -102,7 +102,7 @@ #include "util/statistics.h" #include "util/stats_base.h" -namespace CVC4 { +namespace CVC5 { /** A statistic that contains a SExpr. */ class SExprStat : public Stat { @@ -196,6 +196,6 @@ private: }; /* class RegisterStatistic */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp index f55e2f5ab..758883cbe 100644 --- a/src/util/stats_base.cpp +++ b/src/util/stats_base.cpp @@ -18,7 +18,7 @@ #include "util/statistics_registry.h" -namespace CVC4 { +namespace CVC5 { Stat::Stat(const std::string& name) : d_name(name) { @@ -112,4 +112,4 @@ SExpr AverageStat::getValue() const return SExpr(Rational::fromDecimal(ss.str())); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/stats_base.h b/src/util/stats_base.h index 24a2ca560..f7d19624a 100644 --- a/src/util/stats_base.h +++ b/src/util/stats_base.h @@ -34,7 +34,7 @@ #define CVC4_USE_STATISTICS false #endif -namespace CVC4 { +namespace CVC5 { /** * The base class for all statistics. @@ -274,6 +274,6 @@ class SizeStat : public Stat const T& d_sized; }; /* class SizeStat */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h index 49306ba28..44d4b9e7c 100644 --- a/src/util/stats_histogram.h +++ b/src/util/stats_histogram.h @@ -24,7 +24,7 @@ #include "util/stats_base.h" -namespace CVC4 { +namespace CVC5 { /** * A histogram statistic class for integral types. @@ -123,6 +123,6 @@ class IntegralHistogramStat : public Stat int64_t d_offset; }; /* class IntegralHistogramStat */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp index 63d9914d6..6280b79e1 100644 --- a/src/util/stats_timer.cpp +++ b/src/util/stats_timer.cpp @@ -21,7 +21,7 @@ #include "base/check.h" #include "util/ostream_util.h" -namespace CVC4 { +namespace CVC5 { template <> void safe_print(int fd, const timer_stat_detail::duration& t) @@ -101,4 +101,4 @@ CodeTimer::~CodeTimer() } } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h index 36e254795..40df52ade 100644 --- a/src/util/stats_timer.h +++ b/src/util/stats_timer.h @@ -24,7 +24,7 @@ #include "cvc4_export.h" #include "util/stats_base.h" -namespace CVC4 { +namespace CVC5 { namespace timer_stat_detail { using clock = std::chrono::steady_clock; using time_point = clock::time_point; @@ -46,7 +46,7 @@ class CodeTimer; class CVC4_EXPORT TimerStat : public BackedStat<timer_stat_detail::duration> { public: - typedef CVC4::CodeTimer CodeTimer; + typedef CVC5::CodeTimer CodeTimer; /** * Construct a timer statistic with the given name. Newly-constructed @@ -108,6 +108,6 @@ private: CodeTimer& operator=(const CodeTimer& timer) = delete; }; /* class CodeTimer */ -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp index 893afcb4c..2a87ff439 100644 --- a/src/util/stats_utils.cpp +++ b/src/util/stats_utils.cpp @@ -23,7 +23,7 @@ #include "util/ostream_util.h" #include "util/stats_timer.h" -namespace CVC4 { +namespace CVC5 { std::ostream& operator<<(std::ostream& os, const timer_stat_detail::duration& dur) @@ -35,4 +35,4 @@ std::ostream& operator<<(std::ostream& os, << (dur % std::chrono::seconds(1)).count(); } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h index b38f7b641..d511539ca 100644 --- a/src/util/stats_utils.h +++ b/src/util/stats_utils.h @@ -23,7 +23,7 @@ #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { namespace timer_stat_detail { struct duration; @@ -32,6 +32,6 @@ struct duration; std::ostream& operator<<(std::ostream& os, const timer_stat_detail::duration& dur) CVC4_EXPORT; -} // namespace CVC4 +} // namespace CVC5 #endif diff --git a/src/util/string.cpp b/src/util/string.cpp index 73a0d78ee..d1d7fadc2 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -25,7 +25,7 @@ using namespace std; -namespace CVC4 { +namespace CVC5 { static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values."); @@ -101,7 +101,7 @@ void String::addCharToInternal(unsigned char ch, std::vector<unsigned>& str) std::stringstream serr; serr << "Illegal string character: \"" << ch << "\", must use escape sequence"; - throw CVC4::Exception(serr.str()); + throw CVC5::Exception(serr.str()); } else { @@ -513,4 +513,4 @@ std::ostream &operator<<(std::ostream &os, const String &s) { return os << "\"" << s.toString() << "\""; } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/string.h b/src/util/string.h index 6c620587a..a3e0245aa 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -23,7 +23,7 @@ #include "util/rational.h" -namespace CVC4 { +namespace CVC5 { /** The CVC4 string class * @@ -46,7 +46,7 @@ class String static inline unsigned num_codes() { return 196608; } /** constructors for String * - * Internally, a CVC4::String is represented by a vector of unsigned + * Internally, a CVC5::String is represented by a vector of unsigned * integers (d_str) representing the code points of the characters. * * To build a string from a C++ string, we may process escape sequences @@ -61,7 +61,7 @@ class String * where d_0 ... d_4 are hexadecimal digits, to the appropriate character. * * If useEscSequences is false, then the characters of the constructed - * CVC4::String correspond one-to-one with the input string. + * CVC5::String correspond one-to-one with the input string. */ String() = default; explicit String(const std::string& s, bool useEscSequences = false) @@ -112,7 +112,7 @@ class String * If useEscSequences is false, the string's printable characters are * printed as characters. Notice that for all std::string s having only * printable characters, we have that - * CVC4::String( s ).toString() = s. + * CVC5::String( s ).toString() = s. */ std::string toString(bool useEscSequences = false) const; /* toWString @@ -265,7 +265,8 @@ namespace strings { struct StringHashFunction { - size_t operator()(const ::CVC4::String& s) const { + size_t operator()(const ::CVC5::String& s) const + { return std::hash<std::string>()(s.toString()); } }; /* struct StringHashFunction */ @@ -274,6 +275,6 @@ struct StringHashFunction std::ostream& operator<<(std::ostream& os, const String& s); -} // namespace CVC4 +} // namespace CVC5 #endif /* CVC4__UTIL__STRING_H */ diff --git a/src/util/tuple.h b/src/util/tuple.h index d77d7bf97..571bfe797 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -23,7 +23,7 @@ #include <vector> #include <utility> -namespace CVC4 { +namespace CVC5 { class TupleUpdate { @@ -49,6 +49,6 @@ inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { return out << "[" << t.getIndex() << "]"; } -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__TUPLE_H */ diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 29c22409c..31fe26577 100644 --- a/src/util/unsafe_interrupt_exception.h +++ b/src/util/unsafe_interrupt_exception.h @@ -21,9 +21,9 @@ #include "base/exception.h" #include "cvc4_export.h" -namespace CVC4 { +namespace CVC5 { -class CVC4_EXPORT UnsafeInterruptException : public CVC4::Exception +class CVC4_EXPORT UnsafeInterruptException : public CVC5::Exception { public: UnsafeInterruptException() : @@ -40,6 +40,6 @@ class CVC4_EXPORT UnsafeInterruptException : public CVC4::Exception } }; /* class UnsafeInterruptException */ -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */ diff --git a/src/util/utility.cpp b/src/util/utility.cpp index 6ce331fc4..480b68ff2 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -22,7 +22,7 @@ #include "base/check.h" -namespace CVC4 { +namespace CVC5 { std::unique_ptr<std::fstream> openTmpFile(std::string* pattern) { @@ -52,4 +52,4 @@ std::unique_ptr<std::fstream> openTmpFile(std::string* pattern) return tmpStream; } -} // namespace CVC4 +} // namespace CVC5 diff --git a/src/util/utility.h b/src/util/utility.h index 411d3a6f3..006f2072c 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -24,8 +24,7 @@ #include <memory> #include <string> -namespace CVC4 { - +namespace CVC5 { /** * Using std::find_if(), finds the first iterator in [first,last) @@ -78,6 +77,6 @@ void container_to_stream(std::ostream& out, */ std::unique_ptr<std::fstream> openTmpFile(std::string* pattern); -}/* CVC4 namespace */ +} // namespace CVC5 #endif /* CVC4__UTILITY_H */ |