summaryrefslogtreecommitdiff
path: root/src/theory/theory_engine.h
diff options
context:
space:
mode:
Diffstat (limited to 'src/theory/theory_engine.h')
-rw-r--r--src/theory/theory_engine.h189
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 */
generated by cgit on debian on lair
contact matthew@masot.net with questions or feedback