cvc4-1.3
CVC4::Cardinality Class Reference

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...
 
Cardinalityoperator+= (const Cardinality &c) throw ()
 Assigning addition of this cardinality with another. More...
 
Cardinalityoperator*= (const Cardinality &c) throw ()
 Assigning multiplication of this cardinality with another. More...
 
Cardinalityoperator^= (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...
 

Detailed Description

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.

Member Enumeration Documentation

Used as a result code for Cardinality::compare().

Enumerator
LESS 
EQUAL 
GREATER 
UNKNOWN 

Definition at line 102 of file cardinality.h.

Constructor & Destructor Documentation

CVC4::Cardinality::Cardinality ( long  card)
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().

CVC4::Cardinality::Cardinality ( const Integer card)
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().

CVC4::Cardinality::Cardinality ( CardinalityBeth  beth)
inline

Construct an infinite cardinality equal to the given Beth number.

Definition at line 135 of file cardinality.h.

CVC4::Cardinality::Cardinality ( CardinalityUnknown  )
inline

Construct an unknown cardinality.

Definition at line 141 of file cardinality.h.

Member Function Documentation

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.

Integer CVC4::Cardinality::getBethNumber ( ) const
throw (IllegalArgumentException
)
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().

Integer CVC4::Cardinality::getFiniteCardinality ( ) const
throw (IllegalArgumentException
)
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().

bool CVC4::Cardinality::isCountable ( ) const
throw (
)
inline

Returns true iff this cardinality is finite or countably infinite.

Definition at line 177 of file cardinality.h.

bool CVC4::Cardinality::isFinite ( ) const
throw (
)
inline

Returns true iff this cardinality is finite.

Definition at line 156 of file cardinality.h.

bool CVC4::Cardinality::isInfinite ( ) const
throw (
)
inline

Returns true iff this cardinality is infinite.

Definition at line 169 of file cardinality.h.

bool CVC4::Cardinality::isLargeFinite ( ) const
throw (
)
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.

bool CVC4::Cardinality::isUnknown ( ) const
throw (
)
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.

Cardinality CVC4::Cardinality::operator* ( const Cardinality c) const
throw (
)
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.

Cardinality CVC4::Cardinality::operator+ ( const Cardinality c) const
throw (
)
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.

Cardinality CVC4::Cardinality::operator^ ( const Cardinality c) const
throw (
)
inline

Exponentiation of two cardinalities.

Definition at line 229 of file cardinality.h.

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.

Field Documentation

const Cardinality CVC4::Cardinality::INTEGERS
static

The cardinality of the set of integers.

Definition at line 93 of file cardinality.h.

const Cardinality CVC4::Cardinality::REALS
static

The cardinality of the set of real numbers.

Definition at line 96 of file cardinality.h.

const Cardinality CVC4::Cardinality::UNKNOWN_CARD
static

The unknown cardinality.

Definition at line 99 of file cardinality.h.


The documentation for this class was generated from the following file: