getting rid of a rewrite in uf sharing, speeds things up a bit

diff --git a/src/theory/uf/theory_uf.cpp b/src/theory/uf/theory_uf.cpp
index a3e347b90ef4c08f5eeceaa0635a8b71057cc757..4ac81bc7446b8e3f206c17ceb140ee479825ce56 100644 (file)
--- a/src/theory/uf/theory_uf.cpp
+++ b/src/theory/uf/theory_uf.cpp
@@ -397,22 +397,18 @@ void TheoryUF::ppStaticLearn(TNode n, NodeBuilder<>& learned) {
 
 EqualityStatus TheoryUF::getEqualityStatus(TNode a, TNode b) {
 
-  Node equality = a.eqNode(b);
-  Node rewrittenEquality = Rewriter::rewrite(equality);
-  if (rewrittenEquality.isConst()) {
-    if (!rewrittenEquality.getConst<bool>()) {
-      return EQUALITY_FALSE;
-    }
-  }
-
+  // Check for equality (simplest)
   if (d_equalityEngine.areEqual(a, b)) {
     // The terms are implied to be equal
     return EQUALITY_TRUE;
   }
+
+  // Check for disequality
   if (d_equalityEngine.areDisequal(a, b)) {
     // The terms are implied to be dis-equal
     return EQUALITY_FALSE;
   }
+
   // All other terms we interpret as dis-equal in the model
   return EQUALITY_FALSE_IN_MODEL;
 }