diff options
Diffstat (limited to 'src/theory/quantifiers/sygus/sygus_reconstruct.h')
| -rw-r--r-- | src/theory/quantifiers/sygus/sygus_reconstruct.h | 22 |
1 files changed, 10 insertions, 12 deletions
diff --git a/src/theory/quantifiers/sygus/sygus_reconstruct.h b/src/theory/quantifiers/sygus/sygus_reconstruct.h index 334b95e71..e3c214bde 100644 --- a/src/theory/quantifiers/sygus/sygus_reconstruct.h +++ b/src/theory/quantifiers/sygus/sygus_reconstruct.h @@ -28,9 +28,8 @@ namespace cvc5 { namespace theory { namespace quantifiers { -using ObligationSet = std::unordered_set<Node, NodeHashFunction>; -using TypeObligationSetMap = - std::unordered_map<TypeNode, ObligationSet, TypeNodeHashFunction>; +using ObligationSet = std::unordered_set<Node>; +using TypeObligationSetMap = std::unordered_map<TypeNode, ObligationSet>; /** SygusReconstruct * @@ -288,9 +287,8 @@ class SygusReconstruct : public expr::NotifyMatch * * @param pool a pool of patterns/shapes to print */ - void printPool(const std::unordered_map<TypeNode, - std::vector<Node>, - TypeNodeHashFunction>& pool) const; + void printPool( + const std::unordered_map<TypeNode, std::vector<Node>>& pool) const; /** pointer to the sygus term database */ TermDbSygus* d_tds; @@ -298,20 +296,20 @@ class SygusReconstruct : public expr::NotifyMatch SygusStatistics& d_stats; /** a map from an obligation to its reconstruction info */ - std::unordered_map<Node, RConsObligationInfo, NodeHashFunction> d_obInfo; + std::unordered_map<Node, RConsObligationInfo> d_obInfo; /** a map from a sygus datatype type to its reconstruction info */ - std::unordered_map<TypeNode, RConsTypeInfo, TypeNodeHashFunction> d_stnInfo; + std::unordered_map<TypeNode, RConsTypeInfo> d_stnInfo; /** a map from an obligation to its sygus solution (if it exists) */ - std::unordered_map<TNode, TNode, TNodeHashFunction> d_sol; + std::unordered_map<TNode, TNode> d_sol; /** a map from a candidate solution to its sub-obligations */ - std::unordered_map<Node, std::vector<Node>, NodeHashFunction> d_subObs; + std::unordered_map<Node, std::vector<Node>> d_subObs; /** a map from a candidate solution to its parent obligation */ - std::unordered_map<Node, Node, NodeHashFunction> d_parentOb; + std::unordered_map<Node, Node> d_parentOb; /** a cache of sygus variables treated as ground terms by matching */ - std::unordered_map<Node, Node, NodeHashFunction> d_sygusVars; + std::unordered_map<Node, Node> d_sygusVars; /** A trie for filtering out redundant terms from the paterns pool */ expr::MatchTrie d_poolTrie; |