diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-09-15 06:53:33 +0000 |
commit | 72f552ead344b13d90832222157b970ae3dec8ff (patch) | |
tree | b02854356d5c5f98b3873f858f38b6762135bdc1 /src/theory/term_registration_visitor.cpp | |
parent | 62a50760346e130345b24e8a14ad0dac0dca5d38 (diff) |
additional stuff for sharing,
Diffstat (limited to 'src/theory/term_registration_visitor.cpp')
-rw-r--r-- | src/theory/term_registration_visitor.cpp | 182 |
1 files changed, 182 insertions, 0 deletions
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp new file mode 100644 index 000000000..1e7222532 --- /dev/null +++ b/src/theory/term_registration_visitor.cpp @@ -0,0 +1,182 @@ +/********************* */ +/*! \file term_registration_visitor.h + ** \verbatim + ** Original author: dejan + ** Major contributors: + ** Minor contributors (to current version): + ** This file is part of the CVC4 prototype. + ** Copyright (c) 2009, 2010, 2011 The Analysis of Computer Systems Group (ACSys) + ** Courant Institute of Mathematical Sciences + ** New York University + ** See the file COPYING in the top-level source directory for licensing + ** information.\endverbatim + **/ + +#include "theory/term_registration_visitor.h" +#include "theory/theory_engine.h" + +using namespace std; +using namespace CVC4; +using namespace theory; + +std::string PreRegisterVisitor::toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + } + return ss.str(); +} + +bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) const { + + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + TNodeVisitedMap::iterator find = d_visited.find(current); + + // If node is not visited at all, just return false + if (find == d_visited.end()) { + Debug("register::internal") << "1:false" << std::endl; + return false; + } + + Theory::Set theories = (*find).second; + + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (Theory::setContains(currentTheoryId, theories)) { + // The current theory has already visited it, so now it depends on the parent + Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, theories); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "2:false" << std::endl; + return false; + } +} + +void PreRegisterVisitor::visit(TNode current, TNode parent) { + + Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + Theory::Set theories = d_visited[current]; + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; + if (!Theory::setContains(currentTheoryId, theories)) { + d_multipleTheories = d_multipleTheories || (theories != 0); + d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); + d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(currentTheoryId, d_theories); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; + } + if (!Theory::setContains(parentTheoryId, theories)) { + d_multipleTheories = d_multipleTheories || (theories != 0); + d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; + } + Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; + + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); +} + +void PreRegisterVisitor::start(TNode node) { + d_theories = 0; + d_multipleTheories = false; +} + +bool PreRegisterVisitor::done(TNode node) { + d_engine->markActive(d_theories); + return d_multipleTheories; +} + +std::string SharedTermsVisitor::toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl; + } + return ss.str(); +} + +bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const { + + Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + TNodeVisitedMap::const_iterator find = d_visited.find(current); + + // If node is not visited at all, just return false + if (find == d_visited.end()) { + Debug("register::internal") << "1:false" << std::endl; + return false; + } + + Theory::Set theories = (*find).second; + + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (Theory::setContains(currentTheoryId, theories)) { + // The current theory has already visited it, so now it depends on the parent + Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl; + return Theory::setContains(parentTheoryId, theories); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "2:false" << std::endl; + return false; + } +} + +void SharedTermsVisitor::visit(TNode current, TNode parent) { + + Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + Theory::Set theories = d_visited[current]; + unsigned theoriesCount = theories == 0 ? 0 : 1; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl; + if (!Theory::setContains(currentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories); + theoriesCount ++; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl; + } + if (!Theory::setContains(parentTheoryId, theories)) { + d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories); + theoriesCount ++; + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl; + } + Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl; + + // If there is more than two theories and a new one has been added notify the shared terms database + if (theoriesCount > 1) { + d_sharedTerms.addSharedTerm(d_atom, current, theories); + } + + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); +} + +void SharedTermsVisitor::start(TNode node) { + clear(); + d_atom = node; +} + +void SharedTermsVisitor::done(TNode node) { + clear(); +} + +void SharedTermsVisitor::clear() { + d_atom = TNode(); + d_visited.clear(); +} |