Do not eagerly construct explanations in relation solver.

diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp
index e71333075b8c9852e8c609891ecbd6e35c9ab7f7..e53fec02f3a76f8f645a2eaef3cc6fc100977c63 100644 (file)
--- a/src/theory/sets/theory_sets_private.cpp
+++ b/src/theory/sets/theory_sets_private.cpp
@@ -1966,9 +1966,6 @@ Node TheorySetsPrivate::explain(TNode literal)
   if(atom.getKind() == kind::EQUAL) {
     d_equalityEngine.explainEquality(atom[0], atom[1], polarity, assumptions);
   } else if(atom.getKind() == kind::MEMBER) {
-    if( !d_equalityEngine.hasTerm(atom)) {
-      d_equalityEngine.addTerm(atom);
-    }
     d_equalityEngine.explainPredicate(atom, polarity, assumptions);
   } else {
     Debug("sets") << "unhandled: " << literal << "; (" << atom << ", "

diff --git a/src/theory/sets/theory_sets_rels.cpp b/src/theory/sets/theory_sets_rels.cpp
index 09865647e240e72ef9ee68ca645e55d10a029845..b5b7c90b455ea57b7754e188127a85095baff9ed 100644 (file)
--- a/src/theory/sets/theory_sets_rels.cpp
+++ b/src/theory/sets/theory_sets_rels.cpp
@@ -1090,27 +1090,9 @@ int TheorySetsRels::EqcInfo::counter        = 0;
     }
   }
 
-  Node TheorySetsRels::explain( Node literal )
-  {
-    Trace("rels-exp") << "[sets-rels] TheorySetsRels::explain(" << literal << ")"<< std::endl;
-    std::vector<TNode>  assumptions;
-    bool                polarity        = literal.getKind() != kind::NOT;
-    TNode               atom            = polarity ? literal : literal[0];
-
-    if(atom.getKind() == kind::EQUAL) {
-      d_eqEngine->explainEquality(atom[0], atom[1], polarity, assumptions);
-    } else if(atom.getKind() == kind::MEMBER) {
-      if( !d_eqEngine->hasTerm(atom)) {
-        d_eqEngine->addTerm(atom);
-      }
-      d_eqEngine->explainPredicate(atom, polarity, assumptions);
-    } else {
-      Trace("rels-exp") << "unhandled: " << literal << "; (" << atom << ", "
-                    << polarity << "); kind" << atom.getKind() << std::endl;
-      Unhandled();
-    }
-    Trace("rels-exp") << "[sets-rels] ****** done with TheorySetsRels::explain(" << literal << ")"<< std::endl;
-    return mkAnd(assumptions);
+  Node TheorySetsRels::explain( Node literal ){
+    //use lazy explanations
+    return literal;
   }
 
   TheorySetsRels::EqcInfo::EqcInfo( context::Context* c ) :