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