diff options
| -rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 3 | ||||
| -rw-r--r-- | src/theory/sets/theory_sets_rels.cpp | 24 |
2 files changed, 3 insertions, 24 deletions
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 ) : |