* ability to output NodeBuilders without first converting them to Nodes---useful for debugging.

* language-dependent Node::toString()
* some minor proof-related cleanup

1 files changed, 21 insertions, 21 deletions

diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index c03b09be2..e09e9f47f 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -90,7 +90,7 @@ void TheoryEngine::preRegister(TNode preprocessed) {
   // Pre-register the terms in the atom
   bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
   if (multipleTheories) {
-    // Collect the shared terms if there are multipe theories 
+    // Collect the shared terms if there are multipe theories
     NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
     // Mark the multiple theories flag
     d_sharedTermsExist = true;
@@ -173,7 +173,7 @@ void TheoryEngine::check(Theory::Effort effort) {
         break;
       }
     }
-    
+
     // Clear any leftover propagated equalities
     d_propagatedEqualities.clear();
 
@@ -214,10 +214,10 @@ void TheoryEngine::combineTheories() {
      CareGraph theoryGraph; \
      reinterpret_cast<theory::TheoryTraits<THEORY>::theory_class*>(theoryOf(THEORY))->computeCareGraph(theoryGraph); \
      careGraph.insert(careGraph.end(), theoryGraph.begin(), theoryGraph.end()); \
-  } 
+  }
 
   CVC4_FOR_EACH_THEORY;
-    
+
   // Now add splitters for the ones we are interested in
   for (unsigned i = 0; i < careGraph.size(); ++ i) {
     const CarePair& carePair = careGraph[i];
@@ -505,7 +505,7 @@ Node TheoryEngine::preprocess(TNode assertion) {
   return d_atomPreprocessingCache[assertion];
 }
 
-void TheoryEngine::assertFact(TNode node) 
+void TheoryEngine::assertFact(TNode node)
 {
   Trace("theory") << "TheoryEngine::assertFact(" << node << ")" << std::endl;
 
@@ -516,7 +516,7 @@ void TheoryEngine::assertFact(TNode node)
 
   // Assert the fact to the apropriate theory
   theoryOf(atom)->assertFact(node, true);
-    
+
   // If any shared terms, notify the theories
   if (d_sharedTerms.hasSharedTerms(atom)) {
     SharedTermsDatabase::shared_terms_iterator it = d_sharedTerms.begin(atom);
@@ -536,11 +536,11 @@ void TheoryEngine::assertFact(TNode node)
 }
 
 void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
-      
+
   Debug("theory") << "EngineOutputChannel::propagate(" << literal << ", " << theory << ")" << std::endl;
 
   d_propEngine->checkTime();
-      
+
   if(Dump.isOn("t-propagations")) {
     Dump("t-propagations") << CommentCommand("negation of theory propagation: expect valid") << std::endl
                            << QueryCommand(literal.toExpr()) << std::endl;
@@ -550,7 +550,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
   }
 
   TNode atom = literal.getKind() == kind::NOT ? literal[0] : literal;
-  
+
   if (!d_sharedTermsExist || atom.getKind() != kind::EQUAL) {
     // If not an equality it must be a SAT literal so we enlist it, and it can only
     // be propagated by the theory that owns it, as it is the only one that got
@@ -563,7 +563,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
     if (d_propEngine->isSatLiteral(normalizedEquality)) {
       // If there is a literal, just enqueue it, same as above
       d_propagatedLiterals.push_back(normalizedEquality);
-    } 
+    }
     // Otherwise, we assert it to all interested theories
     Theory::Set lhsNotified = d_sharedTerms.getNotifiedTheories(atom[0]);
     Theory::Set rhsNotified = d_sharedTerms.getNotifiedTheories(atom[1]);
@@ -586,7 +586,7 @@ void TheoryEngine::propagate(TNode literal, theory::TheoryId theory) {
         }
       }
     }
-  } 
+  }
 }
 
 theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
@@ -594,33 +594,33 @@ theory::EqualityStatus TheoryEngine::getEqualityStatus(TNode a, TNode b) {
   return theoryOf(Theory::theoryOf(a.getType()))->getEqualityStatus(a, b);
 }
 
-Node TheoryEngine::getExplanation(TNode node) 
+Node TheoryEngine::getExplanation(TNode node)
 {
-  Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl; 
+  Debug("theory") << "TheoryEngine::getExplanation(" << node << ")" << std::endl;
 
   TNode atom = node.getKind() == kind::NOT ? node[0] : node;
-  
+
   Node explanation;
 
   // The theory that has explaining to do
   Theory* theory = theoryOf(atom);
   if (d_sharedTermsExist && atom.getKind() == kind::EQUAL) {
     SharedAssertionsMap::iterator find = d_sharedAssertions.find(NodeTheoryPair(node, theory::THEORY_LAST));
-    if (find == d_sharedAssertions.end()) {             
+    if (find == d_sharedAssertions.end()) {
       theory = theoryOf(atom);
-    } 
-  } 
+    }
+  }
 
   // Get the explanation
   explanation = theory->explain(node);
-  
+
   // Explain any shared equalities that might be in the explanation
   if (d_sharedTermsExist) {
     NodeBuilder<> nb(kind::AND);
     explainEqualities(theory->getId(), explanation, nb);
     explanation = nb;
   }
-  
+
   Assert(!explanation.isNull());
   if(Dump.isOn("t-explanations")) {
     Dump("t-explanations") << CommentCommand(std::string("theory explanation from ") + theoryOf(atom)->identify() + ": expect valid") << std::endl
@@ -657,7 +657,7 @@ void TheoryEngine::conflict(TNode conflict, TheoryId theoryId) {
 }
 
 void TheoryEngine::explainEqualities(TheoryId theoryId, TNode literals, NodeBuilder<>& builder) {
-  Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl; 
+  Debug("theory") << "TheoryEngine::explainEqualities(" << theoryId << ", " << literals << ")" << std::endl;
   if (literals.getKind() == kind::AND) {
     for (unsigned i = 0, i_end = literals.getNumChildren(); i != i_end; ++ i) {
       TNode literal = literals[i];
@@ -695,6 +695,6 @@ void TheoryEngine::explainEquality(TheoryId theoryId, TNode eqLiteral, NodeBuild
       Node explanation = theoryOf(explainingTheory)->explain((*find).second.node);
       explainEqualities(explainingTheory, explanation, builder);
     }
-  }  
+  }
 }