refactor: replace string-based formula representation with interned SymbolIds and introduce stateful Clausifier for TPTP parsing

7 files changed, 416 insertions, 24 deletions

diff --git a/.gitignore b/.gitignore
index 7242ee6..2a1b7e2 100644
--- a/.gitignore
+++ b/.gitignore
@@ -1,6 +1,7 @@
 # Build
 build/
 cmake-build-*/
+.cache/
 compile_commands.json
 
 # IDE
diff --git a/data/monkey_banana.p b/data/monkey_banana.p
index e69de29..446c20a 100644
--- a/data/monkey_banana.p
+++ b/data/monkey_banana.p
@@ -0,0 +1,27 @@
+% ========================================================================= 
+% Monkey and Banana Problem 
+% State representation: state(Monkey, Box, Banana, Height, Situation) 
+% ========================================================================= 
+
+% 1. Initial state (corresponding sample input: A B C 0) 
+cnf(init_state, axiom, state(a, b, c, h0, s0)). 
+
+% 2. State transition axioms (action rules) 
+% Action: Go(X) 
+cnf(action_go, axiom, ~state(M, B, G, h0, S) | state(X, B, G, h0, do(go(X), S)) ). 
+
+% Action: Push(X) (Note M and B use the same variable M representing M=B) 
+cnf(action_push, axiom, ~state(M, M, G, h0, S) | state(X, X, G, h0, do(push(X), S)) ). 
+
+% Action: Climb() 
+cnf(action_climb, axiom, ~state(M, M, G, h0, S) | state(M, M, G, h1, do(climb, S)) ). 
+
+% Action: Down() 
+cnf(action_down, axiom, ~state(M, B, G, h1, S) | state(M, B, G, h0, do(down, S)) ). 
+
+% Action: Reach() (Note M, B, G all use G uniformly, representing M=G and B=G) 
+cnf(action_reach, axiom, ~state(G, G, G, h1, S) | goal_reached(do(reach, S)) ). 
+
+% 3. Goal theorem (using proof by contradiction) 
+% Goal: There exists a state S such that goal_reached(S) is true. 
+cnf(negated_goal, negated_conjecture, ~goal_reached(S) ).
\ No newline at end of file
diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h
index 1b4f65c..a3192a9 100644
--- a/include/atp/core/literal.h
+++ b/include/atp/core/literal.h
@@ -32,7 +32,7 @@ struct Literal {
     bool is_positive;    ///< true = positive, false = negated
 
     /// Complement: flip polarity, same atom.
-    [[nodiscard]] Literal complement() const { return {atom, !is_positive}; }
+    [[nodiscard]] Literal complement() const { return {.atom = atom, .is_positive = !is_positive}; }
 
     bool operator==(const Literal& other) const = default;
 };
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index f43f020..075b45e 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -16,13 +16,21 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file tptp_parser.h
-/// @brief Bridge from ANTLR4-generated parse tree to internal Formula AST.
+/// @brief TPTP format parser — converts .p files to internal representations.
+///
+/// The parser interns all symbols (predicates, functions, variables) into the
+/// SymbolTable and builds terms in the TermBank during parsing. This is the
+/// E Prover approach: parse and intern simultaneously, avoiding a separate
+/// resolution pass.
+///
+/// V1: Hand-written recursive descent for TPTP CNF/FOF subset.
+///     (ANTLR4 integration deferred — avoids build complexity for V1.)
 
 #include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
 #include "atp/core/term_bank.h"
 #include "atp/normalize/formula.h"
 
@@ -31,22 +39,64 @@
 
 namespace atp {
 
-/// Role of a TPTP formula (axiom, hypothesis, conjecture, etc.)
+/// Role of a TPTP formula.
+/// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html
 enum class FormulaRole : uint8_t {
-    kAxiom,
-    kHypothesis,
-    kConjecture,
-    kNegatedConjecture,
+    kAxiom,                ///< Background truth
+    kHypothesis,           ///< Problem-specific assumption
+    kDefinition,           ///< Symbol definition (can be unfolded)
+    kAssumption,           ///< Assumed for this proof attempt
+    kLemma,                ///< Derived intermediate result
+    kTheorem,              ///< Previously proved statement (used as axiom)
+    kConjecture,           ///< The statement to prove
+    kNegatedConjecture,    ///< Already negated conjecture (input was cnf)
+    kPlain,                ///< No semantic role specified
 };
 
+/// Map a TPTP role string to enum. Returns kPlain for unknown roles.
+FormulaRole parseRole(std::string_view role_str);
+
 /// A parsed TPTP formula with its name and role.
 struct AnnotatedFormula {
-    std::string name;
-    FormulaRole role;
-    std::unique_ptr<Formula> formula;
+    std::string name;                  ///< Formula name (e.g., "axiom1")
+    FormulaRole role;                  ///< Semantic role
+    std::unique_ptr<Formula> formula;  ///< The FOL formula (for fof(...))
+    std::vector<Clause> clauses;       ///< Direct clauses (for cnf(...))
+    bool is_cnf = false;               ///< true if input was cnf(), false if fof()
+};
+
+/// A complete parsed TPTP problem.
+struct ParsedProblem {
+    std::vector<AnnotatedFormula> formulas;
+
+    /// Does any formula contain an equality predicate?
+    bool has_equality = false;
+
+    /// Original file path (for error messages).
+    std::string source_file;
 };
 
-/// Parse a TPTP file and return the annotated formulas.
-std::vector<AnnotatedFormula> parseTptpFile(const std::string& filepath, TermBank& bank);
+/// Parse a TPTP file.
+///
+/// For `cnf(...)` entries: clauses are built directly (no clausification needed).
+/// For `fof(...)` entries: Formula AST is built (clausification happens later).
+///
+/// All symbols are interned into `symbols` and terms into `bank` during parsing.
+ParsedProblem parseTptpFile(const std::string& filepath,
+                            TermBank& bank, SymbolTable& symbols);
+
+/// Parse a TPTP string (for testing).
+ParsedProblem parseTptpString(const std::string& input,
+                              TermBank& bank, SymbolTable& symbols);
+
+/// Prepare a parsed problem for proving:
+///   1. Negate conjecture formulas.
+///   2. Clausify all fof() formulas.
+///   3. Collect all cnf() clauses directly.
+///   4. Assign ClauseIds and set provenance to kInput.
+///
+/// Returns the final clause set ready for the Prover.
+std::vector<Clause> prepareForProving(ParsedProblem& problem,
+                                      TermBank& bank, SymbolTable& symbols);
 
 }  // namespace atp
diff --git a/include/atp/normalize/clausifier.h b/include/atp/normalize/clausifier.h
index 1ff4d27..61d2505 100644
--- a/include/atp/normalize/clausifier.h
+++ b/include/atp/normalize/clausifier.h
@@ -16,15 +16,20 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file clausifier.h
 /// @brief Converts FOL formulas to Clause Normal Form (CNF).
 ///
+/// Clausifier is a stateful object because:
+///   1. Skolem function counter must be shared across all formulas in a problem
+///      (otherwise different formulas generate conflicting Skolem names).
+///   2. Variable renaming counter must be shared for the same reason.
+///
 /// Pipeline: eliminate ↔/→  →  NNF  →  Skolemize  →  distribute ∨ over ∧  →  flatten.
 
 #include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
 #include "atp/core/term_bank.h"
 #include "atp/normalize/formula.h"
 
@@ -32,7 +37,33 @@
 
 namespace atp {
 
-/// Convert a first-order formula into a set of clauses (CNF).
-std::vector<Clause> clausify(const Formula& formula, TermBank& bank);
+/// Stateful clausifier. Create one per proof problem.
+///
+/// Usage:
+///   Clausifier clausifier(bank, symbols);
+///   auto clauses1 = clausifier.clausify(formula1);
+///   auto clauses2 = clausifier.clausify(formula2);
+///   // Skolem IDs are unique across both calls.
+class Clausifier {
+  public:
+    Clausifier(TermBank& bank, SymbolTable& symbols);
+
+    /// Convert a single formula to CNF clauses.
+    /// Skolem functions generated here are globally unique (counter persists).
+    [[nodiscard]] std::vector<Clause> clausify(const Formula& formula);
+
+    /// Negate a formula: wraps it in ¬(...)
+    /// Used to negate the conjecture before clausification.
+    [[nodiscard]] static std::unique_ptr<Formula> negate(std::unique_ptr<Formula> formula);
+
+    /// Number of Skolem functions generated so far.
+    [[nodiscard]] uint32_t skolemCount() const { return next_skolem_id_; }
+
+  private:
+    TermBank& bank_;
+    SymbolTable& symbols_;
+    uint32_t next_skolem_id_ = 0;
+    uint32_t next_var_id_ = 0;  ///< For variable standardization apart
+};
 
 }  // namespace atp
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index ccf1302..2cd7900 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -16,16 +16,19 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file formula.h
 /// @brief First-order logic formula AST (pre-clausification).
+///
+/// Design decision: atoms use TermId (interned), quantifier variables use
+/// SymbolId (interned). The parser interns all symbols during parsing.
+/// This avoids string→ID lookups during clausification and ensures
+/// consistent variable identity across quantifier scopes.
 
 #include "atp/core/types.h"
 
 #include <memory>
-#include <string>
 #include <vector>
 
 namespace atp {
@@ -33,6 +36,7 @@ namespace atp {
 /// AST node types for first-order logic formulas.
 enum class FormulaKind : uint8_t {
     kAtom,       ///< Predicate application: P(t1, ..., tn)
+    kEquality,   ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
     kNot,        ///< Negation: ¬F
     kAnd,        ///< Conjunction: F ∧ G
     kOr,         ///< Disjunction: F ∨ G
@@ -43,19 +47,27 @@ enum class FormulaKind : uint8_t {
 };
 
 /// A first-order logic formula node.
+///
+/// All identifiers are interned: atoms as TermIds, quantifier variables as
+/// SymbolIds. No raw strings survive past the parser.
 struct Formula {
     FormulaKind kind;
 
-    // For kAtom: the predicate term
+    /// For kAtom / kEquality: the predicate/equality term, already interned.
     TermId atom = kInvalidId;
 
-    // For quantifiers: the bound variable name
-    std::string var_name;
+    /// For kForall / kExists: the bound variable, as an interned SymbolId.
+    /// Using SymbolId (not string) so the clausifier can map bound variables
+    /// back to term-bank variables without string lookups.
+    SymbolId bound_var = kInvalidId;
 
-    // Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives)
+    /// Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives).
     std::vector<std::unique_ptr<Formula>> children;
 
+    // ── Factory methods ──
+
     static std::unique_ptr<Formula> makeAtom(TermId atom);
+    static std::unique_ptr<Formula> makeEquality(TermId lhs, TermId rhs, TermId eq_atom);
     static std::unique_ptr<Formula> makeNot(std::unique_ptr<Formula> child);
     static std::unique_ptr<Formula> makeAnd(std::unique_ptr<Formula> lhs,
                                             std::unique_ptr<Formula> rhs);
@@ -65,9 +77,9 @@ struct Formula {
                                                 std::unique_ptr<Formula> rhs);
     static std::unique_ptr<Formula> makeIff(std::unique_ptr<Formula> lhs,
                                             std::unique_ptr<Formula> rhs);
-    static std::unique_ptr<Formula> makeForall(std::string var,
+    static std::unique_ptr<Formula> makeForall(SymbolId var,
                                                std::unique_ptr<Formula> body);
-    static std::unique_ptr<Formula> makeExists(std::string var,
+    static std::unique_ptr<Formula> makeExists(SymbolId var,
                                                std::unique_ptr<Formula> body);
 };
 
diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc
index b62ffd0..df8baeb 100644
--- a/src/frontend/tptp_parser.cc
+++ b/src/frontend/tptp_parser.cc
@@ -16,4 +16,275 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include "atp/frontend/tptp_parser.h"
+#include "atp/core/clause.h"
+#include "atp/core/literal.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include <cctype>
+#include <fstream>
+#include <stdexcept>
+#include <string>
+#include <string_view>
+#include <unordered_map>
+#include <vector>
 
+namespace atp {
+
+FormulaRole parseRole(std::string_view role_str){
+    if (role_str == "axiom") return FormulaRole::kAxiom;
+    if (role_str == "hypothesis") return FormulaRole::kHypothesis;
+    if (role_str == "definition") return FormulaRole::kDefinition;
+    if (role_str == "assumption") return FormulaRole::kAssumption;
+    if (role_str == "lemma") return FormulaRole::kLemma;
+    if (role_str == "theorem") return FormulaRole::kTheorem;
+    if (role_str == "conjecture") return FormulaRole::kConjecture;
+    if (role_str == "negated_conjecture") return FormulaRole::kNegatedConjecture;
+    if (role_str == "plain") return FormulaRole::kPlain;
+    return FormulaRole::kPlain;
+}
+
+
+enum class TokenType {
+    kWord,
+    kLParen,
+    kRParen,
+    kOr,
+    kNot,
+    kDot,
+    kComma,
+    kEOF,
+    kUnkown
+};
+
+struct Token {
+    TokenType type;
+    std::string_view value;
+    size_t line;
+    size_t column;
+};
+
+class TptpLexer {
+public:
+    explicit TptpLexer(std::string_view input) : source_(input) {}
+
+    Token next_token() {
+        skip_whitespace_and_comments();
+
+        if (pos_ >= source_.length()) {
+            return {.type = TokenType::kEOF, .value = "", .line = line_, .column = column_};
+        }
+
+        size_t start_pos = pos_;
+        [[maybe_unused]] size_t start_col = column_;
+        char c = source_[pos_];
+
+        if (std::isalpha(static_cast<unsigned char>(c)) || c == '_') {
+            while (pos_ < source_.size() && (std::isalnum(static_cast<unsigned char>(source_[pos_])) || source_[pos_] == '_')) {
+                advance_char();
+            }
+            return {.type = TokenType::kWord, .value = source_.substr(start_pos, pos_ - start_pos), .line = line_, .column = column_};
+        }
+
+        advance_char();
+        switch (c) {
+            case '(': return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_};
+            case ')': return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_};
+            case ',': return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_};
+            case '.': return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_};
+            case '~': return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_};
+            case '|': return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_};
+            default: return {.type = TokenType::kUnkown, .value = source_.substr(start_pos, 1), .line = line_, .column = column_};
+        }
+    }
+
+private:
+    std::string_view source_;
+    size_t pos_ = 0;
+    size_t line_ = 1;
+    size_t column_ = 1;
+
+    void advance_char() {
+        if (pos_ < source_.size()) {
+            if (source_[pos_] == '\n') {
+                line_++;
+                column_ = 1;
+            } else {
+                column_++;
+            }
+            pos_++;
+        }
+    }
+
+    void skip_whitespace_and_comments() {
+        while (pos_ < source_.size()) {
+            char c = source_[pos_];
+            if (std::isspace(static_cast<unsigned char>(c))) {
+                advance_char();
+            } else if (c == '%') {
+                while (pos_ < source_.size() && source_[pos_] != '\n') {
+                    advance_char();
+                }
+            } else {
+                break;
+            }
+        }
+    }
+};
+
+class TptpParser {
+public:
+    explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols) : lexer_(input), bank_(bank), symbols_(symbols) {
+        advance();
+    }
+
+    void parseProblem(ParsedProblem& problem) {
+        while (current_token_.type != TokenType::kEOF) {
+            if (current_token_.type == TokenType::kWord && current_token_.value == "cnf") {
+                advance();
+                expect(TokenType::kLParen);
+
+                AnnotatedFormula af;
+                af.is_cnf = true;
+                
+                af.name = std::string(current_token_.value);
+                expect(TokenType::kWord);
+                expect(TokenType::kComma);
+                
+                af.role = parseRole(current_token_.value);
+                expect(TokenType::kWord);
+                expect(TokenType::kComma);
+
+                Clause clause;
+                clause.literals.push_back(parseLiteral());
+                while (current_token_.type == TokenType::kOr) {
+                    advance();
+                    clause.literals.push_back(parseLiteral());
+                }
+                af.clauses.push_back(std::move(clause));
+
+                expect(TokenType::kRParen);
+                expect(TokenType::kDot);
+                problem.formulas.push_back(std::move(af));
+
+                variable_cache_.clear();
+            } else if (current_token_.value == "fof") {
+                throw std::runtime_error("FOF parsing not implemented. Line " + std::to_string(current_token_.line));
+            } else {
+                throw std::runtime_error("Unknown declaration: '" + std::string(current_token_.value) + "'");
+            }
+        }
+    }
+
+private:
+    TptpLexer lexer_;
+    TermBank& bank_;
+    SymbolTable& symbols_;
+    Token current_token_;
+
+    std::unordered_map<std::string_view, TermId> variable_cache_;
+
+    void advance() {
+        current_token_ = lexer_.next_token();
+    }
+
+    void expect(TokenType type) {
+        if (current_token_.type != type) {
+            throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line) + 
+                                     ", col " + std::to_string(current_token_.column) + 
+                                     ": unexpected token '" + std::string(current_token_.value) + "'");
+        }
+        advance();
+    }
+
+    TermId parseTerm() {
+        if (current_token_.type != TokenType::kWord) {
+            throw std::runtime_error("Expected variable or function name at line " + std::to_string(current_token_.line) + 
+                                     ", col " + std::to_string(current_token_.column) + 
+                                     ": unexpected token '" + std::string(current_token_.value) + "'");
+        }
+
+        std::string_view name = current_token_.value;
+        bool is_variable = std::isupper(static_cast<unsigned char>(name[0]));
+        advance();
+
+        if (is_variable) {
+            // Check cache first — same variable name in one clause → same TermId
+            auto it = variable_cache_.find(name);
+            if (it != variable_cache_.end()) {
+                return it->second;
+            }
+            SymbolId sym = symbols_.intern(name, SymbolKind::kVariable);
+            TermId var_id = bank_.makeVar(sym);
+            variable_cache_[name] = var_id;
+            return var_id;
+        } else {
+            // Check if this is a function/predicate (has args) or a constant (no parens)
+            if (current_token_.type == TokenType::kLParen) {
+                advance();  // consume '('
+                std::vector<TermId> args;
+                if (current_token_.type != TokenType::kRParen) {
+                    args.push_back(parseTerm());
+                    while (current_token_.type == TokenType::kComma) {
+                        advance();
+                        args.push_back(parseTerm());
+                    }
+                }
+                expect(TokenType::kRParen);
+                SymbolId sym = symbols_.intern(name, SymbolKind::kFunction,
+                                               static_cast<uint16_t>(args.size()));
+                return bank_.makeTerm(sym, args);
+            } else {
+                // Constant: no parentheses (e.g., a, b, h0, s0)
+                SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
+                return bank_.makeTerm(sym, {});
+            }
+        }
+    }
+
+    Literal parseLiteral() {
+        bool is_positive = true;
+        if (current_token_.type == TokenType::kNot) {
+            is_positive = false;
+            advance();
+        }
+        TermId term = parseTerm();
+        return Literal{.atom = term, .is_positive = is_positive};
+    }
+};
+
+ParsedProblem parseTptpString(const std::string &input, TermBank &bank, SymbolTable &symbols){
+    ParsedProblem problem;
+    TptpParser parser(input, bank, symbols);
+    parser.parseProblem(problem);
+    return problem;
+}
+
+ParsedProblem parseTptpFile(const std::string &filename, TermBank &bank, SymbolTable &symbols){
+    std::ifstream file(filename, std::ios::binary);
+    if (!file.is_open()) {
+        throw std::runtime_error("Failed to open file: " + filename);
+    }
+    std::string content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
+    ParsedProblem problem = parseTptpString(content, bank, symbols);
+    problem.source_file = filename;
+    return problem;
+}
+
+std::vector<Clause> prepareForProving(ParsedProblem &problem, TermBank &bank, SymbolTable &symbols){
+    std::vector<Clause> final_clauses;
+
+    for (auto& af : problem.formulas){
+        if (af.is_cnf){
+            for (auto& clause : af.clauses){
+                clause.rule = InferenceRule::kInput;
+                clause.parent1 = kInvalidId;
+                clause.parent2 = kInvalidId;
+                final_clauses.push_back(std::move(clause));
+            }
+        }
+    }
+    return final_clauses;
+}
+
+} // namespace atp