diff options
Diffstat (limited to 'src/prop/sat_proof_manager.cpp')
| -rw-r--r-- | src/prop/sat_proof_manager.cpp | 14 |
1 files changed, 7 insertions, 7 deletions
diff --git a/src/prop/sat_proof_manager.cpp b/src/prop/sat_proof_manager.cpp index 5fdc0eb79..60a4c9704 100644 --- a/src/prop/sat_proof_manager.cpp +++ b/src/prop/sat_proof_manager.cpp @@ -330,8 +330,8 @@ void SatProofManager::processRedundantLit( !negated); } -void SatProofManager::explainLit( - SatLiteral lit, std::unordered_set<TNode, TNodeHashFunction>& premises) +void SatProofManager::explainLit(SatLiteral lit, + std::unordered_set<TNode>& premises) { Trace("sat-proof") << push << "SatProofManager::explainLit: Lit: " << lit; Node litNode = getClauseNode(lit); @@ -393,7 +393,7 @@ void SatProofManager::explainLit( { continue; } - std::unordered_set<TNode, TNodeHashFunction> childPremises; + std::unordered_set<TNode> childPremises; explainLit(~currLit, childPremises); // save to resolution chain premises / arguments Assert(d_cnfStream->getNodeCache().find(currLit) @@ -462,7 +462,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, Trace("sat-proof-debug2") << push << "SatProofManager::finalizeProof: saved proofs in chain:\n"; std::map<Node, std::shared_ptr<ProofNode>> links = d_resChains.getLinks(); - std::unordered_set<Node, NodeHashFunction> skip; + std::unordered_set<Node> skip; for (const std::pair<const Node, std::shared_ptr<ProofNode>>& link : links) { if (skip.count(link.first)) @@ -546,12 +546,12 @@ void SatProofManager::finalizeProof(Node inConflictNode, // we call explainLit on each ~l_i while accumulating the children and // arguments for the resolution step to conclude false. std::vector<Node> children{inConflictNode}, args; - std::unordered_set<TNode, TNodeHashFunction> premises; + std::unordered_set<TNode> premises; for (unsigned i = 0, size = inConflict.size(); i < size; ++i) { Assert(d_cnfStream->getNodeCache().find(inConflict[i]) != d_cnfStream->getNodeCache().end()); - std::unordered_set<TNode, TNodeHashFunction> childPremises; + std::unordered_set<TNode> childPremises; explainLit(~inConflict[i], childPremises); Node negatedLitNode = d_cnfStream->getNodeCache()[~inConflict[i]]; // save to resolution chain premises / arguments @@ -659,7 +659,7 @@ void SatProofManager::finalizeProof(Node inConflictNode, // mark another iteration for the loop, as some resolution link may be // connected because of the new justifications expanded = true; - std::unordered_set<TNode, TNodeHashFunction> childPremises; + std::unordered_set<TNode> childPremises; explainLit(it->second, childPremises); // add the premises used in the justification. We know they will have // been as expanded as possible |