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/normalize/clausifier.h | 37 ++++++++++++++++++++++++++++++++++--- 1 file changed, 34 insertions(+), 3 deletions(-) (limited to 'include/atp/normalize/clausifier.h') 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 . */ - #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 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 clausify(const Formula& formula); + + /// Negate a formula: wraps it in ¬(...) + /// Used to negate the conjecture before clausification. + [[nodiscard]] static std::unique_ptr negate(std::unique_ptr 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 -- cgit v1.2.3