Branch data     Line data    Source code

       1                 :            : /******************************************************************************
       2                 :            :  * Top contributors (to current version):
       3                 :            :  *   Morgan Deters, Tim King, 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                 :            :  * Representation of cardinality.
      14                 :            :  *
      15                 :            :  * Implementation of a simple class to represent a cardinality.
      16                 :            :  */
      17                 :            : 
      18                 :            : #include "util/cardinality.h"
      19                 :            : 
      20                 :            : #include <ostream>
      21                 :            : #include <sstream>
      22                 :            : 
      23                 :            : #include "base/check.h"
      24                 :            : #include "base/exception.h"
      25                 :            : 
      26                 :            : namespace cvc5::internal {
      27                 :            : 
      28                 :            : const Integer Cardinality::s_unknownCard(0);
      29                 :            : const Integer Cardinality::s_intCard(-1);
      30                 :            : const Integer Cardinality::s_realCard(-2);
      31                 :            : const Integer Cardinality::s_largeFiniteCard(
      32                 :            :     Integer("18446744073709551617"));  // 2^64 + 1
      33                 :            : 
      34                 :            : const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
      35                 :            : const Cardinality Cardinality::REALS(CardinalityBeth(1));
      36                 :            : const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
      37                 :            : 
      38                 :      59065 : CardinalityBeth::CardinalityBeth(const Integer& beth) : d_index(beth) {
      39 [ -  + ][ -  - ]:     118130 :   Assert(beth >= 0) << "Beth index must be a nonnegative integer, not "
      40 [ -  + ][ -  + ]:      59065 :                     << beth.toString().c_str();
                 [ -  - ]
      41                 :      59065 : }
      42                 :            : 
      43                 :      27054 : Cardinality::Cardinality(long card) : d_card(card) {
      44 [ -  + ][ -  + ]:      27054 :   Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
                 [ -  - ]
      45                 :          0 :                     << card;
      46                 :      27054 :   d_card += 1;
      47                 :      27054 : }
      48                 :            : 
      49                 :       2039 : Cardinality::Cardinality(const Integer& card) : d_card(card) {
      50 [ -  + ][ -  - ]:       4078 :   Assert(card >= 0) << "Cardinality must be a nonnegative integer, not "
      51 [ -  + ][ -  + ]:       2039 :                     << card.toString().c_str();
                 [ -  - ]
      52                 :       2039 :   d_card += 1;
      53                 :       2039 : }
      54                 :            : 
      55                 :       7889 : Integer Cardinality::getFiniteCardinality() const {
      56 [ -  + ][ -  + ]:       7889 :   Assert(isFinite()) << "This cardinality is not finite.";
                 [ -  - ]
      57 [ -  + ][ -  + ]:       7889 :   Assert(!isLargeFinite())
                 [ -  - ]
      58                 :          0 :       << "This cardinality is finite, but too large to represent.";
      59                 :       7889 :   return d_card - 1;
      60                 :            : }
      61                 :            : 
      62                 :          8 : Integer Cardinality::getBethNumber() const {
      63 [ +  - ][ +  - ]:         16 :   Assert(!isFinite() && !isUnknown())
         [ -  + ][ -  - ]
      64                 :          0 :       << "This cardinality is not infinite (or is unknown).";
      65                 :         16 :   return -d_card - 1;
      66                 :            : }
      67                 :            : 
      68                 :       2066 : Cardinality& Cardinality::operator+=(const Cardinality& c) {
      69         [ -  + ]:       2066 :   if (isUnknown()) {
      70                 :          0 :     return *this;
      71         [ -  + ]:       2066 :   } else if (c.isUnknown()) {
      72                 :          0 :     d_card = s_unknownCard;
      73                 :          0 :     return *this;
      74                 :            :   }
      75                 :            : 
      76 [ +  + ][ -  + ]:       2066 :   if (c.isFinite() && isLargeFinite()) {
                 [ -  + ]
      77                 :          0 :     return *this;
      78 [ +  + ][ -  + ]:       2066 :   } else if (isFinite() && c.isLargeFinite()) {
                 [ -  + ]
      79                 :          0 :     d_card = s_largeFiniteCard;
      80                 :          0 :     return *this;
      81                 :            :   }
      82                 :            : 
      83 [ +  + ][ +  + ]:       2066 :   if (isFinite() && c.isFinite()) {
                 [ +  + ]
      84                 :       2046 :     d_card += c.d_card - 1;
      85                 :       2046 :     return *this;
      86                 :            :   }
      87         [ +  + ]:         20 :   if (compare(c) == LESS) {
      88                 :         10 :     return *this = c;
      89                 :            :   } else {
      90                 :         10 :     return *this;
      91                 :            :   }
      92                 :            : 
      93                 :            :   Unreachable();
      94                 :            : }
      95                 :            : 
      96                 :            : /** Assigning multiplication of this cardinality with another. */
      97                 :        879 : Cardinality& Cardinality::operator*=(const Cardinality& c) {
      98         [ -  + ]:        879 :   if (isUnknown()) {
      99                 :          0 :     return *this;
     100         [ -  + ]:        879 :   } else if (c.isUnknown()) {
     101                 :          0 :     d_card = s_unknownCard;
     102                 :          0 :     return *this;
     103                 :            :   }
     104                 :            : 
     105 [ +  + ][ -  + ]:        879 :   if (c.isFinite() && isLargeFinite()) {
                 [ -  + ]
     106                 :          0 :     return *this;
     107 [ +  + ][ -  + ]:        879 :   } else if (isFinite() && c.isLargeFinite()) {
                 [ -  + ]
     108                 :          0 :     d_card = s_largeFiniteCard;
     109                 :          0 :     return *this;
     110                 :            :   }
     111                 :            : 
     112                 :        879 :   if (compare(0) == EQUAL || c.compare(0) == EQUAL) {
     113                 :          3 :     return *this = 0;
     114 [ +  + ][ +  + ]:        876 :   } else if (!isFinite() || !c.isFinite()) {
                 [ +  + ]
     115         [ +  + ]:         69 :     if (compare(c) == LESS) {
     116                 :         46 :       return *this = c;
     117                 :            :     } else {
     118                 :         23 :       return *this;
     119                 :            :     }
     120                 :            :   } else {
     121                 :        807 :     d_card -= 1;
     122                 :        807 :     d_card *= c.d_card - 1;
     123                 :        807 :     d_card += 1;
     124                 :        807 :     return *this;
     125                 :            :   }
     126                 :            : 
     127                 :            :   Unreachable();
     128                 :            : }
     129                 :            : 
     130                 :            : /** Assigning exponentiation of this cardinality with another. */
     131                 :        446 : Cardinality& Cardinality::operator^=(const Cardinality& c) {
     132         [ -  + ]:        446 :   if (isUnknown()) {
     133                 :          0 :     return *this;
     134         [ -  + ]:        446 :   } else if (c.isUnknown()) {
     135                 :          0 :     d_card = s_unknownCard;
     136                 :          0 :     return *this;
     137                 :            :   }
     138                 :            : 
     139 [ +  + ][ -  + ]:        446 :   if (c.isFinite() && isLargeFinite()) {
                 [ -  + ]
     140                 :          0 :     return *this;
     141 [ +  + ][ -  + ]:        446 :   } else if (isFinite() && c.isLargeFinite()) {
                 [ -  + ]
     142                 :          0 :     d_card = s_largeFiniteCard;
     143                 :          0 :     return *this;
     144                 :            :   }
     145                 :            : 
     146         [ +  + ]:        446 :   if (c.compare(0) == EQUAL) {
     147                 :            :     // (anything) ^ 0 == 1
     148                 :          6 :     d_card = 2;  // remember, +1 for finite cardinalities
     149                 :          6 :     return *this;
     150         [ +  + ]:        440 :   } else if (compare(0) == EQUAL) {
     151                 :            :     // 0 ^ (>= 1) == 0
     152                 :          4 :     return *this;
     153         [ +  + ]:        436 :   } else if (compare(1) == EQUAL) {
     154                 :            :     // 1 ^ (>= 1) == 1
     155                 :         26 :     return *this;
     156         [ +  + ]:        410 :   } else if (c.compare(1) == EQUAL) {
     157                 :            :     // (anything) ^ 1 == (that thing)
     158                 :          3 :     return *this;
     159 [ +  + ][ +  + ]:        407 :   } else if (isFinite() && c.isFinite()) {
                 [ +  + ]
     160                 :            :     // finite ^ finite == finite
     161                 :            :     try {
     162                 :            :       // Note: can throw an assertion if c is too big for
     163                 :            :       // exponentiation
     164                 :        160 :       if (d_card - 1 >= 2 && c.d_card - 1 >= 64) {
     165                 :            :         // don't bother, it's too large anyways
     166                 :          8 :         d_card = s_largeFiniteCard;
     167                 :            :       } else {
     168                 :        152 :         d_card = (d_card - 1).pow(c.d_card.getUnsignedInt() - 1) + 1;
     169                 :            :       }
     170                 :          0 :     } catch (IllegalArgumentException&) {
     171                 :          0 :       d_card = s_largeFiniteCard;
     172                 :            :     }
     173                 :        160 :     return *this;
     174 [ +  + ][ +  + ]:        247 :   } else if (!isFinite() && c.isFinite()) {
                 [ +  + ]
     175                 :            :     // inf ^ finite == inf
     176                 :         14 :     return *this;
     177                 :            :   } else {
     178                 :        466 :     Assert(compare(2) != LESS && !c.isFinite())
     179                 :          0 :         << "fall-through case not as expected:\n"
     180                 :          0 :         << this << "\n"
     181                 :            :         << c;
     182                 :            :     // (>= 2) ^ beth_k == beth_(k+1)
     183                 :            :     // unless the base is already > the exponent
     184         [ +  + ]:        233 :     if (compare(c) == GREATER) {
     185                 :          8 :       return *this;
     186                 :            :     }
     187                 :        225 :     d_card = c.d_card - 1;
     188                 :        225 :     return *this;
     189                 :            :   }
     190                 :            : 
     191                 :            :   Unreachable();
     192                 :            : }
     193                 :            : 
     194                 :      17464 : Cardinality::CardinalityComparison Cardinality::compare(
     195                 :            :     const Cardinality& c) const {
     196 [ +  - ][ -  + ]:      17464 :   if (isUnknown() || c.isUnknown()) {
                 [ -  + ]
     197                 :          0 :     return UNKNOWN;
     198         [ +  + ]:      17464 :   } else if (isLargeFinite()) {
     199         [ +  + ]:         84 :     if (c.isLargeFinite()) {
     200                 :          5 :       return UNKNOWN;
     201         [ +  + ]:         79 :     } else if (c.isFinite()) {
     202                 :         65 :       return GREATER;
     203                 :            :     } else {
     204 [ -  + ][ -  + ]:         14 :       Assert(c.isInfinite());
                 [ -  - ]
     205                 :         14 :       return LESS;
     206                 :            :     }
     207         [ +  + ]:      17380 :   } else if (c.isLargeFinite()) {
     208         [ -  + ]:          6 :     if (isLargeFinite()) {
     209                 :          0 :       return UNKNOWN;
     210         [ +  + ]:          6 :     } else if (isFinite()) {
     211                 :          2 :       return LESS;
     212                 :            :     } else {
     213 [ -  + ][ -  + ]:          4 :       Assert(isInfinite());
                 [ -  - ]
     214                 :          4 :       return GREATER;
     215                 :            :     }
     216         [ +  + ]:      17374 :   } else if (isInfinite()) {
     217         [ +  + ]:       1585 :     if (c.isFinite()) {
     218                 :       1250 :       return GREATER;
     219                 :            :     } else {
     220 [ +  + ][ +  + ]:        335 :       return d_card < c.d_card ? GREATER : (d_card == c.d_card ? EQUAL : LESS);
     221                 :            :     }
     222         [ +  + ]:      15789 :   } else if (c.isInfinite()) {
     223 [ -  + ][ -  + ]:         88 :     Assert(isFinite());
                 [ -  - ]
     224                 :         88 :     return LESS;
     225                 :            :   } else {
     226 [ +  - ][ +  - ]:      31402 :     Assert(isFinite() && !isLargeFinite());
         [ -  + ][ -  - ]
     227 [ +  - ][ +  - ]:      31402 :     Assert(c.isFinite() && !c.isLargeFinite());
         [ -  + ][ -  - ]
     228 [ +  + ][ +  + ]:      15701 :     return d_card < c.d_card ? LESS : (d_card == c.d_card ? EQUAL : GREATER);
     229                 :            :   }
     230                 :            : 
     231                 :            :   Unreachable();
     232                 :            : }
     233                 :            : 
     234                 :          0 : bool Cardinality::knownLessThanOrEqual(const Cardinality& c) const {
     235                 :          0 :   CardinalityComparison cmp = this->compare(c);
     236 [ -  - ][ -  - ]:          0 :   return cmp == LESS || cmp == EQUAL;
     237                 :            : }
     238                 :            : 
     239                 :          0 : std::string Cardinality::toString() const {
     240                 :          0 :   std::stringstream ss;
     241                 :          0 :   ss << *this;
     242                 :          0 :   return ss.str();
     243                 :            : }
     244                 :            : 
     245                 :          1 : std::ostream& operator<<(std::ostream& out, CardinalityBeth b) {
     246                 :          1 :   out << "beth[" << b.getNumber() << ']';
     247                 :            : 
     248                 :          1 :   return out;
     249                 :            : }
     250                 :            : 
     251                 :          1 : std::ostream& operator<<(std::ostream& out, const Cardinality& c) {
     252         [ -  + ]:          1 :   if (c.isUnknown()) {
     253                 :          0 :     out << "Cardinality::UNKNOWN";
     254         [ -  + ]:          1 :   } else if (c.isFinite()) {
     255                 :          0 :     out << c.getFiniteCardinality();
     256                 :            :   } else {
     257                 :          1 :     out << CardinalityBeth(c.getBethNumber());
     258                 :            :   }
     259                 :            : 
     260                 :          1 :   return out;
     261                 :            : }
     262                 :            : 
     263                 :            : }  // namespace cvc5::internal