Merging proof branch

3 files changed, 26 insertions, 11 deletions

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 9b429765e..25b12f75f 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -964,12 +964,9 @@ void EqualityEngine::explainEquality(TNode t1, TNode t2, bool polarity, std::vec
           std::vector<EqProof *> orderedChildren;
           bool nullCongruenceFound = false;
           for (unsigned i = 0; i < eqpc->d_children.size(); ++i) {
-            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE && eqpc->d_children[i]->d_node.isNull()) {
-
-              // For now, assume there can only be one null congruence child
-              Assert(!nullCongruenceFound);
+            if (eqpc->d_children[i]->d_id==eq::MERGED_THROUGH_CONGRUENCE &&
+                eqpc->d_children[i]->d_node.isNull()) {
               nullCongruenceFound = true;
-
               Debug("pf::ee") << "Have congruence with empty d_node. Splitting..." << std::endl;
               orderedChildren.insert(orderedChildren.begin(), eqpc->d_children[i]->d_children[0]);
               orderedChildren.push_back(eqpc->d_children[i]->d_children[1]);
@@ -1192,6 +1189,9 @@ void EqualityEngine::getExplanation(EqualityNodeId t1Id, EqualityNodeId t2Id, st
                 getExplanation(childId, getEqualityNode(childId).getFind(), equalities, eqpcc);
                 if( eqpc ) {
                   eqpc->d_children.push_back( eqpcc );
+
+                  Debug("pf::ee") << "MERGED_THROUGH_CONSTANTS. Dumping the child proof" << std::endl;
+                  eqpc->debug_print("pf::ee", 1);
                 }
               }
 
@@ -1605,6 +1605,7 @@ void EqualityEngine::propagate() {
 }
 
 void EqualityEngine::debugPrintGraph() const {
+  Debug("equality::graph") << std::endl << "Dumping graph" << std::endl;
   for (EqualityNodeId nodeId = 0; nodeId < d_nodes.size(); ++ nodeId) {
 
     Debug("equality::graph") << d_nodes[nodeId] << " " << nodeId << "(" << getEqualityNode(nodeId).getFind() << "):";
@@ -1618,6 +1619,7 @@ void EqualityEngine::debugPrintGraph() const {
 
     Debug("equality::graph") << std::endl;
   }
+  Debug("equality::graph") << std::endl;
 }
 
 bool EqualityEngine::areEqual(TNode t1, TNode t2) const {
@@ -2209,9 +2211,15 @@ bool EqClassIterator::isFinished() const {
   return d_current == null_id;
 }
 
-void EqProof::debug_print( const char * c, unsigned tb ) const{
-  for( unsigned i=0; i<tb; i++ ) { Debug( c ) << "  "; }
-  Debug( c ) << d_id << "(";
+void EqProof::debug_print(const char* c, unsigned tb, PrettyPrinter* prettyPrinter) const {
+  for(unsigned i=0; i<tb; i++) { Debug( c ) << "  "; }
+
+  if (prettyPrinter)
+    Debug( c ) << prettyPrinter->printTag(d_id);
+  else
+    Debug( c ) << d_id;
+
+  Debug( c ) << "(";
   if( !d_children.empty() || !d_node.isNull() ){
     if( !d_node.isNull() ){
       Debug( c ) << std::endl;
@@ -2221,7 +2229,7 @@ void EqProof::debug_print( const char * c, unsigned tb ) const{
     for( unsigned i=0; i<d_children.size(); i++ ){
       if( i>0 || !d_node.isNull() ) Debug( c ) << ",";
       Debug( c ) << std::endl;
-      d_children[i]->debug_print( c, tb+1 );
+      d_children[i]->debug_print( c, tb+1, prettyPrinter );
     }
   }
   Debug( c ) << ")" << std::endl;
diff --git a/src/theory/uf/equality_engine.h b/src/theory/uf/equality_engine.h
index f30f1e8a0..843e7ce7f 100644
--- a/src/theory/uf/equality_engine.h
+++ b/src/theory/uf/equality_engine.h
@@ -902,11 +902,17 @@ public:
 class EqProof
 {
 public:
+  class PrettyPrinter {
+  public:
+    virtual ~PrettyPrinter() {}
+    virtual std::string printTag(unsigned tag) = 0;
+  };
+
   EqProof() : d_id(MERGED_THROUGH_REFLEXIVITY){}
   unsigned d_id;
   Node d_node;
   std::vector< EqProof * > d_children;
-  void debug_print( const char * c, unsigned tb = 0 ) const;
+  void debug_print(const char * c, unsigned tb = 0, PrettyPrinter* prettyPrinter = NULL) const;
 };/* class EqProof */
 
 } // Namespace eq
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index d1685bdd1..9c461f57b 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -502,7 +502,7 @@ void TheoryUF::addCarePairs( quantifiers::TermArgTrie * t1, quantifiers::TermArg
 void TheoryUF::computeCareGraph() {
 
   if (d_sharedTerms.size() > 0) {
-    //use term indexing 
+    //use term indexing
     Debug("uf::sharing") << "TheoryUf::computeCareGraph(): Build term indices..." << std::endl;
     std::map< Node, quantifiers::TermArgTrie > index;
     std::map< Node, unsigned > arity;
@@ -533,6 +533,7 @@ void TheoryUF::computeCareGraph() {
 
 void TheoryUF::conflict(TNode a, TNode b) {
   eq::EqProof* pf = d_proofsEnabled ? new eq::EqProof() : NULL;
+
   if (a.getKind() == kind::CONST_BOOLEAN) {
     d_conflictNode = explain(a.iffNode(b),pf);
   } else {