From: Dejan Jovanović <dejan.jovanovic@gmail.com>
Date: Wed, 28 Mar 2012 15:28:38 +0000 (+0000)
Subject: getting rid of a rewrite in uf sharing, speeds things up a bit
X-Git-Tag: cvc5-1.0.0~8258
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=9a8d0af063302752905bda7f2043a9695c3126d3;p=cvc5.git

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 a3e347b90..4ac81bc74 100644
--- 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;
 }