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