From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Mon, 14 May 2012 15:13:05 +0000 (+0000)
Subject: fixing up preregistration again
X-Git-Tag: cvc5-1.0.0~8183
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=4c49dd9bcc859a07bebf969ee126ee2f4ffa2384;p=cvc5.git

fixing up preregistration again
---

diff --git a/src/theory/arrays/array_info.cpp b/src/theory/arrays/array_info.cpp
index 643fbaedf..c062f4edc 100644
--- a/src/theory/arrays/array_info.cpp
+++ b/src/theory/arrays/array_info.cpp
@@ -176,8 +176,9 @@ void ArrayInfo::setRIntro1Applied(const TNode a) {
 const Info* ArrayInfo::getInfo(const TNode a) const{
   CNodeInfoMap::const_iterator it = info_map.find(a);
 
-  if(it!= info_map.end())
+  if(it!= info_map.end()) {
       return (*it).second;
+  }
   return emptyInfo;
 }
 
@@ -185,8 +186,9 @@ const bool ArrayInfo::isNonLinear(const TNode a) const
 {
   CNodeInfoMap::const_iterator it = info_map.find(a);
 
-  if(it!= info_map.end())
+  if(it!= info_map.end()) {
     return (*it).second->isNonLinear;
+  }
   return false;
 }
 
@@ -194,8 +196,9 @@ const bool ArrayInfo::rIntro1Applied(const TNode a) const
 {
   CNodeInfoMap::const_iterator it = info_map.find(a);
 
-  if(it!= info_map.end())
+  if(it!= info_map.end()) {
     return (*it).second->rIntro1Applied;
+  }
   return false;
 }
 
diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 75426cba4..0f8822e72 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -40,21 +40,17 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
     return false;
   }
 
-  Theory::Set theories;
-
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
-  // Remember the theories interested in this term
-  d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
-  // Check if there are multiple of those
-  d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
+  d_theories = Theory::setInsert(currentTheoryId, d_theories);
+  d_theories = Theory::setInsert(parentTheoryId, d_theories);
 
-  theories = (*find).second;
-  if (Theory::setContains(currentTheoryId, theories)) {
+  Theory::Set visitedTheories = (*find).second;
+  if (Theory::setContains(currentTheoryId, visitedTheories)) {
     // 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);
+    Debug("register::internal") << (Theory::setContains(parentTheoryId, visitedTheories) ? "2:true" : "2:false") << std::endl;
+    return Theory::setContains(parentTheoryId, visitedTheories);
   } else {
     // If the current theory is not registered, it still needs to be visited
     Debug("register::internal") << "3:false" << std::endl;
@@ -64,8 +60,6 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
 void PreRegisterVisitor::visit(TNode current, TNode parent) {
 
-  Theory::Set theories;
-
   Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
   if (Debug.isOn("register::internal")) {
     Debug("register::internal") << toString() << std::endl;
@@ -75,24 +69,21 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
-  // Remember the theories interested in this term
-  d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
-  // If there are theories other than the parent itself, we are in multi-theory case
-  d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
-
-  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_visited[current] = theories = Theory::setInsert(currentTheoryId, theories);
+  Theory::Set visitedTheories = d_visited[current];
+  Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
+  if (!Theory::setContains(currentTheoryId, visitedTheories)) {
+    visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
+    d_visited[current] = visitedTheories;
     d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current);
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
   }
-  if (!Theory::setContains(parentTheoryId, theories)) {
-    d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories);
+  if (!Theory::setContains(parentTheoryId, visitedTheories)) {
+    visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
+    d_visited[current] = visitedTheories;
     d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current);
     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;
+  Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 
   Assert(d_visited.find(current) != d_visited.end());
   Assert(alreadyVisited(current, parent));
@@ -103,11 +94,8 @@ void PreRegisterVisitor::start(TNode node) {
 }
 
 bool PreRegisterVisitor::done(TNode node) {
-// <<<<<<< .working
-//   d_engine->markActive(d_theories[node]);
-// =======
-// >>>>>>> .merge-right.r3396
-  return d_multipleTheories;
+  // We have multiple theories if removing the node theory from others is non-empty
+  return Theory::setRemove(Theory::theoryOf(node), d_theories);
 }
 
 std::string SharedTermsVisitor::toString() const {
diff --git a/src/theory/term_registration_visitor.h b/src/theory/term_registration_visitor.h
index 11a56ec1e..ac3494193 100644
--- a/src/theory/term_registration_visitor.h
+++ b/src/theory/term_registration_visitor.h
@@ -26,7 +26,15 @@ namespace CVC4 {
 class TheoryEngine;
 
 /**
- * Visitor that calls the apropriate theory to preregister the term.
+ * Visitor that calls the appropriate theory to pre-register the term. The visitor also keeps track
+ * of the sets of theories that are involved in the terms, so that it can say if there are multiple
+ * theories involved.
+ *
+ * A sub-term has been visited if the theories of both the parent and the term itself have already
+ * visited this term.
+ *
+ * Computation of the set of theories in the original term are computed in the alreadyVisited method
+ * so as no to skip any theories.
  */
 class PreRegisterVisitor {
 
@@ -41,9 +49,9 @@ class PreRegisterVisitor {
   TNodeToTheorySetMap d_visited;
 
   /**
-   * Map from terms to the theories that have have a sub-term in it.
+   * A set of all theories in the term
    */
-  TNodeToTheorySetMap d_theories;
+  theory::Theory::Set d_theories;
 
   /**
    * Is true if the term we're traversing involves multiple theories.
@@ -63,7 +71,7 @@ public:
   PreRegisterVisitor(TheoryEngine* engine, context::Context* context)
   : d_engine(engine)
   , d_visited(context)
-  , d_theories(context)
+  , d_theories(0)
   , d_multipleTheories(false)
   {}
 
diff --git a/src/theory/theory_engine.cpp b/src/theory/theory_engine.cpp
index 77a768152..a8af6de1d 100644
--- a/src/theory/theory_engine.cpp
+++ b/src/theory/theory_engine.cpp
@@ -91,7 +91,6 @@ void TheoryEngine::preRegister(TNode preprocessed) {
   if(Dump.isOn("missed-t-propagations")) {
     d_possiblePropagations.push_back(preprocessed);
   }
-  //<<<<<<< .working
   d_preregisterQueue.push(preprocessed);
 
   if (!d_inPreregister) {
@@ -109,21 +108,12 @@ void TheoryEngine::preRegister(TNode preprocessed) {
       if (multipleTheories) {
         // Collect the shared terms if there are multipe theories
         NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
-        // Mark the multiple theories flag
-        //d_sharedTermsExist = true;
       }
     }
+
     // Leaving pre-register
     d_inPreregister = false;
   }
-// =======
-  // Pre-register the terms in the atom
-  // bool multipleTheories = NodeVisitor<PreRegisterVisitor>::run(d_preRegistrationVisitor, preprocessed);
-  // if (multipleTheories) {
-  //   // Collect the shared terms if there are multipe theories
-  //   NodeVisitor<SharedTermsVisitor>::run(d_sharedTermsVisitor, preprocessed);
-  //   //>>>>>>> .merge-right.r3396
-  // }
 }
 
 void TheoryEngine::printAssertions(const char* tag) {