diff options
Diffstat (limited to 'src/util')
32 files changed, 188 insertions, 188 deletions
diff --git a/src/util/CMakeLists.txt b/src/util/CMakeLists.txt index 4bc6da1ae..015a484d1 100644 --- a/src/util/CMakeLists.txt +++ b/src/util/CMakeLists.txt @@ -85,14 +85,14 @@ libcvc4_add_sources( utility.h ) -if(CVC4_USE_CLN_IMP) +if(CVC5_USE_CLN_IMP) libcvc4_add_sources(rational_cln_imp.cpp integer_cln_imp.cpp) endif() -if(CVC4_USE_GMP_IMP) +if(CVC5_USE_GMP_IMP) libcvc4_add_sources(rational_gmp_imp.cpp integer_gmp_imp.cpp) endif() -if(CVC4_USE_POLY_IMP) +if(CVC5_USE_POLY_IMP) libcvc4_add_sources(real_algebraic_number_poly_imp.cpp real_algebraic_number_poly_imp.h) endif() diff --git a/src/util/floatingpoint.cpp b/src/util/floatingpoint.cpp index a9d404103..b6fa79e84 100644 --- a/src/util/floatingpoint.cpp +++ b/src/util/floatingpoint.cpp @@ -435,7 +435,7 @@ FloatingPoint::PartialRational FloatingPoint::convertToRational(void) const // unsigned int is not smaller than uint32_t static_assert(sizeof(unsigned int) >= sizeof(uint32_t), "Conversion float -> real could loose data"); -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS // Note that multipling by 2^n requires n bits of space (worst case) // so, in effect, these tests limit us to cases where the resultant // number requires up to 2^32 bits = 512 megabyte to represent. diff --git a/src/util/floatingpoint_literal_symfpu.cpp b/src/util/floatingpoint_literal_symfpu.cpp index 011bce16d..f6bb9d541 100644 --- a/src/util/floatingpoint_literal_symfpu.cpp +++ b/src/util/floatingpoint_literal_symfpu.cpp @@ -15,7 +15,7 @@ #include "base/check.h" -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU #include "symfpu/core/add.h" #include "symfpu/core/classify.h" #include "symfpu/core/compare.h" @@ -34,10 +34,10 @@ /* -------------------------------------------------------------------------- */ -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU namespace symfpu { -#define CVC4_LIT_ITE_DFN(T) \ +#define CVC5_LIT_ITE_DFN(T) \ template <> \ struct ite<::cvc5::symfpuLiteral::Cvc5Prop, T> \ { \ @@ -49,12 +49,12 @@ 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); +CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::rm); +CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::prop); +CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::sbv); +CVC5_LIT_ITE_DFN(::cvc5::symfpuLiteral::traits::ubv); -#undef CVC4_LIT_ITE_DFN +#undef CVC5_LIT_ITE_DFN } // namespace symfpu #endif @@ -64,7 +64,7 @@ namespace cvc5 { uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::exponentWidth(size); #else unimplemented(); @@ -75,7 +75,7 @@ uint32_t FloatingPointLiteral::getUnpackedExponentWidth(FloatingPointSize& size) uint32_t FloatingPointLiteral::getUnpackedSignificandWidth( FloatingPointSize& size) { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return SymFPUUnpackedFloatLiteral::significandWidth(size); #else unimplemented(); @@ -87,7 +87,7 @@ FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, uint32_t sig_size, const BitVector& bv) : d_fp_size(exp_size, sig_size) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(exp_size, sig_size), bv)) @@ -98,7 +98,7 @@ FloatingPointLiteral::FloatingPointLiteral(uint32_t exp_size, FloatingPointLiteral::FloatingPointLiteral( const FloatingPointSize& size, FloatingPointLiteral::SpecialConstKind kind) : d_fp_size(size) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_symuf(SymFPUUnpackedFloatLiteral::makeNaN(size)) #endif @@ -111,7 +111,7 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::SpecialConstKind kind, bool sign) : d_fp_size(size) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_symuf(kind == FloatingPointLiteral::SpecialConstKind::FPINF ? SymFPUUnpackedFloatLiteral::makeInf(size, sign) @@ -125,7 +125,7 @@ FloatingPointLiteral::FloatingPointLiteral( FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv) : d_fp_size(size) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_symuf(symfpu::unpack<symfpuLiteral::traits>(size, bv)) #endif @@ -137,7 +137,7 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, const BitVector& bv, bool signedBV) : d_fp_size(size) -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU , d_symuf(signedBV ? symfpu::convertSBVToFloat<symfpuLiteral::traits>( symfpuLiteral::Cvc5FPSize(size), @@ -153,7 +153,7 @@ FloatingPointLiteral::FloatingPointLiteral(const FloatingPointSize& size, BitVector FloatingPointLiteral::pack(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU BitVector bv(symfpu::pack<symfpuLiteral::traits>(d_fp_size, d_symuf)); #else unimplemented(); @@ -164,7 +164,7 @@ BitVector FloatingPointLiteral::pack(void) const FloatingPointLiteral FloatingPointLiteral::absolute(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::absolute<symfpuLiteral::traits>(d_fp_size, d_symuf)); #else @@ -175,7 +175,7 @@ FloatingPointLiteral FloatingPointLiteral::absolute(void) const FloatingPointLiteral FloatingPointLiteral::negate(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::negate<symfpuLiteral::traits>(d_fp_size, d_symuf)); #else @@ -187,7 +187,7 @@ FloatingPointLiteral FloatingPointLiteral::negate(void) const FloatingPointLiteral FloatingPointLiteral::add( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( @@ -201,7 +201,7 @@ FloatingPointLiteral FloatingPointLiteral::add( FloatingPointLiteral FloatingPointLiteral::sub( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::add<symfpuLiteral::traits>( @@ -215,7 +215,7 @@ FloatingPointLiteral FloatingPointLiteral::sub( FloatingPointLiteral FloatingPointLiteral::mult( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::multiply<symfpuLiteral::traits>( @@ -229,7 +229,7 @@ FloatingPointLiteral FloatingPointLiteral::mult( FloatingPointLiteral FloatingPointLiteral::div( const RoundingMode& rm, const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::divide<symfpuLiteral::traits>( @@ -245,7 +245,7 @@ FloatingPointLiteral FloatingPointLiteral::fma( const FloatingPointLiteral& arg1, const FloatingPointLiteral& arg2) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg1.d_fp_size); Assert(d_fp_size == arg2.d_fp_size); return FloatingPointLiteral( @@ -260,7 +260,7 @@ FloatingPointLiteral FloatingPointLiteral::fma( FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::sqrt<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); #else @@ -271,7 +271,7 @@ FloatingPointLiteral FloatingPointLiteral::sqrt(const RoundingMode& rm) const FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( d_fp_size, symfpu::roundToIntegral<symfpuLiteral::traits>(d_fp_size, rm, d_symuf)); @@ -284,7 +284,7 @@ FloatingPointLiteral FloatingPointLiteral::rti(const RoundingMode& rm) const FloatingPointLiteral FloatingPointLiteral::rem( const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral(d_fp_size, symfpu::remainder<symfpuLiteral::traits>( @@ -298,7 +298,7 @@ FloatingPointLiteral FloatingPointLiteral::rem( FloatingPointLiteral FloatingPointLiteral::maxTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, @@ -313,7 +313,7 @@ FloatingPointLiteral FloatingPointLiteral::maxTotal( FloatingPointLiteral FloatingPointLiteral::minTotal( const FloatingPointLiteral& arg, bool zeroCaseLeft) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return FloatingPointLiteral( d_fp_size, @@ -327,7 +327,7 @@ FloatingPointLiteral FloatingPointLiteral::minTotal( bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return ((d_fp_size == fp.d_fp_size) && symfpu::smtlibEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, fp.d_symuf)); @@ -339,7 +339,7 @@ bool FloatingPointLiteral::operator==(const FloatingPointLiteral& fp) const bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThanOrEqual<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); @@ -351,7 +351,7 @@ bool FloatingPointLiteral::operator<=(const FloatingPointLiteral& arg) const bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU Assert(d_fp_size == arg.d_fp_size); return symfpu::lessThan<symfpuLiteral::traits>( d_fp_size, d_symuf, arg.d_symuf); @@ -363,7 +363,7 @@ bool FloatingPointLiteral::operator<(const FloatingPointLiteral& arg) const BitVector FloatingPointLiteral::getExponent() const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return d_symuf.exponent; #else unimplemented(); @@ -374,7 +374,7 @@ BitVector FloatingPointLiteral::getExponent() const BitVector FloatingPointLiteral::getSignificand() const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return d_symuf.significand; #else unimplemented(); @@ -385,7 +385,7 @@ BitVector FloatingPointLiteral::getSignificand() const bool FloatingPointLiteral::getSign() const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return d_symuf.sign; #else unimplemented(); @@ -396,7 +396,7 @@ bool FloatingPointLiteral::getSign() const bool FloatingPointLiteral::isNormal(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isNormal<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -406,7 +406,7 @@ bool FloatingPointLiteral::isNormal(void) const bool FloatingPointLiteral::isSubnormal(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isSubnormal<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -416,7 +416,7 @@ bool FloatingPointLiteral::isSubnormal(void) const bool FloatingPointLiteral::isZero(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isZero<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -426,7 +426,7 @@ bool FloatingPointLiteral::isZero(void) const bool FloatingPointLiteral::isInfinite(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isInfinite<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -436,7 +436,7 @@ bool FloatingPointLiteral::isInfinite(void) const bool FloatingPointLiteral::isNaN(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isNaN<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -446,7 +446,7 @@ bool FloatingPointLiteral::isNaN(void) const bool FloatingPointLiteral::isNegative(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isNegative<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -456,7 +456,7 @@ bool FloatingPointLiteral::isNegative(void) const bool FloatingPointLiteral::isPositive(void) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::isPositive<symfpuLiteral::traits>(d_fp_size, d_symuf); #else unimplemented(); @@ -467,7 +467,7 @@ bool FloatingPointLiteral::isPositive(void) const FloatingPointLiteral FloatingPointLiteral::convert( const FloatingPointSize& target, const RoundingMode& rm) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return FloatingPointLiteral( target, symfpu::convertFloatToFloat<symfpuLiteral::traits>( @@ -482,7 +482,7 @@ BitVector FloatingPointLiteral::convertToSBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToSBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); #else @@ -495,7 +495,7 @@ BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width, const RoundingMode& rm, BitVector undefinedCase) const { -#ifdef CVC4_USE_SYMFPU +#ifdef CVC5_USE_SYMFPU return symfpu::convertFloatToUBV<symfpuLiteral::traits>( d_fp_size, rm, d_symuf, width, undefinedCase); #else @@ -504,7 +504,7 @@ BitVector FloatingPointLiteral::convertToUBVTotal(BitVectorSize width, #endif } -#ifndef CVC4_USE_SYMFPU +#ifndef CVC5_USE_SYMFPU void FloatingPointLiteral::unimplemented(void) { Unimplemented() << "no concrete implementation of FloatingPointLiteral"; diff --git a/src/util/floatingpoint_literal_symfpu.h.in b/src/util/floatingpoint_literal_symfpu.h.in index 8ef62c63b..e773c1f97 100644 --- a/src/util/floatingpoint_literal_symfpu.h.in +++ b/src/util/floatingpoint_literal_symfpu.h.in @@ -28,7 +28,7 @@ namespace cvc5 { // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on using SymFPUUnpackedFloatLiteral = ::symfpu::unpackedFloat<symfpuLiteral::traits>; @@ -65,7 +65,7 @@ class FloatingPointLiteral static uint32_t getUnpackedSignificandWidth(FloatingPointSize& size); // clang-format off -#if !@CVC4_USE_SYMFPU@ +#if !@CVC5_USE_SYMFPU@ // clang-format on /** Catch-all for unimplemented functions. */ static void unimplemented(void); @@ -197,7 +197,7 @@ class FloatingPointLiteral const RoundingMode& rm, BitVector undefinedCase) const; // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on /** Return wrapped floating-point literal. */ const SymFPUUnpackedFloatLiteral& getSymUF() const { return d_symuf; } @@ -224,7 +224,7 @@ class FloatingPointLiteral const BitVector& sig) : d_fp_size(size) // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on , d_symuf(SymFPUUnpackedFloatLiteral(sign, exp, sig)) @@ -233,7 +233,7 @@ class FloatingPointLiteral } // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on /** Create a FP literal from a symFPU unpacked float. */ @@ -245,7 +245,7 @@ class FloatingPointLiteral /** The floating-point size of this floating-point literal. */ FloatingPointSize d_fp_size; // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on /** The actual floating-point value, a SymFPU unpackedFloat. */ SymFPUUnpackedFloatLiteral d_symuf; diff --git a/src/util/floatingpoint_literal_symfpu_traits.cpp b/src/util/floatingpoint_literal_symfpu_traits.cpp index fe814317d..d1cd7621f 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.cpp +++ b/src/util/floatingpoint_literal_symfpu_traits.cpp @@ -12,7 +12,7 @@ ** \brief SymFPU glue code for floating-point values. **/ -#if CVC4_USE_SYMFPU +#if CVC5_USE_SYMFPU #include "util/floatingpoint_literal_symfpu_traits.h" diff --git a/src/util/floatingpoint_literal_symfpu_traits.h.in b/src/util/floatingpoint_literal_symfpu_traits.h.in index 19abc009e..2c2504ab7 100644 --- a/src/util/floatingpoint_literal_symfpu_traits.h.in +++ b/src/util/floatingpoint_literal_symfpu_traits.h.in @@ -27,7 +27,7 @@ #define CVC5__UTIL__FLOATINGPOINT_LITERAL_SYMFPU_TRAITS_H // clang-format off -#if @CVC4_USE_SYMFPU@ +#if @CVC5_USE_SYMFPU@ // clang-format on #include "util/bitvector.h" diff --git a/src/util/hash.h b/src/util/hash.h index d21188f2c..a7cb214b0 100644 --- a/src/util/hash.h +++ b/src/util/hash.h @@ -25,7 +25,7 @@ namespace std { -#ifdef CVC4_NEED_HASH_UINT64_T +#ifdef CVC5_NEED_HASH_UINT64_T // on some versions and architectures of GNU C++, we need a // specialization of hash for 64-bit values template <> @@ -34,7 +34,7 @@ struct hash<uint64_t> { return v; } };/* struct hash<uint64_t> */ -#endif /* CVC4_NEED_HASH_UINT64_T */ +#endif /* CVC5_NEED_HASH_UINT64_T */ }/* std namespace */ diff --git a/src/util/integer.h.in b/src/util/integer.h.in index dbf1af22a..aabc8109d 100644 --- a/src/util/integer.h.in +++ b/src/util/integer.h.in @@ -16,27 +16,27 @@ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h -#if @CVC4_NEED_INT64_T_OVERLOADS@ -# define CVC4_NEED_INT64_T_OVERLOADS +#if @CVC5_NEED_INT64_T_OVERLOADS@ +# define CVC5_NEED_INT64_T_OVERLOADS #endif -#if /* use CLN */ @CVC4_USE_CLN_IMP@ -# define CVC4_CLN_IMP -#endif /* @CVC4_USE_CLN_IMP@ */ -#if /* use GMP */ @CVC4_USE_GMP_IMP@ -# define CVC4_GMP_IMP -#endif /* @CVC4_USE_GMP_IMP@ */ +#if /* use CLN */ @CVC5_USE_CLN_IMP@ +# define CVC5_CLN_IMP +#endif /* @CVC5_USE_CLN_IMP@ */ +#if /* use GMP */ @CVC5_USE_GMP_IMP@ +# define CVC5_GMP_IMP +#endif /* @CVC5_USE_GMP_IMP@ */ -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP # include "util/integer_cln_imp.h" # if SWIG %include "util/integer_cln_imp.h" # endif /* SWIG */ -#endif /* CVC4_CLN_IMP */ +#endif /* CVC5_CLN_IMP */ -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP # include "util/integer_gmp_imp.h" # if SWIG %include "util/integer_gmp_imp.h" # endif /* SWIG */ -#endif /* CVC4_GMP_IMP */ +#endif /* CVC5_GMP_IMP */ diff --git a/src/util/integer_cln_imp.cpp b/src/util/integer_cln_imp.cpp index 3b70a98bf..c41b17fd6 100644 --- a/src/util/integer_cln_imp.cpp +++ b/src/util/integer_cln_imp.cpp @@ -20,9 +20,9 @@ #include "cvc4autoconfig.h" #include "util/integer.h" -#ifndef CVC4_CLN_IMP -#error "This source should only ever be built if CVC4_CLN_IMP is on !" -#endif /* CVC4_CLN_IMP */ +#ifndef CVC5_CLN_IMP +#error "This source should only ever be built if CVC5_CLN_IMP is on !" +#endif /* CVC5_CLN_IMP */ #include "base/check.h" diff --git a/src/util/integer_cln_imp.h b/src/util/integer_cln_imp.h index c3a9434b9..fdc55871d 100644 --- a/src/util/integer_cln_imp.h +++ b/src/util/integer_cln_imp.h @@ -75,10 +75,10 @@ class CVC4_EXPORT Integer Integer(signed long int z) : d_value(z) {} Integer(unsigned long int z) : d_value(z) {} -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Integer(int64_t z) : d_value(static_cast<long>(z)) {} Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** Destructor. */ ~Integer() {} diff --git a/src/util/integer_gmp_imp.cpp b/src/util/integer_gmp_imp.cpp index 399b7bbbe..a7ba33bb0 100644 --- a/src/util/integer_gmp_imp.cpp +++ b/src/util/integer_gmp_imp.cpp @@ -25,8 +25,8 @@ #include "base/check.h" #include "util/rational.h" -#ifndef CVC4_GMP_IMP -# error "This source should only ever be built if CVC4_GMP_IMP is on !" +#ifndef CVC5_GMP_IMP +#error "This source should only ever be built if CVC5_GMP_IMP is on !" #endif using namespace std; diff --git a/src/util/integer_gmp_imp.h b/src/util/integer_gmp_imp.h index 077babe17..a5cc793ce 100644 --- a/src/util/integer_gmp_imp.h +++ b/src/util/integer_gmp_imp.h @@ -60,10 +60,10 @@ class CVC4_EXPORT Integer Integer(signed long int z) : d_value(z) {} Integer(unsigned long int z) : d_value(z) {} -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Integer(int64_t z) : d_value(static_cast<long>(z)) {} Integer(uint64_t z) : d_value(static_cast<unsigned long>(z)) {} -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** Destructor. */ ~Integer() {} diff --git a/src/util/poly_util.cpp b/src/util/poly_util.cpp index 7cb8baae3..50f42140b 100644 --- a/src/util/poly_util.cpp +++ b/src/util/poly_util.cpp @@ -22,7 +22,7 @@ #include "poly_util.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> @@ -58,10 +58,10 @@ To cast_by_string(const From& f) Integer toInteger(const poly::Integer& i) { const mpz_class& gi = *poly::detail::cast_to_gmp(&i); -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP return Integer(gi); #endif -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP if (std::numeric_limits<long>::min() <= gi && gi <= std::numeric_limits<long>::max()) { @@ -76,10 +76,10 @@ Integer toInteger(const poly::Integer& i) Rational toRational(const poly::Integer& i) { return Rational(toInteger(i)); } Rational toRational(const poly::Rational& r) { -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP return Rational(*poly::detail::cast_to_gmp(&r)); #endif -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP return Rational(toInteger(numerator(r)), toInteger(denominator(r))); #endif } @@ -132,10 +132,10 @@ Rational toRationalBelow(const poly::Value& v) poly::Integer toInteger(const Integer& i) { -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP return poly::Integer(i.getValue()); #endif -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP if (std::numeric_limits<long>::min() <= i.getValue() && i.getValue() <= std::numeric_limits<long>::max()) { @@ -155,10 +155,10 @@ std::vector<poly::Integer> toInteger(const std::vector<Integer>& vi) } poly::Rational toRational(const Rational& r) { -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP return poly::Rational(r.getValue()); #endif -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP return poly::Rational(toInteger(r.getNumerator()), toInteger(r.getDenominator())); #endif diff --git a/src/util/poly_util.h b/src/util/poly_util.h index 2ab44e120..5ab96b5b1 100644 --- a/src/util/poly_util.h +++ b/src/util/poly_util.h @@ -32,7 +32,7 @@ #include "util/rational.h" #include "util/real_algebraic_number.h" -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP #include <poly/polyxx.h> diff --git a/src/util/rational.h.in b/src/util/rational.h.in index ff49ae638..b05aefbd3 100644 --- a/src/util/rational.h.in +++ b/src/util/rational.h.in @@ -16,27 +16,27 @@ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h -#if @CVC4_NEED_INT64_T_OVERLOADS@ -# define CVC4_NEED_INT64_T_OVERLOADS +#if @CVC5_NEED_INT64_T_OVERLOADS@ +# define CVC5_NEED_INT64_T_OVERLOADS #endif -#if /* use CLN */ @CVC4_USE_CLN_IMP@ -# define CVC4_CLN_IMP -#endif /* @CVC4_USE_CLN_IMP@ */ -#if /* use GMP */ @CVC4_USE_GMP_IMP@ -# define CVC4_GMP_IMP -#endif /* @CVC4_USE_GMP_IMP@ */ +#if /* use CLN */ @CVC5_USE_CLN_IMP@ +# define CVC5_CLN_IMP +#endif /* @CVC5_USE_CLN_IMP@ */ +#if /* use GMP */ @CVC5_USE_GMP_IMP@ +# define CVC5_GMP_IMP +#endif /* @CVC5_USE_GMP_IMP@ */ -#ifdef CVC4_CLN_IMP +#ifdef CVC5_CLN_IMP # include "util/rational_cln_imp.h" # if SWIG %include "util/rational_cln_imp.h" # endif /* SWIG */ -#endif /* CVC4_CLN_IMP */ +#endif /* CVC5_CLN_IMP */ -#ifdef CVC4_GMP_IMP +#ifdef CVC5_GMP_IMP # include "util/rational_gmp_imp.h" # if SWIG %include "util/rational_gmp_imp.h" # endif /* SWIG */ -#endif /* CVC4_GMP_IMP */ +#endif /* CVC5_GMP_IMP */ diff --git a/src/util/rational_cln_imp.cpp b/src/util/rational_cln_imp.cpp index b12fd8d28..5d71e63f4 100644 --- a/src/util/rational_cln_imp.cpp +++ b/src/util/rational_cln_imp.cpp @@ -20,9 +20,9 @@ #include "cvc4autoconfig.h" -#ifndef CVC4_CLN_IMP -# error "This source should only ever be built if CVC4_CLN_IMP is on !" -#endif /* CVC4_CLN_IMP */ +#ifndef CVC5_CLN_IMP +#error "This source should only ever be built if CVC5_CLN_IMP is on !" +#endif /* CVC5_CLN_IMP */ #include "base/check.h" diff --git a/src/util/rational_cln_imp.h b/src/util/rational_cln_imp.h index 992218ed0..4614620d5 100644 --- a/src/util/rational_cln_imp.h +++ b/src/util/rational_cln_imp.h @@ -130,10 +130,10 @@ class CVC4_EXPORT Rational Rational(signed long int n) : d_value(n) {} Rational(unsigned long int n) : d_value(n) {} -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Rational(int64_t n) : d_value(static_cast<long>(n)) {} Rational(uint64_t n) : d_value(static_cast<unsigned long>(n)) {} -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** * Constructs a canonical Rational from a numerator and denominator. @@ -155,7 +155,7 @@ class CVC4_EXPORT Rational d_value /= cln::cl_I(d); } -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n)) { d_value /= cln::cl_I(d); @@ -164,7 +164,7 @@ class CVC4_EXPORT Rational { d_value /= cln::cl_I(d); } -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ Rational(const Integer& n, const Integer& d) : d_value(n.get_cl_I()) { diff --git a/src/util/rational_gmp_imp.cpp b/src/util/rational_gmp_imp.cpp index 69a2fa2dd..f64bca32f 100644 --- a/src/util/rational_gmp_imp.cpp +++ b/src/util/rational_gmp_imp.cpp @@ -21,9 +21,9 @@ #include "cvc4autoconfig.h" -#ifndef CVC4_GMP_IMP // Make sure this comes after cvc4autoconfig.h -# error "This source should only ever be built if CVC4_GMP_IMP is on !" -#endif /* CVC4_GMP_IMP */ +#ifndef CVC5_GMP_IMP // Make sure this comes after cvc4autoconfig.h +#error "This source should only ever be built if CVC5_GMP_IMP is on !" +#endif /* CVC5_GMP_IMP */ #include "base/check.h" diff --git a/src/util/rational_gmp_imp.h b/src/util/rational_gmp_imp.h index caaa26d1e..1509e3e16 100644 --- a/src/util/rational_gmp_imp.h +++ b/src/util/rational_gmp_imp.h @@ -97,7 +97,7 @@ class CVC4_EXPORT Rational Rational(signed long int n) : d_value(n, 1) { d_value.canonicalize(); } Rational(unsigned long int n) : d_value(n, 1) { d_value.canonicalize(); } -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Rational(int64_t n) : d_value(static_cast<long>(n), 1) { d_value.canonicalize(); @@ -106,7 +106,7 @@ class CVC4_EXPORT Rational { d_value.canonicalize(); } -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ /** * Constructs a canonical Rational from a numerator and denominator. @@ -128,7 +128,7 @@ class CVC4_EXPORT Rational d_value.canonicalize(); } -#ifdef CVC4_NEED_INT64_T_OVERLOADS +#ifdef CVC5_NEED_INT64_T_OVERLOADS Rational(int64_t n, int64_t d) : d_value(static_cast<long>(n), static_cast<long>(d)) { @@ -139,7 +139,7 @@ class CVC4_EXPORT Rational { d_value.canonicalize(); } -#endif /* CVC4_NEED_INT64_T_OVERLOADS */ +#endif /* CVC5_NEED_INT64_T_OVERLOADS */ Rational(const Integer& n, const Integer& d) : d_value(n.get_mpz(), d.get_mpz()) diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in index 4a8982e0b..910b357d1 100644 --- a/src/util/real_algebraic_number.h.in +++ b/src/util/real_algebraic_number.h.in @@ -16,10 +16,10 @@ // these gestures are used to avoid a public header dependence on cvc4autoconfig.h -#if /* use libpoly */ @CVC4_USE_POLY_IMP@ -# define CVC4_POLY_IMP -#endif /* @CVC4_USE_POLY_IMP@ */ +#if /* use libpoly */ @CVC5_USE_POLY_IMP@ +# define CVC5_POLY_IMP +#endif /* @CVC5_USE_POLY_IMP@ */ -#ifdef CVC4_POLY_IMP +#ifdef CVC5_POLY_IMP # include "util/real_algebraic_number_poly_imp.h" -#endif /* CVC4_POLY_IMP */ +#endif /* CVC5_POLY_IMP */ diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index 5c7dd9468..013fc2a4a 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -17,9 +17,9 @@ #include "cvc4autoconfig.h" #include "util/real_algebraic_number.h" -#ifndef CVC4_POLY_IMP // Make sure this comes after cvc4autoconfig.h -#error "This source should only ever be built if CVC4_POLY_IMP is on!" -#endif /* CVC4_POLY_IMP */ +#ifndef CVC5_POLY_IMP // Make sure this comes after cvc4autoconfig.h +#error "This source should only ever be built if CVC5_POLY_IMP is on!" +#endif /* CVC5_POLY_IMP */ #include <poly/polyxx.h> @@ -60,7 +60,7 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector<long>& coefficients, long lower, long upper) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (long c : coefficients) { Assert(std::numeric_limits<std::int32_t>::min() <= c diff --git a/src/util/roundingmode.h b/src/util/roundingmode.h index 482e28781..871bece21 100644 --- a/src/util/roundingmode.h +++ b/src/util/roundingmode.h @@ -20,7 +20,7 @@ namespace cvc5 { -#define CVC4_NUM_ROUNDING_MODES 5 +#define CVC5_NUM_ROUNDING_MODES 5 /** * A concrete instance of the rounding mode sort diff --git a/src/util/sampler.cpp b/src/util/sampler.cpp index 5351a6175..a5ed5bbb4 100644 --- a/src/util/sampler.cpp +++ b/src/util/sampler.cpp @@ -76,27 +76,27 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) // +/- inf // sign = x, exp = 11...11, sig = 00...00 - case 1: sign = one; CVC4_FALLTHROUGH; + case 1: sign = one; CVC5_FALLTHROUGH; case 2: exp = BitVector::mkOnes(e); break; // +/- zero // sign = x, exp = 00...00, sig = 00...00 - case 3: sign = one; CVC4_FALLTHROUGH; + case 3: sign = one; CVC5_FALLTHROUGH; case 4: break; // +/- max subnormal // sign = x, exp = 00...00, sig = 11...11 - case 5: sign = one; CVC4_FALLTHROUGH; + case 5: sign = one; CVC5_FALLTHROUGH; case 6: sig = BitVector::mkOnes(s - 1); break; // +/- min subnormal // sign = x, exp = 00...00, sig = 00...01 - case 7: sign = one; CVC4_FALLTHROUGH; + case 7: sign = one; CVC5_FALLTHROUGH; case 8: sig = BitVector(s - 1, static_cast<unsigned int>(1)); break; // +/- max normal // sign = x, exp = 11...10, sig = 11...11 - case 9: sign = one; CVC4_FALLTHROUGH; + case 9: sign = one; CVC5_FALLTHROUGH; case 10: exp = BitVector::mkOnes(e) - BitVector(e, static_cast<unsigned int>(1)); sig = BitVector::mkOnes(s - 1); @@ -104,7 +104,7 @@ FloatingPoint Sampler::pickFpBiased(unsigned e, unsigned s) // +/- min normal // sign = x, exp = 00...01, sig = 00...00 - case 11: sign = one; CVC4_FALLTHROUGH; + case 11: sign = one; CVC5_FALLTHROUGH; case 12: exp = BitVector(e, static_cast<unsigned int>(1)); break; default: Unreachable(); diff --git a/src/util/statistics.cpp b/src/util/statistics.cpp index 494a70e6c..7053e9ea0 100644 --- a/src/util/statistics.cpp +++ b/src/util/statistics.cpp @@ -95,7 +95,7 @@ StatisticsBase::const_iterator StatisticsBase::end() const { } void StatisticsBase::flushInformation(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON for(StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { @@ -104,11 +104,11 @@ void StatisticsBase::flushInformation(std::ostream &out) const { s->flushInformation(out); out << std::endl; } -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } void StatisticsBase::safeFlushInformation(int fd) const { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON for (StatSet::iterator i = d_stats.begin(); i != d_stats.end(); ++i) { Stat* s = *i; safe_print(fd, s->getName()); @@ -116,7 +116,7 @@ void StatisticsBase::safeFlushInformation(int fd) const { s->safeFlushInformation(fd); safe_print(fd, "\n"); } -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } SExpr StatisticsBase::getStatistic(std::string name) const { diff --git a/src/util/statistics_registry.cpp b/src/util/statistics_registry.cpp index f9e05e68f..094bf9709 100644 --- a/src/util/statistics_registry.cpp +++ b/src/util/statistics_registry.cpp @@ -24,10 +24,10 @@ #include "lib/clock_gettime.h" #include "util/ostream_util.h" -#ifdef CVC4_STATISTICS_ON -# define CVC4_USE_STATISTICS true +#ifdef CVC5_STATISTICS_ON +#define CVC5_USE_STATISTICS true #else -# define CVC4_USE_STATISTICS false +#define CVC5_USE_STATISTICS false #endif @@ -38,42 +38,42 @@ namespace cvc5 { void StatisticsRegistry::registerStat(Stat* s) { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON PrettyCheckArgument( d_stats.find(s) == d_stats.end(), s, "Statistic `%s' is already registered with this registry.", s->getName().c_str()); d_stats.insert(s); -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ }/* StatisticsRegistry::registerStat_() */ void StatisticsRegistry::unregisterStat(Stat* s) { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON AlwaysAssert(s != nullptr); AlwaysAssert(d_stats.erase(s) > 0) << "Statistic `" << s->getName() << "' was not registered with this registry."; -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } /* StatisticsRegistry::unregisterStat() */ void StatisticsRegistry::flushStat(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON flushInformation(out); -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } void StatisticsRegistry::flushInformation(std::ostream &out) const { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON this->StatisticsBase::flushInformation(out); -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } void StatisticsRegistry::safeFlushInformation(int fd) const { -#ifdef CVC4_STATISTICS_ON +#ifdef CVC5_STATISTICS_ON this->StatisticsBase::safeFlushInformation(fd); -#endif /* CVC4_STATISTICS_ON */ +#endif /* CVC5_STATISTICS_ON */ } RegisterStatistic::RegisterStatistic(StatisticsRegistry* reg, Stat* stat) diff --git a/src/util/statistics_registry.h b/src/util/statistics_registry.h index cf47bdf2e..e0b0dc177 100644 --- a/src/util/statistics_registry.h +++ b/src/util/statistics_registry.h @@ -33,45 +33,45 @@ /** * On the design of the statistics: - * + * * Stat is the abstract base class for all statistic values. * It stores the name and provides (fully virtual) methods * flushInformation() and safeFlushInformation(). - * + * * BackedStat is an abstract templated base class for statistic values * that store the data themselves. It takes care of printing them already * and derived classes usually only need to provide methods to set the * value. - * - * ReferenceStat holds a reference (conceptually, it is implemented as a + * + * ReferenceStat holds a reference (conceptually, it is implemented as a * const pointer) to some data that is stored outside of the statistic. - * + * * IntStat is a BackedStat<std::int64_t>. - * + * * SizeStat holds a const reference to some container and provides the * size of this container. - * + * * AverageStat is a BackedStat<double>. - * + * * HistogramStat counts instances of some type T. It is implemented as a * std::map<T, std::uint64_t>. - * + * * IntegralHistogramStat is a (conceptual) specialization of HistogramStat - * for types that are (convertible to) integral. This allows to use a + * for types that are (convertible to) integral. This allows to use a * std::vector<std::uint64_t> instead of a std::map. - * + * * TimerStat uses std::chrono to collect timing information. It is * implemented as BackedStat<std::chrono::duration> and provides methods * start() and stop(), accumulating times it was activated. It provides * the convenience class CodeTimer to allow for RAII-style usage. - * - * + * + * * All statistic classes should protect their custom methods using - * if (CVC4_USE_STATISTICS) { ... } + * if (CVC5_USE_STATISTICS) { ... } * Output methods (flushInformation() and safeFlushInformation()) are only * called when statistics are enabled and need no protection. - * - * + * + * * The statistic classes try to implement a consistent interface: * - if we store some generic data, we implement set() * - if we (conceptually) store a set of values, we implement operator<<() @@ -90,10 +90,10 @@ #include <sstream> #include <vector> -#ifdef CVC4_STATISTICS_ON -# define CVC4_USE_STATISTICS true +#ifdef CVC5_STATISTICS_ON +#define CVC5_USE_STATISTICS true #else -# define CVC4_USE_STATISTICS false +#define CVC5_USE_STATISTICS false #endif #include "base/exception.h" diff --git a/src/util/stats_base.cpp b/src/util/stats_base.cpp index 3ae50cd51..5d34b43f2 100644 --- a/src/util/stats_base.cpp +++ b/src/util/stats_base.cpp @@ -22,7 +22,7 @@ namespace cvc5 { Stat::Stat(const std::string& name) : d_name(name) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { CheckArgument(d_name.find(", ") == std::string::npos, name, @@ -38,7 +38,7 @@ IntStat::IntStat(const std::string& name, int64_t init) /** Increment the underlying integer statistic. */ IntStat& IntStat::operator++() { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { ++d_data; } @@ -47,7 +47,7 @@ IntStat& IntStat::operator++() /** Increment the underlying integer statistic. */ IntStat& IntStat::operator++(int) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { ++d_data; } @@ -57,7 +57,7 @@ IntStat& IntStat::operator++(int) /** Increment the underlying integer statistic by the given amount. */ IntStat& IntStat::operator+=(int64_t val) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { d_data += val; } @@ -67,7 +67,7 @@ IntStat& IntStat::operator+=(int64_t val) /** Keep the maximum of the current statistic value and the given one. */ void IntStat::maxAssign(int64_t val) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { if (d_data < val) { @@ -79,7 +79,7 @@ void IntStat::maxAssign(int64_t val) /** Keep the minimum of the current statistic value and the given one. */ void IntStat::minAssign(int64_t val) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { if (d_data > val) { @@ -96,7 +96,7 @@ AverageStat::AverageStat(const std::string& name) /** Add an entry to the running-average calculation. */ AverageStat& AverageStat::operator<<(double e) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { ++d_count; d_sum += e; diff --git a/src/util/stats_base.h b/src/util/stats_base.h index 86a9321c0..9d168bad1 100644 --- a/src/util/stats_base.h +++ b/src/util/stats_base.h @@ -28,10 +28,10 @@ #include "util/sexpr.h" #include "util/stats_utils.h" -#ifdef CVC4_STATISTICS_ON -#define CVC4_USE_STATISTICS true +#ifdef CVC5_STATISTICS_ON +#define CVC5_USE_STATISTICS true #else -#define CVC4_USE_STATISTICS false +#define CVC5_USE_STATISTICS false #endif namespace cvc5 { @@ -103,7 +103,7 @@ class BackedStat : public Stat /** Set the underlying data value to the given value. */ void set(const T& t) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { d_data = t; } @@ -164,7 +164,7 @@ class ReferenceStat : public Stat /** Set this reference statistic to refer to the given data cell. */ void set(const T& t) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { d_data = &t; } diff --git a/src/util/stats_histogram.h b/src/util/stats_histogram.h index ba2135b58..e9968dd34 100644 --- a/src/util/stats_histogram.h +++ b/src/util/stats_histogram.h @@ -97,7 +97,7 @@ class IntegralHistogramStat : public Stat IntegralHistogramStat& operator<<(Integral val) { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { int64_t v = static_cast<int64_t>(val); if (d_hist.empty()) diff --git a/src/util/stats_timer.cpp b/src/util/stats_timer.cpp index fa513b0b4..eedb30b4c 100644 --- a/src/util/stats_timer.cpp +++ b/src/util/stats_timer.cpp @@ -33,7 +33,7 @@ void safe_print(int fd, const timer_stat_detail::duration& t) void TimerStat::start() { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { PrettyCheckArgument(!d_running, *this, "timer already running"); d_start = timer_stat_detail::clock::now(); @@ -43,7 +43,7 @@ void TimerStat::start() void TimerStat::stop() { - if (CVC4_USE_STATISTICS) + if (CVC5_USE_STATISTICS) { AlwaysAssert(d_running) << "timer not running"; d_data += timer_stat_detail::clock::now() - d_start; @@ -56,7 +56,7 @@ bool TimerStat::running() const { return d_running; } timer_stat_detail::duration TimerStat::get() const { auto data = d_data; - if (CVC4_USE_STATISTICS && d_running) + if (CVC5_USE_STATISTICS && d_running) { data += timer_stat_detail::clock::now() - d_start; } @@ -66,7 +66,7 @@ timer_stat_detail::duration TimerStat::get() const SExpr TimerStat::getValue() const { auto data = d_data; - if (CVC4_USE_STATISTICS && d_running) + if (CVC5_USE_STATISTICS && d_running) { data += timer_stat_detail::clock::now() - d_start; } diff --git a/src/util/string.cpp b/src/util/string.cpp index ec13956f4..b6f93aa0f 100644 --- a/src/util/string.cpp +++ b/src/util/string.cpp @@ -31,7 +31,7 @@ static_assert(UCHAR_MAX == 255, "Unsigned char is assumed to have 256 values."); String::String(const std::vector<unsigned> &s) : d_str(s) { -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (unsigned u : d_str) { Assert(u < num_codes()); @@ -226,7 +226,7 @@ std::vector<unsigned> String::toInternal(const std::string& s, str.insert(str.end(), nonEscCache.begin(), nonEscCache.end()); } } -#ifdef CVC4_ASSERTIONS +#ifdef CVC5_ASSERTIONS for (unsigned u : str) { Assert(u < num_codes()); diff --git a/src/util/utility.cpp b/src/util/utility.cpp index b07f046bf..cde74c6eb 100644 --- a/src/util/utility.cpp +++ b/src/util/utility.cpp @@ -43,7 +43,7 @@ std::unique_ptr<std::fstream> openTmpFile(std::string* pattern) int r = mkstemp(tmpName); if (r == -1) { - CVC4_FATAL() << "Could not create temporary file " << *pattern; + CVC5_FATAL() << "Could not create temporary file " << *pattern; } std::unique_ptr<std::fstream> tmpStream(new std::fstream(tmpName)); close(r); |