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

1 files changed, 12 insertions, 11 deletions

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 */