cvc4-1.4
|
A simple representation of a cardinality. More...
#include <cardinality.h>
Public Types | |
enum | CardinalityComparison { LESS, EQUAL, GREATER, UNKNOWN } |
Used as a result code for Cardinality::compare(). More... | |
Public Member Functions | |
Cardinality (long card) | |
Construct a finite cardinality equal to the integer argument. More... | |
Cardinality (const Integer &card) | |
Construct a finite cardinality equal to the integer argument. More... | |
Cardinality (CardinalityBeth beth) | |
Construct an infinite cardinality equal to the given Beth number. More... | |
Cardinality (CardinalityUnknown) | |
Construct an unknown cardinality. More... | |
bool | isUnknown () const throw () |
Returns true iff this cardinality is unknown. More... | |
bool | isFinite () const throw () |
Returns true iff this cardinality is finite. More... | |
bool | isLargeFinite () const throw () |
Returns true iff this cardinality is finite and large (i.e., at the ceiling of representable finite cardinalities). More... | |
bool | isInfinite () const throw () |
Returns true iff this cardinality is infinite. More... | |
bool | isCountable () const throw () |
Returns true iff this cardinality is finite or countably infinite. More... | |
Integer | getFiniteCardinality () const throw (IllegalArgumentException) |
In the case that this cardinality is finite, return its cardinality. More... | |
Integer | getBethNumber () const throw (IllegalArgumentException) |
In the case that this cardinality is infinite, return its Beth number. More... | |
Cardinality & | operator+= (const Cardinality &c) throw () |
Assigning addition of this cardinality with another. More... | |
Cardinality & | operator*= (const Cardinality &c) throw () |
Assigning multiplication of this cardinality with another. More... | |
Cardinality & | operator^= (const Cardinality &c) throw () |
Assigning exponentiation of this cardinality with another. More... | |
Cardinality | operator+ (const Cardinality &c) const throw () |
Add two cardinalities. More... | |
Cardinality | operator* (const Cardinality &c) const throw () |
Multiply two cardinalities. More... | |
Cardinality | operator^ (const Cardinality &c) const throw () |
Exponentiation of two cardinalities. More... | |
Cardinality::CardinalityComparison | compare (const Cardinality &c) const throw () |
Compare two cardinalities. More... | |
std::string | toString () const throw () |
Return a string representation of this cardinality. More... | |
bool | knownLessThanOrEqual (const Cardinality &c) const throw () |
Compare two cardinalities and if it is known that the current cardinality is smaller or equal to c, it returns true. More... | |
Static Public Attributes | |
static const Cardinality | INTEGERS |
The cardinality of the set of integers. More... | |
static const Cardinality | REALS |
The cardinality of the set of real numbers. More... | |
static const Cardinality | UNKNOWN_CARD |
The unknown cardinality. More... | |
A simple representation of a cardinality.
We store an arbitrary-precision integer for finite cardinalities, and we distinguish infinite cardinalities represented as Beth numbers.
Definition at line 65 of file cardinality.h.
Used as a result code for Cardinality::compare().
Enumerator | |
---|---|
LESS | |
EQUAL | |
GREATER | |
UNKNOWN |
Definition at line 102 of file cardinality.h.
|
inline |
Construct a finite cardinality equal to the integer argument.
The argument must be nonnegative. If we change this to an "unsigned" argument to enforce the restriction, we mask some errors that automatically convert, like "Cardinality(-1)".
Definition at line 115 of file cardinality.h.
References CVC4::CheckArgument().
|
inline |
Construct a finite cardinality equal to the integer argument.
The argument must be nonnegative.
Definition at line 125 of file cardinality.h.
References CVC4::CheckArgument(), and CVC4::Integer::toString().
|
inline |
Construct an infinite cardinality equal to the given Beth number.
Definition at line 135 of file cardinality.h.
|
inline |
Construct an unknown cardinality.
Definition at line 141 of file cardinality.h.
Cardinality::CardinalityComparison CVC4::Cardinality::compare | ( | const Cardinality & | c | ) | const |
throw | ( | ||||
) |
Compare two cardinalities.
This can return UNKNOWN if two finite cardinalities are at the ceiling (and thus not precisely represented), or if one or the other is the special "unknown" cardinality.
|
inline |
In the case that this cardinality is infinite, return its Beth number.
(If this cardinality is finite, this function throws an IllegalArgumentException.)
Definition at line 197 of file cardinality.h.
References CVC4::CheckArgument().
|
inline |
In the case that this cardinality is finite, return its cardinality.
(If this cardinality is infinite, this function throws an IllegalArgumentException.)
Definition at line 186 of file cardinality.h.
References CVC4::CheckArgument().
|
inline |
Returns true iff this cardinality is finite or countably infinite.
Definition at line 177 of file cardinality.h.
|
inline |
Returns true iff this cardinality is finite.
Definition at line 156 of file cardinality.h.
|
inline |
Returns true iff this cardinality is infinite.
Definition at line 169 of file cardinality.h.
|
inline |
Returns true iff this cardinality is finite and large (i.e., at the ceiling of representable finite cardinalities).
Definition at line 164 of file cardinality.h.
|
inline |
Returns true iff this cardinality is unknown.
"Unknown" in this sense means that the cardinality is completely unknown; it might be finite, or infinite—anything. Large, finite cardinalities at the "ceiling" return "false" for isUnknown() and true for isFinite() and isLargeFinite().
Definition at line 151 of file cardinality.h.
bool CVC4::Cardinality::knownLessThanOrEqual | ( | const Cardinality & | c | ) | const |
throw | ( | ||||
) |
Compare two cardinalities and if it is known that the current cardinality is smaller or equal to c, it returns true.
|
inline |
Multiply two cardinalities.
Definition at line 220 of file cardinality.h.
Cardinality& CVC4::Cardinality::operator*= | ( | const Cardinality & | c | ) | |
throw | ( | ||||
) |
Assigning multiplication of this cardinality with another.
|
inline |
Add two cardinalities.
Definition at line 213 of file cardinality.h.
Cardinality& CVC4::Cardinality::operator+= | ( | const Cardinality & | c | ) | |
throw | ( | ||||
) |
Assigning addition of this cardinality with another.
|
inline |
Exponentiation of two cardinalities.
Definition at line 229 of file cardinality.h.
References CVC3::compare(), CVC4_PUBLIC, CVC4::operator<<(), and CVC4::options::out.
Cardinality& CVC4::Cardinality::operator^= | ( | const Cardinality & | c | ) | |
throw | ( | ||||
) |
Assigning exponentiation of this cardinality with another.
std::string CVC4::Cardinality::toString | ( | ) | const | |
throw | ( | |||
) |
Return a string representation of this cardinality.
|
static |
The cardinality of the set of integers.
Definition at line 93 of file cardinality.h.
|
static |
The cardinality of the set of real numbers.
Definition at line 96 of file cardinality.h.
|
static |
The unknown cardinality.
Definition at line 99 of file cardinality.h.