From: Andrew Reynolds <andrew.j.reynolds@gmail.com>
Date: Fri, 2 May 2014 21:25:56 +0000 (-0500)
Subject: Simplification of EqualityEngine::areDisequal.  Comparison for production : http... 
X-Git-Tag: cvc5-1.0.0~6934
X-Git-Url: https://git.libre-soc.org/?a=commitdiff_plain;h=0f8c9a8c83322c54027b6523afde1faa42530f19;p=cvc5.git

Simplification of EqualityEngine::areDisequal.  Comparison for production : church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6444&reference_id=6445&p=5.  Comparison for debug : http://church.cims.nyu.edu/regress-results/compare_jobs.php?job_id=6449&reference_id=6446&p=5.
---

diff --git a/src/theory/uf/equality_engine.cpp b/src/theory/uf/equality_engine.cpp
index 0fb42231f..65a9b246d 100644
--- a/src/theory/uf/equality_engine.cpp
+++ b/src/theory/uf/equality_engine.cpp
@@ -1494,30 +1494,6 @@ bool EqualityEngine::areDisequal(TNode t1, TNode t2, bool ensureProof) const
     return true;
   }
 
-  // Check the equality itself if it exists
-  Node eq = t1.eqNode(t2);
-  if (hasTerm(eq)) {
-    if (getEqualityNode(eq).getFind() == getEqualityNode(d_falseId).getFind()) {
-      if (ensureProof) {
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId));
-        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
-      }
-      return true;
-    }
-  }
-
-  // Check the other equality itself if it exists
-  eq = t2.eqNode(t1);
-  if (hasTerm(eq)) {
-    if (getEqualityNode(eq).getFind() == getEqualityNode(d_false).getFind()) {
-      if (ensureProof) {
-        nonConst->d_deducedDisequalityReasons.push_back(EqualityPair(getNodeId(eq), d_falseId));
-        nonConst->storePropagatedDisequality(THEORY_LAST, t1Id, t2Id);
-      }
-      return true;
-    }
-  }
-
   // Create the equality
   FunctionApplication eqNormalized(APP_EQUALITY, t1ClassId, t2ClassId);
   ApplicationIdsMap::const_iterator find = d_applicationLookup.find(eqNormalized);