src/theory/term_registration_visitor.cpp

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