From 26da267b732e28e4d9697278e735b410e50e5e08 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Thu, 2 Apr 2026 04:10:53 +0800
Subject: Initial commit: Build project architecture, define interfaces, write
 documentation, with the help of Claude

---
 include/atp/core/symbol_table.h | 68 +++++++++++++++++++++++++++++++++++++++++
 1 file changed, 68 insertions(+)
 create mode 100644 include/atp/core/symbol_table.h

(limited to 'include/atp/core/symbol_table.h')

diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h
new file mode 100644
index 0000000..ed27a4d
--- /dev/null
+++ b/include/atp/core/symbol_table.h
@@ -0,0 +1,68 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+
+#pragma once
+
+/// @file symbol_table.h
+/// @brief Bidirectional mapping between symbol names and SymbolIds,
+///        with kind and sort metadata.
+
+#include <string>
+#include <string_view>
+
+#include "atp/core/types.h"
+
+namespace atp {
+
+/// Metadata associated with an interned symbol.
+struct SymbolInfo {
+    std::string name;
+    SymbolKind kind = SymbolKind::kFunction;
+    uint16_t arity = 0;
+    SortId sort = kUnsorted;  ///< Result sort (for sorted logic)
+};
+
+/// Interns symbol names so that each unique string is stored exactly once.
+/// Also tracks symbol metadata (kind, arity, sort).
+/// Thread-safety: NOT thread-safe (single-threaded prover design).
+class SymbolTable {
+  public:
+    SymbolTable() = default;
+
+    /// Intern a symbol name with metadata. Returns existing ID if already present.
+    SymbolId intern(std::string_view name, SymbolKind kind, uint16_t arity = 0,
+                    SortId sort = kUnsorted);
+
+    /// Look up the name for a given SymbolId. UB if id is out of range.
+    [[nodiscard]] std::string_view getName(SymbolId id) const;
+
+    /// Look up full metadata for a SymbolId.
+    [[nodiscard]] const SymbolInfo& getInfo(SymbolId id) const;
+
+    /// Check if a symbol is a variable.
+    [[nodiscard]] bool isVariable(SymbolId id) const;
+
+    /// Number of interned symbols.
+    [[nodiscard]] size_t size() const;
+
+  private:
+    // TODO: Phase 1 implementation
+};
+
+}  // namespace atp
-- 
cgit v1.2.3