diff options
| author | Morgan Deters <mdeters@gmail.com> | 2011-04-05 18:31:38 +0000 |
|---|---|---|
| committer | Morgan Deters <mdeters@gmail.com> | 2011-04-05 18:31:38 +0000 |
| commit | eca82ddc05ff6e81592f7cceec60b0d3269bab5c (patch) | |
| tree | 79a866c00e0b05c46f8e7a50ddee4029266f1d2e /src/util/congruence_closure.h | |
| parent | 7ab9caadb0d56e7788c879b82944ad4a2485135a (diff) | |
Memory fix for congruence closure; affects many UF benchmarks, probably AX too.
Diffstat (limited to 'src/util/congruence_closure.h')
| -rw-r--r-- | src/util/congruence_closure.h | 15 |
1 files changed, 11 insertions, 4 deletions
diff --git a/src/util/congruence_closure.h b/src/util/congruence_closure.h index 9b1b022fa..83f6d15c0 100644 --- a/src/util/congruence_closure.h +++ b/src/util/congruence_closure.h @@ -146,7 +146,7 @@ class CongruenceClosure { typedef context::CDMap<TNode, UseList*, TNodeHashFunction> UseLists; typedef context::CDMap<Node, Node, NodeHashFunction> LookupMap; - typedef context::CDMap<TNode, Node, NodeHashFunction> EqMap; + typedef __gnu_cxx::hash_map<TNode, Node, TNodeHashFunction> EqMap; typedef context::CDMap<Node, Node, NodeHashFunction> ProofMap; typedef context::CDMap<Node, Node, NodeHashFunction> ProofLabel; @@ -164,6 +164,7 @@ class CongruenceClosure { LookupMap d_lookup; EqMap d_eqMap; + context::CDSet<TNode, TNodeHashFunction> d_added; ProofMap d_proof; ProofLabel d_proofLabel; @@ -203,7 +204,7 @@ public: d_classList(ctxt), d_useList(ctxt), d_lookup(ctxt), - d_eqMap(ctxt), + d_added(ctxt), d_proof(ctxt), d_proofLabel(ctxt), d_proofRewrite(ctxt), @@ -270,10 +271,16 @@ private: ++d_newSkolemVars; Node v = NodeManager::currentNM()->mkSkolem(t.getType()); addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); - d_eqMap.insert(t, v); + d_added.insert(v); + d_eqMap[t] = v; return v; } else { - return (*i).second; + TNode v = (*i).second; + if(!d_added.contains(v)) { + addEq(NodeManager::currentNM()->mkNode(t.getType().isBoolean() ? kind::IFF : kind::EQUAL, t, v), TNode::null()); + d_added.insert(v); + } + return v; } } else { return t; |