fixes for shared term registration. previously the type was not considered when looking at theories of the term and for a term like

read(a, f(x))

the term f(x) would not be registered to arithmetic in AUFLIA. this fixies the issue of bug 330 and moves it to some other assertion fail.

1 files changed, 78 insertions, 30 deletions

diff --git a/src/theory/term_registration_visitor.cpp b/src/theory/term_registration_visitor.cpp
index 0f8822e72..7d82dee8e 100644
--- a/src/theory/term_registration_visitor.cpp
+++ b/src/theory/term_registration_visitor.cpp
@@ -32,28 +32,41 @@ bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
 
   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ") => ";
 
-  TNodeToTheorySetMap::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);
-  TheoryId parentTheoryId  = Theory::theoryOf(parent);
+  TheoryId parentTheoryId = Theory::theoryOf(parent);
 
   d_theories = Theory::setInsert(currentTheoryId, d_theories);
   d_theories = Theory::setInsert(parentTheoryId, d_theories);
 
+  // Should we use the theory of the type
+  bool useType = current != parent && currentTheoryId != parentTheoryId;
+
+  // Get the theories that have already visited this node
+  TNodeToTheorySetMap::iterator find = d_visited.find(current);
+  if (find == d_visited.end()) {
+    if (useType) {
+      TheoryId typeTheoryId = Theory::theoryOf(current.getType());
+      d_theories = Theory::setInsert(typeTheoryId, d_theories);
+    }
+    return false;
+  }
+
   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, visitedTheories) ? "2:true" : "2:false") << std::endl;
-    return Theory::setContains(parentTheoryId, visitedTheories);
+    // The current theory has already visited it, so now it depends on the parent and the type
+    if (Theory::setContains(parentTheoryId, visitedTheories)) {
+      if (useType) {
+        TheoryId typeTheoryId = Theory::theoryOf(current.getType());
+        d_theories = Theory::setInsert(typeTheoryId, d_theories);
+        return Theory::setContains(typeTheoryId, visitedTheories);
+      } else {
+        return true;
+      }
+    } else {
+      return false;
+    }
   } else {
-    // If the current theory is not registered, it still needs to be visited
-    Debug("register::internal") << "3:false" << std::endl;
     return false;
   }
 }
@@ -69,6 +82,9 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
+  // Should we use the theory of the type
+  bool useType = current != parent && currentTheoryId != parentTheoryId;
+
   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)) {
@@ -83,6 +99,15 @@ void PreRegisterVisitor::visit(TNode current, TNode parent) {
     d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current);
     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
   }
+  if (useType) {
+    TheoryId typeTheoryId  = Theory::theoryOf(current.getType());
+    if (!Theory::setContains(typeTheoryId, visitedTheories)) {
+      visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
+      d_visited[current] = visitedTheories;
+      d_engine->theoryOf(typeTheoryId)->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(visitedTheories) << std::endl;
 
   Assert(d_visited.find(current) != d_visited.end());
@@ -124,13 +149,21 @@ bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
   TheoryId currentTheoryId = Theory::theoryOf(current);
   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 
+  // Should we use the theory of the type
+  bool useType = current != parent && currentTheoryId != parentTheoryId;
+
   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);
+      if (Theory::setContains(parentTheoryId, theories)) {
+        if (useType) {
+          TheoryId typeTheoryId = Theory::theoryOf(current.getType());
+          return Theory::setContains(typeTheoryId, theories);
+        } else {
+          return true;
+        }
+      } else {
+        return false;
+      }
   } else {
-    // If the current theory is not registered, it still needs to be visited
-    Debug("register::internal") << "2:false" << std::endl;
     return false;
   }
 }
@@ -144,24 +177,39 @@ void SharedTermsVisitor::visit(TNode current, TNode parent) {
   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 ++;
+  bool useType = current != parent && currentTheoryId != parentTheoryId;
+
+  unsigned newTheoriesCount = 0;
+  Theory::Set visitedTheories = d_visited[current];
+  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
+  if (!Theory::setContains(currentTheoryId, visitedTheories)) {
+    visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
+    newTheoriesCount ++;
     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 ++;
+  if (!Theory::setContains(parentTheoryId, visitedTheories)) {
+    visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
+    newTheoriesCount ++;
     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 (useType) {
+    TheoryId typeTheoryId = Theory::theoryOf(current.getType());
+    if (!Theory::setContains(typeTheoryId, visitedTheories)) {
+      visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
+      newTheoriesCount ++;
+      Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
+    }
+  }
+  Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
+
+  // Record the new theories that we visited
+  if (newTheoriesCount > 0) {
+    d_visited[current] = visitedTheories;
+  }
 
   // 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);
+  if (newTheoriesCount > 1) {
+    d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
   }
 
   Assert(d_visited.find(current) != d_visited.end());