src/theory/rewriter.cpp

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