diff options
Diffstat (limited to 'include')
| -rw-r--r-- | include/atp/core/literal.h | 2 | ||||
| -rw-r--r-- | include/atp/frontend/tptp_parser.h | 74 | ||||
| -rw-r--r-- | include/atp/normalize/clausifier.h | 37 | ||||
| -rw-r--r-- | include/atp/normalize/formula.h | 28 |
4 files changed, 117 insertions, 24 deletions
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); }; |