From b6d9f0bd9058db1358897834ac987f5d34de8734 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 8 Apr 2014 10:29:02 -0400 Subject: some debugging changes --- src/theory/sets/scrutinize.h | 44 ++++++++++++++++++++++ src/theory/sets/theory_sets_private.cpp | 65 +++++++++++++++++++++++++-------- src/theory/sets/theory_sets_private.h | 5 +++ 3 files changed, 98 insertions(+), 16 deletions(-) create mode 100644 src/theory/sets/scrutinize.h (limited to 'src/theory') diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h new file mode 100644 index 000000000..a0e2a1d5b --- /dev/null +++ b/src/theory/sets/scrutinize.h @@ -0,0 +1,44 @@ +/********************* */ +/*! \file scrutinize.h + ** \verbatim + ** Original author: Kshitij Bansal + ** Major contributors: none + ** Minor contributors (to current version): none + ** This file is part of the CVC4 project. + ** Copyright (c) 2013-2014 New York University and The University of Iowa + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + ** + ** \brief Check consistency of internal data structures. + ** + ** Some checks are very low-level with respect to TheorySetsPrivate + ** implementation, and hence might become outdated pretty quickly. + **/ + +#pragma once + +#include "theory/sets/theory_sets_private.h" + +namespace CVC4 { +namespace theory { +namespace sets { + +class TheorySetsScrutinize { + TheorySetsPrivate* d_theory; +public: + TheorySetsScrutinize(TheorySetsPrivate* theory): d_theory(theory) { + Debug("sets") << "[sets] scrunitize enabled" << std::endl; + } + void postCheckInvariants() const { + Debug("sets-scrutinize") << "[sets-scrutinize] postCheckInvariants()" << std::endl; + + // assume not in conflict, and complete: + // - try building model + // - check it + } +}; + +}/* CVC4::theory::sets namespace */ +}/* CVC4::theory namespace */ +}/* CVC4 namespace */ + diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index f487e1566..b29e2d4c6 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -17,6 +17,7 @@ #include #include "theory/theory_model.h" +#include "theory/sets/scrutinize.h" #include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" @@ -88,7 +89,10 @@ void TheorySetsPrivate::check(Theory::Effort level) { Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; Assert( d_conflict ^ d_equalityEngine.consistent() ); - if(d_conflict) return; + if(d_conflict) { + if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } + return; + } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } @@ -96,6 +100,8 @@ void TheorySetsPrivate::check(Theory::Effort level) { d_external.d_out->lemma(getLemma()); } + if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } + return; }/* TheorySetsPrivate::check() */ @@ -526,14 +532,28 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) TNode x = d_equalityEngine.getRepresentative(n[0]); TNode S = d_equalityEngine.getRepresentative(n[1]); settermElementsMap[S].insert(x); - if(Debug.isOn("sets-model-details")) { - vector explanation; - d_equalityEngine.explainPredicate(n, true, explanation); - Debug("sets-model-details") - << "[sets-model-details] > node: " << n << ", explanation:" << std::endl; - BOOST_FOREACH(TNode m, explanation) { - Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; - } + } + if(Debug.isOn("sets-model-details")) { + vector explanation; + d_equalityEngine.explainPredicate(n, true, explanation); + Debug("sets-model-details") + << "[sets-model-details] > node: " << n << ", explanation:" << std::endl; + BOOST_FOREACH(TNode m, explanation) { + Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; + } + } + } + + if(Debug.isOn("sets-model-details")) { + for(eq::EqClassIterator it_eqclasses(false_atom, &d_equalityEngine); + ! it_eqclasses.isFinished() ; ++it_eqclasses) { + TNode n = (*it_eqclasses); + vector explanation; + d_equalityEngine.explainPredicate(n, false, explanation); + Debug("sets-model-details") + << "[sets-model-details] > node: not: " << n << ", explanation:" << std::endl; + BOOST_FOREACH(TNode m, explanation) { + Debug("sets-model-details") << "[sets-model-details] >> " << m << std::endl; } } } @@ -585,8 +605,12 @@ void TheorySetsPrivate::collectModelInfo(TheoryModel* m, bool fullModel) checkPassed &= checkModel(settermElementsMap, term); } } - Assert( checkPassed, - "THEORY_SETS check-model failed. Run with -d sets-model for details." ); + if(Debug.isOn("sets-checkmodel-ignore")) { + Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; + } else { + Assert( checkPassed, + "THEORY_SETS check-model failed. Run with -d sets-model for details." ); + } #endif } @@ -735,10 +759,10 @@ bool TheorySetsPrivate::isComplete() { Node TheorySetsPrivate::getLemma() { Assert(!d_pending.empty() || !d_pendingDisequal.empty()); - Node lemma; + Node n, lemma; if(!d_pending.empty()) { - Node n = d_pending.front(); + n = d_pending.front(); d_pending.pop(); d_pendingEverInserted.insert(n); @@ -747,7 +771,7 @@ Node TheorySetsPrivate::getLemma() { lemma = OR(n, NOT(n)); } else { - Node n = d_pendingDisequal.front(); + n = d_pendingDisequal.front(); d_pendingDisequal.pop(); d_pendingEverInserted.insert(n); @@ -758,7 +782,7 @@ Node TheorySetsPrivate::getLemma() { lemma = OR(n, AND(l1, NOT(l2)), AND(NOT(l1), l2)); } - Debug("sets-lemma") << "[sets-lemma] " << lemma << std::endl; + Debug("sets-lemma") << "[sets-lemma] Generating for " << n << ", lemma: " << lemma << std::endl; return lemma; } @@ -777,7 +801,8 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_nodeSaver(c), d_pending(u), d_pendingDisequal(u), - d_pendingEverInserted(u) + d_pendingEverInserted(u), + d_scrutinize(NULL) { d_termInfoManager = new TermInfoManager(*this, c, &d_equalityEngine); @@ -787,12 +812,20 @@ TheorySetsPrivate::TheorySetsPrivate(TheorySets& external, d_equalityEngine.addFunctionKind(kind::MEMBER); d_equalityEngine.addFunctionKind(kind::SUBSET); + + if( Debug.isOn("sets-scrutinize") ) { + d_scrutinize = new TheorySetsScrutinize(this); + } }/* TheorySetsPrivate::TheorySetsPrivate() */ TheorySetsPrivate::~TheorySetsPrivate() { delete d_termInfoManager; + if( Debug.isOn("sets-scrutinize") ) { + Assert(d_scrutinize != NULL); + delete d_scrutinize; + } } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index 9576384bb..a4c9fb726 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -33,6 +33,7 @@ namespace sets { /** Internal classes, forward declared here */ class TheorySetsTermInfoManager; class TheorySets; +class TheorySetsScrutinize; class TheorySetsPrivate { public: @@ -166,6 +167,10 @@ private: const Elements& getElements(TNode setterm, SettermElementsMap& settermElementsMap) const; Node elementsToShape(Elements elements, TypeNode setType) const; bool checkModel(const SettermElementsMap& settermElementsMap, TNode S) const; + + // more debugging stuff + friend class TheorySetsScrutinize; + TheorySetsScrutinize* d_scrutinize; };/* class TheorySetsPrivate */ -- cgit v1.2.3 From f328d181c943237367a9f7374199ef5e58285faf Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 8 Apr 2014 15:06:38 -0400 Subject: more --- src/theory/sets/scrutinize.h | 33 ++++++++++++++++++++++++++++++++- src/theory/sets/theory_sets.h | 2 ++ src/theory/sets/theory_sets_private.cpp | 18 ++++++++++-------- src/theory/theory.cpp | 4 ++-- src/theory/theory.h | 10 ++++++---- 5 files changed, 52 insertions(+), 15 deletions(-) (limited to 'src/theory') diff --git a/src/theory/sets/scrutinize.h b/src/theory/sets/scrutinize.h index a0e2a1d5b..7343662c6 100644 --- a/src/theory/sets/scrutinize.h +++ b/src/theory/sets/scrutinize.h @@ -17,6 +17,9 @@ #pragma once +#include + +#include "theory/sets/theory_sets.h" #include "theory/sets/theory_sets_private.h" namespace CVC4 { @@ -24,7 +27,8 @@ namespace theory { namespace sets { class TheorySetsScrutinize { - TheorySetsPrivate* d_theory; + /* we don't want to accidentally modify theory data */ + const TheorySetsPrivate* d_theory; public: TheorySetsScrutinize(TheorySetsPrivate* theory): d_theory(theory) { Debug("sets") << "[sets] scrunitize enabled" << std::endl; @@ -35,6 +39,33 @@ public: // assume not in conflict, and complete: // - try building model // - check it + + TheorySetsPrivate::SettermElementsMap settermElementsMap; + TNode true_atom = NodeManager::currentNM()->mkConst(true); + std::set terms; + (d_theory->d_external).computeRelevantTerms(terms); + for(eq::EqClassIterator it_eqclasses(true_atom, &d_theory->d_equalityEngine); + ! it_eqclasses.isFinished() ; ++it_eqclasses) { + TNode n = (*it_eqclasses); + if(n.getKind() == kind::MEMBER) { + Assert(d_theory->d_equalityEngine.areEqual(n, true_atom)); + TNode x = d_theory->d_equalityEngine.getRepresentative(n[0]); + TNode S = d_theory->d_equalityEngine.getRepresentative(n[1]); + settermElementsMap[S].insert(x); + } + } + bool checkPassed = true; + BOOST_FOREACH(TNode term, terms) { + if( term.getType().isSet() ) { + checkPassed &= d_theory->checkModel(settermElementsMap, term); + } + } + if(Debug.isOn("sets-checkmodel-ignore")) { + Debug("sets-checkmodel-ignore") << "[sets-checkmodel-ignore] checkPassed value was " << checkPassed << std::endl; + } else { + Assert( checkPassed, + "THEORY_SETS check-model failed. Run with -d sets-model for details." ); + } } }; diff --git a/src/theory/sets/theory_sets.h b/src/theory/sets/theory_sets.h index f40031514..9f74064cb 100644 --- a/src/theory/sets/theory_sets.h +++ b/src/theory/sets/theory_sets.h @@ -27,10 +27,12 @@ namespace theory { namespace sets { class TheorySetsPrivate; +class TheorySetsScrutinize; class TheorySets : public Theory { private: friend class TheorySetsPrivate; + friend class TheorySetsScrutinize; TheorySetsPrivate* d_internal; public: diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index b29e2d4c6..2cc182819 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -89,18 +89,17 @@ void TheorySetsPrivate::check(Theory::Effort level) { Debug("sets") << "[sets] in conflict = " << d_conflict << std::endl; Assert( d_conflict ^ d_equalityEngine.consistent() ); - if(d_conflict) { - if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } - return; - } + if(d_conflict) { return; } Debug("sets") << "[sets] is complete = " << isComplete() << std::endl; } if( (Theory::EFFORT_FULL || options::setsEagerLemmas() ) && !isComplete()) { d_external.d_out->lemma(getLemma()); + return; } - if(Debug.isOn("sets-scrutinize")) { d_scrutinize.postCheckInvariants(); } + // if we are here, there is no conflict and we are complete + if(Debug.isOn("sets-scrutinize")) { d_scrutinize->postCheckInvariants(); } return; }/* TheorySetsPrivate::check() */ @@ -434,7 +433,8 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, const Elements emptySetOfElements; const Elements& saved = - d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET ? + d_equalityEngine.getRepresentative(S).getKind() == kind::EMPTYSET || + settermElementsMap.find(d_equalityEngine.getRepresentative(S)) == settermElementsMap.end() ? emptySetOfElements : settermElementsMap.find(d_equalityEngine.getRepresentative(S))->second; Debug("sets-model") << "[sets-model] saved : { "; @@ -446,12 +446,14 @@ bool TheorySetsPrivate::checkModel(const SettermElementsMap& settermElementsMap, Elements cur; const Elements& left = - d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET ? + d_equalityEngine.getRepresentative(S[0]).getKind() == kind::EMPTYSET || + settermElementsMap.find(d_equalityEngine.getRepresentative(S[0])) == settermElementsMap.end() ? emptySetOfElements : settermElementsMap.find(d_equalityEngine.getRepresentative(S[0]))->second; const Elements& right = - d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET ? + d_equalityEngine.getRepresentative(S[1]).getKind() == kind::EMPTYSET || + settermElementsMap.find(d_equalityEngine.getRepresentative(S[1])) == settermElementsMap.end() ? emptySetOfElements : settermElementsMap.find(d_equalityEngine.getRepresentative(S[1]))->second; diff --git a/src/theory/theory.cpp b/src/theory/theory.cpp index 9a23d5518..c52ee936a 100644 --- a/src/theory/theory.cpp +++ b/src/theory/theory.cpp @@ -176,7 +176,7 @@ std::hash_set Theory::currentlySharedTerms() const{ } -void Theory::collectTerms(TNode n, set& termSet) +void Theory::collectTerms(TNode n, set& termSet) const { if (termSet.find(n) != termSet.end()) { return; @@ -191,7 +191,7 @@ void Theory::collectTerms(TNode n, set& termSet) } -void Theory::computeRelevantTerms(set& termSet) +void Theory::computeRelevantTerms(set& termSet) const { // Collect all terms appearing in assertions context::CDList::const_iterator assert_it = facts_begin(), assert_it_end = facts_end(); diff --git a/src/theory/theory.h b/src/theory/theory.h index ff648e1f2..c86aa17de 100644 --- a/src/theory/theory.h +++ b/src/theory/theory.h @@ -229,12 +229,14 @@ protected: /** * Helper function for computeRelevantTerms */ - void collectTerms(TNode n, std::set& termSet); + void collectTerms(TNode n, std::set& termSet) const; /** - * Scans the current set of assertions and shared terms top-down until a theory-leaf is reached, and adds all terms found to termSet. - * This is used by collectModelInfo to delimit the set of terms that should be used when constructing a model + * Scans the current set of assertions and shared terms top-down + * until a theory-leaf is reached, and adds all terms found to + * termSet. This is used by collectModelInfo to delimit the set of + * terms that should be used when constructing a model */ - void computeRelevantTerms(std::set& termSet); + void computeRelevantTerms(std::set& termSet) const; /** * Construct a Theory. -- cgit v1.2.3 From b7af8484a897d0ed88dd30a3dd52383903a54b14 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 9 Apr 2014 12:21:07 -0400 Subject: try foreach on CD datastructure --- src/context/cdlist.h | 1 + src/theory/sets/theory_sets_private.cpp | 7 +++---- 2 files changed, 4 insertions(+), 4 deletions(-) (limited to 'src/theory') diff --git a/src/context/cdlist.h b/src/context/cdlist.h index 47d112cd8..c57a315f5 100644 --- a/src/context/cdlist.h +++ b/src/context/cdlist.h @@ -417,6 +417,7 @@ public: } };/* class CDList<>::const_iterator */ + typedef const_iterator iterator; /** * Returns an iterator pointing to the first item in the list. diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 2cc182819..42d417fc3 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1066,18 +1066,17 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue (CDTNodeList* l, TNode S, bool polarity) { - for(typeof(l->begin()) i = l->begin(); i != l->end(); ++i) { + BOOST_FOREACH(TNode x, (*l) ) { Debug("sets-prop") << "[sets-terminfo] setterm todo: " - << MEMBER(*i, d_eqEngine->getRepresentative(S)) + << MEMBER(x, d_eqEngine->getRepresentative(S)) << std::endl; - d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(*i), + d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), d_eqEngine->getRepresentative(S))); for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine); !j.isFinished(); ++j) { - TNode x = (*i); TNode S = (*j); Node cur_atom = MEMBER(x, S); -- cgit v1.2.3 From b9d0c68f2bb755280594c6016e1f327922633747 Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 9 Apr 2014 13:46:00 -0400 Subject: prep for fix --- src/theory/sets/term_info.h | 12 ++++ src/theory/sets/theory_sets_private.cpp | 105 ++++++++++++++++++++++---------- src/theory/sets/theory_sets_private.h | 2 + 3 files changed, 88 insertions(+), 31 deletions(-) (limited to 'src/theory') diff --git a/src/theory/sets/term_info.h b/src/theory/sets/term_info.h index ea435d9b7..2783faa79 100644 --- a/src/theory/sets/term_info.h +++ b/src/theory/sets/term_info.h @@ -31,12 +31,16 @@ class TheorySetsTermInfo { public: CDTNodeList* elementsInThisSet; CDTNodeList* elementsNotInThisSet; + CDTNodeList* setsContainingThisElement; + CDTNodeList* setsNotContainingThisElement; CDTNodeList* parents; TheorySetsTermInfo(context::Context* c) { elementsInThisSet = new(true)CDTNodeList(c); elementsNotInThisSet = new(true)CDTNodeList(c); + setsContainingThisElement = new(true)CDTNodeList(c); + setsNotContainingThisElement = new(true)CDTNodeList(c); parents = new(true)CDTNodeList(c); } @@ -45,11 +49,19 @@ public: else elementsNotInThisSet -> push_back(n); } + void addToSetList(TNode n, bool polarity) { + if(polarity) setsContainingThisElement -> push_back(n); + else setsNotContainingThisElement -> push_back(n); + } + ~TheorySetsTermInfo() { elementsInThisSet -> deleteSelf(); elementsNotInThisSet -> deleteSelf(); + setsContainingThisElement -> deleteSelf(); + setsNotContainingThisElement -> deleteSelf(); parents -> deleteSelf(); } + }; }/* CVC4::theory::sets namespace */ diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 42d417fc3..883e0147e 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -60,10 +60,12 @@ void TheorySetsPrivate::check(Theory::Effort level) { if (!d_equalityEngine.hasTerm(atom[0])) { Assert(atom[0].isConst()); d_equalityEngine.addTerm(atom[0]); + d_termInfoManager->addTerm(atom[0]); } if (!d_equalityEngine.hasTerm(atom[1])) { Assert(atom[1].isConst()); d_equalityEngine.addTerm(atom[1]); + d_termInfoManager->addTerm(atom[1]); } } } @@ -1063,6 +1065,64 @@ void TheorySetsPrivate::TermInfoManager::addTerm(TNode n) { } } +void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue +(TNode x, TNode S, bool polarity) +{ + Node cur_atom = MEMBER(x, S); + + // propagation : empty set + if(polarity && S.getKind() == kind::EMPTYSET) { + Debug("sets-prop") << "[sets-prop] something in empty set? conflict." + << std::endl; + d_theory.learnLiteral(cur_atom, false, cur_atom); + return; + }// propagation: empty set + + // propagation : children + if(S.getKind() == kind::UNION || + S.getKind() == kind::INTERSECTION || + S.getKind() == kind::SETMINUS || + S.getKind() == kind::SET_SINGLETON) { + d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S)); + }// propagation: children + + // propagation : parents + const CDTNodeList* parentList = getParents(S); + for(typeof(parentList->begin()) k = parentList->begin(); + k != parentList->end(); ++k) { + d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k)); + }// propagation : parents + +} + +void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue +(TNode x, CDTNodeList* l, bool polarity) +{ + set alreadyProcessed; + + BOOST_FOREACH(TNode S, (*l) ) { + Debug("sets-prop") << "[sets-terminfo] setterm todo: " + << MEMBER(x, d_eqEngine->getRepresentative(S)) + << std::endl; + + TNode repS = d_eqEngine->getRepresentative(S); + if(alreadyProcessed.find(repS) != alreadyProcessed.end()) { + continue; + } else { + alreadyProcessed.insert(repS); + } + + d_eqEngine->addTerm(MEMBER(d_eqEngine->getRepresentative(x), repS)); + + for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine); + !j.isFinished(); ++j) { + + pushToSettermPropagationQueue(x, *j, polarity); + + }//j loop + } +} + void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue (CDTNodeList* l, TNode S, bool polarity) { @@ -1077,32 +1137,7 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue for(eq::EqClassIterator j(d_eqEngine->getRepresentative(S), d_eqEngine); !j.isFinished(); ++j) { - TNode S = (*j); - Node cur_atom = MEMBER(x, S); - - // propagation : empty set - if(polarity && S.getKind() == kind::EMPTYSET) { - Debug("sets-prop") << "[sets-prop] something in empty set? conflict." - << std::endl; - d_theory.learnLiteral(cur_atom, false, cur_atom); - return; - }// propagation: empty set - - // propagation : children - if(S.getKind() == kind::UNION || - S.getKind() == kind::INTERSECTION || - S.getKind() == kind::SETMINUS || - S.getKind() == kind::SET_SINGLETON) { - d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, S)); - }// propagation: children - - // propagation : parents - const CDTNodeList* parentList = getParents(S); - for(typeof(parentList->begin()) k = parentList->begin(); - k != parentList->end(); ++k) { - d_theory.d_settermPropagationQueue.push_back(std::make_pair(x, *k)); - }// propagation : parents - + pushToSettermPropagationQueue(x, *j, polarity); }//j loop @@ -1110,11 +1145,10 @@ void TheorySetsPrivate::TermInfoManager::pushToSettermPropagationQueue } -void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { - // merge b into a - if(!a.getType().isSet()) return; +void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { + // merge b into a Debug("sets-terminfo") << "[sets-terminfo] Merging (into) a = " << a << ", b = " << b << std::endl; Debug("sets-terminfo") << "[sets-terminfo] reps" @@ -1128,16 +1162,25 @@ void TheorySetsPrivate::TermInfoManager::mergeTerms(TNode a, TNode b) { Assert(ita != d_info.end()); Assert(itb != d_info.end()); + /* elements in this sets */ pushToSettermPropagationQueue( (*ita).second->elementsInThisSet, b, true ); pushToSettermPropagationQueue( (*ita).second->elementsNotInThisSet, b, false ); pushToSettermPropagationQueue( (*itb).second->elementsNotInThisSet, a, false ); pushToSettermPropagationQueue( (*itb).second->elementsInThisSet, a, true ); - mergeLists((*ita).second->elementsInThisSet, (*itb).second->elementsInThisSet); - mergeLists((*ita).second->elementsNotInThisSet, (*itb).second->elementsNotInThisSet); + + /* sets containing this element */ + pushToSettermPropagationQueue( b, (*ita).second->setsContainingThisElement, true); + pushToSettermPropagationQueue( b, (*ita).second->setsNotContainingThisElement, false); + pushToSettermPropagationQueue( a, (*itb).second->setsNotContainingThisElement, false); + pushToSettermPropagationQueue( a, (*itb).second->setsContainingThisElement, true); + mergeLists( (*ita).second->setsContainingThisElement, + (*itb).second->setsContainingThisElement ); + mergeLists( (*ita).second->setsNotContainingThisElement, + (*itb).second->setsNotContainingThisElement ); } diff --git a/src/theory/sets/theory_sets_private.h b/src/theory/sets/theory_sets_private.h index a4c9fb726..7e9d60905 100644 --- a/src/theory/sets/theory_sets_private.h +++ b/src/theory/sets/theory_sets_private.h @@ -108,7 +108,9 @@ private: std::hash_map d_info; void mergeLists(CDTNodeList* la, const CDTNodeList* lb) const; + void pushToSettermPropagationQueue(TNode x, TNode S, bool polarity); void pushToSettermPropagationQueue(CDTNodeList* l, TNode S, bool polarity); + void pushToSettermPropagationQueue(TNode x, CDTNodeList* l, bool polarity); public: TermInfoManager(TheorySetsPrivate&, context::Context* satContext, -- cgit v1.2.3 From b0c881cdcbf598bed9671a9ee4a1c11e51e08b8e Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Wed, 9 Apr 2014 14:03:35 -0400 Subject: fix --- src/theory/sets/theory_sets_private.cpp | 1 + 1 file changed, 1 insertion(+) (limited to 'src/theory') diff --git a/src/theory/sets/theory_sets_private.cpp b/src/theory/sets/theory_sets_private.cpp index 883e0147e..f56f509b2 100644 --- a/src/theory/sets/theory_sets_private.cpp +++ b/src/theory/sets/theory_sets_private.cpp @@ -1035,6 +1035,7 @@ void TheorySetsPrivate::TermInfoManager::notifyMembership(TNode fact) { << " in " << S << " " << polarity << std::endl; d_info[S]->addToElementList(x, polarity); + d_info[x]->addToSetList(S, polarity); } const CDTNodeList* TheorySetsPrivate::TermInfoManager::getParents(TNode x) { -- cgit v1.2.3