src/theory/term_registration_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file term_registration_visitor.h
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors:
   6  ** Minor contributors (to current version):
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009, 2010, 2011  The Analysis of Computer Systems Group (ACSys)
   9  ** Courant Institute of Mathematical Sciences
  10  ** New York University
  11  ** See the file COPYING in the top-level source directory for licensing
  12  ** information.\endverbatim
  13  **/
  14
  15 #include "theory/term_registration_visitor.h"
  16 #include "theory/theory_engine.h"
  17
  18 using namespace std;
  19 using namespace CVC4;
  20 using namespace theory;
  21
  22 std::string PreRegisterVisitor::toString() const {
  23   std::stringstream ss;
  24   TNodeToTheorySetMap::const_iterator it = d_visited.begin();
  25   for (; it != d_visited.end(); ++ it) {
  26     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
  27   }
  28   return ss.str();
  29 }
  30
  31 bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
  32
  33   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
  34
  35   TheoryId currentTheoryId = Theory::theoryOf(current);
  36   TheoryId parentTheoryId = Theory::theoryOf(parent);
  37
  38   d_theories = Theory::setInsert(currentTheoryId, d_theories);
  39   d_theories = Theory::setInsert(parentTheoryId, d_theories);
  40
  41   // Should we use the theory of the type
  42   bool useType = current != parent && currentTheoryId != parentTheoryId;
  43
  44   // Get the theories that have already visited this node
  45   TNodeToTheorySetMap::iterator find = d_visited.find(current);
  46   if (find == d_visited.end()) {
  47     if (useType) {
  48       TheoryId typeTheoryId = Theory::theoryOf(current.getType());
  49       d_theories = Theory::setInsert(typeTheoryId, d_theories);
  50     }
  51     return false;
  52   }
  53
  54   Theory::Set visitedTheories = (*find).second;
  55   if (Theory::setContains(currentTheoryId, visitedTheories)) {
  56     // The current theory has already visited it, so now it depends on the parent and the type
  57     if (Theory::setContains(parentTheoryId, visitedTheories)) {
  58       if (useType) {
  59         TheoryId typeTheoryId = Theory::theoryOf(current.getType());
  60         d_theories = Theory::setInsert(typeTheoryId, d_theories);
  61         return Theory::setContains(typeTheoryId, visitedTheories);
  62       } else {
  63         return true;
  64       }
  65     } else {
  66       return false;
  67     }
  68   } else {
  69     return false;
  70   }
  71 }
  72
  73 void PreRegisterVisitor::visit(TNode current, TNode parent) {
  74
  75   Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
  76   if (Debug.isOn("register::internal")) {
  77     Debug("register::internal") << toString() << std::endl;
  78   }
  79
  80   // Get the theories of the terms
  81   TheoryId currentTheoryId = Theory::theoryOf(current);
  82   TheoryId parentTheoryId  = Theory::theoryOf(parent);
  83
  84   // Should we use the theory of the type
  85   bool useType = current != parent && currentTheoryId != parentTheoryId;
  86
  87   Theory::Set visitedTheories = d_visited[current];
  88   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
  89   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
  90     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
  91     d_visited[current] = visitedTheories;
  92     d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current);
  93     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
  94   }
  95   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
  96     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
  97     d_visited[current] = visitedTheories;
  98     d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current);
  99     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 100   }
 101   if (useType) {
 102     TheoryId typeTheoryId  = Theory::theoryOf(current.getType());
 103     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 104       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 105       d_visited[current] = visitedTheories;
 106       d_engine->theoryOf(typeTheoryId)->preRegisterTerm(current);
 107       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 108     }
 109   }
 110   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 111
 112   Assert(d_visited.find(current) != d_visited.end());
 113   Assert(alreadyVisited(current, parent));
 114 }
 115
 116 void PreRegisterVisitor::start(TNode node) {
 117   d_multipleTheories = false;
 118 }
 119
 120 bool PreRegisterVisitor::done(TNode node) {
 121   // We have multiple theories if removing the node theory from others is non-empty
 122   return Theory::setRemove(Theory::theoryOf(node), d_theories);
 123 }
 124
 125 std::string SharedTermsVisitor::toString() const {
 126   std::stringstream ss;
 127   TNodeVisitedMap::const_iterator it = d_visited.begin();
 128   for (; it != d_visited.end(); ++ it) {
 129     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
 130   }
 131   return ss.str();
 132 }
 133
 134 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 135
 136   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 137
 138   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 139
 140   // If node is not visited at all, just return false
 141   if (find == d_visited.end()) {
 142     Debug("register::internal") << "1:false" << std::endl;
 143     return false;
 144   }
 145
 146   Theory::Set theories = (*find).second;
 147
 148   TheoryId currentTheoryId = Theory::theoryOf(current);
 149   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 150
 151   // Should we use the theory of the type
 152   bool useType = current != parent && currentTheoryId != parentTheoryId;
 153
 154   if (Theory::setContains(currentTheoryId, theories)) {
 155       if (Theory::setContains(parentTheoryId, theories)) {
 156         if (useType) {
 157           TheoryId typeTheoryId = Theory::theoryOf(current.getType());
 158           return Theory::setContains(typeTheoryId, theories);
 159         } else {
 160           return true;
 161         }
 162       } else {
 163         return false;
 164       }
 165   } else {
 166     return false;
 167   }
 168 }
 169
 170 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 171
 172   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
 173   if (Debug.isOn("register::internal")) {
 174     Debug("register::internal") << toString() << std::endl;
 175   }
 176
 177   // Get the theories of the terms
 178   TheoryId currentTheoryId = Theory::theoryOf(current);
 179   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 180
 181   bool useType = current != parent && currentTheoryId != parentTheoryId;
 182
 183   Theory::Set visitedTheories = d_visited[current];
 184   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 185   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 186     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 187     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 188   }
 189   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 190     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 191     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 192   }
 193   if (useType) {
 194     TheoryId typeTheoryId = Theory::theoryOf(current.getType());
 195     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 196       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 197       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
 198     }
 199   }
 200   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 201
 202   // Record the new theories that we visited
 203   d_visited[current] = visitedTheories;
 204
 205   // If there is more than two theories and a new one has been added notify the shared terms database
 206   if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
 207     d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
 208   }
 209
 210   Assert(d_visited.find(current) != d_visited.end());
 211   Assert(alreadyVisited(current, parent));
 212 }
 213
 214 void SharedTermsVisitor::start(TNode node) {
 215   clear();
 216   d_atom = node;
 217 }
 218
 219 void SharedTermsVisitor::done(TNode node) {
 220   clear();
 221 }
 222
 223 void SharedTermsVisitor::clear() {
 224   d_atom = TNode();
 225   d_visited.clear();
 226 }