From 2532f336739081a977b9143e60d775337aad7f18 Mon Sep 17 00:00:00 2001
From: Gereon Kremer <gkremer@stanford.edu>
Date: Mon, 10 Jan 2022 13:29:45 -0800
Subject: [PATCH] Add new methods for RealAlgebraicNumber (#7907)

This PR adds some new methods for the RealAlgebraicNumber class: division, computing the (multiplicative) inverse and a specialization of std::hash.
---
 src/util/real_algebraic_number_poly_imp.cpp   | 31 +++++++++++++++++++
 src/util/real_algebraic_number_poly_imp.h     | 21 +++++++++++++
 .../unit/util/real_algebraic_number_black.cpp | 13 +++++++-
 3 files changed, 64 insertions(+), 1 deletion(-)

diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index 58af26193..d92d917dc 100644
--- a/src/util/real_algebraic_number_poly_imp.cpp
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -149,6 +149,16 @@ RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
 {
   return lhs.getValue() * rhs.getValue();
 }
+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
+  return lhs;
+#endif
+}
 
 RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
                                 const RealAlgebraicNumber& rhs)
@@ -172,5 +182,26 @@ RealAlgebraicNumber& operator*=(RealAlgebraicNumber& 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()); }
+RealAlgebraicNumber inverse(const RealAlgebraicNumber& ran)
+{
+#ifdef CVC5_POLY_IMP
+  Assert(!isZero(ran)) << "Can not invert zero";
+  return inverse(ran.getValue());
+#else
+  return ran;
+#endif
+}
 
 }  // namespace cvc5
+
+namespace std {
+size_t hash<cvc5::RealAlgebraicNumber>::operator()(
+    const cvc5::RealAlgebraicNumber& ran) const
+{
+#ifdef CVC5_POLY_IMP
+  return lp_algebraic_number_hash_approx(ran.getValue().get_internal(), 2);
+#else
+  return 0;
+#endif
+}
+}  // namespace std
diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h
index d71d0eae7..dcb45c036 100644
--- a/src/util/real_algebraic_number_poly_imp.h
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -128,6 +128,9 @@ RealAlgebraicNumber operator-(const RealAlgebraicNumber& ran);
 /** Multiply two real algebraic numbers. */
 RealAlgebraicNumber operator*(const RealAlgebraicNumber& lhs,
                               const RealAlgebraicNumber& rhs);
+/** Divide two real algebraic numbers. */
+RealAlgebraicNumber operator/(const RealAlgebraicNumber& lhs,
+                              const RealAlgebraicNumber& rhs);
 
 /** Add and assign two real algebraic numbers. */
 RealAlgebraicNumber& operator+=(RealAlgebraicNumber& lhs,
@@ -146,7 +149,25 @@ int sgn(const RealAlgebraicNumber& ran);
 bool isZero(const RealAlgebraicNumber& ran);
 /** Check whether a real algebraic number is one. */
 bool isOne(const RealAlgebraicNumber& ran);
+/** Compute the inverse of a real algebraic number. */
+RealAlgebraicNumber inverse(const RealAlgebraicNumber& ran);
+
+using RealAlgebraicNumberHashFunction = std::hash<RealAlgebraicNumber>;
 
 }  // namespace cvc5
 
+namespace std {
+template <>
+struct hash<cvc5::RealAlgebraicNumber>
+{
+  /**
+   * Computes a hash of the given real algebraic number. Given that the internal
+   * representation of real algebraic numbers are inherently mutable (th
+   * interval may be refined for comparisons) we hash a well-defined rational
+   * approximation.
+   */
+  size_t operator()(const cvc5::RealAlgebraicNumber& ran) const;
+};
+}  // namespace std
+
 #endif /* CVC5__REAL_ALGEBRAIC_NUMBER_H */
diff --git a/test/unit/util/real_algebraic_number_black.cpp b/test/unit/util/real_algebraic_number_black.cpp
index 8969091bd..3744f8346 100644
--- a/test/unit/util/real_algebraic_number_black.cpp
+++ b/test/unit/util/real_algebraic_number_black.cpp
@@ -37,7 +37,7 @@ TEST_F(TestUtilBlackRealAlgebraicNumber, creation)
   ASSERT_TRUE(sqrt2 < RealAlgebraicNumber(Integer(2)));
 }
 
-TEST_F(TestUtilBlackRealAlgebraicNumber, comprison)
+TEST_F(TestUtilBlackRealAlgebraicNumber, comparison)
 {
   RealAlgebraicNumber msqrt3({-3, 0, 1}, -2, -1);
   RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
@@ -79,5 +79,16 @@ TEST_F(TestUtilBlackRealAlgebraicNumber, arithmetic)
   ASSERT_EQ(-msqrt2 + sqrt2, sqrt2 + sqrt2);
   ASSERT_EQ(msqrt2 * sqrt2, RealAlgebraicNumber(Integer(-2)));
 }
+
+TEST_F(TestUtilBlackRealAlgebraicNumber, division)
+{
+  RealAlgebraicNumber msqrt2({-2, 0, 1}, -2, -1);
+  RealAlgebraicNumber sqrt2({-2, 0, 1}, 1, 2);
+  RealAlgebraicNumber mone({1, 1}, -2, 0);
+
+  ASSERT_EQ(msqrt2 / sqrt2, mone);
+  ASSERT_TRUE(isOne(sqrt2 / sqrt2));
+}
+
 }  // namespace test
 }  // namespace cvc5
-- 
2.30.2