diff options
author | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-08 15:06:38 -0400 |
---|---|---|
committer | Kshitij Bansal <kshitij@cs.nyu.edu> | 2014-04-09 14:51:22 -0400 |
commit | f328d181c943237367a9f7374199ef5e58285faf (patch) | |
tree | 839cb4742f8a61a0f7b73a6cbb1d7943cbdef850 /src/theory/sets | |
parent | b6d9f0bd9058db1358897834ac987f5d34de8734 (diff) |
more
Diffstat (limited to 'src/theory/sets')
-rw-r--r-- | src/theory/sets/scrutinize.h | 33 | ||||
-rw-r--r-- | src/theory/sets/theory_sets.h | 2 | ||||
-rw-r--r-- | src/theory/sets/theory_sets_private.cpp | 18 |
3 files changed, 44 insertions, 9 deletions
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 <boost/foreach.hpp> + +#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<bool>(true); + std::set<Node> 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; |