src/theory/term_registration_visitor.cpp

   1 /*********************                                                        */
   2 /*! \file term_registration_visitor.cpp
   3  ** \verbatim
   4  ** Original author: Dejan Jovanovic
   5  ** Major contributors: Andrew Reynolds
   6  ** Minor contributors (to current version): Tim King, Clark Barrett, Morgan Deters
   7  ** This file is part of the CVC4 project.
   8  ** Copyright (c) 2009-2014  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 = false;
  54   TheoryId typeTheoryId = THEORY_LAST;
  55
  56   if (current != parent) {
  57     if (currentTheoryId != parentTheoryId) {
  58       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
  59       TypeNode type = current.getType();
  60       useType = true;
  61       typeTheoryId = Theory::theoryOf(type);
  62     } else {
  63       TypeNode type = current.getType();
  64       typeTheoryId = Theory::theoryOf(type);
  65       if (typeTheoryId != currentTheoryId) {
  66         if (options::finiteModelFind() && type.isSort()) {
  67           // We're looking for finite models
  68           useType = true;
  69         } else {
  70           Cardinality card = type.getCardinality();
  71           if (card.isFinite()) {
  72             useType = true;
  73           }
  74         }
  75       }
  76     }
  77   }
  78
  79   // Get the theories that have already visited this node
  80   TNodeToTheorySetMap::iterator find = d_visited.find(current);
  81   if (find == d_visited.end()) {
  82     if (useType) {
  83       d_theories = Theory::setInsert(typeTheoryId, d_theories);
  84     }
  85     return false;
  86   }
  87
  88   Theory::Set visitedTheories = (*find).second;
  89   if (Theory::setContains(currentTheoryId, visitedTheories)) {
  90     // The current theory has already visited it, so now it depends on the parent and the type
  91     if (Theory::setContains(parentTheoryId, visitedTheories)) {
  92       if (useType) {
  93         TheoryId typeTheoryId = Theory::theoryOf(current.getType());
  94         d_theories = Theory::setInsert(typeTheoryId, d_theories);
  95         return Theory::setContains(typeTheoryId, visitedTheories);
  96       } else {
  97         return true;
  98       }
  99     } else {
 100       return false;
 101     }
 102   } else {
 103     return false;
 104   }
 105 }
 106
 107 void PreRegisterVisitor::visit(TNode current, TNode parent) {
 108
 109   Debug("register") << "PreRegisterVisitor::visit(" << current << "," << parent << ")" << std::endl;
 110   if (Debug.isOn("register::internal")) {
 111     Debug("register::internal") << toString() << std::endl;
 112   }
 113
 114   // Get the theories of the terms
 115   TheoryId currentTheoryId = Theory::theoryOf(current);
 116   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 117
 118   // Should we use the theory of the type
 119   bool useType = false;
 120   TheoryId typeTheoryId = THEORY_LAST;
 121
 122   if (current != parent) {
 123     if (currentTheoryId != parentTheoryId) {
 124       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 125       TypeNode type = current.getType();
 126       useType = true;
 127       typeTheoryId = Theory::theoryOf(type);
 128     } else {
 129       TypeNode type = current.getType();
 130       typeTheoryId = Theory::theoryOf(type);
 131       if (typeTheoryId != currentTheoryId) {
 132         if (options::finiteModelFind() && type.isSort()) {
 133           // We're looking for finite models
 134           useType = true;
 135         } else {
 136           Cardinality card = type.getCardinality();
 137           if (card.isFinite()) {
 138             useType = true;
 139           }
 140         }
 141       }
 142     }
 143   }
 144
 145   Theory::Set visitedTheories = d_visited[current];
 146   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 147   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 148     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 149     d_visited[current] = visitedTheories;
 150     Theory* th = d_engine->theoryOf(currentTheoryId);
 151     th->preRegisterTerm(current);
 152     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 153   }
 154   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 155     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 156     d_visited[current] = visitedTheories;
 157     Theory* th = d_engine->theoryOf(parentTheoryId);
 158     th->preRegisterTerm(current);
 159     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 160   }
 161   if (useType) {
 162     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 163       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 164       d_visited[current] = visitedTheories;
 165       Theory* th = d_engine->theoryOf(typeTheoryId);
 166       th->preRegisterTerm(current);
 167       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 168     }
 169   }
 170   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 171
 172   Assert(d_visited.find(current) != d_visited.end());
 173   Assert(alreadyVisited(current, parent));
 174 }
 175
 176 std::string SharedTermsVisitor::toString() const {
 177   std::stringstream ss;
 178   TNodeVisitedMap::const_iterator it = d_visited.begin();
 179   for (; it != d_visited.end(); ++ it) {
 180     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
 181   }
 182   return ss.str();
 183 }
 184
 185 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 186
 187   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 188
 189   if( ( parent.getKind() == kind::FORALL ||
 190         parent.getKind() == kind::EXISTS ||
 191         parent.getKind() == kind::REWRITE_RULE /*||
 192         parent.getKind() == kind::CARDINALITY_CONSTRAINT*/  ) &&
 193       current != parent ) {
 194     Debug("register::internal") << "quantifier:true" << std::endl;
 195     return true;
 196   }
 197   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 198
 199   // If node is not visited at all, just return false
 200   if (find == d_visited.end()) {
 201     Debug("register::internal") << "1:false" << std::endl;
 202     return false;
 203   }
 204
 205   Theory::Set theories = (*find).second;
 206
 207   TheoryId currentTheoryId = Theory::theoryOf(current);
 208   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 209
 210   // Should we use the theory of the type
 211   bool useType = false;
 212   TheoryId typeTheoryId = THEORY_LAST;
 213
 214   if (current != parent) {
 215     if (currentTheoryId != parentTheoryId) {
 216       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 217       TypeNode type = current.getType();
 218       useType = true;
 219       typeTheoryId = Theory::theoryOf(type);
 220     } else {
 221       TypeNode type = current.getType();
 222       typeTheoryId = Theory::theoryOf(type);
 223       if (typeTheoryId != currentTheoryId) {
 224         if (options::finiteModelFind() && type.isSort()) {
 225           // We're looking for finite models
 226           useType = true;
 227         } else {
 228           Cardinality card = type.getCardinality();
 229           if (card.isFinite()) {
 230             useType = true;
 231           }
 232         }
 233       }
 234     }
 235   }
 236   if (current != parent) {
 237     if (currentTheoryId != parentTheoryId) {
 238       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 239       TypeNode type = current.getType();
 240       useType = true;
 241       typeTheoryId = Theory::theoryOf(type);
 242     } else {
 243       TypeNode type = current.getType();
 244       typeTheoryId = Theory::theoryOf(type);
 245       if (typeTheoryId != currentTheoryId) {
 246         if (options::finiteModelFind() && type.isSort()) {
 247           // We're looking for finite models
 248           useType = true;
 249         } else {
 250           Cardinality card = type.getCardinality();
 251           if (card.isFinite()) {
 252             useType = true;
 253           }
 254         }
 255       }
 256     }
 257   }
 258
 259   if (Theory::setContains(currentTheoryId, theories)) {
 260       if (Theory::setContains(parentTheoryId, theories)) {
 261         if (useType) {
 262           return Theory::setContains(typeTheoryId, theories);
 263         } else {
 264           return true;
 265         }
 266       } else {
 267         return false;
 268       }
 269   } else {
 270     return false;
 271   }
 272 }
 273
 274 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 275
 276   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
 277   if (Debug.isOn("register::internal")) {
 278     Debug("register::internal") << toString() << std::endl;
 279   }
 280
 281   // Get the theories of the terms
 282   TheoryId currentTheoryId = Theory::theoryOf(current);
 283   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 284
 285   // Should we use the theory of the type
 286   bool useType = false;
 287   TheoryId typeTheoryId = THEORY_LAST;
 288
 289   if (current != parent) {
 290     if (currentTheoryId != parentTheoryId) {
 291       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 292       TypeNode type = current.getType();
 293       useType = true;
 294       typeTheoryId = Theory::theoryOf(type);
 295     } else {
 296       TypeNode type = current.getType();
 297       typeTheoryId = Theory::theoryOf(type);
 298       if (typeTheoryId != currentTheoryId) {
 299         if (options::finiteModelFind() && type.isSort()) {
 300           // We're looking for finite models
 301           useType = true;
 302         } else {
 303           Cardinality card = type.getCardinality();
 304           if (card.isFinite()) {
 305             useType = true;
 306           }
 307         }
 308       }
 309     }
 310   }
 311
 312   Theory::Set visitedTheories = d_visited[current];
 313   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 314   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 315     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 316     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 317   }
 318   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 319     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 320     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 321   }
 322   if (useType) {
 323     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 324       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 325       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
 326     }
 327   }
 328   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 329
 330   // Record the new theories that we visited
 331   d_visited[current] = visitedTheories;
 332
 333   // If there is more than two theories and a new one has been added notify the shared terms database
 334   if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
 335     d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
 336   }
 337
 338   Assert(d_visited.find(current) != d_visited.end());
 339   Assert(alreadyVisited(current, parent));
 340 }
 341
 342 void SharedTermsVisitor::start(TNode node) {
 343   clear();
 344   d_atom = node;
 345 }
 346
 347 void SharedTermsVisitor::done(TNode node) {
 348   clear();
 349 }
 350
 351 void SharedTermsVisitor::clear() {
 352   d_atom = TNode();
 353   d_visited.clear();
 354 }