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-2013  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     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 106   }
 107   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 108     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 109     d_visited[current] = visitedTheories;
 110     Theory* th = d_engine->theoryOf(parentTheoryId);
 111     th->preRegisterTerm(current);
 112     Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 113   }
 114   if (useType) {
 115     TheoryId typeTheoryId  = Theory::theoryOf(current.getType());
 116     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 117       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 118       d_visited[current] = visitedTheories;
 119       Theory* th = d_engine->theoryOf(typeTheoryId);
 120       th->preRegisterTerm(current);
 121       Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 122     }
 123   }
 124   Debug("register::internal") << "PreRegisterVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 125
 126   Assert(d_visited.find(current) != d_visited.end());
 127   Assert(alreadyVisited(current, parent));
 128 }
 129
 130 std::string SharedTermsVisitor::toString() const {
 131   std::stringstream ss;
 132   TNodeVisitedMap::const_iterator it = d_visited.begin();
 133   for (; it != d_visited.end(); ++ it) {
 134     ss << (*it).first << ": " << Theory::setToString((*it).second) << std::endl;
 135   }
 136   return ss.str();
 137 }
 138
 139 bool SharedTermsVisitor::alreadyVisited(TNode current, TNode parent) const {
 140
 141   Debug("register::internal") << "SharedTermsVisitor::alreadyVisited(" << current << "," << parent << ")" << std::endl;
 142
 143   if( ( parent.getKind() == kind::FORALL ||
 144         parent.getKind() == kind::EXISTS ||
 145         parent.getKind() == kind::REWRITE_RULE /*||
 146         parent.getKind() == kind::CARDINALITY_CONSTRAINT*/  ) &&
 147       current != parent ) {
 148     Debug("register::internal") << "quantifier:true" << std::endl;
 149     return true;
 150   }
 151   TNodeVisitedMap::const_iterator find = d_visited.find(current);
 152
 153   // If node is not visited at all, just return false
 154   if (find == d_visited.end()) {
 155     Debug("register::internal") << "1:false" << std::endl;
 156     return false;
 157   }
 158
 159   Theory::Set theories = (*find).second;
 160
 161   TheoryId currentTheoryId = Theory::theoryOf(current);
 162   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 163
 164   // Should we use the theory of the type
 165   bool useType = false;
 166   TheoryId typeTheoryId = THEORY_LAST;
 167
 168   if (current != parent) {
 169     if (currentTheoryId != parentTheoryId) {
 170       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 171       TypeNode type = current.getType();
 172       useType = true;
 173       typeTheoryId = Theory::theoryOf(type);
 174     } else {
 175       TypeNode type = current.getType();
 176       typeTheoryId = Theory::theoryOf(type);
 177       if (typeTheoryId != currentTheoryId) {
 178         if (options::finiteModelFind() && type.isSort()) {
 179           // We're looking for finite models
 180           useType = true;
 181         } else {
 182           Cardinality card = type.getCardinality();
 183           if (card.isFinite()) {
 184             useType = true;
 185           }
 186         }
 187       }
 188     }
 189   }
 190
 191   if (Theory::setContains(currentTheoryId, theories)) {
 192       if (Theory::setContains(parentTheoryId, theories)) {
 193         if (useType) {
 194           return Theory::setContains(typeTheoryId, theories);
 195         } else {
 196           return true;
 197         }
 198       } else {
 199         return false;
 200       }
 201   } else {
 202     return false;
 203   }
 204 }
 205
 206 void SharedTermsVisitor::visit(TNode current, TNode parent) {
 207
 208   Debug("register") << "SharedTermsVisitor::visit(" << current << "," << parent << ")" << std::endl;
 209   if (Debug.isOn("register::internal")) {
 210     Debug("register::internal") << toString() << std::endl;
 211   }
 212
 213   // Get the theories of the terms
 214   TheoryId currentTheoryId = Theory::theoryOf(current);
 215   TheoryId parentTheoryId  = Theory::theoryOf(parent);
 216
 217   // Should we use the theory of the type
 218   bool useType = false;
 219   TheoryId typeTheoryId = THEORY_LAST;
 220
 221   if (current != parent) {
 222     if (currentTheoryId != parentTheoryId) {
 223       // If enclosed by different theories it's shared -- in read(a, f(a)) f(a) should be shared with integers
 224       TypeNode type = current.getType();
 225       useType = true;
 226       typeTheoryId = Theory::theoryOf(type);
 227     } else {
 228       TypeNode type = current.getType();
 229       typeTheoryId = Theory::theoryOf(type);
 230       if (typeTheoryId != currentTheoryId) {
 231         if (options::finiteModelFind() && type.isSort()) {
 232           // We're looking for finite models
 233           useType = true;
 234         } else {
 235           Cardinality card = type.getCardinality();
 236           if (card.isFinite()) {
 237             useType = true;
 238           }
 239         }
 240       }
 241     }
 242   }
 243
 244   Theory::Set visitedTheories = d_visited[current];
 245   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): previously registered with " << Theory::setToString(visitedTheories) << std::endl;
 246   if (!Theory::setContains(currentTheoryId, visitedTheories)) {
 247     visitedTheories = Theory::setInsert(currentTheoryId, visitedTheories);
 248     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << currentTheoryId << std::endl;
 249   }
 250   if (!Theory::setContains(parentTheoryId, visitedTheories)) {
 251     visitedTheories = Theory::setInsert(parentTheoryId, visitedTheories);
 252     Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << parentTheoryId << std::endl;
 253   }
 254   if (useType) {
 255     if (!Theory::setContains(typeTheoryId, visitedTheories)) {
 256       visitedTheories = Theory::setInsert(typeTheoryId, visitedTheories);
 257       Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): adding " << typeTheoryId << std::endl;
 258     }
 259   }
 260   Debug("register::internal") << "SharedTermsVisitor::visit(" << current << "," << parent << "): now registered with " << Theory::setToString(visitedTheories) << std::endl;
 261
 262   // Record the new theories that we visited
 263   d_visited[current] = visitedTheories;
 264
 265   // If there is more than two theories and a new one has been added notify the shared terms database
 266   if (Theory::setDifference(visitedTheories, Theory::setInsert(currentTheoryId))) {
 267     d_sharedTerms.addSharedTerm(d_atom, current, visitedTheories);
 268   }
 269
 270   Assert(d_visited.find(current) != d_visited.end());
 271   Assert(alreadyVisited(current, parent));
 272 }
 273
 274 void SharedTermsVisitor::start(TNode node) {
 275   clear();
 276   d_atom = node;
 277 }
 278
 279 void SharedTermsVisitor::done(TNode node) {
 280   clear();
 281 }
 282
 283 void SharedTermsVisitor::clear() {
 284   d_atom = TNode();
 285   d_visited.clear();
 286 }