diff options
Diffstat (limited to 'src/theory/booleans')
| -rw-r--r-- | src/theory/booleans/circuit_propagator.h | 8 | ||||
| -rw-r--r-- | src/theory/booleans/proof_checker.cpp | 15 | ||||
| -rw-r--r-- | src/theory/booleans/theory_bool_rewriter.cpp | 2 |
3 files changed, 11 insertions, 14 deletions
diff --git a/src/theory/booleans/circuit_propagator.h b/src/theory/booleans/circuit_propagator.h index 443be0ec7..1d4f6e9ee 100644 --- a/src/theory/booleans/circuit_propagator.h +++ b/src/theory/booleans/circuit_propagator.h @@ -63,8 +63,7 @@ class CircuitPropagator ASSIGNED_TO_FALSE, }; - typedef std::unordered_map<Node, std::vector<Node>, NodeHashFunction> - BackEdgesMap; + typedef std::unordered_map<Node, std::vector<Node>> BackEdgesMap; /** * Construct a new CircuitPropagator. @@ -172,8 +171,7 @@ class CircuitPropagator /** * Assignment status of each node. */ - typedef context::CDHashMap<TNode, AssignmentStatus, TNodeHashFunction> - AssignmentMap; + typedef context::CDHashMap<TNode, AssignmentStatus> AssignmentMap; /** * Assign Node in circuit with the value and add it to the queue; note @@ -245,7 +243,7 @@ class CircuitPropagator /** Nodes that have been attached already (computed forward edges for) */ // All the nodes we've visited so far - context::CDHashSet<Node, NodeHashFunction> d_seen; + context::CDHashSet<Node> d_seen; AssignmentMap d_state; diff --git a/src/theory/booleans/proof_checker.cpp b/src/theory/booleans/proof_checker.cpp index 8b2967fe6..2d2155f44 100644 --- a/src/theory/booleans/proof_checker.cpp +++ b/src/theory/booleans/proof_checker.cpp @@ -140,7 +140,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, return Node::null(); } // remove duplicates while keeping the order of children - std::unordered_set<TNode, TNodeHashFunction> clauseSet; + std::unordered_set<TNode> clauseSet; std::vector<Node> disjuncts; unsigned size = children[0].getNumChildren(); for (unsigned i = 0; i < size; ++i) @@ -166,7 +166,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { Assert(children.size() == 1); Assert(args.size() == 1); - std::unordered_set<Node, NodeHashFunction> clauseSet1, clauseSet2; + std::unordered_set<Node> clauseSet1, clauseSet2; if (children[0].getKind() == kind::OR) { clauseSet1.insert(children[0].begin(), children[0].end()); @@ -201,7 +201,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, Node falseNode = nm->mkConst(false); std::vector<Node> clauseNodes; // literals to be removed from the virtual lhs clause of the resolution - std::unordered_map<Node, unsigned, NodeHashFunction> lhsElim; + std::unordered_map<Node, unsigned> lhsElim; for (std::size_t i = 0, argsSize = args.size(); i < argsSize; i = i + 2) { // whether pivot should occur as is or negated depends on the polarity of @@ -320,7 +320,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, for (std::size_t i = 0, childrenSize = children.size(); i < childrenSize; ++i) { - std::unordered_set<Node, NodeHashFunction> elim; + std::unordered_set<Node> elim; // literals to be removed from "first" clause if (i < childrenSize - 1) { @@ -387,8 +387,8 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, } Trace("bool-pfcheck") << "clause: " << clauseNodes << "\n"; // check that set representation is the same as of the given conclusion - std::unordered_set<Node, NodeHashFunction> clauseComputed{ - clauseNodes.begin(), clauseNodes.end()}; + std::unordered_set<Node> clauseComputed{clauseNodes.begin(), + clauseNodes.end()}; Trace("bool-pfcheck") << "clauseSet: " << clauseComputed << "\n" << pop; if (clauseComputed.empty()) { @@ -415,8 +415,7 @@ Node BoolProofRuleChecker::checkInternal(PfRule id, { return Node::null(); } - std::unordered_set<Node, NodeHashFunction> clauseGiven{args[0].begin(), - args[0].end()}; + std::unordered_set<Node> clauseGiven{args[0].begin(), args[0].end()}; return clauseComputed == clauseGiven ? args[0] : Node::null(); } if (id == PfRule::SPLIT) diff --git a/src/theory/booleans/theory_bool_rewriter.cpp b/src/theory/booleans/theory_bool_rewriter.cpp index 0d7431a8e..44d337c28 100644 --- a/src/theory/booleans/theory_bool_rewriter.cpp +++ b/src/theory/booleans/theory_bool_rewriter.cpp @@ -45,7 +45,7 @@ RewriteResponse TheoryBoolRewriter::postRewrite(TNode node) { */ RewriteResponse flattenNode(TNode n, TNode trivialNode, TNode skipNode) { - typedef std::unordered_set<TNode, TNodeHashFunction> node_set; + typedef std::unordered_set<TNode> node_set; node_set visited; visited.insert(skipNode); |