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