fixes for shared term registration. previously the type was not considered when looki...

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.

diff --git a/src/smt/smt_engine.cpp b/src/smt/smt_engine.cpp
index 5d514744fa1bfd3629fda4d2ceebe507f5a830cc..0acd812489cb7cb094d88b7ceab410b77c714ad4 100644 (file)
--- 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 1179de685e37da4c515192a0a8b724fc9e155cb7..d660cb4cd1fa76ccd53230b8debeb2634c86172a 100644 (file)
--- 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 0f8822e7213c073ebb5c80e48b859ab9bff50fca..7d82dee8e8ee78839df8ae8a5bf9a30471ac643b 100644 (file)
--- 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 40f72dafce56cb9f9b2660430bb2fca9f9744999..9ac07d8492f20c97459bc6d491a593778e92bde9 100644 (file)
--- 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();
   }