src/theory/term_registration_visitor.cpp

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