diff options
author | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-28 15:28:38 +0000 |
---|---|---|
committer | Dejan Jovanović <dejan.jovanovic@gmail.com> | 2012-03-28 15:28:38 +0000 |
commit | 9a8d0af063302752905bda7f2043a9695c3126d3 (patch) | |
tree | 9c6ecc3106797348269fb53cf57b3b3974567086 /src | |
parent | 05d64d040fd7340ec713af7b34515c3daac50220 (diff) |
getting rid of a rewrite in uf sharing, speeds things up a bit
Diffstat (limited to 'src')
-rw-r--r-- | src/theory/uf/theory_uf.cpp | 12 |
1 files changed, 4 insertions, 8 deletions
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; } |