Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Tim King, Mathias Preiner, Christopher L. Conway
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2024 by the authors listed in the file AUTHORS
       8                 :            :  * in the top-level source directory and their institutional affiliations.
       9                 :            :  * All rights reserved.  See the file COPYING in the top-level source
      10                 :            :  * directory for licensing information.
      11                 :            :  * ****************************************************************************
      12                 :            :  *
      13                 :            :  * A multi-precision rational constant.
      14                 :            :  */
      15                 :            : #include <cln/integer_io.h>
      16                 :            : 
      17                 :            : #include <sstream>
      18                 :            : #include <string>
      19                 :            : 
      20                 :            : #include "base/cvc5config.h"
      21                 :            : #include "util/rational.h"
      22                 :            : 
      23                 :            : #ifndef CVC5_CLN_IMP
      24                 :            : #error "This source should only ever be built if CVC5_CLN_IMP is on !"
      25                 :            : #endif /* CVC5_CLN_IMP */
      26                 :            : 
      27                 :            : #include "base/check.h"
      28                 :            : 
      29                 :            : using namespace std;
      30                 :            : 
      31                 :            : namespace cvc5::internal {
      32                 :            : 
      33                 :            : /* Computes a rational given a decimal string. The rational
      34                 :            :  * version of <code>xxx.yyy</code> is <code>xxxyyy/(10^3)</code>.
      35                 :            :  */
      36                 :     906131 : Rational Rational::fromDecimal(const std::string& dec) {
      37                 :            :   // Find the decimal point, if there is one
      38                 :     906131 :   string::size_type i( dec.find(".") );
      39         [ +  + ]:     906131 :   if( i != string::npos ) {
      40                 :            :     /* Erase the decimal point, so we have just the numerator. */
      41                 :     131254 :     Integer numerator( string(dec).erase(i,1) );
      42                 :            : 
      43                 :            :     /* Compute the denominator: 10 raise to the number of decimal places */
      44                 :      65625 :     int decPlaces = dec.size() - (i + 1);
      45                 :     131250 :     Integer denominator( Integer(10).pow(decPlaces) );
      46                 :            : 
      47                 :      65625 :     return Rational( numerator, denominator );
      48                 :            :   } else {
      49                 :            :     /* No decimal point, assume it's just an integer. */
      50                 :     840504 :     return Rational( dec );
      51                 :            :   }
      52                 :            : }
      53                 :            : 
      54                 :     842214 : Rational::Rational(const char* s, uint32_t base)
      55                 :            : {
      56                 :            :   try
      57                 :            :   {
      58                 :            :     cln::cl_read_flags flags;
      59                 :     841856 :     flags.rational_base = base;
      60                 :     841856 :     flags.lsyntax = cln::lsyntax_standard;
      61                 :            : 
      62                 :     841856 :     const char* p = strchr(s, '/');
      63                 :            :     /* read_rational() does not support the case where the denominator is
      64                 :            :      * negative.  In this case we read the numerator and denominator via
      65                 :            :      * read_integer() and build a rational out of two integers. */
      66         [ +  + ]:     841856 :     if (p)
      67                 :            :     {
      68                 :        746 :       flags.syntax = cln::syntax_integer;
      69                 :       1486 :       auto num = cln::read_integer(flags, s, p, nullptr);
      70                 :        740 :       auto den = cln::read_integer(flags, p + 1, nullptr, nullptr);
      71                 :        740 :       d_value = num / den;
      72                 :            :     }
      73                 :            :     else
      74                 :            :     {
      75                 :     841110 :       flags.syntax = cln::syntax_rational;
      76                 :     841110 :       d_value = read_rational(flags, s, NULL, NULL);
      77                 :            :     }
      78                 :            :   }
      79                 :        716 :   catch (...)
      80                 :            :   {
      81                 :        716 :     std::stringstream ss;
      82                 :        358 :     ss << "Rational() failed to parse value \"" << s << "\" in base=" << base;
      83                 :        358 :     throw std::invalid_argument(ss.str());
      84                 :            :   }
      85                 :     841498 : }
      86                 :            : 
      87                 :     841842 : Rational::Rational(const std::string& s, uint32_t base)
      88                 :     841842 :     : Rational(s.c_str(), base)
      89                 :            : {
      90                 :     841484 : }
      91                 :            : 
      92                 :  751438000 : int Rational::sgn() const
      93                 :            : {
      94         [ +  + ]:  751438000 :   if (cln::zerop(d_value))
      95                 :            :   {
      96                 :   75302000 :     return 0;
      97                 :            :   }
      98         [ +  + ]:  676136000 :   else if (cln::minusp(d_value))
      99                 :            :   {
     100                 :  383626000 :     return -1;
     101                 :            :   }
     102                 :            :   else
     103                 :            :   {
     104 [ -  + ][ -  + ]:  292510000 :     Assert(cln::plusp(d_value));
                 [ -  - ]
     105                 :  292510000 :     return 1;
     106                 :            :   }
     107                 :            : }
     108                 :            : 
     109                 :     769728 : std::ostream& operator<<(std::ostream& os, const Rational& q){
     110                 :     769728 :   return os << q.toString();
     111                 :            : }
     112                 :            : 
     113                 :            : 
     114                 :            : 
     115                 :            : /** Equivalent to calling (this->abs()).cmp(b.abs()) */
     116                 :    9767720 : int Rational::absCmp(const Rational& q) const{
     117                 :    9767720 :   const Rational& r = *this;
     118                 :    9767720 :   int rsgn = r.sgn();
     119                 :    9767720 :   int qsgn = q.sgn();
     120         [ -  + ]:    9767720 :   if(rsgn == 0){
     121         [ -  - ]:          0 :     return (qsgn == 0) ? 0 : -1;
     122         [ -  + ]:    9767720 :   }else if(qsgn == 0){
     123                 :          0 :     Assert(rsgn != 0);
     124                 :          0 :     return 1;
     125 [ +  + ][ +  + ]:    9767720 :   }else if((rsgn > 0) && (qsgn > 0)){
     126                 :    6893400 :     return r.cmp(q);
     127 [ +  + ][ +  + ]:    2874320 :   }else if((rsgn < 0) && (qsgn < 0)){
     128                 :            :     // if r < q < 0, q.cmp(r) = +1, (r.abs()).cmp(q.abs()) = +1
     129                 :            :     // if q < r < 0, q.cmp(r) = -1, (r.abs()).cmp(q.abs()) = -1
     130                 :            :     // if q = r < 0, q.cmp(r) =  0, (r.abs()).cmp(q.abs()) =  0
     131                 :     493498 :     return q.cmp(r);
     132 [ +  + ][ +  - ]:    2380820 :   }else if((rsgn < 0) && (qsgn > 0)){
     133                 :    3233780 :     Rational rpos = -r;
     134                 :    1616890 :     return rpos.cmp(q);
     135                 :            :   }else {
     136 [ +  - ][ +  - ]:    1527870 :     Assert(rsgn > 0 && (qsgn < 0));
         [ -  + ][ -  - ]
     137                 :    1527870 :     Rational qpos = -q;
     138                 :     763933 :     return r.cmp(qpos);
     139                 :            :   }
     140                 :            : }
     141                 :            : 
     142                 :         16 : std::optional<Rational> Rational::fromDouble(double d)
     143                 :            : {
     144                 :            :   try{
     145                 :         32 :     cln::cl_DF fromD = d;
     146                 :         32 :     Rational q;
     147                 :         16 :     q.d_value = cln::rationalize(fromD);
     148                 :         16 :     return q;
     149                 :          0 :   }catch(cln::floating_point_underflow_exception& fpue){
     150                 :          0 :     return std::optional<Rational>();
     151                 :          0 :   }catch(cln::floating_point_nan_exception& fpne){
     152                 :          0 :     return std::optional<Rational>();
     153                 :          0 :   }catch(cln::floating_point_overflow_exception& fpoe){
     154                 :          0 :     return std::optional<Rational>();
     155                 :            :   }
     156                 :            : }
     157                 :            : 
     158                 :            : }  // namespace cvc5::internal