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