aboutsummaryrefslogtreecommitdiff
diff options
context:
space:
mode:
Diffstat
-rw-r--r--include/atp/core/clause_store.h3
-rw-r--r--include/atp/core/symbol_table.h4
-rw-r--r--include/atp/core/term.h20
-rw-r--r--include/atp/core/term_bank.h38
-rw-r--r--src/core/clause_store.cc34
-rw-r--r--src/core/symbol_table.cc43
-rw-r--r--src/core/term_bank.cc37
-rw-r--r--tests/test_term_bank.cc316
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<void(const Clause&)>& visitor) const;
+ // function may have type erasure overhead, consider using a template
+ // template <typename Visitor>
+ // void forEach(Visitor&& visitor) const;
private:
std::vector<Clause> 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 <deque>
#include <string>
#include <string_view>
+#include <unordered_map>
#include "atp/core/types.h"
@@ -63,6 +65,8 @@ class SymbolTable {
private:
// TODO: Phase 1 implementation
+ std::deque<SymbolInfo> infos_;
+ std::unordered_map<std::string_view, SymbolId> 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 <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file term.h
/// @brief Core Term data structure — hash-consed, immutable.
+///
+/// V1 uses vector<TermId> for args.
+/// Future: flat arena with contiguous arg storage for cache locality.
-#include <span>
+#include <vector>
#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<TermId> args; ///< Argument sub-term IDs
- /// Access the argument TermIds (stored immediately after this struct in the arena).
- [[nodiscard]] std::span<const TermId> args() const;
- [[nodiscard]] std::span<TermId> mutableArgs();
+ /// Number of arguments.
+ [[nodiscard]] uint16_t arity() const {
+ return static_cast<uint16_t>(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 <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
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 <https://www.gnu.org/licenses/>.
*/
+#include "atp/core/clause_store.h"
+#include <cassert>
+#include <utility>
+namespace atp {
+
+ClauseId ClauseStore::addClause(Clause clause) {
+ auto new_id = static_cast<ClauseId>(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<void(const Clause&)>& 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 <https://www.gnu.org/licenses/>.
*/
+#include "atp/core/symbol_table.h"
+#include "atp/core/types.h"
+#include <cstddef>
+#include <stdexcept>
+#include <string_view>
+
+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<SymbolId>(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 <https://www.gnu.org/licenses/>.
*/
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include <cassert>
+namespace atp {
+
+TermId TermBank::makeTerm(SymbolId symbol, std::span<const TermId> 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<TermId>(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 <https://www.gnu.org/licenses/>.
*/
+#include <gtest/gtest.h>
+#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
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-29 03:05:32 +0000