Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

1 files changed, 173 insertions, 0 deletions

diff --git a/src/theory/rewriter.cpp b/src/theory/rewriter.cpp
new file mode 100644
index 000000000..fe7ad7a9a
--- /dev/null
+++ b/src/theory/rewriter.cpp
@@ -0,0 +1,173 @@
+/*
+ * rewriter.cpp
+ *
+ *  Created on: Dec 13, 2010
+ *      Author: dejan
+ */
+
+#include "theory/theory.h"
+#include "theory/rewriter.h"
+#include "theory/rewriter_tables.h"
+
+namespace CVC4 {
+namespace theory {
+
+/**
+ * TheoryEngine::rewrite() keeps a stack of things that are being pre-
+ * and post-rewritten.  Each element of the stack is a
+ * RewriteStackElement.
+ */
+struct RewriteStackElement {
+
+  /** The node we're currently rewriting */
+  Node node;
+  /** Original node */
+  Node original;
+  /** Id of the theory that's currently rewriting this node */
+  unsigned theoryId         : 8;
+  /** Id of the original theory that started the rewrite */
+  unsigned originalTheoryId : 8;
+  /** Index of the child this node is done rewriting */
+  unsigned nextChild        : 32;
+  /** Builder for this node */
+  NodeBuilder<> builder;
+
+  /**
+   * Construct a fresh stack element.
+   */
+  RewriteStackElement(Node node, TheoryId theoryId) :
+    node(node),
+    original(node),
+    theoryId(theoryId),
+    originalTheoryId(theoryId),
+    nextChild(0) {
+  }
+};
+
+Node Rewriter::rewrite(Node node) {
+  return rewriteTo(theory::Theory::theoryOf(node), node);
+}
+
+Node Rewriter::rewriteTo(theory::TheoryId theoryId, Node node) {
+
+  Debug("rewriter") << "Rewriter::rewriteTo(" << theoryId << "," << node << ")"<< std::endl;
+
+  // Put the node on the stack in order to start the "recursive" rewrite
+  vector<RewriteStackElement> rewriteStack;
+  rewriteStack.push_back(RewriteStackElement(node, theoryId));
+
+  // Rewrite until the stack is empty
+  for (;;){
+
+    // Get the top of the recursion stack
+    RewriteStackElement& rewriteStackTop = rewriteStack.back();
+
+    Debug("rewriter") << "Rewriter::rewriting: " << (TheoryId) rewriteStackTop.theoryId << "," << rewriteStackTop.node << std::endl;
+
+    // Before rewriting children we need to do a pre-rewrite of the node
+    if (rewriteStackTop.nextChild == 0) {
+
+      // Check if the pre-rewrite has already been done (it's in the cache)
+      Node cached = Rewriter::getPreRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+      if (cached.isNull()) {
+        // Rewrite until fix-point is reached
+        for(;;) {
+          // Perform the pre-rewrite
+          RewriteResponse response = Rewriter::callPreRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+          // Put the rewritten node to the top of the stack
+          rewriteStackTop.node = response.node;
+          TheoryId newTheory = Theory::theoryOf(rewriteStackTop.node);
+          // In the pre-rewrite, if changing theories, we just call the other theories pre-rewrite
+          if (newTheory == (TheoryId) rewriteStackTop.theoryId && response.status == REWRITE_DONE) {
+            break;
+          }
+          rewriteStackTop.theoryId = newTheory;
+        }
+        // Cache the rewrite
+        Rewriter::setPreRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
+      }
+      // Otherwise we're have already been pre-rewritten (in pre-rewrite cache)
+      else {
+        // Continue with the cached version
+        rewriteStackTop.node = cached;
+        rewriteStackTop.theoryId = Theory::theoryOf(cached);
+      }
+    }
+
+    // Now it's time to rewrite the children, check if this has already been done
+    Node cached = Rewriter::getPostRewriteCache((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+    // If not, go through the children
+    if(cached.isNull()) {
+
+      // The child we need to rewrite
+      unsigned child = rewriteStackTop.nextChild++;
+
+      // To build the rewritten expression we set up the builder
+      if(child == 0) {
+        if (rewriteStackTop.node.getNumChildren() > 0) {
+          // The children will add themselves to the builder once they're done
+          rewriteStackTop.builder << rewriteStackTop.node.getKind();
+          kind::MetaKind metaKind = rewriteStackTop.node.getMetaKind();
+          if (metaKind == kind::metakind::PARAMETERIZED) {
+            rewriteStackTop.builder << rewriteStackTop.node.getOperator();
+          }
+        }
+      }
+
+      // Process the next child
+      if(child < rewriteStackTop.node.getNumChildren()) {
+        // The child node
+        Node childNode = rewriteStackTop.node[child];
+        // Push the rewrite request to the stack (NOTE: rewriteStackTop might be a bad reference now)
+        rewriteStack.push_back(RewriteStackElement(childNode, Theory::theoryOf(childNode)));
+        // Go on with the rewriting
+        continue;
+      }
+
+      // Incorporate the children if necessary
+      if (rewriteStackTop.node.getNumChildren() > 0) {
+        rewriteStackTop.node = rewriteStackTop.builder;
+        rewriteStackTop.theoryId = Theory::theoryOf(rewriteStackTop.node);
+      }
+
+      // Done with all pre-rewriting, so let's do the post rewrite
+      for(;;) {
+        // Do the post-rewrite
+        RewriteResponse response = Rewriter::callPostRewrite((TheoryId) rewriteStackTop.theoryId, rewriteStackTop.node);
+        // We continue with the response we got
+        rewriteStackTop.node = response.node;
+        TheoryId newTheoryId = Theory::theoryOf(rewriteStackTop.node);
+        if (newTheoryId != (TheoryId) rewriteStackTop.theoryId || response.status == REWRITE_AGAIN_FULL) {
+          // In the post rewrite if we've changed theories, we must do a full rewrite
+          rewriteStackTop.node = rewriteTo(newTheoryId, rewriteStackTop.node);
+          break;
+        } else if (response.status == REWRITE_DONE) {
+          break;
+        }
+      }
+      // We're done with the post rewrite, so we add to the cache
+      Rewriter::setPostRewriteCache((TheoryId) rewriteStackTop.originalTheoryId, rewriteStackTop.original, rewriteStackTop.node);
+
+    } else {
+      // We were already in cache, so just remember it
+      rewriteStackTop.node = cached;
+      rewriteStackTop.theoryId = Theory::theoryOf(cached);
+    }
+
+    // If this is the last node, just return
+    if (rewriteStack.size() == 1) {
+      return rewriteStackTop.node;
+    }
+
+    // We're done with this node, append it to the parent
+    rewriteStack[rewriteStack.size() - 2].builder << rewriteStackTop.node;
+    rewriteStack.pop_back();
+  }
+
+  Unreachable();
+  return Node::null();
+}
+
+
+}
+}