20 #ifndef __CVC4__CARDINALITY_H 21 #define __CVC4__CARDINALITY_H 26 #include "util/integer.h" 41 "Beth index must be a nonnegative integer, not %s.",
70 static const Integer s_realCard;
73 static const Integer s_unknownCard;
76 static const Integer s_largeFiniteCard;
117 "Cardinality must be a nonnegative integer, not %ld.", card);
127 "Cardinality must be a nonnegative integer, not %s.",
165 return d_card >= s_largeFiniteCard;
178 return isFinite() || d_card == s_intCard;
187 CheckArgument(isFinite(), *
this,
"This cardinality is not finite.");
188 CheckArgument(!isLargeFinite(), *
this,
"This cardinality is finite, but too large to represent.");
199 "This cardinality is not infinite (or is unknown).");
246 std::string toString()
const throw();
252 bool knownLessThanOrEqual(
const Cardinality& c)
const throw();
static const Cardinality INTEGERS
The cardinality of the set of integers.
std::string toString(int base=10) const
bool isCountable() const
Returns true iff this cardinality is finite or countably infinite.
Integer getFiniteCardinality() const
In the case that this cardinality is finite, return its cardinality.
Cardinality operator^(const Cardinality &c) const
Exponentiation of two cardinalities.
CardinalityBeth(const Integer &beth)
int compare(const Expr &e1, const Expr &e2)
Cardinality(const Integer &card)
Construct a finite cardinality equal to the integer argument.
static const Cardinality UNKNOWN_CARD
The unknown cardinality.
A simple representation of a cardinality.
bool isLargeFinite() const
Returns true iff this cardinality is finite and large (i.e., at the ceiling of representable finite c...
void CheckArgument(bool cond, const T &arg, const char *fmt,...)
CVC4's exception base class and some associated utilities.
Cardinality(long card)
Construct a finite cardinality equal to the integer argument.
bool isInfinite() const
Returns true iff this cardinality is infinite.
Representation for a Beth number, used only to construct Cardinality objects.
std::ostream & operator<<(std::ostream &out, TypeConstant typeConstant)
Representation for an unknown cardinality.
bool isFinite() const
Returns true iff this cardinality is finite.
Macros that should be defined everywhere during the building of the libraries and driver binary...
Cardinality operator*(const Cardinality &c) const
Multiply two cardinalities.
bool isUnknown() const
Returns true iff this cardinality is unknown.
Cardinality operator+(const Cardinality &c) const
Add two cardinalities.
static const Cardinality REALS
The cardinality of the set of real numbers.
Cardinality(CardinalityUnknown)
Construct an unknown cardinality.
struct CVC4::options::out__option_t out
Cardinality(CardinalityBeth beth)
Construct an infinite cardinality equal to the given Beth number.
CardinalityComparison
Used as a result code for Cardinality::compare().
Integer getBethNumber() const
In the case that this cardinality is infinite, return its Beth number.
const Integer & getNumber() const