From a9990d56eb3bc6f27e5bc5557db0247e4dc6a070 Mon Sep 17 00:00:00 2001 From: Gereon Kremer Date: Wed, 12 Jan 2022 10:18:19 -0800 Subject: [PATCH] Add mkRealAlgebraicNumber (#7923) This PR adds the convenience function NodeManager::mkRealAlgebraicNumber(). --- src/expr/node_manager_template.cpp | 11 +++++++++ src/expr/node_manager_template.h | 17 ++++++++++++++ src/theory/arith/kinds | 2 +- src/util/real_algebraic_number_poly_imp.cpp | 25 +++++++++++++++++++++ src/util/real_algebraic_number_poly_imp.h | 14 ++++++++++++ 5 files changed, 68 insertions(+), 1 deletion(-) diff --git a/src/expr/node_manager_template.cpp b/src/expr/node_manager_template.cpp index 944d7fe66..2345578c2 100644 --- 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 5e562c18e..245fc023e 100644 --- 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 4cd59c1a0..40557bc65 100644 --- 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 d92d917dc..d6ded7c7b 100644 --- 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::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 dcb45c036..d75bd1836 100644 --- 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. -- 2.30.2