From 0f8c9a8c83322c54027b6523afde1faa42530f19 Mon Sep 17 00:00:00 2001 From: Andrew Reynolds Date: Fri, 2 May 2014 16:25:56 -0500 Subject: [PATCH] Simplification of EqualityEngine::areDisequal. Comparison for production : http://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. --- src/theory/uf/equality_engine.cpp | 24 ------------------------ 1 file changed, 24 deletions(-) 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); -- 2.30.2