From f328d181c943237367a9f7374199ef5e58285faf Mon Sep 17 00:00:00 2001 From: Kshitij Bansal Date: Tue, 8 Apr 2014 15:06:38 -0400 Subject: [PATCH] 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(-) 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. -- 2.30.2