Commit for the theory engine and rewriter changes. Changes are substantial and not yet finalized but I need to put it in to work further with the theory writers. Please check the files that you 'own'. Any comments or discussion is welcome. Further details will be coming in a follow up email later.

6 files changed, 98 insertions, 62 deletions

diff --git a/src/theory/builtin/Makefile.am b/src/theory/builtin/Makefile.am
index d1df0e425..9856cdbe6 100644
--- a/src/theory/builtin/Makefile.am
+++ b/src/theory/builtin/Makefile.am
@@ -7,6 +7,8 @@ noinst_LTLIBRARIES = libbuiltin.la
 
 libbuiltin_la_SOURCES = \
 	theory_builtin_type_rules.h \
+	theory_builtin_rewriter.h \
+	theory_builtin_rewriter.cpp \
 	theory_builtin.h \
 	theory_builtin.cpp
 
diff --git a/src/theory/builtin/kinds b/src/theory/builtin/kinds
index ad442fc2f..2831161c3 100644
--- a/src/theory/builtin/kinds
+++ b/src/theory/builtin/kinds
@@ -106,7 +106,14 @@
 # commands.
 #
 
-theory builtin ::CVC4::theory::builtin::TheoryBuiltin "theory_builtin.h"
+theory THEORY_BUILTIN ::CVC4::theory::builtin::TheoryBuiltin "theory/builtin/theory_builtin.h"
+
+properties stable-infinite  
+
+# Rewriter responisble for all the terms of the theory
+rewriter ::CVC4::theory::builtin::TheoryBuiltinRewriter "theory/builtin/theory_builtin_rewriter.h"
+
+sort BUILTIN_OPERATOR_TYPE "Built in type for built in operators"
 
 # A kind representing "inlined" operators defined with OPERATOR
 # Conceptually, (EQUAL a b) is actually an (APPLY EQUAL a b), but it's
@@ -130,7 +137,9 @@ operator TUPLE 2: "a tuple"
 constant TYPE_CONSTANT \
     ::CVC4::TypeConstant \
     ::CVC4::TypeConstantHashStrategy \
-    "expr/type_constant.h" \
+    "expr/kind.h" \
     "basic types"
 operator FUNCTION_TYPE 2: "function type"
 operator TUPLE_TYPE 2: "tuple type"
+
+endtheory
\ No newline at end of file
diff --git a/src/theory/builtin/theory_builtin.cpp b/src/theory/builtin/theory_builtin.cpp
index 810cd1d39..489c97e67 100644
--- a/src/theory/builtin/theory_builtin.cpp
+++ b/src/theory/builtin/theory_builtin.cpp
@@ -26,49 +26,6 @@ namespace CVC4 {
 namespace theory {
 namespace builtin {
 
-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
-    // AND is not required
-    Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ?
-                                               kind::IFF : kind::EQUAL,
-                                               in[0], in[1]);
-    Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
-    return neq;
-  }
-  // assume that in.getNumChildren() > 2 => diseqs.size() > 1
-  vector<Node> diseqs;
-  for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
-    TNode::iterator j = i;
-    while(++j != in.end()) {
-      Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ?
-                                                 kind::IFF : kind::EQUAL,
-                                                 *i, *j);
-      Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
-      diseqs.push_back(neq);
-    }
-  }
-  Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs);
-  return out;
-}
-
-RewriteResponse TheoryBuiltin::preRewrite(TNode in, bool topLevel) {
-  switch(in.getKind()) {
-  case kind::DISTINCT:
-    return RewriteComplete(blastDistinct(in));
-
-  case kind::EQUAL:
-    // EQUAL is a special case that should never end up here
-    Unreachable("TheoryBuiltin can't rewrite EQUAL !");
-
-  default:
-    return RewriteComplete(in);
-  }
-}
-
 Node TheoryBuiltin::getValue(TNode n, TheoryEngine* engine) {
   switch(n.getKind()) {
 
diff --git a/src/theory/builtin/theory_builtin.h b/src/theory/builtin/theory_builtin.h
index cce5ac6b8..baa1493b6 100644
--- a/src/theory/builtin/theory_builtin.h
+++ b/src/theory/builtin/theory_builtin.h
@@ -28,25 +28,10 @@ namespace theory {
 namespace builtin {
 
 class TheoryBuiltin : public Theory {
-  /** rewrite a DISTINCT expr */
-  static Node blastDistinct(TNode in);
-
 public:
-  TheoryBuiltin(int id, context::Context* c, OutputChannel& out) :
-    Theory(id, c, out) {
-  }
-
-  ~TheoryBuiltin() { }
-
-  void preRegisterTerm(TNode n) { Unreachable(); }
-  void registerTerm(TNode n) { Unreachable(); }
-  void check(Effort e) { Unreachable(); }
-  void propagate(Effort e) { Unreachable(); }
-  void explain(TNode n, Effort e) { Unreachable(); }
-  void presolve() { Unreachable(); }
+  TheoryBuiltin(context::Context* c, OutputChannel& out) :
+    Theory(THEORY_BUILTIN, c, out) {}
   Node getValue(TNode n, TheoryEngine* engine);
-  void shutdown() { }
-  RewriteResponse preRewrite(TNode n, bool topLevel);
   std::string identify() const { return std::string("TheoryBuiltin"); }
 };/* class TheoryBuiltin */
 
diff --git a/src/theory/builtin/theory_builtin_rewriter.cpp b/src/theory/builtin/theory_builtin_rewriter.cpp
new file mode 100644
index 000000000..05f7891d6
--- /dev/null
+++ b/src/theory/builtin/theory_builtin_rewriter.cpp
@@ -0,0 +1,35 @@
+#include "theory/builtin/theory_builtin_rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+Node TheoryBuiltinRewriter::blastDistinct(TNode in) {
+
+  Assert(in.getKind() == kind::DISTINCT);
+
+  if(in.getNumChildren() == 2) {
+    // if this is the case exactly 1 != pair will be generated so the
+    // AND is not required
+    Node eq = NodeManager::currentNM()->mkNode(in[0].getType().isBoolean() ? kind::IFF : kind::EQUAL, in[0], in[1]);
+    Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
+    return neq;
+  }
+
+  // assume that in.getNumChildren() > 2 => diseqs.size() > 1
+  vector<Node> diseqs;
+  for(TNode::iterator i = in.begin(); i != in.end(); ++i) {
+    TNode::iterator j = i;
+    while(++j != in.end()) {
+      Node eq = NodeManager::currentNM()->mkNode((*i).getType().isBoolean() ? kind::IFF : kind::EQUAL, *i, *j);
+      Node neq = NodeManager::currentNM()->mkNode(kind::NOT, eq);
+      diseqs.push_back(neq);
+    }
+  }
+  Node out = NodeManager::currentNM()->mkNode(kind::AND, diseqs);
+  return out;
+}
+
+}
+}
+}
diff --git a/src/theory/builtin/theory_builtin_rewriter.h b/src/theory/builtin/theory_builtin_rewriter.h
new file mode 100644
index 000000000..7da4289b1
--- /dev/null
+++ b/src/theory/builtin/theory_builtin_rewriter.h
@@ -0,0 +1,48 @@
+/*
+ * theory_builtin_rewriter.h
+ *
+ *  Created on: Dec 21, 2010
+ *      Author: dejan
+ */
+
+#pragma once
+
+#include "theory/rewriter.h"
+#include "theory/theory.h"
+
+namespace CVC4 {
+namespace theory {
+namespace builtin {
+
+class TheoryBuiltinRewriter {
+
+  static Node blastDistinct(TNode node);
+
+public:
+
+  static inline RewriteResponse postRewrite(TNode node) {
+    if (node.getKind() == kind::EQUAL) {
+      return Rewriter::callPostRewrite(Theory::theoryOf(node[0]), node);
+    }
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  static inline RewriteResponse preRewrite(TNode node) {
+    switch(node.getKind()) {
+    case kind::DISTINCT:
+      return RewriteResponse(REWRITE_DONE, blastDistinct(node));
+    case kind::EQUAL:
+      return Rewriter::callPreRewrite(Theory::theoryOf(node[0]), node);
+    default:
+      return RewriteResponse(REWRITE_DONE, node);
+    }
+  }
+
+  static inline void init() {}
+  static inline void shutdown() {}
+
+};
+
+}
+}
+}