2 files changed, 20 insertions, 0 deletions
diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index 2d7d4e91f..1f09ce81d 100644
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -35,6 +35,18 @@ TheoryUF::TheoryUF(Context* c, OutputChannel& out) :
 TheoryUF::~TheoryUF() {
 }
 
+Node TheoryUF::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 TheoryUF::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/theory_uf.h b/src/theory/uf/theory_uf.h
index 5863a31fc..be08cfee7 100644
--- a/src/theory/uf/theory_uf.h
+++ b/src/theory/uf/theory_uf.h
@@ -119,6 +119,14 @@ 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.
+   */
+  Node rewrite(TNode n);
+
   /**
    * Propagates theory literals. Currently does nothing.
    *