diff options
Diffstat (limited to 'src/util')
72 files changed, 195 insertions, 195 deletions
diff --git a/src/util/abstract_value.cpp b/src/util/abstract_value.cpp index 4f6cadde4..1f8802d22 100644 --- a/src/util/abstract_value.cpp +++ b/src/util/abstract_value.cpp @@ -24,7 +24,7 @@ using namespace std; -namespace CVC5 { +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()); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/abstract_value.h b/src/util/abstract_value.h index ddd1018a2..f933cafdf 100644 --- a/src/util/abstract_value.h +++ b/src/util/abstract_value.h @@ -22,7 +22,7 @@ #include "util/integer.h" -namespace CVC5 { +namespace cvc5 { class AbstractValue { @@ -61,4 +61,4 @@ struct AbstractValueHashFunction } }; /* struct AbstractValueHashFunction */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/bin_heap.h b/src/util/bin_heap.h index 40f2da045..4306cd731 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 CVC5 { +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; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__BIN_HEAP_H */ diff --git a/src/util/bitvector.cpp b/src/util/bitvector.cpp index 85b373886..210d03891 100644 --- a/src/util/bitvector.cpp +++ b/src/util/bitvector.cpp @@ -20,7 +20,7 @@ #include "base/exception.h" -namespace CVC5 { +namespace cvc5 { unsigned BitVector::getSize() const { return d_size; } @@ -375,4 +375,4 @@ BitVector BitVector::mkMaxSigned(unsigned size) return ~BitVector::mkMinSigned(size); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/bitvector.h b/src/util/bitvector.h index fbb91b8e3..12908166d 100644 --- a/src/util/bitvector.h +++ b/src/util/bitvector.h @@ -25,7 +25,7 @@ #include "base/exception.h" #include "util/integer.h" -namespace CVC5 { +namespace cvc5 { class BitVector { @@ -442,6 +442,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntToBitVector& bv) return os << "[" << bv.d_size << "]"; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__BITVECTOR_H */ diff --git a/src/util/bool.h b/src/util/bool.h index d1f57fcd4..01d97a43a 100644 --- a/src/util/bool.h +++ b/src/util/bool.h @@ -19,7 +19,7 @@ #ifndef CVC4__BOOL_H #define CVC4__BOOL_H -namespace CVC5 { +namespace cvc5 { struct BoolHashFunction { inline size_t operator()(bool b) const { @@ -27,6 +27,6 @@ struct BoolHashFunction { } };/* struct BoolHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__BOOL_H */ diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp index 027c3d2db..acbb26b19 100644 --- a/src/util/cardinality.cpp +++ b/src/util/cardinality.cpp @@ -22,7 +22,7 @@ #include "base/check.h" #include "base/exception.h" -namespace CVC5 { +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; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/cardinality.h b/src/util/cardinality.h index 2ab2fdd63..f188a8c8c 100644 --- a/src/util/cardinality.h +++ b/src/util/cardinality.h @@ -24,7 +24,7 @@ #include "util/integer.h" -namespace CVC5 { +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); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__CARDINALITY_H */ diff --git a/src/util/dense_map.h b/src/util/dense_map.h index e6fed6916..f3b0372b2 100644 --- a/src/util/dense_map.h +++ b/src/util/dense_map.h @@ -35,7 +35,7 @@ #include "base/check.h" #include "util/index.h" -namespace CVC5 { +namespace cvc5 { template <class T> class DenseMap { @@ -338,4 +338,4 @@ public: void pop_back() { d_map.pop_back(); } }; /* class DenseMultiset */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/divisible.cpp b/src/util/divisible.cpp index 45b1f6c27..d8c099923 100644 --- a/src/util/divisible.cpp +++ b/src/util/divisible.cpp @@ -22,10 +22,10 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { Divisible::Divisible(const Integer& n) : k(n) { PrettyCheckArgument(n > 0, n, "Divisible predicate must be constructed over positive N"); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/divisible.h b/src/util/divisible.h index 5b3506ee8..95934a52a 100644 --- a/src/util/divisible.h +++ b/src/util/divisible.h @@ -26,7 +26,7 @@ #include "util/integer.h" -namespace CVC5 { +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; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__DIVISIBLE_H */ diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index be5f6a496..a9d404103 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -28,7 +28,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC5 { +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() << ")"; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/floatingpoint.h b/src/util/floatingpoint.h index 060d1de99..e038959a0 100644 --- a/src/util/floatingpoint.h +++ b/src/util/floatingpoint.h @@ -29,7 +29,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC5 { +namespace cvc5 { /* -------------------------------------------------------------------------- */ @@ -514,7 +514,7 @@ struct FloatingPointToBVHashFunction { inline size_t operator()(const FloatingPointToBV& fptbv) const { - UnsignedHashFunction< ::CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__FLOATINGPOINT_H */ diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index efd3e2399..666c3438d 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<::CVC5::symfpuLiteral::CVC4Prop, T> \ + struct ite<::cvc5::symfpuLiteral::CVC4Prop, T> \ { \ - static const T& iteOp(const ::CVC5::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(::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); +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(::CVC5::symfpuLiteral::traits::ubv); /* -------------------------------------------------------------------------- */ -namespace CVC5 { +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 ::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; }; +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 CVC5 +} // namespace cvc5 diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index d01bf6a9d..c4352c080 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -30,7 +30,7 @@ /* -------------------------------------------------------------------------- */ -namespace CVC5 { +namespace cvc5 { class FloatingPointSize; class FloatingPointLiteral; @@ -56,8 +56,8 @@ class wrappedBitVector; using CVC4BitWidth = uint32_t; using CVC4Prop = bool; -using CVC4RM = ::CVC5::RoundingMode; -using CVC4FPSize = ::CVC5::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 CVC5::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 - * CVC5::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 CVC5 +} // namespace cvc5 #endif diff --git a/src/util/floatingpoint_size.cpp b/src/util/floatingpoint_size.cpp index 78558ab27..cf7aea524 100644 --- a/src/util/floatingpoint_size.cpp +++ b/src/util/floatingpoint_size.cpp @@ -15,7 +15,7 @@ #include "base/check.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/floatingpoint_size.h b/src/util/floatingpoint_size.h index ed5dccc4f..8350ffaec 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 CVC5 { +namespace cvc5 { // Inline these! inline bool validExponentSize(uint32_t e) { return e >= 2; } @@ -92,6 +92,6 @@ struct FloatingPointSizeHashFunction | t.significandWidth()); } }; /* struct FloatingPointSizeHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/util/gmp_util.h b/src/util/gmp_util.h index 0ecc6485d..0b08f4f38 100644 --- a/src/util/gmp_util.h +++ b/src/util/gmp_util.h @@ -22,7 +22,7 @@ #include <gmpxx.h> -namespace CVC5 { +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() */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__GMP_UTIL_H */ diff --git a/src/util/hash.h b/src/util/hash.h index 066e01aad..6ba4534d1 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -38,7 +38,7 @@ struct hash<uint64_t> { }/* std namespace */ -namespace CVC5 { +namespace cvc5 { namespace fnv1a { @@ -64,6 +64,6 @@ struct PairHashFunction { } };/* struct PairHashFunction */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__HASH_H */ diff --git a/src/util/iand.h b/src/util/iand.h index a50c4aeb7..e1a42b11b 100644 --- a/src/util/iand.h +++ b/src/util/iand.h @@ -22,7 +22,7 @@ #include "base/exception.h" #include "util/integer.h" -namespace CVC5 { +namespace cvc5 { struct IntAnd { @@ -41,6 +41,6 @@ inline std::ostream& operator<<(std::ostream& os, const IntAnd& ia) return os << "[" << ia.d_size << "]"; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__IAND_H */ diff --git a/src/util/index.cpp b/src/util/index.cpp index 7c9f3c57f..ffb49f943 100644 --- a/src/util/index.cpp +++ b/src/util/index.cpp @@ -19,7 +19,7 @@ #include <limits> -namespace CVC5 { +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. */ -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/index.h b/src/util/index.h index 1fa881eb6..6da0d8602 100644 --- a/src/util/index.h +++ b/src/util/index.h @@ -19,11 +19,11 @@ #ifndef CVC4__INDEX_H #define CVC4__INDEX_H -namespace CVC5 { +namespace cvc5 { /** Index is a standardized unsigned integer used for efficient indexing. */ using Index = uint32_t; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__INDEX_H */ diff --git a/src/util/indexed_root_predicate.h b/src/util/indexed_root_predicate.h index b201630c0..a35ecaa12 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 CVC5 { +namespace cvc5 { /** * The structure representing the index of a root predicate. @@ -69,6 +69,6 @@ struct IndexedRootPredicateHashFunction } }; /* struct IndexedRootPredicateHashFunction */ -} // namespace CVC5 +} // 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 0f02f03e5..3b70a98bf 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index 7d7b002f2..d3d9faf56 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 CVC5 { +namespace cvc5 { class Rational; class CVC4_EXPORT Integer { - friend class CVC5::Rational; + friend class cvc5::Rational; public: /** @@ -380,11 +380,11 @@ class CVC4_EXPORT Integer struct IntegerHashFunction { - size_t operator()(const CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index d1e0d7108..399b7bbbe 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -31,7 +31,7 @@ using namespace std; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index fa206d08f..0d129ef45 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 CVC5 { +namespace cvc5 { class Rational; class CVC4_EXPORT Integer { - friend class CVC5::Rational; + friend class cvc5::Rational; public: /** @@ -330,7 +330,7 @@ class CVC4_EXPORT Integer struct IntegerHashFunction { - inline size_t operator()(const CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__INTEGER_H */ diff --git a/src/util/maybe.h b/src/util/maybe.h index 35c0efd68..688073b8c 100644 --- a/src/util/maybe.h +++ b/src/util/maybe.h @@ -31,7 +31,7 @@ #include "base/exception.h" -namespace CVC5 { +namespace cvc5 { template <class T> class Maybe @@ -84,6 +84,6 @@ inline std::ostream& operator<<(std::ostream& out, const Maybe<T>& m){ return out; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL__MAYBE_H */ diff --git a/src/util/ostream_util.cpp b/src/util/ostream_util.cpp index 37fa0d892..8a3b2b47b 100644 --- a/src/util/ostream_util.cpp +++ b/src/util/ostream_util.cpp @@ -17,7 +17,7 @@ #include <ostream> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/ostream_util.h b/src/util/ostream_util.h index c5e1e2797..ab61faaca 100644 --- a/src/util/ostream_util.h +++ b/src/util/ostream_util.h @@ -22,7 +22,7 @@ #include <ios> #include <iosfwd> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL__OSTREAM_UTIL_H */ diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp index 9dbb24872..7cb8baae3 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 CVC5 { +namespace cvc5 { namespace poly_utils { namespace { @@ -361,6 +361,6 @@ void getVariableInformation(VariableInformation& vi, } } // namespace poly_utils -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/util/poly_util.h b/src/util/poly_util.h index efb185932..217f7c774 100644 --- a/src/util/poly_util.h +++ b/src/util/poly_util.h @@ -36,7 +36,7 @@ #include <poly/polyxx.h> -namespace CVC5 { +namespace cvc5 { /** * Utilities for working with libpoly. * This namespace contains various basic conversion routines necessary for the @@ -49,28 +49,28 @@ namespace CVC5 { */ namespace poly_utils { -/** Converts a poly::Integer to a CVC5::Integer. */ +/** Converts a poly::Integer to a cvc5::Integer. */ Integer toInteger(const poly::Integer& i); -/** Converts a poly::Integer to a CVC5::Rational. */ +/** Converts a poly::Integer to a cvc5::Rational. */ Rational toRational(const poly::Integer& r); -/** Converts a poly::Rational to a CVC5::Rational. */ +/** Converts a poly::Rational to a cvc5::Rational. */ Rational toRational(const poly::Rational& r); -/** Converts a poly::DyadicRational to a CVC5::Rational. */ +/** Converts a poly::DyadicRational to a cvc5::Rational. */ Rational toRational(const poly::DyadicRational& dr); -/** Converts a poly::Value to a CVC5::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 CVC5::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 CVC5::Integer to a poly::Integer. */ +/** Converts a cvc5::Integer to a poly::Integer. */ poly::Integer toInteger(const Integer& i); -/** Converts a vector of CVC5::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 CVC5::Rational to a poly::Rational. */ +/** Converts a cvc5::Rational to a poly::Rational. */ poly::Rational toRational(const Rational& r); /** - * Converts a CVC5::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 - * CVC5::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 CVC5::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 CVC5 +} // namespace cvc5 #endif diff --git a/src/util/random.cpp b/src/util/random.cpp index ab35bd389..feac8d5b6 100644 --- a/src/util/random.cpp +++ b/src/util/random.cpp @@ -21,7 +21,7 @@ #include <cfloat> #include "base/check.h" -namespace CVC5 { +namespace cvc5 { Random::Random(uint64_t seed) { setSeed(seed); } @@ -66,4 +66,4 @@ bool Random::pickWithProb(double probability) return r < p; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/random.h b/src/util/random.h index 67d4e052d..738f5c510 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 CVC5 { +namespace cvc5 { class Random { @@ -69,5 +69,5 @@ class Random uint64_t d_state; }; -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index a974a6155..b12fd8d28 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index d2c57e90d..d62694868 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 CVC5 { +namespace cvc5 { /** ** A multi-precision rational constant. @@ -336,11 +336,11 @@ class CVC4_EXPORT Rational struct RationalHashFunction { - inline size_t operator()(const CVC5::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 CVC5 +} // namespace cvc5 #endif /* CVC4__RATIONAL_H */ diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 0762e17c1..69a2fa2dd 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -27,7 +27,7 @@ #include "base/check.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index 0d7569b21..2bfc2a5b9 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 CVC5 { +namespace cvc5 { /** ** A multi-precision rational constant. @@ -326,11 +326,11 @@ class CVC4_EXPORT Rational struct RationalHashFunction { - inline size_t operator()(const CVC5::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 CVC5 +} // 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 6a8111b55..5c7dd9468 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 CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index 4819e8866..b376a236a 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 CVC5 { +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 CVC5 +} // namespace cvc5 #endif /* CVC4__REAL_ALGEBRAIC_NUMBER_H */ diff --git a/src/util/regexp.cpp b/src/util/regexp.cpp index 5df83b1ce..ef08da6fa 100644 --- a/src/util/regexp.cpp +++ b/src/util/regexp.cpp @@ -16,7 +16,7 @@ #include <ostream> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/regexp.h b/src/util/regexp.h index c28f121c0..0f929ff9e 100644 --- a/src/util/regexp.h +++ b/src/util/regexp.h @@ -19,7 +19,7 @@ #include <iosfwd> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL__REGEXP_H */ diff --git a/src/util/resource_manager.cpp b/src/util/resource_manager.cpp index 00395178c..a982c5e1d 100644 --- a/src/util/resource_manager.cpp +++ b/src/util/resource_manager.cpp @@ -28,7 +28,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { bool WallClockTimer::on() const { @@ -420,4 +420,4 @@ void ResourceManager::registerListener(Listener* listener) return d_listeners.push_back(listener); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/resource_manager.h b/src/util/resource_manager.h index 3a6269e99..64a94cdc9 100644 --- a/src/util/resource_manager.h +++ b/src/util/resource_manager.h @@ -26,7 +26,7 @@ #include <memory> #include <vector> -namespace CVC5 { +namespace cvc5 { class Listener; class Options; @@ -206,6 +206,6 @@ class ResourceManager }; /* class ResourceManager */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__RESOURCE_MANAGER_H */ diff --git a/src/util/result.cpp b/src/util/result.cpp index f9fa94266..32a7e5895 100644 --- a/src/util/result.cpp +++ b/src/util/result.cpp @@ -26,7 +26,7 @@ using namespace std; -namespace CVC5 { +namespace cvc5 { Result::Result() : d_sat(SAT_UNKNOWN), @@ -374,4 +374,4 @@ void Result::toStream(std::ostream& out, OutputLanguage language) const { }; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/result.h b/src/util/result.h index e2a3a268a..9fdd61792 100644 --- a/src/util/result.h +++ b/src/util/result.h @@ -24,7 +24,7 @@ #include "options/language.h" -namespace CVC5 { +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); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__RESULT_H */ diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index e58689df6..2acc5a457 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -18,7 +18,7 @@ #include <fenv.h> -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif diff --git a/src/util/safe_print.cpp b/src/util/safe_print.cpp index c70119822..ce4f529a4 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 CVC5 { +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) { } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/safe_print.h b/src/util/safe_print.h index 553f78bb7..ca844ef73 100644 --- a/src/util/safe_print.h +++ b/src/util/safe_print.h @@ -44,7 +44,7 @@ #include "cvc4_export.h" -namespace CVC5 { +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); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SAFE_PRINT_H */ diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index a39aebc63..5351a6175 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -23,7 +23,7 @@ #include "util/bitvector.h" #include "util/random.h" -namespace CVC5 { +namespace cvc5 { BitVector Sampler::pickBvUniform(unsigned sz) { @@ -172,4 +172,4 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) return FloatingPoint(e, s, bv); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/sampler.h b/src/util/sampler.h index f715536bc..19ed68c0f 100644 --- a/src/util/sampler.h +++ b/src/util/sampler.h @@ -22,7 +22,7 @@ #include "util/floatingpoint.h" -namespace CVC5 { +namespace cvc5 { class Sampler { @@ -52,6 +52,6 @@ class Sampler static constexpr double probSpecial = 0.2; }; -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL_FLOATINGPOINT_SAMPLER_H */ diff --git a/src/util/sexpr.cpp b/src/util/sexpr.cpp index 3c93ef5ae..85dd038bb 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 CVC5 { +namespace cvc5 { const int PrettySExprs::s_iosIndex = std::ios_base::xalloc(); @@ -90,7 +90,7 @@ SExpr::SExpr(const SExpr& other) Assert((d_children == NULL) == isAtom()); } -SExpr::SExpr(const CVC5::Integer& value) +SExpr::SExpr(const cvc5::Integer& value) : d_sexprType(SEXPR_INTEGER), d_integerValue(value), d_rationalValue(0), @@ -127,7 +127,7 @@ SExpr::SExpr(unsigned long int value) d_stringValue(""), d_children(NULL) {} -SExpr::SExpr(const CVC5::Rational& value) +SExpr::SExpr(const cvc5::Rational& value) : d_sexprType(SEXPR_RATIONAL), d_integerValue(0), d_rationalValue(value), @@ -308,13 +308,13 @@ std::string SExpr::getValue() const { return std::string(); } -const CVC5::Integer& SExpr::getIntegerValue() const +const cvc5::Integer& SExpr::getIntegerValue() const { PrettyCheckArgument(isInteger(), this); return d_integerValue; } -const CVC5::Rational& SExpr::getRationalValue() const +const cvc5::Rational& SExpr::getRationalValue() const { PrettyCheckArgument(isRational(), this); return d_rationalValue; @@ -383,4 +383,4 @@ SExpr SExpr::parseListOfListOfAtoms( return SExpr(parsedListsOfAtoms); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/sexpr.h b/src/util/sexpr.h index f4eaca663..3fcd398f7 100644 --- a/src/util/sexpr.h +++ b/src/util/sexpr.h @@ -35,7 +35,7 @@ #include "util/integer.h" #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { class SExprKeyword { @@ -61,14 +61,14 @@ class CVC4_EXPORT SExpr SExpr& operator=(const SExpr& other); ~SExpr(); - SExpr(const CVC5::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 CVC5::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 CVC5::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 CVC5::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. */ - CVC5::Integer d_integerValue; + cvc5::Integer d_integerValue; /** The value of an atomic rational-valued S-expression. */ - CVC5::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); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__SEXPR_H */ diff --git a/src/util/smt2_quote_string.cpp b/src/util/smt2_quote_string.cpp index 7d255c6f1..c4e01acc4 100644 --- a/src/util/smt2_quote_string.cpp +++ b/src/util/smt2_quote_string.cpp @@ -19,7 +19,7 @@ #include <sstream> #include <string> -namespace CVC5 { +namespace cvc5 { /** * SMT-LIB 2 quoting for symbols @@ -43,4 +43,4 @@ std::string quoteSymbol(const std::string& s){ return s; } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/smt2_quote_string.h b/src/util/smt2_quote_string.h index b9e6592df..be2546053 100644 --- a/src/util/smt2_quote_string.h +++ b/src/util/smt2_quote_string.h @@ -21,13 +21,13 @@ #include <string> -namespace CVC5 { +namespace cvc5 { /** * SMT-LIB 2 quoting for symbols */ std::string quoteSymbol(const std::string& s); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL__SMT2_QUOTE_STRING_H */ diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 3c7ac6731..494a70e6c 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -20,7 +20,7 @@ #include "util/safe_print.h" #include "util/statistics_registry.h" // for details about class Stat -namespace CVC5 { +namespace cvc5 { bool StatisticsBase::StatCmp::operator()(const Stat* s1, const Stat* s2) const { return s1->getName() < s2->getName(); @@ -130,4 +130,4 @@ SExpr StatisticsBase::getStatistic(std::string name) const { } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/statistics.h b/src/util/statistics.h index 0c52cfe8e..8989cb60d 100644 --- a/src/util/statistics.h +++ b/src/util/statistics.h @@ -29,7 +29,7 @@ #include "cvc4_export.h" #include "util/sexpr.h" -namespace CVC5 { +namespace cvc5 { class Stat; @@ -127,6 +127,6 @@ public: }; /* class Statistics */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__STATISTICS_H */ diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index bbd98ffaf..f9e05e68f 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -34,7 +34,7 @@ /****************************************************************************/ /* Some utility functions for timespec */ /****************************************************************************/ -namespace CVC5 { +namespace cvc5 { void StatisticsRegistry::registerStat(Stat* s) { @@ -89,4 +89,4 @@ RegisterStatistic::~RegisterStatistic() { d_reg->unregisterStat(d_stat); } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index b8c83436f..44f40d5d3 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 CVC5 { +namespace cvc5 { /** A statistic that contains a SExpr. */ class SExprStat : public Stat { @@ -196,6 +196,6 @@ private: }; /* class RegisterStatistic */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__STATISTICS_REGISTRY_H */ diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp index 758883cbe..3ae50cd51 100644 --- a/src/util/stats_base.cpp +++ b/src/util/stats_base.cpp @@ -18,7 +18,7 @@ #include "util/statistics_registry.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/stats_base.h b/src/util/stats_base.h index f7d19624a..e59e6e57c 100644 --- a/src/util/stats_base.h +++ b/src/util/stats_base.h @@ -34,7 +34,7 @@ #define CVC4_USE_STATISTICS false #endif -namespace CVC5 { +namespace cvc5 { /** * The base class for all statistics. @@ -274,6 +274,6 @@ class SizeStat : public Stat const T& d_sized; }; /* class SizeStat */ -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h index 44d4b9e7c..5a8f21fe8 100644 --- a/src/util/stats_histogram.h +++ b/src/util/stats_histogram.h @@ -24,7 +24,7 @@ #include "util/stats_base.h" -namespace CVC5 { +namespace cvc5 { /** * A histogram statistic class for integral types. @@ -123,6 +123,6 @@ class IntegralHistogramStat : public Stat int64_t d_offset; }; /* class IntegralHistogramStat */ -} // namespace CVC5 +} // namespace cvc5 #endif diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp index 6280b79e1..fa513b0b4 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 CVC5 { +namespace cvc5 { template <> void safe_print(int fd, const timer_stat_detail::duration& t) @@ -101,4 +101,4 @@ CodeTimer::~CodeTimer() } } -} // namespace CVC5 +} // namespace cvc5 diff --git a/src/util/stats_timer.h b/src/util/stats_timer.h index 40df52ade..92ea87b59 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 CVC5 { +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 CVC5::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 CVC5 +} // namespace cvc5 #endif diff --git a/src/util/stats_utils.cpp b/src/util/stats_utils.cpp index 2a87ff439..7908e0912 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 CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/stats_utils.h b/src/util/stats_utils.h index d511539ca..001a4cf82 100644 --- a/src/util/stats_utils.h +++ b/src/util/stats_utils.h @@ -23,7 +23,7 @@ #include "cvc4_export.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 #endif diff --git a/src/util/string.cpp b/src/util/string.cpp index d1d7fadc2..ec13956f4 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -25,7 +25,7 @@ using namespace std; -namespace CVC5 { +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 CVC5::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 CVC5 +} // namespace cvc5 diff --git a/src/util/string.h b/src/util/string.h index a3e0245aa..6fc23f124 100644 --- a/src/util/string.h +++ b/src/util/string.h @@ -23,7 +23,7 @@ #include "util/rational.h" -namespace CVC5 { +namespace cvc5 { /** The CVC4 string class * @@ -46,7 +46,7 @@ class String static inline unsigned num_codes() { return 196608; } /** constructors for String * - * Internally, a CVC5::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 - * CVC5::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 - * CVC5::String( s ).toString() = s. + * cvc5::String( s ).toString() = s. */ std::string toString(bool useEscSequences = false) const; /* toWString @@ -265,7 +265,7 @@ namespace strings { struct StringHashFunction { - size_t operator()(const ::CVC5::String& s) const + size_t operator()(const ::cvc5::String& s) const { return std::hash<std::string>()(s.toString()); } @@ -275,6 +275,6 @@ struct StringHashFunction std::ostream& operator<<(std::ostream& os, const String& s); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UTIL__STRING_H */ diff --git a/src/util/tuple.h b/src/util/tuple.h index 571bfe797..5a3693691 100644 --- a/src/util/tuple.h +++ b/src/util/tuple.h @@ -23,7 +23,7 @@ #include <vector> #include <utility> -namespace CVC5 { +namespace cvc5 { class TupleUpdate { @@ -49,6 +49,6 @@ inline std::ostream& operator<<(std::ostream& out, const TupleUpdate& t) { return out << "[" << t.getIndex() << "]"; } -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__TUPLE_H */ diff --git a/src/util/unsafe_interrupt_exception.h b/src/util/unsafe_interrupt_exception.h index 31fe26577..39817620d 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 CVC5 { +namespace cvc5 { -class CVC4_EXPORT UnsafeInterruptException : public CVC5::Exception +class CVC4_EXPORT UnsafeInterruptException : public cvc5::Exception { public: UnsafeInterruptException() : @@ -40,6 +40,6 @@ class CVC4_EXPORT UnsafeInterruptException : public CVC5::Exception } }; /* class UnsafeInterruptException */ -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UNSAFE_INTERRUPT_EXCEPTION_H */ diff --git a/src/util/utility.cpp b/src/util/utility.cpp index 480b68ff2..b07f046bf 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -22,7 +22,7 @@ #include "base/check.h" -namespace CVC5 { +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 CVC5 +} // namespace cvc5 diff --git a/src/util/utility.h b/src/util/utility.h index 006f2072c..133e51025 100644 --- a/src/util/utility.h +++ b/src/util/utility.h @@ -24,7 +24,7 @@ #include <memory> #include <string> -namespace CVC5 { +namespace cvc5 { /** * Using std::find_if(), finds the first iterator in [first,last) @@ -77,6 +77,6 @@ void container_to_stream(std::ostream& out, */ std::unique_ptr<std::fstream> openTmpFile(std::string* pattern); -} // namespace CVC5 +} // namespace cvc5 #endif /* CVC4__UTILITY_H */ |