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, 82 insertions, 0 deletions

diff --git a/src/util/output.h b/src/util/output.h
index 651f6b607..87b7f69a6 100644
--- a/src/util/output.h
+++ b/src/util/output.h
@@ -127,6 +127,41 @@ extern DebugC DebugOut CVC4_PUBLIC;
 #  define Debug if(0) debugNullCvc4Stream
 #endif /* CVC4_DEBUG */
 
+class CVC4_PUBLIC ScopedDebug {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedDebug(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ScopedDebug(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Debug.isOn(d_tag);
+    if(newSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+
+  ~ScopedDebug() {
+    if(d_oldSetting) {
+      Debug.on(d_tag);
+    } else {
+      Debug.off(d_tag);
+    }
+  }
+};/* class ScopedDebug */
+
 /** The warning output class */
 class CVC4_PUBLIC WarningC {
   std::ostream *d_os;
@@ -286,6 +321,41 @@ extern TraceC TraceOut CVC4_PUBLIC;
 #  define Trace if(0) debugNullCvc4Stream
 #endif /* CVC4_TRACING */
 
+class CVC4_PUBLIC ScopedTrace {
+  std::string d_tag;
+  bool d_oldSetting;
+
+public:
+
+  ScopedTrace(std::string tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Trace.isOn(d_tag);
+    if(newSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+
+  ScopedTrace(const char* tag, bool newSetting = true) :
+    d_tag(tag) {
+    d_oldSetting = Trace.isOn(d_tag);
+    if(newSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+
+  ~ScopedTrace() {
+    if(d_oldSetting) {
+      Trace.on(d_tag);
+    } else {
+      Trace.off(d_tag);
+    }
+  }
+};/* class ScopedTrace */
+
 #else /* ! CVC4_MUZZLE */
 
 #  define Debug if(0) debugNullCvc4Stream
@@ -295,6 +365,18 @@ extern TraceC TraceOut CVC4_PUBLIC;
 #  define Chat if(0) nullCvc4Stream
 #  define Trace if(0) debugNullCvc4Stream
 
+class CVC4_PUBLIC ScopedDebug {
+public:
+  ScopedDebug(std::string tag, bool newSetting = true) {}
+  ScopedDebug(const char* tag, bool newSetting = true) {}
+};/* class ScopedDebug */
+
+class CVC4_PUBLIC ScopedTrace {
+public:
+  ScopedTrace(std::string tag, bool newSetting = true) {}
+  ScopedTrace(const char* tag, bool newSetting = true) {}
+};/* class ScopedTrace */
+
 #endif /* ! CVC4_MUZZLE */
 
 /**