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                 :            :  * [[ Add one-line brief description here ]]
      11                 :            :  *
      12                 :            :  * [[ Add lengthier description here ]]
      13                 :            :  * \todo document this file
      14                 :            :  */
      15                 :            : 
      16                 :            : #include "cvc5_private.h"
      17                 :            : 
      18                 :            : #pragma once
      19                 :            : 
      20                 :            : #include <ostream>
      21                 :            : 
      22                 :            : #include "base/check.h"
      23                 :            : #include "base/exception.h"
      24                 :            : #include "util/integer.h"
      25                 :            : #include "util/rational.h"
      26                 :            : 
      27                 :            : namespace cvc5::internal {
      28                 :            : 
      29                 :            : class DeltaRational;
      30                 :            : 
      31                 :            : class DeltaRationalException : public Exception
      32                 :            : {
      33                 :            :  public:
      34                 :            :   DeltaRationalException(const char* op,
      35                 :            :                          const DeltaRational& a,
      36                 :            :                          const DeltaRational& b);
      37                 :            :   ~DeltaRationalException() override;
      38                 :            : };
      39                 :            : 
      40                 :            : /**
      41                 :            :  * A DeltaRational is a pair of rationals (c,k) that represent the number
      42                 :            :  *   c + kd
      43                 :            :  * where d is an implicit system wide symbolic infinitesimal.
      44                 :            :  */
      45                 :            : class DeltaRational
      46                 :            : {
      47                 :            :  private:
      48                 :            :   cvc5::internal::Rational c;
      49                 :            :   cvc5::internal::Rational k;
      50                 :            : 
      51                 :            :  public:
      52                 :    8139858 :   DeltaRational() : c(0, 1), k(0, 1) {}
      53                 :    6031625 :   DeltaRational(const cvc5::internal::Rational& base) : c(base), k(0, 1) {}
      54                 :   49628154 :   DeltaRational(const cvc5::internal::Rational& base,
      55                 :            :                 const cvc5::internal::Rational& coeff)
      56                 :   49628154 :       : c(base), k(coeff)
      57                 :            :   {
      58                 :   49628154 :   }
      59                 :            : 
      60                 :   40679106 :   const cvc5::internal::Rational& getInfinitesimalPart() const { return k; }
      61                 :            : 
      62                 :   42790520 :   const cvc5::internal::Rational& getNoninfinitesimalPart() const { return c; }
      63                 :            : 
      64                 :   12401685 :   int sgn() const
      65                 :            :   {
      66                 :   12401685 :     int s = getNoninfinitesimalPart().sgn();
      67         [ +  + ]:   12401685 :     if (s == 0)
      68                 :            :     {
      69                 :    9067552 :       return infinitesimalSgn();
      70                 :            :     }
      71                 :            :     else
      72                 :            :     {
      73                 :    3334133 :       return s;
      74                 :            :     }
      75                 :            :   }
      76                 :            : 
      77                 :   13457799 :   int infinitesimalSgn() const { return getInfinitesimalPart().sgn(); }
      78                 :            : 
      79                 :   18304807 :   bool infinitesimalIsZero() const { return getInfinitesimalPart().isZero(); }
      80                 :            : 
      81                 :          6 :   bool noninfinitesimalIsZero() const
      82                 :            :   {
      83                 :          6 :     return getNoninfinitesimalPart().isZero();
      84                 :            :   }
      85                 :            : 
      86                 :          0 :   bool isZero() const
      87                 :            :   {
      88 [ -  - ][ -  - ]:          0 :     return noninfinitesimalIsZero() && infinitesimalIsZero();
      89                 :            :   }
      90                 :            : 
      91                 :   22996506 :   int cmp(const DeltaRational& other) const
      92                 :            :   {
      93                 :   22996506 :     int cmp = c.cmp(other.c);
      94         [ +  + ]:   22996506 :     if (cmp == 0)
      95                 :            :     {
      96                 :   10837952 :       return k.cmp(other.k);
      97                 :            :     }
      98                 :            :     else
      99                 :            :     {
     100                 :   12158554 :       return cmp;
     101                 :            :     }
     102                 :            :   }
     103                 :            : 
     104                 :   20639595 :   DeltaRational operator+(const DeltaRational& other) const
     105                 :            :   {
     106                 :   20639595 :     cvc5::internal::Rational tmpC = c + other.c;
     107                 :   20639595 :     cvc5::internal::Rational tmpK = k + other.k;
     108                 :   41279190 :     return DeltaRational(tmpC, tmpK);
     109                 :   20639595 :   }
     110                 :            : 
     111                 :   24252529 :   DeltaRational operator*(const Rational& a) const
     112                 :            :   {
     113                 :   24252529 :     cvc5::internal::Rational tmpC = a * c;
     114                 :   24252529 :     cvc5::internal::Rational tmpK = a * k;
     115                 :   48505058 :     return DeltaRational(tmpC, tmpK);
     116                 :   24252529 :   }
     117                 :            : 
     118                 :            :   /**
     119                 :            :    * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
     120                 :            :    * This can be done whenever this->k or a.k is 0.
     121                 :            :    * Otherwise, the result is not a DeltaRational and a DeltaRationalException
     122                 :            :    * is thrown.
     123                 :            :    */
     124                 :      57902 :   DeltaRational operator*(const DeltaRational& a) const
     125                 :            :   /* throw(DeltaRationalException) */ {
     126         [ +  - ]:      57902 :     if (infinitesimalIsZero())
     127                 :            :     {
     128                 :      57902 :       return a * (this->getNoninfinitesimalPart());
     129                 :            :     }
     130         [ -  - ]:          0 :     else if (a.infinitesimalIsZero())
     131                 :            :     {
     132                 :          0 :       return (*this) * a.getNoninfinitesimalPart();
     133                 :            :     }
     134                 :            :     else
     135                 :            :     {
     136                 :          0 :       throw DeltaRationalException("operator*", *this, a);
     137                 :            :     }
     138                 :            :   }
     139                 :            : 
     140                 :    2881204 :   DeltaRational operator-(const DeltaRational& a) const
     141                 :            :   {
     142                 :    2881204 :     cvc5::internal::Rational negOne(cvc5::internal::Integer(-1));
     143                 :    8643612 :     return *(this) + (a * negOne);
     144                 :    2881204 :   }
     145                 :            : 
     146                 :       7032 :   DeltaRational operator-() const { return DeltaRational(-c, -k); }
     147                 :            : 
     148                 :    1401467 :   DeltaRational operator/(const Rational& a) const
     149                 :            :   {
     150                 :    1401467 :     cvc5::internal::Rational tmpC = c / a;
     151                 :    1401467 :     cvc5::internal::Rational tmpK = k / a;
     152                 :    2802934 :     return DeltaRational(tmpC, tmpK);
     153                 :    1401467 :   }
     154                 :            : 
     155                 :            :   DeltaRational operator/(const Integer& a) const
     156                 :            :   {
     157                 :            :     cvc5::internal::Rational tmpC = c / a;
     158                 :            :     cvc5::internal::Rational tmpK = k / a;
     159                 :            :     return DeltaRational(tmpC, tmpK);
     160                 :            :   }
     161                 :            : 
     162                 :            :   /**
     163                 :            :    * Divides (*this) / (a.c + a.k * delta)
     164                 :            :    * This can be done when a.k is 0 and a.c is non-zero.
     165                 :            :    * Otherwise, the result is not a DeltaRational and a DeltaRationalException
     166                 :            :    * is thrown.
     167                 :            :    */
     168                 :          0 :   DeltaRational operator/(const DeltaRational& a) const
     169                 :            :   /* throw(DeltaRationalException) */ {
     170         [ -  - ]:          0 :     if (a.infinitesimalIsZero())
     171                 :            :     {
     172                 :          0 :       return (*this) / a.getNoninfinitesimalPart();
     173                 :            :     }
     174                 :            :     else
     175                 :            :     {
     176                 :          0 :       throw DeltaRationalException("operator/", *this, a);
     177                 :            :     }
     178                 :            :   }
     179                 :            : 
     180                 :            :   DeltaRational abs() const
     181                 :            :   {
     182                 :            :     if (sgn() >= 0)
     183                 :            :     {
     184                 :            :       return *this;
     185                 :            :     }
     186                 :            :     else
     187                 :            :     {
     188                 :            :       return (*this) * Rational(-1);
     189                 :            :     }
     190                 :            :   }
     191                 :            : 
     192                 :    4103604 :   bool operator==(const DeltaRational& other) const
     193                 :            :   {
     194 [ +  + ][ +  + ]:    4103604 :     return (k == other.k) && (c == other.c);
     195                 :            :   }
     196                 :            : 
     197                 :     136424 :   bool operator!=(const DeltaRational& other) const
     198                 :            :   {
     199                 :     136424 :     return !(*this == other);
     200                 :            :   }
     201                 :            : 
     202                 :  129359069 :   bool operator<=(const DeltaRational& other) const
     203                 :            :   {
     204                 :  129359069 :     int cmp = c.cmp(other.c);
     205 [ +  + ][ +  + ]:  129359069 :     return (cmp < 0) || ((cmp == 0) && (k <= other.k));
                 [ +  + ]
     206                 :            :   }
     207                 :  114376283 :   bool operator<(const DeltaRational& other) const { return (other > *this); }
     208                 :    3430615 :   bool operator>=(const DeltaRational& other) const { return (other <= *this); }
     209                 :  118122559 :   bool operator>(const DeltaRational& other) const { return !(*this <= other); }
     210                 :            : 
     211                 :            :   int compare(const DeltaRational& other) const
     212                 :            :   {
     213                 :            :     int cmpRes = c.cmp(other.c);
     214                 :            :     return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
     215                 :            :   }
     216                 :            : 
     217                 :            :   DeltaRational& operator*=(const cvc5::internal::Rational& a)
     218                 :            :   {
     219                 :            :     c *= a;
     220                 :            :     k *= a;
     221                 :            : 
     222                 :            :     return *(this);
     223                 :            :   }
     224                 :            : 
     225                 :    3786631 :   DeltaRational& operator+=(const DeltaRational& other)
     226                 :            :   {
     227                 :    3786631 :     c += other.c;
     228                 :    3786631 :     k += other.k;
     229                 :            : 
     230                 :    3786631 :     return *(this);
     231                 :            :   }
     232                 :            : 
     233                 :            :   DeltaRational& operator/=(const Rational& a)
     234                 :            :   {
     235                 :            :     Assert(!a.isZero());
     236                 :            :     c /= a;
     237                 :            :     k /= a;
     238                 :            :     return *(this);
     239                 :            :   }
     240                 :            : 
     241                 :   15582484 :   bool isIntegral() const
     242                 :            :   {
     243         [ +  + ]:   15582484 :     if (infinitesimalIsZero())
     244                 :            :     {
     245                 :   15572035 :       return getNoninfinitesimalPart().isIntegral();
     246                 :            :     }
     247                 :            :     else
     248                 :            :     {
     249                 :      10449 :       return false;
     250                 :            :     }
     251                 :            :   }
     252                 :            : 
     253                 :    1913220 :   Integer floor() const
     254                 :            :   {
     255         [ +  - ]:    1913220 :     if (getNoninfinitesimalPart().isIntegral())
     256                 :            :     {
     257         [ +  + ]:    1913220 :       if (getInfinitesimalPart().sgn() >= 0)
     258                 :            :       {
     259                 :      48589 :         return getNoninfinitesimalPart().getNumerator();
     260                 :            :       }
     261                 :            :       else
     262                 :            :       {
     263                 :    3729262 :         return getNoninfinitesimalPart().getNumerator() - Integer(1);
     264                 :            :       }
     265                 :            :     }
     266                 :            :     else
     267                 :            :     {
     268                 :          0 :       return getNoninfinitesimalPart().floor();
     269                 :            :     }
     270                 :            :   }
     271                 :            : 
     272                 :     150360 :   Integer ceiling() const
     273                 :            :   {
     274         [ +  - ]:     150360 :     if (getNoninfinitesimalPart().isIntegral())
     275                 :            :     {
     276         [ -  + ]:     150360 :       if (getInfinitesimalPart().sgn() <= 0)
     277                 :            :       {
     278                 :          0 :         return getNoninfinitesimalPart().getNumerator();
     279                 :            :       }
     280                 :            :       else
     281                 :            :       {
     282                 :     300720 :         return getNoninfinitesimalPart().getNumerator() + Integer(1);
     283                 :            :       }
     284                 :            :     }
     285                 :            :     else
     286                 :            :     {
     287                 :          0 :       return getNoninfinitesimalPart().ceiling();
     288                 :            :     }
     289                 :            :   }
     290                 :            : 
     291                 :            :   /** Only well defined if both this and y are integral. */
     292                 :            :   Integer euclidianDivideQuotient(const DeltaRational& y) const
     293                 :            :       /* throw(DeltaRationalException) */;
     294                 :            : 
     295                 :            :   /** Only well defined if both this and y are integral. */
     296                 :            :   Integer euclidianDivideRemainder(const DeltaRational& y) const
     297                 :            :       /* throw(DeltaRationalException) */;
     298                 :            : 
     299                 :            :   std::string toString() const;
     300                 :            : 
     301                 :    3185672 :   Rational substituteDelta(const Rational& d) const
     302                 :            :   {
     303                 :    6371344 :     return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
     304                 :            :   }
     305                 :            : 
     306                 :            :   /**
     307                 :            :    * Computes a sufficient upperbound to separate two DeltaRationals.
     308                 :            :    * This value is stored in res.
     309                 :            :    * For any rational d such that
     310                 :            :    *   0 < d < res
     311                 :            :    * then
     312                 :            :    *   a < b if and only if substituteDelta(a, d) < substituteDelta(b,d).
     313                 :            :    * (Similar relationships hold for for a == b and a > b.)
     314                 :            :    * Precondition: res > 0
     315                 :            :    */
     316                 :            :   static void seperatingDelta(Rational& res,
     317                 :            :                               const DeltaRational& a,
     318                 :            :                               const DeltaRational& b);
     319                 :            : 
     320                 :            :   uint32_t complexity() const { return c.complexity() + k.complexity(); }
     321                 :            : 
     322                 :        158 :   double approx(double deltaSub) const
     323                 :            :   {
     324                 :        158 :     double maj = getNoninfinitesimalPart().getDouble();
     325                 :        158 :     double min = deltaSub * (getInfinitesimalPart().getDouble());
     326                 :        158 :     return maj + min;
     327                 :            :   }
     328                 :            : };
     329                 :            : 
     330                 :            : std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
     331                 :            : 
     332                 :            : }  // namespace cvc5::internal