From: Morgan Deters <mdeters@gmail.com>
Date: Sun, 4 Jul 2010 02:18:02 +0000 (+0000)
Subject: bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem... 
X-Git-Tag: cvc5-1.0.0~8956
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=994427c682dfe7323a0e806b18095b862508d454;p=cvc5.git

bug 168 fixed (TheoryEngine::rewrite is not fully rewriting to a fix point); problem had to do with the builtin theory post-rewriting DISTINCT into an arithmetic term not in normal form.  fix was to do DISTINCT rewriting in pre-rewrite.  note that this doesn't add to the amount of theory rewriting work that needs to be done, because everything is cached
---

diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 1951e438c..6cdcb4032 100644
--- 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 5c0a70dea..20b6b038b 100644
--- 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 */