With "-d extra-checking", rewrites are now checked (after

post-rewrite, another full rewrite is performed and the results
compared).

Also added another response code to rewriters.  Theories return a
CVC4::theory::RewriteResponse from preRewrite() and postRewrite().
This class has nice subclasses to make the theory rewriters somewhat
self-documenting in termination behavior.  They look like
tail-recursive rewriting calls, but they're not; they are
instantiations of the RewriteResponse result code, which carries the
Node being returned:

  // Flags the node as DONE pre- or post-rewriting, though this is
  // ignored if n belongs to another theory.
  //
  // NOTE this just changed name from RewritingComplete(), which
  // didn't match RewriteAgain().
  //
  return RewriteComplete(n);


  // Flags the node as needing another pre-rewrite (if returned from a
  // preRewrite()) or post-rewrite (if returned from a postRewrite()).
  //
  return RewriteAgain(n);


  // Flags the node as needing another FULL rewrite.  This is the same
  // as RewriteAgain() if returned from preRewrite().  If it's returned
  // from postRewrite(), however, this causes a full preRewrite() and
  // postRewrite() of the Node and all its children (though the cache is
  // still in effect, which might elide some rewriting calls).
  //
  // This would have been another fix for bug #168.  Its use should be
  // discouraged in practice, but there are places where it will
  // probably be necessary, where a theory rewrites a Node into
  // something in another theory about which it knows nothing.
  // A common case is where the returned Node is expressed as a
  // conjuction or disjunction of EQUALs, or a negation of EQUAL,
  // where the EQUAL is across terms in another theory, and that EQUAL
  // subterm should be seen by the owning theory.
  //
  return FullRewriteNeeded(n);

1 files changed, 46 insertions, 15 deletions

diff --git a/src/theory/theory.h b/src/theory/theory.h
index 8481aa5ff..ccc0a5f82 100644
--- a/src/theory/theory.h
+++ b/src/theory/theory.h
@@ -49,12 +49,13 @@ typedef expr::Attribute<PostRewriteCacheTag<false>, Node> PostRewriteCache;
 /**
  * Instances of this class serve as response codes from
  * Theory::preRewrite() and Theory::postRewrite().  Instances of
- * derived classes RewritingComplete(n) and RewriteAgain(n) should
- * be used for better self-documenting behavior.
+ * derived classes RewriteComplete(n), RewriteAgain(n), and
+ * FullRewriteNeeded(n) should be used, giving self-documenting
+ * rewrite behavior.
  */
 class RewriteResponse {
 protected:
-  enum Status { DONE, REWRITE };
+  enum Status { DONE, REWRITE, REWRITE_FULL };
 
   RewriteResponse(Status s, Node n) : d_status(s), d_node(n) {}
 
@@ -64,25 +65,55 @@ private:
 
 public:
   bool isDone() const { return d_status == DONE; }
-  bool needsMoreRewriting() const { return d_status == REWRITE; }
+  bool needsMoreRewriting() const { return d_status != DONE; }
+  bool needsFullRewriting() const { return d_status == REWRITE_FULL; }
   Node getNode() const { return d_node; }
-};
+};/* class RewriteResponse */
 
 /**
- * Return n, but request additional (pre,post)rewriting of it.
+ * Signal that (pre,post)rewriting of the Node is complete at n.  Note
+ * that if theory A returns this, and the Node is in another theory B,
+ * theory B will still be called on to pre- or postrewrite it.
+ */
+class RewriteComplete : public RewriteResponse {
+public:
+  RewriteComplete(Node n) : RewriteResponse(DONE, n) {}
+};/* class RewriteComplete */
+
+/**
+ * Return n, but request additional rewriting of it; if this is
+ * returned from preRewrite(), this re-preRewrite()'s the Node.  If
+ * this is returned from postRewrite(), this re-postRewrite()'s the
+ * Node, but does NOT re-preRewrite() it, nor does it rewrite the
+ * Node's children.
+ *
+ * Note that this is the behavior if a theory returns
+ * RewriteComplete() for a Node belonging to another theory.
  */
 class RewriteAgain : public RewriteResponse {
 public:
   RewriteAgain(Node n) : RewriteResponse(REWRITE, n) {}
-};
+};/* class RewriteAgain */
 
 /**
- * Signal that (pre,post)rewriting of the node is complete at n.
+ * Return n, but request an additional complete rewriting pass over
+ * it.  This has the same behavior as RewriteAgain() for
+ * pre-rewriting.  However, in post-rewriting, FullRewriteNeeded will
+ * _completely_ pre- and post-rewrite the term and the term's children
+ * (though it will use the cache to elide what calls it can).  Use
+ * with caution; it has bad effects on performance.  This might be
+ * useful if theory A rewrites a term into something quite different,
+ * and certain child nodes might belong to another theory whose normal
+ * form is unknown to theory A.  For example, if the builtin theory
+ * post-rewrites (DISTINCT a b c) into pairwise NOT EQUAL expressions,
+ * the theories owning a, b, and c might need to rewrite that EQUAL.
+ * (This came up, but the fix was to rewrite DISTINCT in
+ * pre-rewriting, obviating the problem.  See bug #168.)
  */
-class RewritingComplete : public RewriteResponse {
+class FullRewriteNeeded : public RewriteResponse {
 public:
-  RewritingComplete(Node n) : RewriteResponse(DONE, n) {}
-};
+  FullRewriteNeeded(Node n) : RewriteResponse(REWRITE_FULL, n) {}
+};/* class FullRewriteNeeded */
 
 /**
  * Base class for T-solvers.  Abstract DPLL(T).
@@ -266,26 +297,26 @@ public:
 
   /**
    * Pre-rewrite a term.  This default base-class implementation
-   * simply returns RewritingComplete(n).  A theory should never
+   * simply returns RewriteComplete(n).  A theory should never
    * rewrite a term to a strictly larger term that contains itself, as
    * this will cause a loop of hard Node links in the cache (and thus
    * memory leakage).
    */
   virtual RewriteResponse preRewrite(TNode n, bool topLevel) {
     Debug("theory-rewrite") << "no pre-rewriting to perform for " << n << std::endl;
-    return RewritingComplete(n);
+    return RewriteComplete(n);
   }
 
   /**
    * Post-rewrite a term.  This default base-class implementation
-   * simply returns RewritingComplete(n).  A theory should never
+   * simply returns RewriteComplete(n).  A theory should never
    * rewrite a term to a strictly larger term that contains itself, as
    * this will cause a loop of hard Node links in the cache (and thus
    * memory leakage).
    */
   virtual RewriteResponse postRewrite(TNode n, bool topLevel) {
     Debug("theory-rewrite") << "no post-rewriting to perform for " << n << std::endl;
-    return RewritingComplete(n);
+    return RewriteComplete(n);
   }
 
   /**