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                 :            :  * A multi-precision rational constant.
      11                 :            :  */
      12                 :            : #include <cln/integer_io.h>
      13                 :            : 
      14                 :            : #include <sstream>
      15                 :            : #include <string>
      16                 :            : 
      17                 :            : #include "base/cvc5config.h"
      18                 :            : #include "util/rational.h"
      19                 :            : 
      20                 :            : #ifndef CVC5_CLN_IMP
      21                 :            : #error "This source should only ever be built if CVC5_CLN_IMP is on !"
      22                 :            : #endif /* CVC5_CLN_IMP */
      23                 :            : 
      24                 :            : #include "base/check.h"
      25                 :            : 
      26                 :            : using namespace std;
      27                 :            : 
      28                 :            : namespace cvc5::internal {
      29                 :            : 
      30                 :            : /* Computes a rational given a decimal string. The rational
      31                 :            :  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
      32                 :            :  */
      33                 :     910765 : Rational Rational::fromDecimal(const std::string& dec)
      34                 :            : {
      35                 :            :   // Find the decimal point, if there is one
      36                 :     910765 :   string::size_type i(dec.find("."));
      37         [ +  + ]:     910765 :   if (i != string::npos)
      38                 :            :   {
      39                 :            :     /* Erase the decimal point, so we have just the numerator. */
      40                 :      66394 :     Integer numerator(string(dec).erase(i, 1));
      41                 :            : 
      42                 :            :     /* Compute the denominator: 10 raise to the number of decimal places */
      43                 :      66390 :     int decPlaces = dec.size() - (i + 1);
      44                 :      66390 :     Integer denominator(Integer(10).pow(decPlaces));
      45                 :            : 
      46                 :      66390 :     return Rational(numerator, denominator);
      47                 :      66390 :   }
      48                 :            :   else
      49                 :            :   {
      50                 :            :     /* No decimal point, assume it's just an integer. */
      51                 :     844373 :     return Rational(dec);
      52                 :            :   }
      53                 :            : }
      54                 :            : 
      55                 :     890321 : Rational::Rational(const char* s, uint32_t base)
      56                 :            : {
      57                 :            :   try
      58                 :            :   {
      59                 :            :     cln::cl_read_flags flags;
      60                 :     890321 :     flags.rational_base = base;
      61                 :     890321 :     flags.lsyntax = cln::lsyntax_standard;
      62                 :            : 
      63                 :     890321 :     const char* p = strchr(s, '/');
      64                 :            :     /* read_rational() does not support the case where the denominator is
      65                 :            :      * negative.  In this case we read the numerator and denominator via
      66                 :            :      * read_integer() and build a rational out of two integers. */
      67         [ +  + ]:     890321 :     if (p)
      68                 :            :     {
      69                 :      45302 :       flags.syntax = cln::syntax_integer;
      70                 :      45302 :       auto num = cln::read_integer(flags, s, p, nullptr);
      71                 :      45296 :       auto den = cln::read_integer(flags, p + 1, nullptr, nullptr);
      72                 :      45296 :       d_value = num / den;
      73                 :      45296 :     }
      74                 :            :     else
      75                 :            :     {
      76                 :     845019 :       flags.syntax = cln::syntax_rational;
      77                 :     845019 :       d_value = read_rational(flags, s, NULL, NULL);
      78                 :            :     }
      79                 :            :   }
      80                 :        388 :   catch (...)
      81                 :            :   {
      82                 :        388 :     std::stringstream ss;
      83                 :        388 :     ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
      84                 :        388 :     throw std::invalid_argument(ss.str());
      85                 :        776 :   }
      86                 :     890321 : }
      87                 :            : 
      88                 :     845842 : Rational::Rational(const std::string& s, uint32_t base)
      89                 :     845842 :     : Rational(s.c_str(), base)
      90                 :            : {
      91                 :     845454 : }
      92                 :            : 
      93                 :  650546497 : int Rational::sgn() const
      94                 :            : {
      95         [ +  + ]:  650546497 :   if (cln::zerop(d_value))
      96                 :            :   {
      97                 :   64492229 :     return 0;
      98                 :            :   }
      99         [ +  + ]:  586054268 :   else if (cln::minusp(d_value))
     100                 :            :   {
     101                 :  347944604 :     return -1;
     102                 :            :   }
     103                 :            :   else
     104                 :            :   {
     105 [ -  + ][ -  + ]:  238109664 :     Assert(cln::plusp(d_value));
                 [ -  - ]
     106                 :  238109664 :     return 1;
     107                 :            :   }
     108                 :            : }
     109                 :            : 
     110                 :    1825003 : std::ostream& operator<<(std::ostream& os, const Rational& q)
     111                 :            : {
     112                 :    1825003 :   return os << q.toString();
     113                 :            : }
     114                 :            : 
     115                 :            : /** Equivalent to calling (this->abs()).cmp(b.abs()) */
     116                 :    9881930 : int Rational::absCmp(const Rational& q) const
     117                 :            : {
     118                 :    9881930 :   const Rational& r = *this;
     119                 :    9881930 :   int rsgn = r.sgn();
     120                 :    9881930 :   int qsgn = q.sgn();
     121         [ -  + ]:    9881930 :   if (rsgn == 0)
     122                 :            :   {
     123         [ -  - ]:          0 :     return (qsgn == 0) ? 0 : -1;
     124                 :            :   }
     125         [ -  + ]:    9881930 :   else if (qsgn == 0)
     126                 :            :   {
     127                 :          0 :     Assert(rsgn != 0);
     128                 :          0 :     return 1;
     129                 :            :   }
     130 [ +  + ][ +  + ]:    9881930 :   else if ((rsgn > 0) && (qsgn > 0))
     131                 :            :   {
     132                 :    6951739 :     return r.cmp(q);
     133                 :            :   }
     134 [ +  + ][ +  + ]:    2930191 :   else if ((rsgn < 0) && (qsgn < 0))
     135                 :            :   {
     136                 :            :     // if r < q < 0, q.cmp(r) = +1, (r.abs()).cmp(q.abs()) = +1
     137                 :            :     // if q < r < 0, q.cmp(r) = -1, (r.abs()).cmp(q.abs()) = -1
     138                 :            :     // if q = r < 0, q.cmp(r) =  0, (r.abs()).cmp(q.abs()) =  0
     139                 :     530518 :     return q.cmp(r);
     140                 :            :   }
     141 [ +  + ][ +  - ]:    2399673 :   else if ((rsgn < 0) && (qsgn > 0))
     142                 :            :   {
     143                 :    1517239 :     Rational rpos = -r;
     144                 :    1517239 :     return rpos.cmp(q);
     145                 :    1517239 :   }
     146                 :            :   else
     147                 :            :   {
     148 [ +  - ][ +  - ]:     882434 :     Assert(rsgn > 0 && (qsgn < 0));
         [ -  + ][ -  + ]
                 [ -  - ]
     149                 :     882434 :     Rational qpos = -q;
     150                 :     882434 :     return r.cmp(qpos);
     151                 :     882434 :   }
     152                 :            : }
     153                 :            : 
     154                 :         16 : std::optional<Rational> Rational::fromDouble(double d)
     155                 :            : {
     156                 :            :   try
     157                 :            :   {
     158                 :         16 :     cln::cl_DF fromD = d;
     159                 :         16 :     Rational q;
     160                 :         16 :     q.d_value = cln::rationalize(fromD);
     161                 :         16 :     return q;
     162                 :         16 :   }
     163 [ -  - ][ -  - ]:          0 :   catch (cln::floating_point_underflow_exception& fpue)
     164                 :            :   {
     165                 :          0 :     return std::optional<Rational>();
     166                 :          0 :   }
     167                 :          0 :   catch (cln::floating_point_nan_exception& fpne)
     168                 :            :   {
     169                 :          0 :     return std::optional<Rational>();
     170                 :          0 :   }
     171                 :          0 :   catch (cln::floating_point_overflow_exception& fpoe)
     172                 :            :   {
     173                 :          0 :     return std::optional<Rational>();
     174                 :          0 :   }
     175                 :            : }
     176                 :            : 
     177                 :            : }  // namespace cvc5::internal