From 31a3d01ef27c559bf7ff453ca60033478ac19ef8 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Thu, 2 Apr 2026 15:23:43 +0800 Subject: refactor: replace string-based formula representation with interned SymbolIds and introduce stateful Clausifier for TPTP parsing --- include/atp/frontend/tptp_parser.h | 74 +++++++++++++++++++++++++++++++------- 1 file changed, 62 insertions(+), 12 deletions(-) (limited to 'include/atp/frontend/tptp_parser.h') 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 . */ - #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; + std::string name; ///< Formula name (e.g., "axiom1") + FormulaRole role; ///< Semantic role + std::unique_ptr formula; ///< The FOL formula (for fof(...)) + std::vector 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 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 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 prepareForProving(ParsedProblem& problem, + TermBank& bank, SymbolTable& symbols); } // namespace atp -- cgit v1.2.3