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