src/theory/rewriter.cpp

   1 /*********************                                                        */
   2 /*! \file rewriter.cpp
   3  ** \verbatim
   4  ** Top contributors (to current version):
   5  **   Dejan Jovanovic, Morgan Deters, Liana Hadarean
   6  ** This file is part of the CVC4 project.
   7  ** Copyright (c) 2009-2017 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  ** \brief [[ Add one-line brief description here ]]
  13  **
  14  ** [[ Add lengthier description here ]]
  15  ** \todo document this file
  16  **/
  17
  18 #include "theory/rewriter.h"
  19
  20 #include "theory/theory.h"
  21 #include "smt/smt_engine_scope.h"
  22 #include "smt/smt_statistics_registry.h"
  23 #include "theory/rewriter_tables.h"
  24 #include "util/resource_manager.h"
  25
  26 using namespace std;
  27
  28 namespace CVC4 {
  29 namespace theory {
  30
  31 unsigned long Rewriter::d_iterationCount = 0;
  32
  33 static TheoryId theoryOf(TNode node) {
  34   return Theory::theoryOf(THEORY_OF_TYPE_BASED, node);
  35 }
  36
  37 #ifdef CVC4_ASSERTIONS
  38 static CVC4_THREAD_LOCAL std::unordered_set<Node, NodeHashFunction>* s_rewriteStack = NULL;
  39 #endif /* CVC4_ASSERTIONS */
  40
  41 class RewriterInitializer {
  42   static RewriterInitializer s_rewriterInitializer;
  43   RewriterInitializer() {
  44     Rewriter::init();
  45   }
  46   ~RewriterInitializer() { Rewriter::shutdown(); }
  47 };/* class RewriterInitializer */
  48
  49 /**
  50  * This causes initialization of the rewriter before first use,
  51  * and tear-down at exit time.
  52  */
  53 RewriterInitializer RewriterInitializer::s_rewriterInitializer;
  54
  55 /**
  56  * TheoryEngine::rewrite() keeps a stack of things that are being pre-
  57  * and post-rewritten.  Each element of the stack is a
  58  * RewriteStackElement.
  59  */
  60 struct RewriteStackElement {
  61
  62   /** The node we're currently rewriting */
  63   Node node;
  64   /** Original node */
  65   Node original;
  66   /** Id of the theory that's currently rewriting this node */
  67   unsigned theoryId         : 8;
  68   /** Id of the original theory that started the rewrite */
  69   unsigned originalTheoryId : 8;
  70   /** Index of the child this node is done rewriting */
  71   unsigned nextChild        : 32;
  72   /** Builder for this node */
  73   NodeBuilder<> builder;
  74
  75   /**
  76    * Construct a fresh stack element.
  77    */
  78   RewriteStackElement(TNode node, TheoryId theoryId) :
  79     node(node),
  80     original(node),
  81     theoryId(theoryId),
  82     originalTheoryId(theoryId),
  83     nextChild(0) {
  84   }
  85 };
  86
  87 Node Rewriter::rewrite(TNode node) {
  88   return rewriteTo(theoryOf(node), node);
  89 }
  90
  91 Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
  92
  93 #ifdef CVC4_ASSERTIONS
  94   bool isEquality = node.getKind() == kind::EQUAL && (!node[0].getType().isBoolean());
  95
  96   if(s_rewriteStack == NULL) {
  97     s_rewriteStack = new std::unordered_set<Node, NodeHashFunction>();
  98   }
  99 #endif
 100
 101   Trace("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
 102
 103   // Check if it's been cached already
 104   Node cached = getPostRewriteCache(theoryId, node);
 105   if (!cached.isNull()) {
 106     return cached;
 107   }
 108
 109   // Put the node on the stack in order to start the "recursive" rewrite
 110   vector<RewriteStackElement> rewriteStack;
 111   rewriteStack.push_back(RewriteStackElement(node, theoryId));
 112
 113   ResourceManager* rm = NULL;
 114   bool hasSmtEngine = smt::smtEngineInScope();
 115   if (hasSmtEngine) {
 116     rm = NodeManager::currentResourceManager();
 117   }
 118   // Rewrite until the stack is empty
 119   for (;;){
 120
 121     if (hasSmtEngine &&
 122                 d_iterationCount % ResourceManager::getFrequencyCount() == 0) {
 123       rm->spendResource(options::rewriteStep());
 124       d_iterationCount = 0;
 125     }
 126
 127     // Get the top of the recursion stack
 128     RewriteStackElement& rewriteStackTop = rewriteStack.back();
 129
 130     Trace("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl;
 131
 132     // Before rewriting children we need to do a pre-rewrite of the node
 133     if (rewriteStackTop.nextChild == 0) {
 134
 135       // Check if the pre-rewrite has already been done (it's in the cache)
 136       Node cached = Rewriter::getPreRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
 137       if (cached.isNull()) {
 138         // Rewrite until fix-point is reached
 139         for(;;) {
 140           // Perform the pre-rewrite
 141           RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
 142           // Put the rewritten node to the top of the stack
 143           rewriteStackTop.node = response.node;
 144           TheoryId newTheory = theoryOf(rewriteStackTop.node);
 145           // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
 146           if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) {
 147             break;
 148           }
 149           rewriteStackTop.theoryId = newTheory;
 150         }
 151         // Cache the rewrite
 152         Rewriter::setPreRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
 153       }
 154       // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
 155       else {
 156         // Continue with the cached version
 157         rewriteStackTop.node = cached;
 158         rewriteStackTop.theoryId = theoryOf(cached);
 159       }
 160     }
 161
 162     rewriteStackTop.original =rewriteStackTop.node;
 163     // Now it's time to rewrite the children, check if this has already been done
 164     Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
 165     // If not, go through the children
 166     if(cached.isNull()) {
 167
 168       // The child we need to rewrite
 169       unsigned child = rewriteStackTop.nextChild++;
 170
 171       // To build the rewritten expression we set up the builder
 172       if(child == 0) {
 173         if (rewriteStackTop.node.getNumChildren() > 0) {
 174           // The children will add themselves to the builder once they're done
 175           rewriteStackTop.builder << rewriteStackTop.node.getKind();
 176           kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind();
 177           if (metaKind == kind::metakind::PARAMETERIZED) {
 178             rewriteStackTop.builder << rewriteStackTop.node.getOperator();
 179           }
 180         }
 181       }
 182
 183       // Process the next child
 184       if(child < rewriteStackTop.node.getNumChildren()) {
 185         // The child node
 186         Node childNode = rewriteStackTop.node[child];
 187         // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
 188         rewriteStack.push_back(RewriteStackElement(childNode, theoryOf(childNode)));
 189         // Go on with the rewriting
 190         continue;
 191       }
 192
 193       // Incorporate the children if necessary
 194       if (rewriteStackTop.node.getNumChildren() > 0) {
 195         Node rewritten = rewriteStackTop.builder;
 196         rewriteStackTop.node = rewritten;
 197         rewriteStackTop.theoryId = theoryOf(rewriteStackTop.node);
 198       }
 199
 200       // Done with all pre-rewriting, so let's do the post rewrite
 201       for(;;) {
 202         // Do the post-rewrite
 203         RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
 204         // We continue with the response we got
 205         TheoryId newTheoryId = theoryOf(response.node);
 206         if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) {
 207           // In the post rewrite if we've changed theories, we must do a full rewrite
 208           Assert(response.node != rewriteStackTop.node);
 209           //TODO: this is not thread-safe - should make this assertion dependent on sequential build
 210 #ifdef CVC4_ASSERTIONS
 211           Assert(s_rewriteStack->find(response.node) == s_rewriteStack->end());
 212           s_rewriteStack->insert(response.node);
 213 #endif
 214           Node rewritten = rewriteTo(newTheoryId, response.node);
 215           rewriteStackTop.node = rewritten;
 216 #ifdef CVC4_ASSERTIONS
 217           s_rewriteStack->erase(response.node);
 218 #endif
 219           break;
 220         } else if (response.status == REWRITE_DONE) {
 221 #ifdef CVC4_ASSERTIONS
 222           RewriteResponse r2 = Rewriter::callPostRewrite(newTheoryId, response.node);
 223           Assert(r2.node == response.node);
 224 #endif
 225           rewriteStackTop.node = response.node;
 226           break;
 227         }
 228         // Check for trivial rewrite loops of size 1 or 2
 229         Assert(response.node != rewriteStackTop.node);
 230         Assert(Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, response.node).node != rewriteStackTop.node);
 231         rewriteStackTop.node = response.node;
 232       }
 233       // We're done with the post rewrite, so we add to the cache
 234       Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
 235
 236     } else {
 237       // We were already in cache, so just remember it
 238       rewriteStackTop.node = cached;
 239       rewriteStackTop.theoryId = theoryOf(cached);
 240     }
 241
 242     // If this is the last node, just return
 243     if (rewriteStack.size() == 1) {
 244       Assert(!isEquality || rewriteStackTop.node.getKind() == kind::EQUAL || rewriteStackTop.node.isConst());
 245       return rewriteStackTop.node;
 246     }
 247
 248     // We're done with this node, append it to the parent
 249     rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node;
 250     rewriteStack.pop_back();
 251   }
 252
 253   Unreachable();
 254 }/* Rewriter::rewriteTo() */
 255
 256 void Rewriter::clearCaches() {
 257 #ifdef CVC4_ASSERTIONS
 258   if(s_rewriteStack != NULL) {
 259     delete s_rewriteStack;
 260     s_rewriteStack = NULL;
 261   }
 262 #endif
 263   Rewriter::clearCachesInternal();
 264 }
 265
 266 }/* CVC4::theory namespace */
 267 }/* CVC4 namespace */