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 << ") => ";
  34
  35   TNodeToTheorySetMap::iterator find = d_visited.find(current);
  36
  37   // If node is not visited at all, just return false
  38   if (find == d_visited.end()) {
  39     Debug("register::internal") << "1:false" << std::endl;
  40     return false;
  41   }
  42
  43   Theory::Set theories;
  44
  45   TheoryId currentTheoryId = Theory::theoryOf(current);
  46   TheoryId parentTheoryId  = Theory::theoryOf(parent);
  47
  48   // Remember the theories interested in this term
  49   d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
  50   // Check if there are multiple of those
  51   d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
  52
  53   theories = (*find).second;
  54   if (Theory::setContains(currentTheoryId, theories)) {
  55     // The current theory has already visited it, so now it depends on the parent
  56     Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl;
  57     return Theory::setContains(parentTheoryId, theories);
  58   } else {
  59     // If the current theory is not registered, it still needs to be visited
  60     Debug("register::internal") << "3:false" << std::endl;
  61     return false;
  62   }
  63 }
  64
  65 void PreRegisterVisitor::visit(TNode current, TNode parent) {
  66
  67   Theory::Set theories;
  68
  69   Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
  70   Debug("register::internal") << toString() << std::endl;
  71
  72   // Get the theories of the terms
  73   TheoryId currentTheoryId = Theory::theoryOf(current);
  74   TheoryId parentTheoryId  = Theory::theoryOf(parent);
  75
  76   // Remember the theories interested in this term
  77   d_theories[parent] = theories = Theory::setInsert(currentTheoryId, d_theories[parent]);
  78   // If there are theories other than the parent itself, we are in multi-theory case
  79   d_multipleTheories = d_multipleTheories || Theory::setRemove(parentTheoryId, theories);
  80
  81   theories = d_visited[current];
  82   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl;
  83   if (!Theory::setContains(currentTheoryId, theories)) {
  84     d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories);
  85     d_engine->theoryOf(currentTheoryId)->preRegisterTerm(current);
  86     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
  87   }
  88   if (!Theory::setContains(parentTheoryId, theories)) {
  89     d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories);
  90     d_engine->theoryOf(parentTheoryId)->preRegisterTerm(current);
  91     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
  92   }
  93   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl;
  94
  95   Assert(d_visited.find(current) != d_visited.end());
  96   Assert(alreadyVisited(current, parent));
  97 }
  98
  99 void PreRegisterVisitor::start(TNode node) {
 100   d_multipleTheories = false;
 101 }
 102
 103 bool PreRegisterVisitor::done(TNode node) {
 104   return d_multipleTheories;
 105 }
 106
 107 std::string SharedTermsVisitor::toString() const {
 108   std::stringstream ss;
 109   TNodeVisitedMap::const_iterator it = d_visited.begin();
 110   for (; it != d_visited.end(); ++ it) {
 111     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
 112   }
 113   return ss.str();
 114 }
 115
 116 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 117
 118   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ") => ";
 119
 120   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 121
 122   // If node is not visited at all, just return false
 123   if (find == d_visited.end()) {
 124     Debug("register::internal") << "1:false" << std::endl;
 125     return false;
 126   }
 127
 128   Theory::Set theories = (*find).second;
 129
 130   TheoryId currentTheoryId = Theory::theoryOf(current);
 131   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 132
 133   if (Theory::setContains(currentTheoryId, theories)) {
 134     // The current theory has already visited it, so now it depends on the parent
 135     Debug("register::internal") << (Theory::setContains(parentTheoryId, theories) ? "2:true" : "2:false") << std::endl;
 136     return Theory::setContains(parentTheoryId, theories);
 137   } else {
 138     // If the current theory is not registered, it still needs to be visited
 139     Debug("register::internal") << "2:false" << std::endl;
 140     return false;
 141   }
 142 }
 143
 144 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 145
 146   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
 147   Debug("register::internal") << toString() << std::endl;
 148
 149   // Get the theories of the terms
 150   TheoryId currentTheoryId = Theory::theoryOf(current);
 151   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 152
 153   Theory::Set theories = d_visited[current];
 154   unsigned theoriesCount = theories == 0 ? 0 : 1;
 155   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(theories) << std::endl;
 156   if (!Theory::setContains(currentTheoryId, theories)) {
 157     d_visited[current] = theories = Theory::setInsert(currentTheoryId, theories);
 158     theoriesCount ++;
 159     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 160   }
 161   if (!Theory::setContains(parentTheoryId, theories)) {
 162     d_visited[current] = theories = Theory::setInsert(parentTheoryId, theories);
 163     theoriesCount ++;
 164     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 165   }
 166   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(theories) << std::endl;
 167
 168   // If there is more than two theories and a new one has been added notify the shared terms database
 169   if (theoriesCount > 1) {
 170     d_sharedTerms.addSharedTerm(d_atom, current, theories);
 171   }
 172
 173   Assert(d_visited.find(current) != d_visited.end());
 174   Assert(alreadyVisited(current, parent));
 175 }
 176
 177 void SharedTermsVisitor::start(TNode node) {
 178   clear();
 179   d_atom = node;
 180 }
 181
 182 void SharedTermsVisitor::done(TNode node) {
 183   clear();
 184 }
 185
 186 void SharedTermsVisitor::clear() {
 187   d_atom = TNode();
 188   d_visited.clear();
 189 }