* 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

1 files changed, 20 insertions, 0 deletions

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.
    *