src/util/cardinality.cpp

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