diff options
| author | Gereon Kremer <gkremer@stanford.edu> | 2021-04-27 07:31:58 +0200 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2021-04-27 05:31:58 +0000 |
| commit | 20820daece2eaf340a944ff386ffbafed1b79b75 (patch) | |
| tree | fc7865a1bb468fa4d3749052f65106d15532dd31 /src/parser | |
| parent | baeb7af81166d709bfbbc7b8da13ac238c1e9579 (diff) | |
Use std::hash for API types (#6432)
This PR replaces all api::*HashFunction objects by specializations of std::hash. std::hash is meant to be extended in this way, and it allows for a much cleaner usage of std::unordered_set and std::unordered_map with these types.
Diffstat (limited to 'src/parser')
| -rw-r--r-- | src/parser/tptp/tptp.h | 2 |
1 files changed, 1 insertions, 1 deletions
diff --git a/src/parser/tptp/tptp.h b/src/parser/tptp/tptp.h index daeb5be58..0be74c79d 100644 --- a/src/parser/tptp/tptp.h +++ b/src/parser/tptp/tptp.h @@ -193,7 +193,7 @@ class Tptp : public Parser { api::Term d_utr_op; api::Term d_uts_op; // The set of expression that already have a bridge - std::unordered_set<api::Term, api::TermHashFunction> d_r_converted; + std::unordered_set<api::Term> d_r_converted; std::unordered_map<std::string, api::Term> d_distinct_objects; std::vector< pANTLR3_INPUT_STREAM > d_in_created; |