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                 :            :  * Representation of cardinality.
      11                 :            :  *
      12                 :            :  * Implementation of a simple class to represent a cardinality.
      13                 :            :  */
      14                 :            : 
      15                 :            : #include "util/cardinality.h"
      16                 :            : 
      17                 :            : #include <ostream>
      18                 :            : #include <sstream>
      19                 :            : 
      20                 :            : #include "base/check.h"
      21                 :            : #include "base/exception.h"
      22                 :            : 
      23                 :            : namespace cvc5::internal {
      24                 :            : 
      25                 :            : const Integer Cardinality::s_unknownCard(0);
      26                 :            : const Integer Cardinality::s_intCard(-1);
      27                 :            : const Integer Cardinality::s_realCard(-2);
      28                 :            : const Integer Cardinality::s_largeFiniteCard(
      29                 :            :     Integer("18446744073709551617"));  // 2^64 + 1
      30                 :            : 
      31                 :            : const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
      32                 :            : const Cardinality Cardinality::REALS(CardinalityBeth(1));
      33                 :            : const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
      34                 :            : 
      35                 :      59145 : CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth)
      36                 :            : {
      37 [ -  + ][ -  - ]:     118290 :   Assert(beth >= 0) << "Beth index must be a nonnegative integer, not "
      38 [ -  + ][ -  + ]:      59145 :                     << beth.toString().c_str();
                 [ -  - ]
      39                 :      59145 : }
      40                 :            : 
      41                 :      29401 : Cardinality::Cardinality(long card) : d_card(card)
      42                 :            : {
      43 [ -  + ][ -  + ]:      29401 :   Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
                 [ -  - ]
      44                 :          0 :                     << card;
      45                 :      29401 :   d_card += 1;
      46                 :      29401 : }
      47                 :            : 
      48                 :       2110 : Cardinality::Cardinality(const Integer& card) : d_card(card)
      49                 :            : {
      50 [ -  + ][ -  - ]:       4220 :   Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
      51 [ -  + ][ -  + ]:       2110 :                     << card.toString().c_str();
                 [ -  - ]
      52                 :       2110 :   d_card += 1;
      53                 :       2110 : }
      54                 :            : 
      55                 :       7743 : Integer Cardinality::getFiniteCardinality() const
      56                 :            : {
      57 [ -  + ][ -  + ]:       7743 :   Assert(isFinite()) << "This cardinality is not finite.";
                 [ -  - ]
      58 [ -  + ][ -  + ]:       7743 :   Assert(!isLargeFinite())
                 [ -  - ]
      59                 :          0 :       << "This cardinality is finite, but too large to represent.";
      60                 :       7743 :   return d_card - 1;
      61                 :            : }
      62                 :            : 
      63                 :          8 : Integer Cardinality::getBethNumber() const
      64                 :            : {
      65 [ +  - ][ +  - ]:          8 :   Assert(!isFinite() && !isUnknown())
         [ -  + ][ -  + ]
                 [ -  - ]
      66                 :          0 :       << "This cardinality is not infinite (or is unknown).";
      67                 :         16 :   return -d_card - 1;
      68                 :            : }
      69                 :            : 
      70                 :       2042 : Cardinality& Cardinality::operator+=(const Cardinality& c)
      71                 :            : {
      72         [ -  + ]:       2042 :   if (isUnknown())
      73                 :            :   {
      74                 :          0 :     return *this;
      75                 :            :   }
      76         [ -  + ]:       2042 :   else if (c.isUnknown())
      77                 :            :   {
      78                 :          0 :     d_card = s_unknownCard;
      79                 :          0 :     return *this;
      80                 :            :   }
      81                 :            : 
      82 [ +  + ][ -  + ]:       2042 :   if (c.isFinite() && isLargeFinite())
                 [ -  + ]
      83                 :            :   {
      84                 :          0 :     return *this;
      85                 :            :   }
      86 [ +  + ][ -  + ]:       2042 :   else if (isFinite() && c.isLargeFinite())
                 [ -  + ]
      87                 :            :   {
      88                 :          0 :     d_card = s_largeFiniteCard;
      89                 :          0 :     return *this;
      90                 :            :   }
      91                 :            : 
      92 [ +  + ][ +  + ]:       2042 :   if (isFinite() && c.isFinite())
                 [ +  + ]
      93                 :            :   {
      94                 :       2022 :     d_card += c.d_card - 1;
      95                 :       2022 :     return *this;
      96                 :            :   }
      97         [ +  + ]:         20 :   if (compare(c) == LESS)
      98                 :            :   {
      99                 :         10 :     return *this = c;
     100                 :            :   }
     101                 :            :   else
     102                 :            :   {
     103                 :         10 :     return *this;
     104                 :            :   }
     105                 :            : 
     106                 :            :   Unreachable();
     107                 :            : }
     108                 :            : 
     109                 :            : /** Assigning multiplication of this cardinality with another. */
     110                 :        829 : Cardinality& Cardinality::operator*=(const Cardinality& c)
     111                 :            : {
     112         [ -  + ]:        829 :   if (isUnknown())
     113                 :            :   {
     114                 :          0 :     return *this;
     115                 :            :   }
     116         [ -  + ]:        829 :   else if (c.isUnknown())
     117                 :            :   {
     118                 :          0 :     d_card = s_unknownCard;
     119                 :          0 :     return *this;
     120                 :            :   }
     121                 :            : 
     122 [ +  + ][ -  + ]:        829 :   if (c.isFinite() && isLargeFinite())
                 [ -  + ]
     123                 :            :   {
     124                 :          0 :     return *this;
     125                 :            :   }
     126 [ +  + ][ -  + ]:        829 :   else if (isFinite() && c.isLargeFinite())
                 [ -  + ]
     127                 :            :   {
     128                 :          0 :     d_card = s_largeFiniteCard;
     129                 :          0 :     return *this;
     130                 :            :   }
     131                 :            : 
     132                 :        829 :   if (compare(0) == EQUAL || c.compare(0) == EQUAL)
     133                 :            :   {
     134                 :          3 :     return *this = 0;
     135                 :            :   }
     136 [ +  + ][ +  + ]:        826 :   else if (!isFinite() || !c.isFinite())
                 [ +  + ]
     137                 :            :   {
     138         [ +  + ]:         69 :     if (compare(c) == LESS)
     139                 :            :     {
     140                 :         46 :       return *this = c;
     141                 :            :     }
     142                 :            :     else
     143                 :            :     {
     144                 :         23 :       return *this;
     145                 :            :     }
     146                 :            :   }
     147                 :            :   else
     148                 :            :   {
     149                 :        757 :     d_card -= 1;
     150                 :        757 :     d_card *= c.d_card - 1;
     151                 :        757 :     d_card += 1;
     152                 :        757 :     return *this;
     153                 :            :   }
     154                 :            : 
     155                 :            :   Unreachable();
     156                 :            : }
     157                 :            : 
     158                 :            : /** Assigning exponentiation of this cardinality with another. */
     159                 :        427 : Cardinality& Cardinality::operator^=(const Cardinality& c)
     160                 :            : {
     161         [ -  + ]:        427 :   if (isUnknown())
     162                 :            :   {
     163                 :          0 :     return *this;
     164                 :            :   }
     165         [ -  + ]:        427 :   else if (c.isUnknown())
     166                 :            :   {
     167                 :          0 :     d_card = s_unknownCard;
     168                 :          0 :     return *this;
     169                 :            :   }
     170                 :            : 
     171 [ +  + ][ -  + ]:        427 :   if (c.isFinite() && isLargeFinite())
                 [ -  + ]
     172                 :            :   {
     173                 :          0 :     return *this;
     174                 :            :   }
     175 [ +  + ][ -  + ]:        427 :   else if (isFinite() && c.isLargeFinite())
                 [ -  + ]
     176                 :            :   {
     177                 :          0 :     d_card = s_largeFiniteCard;
     178                 :          0 :     return *this;
     179                 :            :   }
     180                 :            : 
     181         [ +  + ]:        427 :   if (c.compare(0) == EQUAL)
     182                 :            :   {
     183                 :            :     // (anything) ^ 0 == 1
     184                 :          6 :     d_card = 2;  // remember, +1 for finite cardinalities
     185                 :          6 :     return *this;
     186                 :            :   }
     187         [ +  + ]:        421 :   else if (compare(0) == EQUAL)
     188                 :            :   {
     189                 :            :     // 0 ^ (>= 1) == 0
     190                 :          4 :     return *this;
     191                 :            :   }
     192         [ +  + ]:        417 :   else if (compare(1) == EQUAL)
     193                 :            :   {
     194                 :            :     // 1 ^ (>= 1) == 1
     195                 :         23 :     return *this;
     196                 :            :   }
     197         [ +  + ]:        394 :   else if (c.compare(1) == EQUAL)
     198                 :            :   {
     199                 :            :     // (anything) ^ 1 == (that thing)
     200                 :          3 :     return *this;
     201                 :            :   }
     202 [ +  + ][ +  + ]:        391 :   else if (isFinite() && c.isFinite())
                 [ +  + ]
     203                 :            :   {
     204                 :            :     // finite ^ finite == finite
     205                 :            :     try
     206                 :            :     {
     207                 :            :       // Note: can throw an assertion if c is too big for
     208                 :            :       // exponentiation
     209                 :        161 :       if (d_card - 1 >= 2 && c.d_card - 1 >= 64)
     210                 :            :       {
     211                 :            :         // don't bother, it's too large anyways
     212                 :          8 :         d_card = s_largeFiniteCard;
     213                 :            :       }
     214                 :            :       else
     215                 :            :       {
     216                 :        153 :         d_card = (d_card - 1).pow(c.d_card.getUnsignedInt() - 1) + 1;
     217                 :            :       }
     218                 :            :     }
     219         [ -  - ]:          0 :     catch (IllegalArgumentException&)
     220                 :            :     {
     221                 :          0 :       d_card = s_largeFiniteCard;
     222                 :          0 :     }
     223                 :        161 :     return *this;
     224                 :            :   }
     225 [ +  + ][ +  + ]:        230 :   else if (!isFinite() && c.isFinite())
                 [ +  + ]
     226                 :            :   {
     227                 :            :     // inf ^ finite == inf
     228                 :         14 :     return *this;
     229                 :            :   }
     230                 :            :   else
     231                 :            :   {
     232                 :        216 :     Assert(compare(2) != LESS && !c.isFinite())
     233                 :          0 :         << "fall-through case not as expected:\n"
     234                 :          0 :         << this << "\n"
     235                 :            :         << c;
     236                 :            :     // (>= 2) ^ beth_k == beth_(k+1)
     237                 :            :     // unless the base is already > the exponent
     238         [ +  + ]:        216 :     if (compare(c) == GREATER)
     239                 :            :     {
     240                 :          8 :       return *this;
     241                 :            :     }
     242                 :        208 :     d_card = c.d_card - 1;
     243                 :        208 :     return *this;
     244                 :            :   }
     245                 :            : 
     246                 :            :   Unreachable();
     247                 :            : }
     248                 :            : 
     249                 :      18745 : Cardinality::CardinalityComparison Cardinality::compare(
     250                 :            :     const Cardinality& c) const
     251                 :            : {
     252 [ +  - ][ -  + ]:      18745 :   if (isUnknown() || c.isUnknown())
                 [ -  + ]
     253                 :            :   {
     254                 :          0 :     return UNKNOWN;
     255                 :            :   }
     256         [ +  + ]:      18745 :   else if (isLargeFinite())
     257                 :            :   {
     258         [ +  + ]:         82 :     if (c.isLargeFinite())
     259                 :            :     {
     260                 :          5 :       return UNKNOWN;
     261                 :            :     }
     262         [ +  + ]:         77 :     else if (c.isFinite())
     263                 :            :     {
     264                 :         63 :       return GREATER;
     265                 :            :     }
     266                 :            :     else
     267                 :            :     {
     268 [ -  + ][ -  + ]:         14 :       Assert(c.isInfinite());
                 [ -  - ]
     269                 :         14 :       return LESS;
     270                 :            :     }
     271                 :            :   }
     272         [ +  + ]:      18663 :   else if (c.isLargeFinite())
     273                 :            :   {
     274         [ -  + ]:          6 :     if (isLargeFinite())
     275                 :            :     {
     276                 :          0 :       return UNKNOWN;
     277                 :            :     }
     278         [ +  + ]:          6 :     else if (isFinite())
     279                 :            :     {
     280                 :          2 :       return LESS;
     281                 :            :     }
     282                 :            :     else
     283                 :            :     {
     284 [ -  + ][ -  + ]:          4 :       Assert(isInfinite());
                 [ -  - ]
     285                 :          4 :       return GREATER;
     286                 :            :     }
     287                 :            :   }
     288         [ +  + ]:      18657 :   else if (isInfinite())
     289                 :            :   {
     290         [ +  + ]:       1480 :     if (c.isFinite())
     291                 :            :     {
     292                 :       1162 :       return GREATER;
     293                 :            :     }
     294                 :            :     else
     295                 :            :     {
     296 [ +  + ][ +  + ]:        318 :       return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
     297                 :            :     }
     298                 :            :   }
     299         [ +  + ]:      17177 :   else if (c.isInfinite())
     300                 :            :   {
     301 [ -  + ][ -  + ]:         88 :     Assert(isFinite());
                 [ -  - ]
     302                 :         88 :     return LESS;
     303                 :            :   }
     304                 :            :   else
     305                 :            :   {
     306 [ +  - ][ +  - ]:      17089 :     Assert(isFinite() && !isLargeFinite());
         [ -  + ][ -  + ]
                 [ -  - ]
     307 [ +  - ][ +  - ]:      17089 :     Assert(c.isFinite() && !c.isLargeFinite());
         [ -  + ][ -  + ]
                 [ -  - ]
     308 [ +  + ][ +  + ]:      17089 :     return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
     309                 :            :   }
     310                 :            : 
     311                 :            :   Unreachable();
     312                 :            : }
     313                 :            : 
     314                 :          0 : bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const
     315                 :            : {
     316                 :          0 :   CardinalityComparison cmp = this->compare(c);
     317 [ -  - ][ -  - ]:          0 :   return cmp == LESS || cmp == EQUAL;
     318                 :            : }
     319                 :            : 
     320                 :          0 : std::string Cardinality::toString() const
     321                 :            : {
     322                 :          0 :   std::stringstream ss;
     323                 :          0 :   ss << *this;
     324                 :          0 :   return ss.str();
     325                 :          0 : }
     326                 :            : 
     327                 :          1 : std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
     328                 :            : {
     329                 :          1 :   out << "beth[" << b.getNumber() << ']';
     330                 :            : 
     331                 :          1 :   return out;
     332                 :            : }
     333                 :            : 
     334                 :          1 : std::ostream& operator<<(std::ostream& out, const Cardinality& c)
     335                 :            : {
     336         [ -  + ]:          1 :   if (c.isUnknown())
     337                 :            :   {
     338                 :          0 :     out << "Cardinality::UNKNOWN";
     339                 :            :   }
     340         [ -  + ]:          1 :   else if (c.isFinite())
     341                 :            :   {
     342                 :          0 :     out << c.getFiniteCardinality();
     343                 :            :   }
     344                 :            :   else
     345                 :            :   {
     346                 :          1 :     out << CardinalityBeth(c.getBethNumber());
     347                 :            :   }
     348                 :            : 
     349                 :          1 :   return out;
     350                 :            : }
     351                 :            : 
     352                 :            : }  // namespace cvc5::internal