diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-27 00:33:22 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2011-08-27 00:33:22 +0000 |
commit | 6e81c8b4b146d58d94eb0a84fa8392bae04595ff (patch) | |
tree | 7d289459a318d2dae1c7dddd8be95c2582423f54 /src/theory/theory_engine.h | |
parent | 2faa78b68ca26f73e757f225f0786450e33c625f (diff) |
Removing Theory::registerTerm() as discussed in the meeting. Now pre-register is called on all the theory terms and the foreign-terms also. This means, if x: REAL and f:REAL, that in f(x) >= 0, arithmetic gets pre-register call with x, f(x) and f(x) >= 0, while UF gets pre-register call with x, f(x).
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r-- | src/theory/theory_engine.h | 189 |
1 files changed, 132 insertions, 57 deletions
diff --git a/src/theory/theory_engine.h b/src/theory/theory_engine.h index c472a1c41..ea3fe95c1 100644 --- a/src/theory/theory_engine.h +++ b/src/theory/theory_engine.h @@ -68,19 +68,7 @@ class TheoryEngine { * runs (no sharing), can reduce the cost of walking the DAG on * registration, etc. */ - bool d_theoryIsActive[theory::THEORY_LAST]; - - /** - * The count of active theories in the d_theoryIsActive bitmap. - */ - size_t d_activeTheories; - - /** - * Need the registration infrastructure when theory sharing is on - * (>=2 active theories) or when the sole active theory has - * requested it. - */ - bool d_needRegistration; + theory::Theory::Set d_activeTheories; /** * Cache from proprocessing of atoms. @@ -108,11 +96,6 @@ class TheoryEngine { */ std::vector<TNode> d_propagatedLiterals; - /** Time spent in newFact() (largely spent doing term registration) */ - KEEP_STATISTIC(TimerStat, - d_newFactTimer, - "theory::newFactTimer"); - /** * Check if the node is in conflict for debug purposes */ @@ -150,7 +133,7 @@ class TheoryEngine { // Construct the lemma (note that no CNF caching should happen as all the literals already exists) Assert(isProperConflict(conflictNode)); - d_engine->newLemma(conflictNode, true, true); + d_engine->newLemma(conflictNode, true, false); if(safe) { throw theory::Interrupted(); @@ -214,24 +197,16 @@ class TheoryEngine { /** * Mark a theory active if it's not already. */ - void markActive(theory::TheoryId th) { - if(!d_theoryIsActive[th]) { - d_theoryIsActive[th] = true; - if(th != theory::THEORY_BUILTIN && th != theory::THEORY_BOOL) { - if(++d_activeTheories == 1) { - // theory requests registration - d_needRegistration = hasRegisterTerm(th); - } else { - // need it for sharing - d_needRegistration = true; - } - } - Notice() << "Theory " << th << " has been activated (registration is " - << (d_needRegistration ? "on" : "off") << ")." << std::endl; - } + void markActive(theory::Theory::Set theories) { + d_activeTheories = theory::Theory::setUnion(d_activeTheories, theories); } - bool hasRegisterTerm(theory::TheoryId th) const; + /** + * Is the theory active. + */ + bool isActive(theory::TheoryId theory) { + return theory::Theory::setContains(theory, d_activeTheories); + } /** The logic of the problem */ std::string d_logic; @@ -321,6 +296,16 @@ public: } /** + * Get the theory associated to a the given theory id. + * + * @returns the theory, or NULL if the TNode is + * of built-in type. + */ + inline theory::Theory* theoryOf(theory::TheoryId theoryId) { + return d_theoryTable[theoryId]; + } + + /** * Solve the given literal with a theory that owns it. */ theory::Theory::SolveStatus solve(TNode literal, theory::SubstitutionMap& substitionOut); @@ -453,40 +438,130 @@ private: /** The engine */ TheoryEngine& d_engine; + /** + * Cache from proprocessing of atoms. + */ + typedef std::hash_map<TNode, theory::Theory::Set, TNodeHashFunction> TNodeVisitedMap; + TNodeVisitedMap d_visited; + + /** + * All the theories of the visitation. + */ + theory::Theory::Set d_theories; + + std::string toString() const { + std::stringstream ss; + TNodeVisitedMap::const_iterator it = d_visited.begin(); + for (; it != d_visited.end(); ++ it) { + ss << it->first << ": " << theory::Theory::setToString(it->second) << std::endl; + } + return ss.str(); + } + public: - PreRegisterVisitor(TheoryEngine& engine): d_engine(engine) {} + PreRegisterVisitor(TheoryEngine& engine): d_engine(engine), d_theories(0) {} - void operator () (TNode current) { - // Get the theory of the term and pre-register it with the owning theory - theory::TheoryId currentTheoryId = theory::Theory::theoryOf(current); - Debug("register") << "preregistering " << current << " with " << currentTheoryId << std::endl; - d_engine.markActive(currentTheoryId); - theory::Theory* currentTheory = d_engine.theoryOf(current); - currentTheory->preRegisterTerm(current); + bool alreadyVisited(TNode current, TNode parent) { + + Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => "; + + using namespace theory; + + 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; + } + + TheoryId currentTheoryId = Theory::theoryOf(current); + if (Theory::setContains(currentTheoryId, find->second)) { + // The current theory has already visited it, so now it depends on the parent + TheoryId parentTheoryId = Theory::theoryOf(parent); + if (parentTheoryId == currentTheoryId) { + // If it's the same theory, we've visited it already + Debug("register::internal") << "2:true" << std::endl; + return true; + } + // If not the same theory, we might have visited it, just check + Debug("register::internal") << (Theory::setContains(parentTheoryId, find->second) ? "3:true" : "3:false") << std::endl; + return Theory::setContains(parentTheoryId, find->second); + } else { + // If the current theory is not registered, it still needs to be visited + Debug("register::internal") << "4:false" << std::endl; + return false; + } } - }; - /** - * Visitor that calls the apropriate theory to preregister the term. - */ - class RegisterVisitor { + void visit(TNode current, TNode parent) { - /** The engine */ - TheoryEngine& d_engine; + Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl; + Debug("register::internal") << toString() << std::endl; - public: + using namespace theory; + + // Get the theories of the terms + TheoryId currentTheoryId = Theory::theoryOf(current); + TheoryId parentTheoryId = Theory::theoryOf(parent); + + if (currentTheoryId == parentTheoryId) { + // If it's the same theory we just add it + TNodeVisitedMap::iterator find = d_visited.find(current); + if (find == d_visited.end()) { + d_visited[current] = Theory::setInsert(currentTheoryId); + } else { + find->second = Theory::setInsert(currentTheoryId, find->second); + } + // Visit it + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + // Mark the theory as active + d_theories = Theory::setInsert(currentTheoryId, d_theories); + } else { + // If two theories, one might have visited it already + // If it's the same theory we just add it + TNodeVisitedMap::iterator find = d_visited.find(current); + if (find == d_visited.end()) { + // If not in the map at all, we just add both + d_visited[current] = Theory::setInsert(parentTheoryId, Theory::setInsert(currentTheoryId)); + // And visit both + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); + // Mark both theories as active + d_theories = Theory::setInsert(currentTheoryId, d_theories); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + } else { + if (!Theory::setContains(currentTheoryId, find->second)) { + find->second = Theory::setInsert(currentTheoryId, find->second); + d_engine.theoryOf(currentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(currentTheoryId, d_theories); + } + if (!Theory::setContains(parentTheoryId, find->second)) { + find->second = Theory::setInsert(parentTheoryId, find->second); + d_engine.theoryOf(parentTheoryId)->preRegisterTerm(current); + d_theories = Theory::setInsert(parentTheoryId, d_theories); + } + } + } - RegisterVisitor(TheoryEngine& engine): d_engine(engine) {} + Assert(d_visited.find(current) != d_visited.end()); + Assert(alreadyVisited(current, parent)); + } - void operator () (TNode current) { - // Register this node to it's theory - theory::Theory* currentTheory = d_engine.theoryOf(current); - Debug("register") << "registering " << current << " with " << currentTheory->getId() << std::endl; - currentTheory->registerTerm(current); + void start(TNode node) { + d_theories = 0; } + + void done(TNode node) { + d_engine.markActive(d_theories); + } + }; + /** Default visitor for pre-registration */ + PreRegisterVisitor d_preRegistrationVisitor; + };/* class TheoryEngine */ }/* CVC4 namespace */ |