diff options
Diffstat (limited to 'src/theory/bv/bitblast')
-rw-r--r-- | src/theory/bv/bitblast/aig_bitblaster.h | 4 | ||||
-rw-r--r-- | src/theory/bv/bitblast/bitblaster.h | 10 | ||||
-rw-r--r-- | src/theory/bv/bitblast/eager_bitblaster.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.cpp | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/proof_bitblaster.h | 2 | ||||
-rw-r--r-- | src/theory/bv/bitblast/simple_bitblaster.h | 2 |
6 files changed, 11 insertions, 11 deletions
diff --git a/src/theory/bv/bitblast/aig_bitblaster.h b/src/theory/bv/bitblast/aig_bitblaster.h index a7dfb00e5..39ecbc12c 100644 --- a/src/theory/bv/bitblast/aig_bitblaster.h +++ b/src/theory/bv/bitblast/aig_bitblaster.h @@ -56,8 +56,8 @@ class AigBitblaster : public TBitblaster<Abc_Obj_t*> static Abc_Ntk_t* currentAigNtk(); private: - typedef std::unordered_map<TNode, Abc_Obj_t*, TNodeHashFunction> TNodeAigMap; - typedef std::unordered_map<Node, Abc_Obj_t*, NodeHashFunction> NodeAigMap; + typedef std::unordered_map<TNode, Abc_Obj_t*> TNodeAigMap; + typedef std::unordered_map<Node, Abc_Obj_t*> NodeAigMap; static thread_local Abc_Ntk_t* s_abcAigNetwork; std::unique_ptr<context::Context> d_nullContext; diff --git a/src/theory/bv/bitblast/bitblaster.h b/src/theory/bv/bitblast/bitblaster.h index 2a7931aa0..a669e4a86 100644 --- a/src/theory/bv/bitblast/bitblaster.h +++ b/src/theory/bv/bitblast/bitblaster.h @@ -38,8 +38,8 @@ namespace cvc5 { namespace theory { namespace bv { -typedef std::unordered_set<Node, NodeHashFunction> NodeSet; -typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; +typedef std::unordered_set<Node> NodeSet; +typedef std::unordered_set<TNode> TNodeSet; /** * The Bitblaster that manages the mapping between Nodes @@ -52,9 +52,9 @@ class TBitblaster { protected: typedef std::vector<T> Bits; - typedef std::unordered_map<Node, Bits, NodeHashFunction> TermDefMap; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; - typedef std::unordered_map<Node, Node, NodeHashFunction> ModelCache; + typedef std::unordered_map<Node, Bits> TermDefMap; + typedef std::unordered_set<TNode> TNodeSet; + typedef std::unordered_map<Node, Node> ModelCache; typedef void (*TermBBStrategy)(TNode, Bits&, TBitblaster<T>*); typedef T (*AtomBBStrategy)(TNode, TBitblaster<T>*); diff --git a/src/theory/bv/bitblast/eager_bitblaster.h b/src/theory/bv/bitblast/eager_bitblaster.h index 765f3051e..9e5ace9d8 100644 --- a/src/theory/bv/bitblast/eager_bitblaster.h +++ b/src/theory/bv/bitblast/eager_bitblaster.h @@ -56,7 +56,7 @@ class EagerBitblaster : public TBitblaster<Node> private: context::Context* d_context; - typedef std::unordered_set<TNode, TNodeHashFunction> TNodeSet; + typedef std::unordered_set<TNode> TNodeSet; std::unique_ptr<prop::SatSolver> d_satSolver; std::unique_ptr<BitblastingRegistrar> d_bitblastingRegistrar; diff --git a/src/theory/bv/bitblast/proof_bitblaster.cpp b/src/theory/bv/bitblast/proof_bitblaster.cpp index 09448da8a..4d6501673 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.cpp +++ b/src/theory/bv/bitblast/proof_bitblaster.cpp @@ -81,7 +81,7 @@ void BBProof::bbAtom(TNode node) { std::vector<TNode> visit; visit.push_back(node); - std::unordered_set<TNode, TNodeHashFunction> visited; + std::unordered_set<TNode> visited; bool fproofs = options::proofGranularityMode() != options::ProofGranularityMode::OFF; diff --git a/src/theory/bv/bitblast/proof_bitblaster.h b/src/theory/bv/bitblast/proof_bitblaster.h index 6cd4960fb..ef23c05c0 100644 --- a/src/theory/bv/bitblast/proof_bitblaster.h +++ b/src/theory/bv/bitblast/proof_bitblaster.h @@ -60,7 +60,7 @@ class BBProof /** The associated term conversion proof generator. */ TConvProofGenerator* d_tcpg; /** Map bit-vector nodes to bit-blasted nodes. */ - std::unordered_map<Node, Node, NodeHashFunction> d_bbMap; + std::unordered_map<Node, Node> d_bbMap; }; } // namespace bv diff --git a/src/theory/bv/bitblast/simple_bitblaster.h b/src/theory/bv/bitblast/simple_bitblaster.h index 04a35bc4f..ebbb2891f 100644 --- a/src/theory/bv/bitblast/simple_bitblaster.h +++ b/src/theory/bv/bitblast/simple_bitblaster.h @@ -68,7 +68,7 @@ class BBSimple : public TBitblaster<Node> /** Caches variables for which we already created bits. */ TNodeSet d_variables; /** Stores bit-blasted atoms. */ - std::unordered_map<Node, Node, NodeHashFunction> d_bbAtoms; + std::unordered_map<Node, Node> d_bbAtoms; /** Theory state. */ TheoryState* d_state; }; |