summaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/util/cardinality.cpp118
-rw-r--r--src/util/cardinality.h84
2 files changed, 137 insertions, 65 deletions
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index 8aba4ad41..fd2ac3d08 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -23,10 +23,11 @@ namespace CVC4 {
const Integer Cardinality::s_unknownCard(0);
const Integer Cardinality::s_intCard(-1);
const Integer Cardinality::s_realCard(-2);
+const Integer Cardinality::s_largeFiniteCard(Integer("18446744073709551617")); // 2^64 + 1
const Cardinality Cardinality::INTEGERS(CardinalityBeth(0));
const Cardinality Cardinality::REALS(CardinalityBeth(1));
-const Cardinality Cardinality::UNKNOWN((CardinalityUnknown()));
+const Cardinality Cardinality::UNKNOWN_CARD((CardinalityUnknown()));
Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
if(isUnknown()) {
@@ -36,15 +37,24 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
return *this;
}
+ if(c.isFinite() && isLargeFinite()) {
+ return *this;
+ } else if(isFinite() && c.isLargeFinite()) {
+ d_card = s_largeFiniteCard;
+ return *this;
+ }
+
if(isFinite() && c.isFinite()) {
d_card += c.d_card - 1;
return *this;
}
- if(*this >= c) {
- return *this;
- } else {
+ if(compare(c) == LESS) {
return *this = c;
+ } else {
+ return *this;
}
+
+ Unreachable();
}
/** Assigning multiplication of this cardinality with another. */
@@ -56,13 +66,20 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
return *this;
}
- if(*this == 0 || c == 0) {
+ if(c.isFinite() && isLargeFinite()) {
+ return *this;
+ } else if(isFinite() && c.isLargeFinite()) {
+ d_card = s_largeFiniteCard;
+ return *this;
+ }
+
+ if(compare(0) == EQUAL || c.compare(0) == EQUAL) {
return *this = 0;
} else if(!isFinite() || !c.isFinite()) {
- if(*this >= c) {
- return *this;
- } else {
+ if(compare(c) == LESS) {
return *this = c;
+ } else {
+ return *this;
}
} else {
d_card -= 1;
@@ -70,11 +87,12 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
d_card += 1;
return *this;
}
+
+ Unreachable();
}
/** Assigning exponentiation of this cardinality with another. */
-Cardinality& Cardinality::operator^=(const Cardinality& c)
- throw(IllegalArgumentException) {
+Cardinality& Cardinality::operator^=(const Cardinality& c) throw() {
if(isUnknown()) {
return *this;
} else if(c.isUnknown()) {
@@ -82,41 +100,99 @@ Cardinality& Cardinality::operator^=(const Cardinality& c)
return *this;
}
- if(c == 0) {
+ if(c.isFinite() && isLargeFinite()) {
+ return *this;
+ } else if(isFinite() && c.isLargeFinite()) {
+ d_card = s_largeFiniteCard;
+ return *this;
+ }
+
+ if(c.compare(0) == EQUAL) {
// (anything) ^ 0 == 1
- d_card = 2;// remember +1 for finite cardinalities
+ d_card = 2; // remember, +1 for finite cardinalities
return *this;
- } else if(*this == 0) {
+ } else if(compare(0) == EQUAL) {
// 0 ^ (>= 1) == 0
return *this;
- } else if(*this == 1) {
+ } else if(compare(1) == EQUAL) {
// 1 ^ (>= 1) == 1
return *this;
- } else if(c == 1) {
+ } else if(c.compare(1) == EQUAL) {
// (anything) ^ 1 == (that thing)
return *this;
} else if(isFinite() && c.isFinite()) {
// finite ^ finite == finite
- //
- // Note: can throw an assertion if c is too big for
- // exponentiation
- d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
+ try {
+ // Note: can throw an assertion if c is too big for
+ // exponentiation
+ if(d_card - 1 >= 2 && c.d_card - 1 >= 64) {
+ // don't bother, it's too large anyways
+ d_card = s_largeFiniteCard;
+ } else {
+ d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
+ }
+ } catch(IllegalArgumentException&) {
+ d_card = s_largeFiniteCard;
+ }
return *this;
} else if(!isFinite() && c.isFinite()) {
// inf ^ finite == inf
return *this;
} else {
- Assert(*this >= 2 && !c.isFinite(),
+ Assert(compare(2) != LESS && !c.isFinite(),
"fall-through case not as expected:\n%s\n%s",
this->toString().c_str(), c.toString().c_str());
// (>= 2) ^ beth_k == beth_(k+1)
// unless the base is already > the exponent
- if(*this > c) {
+ if(compare(c) == GREATER) {
return *this;
}
d_card = c.d_card - 1;
return *this;
}
+
+ Unreachable();
+}
+
+Cardinality::CardinalityComparison Cardinality::compare(const Cardinality& c) const throw() {
+ if(isUnknown() || c.isUnknown()) {
+ return UNKNOWN;
+ } else if(isLargeFinite()) {
+ if(c.isLargeFinite()) {
+ return UNKNOWN;
+ } else if(c.isFinite()) {
+ return GREATER;
+ } else {
+ Assert(c.isInfinite());
+ return LESS;
+ }
+ } else if(c.isLargeFinite()) {
+ if(isLargeFinite()) {
+ return UNKNOWN;
+ } else if(isFinite()) {
+ return LESS;
+ } else {
+ Assert(isInfinite());
+ return GREATER;
+ }
+ } else if(isInfinite()) {
+ if(c.isFinite()) {
+ return GREATER;
+ } else {
+ return d_card < c.d_card ? GREATER :
+ (d_card == c.d_card ? EQUAL : LESS);
+ }
+ } else if(c.isInfinite()) {
+ Assert(isFinite());
+ return LESS;
+ } else {
+ Assert(isFinite() && !isLargeFinite());
+ Assert(c.isFinite() && !c.isLargeFinite());
+ return d_card < c.d_card ? LESS :
+ (d_card == c.d_card ? EQUAL : GREATER);
+ }
+
+ Unreachable();
}
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index 057bb0b0c..30bdea78d 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -74,11 +74,18 @@ class CVC4_PUBLIC Cardinality {
/** A representation for unknown cardinality */
static const Integer s_unknownCard;
+ /** A representation for large, finite cardinality */
+ static const Integer s_largeFiniteCard;
+
/**
* In the case of finite cardinality, this is > 0, and is equal to
* the cardinality+1. If infinite, it is < 0, and is Beth[|card|-1].
* That is, "-1" means Beth 0 == |Z|, "-2" means Beth 1 == |R|, etc.
* If this field is 0, the cardinality is unknown.
+ *
+ * We impose a ceiling on finite cardinalities of 2^64. If this field
+ * is >= 2^64 + 1, we consider it at "ceiling" cardinality, and
+ * comparisons between all such cardinalities result in "unknown."
*/
Integer d_card;
@@ -91,7 +98,15 @@ public:
static const Cardinality REALS;
/** The unknown cardinality */
- static const Cardinality UNKNOWN;
+ static const Cardinality UNKNOWN_CARD;
+
+ /** Used as a result code for Cardinality::compare(). */
+ enum CVC4_PUBLIC CardinalityComparison {
+ LESS,
+ EQUAL,
+ GREATER,
+ UNKNOWN
+ };/* enum CardinalityComparison */
/**
* Construct a finite cardinality equal to the integer argument.
@@ -131,7 +146,13 @@ public:
Cardinality(CardinalityUnknown) : d_card(0) {
}
- /** Returns true iff this cardinality is unknown. */
+ /**
+ * 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().
+ */
bool isUnknown() const throw() {
return d_card == 0;
}
@@ -141,6 +162,14 @@ public:
return d_card > 0;
}
+ /**
+ * Returns true iff this cardinality is finite and large (i.e.,
+ * at the ceiling of representable finite cardinalities).
+ . */
+ bool isLargeFinite() const throw() {
+ return d_card >= s_largeFiniteCard;
+ }
+
/** Returns true iff this cardinality is infinite. */
bool isInfinite() const throw() {
return d_card < 0;
@@ -161,6 +190,7 @@ public:
*/
Integer getFiniteCardinality() const throw(IllegalArgumentException) {
CheckArgument(isFinite(), *this, "This cardinality is not finite.");
+ CheckArgument(!isLargeFinite(), *this, "This cardinality is finite, but too large to represent.");
return d_card - 1;
}
@@ -182,7 +212,7 @@ public:
Cardinality& operator*=(const Cardinality& c) throw();
/** Assigning exponentiation of this cardinality with another. */
- Cardinality& operator^=(const Cardinality& c) throw(IllegalArgumentException);
+ Cardinality& operator^=(const Cardinality& c) throw();
/** Add two cardinalities. */
Cardinality operator+(const Cardinality& c) const throw() {
@@ -199,54 +229,21 @@ public:
}
/**
- * Exponentiation of two cardinalities. Throws an exception if both
- * are finite and the exponent is too large.
+ * Exponentiation of two cardinalities.
*/
- Cardinality operator^(const Cardinality& c) const throw(IllegalArgumentException) {
+ Cardinality operator^(const Cardinality& c) const throw() {
Cardinality card(*this);
card ^= c;
return card;
}
- /** Test for equality between cardinalities. */
- bool operator==(const Cardinality& c) const throw() {
- return !isUnknown() && d_card == c.d_card;
- }
-
- /** Test for disequality between cardinalities. */
- bool operator!=(const Cardinality& c) const throw() {
- return !isUnknown() && !c.isUnknown() && d_card != c.d_card;
- }
-
- /** Test whether this cardinality is less than another. */
- bool operator<(const Cardinality& c) const throw() {
- return
- !isUnknown() && !c.isUnknown() &&
- ( ( isFinite() && !c.isFinite() ) ||
- ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
- ( !isFinite() && !c.isFinite() && d_card > c.d_card ) );
- }
-
- /**
- * Test whether this cardinality is less than or equal to
- * another.
- */
- bool operator<=(const Cardinality& c) const throw() {
- return !isUnknown() && !c.isUnknown() && (*this < c || *this == c);
- }
-
- /** Test whether this cardinality is greater than another. */
- bool operator>(const Cardinality& c) const throw() {
- return !isUnknown() && !c.isUnknown() && !(*this <= c);
- }
-
/**
- * Test whether this cardinality is greater than or equal to
- * another.
+ * 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.
*/
- bool operator>=(const Cardinality& c) const throw() {
- return !isUnknown() && !c.isUnknown() && !(*this < c);
- }
+ Cardinality::CardinalityComparison compare(const Cardinality& c) const throw();
/**
* Return a string representation of this cardinality.
@@ -265,7 +262,6 @@ std::ostream& operator<<(std::ostream& out, CardinalityBeth b)
std::ostream& operator<<(std::ostream& out, const Cardinality& c)
throw() CVC4_PUBLIC;
-
}/* CVC4 namespace */
#endif /* __CVC4__CARDINALITY_H */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback