diff options
Diffstat (limited to 'src/theory/sets/scrutinize.h')
| -rw-r--r-- | src/theory/sets/scrutinize.h | 33 |
1 files changed, 32 insertions, 1 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." ); + } } }; |