1 /********************* */ 2 /*! \file cardinality.h 3 ** \verbatim 4 ** Top contributors (to current version): 5 ** Morgan Deters, Tim King, Andrew Reynolds 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 ** Simple class to represent a cardinality; used by the CVC4 type system 15 ** give the cardinality of sorts. 16 **/ 17 18 #include "cvc4_public.h" 19 20 #ifndef __CVC4__CARDINALITY_H 21 #define __CVC4__CARDINALITY_H 22 23 #include <iostream> 24 #include <utility> 25 26 #include "base/exception.h" 27 #include "util/integer.h" 28 29 namespace CVC4 { 30 31 /** 32 * Representation for a Beth number, used only to construct 33 * Cardinality objects. 34 */ 35 class CVC4_PUBLIC CardinalityBeth { 36 Integer d_index; 37 38 public: 39 CardinalityBeth(const Integer& beth); 40 getNumber()41 const Integer& getNumber() const { return d_index; } 42 43 }; /* class CardinalityBeth */ 44 45 /** 46 * Representation for an unknown cardinality. 47 */ 48 class CVC4_PUBLIC CardinalityUnknown { 49 public: CardinalityUnknown()50 CardinalityUnknown() {} ~CardinalityUnknown()51 ~CardinalityUnknown() {} 52 }; /* class CardinalityUnknown */ 53 54 /** 55 * A simple representation of a cardinality. We store an 56 * arbitrary-precision integer for finite cardinalities, and we 57 * distinguish infinite cardinalities represented as Beth numbers. 58 */ 59 class CVC4_PUBLIC Cardinality { 60 /** Cardinality of the integers */ 61 static const Integer s_intCard; 62 63 /** Cardinality of the reals */ 64 static const Integer s_realCard; 65 66 /** A representation for unknown cardinality */ 67 static const Integer s_unknownCard; 68 69 /** A representation for large, finite cardinality */ 70 static const Integer s_largeFiniteCard; 71 72 /** 73 * In the case of finite cardinality, this is > 0, and is equal to 74 * the cardinality+1. If infinite, it is < 0, and is Beth[|card|-1]. 75 * That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc. 76 * If this field is 0, the cardinality is unknown. 77 * 78 * We impose a ceiling on finite cardinalities of 2^64. If this field 79 * is >= 2^64 + 1, we consider it at "ceiling" cardinality, and 80 * comparisons between all such cardinalities result in "unknown." 81 */ 82 Integer d_card; 83 84 public: 85 /** The cardinality of the set of integers. */ 86 static const Cardinality INTEGERS; 87 88 /** The cardinality of the set of real numbers. */ 89 static const Cardinality REALS; 90 91 /** The unknown cardinality */ 92 static const Cardinality UNKNOWN_CARD; 93 94 /** Used as a result code for Cardinality::compare(). */ 95 enum CVC4_PUBLIC CardinalityComparison { 96 LESS, 97 EQUAL, 98 GREATER, 99 UNKNOWN 100 }; /* enum CardinalityComparison */ 101 102 /** 103 * Construct a finite cardinality equal to the integer argument. 104 * The argument must be nonnegative. If we change this to an 105 * "unsigned" argument to enforce the restriction, we mask some 106 * errors that automatically convert, like "Cardinality(-1)". 107 */ 108 Cardinality(long card); 109 110 /** 111 * Construct a finite cardinality equal to the integer argument. 112 * The argument must be nonnegative. 113 */ 114 Cardinality(const Integer& card); 115 116 /** 117 * Construct an infinite cardinality equal to the given Beth number. 118 */ Cardinality(CardinalityBeth beth)119 Cardinality(CardinalityBeth beth) : d_card(-beth.getNumber() - 1) {} 120 121 /** 122 * Construct an unknown cardinality. 123 */ Cardinality(CardinalityUnknown)124 Cardinality(CardinalityUnknown) : d_card(0) {} 125 126 /** 127 * Returns true iff this cardinality is unknown. "Unknown" in this 128 * sense means that the cardinality is completely unknown; it might 129 * be finite, or infinite---anything. Large, finite cardinalities 130 * at the "ceiling" return "false" for isUnknown() and true for 131 * isFinite() and isLargeFinite(). 132 */ isUnknown()133 bool isUnknown() const { return d_card == 0; } 134 135 /** Returns true iff this cardinality is finite. */ isFinite()136 bool isFinite() const { return d_card > 0; } 137 /** Returns true iff this cardinality is one */ isOne()138 bool isOne() const { return d_card == 2; } 139 /** 140 * Returns true iff this cardinality is finite and large (i.e., 141 * at the ceiling of representable finite cardinalities). 142 */ isLargeFinite()143 bool isLargeFinite() const { return d_card >= s_largeFiniteCard; } 144 145 /** Returns true iff this cardinality is infinite. */ isInfinite()146 bool isInfinite() const { return d_card < 0; } 147 148 /** 149 * Returns true iff this cardinality is finite or countably 150 * infinite. 151 */ isCountable()152 bool isCountable() const { return isFinite() || d_card == s_intCard; } 153 154 /** 155 * In the case that this cardinality is finite, return its 156 * cardinality. (If this cardinality is infinite, this function 157 * throws an IllegalArgumentException.) 158 */ 159 Integer getFiniteCardinality() const; 160 161 /** 162 * In the case that this cardinality is infinite, return its Beth 163 * number. (If this cardinality is finite, this function throws an 164 * IllegalArgumentException.) 165 */ 166 Integer getBethNumber() const; 167 168 /** Assigning addition of this cardinality with another. */ 169 Cardinality& operator+=(const Cardinality& c); 170 171 /** Assigning multiplication of this cardinality with another. */ 172 Cardinality& operator*=(const Cardinality& c); 173 174 /** Assigning exponentiation of this cardinality with another. */ 175 Cardinality& operator^=(const Cardinality& c); 176 177 /** Add two cardinalities. */ 178 Cardinality operator+(const Cardinality& c) const { 179 Cardinality card(*this); 180 card += c; 181 return card; 182 } 183 184 /** Multiply two cardinalities. */ 185 Cardinality operator*(const Cardinality& c) const { 186 Cardinality card(*this); 187 card *= c; 188 return card; 189 } 190 191 /** 192 * Exponentiation of two cardinalities. 193 */ 194 Cardinality operator^(const Cardinality& c) const { 195 Cardinality card(*this); 196 card ^= c; 197 return card; 198 } 199 200 /** 201 * Compare two cardinalities. This can return UNKNOWN if two 202 * finite cardinalities are at the ceiling (and thus not precisely 203 * represented), or if one or the other is the special "unknown" 204 * cardinality. 205 */ 206 Cardinality::CardinalityComparison compare(const Cardinality& c) const; 207 208 /** 209 * Return a string representation of this cardinality. 210 */ 211 std::string toString() const; 212 213 /** 214 * Compare two cardinalities and if it is known that the current 215 * cardinality is smaller or equal to c, it returns true. 216 */ 217 bool knownLessThanOrEqual(const Cardinality& c) const; 218 }; /* class Cardinality */ 219 220 /** Print an element of the InfiniteCardinality enumeration. */ 221 std::ostream& operator<<(std::ostream& out, CardinalityBeth b) CVC4_PUBLIC; 222 223 /** Print a cardinality in a human-readable fashion. */ 224 std::ostream& operator<<(std::ostream& out, const Cardinality& c) CVC4_PUBLIC; 225 226 } /* CVC4 namespace */ 227 228 #endif /* __CVC4__CARDINALITY_H */ 229