Add mkRealAlgebraicNumber (#7923)

This PR adds the convenience function NodeManager::mkRealAlgebraicNumber().

diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp
index 944d7fe66d7f0bca528e5260237f8d416b37bb88..2345578c20c91d2d66ebef89d8d95e14ff3914a5 100644 (file)
--- a/src/expr/node_manager_template.cpp
+++ b/src/expr/node_manager_template.cpp
@@ -35,6 +35,7 @@
 #include "theory/type_enumerator.h"
 #include "util/abstract_value.h"
 #include "util/bitvector.h"
+#include "util/poly_util.h"
 #include "util/rational.h"
 #include "util/resource_manager.h"
 
@@ -1303,4 +1304,14 @@ Node NodeManager::mkConstRealOrInt(const TypeNode& tn, const Rational& r)
   return mkConstInt(r);
 }
 
+Node NodeManager::mkRealAlgebraicNumber(const RealAlgebraicNumber& ran)
+{
+  if (ran.isRational())
+  {
+    return mkConstReal(ran.toRational());
+  }
+  return mkNode(Kind::REAL_ALGEBRAIC_NUMBER,
+                mkConst(Kind::REAL_ALGEBRAIC_NUMBER_OP, ran));
+}
+
 }  // namespace cvc5

diff --git a/src/expr/node_manager_template.h b/src/expr/node_manager_template.h
index 5e562c18eb9449d6ebdcd0e32869c87a51434488..245fc023e95446cad133d42e7c9dcecbe8887350 100644 (file)
--- a/src/expr/node_manager_template.h
+++ b/src/expr/node_manager_template.h
@@ -751,6 +751,23 @@ class NodeManager
    */
   Node mkConstRealOrInt(const TypeNode& tn, const Rational& r);
 
+  /**
+   * Make a real algebraic number node from a RealAlgebraicNumber.
+   * If the real algebraic number is found to be rational, this method returns a
+   * node of kind CONST_RATIONAL. Otherwise, it returns a node of kind
+   * REAL_ALGEBRIAC_NUMBER.
+   *
+   * It is, unfortunately, not entirely possible to provide the usual uniqueness
+   * guarantees for real algebraic number nodes. As a REAL_ALGEBRIAC_NUMBER node
+   * may turn out to be rational later on, it may be semantically equal to a
+   * CONST_RATIONAL node, although the comparison operator would always return
+   * false. For this reason, comparisons should be performed by evaluating (i.e.
+   * rewriting) the EQUAL predicate, or by inspecting the values manually. Note
+   * that the comparison operators for RealAlgebraicNumber properly support
+   * Rational as well.
+   */
+  Node mkRealAlgebraicNumber(const RealAlgebraicNumber& ran);
+
   /** Create a node with children. */
   TypeNode mkTypeNode(Kind kind, TypeNode child1);
   TypeNode mkTypeNode(Kind kind, TypeNode child1, TypeNode child2);

diff --git a/src/theory/arith/kinds b/src/theory/arith/kinds
index 4cd59c1a08c6e91dfc85b075e49a0857bb417abe..40557bc657d3b55d73721f7b645109b46cb80c93 100644 (file)
--- a/src/theory/arith/kinds
+++ b/src/theory/arith/kinds
@@ -80,7 +80,7 @@ constant CONST_INTEGER \
 
 constant REAL_ALGEBRAIC_NUMBER_OP \
     class \
-    RealAlgebraicNumber \
+    RealAlgebraicNumber+ \
     ::cvc5::RealAlgebraicNumberHashFunction \
     "util/real_algebraic_number.h" \
     "a real algebraic number constant; payload is an instance of the cvc5::RealAlgebraicNumber class"

diff --git a/src/util/real_algebraic_number_poly_imp.cpp b/src/util/real_algebraic_number_poly_imp.cpp
index d92d917dc192fed804b668f27ade56be144e8a5d..d6ded7c7be121404d27617f8dacf011d20b8c2a1 100644 (file)
--- a/src/util/real_algebraic_number_poly_imp.cpp
+++ b/src/util/real_algebraic_number_poly_imp.cpp
@@ -27,6 +27,9 @@
 #include "base/check.h"
 #include "util/poly_util.h"
 
+#define RAN_UNREACHABLE \
+  Unreachable() << "RealAlgebraicNumber is not available without libpoly."
+
 namespace cvc5 {
 
 RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an)
@@ -100,6 +103,25 @@ RealAlgebraicNumber::RealAlgebraicNumber(
       poly::UPolynomial(std::move(coeffs)), lower, upper);
 }
 
+bool RealAlgebraicNumber::isRational() const
+{
+#ifdef CVC5_POLY_IMP
+  return poly::is_rational(getValue());
+#else
+  RAN_UNREACHABLE;
+  return true;
+#endif
+}
+Rational RealAlgebraicNumber::toRational() const
+{
+#ifdef CVC5_POLY_IMP
+  return poly_utils::toRational(poly::to_rational_approximation(getValue()));
+#else
+  RAN_UNREACHABLE;
+  return Rational(0);
+#endif
+}
+
 std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran)
 {
   return os << ran.getValue();
@@ -156,6 +178,7 @@ RealAlgebraicNumber operator/(const RealAlgebraicNumber& lhs,
   Assert(!isZero(rhs)) << "Can not divide by zero";
   return lhs.getValue() / rhs.getValue();
 #else
+  RAN_UNREACHABLE;
   return lhs;
 #endif
 }
@@ -188,6 +211,7 @@ RealAlgebraicNumber inverse(const RealAlgebraicNumber& ran)
   Assert(!isZero(ran)) << "Can not invert zero";
   return inverse(ran.getValue());
 #else
+  RAN_UNREACHABLE;
   return ran;
 #endif
 }
@@ -201,6 +225,7 @@ size_t hash<cvc5::RealAlgebraicNumber>::operator()(
 #ifdef CVC5_POLY_IMP
   return lp_algebraic_number_hash_approx(ran.getValue().get_internal(), 2);
 #else
+  RAN_UNREACHABLE;
   return 0;
 #endif
 }

diff --git a/src/util/real_algebraic_number_poly_imp.h b/src/util/real_algebraic_number_poly_imp.h
index dcb45c036dcd3a3d5f461f8fb02162d9f1eae5df..d75bd1836d1f9614f2e7617c15a03de9621446ad 100644 (file)
--- a/src/util/real_algebraic_number_poly_imp.h
+++ b/src/util/real_algebraic_number_poly_imp.h
@@ -94,6 +94,20 @@ class RealAlgebraicNumber
   /** Get the internal value as a non-const reference. */
   poly::AlgebraicNumber& getValue() { return d_value; }
 
+  /**
+   * Check if this real algebraic number is actually rational.
+   * If true, the value is rational and toRational() can safely be called.
+   * If false, the value may still be rational, but was not recognized as
+   * such yet.
+   */
+  bool isRational() const;
+  /**
+   * Returns the stored value as a rational.
+   * The value is exact if isRational() returns true, otherwise it may only be a
+   * rational approximation (of unknown precision).
+   */
+  Rational toRational() const;
+
  private:
   /**
    * Stores the actual real algebraic number.