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