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.

8 files changed, 130 insertions, 122 deletions

diff --git a/src/theory/uf/Makefile.am b/src/theory/uf/Makefile.am
index 04fe533ae..e4647b442 100644
--- a/src/theory/uf/Makefile.am
+++ b/src/theory/uf/Makefile.am
@@ -11,7 +11,8 @@ nodist_EXTRA_libuf_la_SOURCES = \
 
 libuf_la_SOURCES = \
 	theory_uf.h \
-	theory_uf_type_rules.h 
+	theory_uf_type_rules.h \
+	theory_uf_rewriter.h
 
 libuf_la_LIBADD = \
 	@builddir@/tim/libuftim.la \
diff --git a/src/theory/uf/kinds b/src/theory/uf/kinds
index 8cd6aec70..a1fcac1df 100644
--- a/src/theory/uf/kinds
+++ b/src/theory/uf/kinds
@@ -4,9 +4,17 @@
 # src/theory/builtin/kinds.
 #
 
-theory ::CVC4::theory::uf::TheoryUF "theory_uf.h"
+theory THEORY_UF ::CVC4::theory::uf::TheoryUF "theory/uf/theory_uf.h"
+
+properties stable-infinite check propagate staticLearning presolve 
+
+rewriter ::CVC4::theory::uf::TheoryUfRewriter "theory/uf/theory_uf_rewriter.h"
+
+sort KIND_TYPE "Uninterpreted Sort"  
 
 parameterized APPLY_UF VARIABLE 1: "uninterpreted function application"
 
 variable SORT_TAG "sort tag"
 parameterized SORT_TYPE SORT_TAG 0: "sort type"
+
+endtheory
\ No newline at end of file
diff --git a/src/theory/uf/morgan/theory_uf_morgan.cpp b/src/theory/uf/morgan/theory_uf_morgan.cpp
index cd9ee79c3..33c8bc7b6 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.cpp
+++ b/src/theory/uf/morgan/theory_uf_morgan.cpp
@@ -31,8 +31,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 using namespace CVC4::theory::uf::morgan;
 
-TheoryUFMorgan::TheoryUFMorgan(int id, Context* ctxt, OutputChannel& out) :
-  TheoryUF(id, ctxt, out),
+TheoryUFMorgan::TheoryUFMorgan(Context* ctxt, OutputChannel& out) :
+  TheoryUF(ctxt, out),
   d_assertions(ctxt),
   d_ccChannel(this),
   d_cc(ctxt, &d_ccChannel),
@@ -70,23 +70,6 @@ TheoryUFMorgan::~TheoryUFMorgan() {
   StatisticsRegistry::unregisterStat(&d_ccNewSkolemVars);
 }
 
-RewriteResponse TheoryUFMorgan::postRewrite(TNode n, bool topLevel) {
-  if(topLevel) {
-    Debug("uf") << "uf: begin rewrite(" << n << ")" << endl;
-    Node ret(n);
-    if(n.getKind() == kind::EQUAL ||
-       n.getKind() == kind::IFF) {
-      if(n[0] == n[1]) {
-        ret = NodeManager::currentNM()->mkConst(true);
-      }
-    }
-    Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << endl;
-    return RewriteComplete(ret);
-  } else {
-    return RewriteComplete(n);
-  }
-}
-
 void TheoryUFMorgan::preRegisterTerm(TNode n) {
   Debug("uf") << "uf: preRegisterTerm(" << n << ")" << endl;
   if(n.getKind() == kind::EQUAL || n.getKind() == kind::IFF) {
@@ -258,63 +241,63 @@ void TheoryUFMorgan::merge(TNode a, TNode b) {
   // disequal to, and the attendant disequality
 
   // FIXME these could be "remembered" and then done in propagation (?)
-  EqLists::iterator eq_i = d_equalities.find(a);
-  if(eq_i != d_equalities.end()) {
-    EqList* eq = (*eq_i).second;
-    if(Debug.isOn("uf")) {
-      Debug("uf") << "a == " << a << endl;
-      Debug("uf") << "size of eq(a) is " << eq->size() << endl;
-    }
-    for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) {
-      Debug("uf") << "  eq(a) ==> " << *j << endl;
-      TNode eqn = *j;
-      Assert(eqn.getKind() == kind::EQUAL ||
-             eqn.getKind() == kind::IFF);
-      TNode s = eqn[0];
-      TNode t = eqn[1];
-      if(Debug.isOn("uf")) {
-        Debug("uf") << "       s  ==> " << s << endl
-                    << "       t  ==> " << t << endl
-                    << "  find(s) ==> " << debugFind(s) << endl
-                    << "  find(t) ==> " << debugFind(t) << endl;
-      }
-      TNode sp = find(s);
-      TNode tp = find(t);
-      if(sp == tp) {
-        // propagation of equality
-        Debug("uf:prop") << "  uf-propagating " << eqn << endl;
-        ++d_propagations;
-        d_out->propagate(eqn);
-      } else {
-        Assert(sp == b || tp == b);
-        appendToEqList(b, eqn);
-        if(sp == b) {
-          map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp);
-          if(k != alreadyDiseqs.end()) {
-            // propagation of disequality
-            // FIXME: this will propagate the same disequality on every
-            // subsequent merge, won't it??
-            Node deqn = (*k).second.notNode();
-            Debug("uf:prop") << "  uf-propagating " << deqn << endl;
-            ++d_propagations;
-            d_out->propagate(deqn);
-          }
-        } else {
-          map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp);
-          if(k != alreadyDiseqs.end()) {
-            // propagation of disequality
-            // FIXME: this will propagate the same disequality on every
-            // subsequent merge, won't it??
-            Node deqn = (*k).second.notNode();
-            Debug("uf:prop") << "  uf-propagating " << deqn << endl;
-            ++d_propagations;
-            d_out->propagate(deqn);
-          }
-        }
-      }
-    }
-    Debug("uf") << "end eq-list." << endl;
-  }
+//  EqLists::iterator eq_i = d_equalities.find(a);
+//  if(eq_i != d_equalities.end()) {
+//    EqList* eq = (*eq_i).second;
+//    if(Debug.isOn("uf")) {
+//      Debug("uf") << "a == " << a << endl;
+//      Debug("uf") << "size of eq(a) is " << eq->size() << endl;
+//    }
+//    for(EqList::const_iterator j = eq->begin(); j != eq->end(); ++j) {
+//      Debug("uf") << "  eq(a) ==> " << *j << endl;
+//      TNode eqn = *j;
+//      Assert(eqn.getKind() == kind::EQUAL ||
+//             eqn.getKind() == kind::IFF);
+//      TNode s = eqn[0];
+//      TNode t = eqn[1];
+//      if(Debug.isOn("uf")) {
+//        Debug("uf") << "       s  ==> " << s << endl
+//                    << "       t  ==> " << t << endl
+//                    << "  find(s) ==> " << debugFind(s) << endl
+//                    << "  find(t) ==> " << debugFind(t) << endl;
+//      }
+//      TNode sp = find(s);
+//      TNode tp = find(t);
+//      if(sp == tp) {
+//        // propagation of equality
+//        Debug("uf:prop") << "  uf-propagating " << eqn << endl;
+//        ++d_propagations;
+//        d_out->propagate(eqn);
+//      } else {
+//        Assert(sp == b || tp == b);
+//        appendToEqList(b, eqn);
+//        if(sp == b) {
+//          map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(tp);
+//          if(k != alreadyDiseqs.end()) {
+//            // propagation of disequality
+//            // FIXME: this will propagate the same disequality on every
+//            // subsequent merge, won't it??
+//            Node deqn = (*k).second.notNode();
+//            Debug("uf:prop") << "  uf-propagating " << deqn << endl;
+//            ++d_propagations;
+//            d_out->propagate(deqn);
+//          }
+//        } else {
+//          map<TNode, TNode>::const_iterator k = alreadyDiseqs.find(sp);
+//          if(k != alreadyDiseqs.end()) {
+//            // propagation of disequality
+//            // FIXME: this will propagate the same disequality on every
+//            // subsequent merge, won't it??
+//            Node deqn = (*k).second.notNode();
+//            Debug("uf:prop") << "  uf-propagating " << deqn << endl;
+//            ++d_propagations;
+//            d_out->propagate(deqn);
+//          }
+//        }
+//      }
+//    }
+//    Debug("uf") << "end eq-list." << endl;
+//  }
 }
 
 void TheoryUFMorgan::appendToDiseqList(TNode of, TNode eq) {
@@ -564,12 +547,12 @@ void TheoryUFMorgan::propagate(Effort level) {
   Debug("uf") << "uf: end propagate(" << level << ")" << endl;
 }
 
-void TheoryUFMorgan::explain(TNode n, Effort level) {
+void TheoryUFMorgan::explain(TNode n) {
   TimerStat::CodeTimer codeTimer(d_explainTimer);
 
-  Debug("uf") << "uf: begin explain([" << n << "], " << level << ")" << endl;
+  Debug("uf") << "uf: begin explain([" << n << "])" << endl;
   Unimplemented();
-  Debug("uf") << "uf: end explain([" << n << "], " << level << ")" << endl;
+  Debug("uf") << "uf: end explain([" << n << "])" << endl;
 }
 
 void TheoryUFMorgan::presolve() {
diff --git a/src/theory/uf/morgan/theory_uf_morgan.h b/src/theory/uf/morgan/theory_uf_morgan.h
index cbc5f1eab..2a079603b 100644
--- a/src/theory/uf/morgan/theory_uf_morgan.h
+++ b/src/theory/uf/morgan/theory_uf_morgan.h
@@ -132,7 +132,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUFMorgan(int id, context::Context* ctxt, OutputChannel& out);
+  TheoryUFMorgan(context::Context* ctxt, OutputChannel& out);
 
   /** Destructor for UF theory, cleans up memory and statistics. */
   ~TheoryUFMorgan();
@@ -170,13 +170,6 @@ public:
   void check(Effort level);
 
   /**
-   * Rewrites a node in the theory of uninterpreted functions.
-   * This is fairly basic and only ensures that atoms that are
-   * unsatisfiable or a valid are rewritten to false or true respectively.
-   */
-  RewriteResponse postRewrite(TNode n, bool topLevel);
-
-  /**
    * Propagates theory literals.
    *
    * Overloads void propagate(Effort level); from theory.h.
@@ -190,7 +183,7 @@ public:
    * Overloads void explain(TNode n, Effort level); from theory.h.
    * See theory/theory.h for more information about this method.
    */
-  void explain(TNode n, Effort level);
+  void explain(TNode n);
 
   /**
    * The theory should only add (via .operator<< or .append()) to the
diff --git a/src/theory/uf/theory_uf.h b/src/theory/uf/theory_uf.h
index f745cf402..be3d7ac69 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -37,8 +37,8 @@ class TheoryUF : public Theory {
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUF(int id, context::Context* ctxt, OutputChannel& out)
-    : Theory(id, ctxt, out) {}
+  TheoryUF(context::Context* ctxt, OutputChannel& out)
+    : Theory(THEORY_UF, ctxt, out) {}
 
 };/* class TheoryUF */
 
diff --git a/src/theory/uf/theory_uf_rewriter.h b/src/theory/uf/theory_uf_rewriter.h
new file mode 100644
index 000000000..e71f74fea
--- /dev/null
+++ b/src/theory/uf/theory_uf_rewriter.h
@@ -0,0 +1,49 @@
+/*
+ * theory_uf_rewriter.h
+ *
+ *  Created on: Dec 21, 2010
+ *      Author: dejan
+ */
+
+#pragma once
+
+#include "theory/rewriter.h"
+
+namespace CVC4 {
+namespace theory {
+namespace uf {
+
+class TheoryUfRewriter {
+
+public:
+
+  static RewriteResponse postRewrite(TNode node) {
+    if(node.getKind() == kind::EQUAL || node.getKind() == kind::IFF) {
+      if(node[0] == node[1]) {
+        return RewriteResponse(REWRITE_DONE, NodeManager::currentNM()->mkConst(true));
+      }
+      if (node[0] > node[1]) {
+        Node newNode = NodeManager::currentNM()->mkNode(node.getKind(), node[1], node[0]);
+        // If we've switched theories, we need to rewrite again (TODO: THIS IS HACK, once theories accept eq, change)
+        if (Theory::theoryOf(newNode[0]) != Theory::theoryOf(newNode[1])) {
+          return RewriteResponse(REWRITE_AGAIN_FULL, newNode);
+        } else {
+          return RewriteResponse(REWRITE_DONE, newNode);
+        }
+      }
+    }
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  static RewriteResponse preRewrite(TNode node) {
+    return RewriteResponse(REWRITE_DONE, node);
+  }
+
+  static inline void init() {}
+  static inline void shutdown() {}
+
+};
+
+}
+}
+}
diff --git a/src/theory/uf/tim/theory_uf_tim.cpp b/src/theory/uf/tim/theory_uf_tim.cpp
index ccc37a24b..db0574d4f 100644
--- a/src/theory/uf/tim/theory_uf_tim.cpp
+++ b/src/theory/uf/tim/theory_uf_tim.cpp
@@ -27,8 +27,8 @@ using namespace CVC4::theory;
 using namespace CVC4::theory::uf;
 using namespace CVC4::theory::uf::tim;
 
-TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
-  TheoryUF(id, c, out),
+TheoryUFTim::TheoryUFTim(Context* c, OutputChannel& out) :
+  TheoryUF(c, out),
   d_assertions(c),
   d_pending(c),
   d_currentPendingIdx(c,0),
@@ -39,18 +39,6 @@ TheoryUFTim::TheoryUFTim(int id, Context* c, OutputChannel& out) :
 TheoryUFTim::~TheoryUFTim() {
 }
 
-Node TheoryUFTim::rewrite(TNode n){
-  Debug("uf") << "uf: begin rewrite(" << n << ")" << std::endl;
-  Node ret(n);
-  if(n.getKind() == EQUAL){
-    Assert(n.getNumChildren() == 2);
-    if(n[0] == n[1]) {
-      ret = NodeManager::currentNM()->mkConst(true);
-    }
-  }
-  Debug("uf") << "uf: end rewrite(" << n << ") : " << ret << std::endl;
-  return ret;
-}
 void TheoryUFTim::preRegisterTerm(TNode n) {
   Debug("uf") << "uf: begin preRegisterTerm(" << n << ")" << std::endl;
   Debug("uf") << "uf: end preRegisterTerm(" << n << ")" << std::endl;
diff --git a/src/theory/uf/tim/theory_uf_tim.h b/src/theory/uf/tim/theory_uf_tim.h
index 73033f387..cdaa7975c 100644
--- a/src/theory/uf/tim/theory_uf_tim.h
+++ b/src/theory/uf/tim/theory_uf_tim.h
@@ -86,7 +86,7 @@ private:
 public:
 
   /** Constructs a new instance of TheoryUF w.r.t. the provided context.*/
-  TheoryUFTim(int id, context::Context* c, OutputChannel& out);
+  TheoryUFTim(context::Context* c, OutputChannel& out);
 
   /** Destructor for the TheoryUF object. */
   ~TheoryUFTim();
@@ -130,20 +130,6 @@ public:
   }
 
   /**
-   * Rewrites a node in the theory of uninterpreted functions.
-   * This is fairly basic and only ensures that atoms that are
-   * unsatisfiable or a valid are rewritten to false or true respectively.
-   */
-  Node rewrite(TNode n);
-
-  /**
-   * Plug in old rewrite to the new (pre,post)rewrite interface.
-   */
-  RewriteResponse postRewrite(TNode n, bool topLevel) {
-    return RewriteComplete(topLevel ? rewrite(n) : Node(n));
-  }
-
-  /**
    * Propagates theory literals. Currently does nothing.
    *
    * Overloads void propagate(Effort level); from theory.h.
@@ -157,7 +143,7 @@ public:
    * Overloads void explain(TNode n, Effort level); from theory.h.
    * See theory/theory.h for more information about this method.
    */
-  void explain(TNode n, Effort level) {}
+  void explain(TNode n) {}
 
   /**
    * Get a theory value.