diff options
author | Morgan Deters <mdeters@gmail.com> | 2011-05-13 20:42:57 +0000 |
---|---|---|
committer | Morgan Deters <mdeters@gmail.com> | 2011-05-13 20:42:57 +0000 |
commit | 69c9ec0e1e42f3f2f2f79d3e98398c5cd1559c66 (patch) | |
tree | 4761dc1485594a7d26630b3eea7f305dde0e2766 /src/theory/theory.h | |
parent | 9462ccde8b06aae3b13e271465ab74b2e312a095 (diff) |
* 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
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 20 |
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. * |