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 077c260f652e3ad4283d4aee44aea7ee7757f057..fd35b889f274b158e8bbb4e7e926c6681305a9b6 100644 (file)
--- 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 d6ded7c7be121404d27617f8dacf011d20b8c2a1..0181db7dcf8849a0e022dd77d2b9ad418591fd06 100644 (file)
--- 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 <poly/polyxx.h>
+#endif
 
 #include <limits>
 
@@ -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<long>& coefficients,
@@ -71,8 +80,12 @@ RealAlgebraicNumber::RealAlgebraicNumber(const std::vector<long>& 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<Rational>& 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 d75bd1836d1f9614f2e7617c15a03de9621446ad..14b755bd75c7362db4c2ce4f624a70ebd2a81d72 100644 (file)
--- a/src/util/real_algebraic_number_poly_imp.h
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -20,7 +20,9 @@
 
 #include <vector>
 
+#ifdef CVC5_POLY_IMP
 #include <poly/polyxx.h>
+#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. */