* fix for Mac OS (includes some ThreadLocal stuff copied in from portfolio

  branch)
* add Theory::isSharedTermFact() -- it currently always returns false,
  pending theory combination work
* Add "unknown" cardinalities to Cardinality class
* Fix run_regression script to handle CRLF line terminators on Macs
  (where sed is non-GNU)
* Convert CRLF line terminators in datatypes regressions to LF

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@ */