aboutsummaryrefslogtreecommitdiff
path: root/include/atp/core/term.h
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-03 02:46:12 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-03 02:46:12 +0800
commit9ab592ce3765d07b6dbdb9c1d9b62dc8045e784e (patch)
tree5b2bf93147980c5dabef80eff4c6209caa95f034 /include/atp/core/term.h
parent1e35f078fe5ace02b22e6f4ba89f57ba4a58b8c9 (diff)
downloadratp-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.h')
-rw-r--r--include/atp/core/term.h20
1 files changed, 11 insertions, 9 deletions
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