summaryrefslogtreecommitdiff
path: root/src/util
diff options
context:
space:
mode:
Diffstat (limited to 'src/util')
-rw-r--r--src/util/cardinality.cpp44
-rw-r--r--src/util/cardinality.h63
-rw-r--r--src/util/tls.h.in50
3 files changed, 131 insertions, 26 deletions
diff --git a/src/util/cardinality.cpp b/src/util/cardinality.cpp
index d38be1c92..b8a79cd9e 100644
--- a/src/util/cardinality.cpp
+++ b/src/util/cardinality.cpp
@@ -20,15 +20,24 @@
namespace CVC4 {
+const Integer Cardinality::s_unknownCard(0);
const Integer Cardinality::s_intCard(-1);
const Integer Cardinality::s_realCard(-2);
const Cardinality Cardinality::INTEGERS(Cardinality::Beth(0));
const Cardinality Cardinality::REALS(Cardinality::Beth(1));
+const Cardinality Cardinality::UNKNOWN((Cardinality::Unknown()));
Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(isFinite() && c.isFinite()) {
- d_card += c.d_card;
+ d_card += c.d_card - 1;
return *this;
}
if(*this >= c) {
@@ -40,6 +49,13 @@ Cardinality& Cardinality::operator+=(const Cardinality& c) throw() {
/** Assigning multiplication of this cardinality with another. */
Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(*this == 0 || c == 0) {
return *this = 0;
} else if(!isFinite() || !c.isFinite()) {
@@ -49,7 +65,9 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
return *this = c;
}
} else {
- d_card *= c.d_card;
+ d_card -= 1;
+ d_card *= c.d_card - 1;
+ d_card += 1;
return *this;
}
}
@@ -57,9 +75,16 @@ Cardinality& Cardinality::operator*=(const Cardinality& c) throw() {
/** Assigning exponentiation of this cardinality with another. */
Cardinality& Cardinality::operator^=(const Cardinality& c)
throw(IllegalArgumentException) {
+ if(isUnknown()) {
+ return *this;
+ } else if(c.isUnknown()) {
+ d_card = s_unknownCard;
+ return *this;
+ }
+
if(c == 0) {
// (anything) ^ 0 == 1
- d_card = 1;
+ d_card = 2;// remember +1 for finite cardinalities
return *this;
} else if(*this == 0) {
// 0 ^ (>= 1) == 0
@@ -75,7 +100,7 @@ Cardinality& Cardinality::operator^=(const Cardinality& c)
//
// Note: can throw an assertion if c is too big for
// exponentiation
- d_card = d_card.pow(c.d_card.getUnsignedLong());
+ d_card = (d_card - 1).pow(c.d_card.getUnsignedLong() - 1) + 1;
return *this;
} else if(!isFinite() && c.isFinite()) {
// inf ^ finite == inf
@@ -102,18 +127,17 @@ std::string Cardinality::toString() const throw() {
}
-std::ostream& operator<<(std::ostream& out,
- Cardinality::Beth b)
- throw() {
+std::ostream& operator<<(std::ostream& out, Cardinality::Beth b) throw() {
out << "beth[" << b.getNumber() << ']';
return out;
}
-std::ostream& operator<<(std::ostream& out, const Cardinality& c)
- throw() {
- if(c.isFinite()) {
+std::ostream& operator<<(std::ostream& out, const Cardinality& c) throw() {
+ if(c.isUnknown()) {
+ out << "Cardinality::UNKNOWN";
+ } else if(c.isFinite()) {
out << c.getFiniteCardinality();
} else {
out << Cardinality::Beth(c.getBethNumber());
diff --git a/src/util/cardinality.h b/src/util/cardinality.h
index c520c2735..e7f86c80e 100644
--- a/src/util/cardinality.h
+++ b/src/util/cardinality.h
@@ -42,10 +42,14 @@ class CVC4_PUBLIC Cardinality {
/** Cardinality of the reals */
static const Integer s_realCard;
+ /** A representation for unknown cardinality */
+ static const Integer s_unknownCard;
+
/**
- * In the case of finite cardinality, this is >= 0, and is equal to
- * the cardinality. If infinite, it is < 0, and is Beth[|card|-1].
+ * 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.
*/
Integer d_card;
@@ -57,11 +61,14 @@ public:
/** The cardinality of the set of real numbers. */
static const Cardinality REALS;
+ /** The unknown cardinality */
+ static const Cardinality UNKNOWN;
+
/**
* Representation for a Beth number, used only to construct
* Cardinality objects.
*/
- class Beth {
+ class CVC4_PUBLIC Beth {
Integer d_index;
public:
@@ -77,6 +84,15 @@ public:
};/* class Cardinality::Beth */
/**
+ * Representation for an unknown cardinality.
+ */
+ class CVC4_PUBLIC Unknown {
+ public:
+ Unknown() throw() {}
+ ~Unknown() throw() {}
+ };/* class Cardinality::Unknown */
+
+ /**
* 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
@@ -85,6 +101,7 @@ public:
Cardinality(long card) : d_card(card) {
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %ld.", card);
+ d_card += 1;
Assert(isFinite());
}
@@ -96,6 +113,7 @@ public:
CheckArgument(card >= 0, card,
"Cardinality must be a nonnegative integer, not %s.",
card.toString().c_str());
+ d_card += 1;
Assert(isFinite());
}
@@ -106,9 +124,20 @@ public:
Assert(!isFinite());
}
+ /**
+ * Construct an unknown cardinality.
+ */
+ Cardinality(Unknown) : d_card(0) {
+ }
+
+ /** Returns true iff this cardinality is unknown. */
+ bool isUnknown() const throw() {
+ return d_card == 0;
+ }
+
/** Returns true iff this cardinality is finite. */
bool isFinite() const throw() {
- return d_card >= 0;
+ return d_card > 0;
}
/**
@@ -116,7 +145,7 @@ public:
* infinite.
*/
bool isCountable() const throw() {
- return d_card >= s_intCard;
+ return isFinite() || d_card == s_intCard;
}
/**
@@ -124,9 +153,9 @@ public:
* cardinality. (If this cardinality is infinite, this function
* throws an IllegalArgumentException.)
*/
- const Integer& getFiniteCardinality() const throw(IllegalArgumentException) {
+ Integer getFiniteCardinality() const throw(IllegalArgumentException) {
CheckArgument(isFinite(), *this, "This cardinality is not finite.");
- return d_card;
+ return d_card - 1;
}
/**
@@ -135,7 +164,8 @@ public:
* IllegalArgumentException.)
*/
Integer getBethNumber() const throw(IllegalArgumentException) {
- CheckArgument(!isFinite(), *this, "This cardinality is not infinite.");
+ CheckArgument(!isFinite() && !isUnknown(), *this,
+ "This cardinality is not infinite (or is unknown).");
return -d_card - 1;
}
@@ -174,20 +204,21 @@ public:
/** Test for equality between cardinalities. */
bool operator==(const Cardinality& c) const throw() {
- return d_card == c.d_card;
+ return !isUnknown() && d_card == c.d_card;
}
/** Test for disequality between cardinalities. */
bool operator!=(const Cardinality& c) const throw() {
- return !(*this == c);
+ 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
- ( isFinite() && !c.isFinite() ) ||
- ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
- ( !isFinite() && !c.isFinite() && d_card > c.d_card );
+ !isUnknown() && !c.isUnknown() &&
+ ( ( isFinite() && !c.isFinite() ) ||
+ ( isFinite() && c.isFinite() && d_card < c.d_card ) ||
+ ( !isFinite() && !c.isFinite() && d_card > c.d_card ) );
}
/**
@@ -195,12 +226,12 @@ public:
* another.
*/
bool operator<=(const Cardinality& c) const throw() {
- return *this < c || *this == c;
+ return !isUnknown() && !c.isUnknown() && (*this < c || *this == c);
}
/** Test whether this cardinality is greater than another. */
bool operator>(const Cardinality& c) const throw() {
- return !(*this <= c);
+ return !isUnknown() && !c.isUnknown() && !(*this <= c);
}
/**
@@ -208,7 +239,7 @@ public:
* another.
*/
bool operator>=(const Cardinality& c) const throw() {
- return !(*this < c);
+ return !isUnknown() && !c.isUnknown() && !(*this < c);
}
/**
diff --git a/src/util/tls.h.in b/src/util/tls.h.in
index fc0b6932b..bb69e7c82 100644
--- a/src/util/tls.h.in
+++ b/src/util/tls.h.in
@@ -143,6 +143,56 @@ public:
}
};/* class ThreadLocal<T> */
+template <class T>
+class ThreadLocal<T*> : public ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> {
+ typedef ThreadLocalImpl<T*, sizeof(T*) <= sizeof(void*)> super;
+
+public:
+ ThreadLocal() : super() {}
+ ThreadLocal(T* t) : super(t) {}
+ ThreadLocal(const ThreadLocal<T*>& tl) : super(tl) {}
+
+ ThreadLocal<T*>& operator=(T* t) {
+ return static_cast< ThreadLocal<T*>& >(super::operator=(t));
+ }
+ ThreadLocal<T*>& operator=(const ThreadLocal<T*>& tl) {
+ return static_cast< ThreadLocal<T*>& >(super::operator=(tl));
+ }
+ // special operators for pointers
+ T& operator*() {
+ return *static_cast<T*>(*this);
+ }
+ const T& operator*() const {
+ return *static_cast<const T*>(*this);
+ }
+ T* operator->() {
+ return static_cast<T*>(*this);
+ }
+ const T* operator->() const {
+ return static_cast<const T*>(*this);
+ }
+ T* operator++() {
+ T* p = *this;
+ *this = ++p;
+ return p;
+ }
+ T* operator++(int) {
+ T* p = *this;
+ *this = p + 1;
+ return p;
+ }
+ T* operator--() {
+ T* p = *this;
+ *this = --p;
+ return p;
+ }
+ T* operator--(int) {
+ T* p = *this;
+ *this = p - 1;
+ return p;
+ }
+};/* class ThreadLocal<T*> */
+
}/* CVC4 namespace */
#endif /* @CVC4_TLS_SUPPORTED@ */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback