From 9ab592ce3765d07b6dbdb9c1d9b62dc8045e784e Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Fri, 3 Apr 2026 02:46:12 +0800 Subject: feat: implement core term, symbol, and clause storage logic with canonicalization support --- include/atp/core/clause_store.h | 3 + include/atp/core/symbol_table.h | 4 + include/atp/core/term.h | 20 +-- include/atp/core/term_bank.h | 38 ++++- src/core/clause_store.cc | 34 +++++ src/core/symbol_table.cc | 43 ++++++ src/core/term_bank.cc | 37 +++++ tests/test_term_bank.cc | 316 ++++++++++++++++++++++++++++++++++++++++ 8 files changed, 481 insertions(+), 14 deletions(-) diff --git a/include/atp/core/clause_store.h b/include/atp/core/clause_store.h index 6e220cc..23db996 100644 --- a/include/atp/core/clause_store.h +++ b/include/atp/core/clause_store.h @@ -54,6 +54,9 @@ class ClauseStore { /// Iterate over all clauses with a visitor. void forEach(const std::function& visitor) const; + // function may have type erasure overhead, consider using a template + // template + // void forEach(Visitor&& visitor) const; private: std::vector clauses_; diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h index ed27a4d..856c395 100644 --- a/include/atp/core/symbol_table.h +++ b/include/atp/core/symbol_table.h @@ -23,8 +23,10 @@ /// @brief Bidirectional mapping between symbol names and SymbolIds, /// with kind and sort metadata. +#include #include #include +#include #include "atp/core/types.h" @@ -63,6 +65,8 @@ class SymbolTable { private: // TODO: Phase 1 implementation + std::deque infos_; + std::unordered_map name_to_id_; }; } // namespace atp diff --git a/include/atp/core/term.h b/include/atp/core/term.h index e1edfcf..017882a 100644 --- a/include/atp/core/term.h +++ b/include/atp/core/term.h @@ -16,28 +16,30 @@ * along with this program. If not, see . */ - #pragma once /// @file term.h /// @brief Core Term data structure — hash-consed, immutable. +/// +/// V1 uses vector for args. +/// Future: flat arena with contiguous arg storage for cache locality. -#include +#include #include "atp/core/types.h" namespace atp { /// A term is a function/predicate application: f(t1, t2, ..., tn). -/// Stored in a flat arena; args are contiguous TermIds following the header. -/// Variables are represented as terms with a special symbol range. +/// Variables are 0-arity terms whose symbol has SymbolKind::kVariable. struct Term { - SymbolId symbol_id; ///< Index into the SymbolTable - uint16_t arity; ///< Number of arguments + SymbolId symbol_id; ///< Index into the SymbolTable + std::vector args; ///< Argument sub-term IDs - /// Access the argument TermIds (stored immediately after this struct in the arena). - [[nodiscard]] std::span args() const; - [[nodiscard]] std::span mutableArgs(); + /// Number of arguments. + [[nodiscard]] uint16_t arity() const { + return static_cast(args.size()); + } }; } // namespace atp 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 . */ - #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 +#include +#include 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 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 args; + + bool operator==(const TermKey& other) const = default; + }; + + struct TermKeyHash { + size_t operator()(const TermKey& key) const { + size_t seed = std::hash{}(key.symbol); + for (TermId arg : key.args) { + seed ^= std::hash{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + } + return seed; + } + }; + + const SymbolTable& symbols_; + std::vector terms_; + std::unordered_map term_to_id_; }; } // namespace atp diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc index b62ffd0..a0adbe6 100644 --- a/src/core/clause_store.cc +++ b/src/core/clause_store.cc @@ -16,4 +16,38 @@ * along with this program. If not, see . */ +#include "atp/core/clause_store.h" +#include +#include +namespace atp { + +ClauseId ClauseStore::addClause(Clause clause) { + auto new_id = static_cast(clauses_.size()); + clause.id = new_id; + clauses_.push_back(std::move(clause)); + return new_id; +} + +const Clause& ClauseStore::getClause(ClauseId id) const { + assert(id < clauses_.size() && "ClauseId out of bounds!"); + return clauses_[id]; +} + +Clause& ClauseStore::getMutableClause(ClauseId id) { + assert(id < clauses_.size() && "ClauseId out of bounds!"); + return clauses_[id]; +} + +size_t ClauseStore::size() const { + return clauses_.size(); +} + +void ClauseStore::forEach(const std::function& visitor) const { + for (const auto& clause : clauses_) { + // TODO: Tombstone mechanism + visitor(clause); + } +} + +} // namespace atp diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc index b62ffd0..261805a 100644 --- a/src/core/symbol_table.cc +++ b/src/core/symbol_table.cc @@ -16,4 +16,47 @@ * along with this program. If not, see . */ +#include "atp/core/symbol_table.h" +#include "atp/core/types.h" +#include +#include +#include + +namespace atp { + +SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, + SortId sort) { + auto it = name_to_id_.find(name); + if (it != name_to_id_.end()) { + SymbolId id = it->second; + SymbolInfo& info = infos_[id]; + if (info.kind != kind || info.arity != arity) { + throw std::runtime_error("Symbol kind or arity mismatch for: " + std::string(name)); + } + return id; + } + auto new_id = static_cast(infos_.size()); + infos_.push_back({.name = std::string(name), .kind = kind, .arity = arity, .sort = sort}); + std::string_view stable_name_view = infos_.back().name; + name_to_id_.emplace(stable_name_view, new_id); + return new_id; +} + +std::string_view SymbolTable::getName(SymbolId id) const { + return infos_[id].name; +} + +const SymbolInfo& SymbolTable::getInfo(SymbolId id) const { + return infos_[id]; +} + +bool SymbolTable::isVariable(SymbolId id) const { + return infos_[id].kind == SymbolKind::kVariable; +} + +size_t SymbolTable::size() const { + return infos_.size(); +} + +} // namespace atp diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc index b62ffd0..53b4f0c 100644 --- a/src/core/term_bank.cc +++ b/src/core/term_bank.cc @@ -16,4 +16,41 @@ * along with this program. If not, see . */ +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include +namespace atp { + +TermId TermBank::makeTerm(SymbolId symbol, std::span args) { + TermKey key{.symbol = symbol, .args = {args.begin(), args.end()}}; + auto it = term_to_id_.find(key); + if (it != term_to_id_.end()) { + return it->second; + } + auto new_id = static_cast(terms_.size()); + Term new_term{.symbol_id = symbol, .args = {args.begin(), args.end()}}; + terms_.push_back(std::move(new_term)); + term_to_id_.emplace(std::move(key), new_id); + return new_id; +} + +TermId TermBank::makeVar(SymbolId var_symbol) { + return makeTerm(var_symbol, {}); +} + +const Term& TermBank::getTerm(TermId id) const { + assert(id < terms_.size() && "TermId out of bounds!"); + return terms_[id]; +} + +bool TermBank::isVariable(TermId id) const { + assert(id < terms_.size() && "TermId out of bounds!"); + return symbols_.isVariable(terms_[id].symbol_id); +} + +size_t TermBank::size() const { + return terms_.size(); +} + +} // namespace atp diff --git a/tests/test_term_bank.cc b/tests/test_term_bank.cc index b62ffd0..63acc34 100644 --- a/tests/test_term_bank.cc +++ b/tests/test_term_bank.cc @@ -16,4 +16,320 @@ * along with this program. If not, see . */ +#include +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/literal.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// SymbolTable Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(SymbolTableTest, InternReturnsConsistentId) { + SymbolTable st; + SymbolId id1 = st.intern("foo", SymbolKind::kFunction, 2); + SymbolId id2 = st.intern("foo", SymbolKind::kFunction, 2); + EXPECT_EQ(id1, id2); +} + +TEST(SymbolTableTest, DifferentNamesGetDifferentIds) { + SymbolTable st; + SymbolId a = st.intern("a", SymbolKind::kConstant); + SymbolId b = st.intern("b", SymbolKind::kConstant); + EXPECT_NE(a, b); +} + +TEST(SymbolTableTest, GetNameRoundTrips) { + SymbolTable st; + SymbolId id = st.intern("hello", SymbolKind::kFunction, 1); + EXPECT_EQ(st.getName(id), "hello"); +} + +TEST(SymbolTableTest, GetInfoPreservesMetadata) { + SymbolTable st; + SymbolId id = st.intern("P", SymbolKind::kPredicate, 3, 42); + const SymbolInfo& info = st.getInfo(id); + EXPECT_EQ(info.name, "P"); + EXPECT_EQ(info.kind, SymbolKind::kPredicate); + EXPECT_EQ(info.arity, 3); + EXPECT_EQ(info.sort, 42); +} + +TEST(SymbolTableTest, IsVariableDetectsKind) { + SymbolTable st; + SymbolId var = st.intern("X", SymbolKind::kVariable); + SymbolId con = st.intern("a", SymbolKind::kConstant); + SymbolId fun = st.intern("f", SymbolKind::kFunction, 1); + EXPECT_TRUE(st.isVariable(var)); + EXPECT_FALSE(st.isVariable(con)); + EXPECT_FALSE(st.isVariable(fun)); +} + +TEST(SymbolTableTest, MismatchKindThrows) { + SymbolTable st; + st.intern("x", SymbolKind::kConstant); + EXPECT_THROW(st.intern("x", SymbolKind::kVariable), std::runtime_error); +} + +TEST(SymbolTableTest, MismatchArityThrows) { + SymbolTable st; + st.intern("f", SymbolKind::kFunction, 1); + EXPECT_THROW(st.intern("f", SymbolKind::kFunction, 2), std::runtime_error); +} + +TEST(SymbolTableTest, SizeTracksInternedSymbols) { + SymbolTable st; + EXPECT_EQ(st.size(), 0); + st.intern("a", SymbolKind::kConstant); + EXPECT_EQ(st.size(), 1); + st.intern("b", SymbolKind::kConstant); + EXPECT_EQ(st.size(), 2); + st.intern("a", SymbolKind::kConstant); // duplicate + EXPECT_EQ(st.size(), 2); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// TermBank Tests +// ═══════════════════════════════════════════════════════════════════════════ + +class TermBankTest : public ::testing::Test { + protected: + SymbolTable symbols; + TermBank bank{symbols}; + + SymbolId sym_a, sym_b, sym_f, sym_g, sym_X, sym_Y; + + void SetUp() override { + sym_a = symbols.intern("a", SymbolKind::kConstant); + sym_b = symbols.intern("b", SymbolKind::kConstant); + sym_f = symbols.intern("f", SymbolKind::kFunction, 1); + sym_g = symbols.intern("g", SymbolKind::kFunction, 2); + sym_X = symbols.intern("X", SymbolKind::kVariable); + sym_Y = symbols.intern("Y", SymbolKind::kVariable); + } +}; + +TEST_F(TermBankTest, HashConsingReturnsSameId) { + TermId a1 = bank.makeTerm(sym_a, {}); + TermId a2 = bank.makeTerm(sym_a, {}); + EXPECT_EQ(a1, a2) << "Hash consing failed: same term got different IDs"; +} + +TEST_F(TermBankTest, DifferentTermsGetDifferentIds) { + TermId a = bank.makeTerm(sym_a, {}); + TermId b = bank.makeTerm(sym_b, {}); + EXPECT_NE(a, b); +} + +TEST_F(TermBankTest, CompoundTermHashConsing) { + TermId a = bank.makeTerm(sym_a, {}); + TermId b = bank.makeTerm(sym_b, {}); + // f(a) + TermId fa1 = bank.makeTerm(sym_f, {{a}}); + TermId fa2 = bank.makeTerm(sym_f, {{a}}); + EXPECT_EQ(fa1, fa2); + // f(b) != f(a) + TermId fb = bank.makeTerm(sym_f, {{b}}); + EXPECT_NE(fa1, fb); +} + +TEST_F(TermBankTest, NestedTermHashConsing) { + TermId a = bank.makeTerm(sym_a, {}); + TermId fa = bank.makeTerm(sym_f, {{a}}); + // g(f(a), a) + TermId gfa_a_1 = bank.makeTerm(sym_g, {{fa, a}}); + TermId gfa_a_2 = bank.makeTerm(sym_g, {{fa, a}}); + EXPECT_EQ(gfa_a_1, gfa_a_2); +} + +TEST_F(TermBankTest, GetTermReturnsCorrectSymbol) { + TermId a = bank.makeTerm(sym_a, {}); + const Term& t = bank.getTerm(a); + EXPECT_EQ(t.symbol_id, sym_a); + EXPECT_EQ(t.arity(), 0); +} + +TEST_F(TermBankTest, GetTermReturnsCorrectArgs) { + TermId a = bank.makeTerm(sym_a, {}); + TermId b = bank.makeTerm(sym_b, {}); + TermId gab = bank.makeTerm(sym_g, {{a, b}}); + + const Term& t = bank.getTerm(gab); + EXPECT_EQ(t.symbol_id, sym_g); + EXPECT_EQ(t.arity(), 2); + ASSERT_EQ(t.args.size(), 2); + EXPECT_EQ(t.args[0], a); + EXPECT_EQ(t.args[1], b); +} + +TEST_F(TermBankTest, MakeVarCreatesZeroArityTerm) { + TermId x = bank.makeVar(sym_X); + const Term& t = bank.getTerm(x); + EXPECT_EQ(t.symbol_id, sym_X); + EXPECT_EQ(t.arity(), 0); + EXPECT_TRUE(t.args.empty()); +} + +TEST_F(TermBankTest, IsVariableDistinguishesFromConstants) { + TermId x = bank.makeVar(sym_X); + TermId a = bank.makeTerm(sym_a, {}); + + EXPECT_TRUE(bank.isVariable(x)) << "Variable should be detected as variable"; + EXPECT_FALSE(bank.isVariable(a)) << "Constant should NOT be detected as variable"; +} + +TEST_F(TermBankTest, VariableHashConsing) { + TermId x1 = bank.makeVar(sym_X); + TermId x2 = bank.makeVar(sym_X); + EXPECT_EQ(x1, x2); + + TermId y = bank.makeVar(sym_Y); + EXPECT_NE(x1, y); +} + +TEST_F(TermBankTest, SizeTracksUniqueTerms) { + EXPECT_EQ(bank.size(), 0); + TermId a = bank.makeTerm(sym_a, {}); + EXPECT_EQ(bank.size(), 1); + bank.makeTerm(sym_a, {}); // duplicate + EXPECT_EQ(bank.size(), 1); + bank.makeTerm(sym_b, {}); + EXPECT_EQ(bank.size(), 2); + bank.makeTerm(sym_f, {{a}}); + EXPECT_EQ(bank.size(), 3); +} + +TEST_F(TermBankTest, CompoundTermWithVariableArgs) { + // f(X) — a function applied to a variable + TermId x = bank.makeVar(sym_X); + TermId fx = bank.makeTerm(sym_f, {{x}}); + + const Term& t = bank.getTerm(fx); + EXPECT_EQ(t.symbol_id, sym_f); + EXPECT_EQ(t.arity(), 1); + EXPECT_EQ(t.args[0], x); + + EXPECT_FALSE(bank.isVariable(fx)); + EXPECT_TRUE(bank.isVariable(x)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// ClauseStore Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(ClauseStoreTest, AddAndRetrieve) { + ClauseStore store; + Clause c; + c.literals.push_back(Literal{.atom = 0, .is_positive = true}); + c.literals.push_back(Literal{.atom = 1, .is_positive = false}); + + ClauseId id = store.addClause(std::move(c)); + EXPECT_EQ(id, 0); + + const Clause& retrieved = store.getClause(id); + EXPECT_EQ(retrieved.id, id); + EXPECT_EQ(retrieved.literals.size(), 2); + EXPECT_EQ(retrieved.literals[0].atom, 0); + EXPECT_TRUE(retrieved.literals[0].is_positive); + EXPECT_EQ(retrieved.literals[1].atom, 1); + EXPECT_FALSE(retrieved.literals[1].is_positive); +} + +TEST(ClauseStoreTest, AssignsSequentialIds) { + ClauseStore store; + ClauseId id0 = store.addClause(Clause{}); + ClauseId id1 = store.addClause(Clause{}); + ClauseId id2 = store.addClause(Clause{}); + EXPECT_EQ(id0, 0); + EXPECT_EQ(id1, 1); + EXPECT_EQ(id2, 2); + EXPECT_EQ(store.size(), 3); +} + +TEST(ClauseStoreTest, StampsClauseWithId) { + ClauseStore store; + Clause c; + c.id = kInvalidId; // unset + ClauseId id = store.addClause(std::move(c)); + EXPECT_EQ(store.getClause(id).id, id); +} + +TEST(ClauseStoreTest, MutableAccess) { + ClauseStore store; + Clause c; + c.depth = 0; + ClauseId id = store.addClause(std::move(c)); + + store.getMutableClause(id).depth = 42; + EXPECT_EQ(store.getClause(id).depth, 42); +} + +TEST(ClauseStoreTest, ForEachVisitsAll) { + ClauseStore store; + store.addClause(Clause{}); + store.addClause(Clause{}); + store.addClause(Clause{}); + + size_t count = 0; + store.forEach([&count](const Clause&) { count++; }); + EXPECT_EQ(count, 3); +} + +TEST(ClauseStoreTest, EmptyClauseDetection) { + Clause c; + EXPECT_TRUE(c.isEmpty()); + c.literals.push_back(Literal{.atom = 0, .is_positive = true}); + EXPECT_FALSE(c.isEmpty()); + EXPECT_EQ(c.size(), 1); +} + +TEST(ClauseStoreTest, ProvenancePreserved) { + ClauseStore store; + Clause c; + c.rule = InferenceRule::kResolution; + c.parent1 = 3; + c.parent2 = 7; + c.depth = 5; + + ClauseId id = store.addClause(std::move(c)); + const Clause& retrieved = store.getClause(id); + EXPECT_EQ(retrieved.rule, InferenceRule::kResolution); + EXPECT_EQ(retrieved.parent1, 3); + EXPECT_EQ(retrieved.parent2, 7); + EXPECT_EQ(retrieved.depth, 5); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Literal Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST(LiteralTest, Complement) { + Literal pos{.atom = 42, .is_positive = true}; + Literal neg = pos.complement(); + EXPECT_EQ(neg.atom, 42); + EXPECT_FALSE(neg.is_positive); + + Literal back = neg.complement(); + EXPECT_EQ(back, pos); +} + +TEST(LiteralTest, Equality) { + Literal a{.atom = 1, .is_positive = true}; + Literal b{.atom = 1, .is_positive = true}; + Literal c{.atom = 1, .is_positive = false}; + Literal d{.atom = 2, .is_positive = true}; + EXPECT_EQ(a, b); + EXPECT_NE(a, c); + EXPECT_NE(a, d); +} + +} // namespace +} // namespace atp -- cgit v1.2.3