From: ajreynol <andrew.j.reynolds@gmail.com>
Date: Mon, 6 Mar 2017 16:18:17 +0000 (-0600)
Subject: Do not eagerly construct explanations in relation solver.
X-Git-Tag: cvc5-1.0.0~5899
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9b7af3ef07120280d0ef4acd94f9de9e90a2b7b0;p=cvc5.git

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 e71333075..e53fec02f 100644
--- 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 09865647e..b5b7c90b4 100644
--- 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 ) :