From f0014b7ed0f810cba313aafde9236571625d2927 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Mon, 24 Jan 2022 09:49:02 -0800 Subject: [PATCH] Have RAN fall back to RANs (#7976) Right now, the RealAlgebraicNumber can not be used if libpoly is not available. This makes using it in the arithmetic rewriter incredibly awkward. This PR makes it fall back to a wrapper around Rational if libpoly is disabled, making its usage way easier. --- src/util/real_algebraic_number_poly_imp.cpp | 104 +++----------------- src/util/real_algebraic_number_poly_imp.h | 10 ++ 2 files changed, 24 insertions(+), 90 deletions(-) diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index 0181db7dc..d464f312d 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -40,14 +40,16 @@ RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an) RealAlgebraicNumber::RealAlgebraicNumber(const Integer& i) #ifdef CVC5_POLY_IMP : d_value(poly::DyadicRational(poly_utils::toInteger(i))) +#else + : d_value(i) #endif { -#ifndef CVC5_POLY_IMP - RAN_UNREACHABLE; -#endif } RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r) +#ifndef CVC5_POLY_IMP + : d_value(r) +#endif { #ifdef CVC5_POLY_IMP poly::Rational pr = poly_utils::toRational(r); @@ -62,8 +64,6 @@ RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r) poly::UPolynomial({numerator(pr), -denominator(pr)}), poly::DyadicInterval(floor(pr), ceil(pr))); } -#else - RAN_UNREACHABLE; #endif } @@ -96,6 +96,8 @@ RealAlgebraicNumber::RealAlgebraicNumber( #ifdef CVC5_POLY_IMP *this = poly_utils::toRanWithRefinement( poly::UPolynomial(poly_utils::toInteger(coefficients)), lower, upper); +#else + RAN_UNREACHABLE; #endif } RealAlgebraicNumber::RealAlgebraicNumber( @@ -127,7 +129,6 @@ bool RealAlgebraicNumber::isRational() const #ifdef CVC5_POLY_IMP return poly::is_rational(getValue()); #else - RAN_UNREACHABLE; return true; #endif } @@ -136,155 +137,82 @@ Rational RealAlgebraicNumber::toRational() const #ifdef CVC5_POLY_IMP return poly_utils::toRational(poly::to_rational_approximation(getValue())); #else - RAN_UNREACHABLE; - return Rational(0); + return d_value; #endif } std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran) { -#ifdef CVC5_POLY_IMP return os << ran.getValue(); -#else - RAN_UNREACHABLE; - return os; -#endif } bool operator==(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() == rhs.getValue(); -#else - RAN_UNREACHABLE; - return true; -#endif } bool operator!=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() != rhs.getValue(); -#else - RAN_UNREACHABLE; - return false; -#endif } bool operator<(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() < rhs.getValue(); -#else - RAN_UNREACHABLE; - return false; -#endif } bool operator<=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() <= rhs.getValue(); -#else - RAN_UNREACHABLE; - return true; -#endif } bool operator>(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() > rhs.getValue(); -#else - RAN_UNREACHABLE; - return false; -#endif } bool operator>=(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() >= rhs.getValue(); -#else - RAN_UNREACHABLE; - return true; -#endif } RealAlgebraicNumber operator+(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() + rhs.getValue(); -#else - RAN_UNREACHABLE; - return lhs; -#endif } RealAlgebraicNumber operator-(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() - rhs.getValue(); -#else - RAN_UNREACHABLE; - return lhs; -#endif } RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran) { -#ifdef CVC5_POLY_IMP return -ran.getValue(); -#else - RAN_UNREACHABLE; - return ran; -#endif } RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP return lhs.getValue() * rhs.getValue(); -#else - RAN_UNREACHABLE; - return lhs; -#endif } RealAlgebraicNumber operator/(const RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP Assert(!isZero(rhs)) << "Can not divide by zero"; return lhs.getValue() / rhs.getValue(); -#else - RAN_UNREACHABLE; - return lhs; -#endif } RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP lhs.getValue() = lhs.getValue() + rhs.getValue(); -#else - RAN_UNREACHABLE; -#endif return lhs; } RealAlgebraicNumber& operator-=(RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP lhs.getValue() = lhs.getValue() - rhs.getValue(); -#else - RAN_UNREACHABLE; -#endif return lhs; } RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { -#ifdef CVC5_POLY_IMP lhs.getValue() = lhs.getValue() * rhs.getValue(); -#else - RAN_UNREACHABLE; -#endif return lhs; } @@ -292,33 +220,30 @@ int sgn(const RealAlgebraicNumber& ran) { #ifdef CVC5_POLY_IMP return sgn(ran.getValue()); #else - RAN_UNREACHABLE; - return ran; + return ran.getValue().sgn(); #endif } bool isZero(const RealAlgebraicNumber& ran) { #ifdef CVC5_POLY_IMP return is_zero(ran.getValue()); #else - return ran; + return ran.getValue().isZero(); #endif } bool isOne(const RealAlgebraicNumber& ran) { #ifdef CVC5_POLY_IMP return is_one(ran.getValue()); #else - RAN_UNREACHABLE; - return ran; + return ran.getValue().isOne(); #endif } RealAlgebraicNumber inverse(const RealAlgebraicNumber& ran) { -#ifdef CVC5_POLY_IMP Assert(!isZero(ran)) << "Can not invert zero"; +#ifdef CVC5_POLY_IMP return inverse(ran.getValue()); #else - RAN_UNREACHABLE; - return ran; + return ran.getValue().inverse(); #endif } @@ -331,8 +256,7 @@ size_t hash::operator()( #ifdef CVC5_POLY_IMP return lp_algebraic_number_hash_approx(ran.getValue().get_internal(), 2); #else - RAN_UNREACHABLE; - return 0; + return ran.getValue().hash(); #endif } } // namespace std diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index 14b755bd7..079bbf824 100644 --- a/src/util/real_algebraic_number_poly_imp.h +++ b/src/util/real_algebraic_number_poly_imp.h @@ -40,6 +40,9 @@ namespace cvc5 { * square roots), but no trancendentals (like pi). * Note that the interval representation uses dyadic rationals (denominators are * only powers of two). + * + * If libpoly is not available, this class serves as a wrapper around Rational + * to allow using RealAlgebraicNumber, even if libpoly is not enabled. */ class RealAlgebraicNumber { @@ -98,6 +101,11 @@ class RealAlgebraicNumber const poly::AlgebraicNumber& getValue() const { return d_value; } /** Get the internal value as a non-const reference. */ poly::AlgebraicNumber& getValue() { return d_value; } +#else + /** Get the internal value as a const reference. */ + const Rational& getValue() const { return d_value; } + /** Get the internal value as a non-const reference. */ + Rational& getValue() { return d_value; } #endif /** @@ -120,6 +128,8 @@ class RealAlgebraicNumber */ #ifdef CVC5_POLY_IMP poly::AlgebraicNumber d_value; +#else + Rational d_value; #endif }; /* class RealAlgebraicNumber */ -- 2.30.2