Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * This file is part of the cvc5 project.
       3                 :            :  *
       4                 :            :  * Copyright (c) 2009-2026 by the authors listed in the file AUTHORS
       5                 :            :  * in the top-level source directory and their institutional affiliations.
       6                 :            :  * All rights reserved.  See the file COPYING in the top-level source
       7                 :            :  * directory for licensing information.
       8                 :            :  * ****************************************************************************
       9                 :            :  *
      10                 :            :  * Implementation of RealAlgebraicNumber based on libpoly.
      11                 :            :  */
      12                 :            : 
      13                 :            : #include "base/cvc5config.h"
      14                 :            : #include "util/real_algebraic_number.h"
      15                 :            : 
      16                 :            : #ifdef CVC5_POLY_IMP
      17                 :            : #include <poly/polyxx.h>
      18                 :            : #endif
      19                 :            : 
      20                 :            : #include <limits>
      21                 :            : #include <sstream>
      22                 :            : 
      23                 :            : #include "base/check.h"
      24                 :            : #include "util/poly_util.h"
      25                 :            : 
      26                 :            : #define RAN_UNREACHABLE \
      27                 :            :   Unreachable() << "RealAlgebraicNumber is not available without libpoly."
      28                 :            : 
      29                 :            : namespace cvc5::internal {
      30                 :            : 
      31                 :    2428970 : RealAlgebraicNumber::RealAlgebraicNumber()
      32                 :            :     :
      33                 :            : #ifdef CVC5_POLY_IMP
      34                 :    2428970 :       d_isRational(true),
      35                 :            : #endif
      36                 :    2428970 :       d_rat()
      37                 :            : {
      38                 :    2428970 : }
      39                 :            : 
      40                 :            : #ifdef CVC5_POLY_IMP
      41                 :        166 : RealAlgebraicNumber::RealAlgebraicNumber(poly::AlgebraicNumber&& an)
      42                 :        166 :     : d_isRational(false), d_value(std::move(an))
      43                 :            : {
      44                 :        166 : }
      45                 :            : #endif
      46                 :            : 
      47                 :   23603615 : RealAlgebraicNumber::RealAlgebraicNumber(const Integer& i)
      48                 :            :     :
      49                 :            : #ifdef CVC5_POLY_IMP
      50                 :   23603615 :       d_isRational(true),
      51                 :            : #endif
      52                 :   23603615 :       d_rat(i)
      53                 :            : {
      54                 :   23603615 : }
      55                 :            : 
      56                 :   28525362 : RealAlgebraicNumber::RealAlgebraicNumber(const Rational& r)
      57                 :            :     :
      58                 :            : #ifdef CVC5_POLY_IMP
      59                 :   28525362 :       d_isRational(true),
      60                 :            : #endif
      61                 :   28525362 :       d_rat(r)
      62                 :            : {
      63                 :   28525362 : }
      64                 :            : 
      65                 :         21 : RealAlgebraicNumber::RealAlgebraicNumber(
      66                 :            :     CVC5_UNUSED const std::vector<long>& coefficients,
      67                 :            :     CVC5_UNUSED long lower,
      68                 :         21 :     CVC5_UNUSED long upper)
      69                 :            : {
      70                 :            : #ifdef CVC5_ASSERTIONS
      71         [ +  + ]:         84 :   for (long c : coefficients)
      72                 :            :   {
      73 [ +  - ][ +  - ]:         63 :     Assert(std::numeric_limits<int32_t>::min() <= c
         [ -  + ][ -  + ]
                 [ -  - ]
      74                 :            :            && c <= std::numeric_limits<int32_t>::max())
      75                 :            :         << "Coefficients need to fit within 32 bit integers. Please use the "
      76                 :          0 :            "constructor based on Integer instead.";
      77                 :            :   }
      78                 :            : #endif
      79                 :            : #ifdef CVC5_POLY_IMP
      80                 :         21 :   d_isRational = false;
      81                 :         42 :   d_value = poly::AlgebraicNumber(poly::UPolynomial(coefficients),
      82                 :         63 :                                   poly::DyadicInterval(lower, upper));
      83                 :            : #else
      84                 :            :   RAN_UNREACHABLE;
      85                 :            : #endif
      86                 :         21 : }
      87                 :            : 
      88                 :          0 : RealAlgebraicNumber::RealAlgebraicNumber(
      89                 :            :     CVC5_UNUSED const std::vector<Integer>& coefficients,
      90                 :            :     CVC5_UNUSED const Rational& lower,
      91                 :          0 :     CVC5_UNUSED const Rational& upper)
      92                 :            : {
      93                 :            : #ifdef CVC5_POLY_IMP
      94                 :          0 :   d_isRational = false;
      95                 :          0 :   *this = poly_utils::toRanWithRefinement(
      96                 :          0 :       poly::UPolynomial(poly_utils::toInteger(coefficients)), lower, upper);
      97                 :            : #else
      98                 :            :   RAN_UNREACHABLE;
      99                 :            : #endif
     100                 :          0 : }
     101                 :          1 : RealAlgebraicNumber::RealAlgebraicNumber(
     102                 :            :     CVC5_UNUSED const std::vector<Rational>& coefficients,
     103                 :            :     CVC5_UNUSED const Rational& lower,
     104                 :          1 :     CVC5_UNUSED const Rational& upper)
     105                 :            : {
     106                 :            : #ifdef CVC5_POLY_IMP
     107                 :          1 :   d_isRational = false;
     108                 :          1 :   Integer factor = Integer(1);
     109         [ +  + ]:          4 :   for (const auto& c : coefficients)
     110                 :            :   {
     111                 :          3 :     factor = factor.lcm(c.getDenominator());
     112                 :            :   }
     113                 :          1 :   std::vector<poly::Integer> coeffs;
     114         [ +  + ]:          4 :   for (const auto& c : coefficients)
     115                 :            :   {
     116 [ -  + ][ -  + ]:          3 :     Assert((c * factor).getDenominator() == Integer(1));
                 [ -  - ]
     117                 :          3 :     coeffs.emplace_back(poly_utils::toInteger((c * factor).getNumerator()));
     118                 :            :   }
     119                 :          2 :   *this = poly_utils::toRanWithRefinement(
     120                 :          3 :       poly::UPolynomial(std::move(coeffs)), lower, upper);
     121                 :            : #else
     122                 :            :   RAN_UNREACHABLE;
     123                 :            : #endif
     124                 :          1 : }
     125                 :            : 
     126                 :   37031567 : bool RealAlgebraicNumber::isRational() const
     127                 :            : {
     128                 :            : #ifdef CVC5_POLY_IMP
     129         [ +  + ]:   37031567 :   if (!d_isRational)
     130                 :            :   {
     131                 :       1400 :     return poly::is_rational(getValue());
     132                 :            :   }
     133                 :            : #endif
     134                 :   37030167 :   return true;
     135                 :            : }
     136                 :   35260018 : Rational RealAlgebraicNumber::toRational() const
     137                 :            : {
     138                 :            : #ifdef CVC5_POLY_IMP
     139         [ +  + ]:   35260018 :   if (!d_isRational)
     140                 :            :   {
     141                 :         88 :     return poly_utils::toRational(poly::to_rational_approximation(getValue()));
     142                 :            :   }
     143                 :            : #endif
     144                 :   35259974 :   return getRationalValue();
     145                 :            : }
     146                 :            : 
     147                 :          4 : std::string RealAlgebraicNumber::toString() const
     148                 :            : {
     149                 :          4 :   std::stringstream ss;
     150                 :            : #ifdef CVC5_POLY_IMP
     151         [ +  - ]:          4 :   if (!d_isRational)
     152                 :            :   {
     153                 :          4 :     ss << getValue();
     154                 :          4 :     return ss.str();
     155                 :            :   }
     156                 :            : #endif
     157                 :          0 :   ss << getRationalValue();
     158                 :          0 :   return ss.str();
     159                 :          4 : }
     160                 :            : 
     161                 :            : #ifdef CVC5_POLY_IMP
     162                 :       4656 : poly::AlgebraicNumber RealAlgebraicNumber::convertToPoly(
     163                 :            :     const RealAlgebraicNumber& r)
     164                 :            : {
     165                 :            :   // if we are already poly, just return the value
     166         [ +  + ]:       4656 :   if (!r.d_isRational)
     167                 :            :   {
     168                 :       4018 :     return r.d_value;
     169                 :            :   }
     170                 :            :   // otherwise, this converts the rational value of r to poly
     171                 :        638 :   const Rational& rr = r.getRationalValue();
     172                 :        638 :   poly::Rational pr = poly_utils::toRational(rr);
     173                 :        638 :   auto dr = poly_utils::toDyadicRational(rr);
     174         [ +  + ]:        638 :   if (dr)
     175                 :            :   {
     176                 :        611 :     return poly::AlgebraicNumber(dr.value());
     177                 :            :   }
     178                 :            :   return poly::AlgebraicNumber(
     179 [ +  + ][ -  - ]:        108 :       poly::UPolynomial({-numerator(pr), denominator(pr)}),
     180                 :         81 :       poly::DyadicInterval(floor(pr), ceil(pr)));
     181                 :        638 : }
     182                 :            : #endif
     183                 :            : 
     184                 :       1700 : bool RealAlgebraicNumber::operator==(const RealAlgebraicNumber& rhs) const
     185                 :            : {
     186                 :            : #ifdef CVC5_POLY_IMP
     187 [ +  + ][ +  - ]:       1700 :   if (!d_isRational || !rhs.d_isRational)
     188                 :            :   {
     189                 :       1700 :     return convertToPoly(*this) == convertToPoly(rhs);
     190                 :            :   }
     191                 :            : #endif
     192                 :          0 :   return getRationalValue() == rhs.getRationalValue();
     193                 :            : }
     194                 :          0 : bool RealAlgebraicNumber::operator!=(const RealAlgebraicNumber& rhs) const
     195                 :            : {
     196                 :          0 :   return !(*this == rhs);
     197                 :            : }
     198                 :         12 : bool RealAlgebraicNumber::operator<(const RealAlgebraicNumber& rhs) const
     199                 :            : {
     200                 :            : #ifdef CVC5_POLY_IMP
     201 [ +  + ][ +  - ]:         12 :   if (!d_isRational || !rhs.d_isRational)
     202                 :            :   {
     203                 :         12 :     return convertToPoly(*this) < convertToPoly(rhs);
     204                 :            :   }
     205                 :            : #endif
     206                 :          0 :   return getRationalValue() < rhs.getRationalValue();
     207                 :            : }
     208                 :        152 : bool RealAlgebraicNumber::operator<=(const RealAlgebraicNumber& rhs) const
     209                 :            : {
     210                 :            : #ifdef CVC5_POLY_IMP
     211 [ +  - ][ +  - ]:        152 :   if (!d_isRational || !rhs.d_isRational)
     212                 :            :   {
     213                 :        152 :     return convertToPoly(*this) <= convertToPoly(rhs);
     214                 :            :   }
     215                 :            : #endif
     216                 :          0 :   return getRationalValue() <= rhs.getRationalValue();
     217                 :            : }
     218                 :          0 : bool RealAlgebraicNumber::operator>(const RealAlgebraicNumber& rhs) const
     219                 :            : {
     220                 :          0 :   return rhs < *this;
     221                 :            : }
     222                 :        152 : bool RealAlgebraicNumber::operator>=(const RealAlgebraicNumber& rhs) const
     223                 :            : {
     224                 :        152 :   return rhs <= *this;
     225                 :            :   ;
     226                 :            : }
     227                 :            : 
     228                 :          3 : RealAlgebraicNumber RealAlgebraicNumber::operator+(
     229                 :            :     const RealAlgebraicNumber& rhs) const
     230                 :            : {
     231                 :            : #ifdef CVC5_POLY_IMP
     232                 :            :   // if either is poly, we convert both and return the result
     233 [ -  + ][ -  - ]:          3 :   if (!d_isRational || !rhs.d_isRational)
     234                 :            :   {
     235                 :          6 :     return convertToPoly(*this) + convertToPoly(rhs);
     236                 :            :   }
     237                 :            : #endif
     238                 :          0 :   return getRationalValue() + rhs.getRationalValue();
     239                 :            : }
     240                 :          0 : RealAlgebraicNumber RealAlgebraicNumber::operator-(
     241                 :            :     const RealAlgebraicNumber& rhs) const
     242                 :            : {
     243                 :            : #ifdef CVC5_POLY_IMP
     244 [ -  - ][ -  - ]:          0 :   if (!d_isRational || !rhs.d_isRational)
     245                 :            :   {
     246                 :          0 :     return convertToPoly(*this) - convertToPoly(rhs);
     247                 :            :   }
     248                 :            : #endif
     249                 :          0 :   return getRationalValue() - rhs.getRationalValue();
     250                 :            : }
     251                 :    3558670 : RealAlgebraicNumber RealAlgebraicNumber::operator-() const
     252                 :            : {
     253                 :            : #ifdef CVC5_POLY_IMP
     254         [ +  + ]:    3558670 :   if (!d_isRational)
     255                 :            :   {
     256                 :         20 :     return -getValue();
     257                 :            :   }
     258                 :            : #endif
     259                 :    7117320 :   return -getRationalValue();
     260                 :            : }
     261                 :     147806 : RealAlgebraicNumber RealAlgebraicNumber::operator*(
     262                 :            :     const RealAlgebraicNumber& rhs) const
     263                 :            : {
     264                 :            : #ifdef CVC5_POLY_IMP
     265 [ +  + ][ -  + ]:     147806 :   if (!d_isRational || !rhs.d_isRational)
     266                 :            :   {
     267                 :        142 :     return convertToPoly(*this) * convertToPoly(rhs);
     268                 :            :   }
     269                 :            : #endif
     270                 :     295470 :   return getRationalValue() * rhs.getRationalValue();
     271                 :            : }
     272                 :     432435 : RealAlgebraicNumber RealAlgebraicNumber::operator/(
     273                 :            :     const RealAlgebraicNumber& rhs) const
     274                 :            : {
     275 [ -  + ][ -  + ]:     432435 :   Assert(!rhs.isZero()) << "Can not divide by zero";
                 [ -  - ]
     276                 :            : #ifdef CVC5_POLY_IMP
     277 [ +  + ][ +  + ]:     432435 :   if (!d_isRational || !rhs.d_isRational)
     278                 :            :   {
     279                 :         22 :     return convertToPoly(*this) / convertToPoly(rhs);
     280                 :            :   }
     281                 :            : #endif
     282                 :     864848 :   return getRationalValue() / rhs.getRationalValue();
     283                 :            : }
     284                 :            : 
     285                 :     726888 : RealAlgebraicNumber& RealAlgebraicNumber::operator+=(
     286                 :            :     const RealAlgebraicNumber& rhs)
     287                 :            : {
     288                 :            : #ifdef CVC5_POLY_IMP
     289 [ +  + ][ +  + ]:     726888 :   if (!d_isRational || !rhs.d_isRational)
     290                 :            :   {
     291                 :         78 :     getValue() = convertToPoly(*this) + convertToPoly(rhs);
     292                 :            :     // ensure it is no longer marked as rational
     293                 :         78 :     d_isRational = false;
     294                 :         78 :     return *this;
     295                 :            :   }
     296                 :            : #endif
     297                 :     726810 :   getRationalValue() = getRationalValue() + rhs.getRationalValue();
     298                 :     726810 :   return *this;
     299                 :            : }
     300                 :          0 : RealAlgebraicNumber& RealAlgebraicNumber::operator-=(
     301                 :            :     const RealAlgebraicNumber& rhs)
     302                 :            : {
     303                 :            : #ifdef CVC5_POLY_IMP
     304 [ -  - ][ -  - ]:          0 :   if (!d_isRational || !rhs.d_isRational)
     305                 :            :   {
     306                 :          0 :     getValue() = convertToPoly(*this) - convertToPoly(rhs);
     307                 :            :     // ensure it is no longer marked as rational
     308                 :          0 :     d_isRational = false;
     309                 :          0 :     return *this;
     310                 :            :   }
     311                 :            : #endif
     312                 :          0 :   getRationalValue() = getRationalValue() - rhs.getRationalValue();
     313                 :          0 :   return *this;
     314                 :            : }
     315                 :   17493058 : RealAlgebraicNumber& RealAlgebraicNumber::operator*=(
     316                 :            :     const RealAlgebraicNumber& rhs)
     317                 :            : {
     318                 :            : #ifdef CVC5_POLY_IMP
     319 [ +  + ][ +  + ]:   17493058 :   if (!d_isRational || !rhs.d_isRational)
     320                 :            :   {
     321                 :        301 :     getValue() = convertToPoly(*this) * convertToPoly(rhs);
     322                 :            :     // ensure it is no longer marked as rational
     323                 :        301 :     d_isRational = false;
     324                 :        301 :     return *this;
     325                 :            :   }
     326                 :            : #endif
     327                 :   17492757 :   getRationalValue() = getRationalValue() * rhs.getRationalValue();
     328                 :   17492757 :   return *this;
     329                 :            : }
     330                 :            : 
     331                 :    4205181 : int RealAlgebraicNumber::sgn() const
     332                 :            : {
     333                 :            : #ifdef CVC5_POLY_IMP
     334         [ +  + ]:    4205181 :   if (!d_isRational)
     335                 :            :   {
     336                 :          2 :     return poly::sgn(getValue());
     337                 :            :   }
     338                 :            : #endif
     339                 :    4205179 :   return getRationalValue().sgn();
     340                 :            : }
     341                 :   18826718 : bool RealAlgebraicNumber::isZero() const
     342                 :            : {
     343                 :            : #ifdef CVC5_POLY_IMP
     344         [ +  + ]:   18826718 :   if (!d_isRational)
     345                 :            :   {
     346                 :        210 :     return poly::is_zero(getValue());
     347                 :            :   }
     348                 :            : #endif
     349                 :   18826508 :   return getRationalValue().isZero();
     350                 :            : }
     351                 :     761881 : bool RealAlgebraicNumber::isOne() const
     352                 :            : {
     353                 :            : #ifdef CVC5_POLY_IMP
     354         [ +  + ]:     761881 :   if (!d_isRational)
     355                 :            :   {
     356                 :          1 :     return poly::is_one(getValue());
     357                 :            :   }
     358                 :            : #endif
     359                 :     761880 :   return getRationalValue().isOne();
     360                 :            : }
     361                 :          0 : RealAlgebraicNumber RealAlgebraicNumber::inverse() const
     362                 :            : {
     363                 :          0 :   Assert(!isZero()) << "Can not invert zero";
     364                 :            : #ifdef CVC5_POLY_IMP
     365         [ -  - ]:          0 :   if (!d_isRational)
     366                 :            :   {
     367                 :          0 :     return poly::inverse(getValue());
     368                 :            :   }
     369                 :            : #endif
     370                 :          0 :   return getRationalValue().inverse();
     371                 :            : }
     372                 :            : 
     373                 :       1030 : size_t RealAlgebraicNumber::hash() const
     374                 :            : {
     375                 :            : #ifdef CVC5_POLY_IMP
     376         [ +  - ]:       1030 :   if (!d_isRational)
     377                 :            :   {
     378                 :       1030 :     return lp_algebraic_number_hash_approx(getValue().get_internal(), 2);
     379                 :            :   }
     380                 :            : #endif
     381                 :          0 :   return getRationalValue().hash();
     382                 :            : }
     383                 :            : 
     384                 :          4 : std::ostream& operator<<(std::ostream& os, const RealAlgebraicNumber& ran)
     385                 :            : {
     386                 :          4 :   return os << ran.toString();
     387                 :            : }
     388                 :            : 
     389                 :            : }  // namespace cvc5::internal
     390                 :            : 
     391                 :            : namespace std {
     392                 :       1030 : size_t hash<cvc5::internal::RealAlgebraicNumber>::operator()(
     393                 :            :     const cvc5::internal::RealAlgebraicNumber& ran) const
     394                 :            : {
     395                 :       1030 :   return ran.hash();
     396                 :            : }
     397                 :            : 
     398                 :            : }  // namespace std