diff options
Diffstat (limited to 'src/theory/uf/eq_proof.cpp')
| -rw-r--r-- | src/theory/uf/eq_proof.cpp | 20 |
1 files changed, 9 insertions, 11 deletions
diff --git a/src/theory/uf/eq_proof.cpp b/src/theory/uf/eq_proof.cpp index 8e5e0f659..c63f8b51d 100644 --- a/src/theory/uf/eq_proof.cpp +++ b/src/theory/uf/eq_proof.cpp @@ -106,7 +106,7 @@ bool EqProof::expandTransitivityForDisequalities( Node conclusion, std::vector<Node>& premises, CDProof* p, - std::unordered_set<Node, NodeHashFunction>& assumptions) const + std::unordered_set<Node>& assumptions) const { Trace("eqproof-conv") << "EqProof::expandTransitivityForDisequalities: check if need " @@ -684,8 +684,8 @@ void EqProof::reduceNestedCongruence( Node conclusion, std::vector<std::vector<Node>>& transitivityMatrix, CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions, bool isNary) const { Trace("eqproof-conv") << "EqProof::reduceNestedCongruence: building for " << i @@ -785,8 +785,8 @@ void EqProof::reduceNestedCongruence( Node EqProof::addToProof(CDProof* p) const { - std::unordered_map<Node, Node, NodeHashFunction> cache; - std::unordered_set<Node, NodeHashFunction> assumptions; + std::unordered_map<Node, Node> cache; + std::unordered_set<Node> assumptions; Node conclusion = addToProof(p, cache, assumptions); Trace("eqproof-conv") << "EqProof::addToProof: root of proof: " << conclusion << "\n"; @@ -840,13 +840,11 @@ Node EqProof::addToProof(CDProof* p) const return newConclusion; } -Node EqProof::addToProof( - CDProof* p, - std::unordered_map<Node, Node, NodeHashFunction>& visited, - std::unordered_set<Node, NodeHashFunction>& assumptions) const +Node EqProof::addToProof(CDProof* p, + std::unordered_map<Node, Node>& visited, + std::unordered_set<Node>& assumptions) const { - std::unordered_map<Node, Node, NodeHashFunction>::const_iterator it = - visited.find(d_node); + std::unordered_map<Node, Node>::const_iterator it = visited.find(d_node); if (it != visited.end()) { Trace("eqproof-conv") << "EqProof::addToProof: already processed " << d_node |