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.

4 files changed, 91 insertions, 29 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);
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index e21e83671..75c64654d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -133,6 +133,33 @@ void TheoryEngine::check(Theory::Effort effort) {
 
       Debug("theory") << "TheoryEngine::check(" << effort << "): running check" << std::endl;
 
+      if (Debug.isOn("theory::assertions")) {
+        for (unsigned theoryId = 0; theoryId < THEORY_LAST; ++ theoryId) {
+          Theory* theory = d_theoryTable[theoryId];
+          if (theory && Theory::setContains((TheoryId)theoryId, d_activeTheories)) {
+            Debug("theory::assertions") << "--------------------------------------------" << std::endl;
+            Debug("theory::assertions") << "Assertions of " << theory->getId() << ": " << std::endl;
+            context::CDList<Assertion>::const_iterator it = theory->facts_begin(), it_end = theory->facts_end();
+            for (unsigned i = 0; it != it_end; ++ it, ++i) {
+                if ((*it).isPreregistered) {
+                  Debug("theory::assertions") << "[" << i << "]: ";
+                } else {
+                  Debug("theory::assertions") << "(" << i << "): ";
+                }
+                Debug("theory::assertions") << (*it).assertion << endl;
+            }
+
+            if (d_sharedTermsExist) {
+              Debug("theory::assertions") << "Shared terms of " << theory->getId() << ": " << std::endl;
+              context::CDList<TNode>::const_iterator it = theory->shared_terms_begin(), it_end = theory->shared_terms_end();
+              for (unsigned i = 0; it != it_end; ++ it, ++i) {
+                  Debug("theory::assertions") << "[" << i << "]: " << (*it) << endl;
+              }
+            }
+          }
+        }
+      }
+
       // Do the checking
       CVC4_FOR_EACH_THEORY;
 
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index 29f932e04..41b39af97 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -311,8 +311,22 @@ private:
   /** A context-dependents count of nodes */
   context::CDO<size_t> d_nodesCount;
 
+  /**
+   * At time of addition a function application can already normalize to something, so
+   * we keep both the original, and the normalized version.
+   */
+  struct FunctionApplicationPair {
+    FunctionApplication original;
+    FunctionApplication normalized;
+    FunctionApplicationPair() {}
+    FunctionApplicationPair(const FunctionApplication& original, const FunctionApplication& normalized)
+    : original(original), normalized(normalized) {}
+    bool isNull() const {
+      return !original.isApplication();
+    }
+  };
   /** Map from ids to the applications */
-  std::vector<FunctionApplication> d_applications;
+  std::vector<FunctionApplicationPair> d_applications;
 
   /** Map from ids to the equality nodes */
   std::vector<EqualityNode> d_equalityNodes;
diff --git a/src/theory/uf/equality_engine_impl.h b/src/theory/uf/equality_engine_impl.h
index f30006cb9..02426c849 100644
--- a/src/theory/uf/equality_engine_impl.h
+++ b/src/theory/uf/equality_engine_impl.h
@@ -41,13 +41,14 @@ EqualityNodeId EqualityEngine<NotifyClass>::newApplicationNode(TNode original, E
 
   // Get another id for this
   EqualityNodeId funId = newNode(original, true);
-    // The function application we're creating
+  FunctionApplication funOriginal(t1, t2);
+  // The function application we're creating
   EqualityNodeId t1ClassId = getEqualityNode(t1).getFind();
   EqualityNodeId t2ClassId = getEqualityNode(t2).getFind();
   FunctionApplication funNormalized(t1ClassId, t2ClassId);
 
-  // We add the normalized version, the term needs to be re-added on each backtrack
-  d_applications[funId] = funNormalized;
+  // We add the original version
+  d_applications[funId] = FunctionApplicationPair(funOriginal, funNormalized);
 
   // Add the lookup data, if it's not already there
   typename ApplicationIdsMap::iterator find = d_applicationLookup.find(funNormalized);
@@ -86,7 +87,7 @@ EqualityNodeId EqualityEngine<NotifyClass>::newNode(TNode node, bool isApplicati
   // Add the node to it's position
   d_nodes.push_back(node);
   // Note if this is an application or not
-  d_applications.push_back(FunctionApplication());
+  d_applications.push_back(FunctionApplicationPair());
   // Add the trigger list for this node
   d_nodeTriggers.push_back(+null_trigger);
   // Add it to the equality graph
@@ -294,7 +295,7 @@ void EqualityEngine<NotifyClass>::merge(EqualityNode& class1, EqualityNode& clas
       // Get the function application
       EqualityNodeId funId = useNode.getApplicationId();
       Debug("equality") << "EqualityEngine::merge(" << class1.getFind() << "," << class2.getFind() << "): " << currentId << " in " << d_nodes[funId] << std::endl;
-      const FunctionApplication& fun = d_applications[useNode.getApplicationId()];
+      const FunctionApplication& fun = d_applications[useNode.getApplicationId()].normalized;
       // Check if there is an application with find arguments
       EqualityNodeId aNormalized = getEqualityNode(fun.a).getFind();
       EqualityNodeId bNormalized = getEqualityNode(fun.b).getFind();
@@ -441,7 +442,7 @@ void EqualityEngine<NotifyClass>::backtrack() {
       Debug("equality") << "EqualityEngine::backtrack(): removing node " << d_nodes[i] << std::endl;
       d_nodeIds.erase(d_nodes[i]);
 
-      const FunctionApplication& app = d_applications[i];
+      const FunctionApplication& app = d_applications[i].normalized;
       if (app.isApplication()) {
         // Remove b from use-list
         getEqualityNode(app.b).removeTopFromUseList(d_useListNodes);
@@ -593,8 +594,8 @@ void EqualityEngine<NotifyClass>::getExplanation(EqualityNodeId t1Id, EqualityNo
             if (reasonType == MERGED_THROUGH_CONGRUENCE) {
               // f(x1, x2) == f(y1, y2) because x1 = y1 and x2 = y2
               Debug("equality") << "EqualityEngine::getExplanation(): due to congruence, going deeper" << std::endl;
-              const FunctionApplication& f1 = d_applications[currentNode];
-              const FunctionApplication& f2 = d_applications[edgeNode];
+              const FunctionApplication& f1 = d_applications[currentNode].original;
+              const FunctionApplication& f2 = d_applications[edgeNode].original;
               Debug("equality") << push;
               getExplanation(f1.a, f2.a, equalities);
               getExplanation(f1.b, f2.b, equalities);