diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-21 19:43:46 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-02-21 19:43:46 +0000 |
commit | f52bee51e20b0670f9a2bd13ae2fdefd5eba1546 (patch) | |
tree | e77af4a3fd4bd726d1f9ed1215fccf5aad1c50f2 /src/theory/theory.h | |
parent | 9dcfc2fdc58bf46a434f9c228a828be8d580f529 (diff) |
Fix for bug303. The problem was with function applications that get normalized when added to the term database. For example, if x=y exists, and the term f(x) is added, f(y) was stored. So, when getExplanation(f(x), f(y)) was called, trouble ensued. I now keep the original version so that explanations can be properly produced.
Also added theory::assertions debug flag that will printout assertions of each theory for ease and uniformity of debugging in the future.
Diffstat (limited to 'src/theory/theory.h')
-rw-r--r-- | src/theory/theory.h | 60 |
1 files changed, 40 insertions, 20 deletions
diff --git a/src/theory/theory.h b/src/theory/theory.h index af891e3a3..cf986a1f2 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -206,26 +206,6 @@ protected: } /** - * Provides access to the facts queue, primarily intended for theory - * debugging purposes. - * - * @return the iterator to the beginning of the fact queue - */ - context::CDList<Assertion>::const_iterator facts_begin() const { - return d_facts.begin(); - } - - /** - * Provides access to the facts queue, primarily intended for theory - * debugging purposes. - * - * @return the iterator to the end of the fact queue - */ - context::CDList<Assertion>::const_iterator facts_end() const { - return d_facts.end(); - } - - /** * The theory that owns the uninterpreted sort. */ static TheoryId d_uninterpretedSortOwner; @@ -605,6 +585,46 @@ public: return ss.str(); } + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the fact queue + */ + context::CDList<Assertion>::const_iterator facts_begin() const { + return d_facts.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the fact queue + */ + context::CDList<Assertion>::const_iterator facts_end() const { + return d_facts.end(); + } + + /** + * Provides access to the shared terms, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the beginning of the shared terms list + */ + context::CDList<TNode>::const_iterator shared_terms_begin() const { + return d_sharedTerms.begin(); + } + + /** + * Provides access to the facts queue, primarily intended for theory + * debugging purposes. + * + * @return the iterator to the end of the shared terms list + */ + context::CDList<TNode>::const_iterator shared_terms_end() const { + return d_sharedTerms.end(); + } + };/* class Theory */ std::ostream& operator<<(std::ostream& os, Theory::Effort level); |