bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem...

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1951e438c7a080e7f97537819ee294a940ce1b1e..6cdcb40326e05354739d583a5b654aa23ef483fe 100644 (file)
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -27,8 +27,8 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-Node blastDistinct(TNode in) {
-  Debug("theory-rewrite") << "blastDistinct: " << in << std::endl;
+Node TheoryBuiltin::blastDistinct(TNode in) {
+  Debug("theory-rewrite") << "TheoryBuiltin::blastDistinct: " << in << std::endl;
   Assert(in.getKind() == kind::DISTINCT);
   if(in.getNumChildren() == 2) {
     // if this is the case exactly 1 != pair will be generated so the
@@ -51,17 +51,18 @@ Node blastDistinct(TNode in) {
   return out;
 }
 
-RewriteResponse TheoryBuiltin::postRewrite(TNode in, bool topLevel) {
-  if(topLevel) {
-    if(in.getKind() == kind::DISTINCT) {
-      return RewritingComplete(blastDistinct(in));
-    }
-  }
+RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) {
+  switch(in.getKind()) {
+  case kind::DISTINCT:
+    return RewritingComplete(blastDistinct(in));
 
-  // EQUAL is a special case that should never end up here
-  Assert(in.getKind() != kind::EQUAL);
+  case kind::EQUAL:
+    // EQUAL is a special case that should never end up here
+    Unreachable("TheoryBuiltin can't rewrite EQUAL !");
 
-  return RewritingComplete(in);
+  default:
+    return RewritingComplete(in);
+  }
 }
 
 }/* CVC4::theory::builtin namespace */

diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index 5c0a70dea5dc881fc8b65a8018a5b2db65a6abec..20b6b038b44159c4b151f5559bbabed004a1428c 100644 (file)
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -28,6 +28,9 @@ namespace theory {
 namespace builtin {
 
 class TheoryBuiltin : public Theory {
+  /** rewrite a DISTINCT expr */
+  static Node blastDistinct(TNode in);
+
 public:
   TheoryBuiltin(context::Context* c, OutputChannel& out) : Theory(c, out) { }
   ~TheoryBuiltin() { }
@@ -37,7 +40,7 @@ public:
   void propagate(Effort e) { Unreachable(); }
   void explain(TNode n, Effort e) { Unreachable(); }
   void shutdown() { }
-  RewriteResponse postRewrite(TNode n, bool topLevel);
+  RewriteResponse preRewrite(TNode n, bool topLevel);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */