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