diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-08 03:23:16 +0800 |
| commit | 4b31d8f59a6d3237f176a122c82f46fdaef4551d (patch) | |
| tree | 917c9d42bb2cdbe96f5fc5416ae55789986029d7 /include/atp/core/term_bank.h | |
| parent | 5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 (diff) | |
| download | ratp-master.tar.gz ratp-master.tar.xz | |
Diffstat (limited to 'include/atp/core/term_bank.h')
| -rw-r--r-- | include/atp/core/term_bank.h | 11 |
1 files changed, 6 insertions, 5 deletions
diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h index 3339ceb..ca12759 100644 --- a/include/atp/core/term_bank.h +++ b/include/atp/core/term_bank.h @@ -39,7 +39,7 @@ class TermBank { public: /// TermBank needs the SymbolTable to distinguish variables from constants /// (both have 0 args, but SymbolKind differs). - explicit TermBank(const SymbolTable& symbols) : symbols_(symbols) {} + explicit TermBank(SymbolTable& symbols) : symbols_(&symbols) {} /// Create or retrieve a term. Returns the canonical TermId. TermId makeTerm(SymbolId symbol, std::span<const TermId> args); @@ -57,7 +57,8 @@ class TermBank { [[nodiscard]] size_t size() const; /// Access the underlying SymbolTable. - [[nodiscard]] const SymbolTable& symbols() const { return symbols_; } + [[nodiscard]] const SymbolTable& symbols() const { return *symbols_; } + [[nodiscard]] SymbolTable& mutableSymbols() { return *symbols_; } private: struct TermKey { @@ -70,14 +71,14 @@ class TermBank { struct TermKeyHash { size_t operator()(const TermKey& key) const { size_t seed = std::hash<uint32_t>{}(key.symbol_); - for (const TermId kArg : key.args_) { - seed ^= std::hash<TermId>{}(kArg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + for (const TermId arg : key.args_) { + seed ^= std::hash<TermId>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); } return seed; } }; - const SymbolTable& symbols_; + SymbolTable* symbols_; std::vector<Term> terms_; std::unordered_map<TermKey, TermId, TermKeyHash> term_to_id_; }; |
