From bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 05:21:26 +0800 Subject: style: reformat codebase with consistent indentation --- include/atp/core/clause.h | 5 ++--- include/atp/core/clause_store.h | 1 - include/atp/core/literal.h | 5 ++--- include/atp/core/symbol_table.h | 5 ++--- include/atp/core/term.h | 12 +++++------- include/atp/core/types.h | 23 +++++++++++------------ include/atp/frontend/tptp_parser.h | 27 ++++++++++++--------------- include/atp/index/discrim_tree.h | 1 - include/atp/infer/resolution.h | 13 ++++--------- include/atp/infer/unification.h | 1 - include/atp/normalize/formula.h | 24 +++++++++++------------- include/atp/proof/proof_trace.h | 4 ++-- include/atp/rewrite/ordering.h | 12 +++++------- include/atp/rewrite/paramodulation.h | 1 - include/atp/search/clause_queue.h | 1 - include/atp/search/prover.h | 7 +++---- include/atp/simplify/subsumption.h | 1 - include/atp/simplify/tautology.h | 1 - include/atp/strategy/calculus.h | 1 - include/atp/strategy/inference_rule.h | 11 +++++------ include/atp/strategy/problem_analyzer.h | 7 +++---- include/atp/utils/hash_utils.h | 1 - include/atp/utils/logger.h | 16 +++++++--------- 23 files changed, 74 insertions(+), 106 deletions(-) (limited to 'include') diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h index b4d3e68..7e0cbff 100644 --- a/include/atp/core/clause.h +++ b/include/atp/core/clause.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file clause.h @@ -25,11 +24,11 @@ /// NOTE: V1 uses std::vector for simplicity. /// Future optimization: migrate to a Clause Arena with contiguous storage. -#include - #include "atp/core/literal.h" #include "atp/core/types.h" +#include + namespace atp { /// A clause: a disjunction of literals plus provenance for proof reconstruction. diff --git a/include/atp/core/clause_store.h b/include/atp/core/clause_store.h index 23db996..5d6562a 100644 --- a/include/atp/core/clause_store.h +++ b/include/atp/core/clause_store.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file clause_store.h diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h index a3192a9..212c281 100644 --- a/include/atp/core/literal.h +++ b/include/atp/core/literal.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file literal.h @@ -28,8 +27,8 @@ namespace atp { /// A literal: a polarity flag plus the TermId of the atom. struct Literal { - TermId atom; ///< TermId of the predicate application - bool is_positive; ///< true = positive, false = negated + TermId atom; ///< TermId of the predicate application + bool is_positive; ///< true = positive, false = negated /// Complement: flip polarity, same atom. [[nodiscard]] Literal complement() const { return {.atom = atom, .is_positive = !is_positive}; } diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h index 856c395..30453fc 100644 --- a/include/atp/core/symbol_table.h +++ b/include/atp/core/symbol_table.h @@ -16,20 +16,19 @@ * along with this program. If not, see . */ - #pragma once /// @file symbol_table.h /// @brief Bidirectional mapping between symbol names and SymbolIds, /// with kind and sort metadata. +#include "atp/core/types.h" + #include #include #include #include -#include "atp/core/types.h" - namespace atp { /// Metadata associated with an interned symbol. diff --git a/include/atp/core/term.h b/include/atp/core/term.h index 017882a..2be01e7 100644 --- a/include/atp/core/term.h +++ b/include/atp/core/term.h @@ -24,22 +24,20 @@ /// V1 uses vector for args. /// Future: flat arena with contiguous arg storage for cache locality. -#include - #include "atp/core/types.h" +#include + namespace atp { /// A term is a function/predicate application: f(t1, t2, ..., tn). /// Variables are 0-arity terms whose symbol has SymbolKind::kVariable. struct Term { - SymbolId symbol_id; ///< Index into the SymbolTable - std::vector args; ///< Argument sub-term IDs + SymbolId symbol_id; ///< Index into the SymbolTable + std::vector args; ///< Argument sub-term IDs /// Number of arguments. - [[nodiscard]] uint16_t arity() const { - return static_cast(args.size()); - } + [[nodiscard]] uint16_t arity() const { return static_cast(args.size()); } }; } // namespace atp diff --git a/include/atp/core/types.h b/include/atp/core/types.h index c68e716..23f2322 100644 --- a/include/atp/core/types.h +++ b/include/atp/core/types.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file types.h @@ -57,24 +56,24 @@ enum class SymbolKind : uint8_t { /// Deliberately uses uint16_t for extensibility toward algebra/analysis rules. enum class InferenceRule : uint16_t { // ── Core resolution rules ── - kInput = 0, ///< Original input clause (axiom / negated conjecture) - kResolution = 1, ///< Binary resolution - kFactoring = 2, ///< Factoring + kInput = 0, ///< Original input clause (axiom / negated conjecture) + kResolution = 1, ///< Binary resolution + kFactoring = 2, ///< Factoring // ── Equality rules (algebra) ── - kParamodulation = 100, ///< Paramodulation (equality resolution) - kDemodulation = 101, ///< Demodulation (simplification by rewriting) - kEqualityResolution = 102, ///< s != t resolved with unifier - kEqualityFactoring = 103, ///< Factoring with equality + kParamodulation = 100, ///< Paramodulation (equality resolution) + kDemodulation = 101, ///< Demodulation (simplification by rewriting) + kEqualityResolution = 102, ///< s != t resolved with unifier + kEqualityFactoring = 103, ///< Factoring with equality // ── Simplification rules ── - kSubsumption = 200, ///< Removed by subsumption - kTautologyElim = 201, ///< Removed as tautology - kPureLiteralElim = 202, ///< Pure literal elimination + kSubsumption = 200, ///< Removed by subsumption + kTautologyElim = 201, ///< Removed as tautology + kPureLiteralElim = 202, ///< Pure literal elimination // ── Theory rules (analysis, arithmetic) ── kTheoryResolution = 300, ///< Theory-specific resolution - kTheoryRewrite = 301, ///< Theory-driven rewriting + kTheoryRewrite = 301, ///< Theory-driven rewriting }; } // namespace atp diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h index 075b45e..738d34b 100644 --- a/include/atp/frontend/tptp_parser.h +++ b/include/atp/frontend/tptp_parser.h @@ -42,15 +42,15 @@ namespace atp { /// Role of a TPTP formula. /// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html enum class FormulaRole : uint8_t { - 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 + 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. @@ -82,12 +82,10 @@ struct ParsedProblem { /// 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); +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); +ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols); /// Prepare a parsed problem for proving: /// 1. Negate conjecture formulas. @@ -96,7 +94,6 @@ ParsedProblem parseTptpString(const std::string& input, /// 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); +std::vector prepareForProving(ParsedProblem& problem, TermBank& bank, SymbolTable& symbols); } // namespace atp diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h index 8cadaa6..c5954d7 100644 --- a/include/atp/index/discrim_tree.h +++ b/include/atp/index/discrim_tree.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file discrim_tree.h diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h index df9cab3..6e2954d 100644 --- a/include/atp/infer/resolution.h +++ b/include/atp/infer/resolution.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file resolution.h @@ -24,32 +23,28 @@ #include "atp/core/clause.h" #include "atp/core/term_bank.h" +#include "atp/infer/unification.h" #include #include -#include "atp/infer/unification.h" - namespace atp { /// Attempt binary resolution between two clauses on the specified literal indices. /// @return The resolvent clause if resolution succeeds, std::nullopt otherwise. -std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, - const Clause& c2, size_t lit_idx2, - const UnificationConfig& uconfig = {}); +std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, + size_t lit_idx2, const UnificationConfig& uconfig = {}); /// Generate all possible resolvents between two clauses. std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, const UnificationConfig& uconfig = {}); /// Attempt factoring on a single clause (merge two unifiable literals). -std::vector factor(TermBank& bank, const Clause& c, - const UnificationConfig& uconfig = {}); +std::vector factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {}); /// Rename all variables in a clause to fresh ones, avoiding conflicts /// with variables already in the bank. Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, uint32_t& next_var_id); - } // namespace atp diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h index f2ea180..9a4b6cc 100644 --- a/include/atp/infer/unification.h +++ b/include/atp/infer/unification.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file unification.h diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h index 2cd7900..1bcc021 100644 --- a/include/atp/normalize/formula.h +++ b/include/atp/normalize/formula.h @@ -35,15 +35,15 @@ 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 - kImplies, ///< Implication: F → G - kIff, ///< Biconditional: F ↔ G - kForall, ///< Universal: ∀x. F - kExists, ///< Existential: ∃x. F + 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 + kImplies, ///< Implication: F → G + kIff, ///< Biconditional: F ↔ G + kForall, ///< Universal: ∀x. F + kExists, ///< Existential: ∃x. F }; /// A first-order logic formula node. @@ -77,10 +77,8 @@ struct Formula { std::unique_ptr rhs); static std::unique_ptr makeIff(std::unique_ptr lhs, std::unique_ptr rhs); - static std::unique_ptr makeForall(SymbolId var, - std::unique_ptr body); - static std::unique_ptr makeExists(SymbolId var, - std::unique_ptr body); + static std::unique_ptr makeForall(SymbolId var, std::unique_ptr body); + static std::unique_ptr makeExists(SymbolId var, std::unique_ptr body); }; } // namespace atp diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h index a80a327..28099fe 100644 --- a/include/atp/proof/proof_trace.h +++ b/include/atp/proof/proof_trace.h @@ -49,7 +49,7 @@ std::string termToString(TermId id, const TermBank& bank); std::string clauseToString(const Clause& clause, const TermBank& bank); /// Format a proof as a human-readable string. -std::string formatProof(const std::vector& proof, - const ClauseStore& store, const TermBank& bank); +std::string formatProof(const std::vector& proof, const ClauseStore& store, + const TermBank& bank); } // namespace atp diff --git a/include/atp/rewrite/ordering.h b/include/atp/rewrite/ordering.h index 5696766..195c3c6 100644 --- a/include/atp/rewrite/ordering.h +++ b/include/atp/rewrite/ordering.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file ordering.h @@ -34,10 +33,10 @@ namespace atp { /// Ordering comparison result. enum class OrderResult : uint8_t { - kLessThan, ///< t1 < t2 - kEqual, ///< t1 = t2 - kGreaterThan, ///< t1 > t2 - kIncomparable, ///< t1 and t2 are incomparable + kLessThan, ///< t1 < t2 + kEqual, ///< t1 = t2 + kGreaterThan, ///< t1 > t2 + kIncomparable, ///< t1 and t2 are incomparable }; /// Abstract base for term orderings. @@ -47,8 +46,7 @@ class TermOrdering { virtual ~TermOrdering() = default; /// Compare two terms under the ordering. - [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, - TermId t2) const = 0; + [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, TermId t2) const = 0; }; } // namespace atp diff --git a/include/atp/rewrite/paramodulation.h b/include/atp/rewrite/paramodulation.h index f43cd7b..9dfbd66 100644 --- a/include/atp/rewrite/paramodulation.h +++ b/include/atp/rewrite/paramodulation.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file paramodulation.h diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h index 828a725..6a8f9fc 100644 --- a/include/atp/search/clause_queue.h +++ b/include/atp/search/clause_queue.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file clause_queue.h diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h index d84a647..6ee22f0 100644 --- a/include/atp/search/prover.h +++ b/include/atp/search/prover.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file prover.h @@ -39,9 +38,9 @@ namespace atp { /// Result of a proof attempt. enum class ProverResult : uint8_t { - kTheorem, ///< Empty clause derived — conjecture is a theorem - kSaturation, ///< Search space saturated — cannot prove - kTimeout, ///< Resource limit exceeded + kTheorem, ///< Empty clause derived — conjecture is a theorem + kSaturation, ///< Search space saturated — cannot prove + kTimeout, ///< Resource limit exceeded }; /// V1 configuration — simple and direct. diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h index c39b586..970b6d8 100644 --- a/include/atp/simplify/subsumption.h +++ b/include/atp/simplify/subsumption.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file subsumption.h diff --git a/include/atp/simplify/tautology.h b/include/atp/simplify/tautology.h index 80aa1f9..f17f0c7 100644 --- a/include/atp/simplify/tautology.h +++ b/include/atp/simplify/tautology.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file tautology.h diff --git a/include/atp/strategy/calculus.h b/include/atp/strategy/calculus.h index ee8ee09..e06988e 100644 --- a/include/atp/strategy/calculus.h +++ b/include/atp/strategy/calculus.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file calculus.h diff --git a/include/atp/strategy/inference_rule.h b/include/atp/strategy/inference_rule.h index 1c7dbba..88b6fe0 100644 --- a/include/atp/strategy/inference_rule.h +++ b/include/atp/strategy/inference_rule.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file inference_rule.h @@ -62,9 +61,10 @@ class GeneratingRule : public InferenceRuleBase { /// @param processed All previously processed clauses (accessed via store). /// @param bank The global term bank. /// @return Newly generated clauses (not yet added to the store). - [[nodiscard]] virtual std::vector generate( - const Clause& given, const std::vector& processed, - const ClauseStore& store, TermBank& bank) const = 0; + [[nodiscard]] virtual std::vector generate(const Clause& given, + const std::vector& processed, + const ClauseStore& store, + TermBank& bank) const = 0; }; /// Simplifying inference rule: rewrite or delete a clause in-place. @@ -74,8 +74,7 @@ class SimplifyingRule : public InferenceRuleBase { /// Attempt to simplify a clause. Returns true if the clause was modified. /// If the clause should be deleted entirely, clear its literals. - virtual bool simplify(Clause& clause, const ClauseStore& store, - TermBank& bank) const = 0; + virtual bool simplify(Clause& clause, const ClauseStore& store, TermBank& bank) const = 0; }; } // namespace atp diff --git a/include/atp/strategy/problem_analyzer.h b/include/atp/strategy/problem_analyzer.h index b5fdef4..5e6c5cf 100644 --- a/include/atp/strategy/problem_analyzer.h +++ b/include/atp/strategy/problem_analyzer.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file problem_analyzer.h @@ -41,10 +40,10 @@ namespace atp { /// Features detected in the input problem. struct ProblemFeatures { - bool has_equality = false; ///< Contains '=' predicate + bool has_equality = false; ///< Contains '=' predicate bool is_purely_propositional = false; ///< No function symbols, no variables - bool is_horn = false; ///< All clauses are Horn clauses - bool has_existential = false; ///< Had existential quantifiers (Skolemized) + bool is_horn = false; ///< All clauses are Horn clauses + bool has_existential = false; ///< Had existential quantifiers (Skolemized) size_t num_clauses = 0; size_t num_predicates = 0; size_t num_functions = 0; diff --git a/include/atp/utils/hash_utils.h b/include/atp/utils/hash_utils.h index 4531fa6..ae31f43 100644 --- a/include/atp/utils/hash_utils.h +++ b/include/atp/utils/hash_utils.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file hash_utils.h diff --git a/include/atp/utils/logger.h b/include/atp/utils/logger.h index 95d3dd2..de77c54 100644 --- a/include/atp/utils/logger.h +++ b/include/atp/utils/logger.h @@ -16,7 +16,6 @@ * along with this program. If not, see . */ - #pragma once /// @file logger.h @@ -28,16 +27,15 @@ #define ATP_LOG_LEVEL 2 // 0=TRACE, 1=DEBUG, 2=INFO, 3=WARN, 4=ERROR #endif -#define ATP_LOG(level, level_str, fmt, ...) \ - do { \ - if constexpr (level >= ATP_LOG_LEVEL) { \ - std::fprintf(stderr, "[%s] " fmt "\n", level_str, \ - ##__VA_ARGS__); \ - } \ +#define ATP_LOG(level, level_str, fmt, ...) \ + do { \ + if constexpr (level >= ATP_LOG_LEVEL) { \ + std::fprintf(stderr, "[%s] " fmt "\n", level_str, ##__VA_ARGS__); \ + } \ } while (0) #define ATP_TRACE(fmt, ...) ATP_LOG(0, "TRACE", fmt, ##__VA_ARGS__) #define ATP_DEBUG(fmt, ...) ATP_LOG(1, "DEBUG", fmt, ##__VA_ARGS__) -#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__) -#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__) +#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__) +#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__) #define ATP_ERROR(fmt, ...) ATP_LOG(4, "ERROR", fmt, ##__VA_ARGS__) -- cgit v1.2.3