src/theory/term_registration_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file term_registration_visitor.cpp
   3  ** \verbatim
   4  ** Original author: dejan
   5  ** Major contributors: mdeters
   6  ** Minor contributors (to current version): taking, barrett
   7  ** This file is part of the CVC4 prototype.
   8  ** Copyright (c) 2009-2012  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  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "theory/term_registration_visitor.h"
  19 #include "theory/theory_engine.h"
  20 #include "theory/quantifiers/options.h"
  21
  22 using namespace std;
  23 using namespace CVC4;
  24 using namespace theory;
  25
  26 std::string PreRegisterVisitor::toString() const {
  27   std::stringstream ss;
  28   TNodeToTheorySetMap::const_iterator it = d_visited.begin();
  29   for (; it != d_visited.end(); ++ it) {
  30     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
  31   }
  32   return ss.str();
  33 }
  34
  35 bool PreRegisterVisitor::alreadyVisited(TNode current, TNode parent) {
  36
  37   Debug("register::internal") << "PreRegisterVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
  38
  39   if( ( parent.getKind() == kind::FORALL ||
  40         parent.getKind() == kind::EXISTS ||
  41         parent.getKind() == kind::REWRITE_RULE /*||
  42         parent.getKind() == kind::CARDINALITY_CONSTRAINT*/ ) &&
  43       current != parent ) {
  44     Debug("register::internal") << "quantifier:true" << std::endl;
  45     return true;
  46   }
  47
  48   TheoryId currentTheoryId = Theory::theoryOf(current);
  49   TheoryId parentTheoryId = Theory::theoryOf(parent);
  50
  51   d_theories = Theory::setInsert(currentTheoryId, d_theories);
  52   d_theories = Theory::setInsert(parentTheoryId, d_theories);
  53
  54   // Should we use the theory of the type
  55   bool useType = current != parent && currentTheoryId != parentTheoryId;
  56
  57   // Get the theories that have already visited this node
  58   TNodeToTheorySetMap::iterator find = d_visited.find(current);
  59   if (find == d_visited.end()) {
  60     if (useType) {
  61       TheoryId typeTheoryId = Theory::theoryOf(current.getType());
  62       d_theories = Theory::setInsert(typeTheoryId, d_theories);
  63     }
  64     return false;
  65   }
  66
  67   Theory::Set visitedTheories = (*find).second;
  68   if (Theory::setContains(currentTheoryId, visitedTheories)) {
  69     // The current theory has already visited it, so now it depends on the parent and the type
  70     if (Theory::setContains(parentTheoryId, visitedTheories)) {
  71       if (useType) {
  72         TheoryId typeTheoryId = Theory::theoryOf(current.getType());
  73         d_theories = Theory::setInsert(typeTheoryId, d_theories);
  74         return Theory::setContains(typeTheoryId, visitedTheories);
  75       } else {
  76         return true;
  77       }
  78     } else {
  79       return false;
  80     }
  81   } else {
  82     return false;
  83   }
  84 }
  85
  86 void PreRegisterVisitor::visit(TNode current, TNode parent) {
  87
  88   Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
  89   if (Debug.isOn("register::internal")) {
  90     Debug("register::internal") << toString() << std::endl;
  91   }
  92
  93   // Get the theories of the terms
  94   TheoryId currentTheoryId = Theory::theoryOf(current);
  95   TheoryId parentTheoryId  = Theory::theoryOf(parent);
  96
  97   // Should we use the theory of the type
  98   bool useType = current != parent && currentTheoryId != parentTheoryId;
  99
 100   Theory::Set visitedTheories = d_visited[current];
 101   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 102   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 103     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 104     d_visited[current] = visitedTheories;
 105     Theory* th = d_engine->theoryOf(currentTheoryId);
 106     th->preRegisterTerm(current);
 107     if(th->getInstantiator() != NULL) {
 108       th->getInstantiator()->preRegisterTerm(current);
 109     }
 110     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 111   }
 112   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 113     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 114     d_visited[current] = visitedTheories;
 115     Theory* th = d_engine->theoryOf(parentTheoryId);
 116     th->preRegisterTerm(current);
 117     if(th->getInstantiator() != NULL) {
 118       th->getInstantiator()->preRegisterTerm(current);
 119     }
 120     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 121   }
 122   if (useType) {
 123     TheoryId typeTheoryId  = Theory::theoryOf(current.getType());
 124     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 125       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 126       d_visited[current] = visitedTheories;
 127       Theory* th = d_engine->theoryOf(typeTheoryId);
 128       th->preRegisterTerm(current);
 129       if(th->getInstantiator() != NULL) {
 130         th->getInstantiator()->preRegisterTerm(current);
 131       }
 132       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 133     }
 134   }
 135   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 136
 137   Assert(d_visited.find(current) != d_visited.end());
 138   Assert(alreadyVisited(current, parent));
 139 }
 140
 141 void PreRegisterVisitor::start(TNode node) {
 142   d_multipleTheories = false;
 143 }
 144
 145 bool PreRegisterVisitor::done(TNode node) {
 146   // We have multiple theories if removing the node theory from others is non-empty
 147   return Theory::setRemove(Theory::theoryOf(node), d_theories);
 148 }
 149
 150 std::string SharedTermsVisitor::toString() const {
 151   std::stringstream ss;
 152   TNodeVisitedMap::const_iterator it = d_visited.begin();
 153   for (; it != d_visited.end(); ++ it) {
 154     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
 155   }
 156   return ss.str();
 157 }
 158
 159 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 160
 161   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 162
 163   if( ( parent.getKind() == kind::FORALL ||
 164         parent.getKind() == kind::EXISTS ||
 165         parent.getKind() == kind::REWRITE_RULE /*||
 166         parent.getKind() == kind::CARDINALITY_CONSTRAINT*/  ) &&
 167       current != parent ) {
 168     Debug("register::internal") << "quantifier:true" << std::endl;
 169     return true;
 170   }
 171   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 172
 173   // If node is not visited at all, just return false
 174   if (find == d_visited.end()) {
 175     Debug("register::internal") << "1:false" << std::endl;
 176     return false;
 177   }
 178
 179   Theory::Set theories = (*find).second;
 180
 181   TheoryId currentTheoryId = Theory::theoryOf(current);
 182   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 183
 184   // Should we use the theory of the type
 185 #if 0
 186   bool useType = current != parent && currentTheoryId != parentTheoryId;
 187 #else
 188   bool useType = false;
 189   TheoryId typeTheoryId = THEORY_LAST;
 190
 191   if (current != parent) {
 192     if (currentTheoryId != parentTheoryId) {
 193       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 194       TypeNode type = current.getType();
 195       useType = true;
 196       typeTheoryId = Theory::theoryOf(type);
 197     } else {
 198       TypeNode type = current.getType();
 199       typeTheoryId = Theory::theoryOf(type);
 200       if (typeTheoryId != currentTheoryId) {
 201         if (options::finiteModelFind() && type.isSort()) {
 202           // We're looking for finite models
 203           useType = true;
 204         } else {
 205           Cardinality card = type.getCardinality();
 206           if (card.isFinite()) {
 207             useType = true;
 208           }
 209         }
 210       }
 211     }
 212   }
 213 #endif
 214
 215   if (Theory::setContains(currentTheoryId, theories)) {
 216       if (Theory::setContains(parentTheoryId, theories)) {
 217         if (useType) {
 218           ////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
 219           return Theory::setContains(typeTheoryId, theories);
 220         } else {
 221           return true;
 222         }
 223       } else {
 224         return false;
 225       }
 226   } else {
 227     return false;
 228   }
 229 }
 230
 231 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 232
 233   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
 234   if (Debug.isOn("register::internal")) {
 235     Debug("register::internal") << toString() << std::endl;
 236   }
 237
 238   // Get the theories of the terms
 239   TheoryId currentTheoryId = Theory::theoryOf(current);
 240   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 241
 242 #if 0
 243   bool useType = current != parent && currentTheoryId != parentTheoryId;
 244 #else
 245   // Should we use the theory of the type
 246   bool useType = false;
 247   TheoryId typeTheoryId = THEORY_LAST;
 248
 249   if (current != parent) {
 250     if (currentTheoryId != parentTheoryId) {
 251       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 252       TypeNode type = current.getType();
 253       useType = true;
 254       typeTheoryId = Theory::theoryOf(type);
 255     } else {
 256       TypeNode type = current.getType();
 257       typeTheoryId = Theory::theoryOf(type);
 258       if (typeTheoryId != currentTheoryId) {
 259         if (options::finiteModelFind() && type.isSort()) {
 260           // We're looking for finite models
 261           useType = true;
 262         } else {
 263           Cardinality card = type.getCardinality();
 264           if (card.isFinite()) {
 265             useType = true;
 266           }
 267         }
 268       }
 269     }
 270   }
 271 #endif
 272
 273   Theory::Set visitedTheories = d_visited[current];
 274   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 275   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 276     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 277     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 278   }
 279   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 280     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 281     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 282   }
 283   if (useType) {
 284     //////TheoryId typeTheoryId = Theory::theoryOf(current.getType());
 285     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 286       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 287       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
 288     }
 289   }
 290   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 291
 292   // Record the new theories that we visited
 293   d_visited[current] = visitedTheories;
 294
 295   // If there is more than two theories and a new one has been added notify the shared terms database
 296   if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
 297     d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
 298   }
 299
 300   Assert(d_visited.find(current) != d_visited.end());
 301   Assert(alreadyVisited(current, parent));
 302 }
 303
 304 void SharedTermsVisitor::start(TNode node) {
 305   clear();
 306   d_atom = node;
 307 }
 308
 309 void SharedTermsVisitor::done(TNode node) {
 310   clear();
 311 }
 312
 313 void SharedTermsVisitor::clear() {
 314   d_atom = TNode();
 315   d_visited.clear();
 316 }