diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/main/Makefile.am | 6 | ||||
-rw-r--r-- | src/theory/theory.h | 20 | ||||
-rw-r--r-- | src/util/cardinality.cpp | 44 | ||||
-rw-r--r-- | src/util/cardinality.h | 63 | ||||
-rw-r--r-- | src/util/tls.h.in | 50 |
5 files changed, 154 insertions, 29 deletions
diff --git a/src/main/Makefile.am b/src/main/Makefile.am index 669ab6fa2..42a306752 100644 --- a/src/main/Makefile.am +++ b/src/main/Makefile.am @@ -31,11 +31,11 @@ TOKENS_FILES = \ smt2_tokens.h cvc_tokens.h: @srcdir@/../parser/cvc/Cvc.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ smt_tokens.h: @srcdir@/../parser/smt/Smt.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ smt2_tokens.h: @srcdir@/../parser/smt2/Smt2.g - $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]\+\)'\''.*/"\1",/' | sort -u >$@ + $(AM_V_GEN)grep "'[a-zA-Z][a-zA-Z0-9][a-zA-Z0-9]*'" $^ | sed 's/.*'\''\([a-zA-Z0-9]*\)'\''.*/"\1",/' | sort -u >$@ clean-local: rm -f $(BUILT_SOURCES) diff --git a/src/theory/theory.h b/src/theory/theory.h index bba4c623a..e97e603e5 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -86,6 +86,12 @@ private: /** Index into the head of the facts list */ context::CDO<unsigned> d_factsHead; + /** + * Whether the last retrieved fact via get() was a shared term fact + * or not. + */ + bool d_wasSharedTermFact; + protected: /** @@ -96,6 +102,7 @@ protected: d_context(ctxt), d_facts(ctxt), d_factsHead(ctxt, 0), + d_wasSharedTermFact(false), d_out(&out), d_valuation(valuation) { } @@ -131,6 +138,7 @@ protected: TNode get() { Assert( !done(), "Theory::get() called with assertion queue empty!" ); TNode fact = d_facts[d_factsHead]; + d_wasSharedTermFact = false; d_factsHead = d_factsHead + 1; Debug("theory") << "Theory::get() => " << fact << "(" << d_facts.size() << " left)" << std::endl; @@ -139,6 +147,18 @@ protected: } /** + * Returns whether the last fact retrieved by get() was a shared + * term fact. + * + * @return true if the fact just retrieved via get() was a shared + * term fact, false if the fact just retrieved was a "normal channel" + * fact. + */ + bool isSharedTermFact() const throw() { + return d_wasSharedTermFact; + } + + /** * Provides access to the facts queue, primarily intended for theory * debugging purposes. * 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@ */ |