From: Gereon Kremer Date: Wed, 12 Jan 2022 18:59:29 +0000 (-0800) Subject: Always enable RAN, but disable its implementation without poly (#7910) X-Git-Tag: cvc5-1.0.0~558 X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=c9daef3594dec48693ede0c13e7fc9804835ef14;p=cvc5.git Always enable RAN, but disable its implementation without poly (#7910) This PR makes sure that the RealAlgebraicNumber class is always visible, but its implementation is only enabled when libpoly is available. This allows us to use this class in more places of cvc5. --- diff --git a/src/util/real_algebraic_number.h.in b/src/util/real_algebraic_number.h.in index 077c260f6..fd35b889f 100644 --- a/src/util/real_algebraic_number.h.in +++ b/src/util/real_algebraic_number.h.in @@ -19,6 +19,4 @@ # define CVC5_POLY_IMP #endif /* @CVC5_USE_POLY_IMP@ */ -#ifdef CVC5_POLY_IMP -# include "util/real_algebraic_number_poly_imp.h" -#endif /* CVC5_POLY_IMP */ +#include "util/real_algebraic_number_poly_imp.h" diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp index d6ded7c7b..0181db7dc 100644 --- a/src/util/real_algebraic_number_poly_imp.cpp +++ b/src/util/real_algebraic_number_poly_imp.cpp @@ -16,11 +16,9 @@ #include "base/cvc5config.h" #include "util/real_algebraic_number.h" -#ifndef CVC5_POLY_IMP // Make sure this comes after base/cvc5config.h -#error "This source should only ever be built if CVC5_POLY_IMP is on!" -#endif /* CVC5_POLY_IMP */ - +#ifdef CVC5_POLY_IMP #include +#endif #include @@ -32,18 +30,26 @@ namespace cvc5 { +#ifdef CVC5_POLY_IMP RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an) : d_value(std::move(an)) { } +#endif RealAlgebraicNumber::RealAlgebraicNumber(const Integer& i) +#ifdef CVC5_POLY_IMP : d_value(poly::DyadicRational(poly_utils::toInteger(i))) +#endif { +#ifndef CVC5_POLY_IMP + RAN_UNREACHABLE; +#endif } RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r) { +#ifdef CVC5_POLY_IMP poly::Rational pr = poly_utils::toRational(r); auto dr = poly_utils::toDyadicRational(r); if (dr) @@ -56,6 +62,9 @@ RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r) poly::UPolynomial({numerator(pr), -denominator(pr)}), poly::DyadicInterval(floor(pr), ceil(pr))); } +#else + RAN_UNREACHABLE; +#endif } RealAlgebraicNumber::RealAlgebraicNumber(const std::vector& coefficients, @@ -71,8 +80,12 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector& coefficients, "constructor based on Integer instead."; } #endif +#ifdef CVC5_POLY_IMP d_value = poly::AlgebraicNumber(poly::UPolynomial(coefficients), poly::DyadicInterval(lower, upper)); +#else + RAN_UNREACHABLE; +#endif } RealAlgebraicNumber::RealAlgebraicNumber( @@ -80,14 +93,17 @@ RealAlgebraicNumber::RealAlgebraicNumber( const Rational& lower, const Rational& upper) { +#ifdef CVC5_POLY_IMP *this = poly_utils::toRanWithRefinement( poly::UPolynomial(poly_utils::toInteger(coefficients)), lower, upper); +#endif } RealAlgebraicNumber::RealAlgebraicNumber( const std::vector& coefficients, const Rational& lower, const Rational& upper) { +#ifdef CVC5_POLY_IMP Integer factor = Integer(1); for (const auto& c : coefficients) { @@ -101,6 +117,9 @@ RealAlgebraicNumber::RealAlgebraicNumber( } *this = poly_utils::toRanWithRefinement( poly::UPolynomial(std::move(coeffs)), lower, upper); +#else + RAN_UNREACHABLE; +#endif } bool RealAlgebraicNumber::isRational() const @@ -124,52 +143,107 @@ Rational RealAlgebraicNumber::toRational() const 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) @@ -186,25 +260,57 @@ RealAlgebraicNumber operator/(const RealAlgebraicNumber& 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; } RealAlgebraicNumber& operator*=(RealAlgebraicNumber& lhs, const RealAlgebraicNumber& rhs) { +#ifdef CVC5_POLY_IMP lhs.getValue() = lhs.getValue() * rhs.getValue(); +#else + RAN_UNREACHABLE; +#endif return lhs; } -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()); } +int sgn(const RealAlgebraicNumber& ran) { +#ifdef CVC5_POLY_IMP + return sgn(ran.getValue()); +#else + RAN_UNREACHABLE; + return ran; +#endif +} +bool isZero(const RealAlgebraicNumber& ran) { +#ifdef CVC5_POLY_IMP + return is_zero(ran.getValue()); +#else + return ran; +#endif +} +bool isOne(const RealAlgebraicNumber& ran) { +#ifdef CVC5_POLY_IMP + return is_one(ran.getValue()); +#else + RAN_UNREACHABLE; + return ran; +#endif +} RealAlgebraicNumber inverse(const RealAlgebraicNumber& ran) { #ifdef CVC5_POLY_IMP diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h index d75bd1836..14b755bd7 100644 --- a/src/util/real_algebraic_number_poly_imp.h +++ b/src/util/real_algebraic_number_poly_imp.h @@ -20,7 +20,9 @@ #include +#ifdef CVC5_POLY_IMP #include +#endif #include "util/integer.h" #include "util/rational.h" @@ -44,8 +46,10 @@ class RealAlgebraicNumber public: /** Construct as zero. */ RealAlgebraicNumber() = default; +#ifdef CVC5_POLY_IMP /** Move from a poly::AlgebraicNumber type. */ RealAlgebraicNumber(poly::AlgebraicNumber&& an); +#endif /** Copy from an Integer. */ RealAlgebraicNumber(const Integer& i); /** Copy from a Rational. */ @@ -89,10 +93,12 @@ class RealAlgebraicNumber /** Move assignment. */ RealAlgebraicNumber& operator=(RealAlgebraicNumber&& ran) = default; +#ifdef CVC5_POLY_IMP /** Get the internal value as a const reference. */ const poly::AlgebraicNumber& getValue() const { return d_value; } /** Get the internal value as a non-const reference. */ poly::AlgebraicNumber& getValue() { return d_value; } +#endif /** * Check if this real algebraic number is actually rational. @@ -112,7 +118,9 @@ class RealAlgebraicNumber /** * Stores the actual real algebraic number. */ +#ifdef CVC5_POLY_IMP poly::AlgebraicNumber d_value; +#endif }; /* class RealAlgebraicNumber */ /** Stream a real algebraic number to an output stream. */