Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Tim King, Mathias Preiner, Aina Niemetz
       4                 :            :  *
       5                 :            :  * This file is part of the cvc5 project.
       6                 :            :  *
       7                 :            :  * Copyright (c) 2009-2025 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                 :            :  * [[ Add one-line brief description here ]]
      14                 :            :  *
      15                 :            :  * [[ Add lengthier description here ]]
      16                 :            :  * \todo document this file
      17                 :            :  */
      18                 :            : 
      19                 :            : #include "cvc5_private.h"
      20                 :            : 
      21                 :            : #pragma once
      22                 :            : 
      23                 :            : #include <ostream>
      24                 :            : 
      25                 :            : #include "base/check.h"
      26                 :            : #include "base/exception.h"
      27                 :            : #include "util/integer.h"
      28                 :            : #include "util/rational.h"
      29                 :            : 
      30                 :            : namespace cvc5::internal {
      31                 :            : 
      32                 :            : class DeltaRational;
      33                 :            : 
      34                 :            : class DeltaRationalException : public Exception {
      35                 :            :  public:
      36                 :            :   DeltaRationalException(const char* op,
      37                 :            :                          const DeltaRational& a,
      38                 :            :                          const DeltaRational& b);
      39                 :            :   ~DeltaRationalException() override;
      40                 :            : };
      41                 :            : 
      42                 :            : 
      43                 :            : /**
      44                 :            :  * A DeltaRational is a pair of rationals (c,k) that represent the number
      45                 :            :  *   c + kd
      46                 :            :  * where d is an implicit system wide symbolic infinitesimal.
      47                 :            :  */
      48                 :            : class DeltaRational {
      49                 :            : private:
      50                 :            :  cvc5::internal::Rational c;
      51                 :            :  cvc5::internal::Rational k;
      52                 :            : 
      53                 :            : public:
      54                 :    7192755 :   DeltaRational() : c(0,1), k(0,1) {}
      55                 :    8822365 :   DeltaRational(const cvc5::internal::Rational& base) : c(base), k(0, 1) {}
      56                 :   49250704 :   DeltaRational(const cvc5::internal::Rational& base, const cvc5::internal::Rational& coeff)
      57                 :   49250704 :       : c(base), k(coeff)
      58                 :            :   {
      59                 :   49250704 :   }
      60                 :            : 
      61                 :   47021307 :   const cvc5::internal::Rational& getInfinitesimalPart() const { return k; }
      62                 :            : 
      63                 :   49580554 :   const cvc5::internal::Rational& getNoninfinitesimalPart() const { return c; }
      64                 :            : 
      65                 :   14350232 :   int sgn() const {
      66                 :   14350232 :     int s = getNoninfinitesimalPart().sgn();
      67         [ +  + ]:   14350232 :     if(s == 0){
      68                 :    9836080 :       return infinitesimalSgn();
      69                 :            :     }else{
      70                 :    4514152 :       return s;
      71                 :            :     }
      72                 :            :   }
      73                 :            : 
      74                 :   15293882 :   int infinitesimalSgn() const {
      75                 :   15293882 :     return getInfinitesimalPart().sgn();
      76                 :            :   }
      77                 :            : 
      78                 :   21397361 :   bool infinitesimalIsZero() const {
      79                 :   21397361 :     return getInfinitesimalPart().isZero();
      80                 :            :   }
      81                 :            : 
      82                 :          6 :   bool noninfinitesimalIsZero() const {
      83                 :          6 :     return getNoninfinitesimalPart().isZero();
      84                 :            :   }
      85                 :            : 
      86                 :          0 :   bool isZero() const {
      87 [ -  - ][ -  - ]:          0 :     return noninfinitesimalIsZero() && infinitesimalIsZero();
      88                 :            :   }
      89                 :            : 
      90                 :            : 
      91                 :   24969575 :   int cmp(const DeltaRational& other) const{
      92                 :   24969575 :     int cmp = c.cmp(other.c);
      93         [ +  + ]:   24969575 :     if(cmp == 0){
      94                 :   11587492 :       return k.cmp(other.k);
      95                 :            :     }else{
      96                 :   13382083 :       return cmp;
      97                 :            :     }
      98                 :            :   }
      99                 :            : 
     100                 :   19471729 :   DeltaRational operator+(const DeltaRational& other) const{
     101                 :   19471729 :     cvc5::internal::Rational tmpC = c + other.c;
     102                 :   19471729 :     cvc5::internal::Rational tmpK = k + other.k;
     103                 :   38943458 :     return DeltaRational(tmpC, tmpK);
     104                 :   19471729 :   }
     105                 :            : 
     106                 :   25028595 :   DeltaRational operator*(const Rational& a) const{
     107                 :   25028595 :     cvc5::internal::Rational tmpC = a * c;
     108                 :   25028595 :     cvc5::internal::Rational tmpK = a * k;
     109                 :   50057190 :     return DeltaRational(tmpC, tmpK);
     110                 :   25028595 :   }
     111                 :            : 
     112                 :            : 
     113                 :            :   /**
     114                 :            :    * Multiplies (this->c + this->k * delta) * (a.c + a.k * delta)
     115                 :            :    * This can be done whenever this->k or a.k is 0.
     116                 :            :    * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
     117                 :            :    */
     118                 :     317470 :   DeltaRational operator*(const DeltaRational& a) const
     119                 :            :   /* throw(DeltaRationalException) */ {
     120         [ +  - ]:     317470 :     if(infinitesimalIsZero()){
     121                 :     317470 :       return a * (this->getNoninfinitesimalPart());
     122         [ -  - ]:          0 :     }else if(a.infinitesimalIsZero()){
     123                 :          0 :       return (*this) * a.getNoninfinitesimalPart();
     124                 :            :     }else{
     125                 :          0 :       throw DeltaRationalException("operator*", *this, a);
     126                 :            :     }
     127                 :            :   }
     128                 :            : 
     129                 :            : 
     130                 :    2756756 :   DeltaRational operator-(const DeltaRational& a) const{
     131                 :    2756756 :     cvc5::internal::Rational negOne(cvc5::internal::Integer(-1));
     132                 :    8270268 :     return *(this) + (a * negOne);
     133                 :    2756756 :   }
     134                 :            : 
     135                 :       2276 :   DeltaRational operator-() const{
     136                 :       4552 :     return DeltaRational(-c, -k);
     137                 :            :   }
     138                 :            : 
     139                 :    1446362 :   DeltaRational operator/(const Rational& a) const{
     140                 :    1446362 :     cvc5::internal::Rational tmpC = c / a;
     141                 :    1446362 :     cvc5::internal::Rational tmpK = k / a;
     142                 :    2892724 :     return DeltaRational(tmpC, tmpK);
     143                 :    1446362 :   }
     144                 :            : 
     145                 :            :   DeltaRational operator/(const Integer& a) const{
     146                 :            :     cvc5::internal::Rational tmpC = c / a;
     147                 :            :     cvc5::internal::Rational tmpK = k / a;
     148                 :            :     return DeltaRational(tmpC, tmpK);
     149                 :            :   }
     150                 :            : 
     151                 :            :   /**
     152                 :            :    * Divides (*this) / (a.c + a.k * delta)
     153                 :            :    * This can be done when a.k is 0 and a.c is non-zero.
     154                 :            :    * Otherwise, the result is not a DeltaRational and a DeltaRationalException is thrown.
     155                 :            :    */
     156                 :          0 :   DeltaRational operator/(const DeltaRational& a) const
     157                 :            :   /* throw(DeltaRationalException) */ {
     158         [ -  - ]:          0 :     if(a.infinitesimalIsZero()){
     159                 :          0 :       return (*this) / a.getNoninfinitesimalPart();
     160                 :            :     }else{
     161                 :          0 :       throw DeltaRationalException("operator/", *this, a);
     162                 :            :     }
     163                 :            :   }
     164                 :            : 
     165                 :            : 
     166                 :            :   DeltaRational abs() const {
     167                 :            :     if(sgn() >= 0){
     168                 :            :       return *this;
     169                 :            :     }else{
     170                 :            :       return (*this) * Rational(-1);
     171                 :            :     }
     172                 :            :   }
     173                 :            : 
     174                 :    4808272 :   bool operator==(const DeltaRational& other) const{
     175 [ +  + ][ +  + ]:    4808272 :     return (k == other.k) && (c == other.c);
     176                 :            :   }
     177                 :            : 
     178                 :     552780 :   bool operator!=(const DeltaRational& other) const{
     179                 :     552780 :     return !(*this == other);
     180                 :            :   }
     181                 :            : 
     182                 :            : 
     183                 :  140518695 :   bool operator<=(const DeltaRational& other) const{
     184                 :  140518695 :     int cmp = c.cmp(other.c);
     185 [ +  + ][ +  + ]:  140518695 :     return (cmp < 0) || ((cmp==0)&&(k <= other.k));
                 [ +  + ]
     186                 :            :   }
     187                 :  122206054 :   bool operator<(const DeltaRational& other) const{
     188                 :  122206054 :     return (other  > *this);
     189                 :            :   }
     190                 :    4139907 :   bool operator>=(const DeltaRational& other) const{
     191                 :    4139907 :     return (other <= *this);
     192                 :            :   }
     193                 :  126554766 :   bool operator>(const DeltaRational& other) const{
     194                 :  126554766 :     return !(*this <= other);
     195                 :            :   }
     196                 :            : 
     197                 :            :   int compare(const DeltaRational& other) const{
     198                 :            :     int cmpRes = c.cmp(other.c);
     199                 :            :     return (cmpRes != 0) ? cmpRes : (k.cmp(other.k));
     200                 :            :   }
     201                 :            : 
     202                 :   33667705 :   DeltaRational& operator=(const DeltaRational& other){
     203                 :   33667705 :     c = other.c;
     204                 :   33667705 :     k = other.k;
     205                 :   33667705 :     return *(this);
     206                 :            :   }
     207                 :            : 
     208                 :            :   DeltaRational& operator*=(const cvc5::internal::Rational& a)
     209                 :            :   {
     210                 :            :     c *=  a;
     211                 :            :     k *=  a;
     212                 :            : 
     213                 :            :     return *(this);
     214                 :            :   }
     215                 :            : 
     216                 :    6139967 :   DeltaRational& operator+=(const DeltaRational& other){
     217                 :    6139967 :     c += other.c;
     218                 :    6139967 :     k += other.k;
     219                 :            : 
     220                 :    6139967 :     return *(this);
     221                 :            :   }
     222                 :            : 
     223                 :            :   DeltaRational& operator/=(const Rational& a){
     224                 :            :     Assert(!a.isZero());
     225                 :            :     c /= a;
     226                 :            :     k /= a;
     227                 :            :     return *(this);
     228                 :            :   }
     229                 :            : 
     230                 :   18203351 :   bool isIntegral() const {
     231         [ +  + ]:   18203351 :     if(infinitesimalIsZero()){
     232                 :   18187549 :       return getNoninfinitesimalPart().isIntegral();
     233                 :            :     }else{
     234                 :      15802 :       return false;
     235                 :            :     }
     236                 :            :   }
     237                 :            : 
     238                 :    2489726 :   Integer floor() const {
     239         [ +  - ]:    2489726 :     if(getNoninfinitesimalPart().isIntegral()){
     240         [ +  + ]:    2489726 :       if(getInfinitesimalPart().sgn() >= 0){
     241                 :      41879 :         return getNoninfinitesimalPart().getNumerator();
     242                 :            :       }else{
     243                 :    4895694 :         return getNoninfinitesimalPart().getNumerator() - Integer(1);
     244                 :            :       }
     245                 :            :     }else{
     246                 :          0 :       return getNoninfinitesimalPart().floor();
     247                 :            :     }
     248                 :            :   }
     249                 :            : 
     250                 :     139993 :   Integer ceiling() const {
     251         [ +  - ]:     139993 :     if(getNoninfinitesimalPart().isIntegral()){
     252         [ -  + ]:     139993 :       if(getInfinitesimalPart().sgn() <= 0){
     253                 :          0 :         return getNoninfinitesimalPart().getNumerator();
     254                 :            :       }else{
     255                 :     279986 :         return getNoninfinitesimalPart().getNumerator() + Integer(1);
     256                 :            :       }
     257                 :            :     }else{
     258                 :          0 :       return getNoninfinitesimalPart().ceiling();
     259                 :            :     }
     260                 :            :   }
     261                 :            : 
     262                 :            :   /** Only well defined if both this and y are integral. */
     263                 :            :   Integer euclidianDivideQuotient(const DeltaRational& y) const
     264                 :            :       /* throw(DeltaRationalException) */;
     265                 :            : 
     266                 :            :   /** Only well defined if both this and y are integral. */
     267                 :            :   Integer euclidianDivideRemainder(const DeltaRational& y) const
     268                 :            :       /* throw(DeltaRationalException) */;
     269                 :            : 
     270                 :            :   std::string toString() const;
     271                 :            : 
     272                 :    3115235 :   Rational substituteDelta(const Rational& d) const{
     273                 :    6230470 :     return getNoninfinitesimalPart() + (d * getInfinitesimalPart());
     274                 :            :   }
     275                 :            : 
     276                 :            :   /**
     277                 :            :    * Computes a sufficient upperbound to separate two DeltaRationals.
     278                 :            :    * This value is stored in res.
     279                 :            :    * For any rational d such that
     280                 :            :    *   0 < d < res
     281                 :            :    * then
     282                 :            :    *   a < b if and only if substituteDelta(a, d) < substituteDelta(b,d).
     283                 :            :    * (Similar relationships hold for for a == b and a > b.)
     284                 :            :    * Precondition: res > 0
     285                 :            :    */
     286                 :            :   static void seperatingDelta(Rational& res, const DeltaRational& a, const DeltaRational& b);
     287                 :            : 
     288                 :            :   uint32_t complexity() const {
     289                 :            :     return c.complexity() + k.complexity();
     290                 :            :   }
     291                 :            : 
     292                 :         38 :   double approx(double deltaSub) const {
     293                 :         38 :     double maj = getNoninfinitesimalPart().getDouble();
     294                 :         38 :     double min = deltaSub * (getInfinitesimalPart().getDouble());
     295                 :         38 :     return maj + min;
     296                 :            :   }
     297                 :            : 
     298                 :            : 
     299                 :            : };
     300                 :            : 
     301                 :            : std::ostream& operator<<(std::ostream& os, const DeltaRational& n);
     302                 :            : 
     303                 :            : }  // namespace cvc5::internal