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.

4 files changed, 92 insertions, 39 deletions

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d514744f..0acd81248 100644
--- a/src/smt/smt_engine.cpp
+++ b/src/smt/smt_engine.cpp
@@ -1102,7 +1102,9 @@ void SmtEnginePrivate::processAssertions() {
 
   // begin: INVARIANT to maintain: no reordering of assertions or
   // introducing new ones
+#ifdef CVC4_ASSERTIONS
   unsigned iteRewriteAssertionsEnd = d_assertionsToCheck.size();
+#endif
 
   Trace("smt") << "SmtEnginePrivate::processAssertions() POST SIMPLIFICATION" << endl;
   Debug("smt") << " d_assertionsToPreprocess: " << d_assertionsToPreprocess.size() << endl;
diff --git a/src/theory/arith/theory_arith.cpp b/src/theory/arith/theory_arith.cpp
index 1179de685..d660cb4cd 100644
--- a/src/theory/arith/theory_arith.cpp
+++ b/src/theory/arith/theory_arith.cpp
@@ -1487,11 +1487,10 @@ DeltaRational TheoryArith::getDeltaValue(TNode n) {
   default:
     {
       if(isSetup(n)){
-	ArithVar var = d_arithvarNodeMap.asArithVar(n);
-	return d_partialModel.getAssignment(var);
+        ArithVar var = d_arithvarNodeMap.asArithVar(n);
+        return d_partialModel.getAssignment(var);
       }else{
-	Warning() << "you did not setup this up!: " << n << endl;
-	return DeltaRational();
+        Unreachable();
       }
     }
   }
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());
diff --git a/src/theory/theory.h b/src/theory/theory.h
index 40f72dafc..9ac07d849 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -619,7 +619,7 @@ public:
 
   /** Add the theory to the set. If no set specified, just returns a singleton set */
   static inline Set setRemove(TheoryId theory, Set set = 0) {
-    return set ^ (1 << theory);
+    return setDifference(set, setInsert(theory));
   }
 
   /** Check if the set contains the theory */
@@ -656,13 +656,15 @@ public:
     return ss.str();
   }
 
+  typedef context::CDList<Assertion>::const_iterator assertions_iterator;
+
   /**
    * Provides access to the facts queue, primarily intended for theory
    * debugging purposes.
    *
    * @return the iterator to the beginning of the fact queue
    */
-  context::CDList<Assertion>::const_iterator facts_begin() const {
+  assertions_iterator facts_begin() const {
     return d_facts.begin();
   }
 
@@ -672,17 +674,19 @@ public:
    *
    * @return the iterator to the end of the fact queue
    */
-  context::CDList<Assertion>::const_iterator facts_end() const {
+  assertions_iterator facts_end() const {
     return d_facts.end();
   }
 
+  typedef context::CDList<TNode>::const_iterator shared_terms_iterator;
+
   /**
    * Provides access to the shared terms, primarily intended for theory
    * debugging purposes.
    *
    * @return the iterator to the beginning of the shared terms list
    */
-  context::CDList<TNode>::const_iterator shared_terms_begin() const {
+  shared_terms_iterator shared_terms_begin() const {
     return d_sharedTerms.begin();
   }
 
@@ -692,7 +696,7 @@ public:
    *
    * @return the iterator to the end of the shared terms list
    */
-  context::CDList<TNode>::const_iterator shared_terms_end() const {
+  shared_terms_iterator shared_terms_end() const {
     return d_sharedTerms.end();
   }