diff options
| author | Richard Qin <richard.qin.x@gmail.com> | 2026-04-03 02:46:12 +0800 |
|---|---|---|
| committer | Richard Qin <richard.qin.x@gmail.com> | 2026-04-03 02:46:12 +0800 |
| commit | 9ab592ce3765d07b6dbdb9c1d9b62dc8045e784e (patch) | |
| tree | 5b2bf93147980c5dabef80eff4c6209caa95f034 /include/atp/core/term_bank.h | |
| parent | 1e35f078fe5ace02b22e6f4ba89f57ba4a58b8c9 (diff) | |
| download | ratp-9ab592ce3765d07b6dbdb9c1d9b62dc8045e784e.tar.gz ratp-9ab592ce3765d07b6dbdb9c1d9b62dc8045e784e.tar.xz | |
feat: implement core term, symbol, and clause storage logic with canonicalization support
Diffstat (limited to 'include/atp/core/term_bank.h')
| -rw-r--r-- | include/atp/core/term_bank.h | 38 |
1 files changed, 33 insertions, 5 deletions
diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h index a121f8a..f909e2f 100644 --- a/include/atp/core/term_bank.h +++ b/include/atp/core/term_bank.h @@ -16,42 +16,70 @@ * along with this program. If not, see <https://www.gnu.org/licenses/>. */ - #pragma once /// @file term_bank.h /// @brief Hash-consing term pool — guarantees structural sharing. +#include "atp/core/symbol_table.h" #include "atp/core/term.h" #include "atp/core/types.h" #include <span> +#include <unordered_map> +#include <vector> namespace atp { /// Global term pool with hash-consing. /// Every structurally identical term maps to the same TermId. +/// +/// Holds a reference to SymbolTable for variable detection. class TermBank { public: - TermBank() = default; + /// TermBank needs the SymbolTable to distinguish variables from constants + /// (both have 0 args, but SymbolKind differs). + explicit TermBank(const SymbolTable& symbols) : symbols_(symbols) {} /// Create or retrieve a term. Returns the canonical TermId. TermId makeTerm(SymbolId symbol, std::span<const TermId> args); - /// Create a variable term. + /// Create a variable term. Convenience for makeTerm(var, {}). TermId makeVar(SymbolId var_symbol); /// Look up a term by its ID. [[nodiscard]] const Term& getTerm(TermId id) const; - /// Check if a TermId represents a variable. + /// Check if a TermId represents a variable (delegates to SymbolTable). [[nodiscard]] bool isVariable(TermId id) const; /// Total number of unique terms stored. [[nodiscard]] size_t size() const; + /// Access the underlying SymbolTable. + [[nodiscard]] const SymbolTable& symbols() const { return symbols_; } + private: - // TODO: Phase 1 implementation — flat arena + hash index + struct TermKey { + SymbolId symbol; + std::vector<TermId> args; + + bool operator==(const TermKey& other) const = default; + }; + + struct TermKeyHash { + size_t operator()(const TermKey& key) const { + size_t seed = std::hash<uint32_t>{}(key.symbol); + for (TermId arg : key.args) { + seed ^= std::hash<uint32_t>{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + return seed; + } + }; + + const SymbolTable& symbols_; + std::vector<Term> terms_; + std::unordered_map<TermKey, TermId, TermKeyHash> term_to_id_; }; } // namespace atp |
