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.

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);