Moving the ITE removal from CnfStream to TheoryEngine, which is a bit closer to its final destination. Added a basic rewriter to TheoryUF. (x=x rewrites to true.) Added DIVISION to src/expr/node_manager.cpp's getType. Fixed the theory returned for variables in theoryOf() for bool and arith. Fixed TheoryEngine rewrite children to properly handle APPLY_UFs. Removed the special case for equality in TheoryEngine rewrite. A few tests are currently broken due to deallocation errors. Morgan and I will try to commit a fix to this in a little bit.

1 files changed, 12 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;