diff options
author | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-02 16:25:56 -0500 |
---|---|---|
committer | Andrew Reynolds <andrew.j.reynolds@gmail.com> | 2014-05-02 16:25:56 -0500 |
commit | 0f8c9a8c83322c54027b6523afde1faa42530f19 (patch) | |
tree | b277a68315ccca9a4fd8c1485d2af1f31b5db366 /src/theory | |
parent | e0fa57b1d82647631984e01cbe700af39e348038 (diff) |
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.
Diffstat (limited to 'src/theory')
-rw-r--r-- | src/theory/uf/equality_engine.cpp | 24 |
1 files changed, 0 insertions, 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); |