diff options
Diffstat (limited to 'src/prop')
-rw-r--r-- | src/prop/cnf_stream.h | 5 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.cpp | 14 | ||||
-rw-r--r-- | src/prop/sat_proof_manager.h | 5 | ||||
-rw-r--r-- | src/prop/skolem_def_manager.cpp | 14 | ||||
-rw-r--r-- | src/prop/skolem_def_manager.h | 7 | ||||
-rw-r--r-- | src/prop/theory_proxy.cpp | 2 | ||||
-rw-r--r-- | src/prop/theory_proxy.h | 2 |
7 files changed, 23 insertions, 26 deletions
diff --git a/src/prop/cnf_stream.h b/src/prop/cnf_stream.h index 2d0b83c33..9901fb18b 100644 --- a/src/prop/cnf_stream.h +++ b/src/prop/cnf_stream.h @@ -75,8 +75,7 @@ class CnfStream { LiteralToNodeMap; /** Cache of what literals have been registered to a node. */ - typedef context::CDInsertHashMap<Node, SatLiteral, NodeHashFunction> - NodeToLiteralMap; + typedef context::CDInsertHashMap<Node, SatLiteral> NodeToLiteralMap; /** * Constructs a CnfStream that performs equisatisfiable CNF transformations @@ -223,7 +222,7 @@ class CnfStream { context::CDList<TNode> d_booleanVariables; /** Formulas that we translated that we are notifying */ - context::CDHashSet<Node, NodeHashFunction> d_notifyFormulas; + context::CDHashSet<Node> d_notifyFormulas; /** Map from nodes to literals */ NodeToLiteralMap d_nodeToLiteralMap; 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 diff --git a/src/prop/sat_proof_manager.h b/src/prop/sat_proof_manager.h index 8f2923981..a53f66cec 100644 --- a/src/prop/sat_proof_manager.h +++ b/src/prop/sat_proof_manager.h @@ -493,8 +493,7 @@ class SatProofManager * have been used as premises of resolution steps while explaining * propagations */ - void explainLit(prop::SatLiteral lit, - std::unordered_set<TNode, TNodeHashFunction>& premises); + void explainLit(prop::SatLiteral lit, std::unordered_set<TNode>& premises); /** Build refutation proof starting from conflict clause * @@ -568,7 +567,7 @@ class SatProofManager /** All clauses added to the SAT solver, kept in a context-dependent manner. */ - context::CDHashSet<Node, NodeHashFunction> d_assumptions; + context::CDHashSet<Node> d_assumptions; /** * A placeholder that may be used to store the literal with the final diff --git a/src/prop/skolem_def_manager.cpp b/src/prop/skolem_def_manager.cpp index 873a748ae..5b51d730c 100644 --- a/src/prop/skolem_def_manager.cpp +++ b/src/prop/skolem_def_manager.cpp @@ -52,7 +52,7 @@ void SkolemDefManager::notifyAsserted(TNode literal, std::vector<TNode>& activatedSkolems, bool useDefs) { - std::unordered_set<Node, NodeHashFunction> skolems; + std::unordered_set<Node> skolems; getSkolems(literal, skolems); for (const Node& k : skolems) { @@ -90,8 +90,8 @@ typedef expr::Attribute<HasSkolemComputedTag, bool> HasSkolemComputedAttr; bool SkolemDefManager::hasSkolems(TNode n) const { - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); @@ -145,11 +145,11 @@ bool SkolemDefManager::hasSkolems(TNode n) const return n.getAttribute(HasSkolemAttr()); } -void SkolemDefManager::getSkolems( - TNode n, std::unordered_set<Node, NodeHashFunction>& skolems) const +void SkolemDefManager::getSkolems(TNode n, + std::unordered_set<Node>& skolems) const { - std::unordered_set<TNode, TNodeHashFunction> visited; - std::unordered_set<TNode, TNodeHashFunction>::iterator it; + std::unordered_set<TNode> visited; + std::unordered_set<TNode>::iterator it; std::vector<TNode> visit; TNode cur; visit.push_back(n); diff --git a/src/prop/skolem_def_manager.h b/src/prop/skolem_def_manager.h index 475f40c85..d3b59f895 100644 --- a/src/prop/skolem_def_manager.h +++ b/src/prop/skolem_def_manager.h @@ -41,8 +41,8 @@ namespace prop { */ class SkolemDefManager { - using NodeNodeMap = context::CDInsertHashMap<Node, Node, NodeHashFunction>; - using NodeSet = context::CDHashSet<Node, NodeHashFunction>; + using NodeNodeMap = context::CDInsertHashMap<Node, Node>; + using NodeSet = context::CDHashSet<Node>; public: SkolemDefManager(context::Context* context, @@ -81,8 +81,7 @@ class SkolemDefManager * @param n The node to traverse * @param skolems The set where the skolems are added */ - void getSkolems(TNode n, - std::unordered_set<Node, NodeHashFunction>& skolems) const; + void getSkolems(TNode n, std::unordered_set<Node>& skolems) const; /** Does n have skolems having definitions managed by this class? */ bool hasSkolems(TNode n) const; diff --git a/src/prop/theory_proxy.cpp b/src/prop/theory_proxy.cpp index 090b44b90..b764695cc 100644 --- a/src/prop/theory_proxy.cpp +++ b/src/prop/theory_proxy.cpp @@ -217,7 +217,7 @@ void TheoryProxy::getSkolems(TNode node, std::vector<Node>& skAsserts, std::vector<Node>& sks) { - std::unordered_set<Node, NodeHashFunction> skolems; + std::unordered_set<Node> skolems; d_skdm->getSkolems(node, skolems); for (const Node& k : skolems) { diff --git a/src/prop/theory_proxy.h b/src/prop/theory_proxy.h index bc834d205..afd99ae83 100644 --- a/src/prop/theory_proxy.h +++ b/src/prop/theory_proxy.h @@ -155,7 +155,7 @@ class TheoryProxy : public Registrar * Set of all lemmas that have been "shared" in the portfolio---i.e., * all imported and exported lemmas. */ - std::unordered_set<Node, NodeHashFunction> d_shared; + std::unordered_set<Node> d_shared; /** The theory preprocessor */ theory::TheoryPreprocessor d_tpp; |