From 5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Tue, 7 Apr 2026 03:59:58 +0800 Subject: refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components --- src/core/clause_store.cc | 7 +- src/core/symbol_table.cc | 17 ++-- src/core/term_bank.cc | 11 ++- src/frontend/tptp_parser.cc | 198 ++++++++++++++++++++++++-------------------- src/infer/resolution.cc | 84 ++++++++++--------- src/infer/substitution.cc | 12 +-- src/infer/unification.cc | 19 +++-- src/main.cc | 20 +++-- src/proof/proof_trace.cc | 114 +++++++++++++------------ src/search/prover.cc | 42 ++++++---- src/simplify/subsumption.cc | 8 +- src/simplify/tautology.cc | 6 +- 12 files changed, 297 insertions(+), 241 deletions(-) (limited to 'src') diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc index 75959c3..f8ee73d 100644 --- a/src/core/clause_store.cc +++ b/src/core/clause_store.cc @@ -18,14 +18,19 @@ #include "atp/core/clause_store.h" +#include "atp/core/clause.h" +#include "atp/core/types.h" + #include +#include +#include #include namespace atp { ClauseId ClauseStore::addClause(Clause clause) { auto new_id = static_cast(clauses_.size()); - clause.id = new_id; + clause.id_ = new_id; clauses_.push_back(std::move(clause)); return new_id; } diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc index 42c7dd8..b707132 100644 --- a/src/core/symbol_table.cc +++ b/src/core/symbol_table.cc @@ -21,7 +21,9 @@ #include "atp/core/types.h" #include +#include #include +#include #include namespace atp { @@ -29,22 +31,23 @@ namespace atp { SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, SortId sort) { auto it = name_to_id_.find(name); if (it != name_to_id_.end()) { - SymbolId id = it->second; - SymbolInfo& info = infos_[id]; - if (info.kind != kind || info.arity != arity) { + SymbolId const id = it->second; + SymbolInfo const& info = infos_[id]; + if (info.kind_ != kind || info.arity_ != arity) { throw std::runtime_error("Symbol kind or arity mismatch for: " + std::string(name)); } return id; } auto new_id = static_cast(infos_.size()); - infos_.push_back({.name = std::string(name), .kind = kind, .arity = arity, .sort = sort}); - std::string_view stable_name_view = infos_.back().name; + infos_.push_back(SymbolInfo{ + .name_ = std::string(name), .kind_ = kind, .arity_ = arity, .sort_ = sort}); + std::string_view const stable_name_view = infos_.back().name_; name_to_id_.emplace(stable_name_view, new_id); return new_id; } std::string_view SymbolTable::getName(SymbolId id) const { - return infos_[id].name; + return infos_[id].name_; } const SymbolInfo& SymbolTable::getInfo(SymbolId id) const { @@ -52,7 +55,7 @@ const SymbolInfo& SymbolTable::getInfo(SymbolId id) const { } bool SymbolTable::isVariable(SymbolId id) const { - return infos_[id].kind == SymbolKind::kVariable; + return infos_[id].kind_ == SymbolKind::kVariable; } size_t SymbolTable::size() const { diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc index 8c8ef29..2e117b3 100644 --- a/src/core/term_bank.cc +++ b/src/core/term_bank.cc @@ -18,20 +18,25 @@ #include "atp/core/term_bank.h" +#include "atp/core/term.h" #include "atp/core/types.h" #include +#include +#include +#include +#include namespace atp { TermId TermBank::makeTerm(SymbolId symbol, std::span args) { - TermKey key{.symbol = symbol, .args = {args.begin(), args.end()}}; + TermKey key{.symbol_ = symbol, .args_ = {args.begin(), args.end()}}; auto it = term_to_id_.find(key); if (it != term_to_id_.end()) { return it->second; } auto new_id = static_cast(terms_.size()); - Term new_term{.symbol_id = symbol, .args = {args.begin(), args.end()}}; + Term new_term{.symbol_id_ = symbol, .args_ = key.args_}; terms_.push_back(std::move(new_term)); term_to_id_.emplace(std::move(key), new_id); return new_id; @@ -48,7 +53,7 @@ const Term& TermBank::getTerm(TermId id) const { bool TermBank::isVariable(TermId id) const { assert(id < terms_.size() && "TermId out of bounds!"); - return symbols_.isVariable(terms_[id].symbol_id); + return symbols_.isVariable(terms_[id].symbol_id_); } size_t TermBank::size() const { diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc index 2f32522..ddf8aad 100644 --- a/src/frontend/tptp_parser.cc +++ b/src/frontend/tptp_parser.cc @@ -20,96 +20,111 @@ #include "atp/core/clause.h" #include "atp/core/literal.h" +#include "atp/core/symbol_table.h" #include "atp/core/term_bank.h" #include "atp/core/types.h" #include +#include +#include #include +#include +#include #include #include #include #include +#include #include namespace atp { FormulaRole parseRole(std::string_view role_str) { - if (role_str == "axiom") + if (role_str == "axiom") { return FormulaRole::kAxiom; - if (role_str == "hypothesis") +} + if (role_str == "hypothesis") { return FormulaRole::kHypothesis; - if (role_str == "definition") +} + if (role_str == "definition") { return FormulaRole::kDefinition; - if (role_str == "assumption") +} + if (role_str == "assumption") { return FormulaRole::kAssumption; - if (role_str == "lemma") +} + if (role_str == "lemma") { return FormulaRole::kLemma; - if (role_str == "theorem") +} + if (role_str == "theorem") { return FormulaRole::kTheorem; - if (role_str == "conjecture") +} + if (role_str == "conjecture") { return FormulaRole::kConjecture; - if (role_str == "negated_conjecture") +} + if (role_str == "negated_conjecture") { return FormulaRole::kNegatedConjecture; - if (role_str == "plain") +} + if (role_str == "plain") { return FormulaRole::kPlain; +} return FormulaRole::kPlain; } -enum class TokenType { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown }; +enum class TokenType : std::uint8_t { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown }; struct Token { - TokenType type; - std::string_view value; - size_t line; - size_t column; + 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(); + Token nextToken() { + skipWhitespaceAndComments(); if (pos_ >= source_.length()) { - return {.type = TokenType::kEOF, .value = "", .line = line_, .column = column_}; + 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_]; + size_t const start_pos = pos_; + [[maybe_unused]] size_t const start_col = column_; + char const c = source_[pos_]; - if (std::isalpha(static_cast(c)) || c == '_') { + if ((std::isalpha(static_cast(c)) != 0) || c == '_') { while ( pos_ < source_.size() && - (std::isalnum(static_cast(source_[pos_])) || source_[pos_] == '_')) { - advance_char(); + ((std::isalnum(static_cast(source_[pos_])) != 0) || source_[pos_] == '_')) { + advanceChar(); } - return {.type = TokenType::kWord, - .value = source_.substr(start_pos, pos_ - start_pos), - .line = line_, - .column = column_}; + return {.type_ = TokenType::kWord, + .value_ = source_.substr(start_pos, pos_ - start_pos), + .line_ = line_, + .column_ = column_}; } - advance_char(); + advanceChar(); switch (c) { case '(': - return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_}; + return {.type_ = TokenType::kLParen, .value_ = "(", .line_ = line_, .column_ = column_}; case ')': - return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_}; + return {.type_ = TokenType::kRParen, .value_ = ")", .line_ = line_, .column_ = column_}; case ',': - return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_}; + return {.type_ = TokenType::kComma, .value_ = ",", .line_ = line_, .column_ = column_}; case '.': - return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_}; + return {.type_ = TokenType::kDot, .value_ = ".", .line_ = line_, .column_ = column_}; case '~': - return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_}; + return {.type_ = TokenType::kNot, .value_ = "~", .line_ = line_, .column_ = column_}; case '|': - return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_}; + return {.type_ = TokenType::kOr, .value_ = "|", .line_ = line_, .column_ = column_}; default: - return {.type = TokenType::kUnkown, - .value = source_.substr(start_pos, 1), - .line = line_, - .column = column_}; + return {.type_ = TokenType::kUnkown, + .value_ = source_.substr(start_pos, 1), + .line_ = line_, + .column_ = column_}; } } @@ -119,7 +134,7 @@ class TptpLexer { size_t line_ = 1; size_t column_ = 1; - void advance_char() { + void advanceChar() { if (pos_ < source_.size()) { if (source_[pos_] == '\n') { line_++; @@ -131,14 +146,14 @@ class TptpLexer { } } - void skip_whitespace_and_comments() { + void skipWhitespaceAndComments() { while (pos_ < source_.size()) { - char c = source_[pos_]; - if (std::isspace(static_cast(c))) { - advance_char(); + char const c = source_[pos_]; + if (std::isspace(static_cast(c)) != 0) { + advanceChar(); } else if (c == '%') { while (pos_ < source_.size() && source_[pos_] != '\n') { - advance_char(); + advanceChar(); } } else { break; @@ -155,41 +170,41 @@ class TptpParser { } void parseProblem(ParsedProblem& problem) { - while (current_token_.type != TokenType::kEOF) { - if (current_token_.type == TokenType::kWord && current_token_.value == "cnf") { + 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.is_cnf_ = true; - af.name = std::string(current_token_.value); + af.name_ = std::string(current_token_.value_); expect(TokenType::kWord); expect(TokenType::kComma); - af.role = parseRole(current_token_.value); + 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) { + clause.literals_.push_back(parseLiteral()); + while (current_token_.type_ == TokenType::kOr) { advance(); - clause.literals.push_back(parseLiteral()); + clause.literals_.push_back(parseLiteral()); } - af.clauses.push_back(std::move(clause)); + af.clauses_.push_back(std::move(clause)); expect(TokenType::kRParen); expect(TokenType::kDot); - problem.formulas.push_back(std::move(af)); + problem.formulas_.push_back(std::move(af)); variable_cache_.clear(); - } else if (current_token_.value == "fof") { + } else if (current_token_.value_ == "fof") { throw std::runtime_error("FOF parsing not implemented. Line " + - std::to_string(current_token_.line)); + std::to_string(current_token_.line_)); } else { throw std::runtime_error("Unknown declaration: '" + - std::string(current_token_.value) + "'"); + std::string(current_token_.value_) + "'"); } } } @@ -198,33 +213,33 @@ class TptpParser { TptpLexer lexer_; TermBank& bank_; SymbolTable& symbols_; - Token current_token_; + Token current_token_{}; + std::vector tokens_; + std::unordered_map variable_cache_{}; - std::unordered_map variable_cache_; - - void advance() { current_token_ = lexer_.next_token(); } + void advance() { current_token_ = lexer_.nextToken(); } 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) + + 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) { + 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::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(name[0])); + std::string_view const name = current_token_.value_; + bool const is_variable = std::isupper(static_cast(name[0])) != 0; advance(); if (is_variable) { @@ -233,18 +248,17 @@ class TptpParser { if (it != variable_cache_.end()) { return it->second; } - SymbolId sym = symbols_.intern(name, SymbolKind::kVariable); - TermId var_id = bank_.makeVar(sym); + SymbolId const sym = symbols_.intern(name, SymbolKind::kVariable); + TermId const 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) { + } // Check if this is a function/predicate (has args) or a constant (no parens) + if (current_token_.type_ == TokenType::kLParen) { advance(); // consume '(' std::vector args; - if (current_token_.type != TokenType::kRParen) { + if (current_token_.type_ != TokenType::kRParen) { args.push_back(parseTerm()); - while (current_token_.type == TokenType::kComma) { + while (current_token_.type_ == TokenType::kComma) { advance(); args.push_back(parseTerm()); } @@ -258,17 +272,17 @@ class TptpParser { SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0); return bank_.makeTerm(sym, {}); } - } + } Literal parseLiteral() { bool is_positive = true; - if (current_token_.type == TokenType::kNot) { + if (current_token_.type_ == TokenType::kNot) { is_positive = false; advance(); } - TermId term = parseTerm(); - return Literal{.atom = term, .is_positive = is_positive}; + TermId const term = parseTerm(); + return Literal{.atom_ = term, .is_positive_ = is_positive}; } }; @@ -284,22 +298,22 @@ ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolT if (!file.is_open()) { throw std::runtime_error("Failed to open file: " + filename); } - std::string content((std::istreambuf_iterator(file)), std::istreambuf_iterator()); + std::string const content((std::istreambuf_iterator(file)), std::istreambuf_iterator()); ParsedProblem problem = parseTptpString(content, bank, symbols); - problem.source_file = filename; + problem.source_file_ = filename; return problem; } -std::vector prepareForProving(ParsedProblem& problem, TermBank& bank, - SymbolTable& symbols) { +std::vector prepareForProving(ParsedProblem& problem, TermBank& /*bank*/, + SymbolTable& /*symbols*/) { std::vector 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; + 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)); } } diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc index f072b8e..82e59b7 100644 --- a/src/infer/resolution.cc +++ b/src/infer/resolution.cc @@ -26,8 +26,12 @@ #include "atp/infer/substitution.h" #include "atp/infer/unification.h" +#include +#include +#include #include #include +#include #include namespace atp { @@ -42,7 +46,7 @@ void collectVariables(TermId term, const TermBank& bank, std::unordered_map var_set; - for (const auto& lit : c.literals) { - collectVariables(lit.atom, bank, var_set); + for (const auto& lit : c.literals_) { + collectVariables(lit.atom_, bank, var_set); } if (var_set.empty()) { @@ -64,22 +68,22 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, // 2. Create fresh variables and build a substitution Substitution rename_subst; for (auto& [old_var_id, _] : var_set) { - std::string fresh_name = "_R" + std::to_string(next_var_id++); - SymbolId fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable); - TermId fresh_var = bank.makeVar(fresh_sym); + std::string const fresh_name = "_R" + std::to_string(next_var_id++); + SymbolId const fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable); + TermId const fresh_var = bank.makeVar(fresh_sym); rename_subst.bind(old_var_id, fresh_var); } // 3. Apply the renaming substitution to all literals Clause renamed; - renamed.id = c.id; - renamed.rule = c.rule; - renamed.parent1 = c.parent1; - renamed.parent2 = c.parent2; - renamed.depth = c.depth; - for (const auto& lit : c.literals) { - TermId new_atom = applySubstitution(rename_subst, lit.atom, bank); - renamed.literals.push_back({.atom = new_atom, .is_positive = lit.is_positive}); + renamed.id_ = c.id_; + renamed.rule_ = c.rule_; + renamed.parent1_ = c.parent1_; + renamed.parent2_ = c.parent2_; + renamed.depth_ = c.depth_; + for (const auto& lit : c.literals_) { + TermId const new_atom = applySubstitution(rename_subst, lit.atom_, bank); + renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_}); } return renamed; } @@ -87,7 +91,7 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2, size_t lit_idx2, const UnificationConfig& uconfig) { // Must have opposite polarity - if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) { + if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) { return std::nullopt; } @@ -99,28 +103,28 @@ std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, // Unify the complementary atoms Substitution subst; - if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst, uconfig)) { + if (!unify(bank, c1.literals_[lit_idx1].atom_, c2r.literals_[lit_idx2].atom_, subst, uconfig)) { return std::nullopt; } // Build the resolvent: all literals except the resolved pair, with subst applied Clause resolvent; - resolvent.rule = InferenceRule::kResolution; - resolvent.parent1 = c1.id; - resolvent.parent2 = c2.id; + resolvent.rule_ = InferenceRule::kResolution; + resolvent.parent1_ = c1.id_; + resolvent.parent2_ = c2.id_; - for (size_t i = 0; i < c1.literals.size(); ++i) { + for (size_t i = 0; i < c1.literals_.size(); ++i) { if (i != lit_idx1) { - TermId new_atom = applySubstitution(subst, c1.literals[i].atom, bank); - resolvent.literals.push_back( - {.atom = new_atom, .is_positive = c1.literals[i].is_positive}); + TermId const new_atom = applySubstitution(subst, c1.literals_[i].atom_, bank); + resolvent.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c1.literals_[i].is_positive_}); } } - for (size_t i = 0; i < c2r.literals.size(); ++i) { + for (size_t i = 0; i < c2r.literals_.size(); ++i) { if (i != lit_idx2) { - TermId new_atom = applySubstitution(subst, c2r.literals[i].atom, bank); - resolvent.literals.push_back( - {.atom = new_atom, .is_positive = c2r.literals[i].is_positive}); + TermId const new_atom = applySubstitution(subst, c2r.literals_[i].atom_, bank); + resolvent.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c2r.literals_[i].is_positive_}); } } return resolvent; @@ -129,9 +133,9 @@ std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause& c2, const UnificationConfig& uconfig) { std::vector results; - for (size_t i = 0; i < c1.literals.size(); ++i) { - for (size_t j = 0; j < c2.literals.size(); ++j) { - if (c1.literals[i].is_positive != c2.literals[j].is_positive) { + for (size_t i = 0; i < c1.literals_.size(); ++i) { + for (size_t j = 0; j < c2.literals_.size(); ++j) { + if (c1.literals_[i].is_positive_ != c2.literals_[j].is_positive_) { if (auto r = resolve(bank, c1, i, c2, j, uconfig)) { results.push_back(std::move(*r)); } @@ -143,24 +147,24 @@ std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause std::vector factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) { std::vector results; - for (size_t i = 0; i < c.literals.size(); ++i) { - for (size_t j = i + 1; j < c.literals.size(); ++j) { - if (c.literals[i].is_positive != c.literals[j].is_positive) { + for (size_t i = 0; i < c.literals_.size(); ++i) { + for (size_t j = i + 1; j < c.literals_.size(); ++j) { + if (c.literals_[i].is_positive_ != c.literals_[j].is_positive_) { continue; // Must have same polarity } Substitution subst; - if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst, uconfig)) { + if (!unify(bank, c.literals_[i].atom_, c.literals_[j].atom_, subst, uconfig)) { continue; } // Build factored clause: drop literal j, apply subst to all Clause factored; - factored.rule = InferenceRule::kFactoring; - factored.parent1 = c.id; - for (size_t k = 0; k < c.literals.size(); ++k) { + factored.rule_ = InferenceRule::kFactoring; + factored.parent1_ = c.id_; + for (size_t k = 0; k < c.literals_.size(); ++k) { if (k != j) { - TermId new_atom = applySubstitution(subst, c.literals[k].atom, bank); - factored.literals.push_back( - {.atom = new_atom, .is_positive = c.literals[k].is_positive}); + TermId const new_atom = applySubstitution(subst, c.literals_[k].atom_, bank); + factored.literals_.push_back( + {.atom_ = new_atom, .is_positive_ = c.literals_[k].is_positive_}); } } results.push_back(std::move(factored)); diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc index a7ce617..8710fb0 100644 --- a/src/infer/substitution.cc +++ b/src/infer/substitution.cc @@ -22,6 +22,8 @@ #include "atp/core/term_bank.h" #include "atp/core/types.h" +#include + namespace atp { bool Substitution::bind(TermId var, TermId term) { @@ -66,8 +68,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const { // IMPORTANT: Copy symbol_id and args BEFORE recursing. // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref. const Term& t = bank.getTerm(term); - SymbolId sym = t.symbol_id; - std::vector old_args(t.args); // copy! + SymbolId const sym = t.symbol_id_; + std::vector const old_args(t.args_); // copy! if (old_args.empty()) { // Constant or 0-arity — no substitution needed @@ -78,8 +80,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const { std::vector new_args; new_args.reserve(old_args.size()); bool changed = false; - for (TermId arg : old_args) { - TermId new_arg = apply(arg, bank); + for (TermId const arg : old_args) { + TermId const new_arg = apply(arg, bank); new_args.push_back(new_arg); if (new_arg != arg) { changed = true; @@ -105,7 +107,7 @@ bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const } const Term& t = bank.getTerm(term); - for (TermId arg : t.args) { + for (TermId const arg : t.args_) { if (occursIn(var, arg, bank)) { return true; } diff --git a/src/infer/unification.cc b/src/infer/unification.cc index 66e1af6..c42bf67 100644 --- a/src/infer/unification.cc +++ b/src/infer/unification.cc @@ -18,9 +18,14 @@ #include "atp/infer/unification.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" #include "atp/core/types.h" #include "atp/infer/substitution.h" +#include +#include + namespace atp { bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, @@ -33,7 +38,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, } if (bank.isVariable(t1)) { - if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { + if (config.enable_occurs_check_ && subst.occursIn(t1, t2, bank)) { return false; } subst.bind(t1, t2); @@ -41,7 +46,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, } if (bank.isVariable(t2)) { - if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { + if (config.enable_occurs_check_ && subst.occursIn(t2, t1, bank)) { return false; } subst.bind(t2, t1); @@ -51,12 +56,12 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, const Term& term1 = bank.getTerm(t1); const Term& term2 = bank.getTerm(t2); - if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + if (term1.symbol_id_ != term2.symbol_id_ || term1.arity() != term2.arity()) { return false; } for (size_t i = 0; i < term1.arity(); ++i) { - if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { + if (!unify(bank, term1.args_[i], term2.args_[i], subst, config)) { return false; } } @@ -73,12 +78,12 @@ TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) // IMPORTANT: Copy args and symbol_id BEFORE recursing. // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. const Term& t = bank.getTerm(term); - SymbolId sym = t.symbol_id; - std::vector old_args(t.args); // copy! + SymbolId const sym = t.symbol_id_; + std::vector const old_args(t.args_); // copy! std::vector new_args; new_args.reserve(old_args.size()); - for (TermId arg : old_args) { + for (TermId const arg : old_args) { new_args.push_back(applySubstitution(subst, arg, bank)); } return bank.makeTerm(sym, new_args); diff --git a/src/main.cc b/src/main.cc index bd385d8..81dbc91 100644 --- a/src/main.cc +++ b/src/main.cc @@ -27,8 +27,10 @@ #include "atp/search/prover.h" #include +#include #include #include +#include int main(int argc, char* argv[]) { std::cerr << "richard-atp-engine Copyright (C) 2026 Richard Qin\n" @@ -41,7 +43,7 @@ int main(int argc, char* argv[]) { return EXIT_FAILURE; } - const std::string filepath = argv[1]; + const std::string kFilepath = argv[1]; try { // 1. Initialize core modules @@ -50,9 +52,9 @@ int main(int argc, char* argv[]) { atp::ClauseStore store; // 2. Parse TPTP input - auto problem = atp::parseTptpFile(filepath, bank, symbols); + auto problem = atp::parseTptpFile(kFilepath, bank, symbols); - std::cerr << "% Parsed " << problem.formulas.size() << " formulas from " << filepath + std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << kFilepath << "\n"; // 3. Prepare clauses for proving @@ -63,28 +65,28 @@ int main(int argc, char* argv[]) { // 4. Run the prover atp::Prover prover(bank, store); prover.addClauses(std::move(clauses)); - atp::ProverResult result = prover.prove(); + atp::ProverResult const result = prover.prove(); // 5. Output result (SZS format) switch (result) { case atp::ProverResult::kTheorem: { - std::cout << "% SZS status Theorem for " << filepath << "\n\n"; + std::cout << "% SZS status Theorem for " << kFilepath << "\n\n"; // Extract and print proof auto eid = prover.getEmptyClauseId(); if (eid.has_value()) { auto proof = atp::extractProof(store, *eid); - std::cout << "% SZS output start Proof for " << filepath << "\n"; + std::cout << "% SZS output start Proof for " << kFilepath << "\n"; std::cout << atp::formatProof(proof, store, bank); - std::cout << "% SZS output end Proof for " << filepath << "\n"; + std::cout << "% SZS output end Proof for " << kFilepath << "\n"; } break; } case atp::ProverResult::kSaturation: - std::cout << "% SZS status Satisfiable for " << filepath << "\n"; + std::cout << "% SZS status Satisfiable for " << kFilepath << "\n"; break; case atp::ProverResult::kTimeout: - std::cout << "% SZS status Timeout for " << filepath << "\n"; + std::cout << "% SZS status Timeout for " << kFilepath << "\n"; break; } diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc index 183ab2e..a0d5a11 100644 --- a/src/proof/proof_trace.cc +++ b/src/proof/proof_trace.cc @@ -19,11 +19,15 @@ #include "atp/proof/proof_trace.h" #include "atp/core/clause.h" +#include "atp/core/clause_store.h" #include "atp/core/symbol_table.h" #include "atp/core/term.h" +#include "atp/core/term_bank.h" #include "atp/core/types.h" #include +#include +#include #include #include #include @@ -43,29 +47,29 @@ std::vector extractProof(const ClauseStore& store, ClauseId empty_cla worklist.push(empty_clause_id); while (!worklist.empty()) { - ClauseId cid = worklist.top(); + const ClauseId kCid = worklist.top(); worklist.pop(); - if (cid == kInvalidId) { + if (kCid == kInvalidId) { continue; } - if (visited.count(cid) > 0) { + if (visited.contains(kCid)) { continue; } - visited.insert(cid); + visited.insert(kCid); - const Clause& c = store.getClause(cid); + const Clause& c = store.getClause(kCid); steps.push_back({ - .clause_id = cid, - .rule = c.rule, - .parent1 = c.parent1, - .parent2 = c.parent2, + .clause_id_ = kCid, + .rule_ = c.rule_, + .parent1_ = c.parent1_, + .parent2_ = c.parent2_, }); // Recurse into parents (axioms have kInvalidId parents, which are // filtered by the check at the top of the loop) - worklist.push(c.parent1); - worklist.push(c.parent2); + worklist.push(c.parent1_); + worklist.push(c.parent2_); } // Reverse: axioms (leaves) first → empty clause (root) last @@ -77,18 +81,18 @@ std::vector extractProof(const ClauseStore& store, ClauseId empty_cla std::string termToString(TermId id, const TermBank& bank) { const Term& t = bank.getTerm(id); - std::string name(bank.symbols().getName(t.symbol_id)); + std::string name(bank.symbols().getName(t.symbol_id_)); - if (t.args.empty()) { + if (t.args_.empty()) { return name; } std::string result = name + "("; - for (size_t i = 0; i < t.args.size(); ++i) { + for (size_t i = 0; i < t.args_.size(); ++i) { if (i > 0) { result += ","; } - result += termToString(t.args[i], bank); + result += termToString(t.args_[i], bank); } result += ")"; return result; @@ -101,15 +105,15 @@ namespace { /// Generate a human-readable variable name from an index. /// 0→X, 1→Y, 2→Z, 3→W, 4→V, 5→U, 6→X1, 7→Y1, ... std::string prettyVarName(size_t index) { - static const char kBaseNames[] = {'X', 'Y', 'Z', 'W', 'V', 'U'}; - static constexpr size_t kBaseCount = sizeof(kBaseNames); + static constexpr std::array kBaseNames = {'X', 'Y', 'Z', 'W', 'V', 'U'}; + static constexpr size_t kBaseCount = kBaseNames.size(); - char base = kBaseNames[index % kBaseCount]; - size_t suffix = index / kBaseCount; - if (suffix == 0) { - return std::string(1, base); + const char kBase = kBaseNames[index % kBaseCount]; + const size_t kSuffix = index / kBaseCount; + if (kSuffix == 0) { + return std::string{kBase}; } - return std::string(1, base) + std::to_string(suffix); + return std::string{kBase} + std::to_string(kSuffix); } /// Pretty-print a term, renaming variables to readable names. @@ -121,29 +125,44 @@ std::string termToPretty(TermId id, const TermBank& bank, if (it != var_map.end()) { return it->second; } - std::string name = prettyVarName(var_map.size()); - var_map[id] = name; - return name; + const std::string kName = prettyVarName(var_map.size()); + var_map[id] = kName; + return kName; } const Term& t = bank.getTerm(id); - std::string name(bank.symbols().getName(t.symbol_id)); + std::string name(bank.symbols().getName(t.symbol_id_)); - if (t.args.empty()) { + if (t.args_.empty()) { return name; } std::string result = name + "("; - for (size_t i = 0; i < t.args.size(); ++i) { + for (size_t i = 0; i < t.args_.size(); ++i) { if (i > 0) { result += ","; } - result += termToPretty(t.args[i], bank, var_map); + result += termToPretty(t.args_[i], bank, var_map); } result += ")"; return result; } +// ruleToString + +std::string ruleToString(InferenceRule rule) { + switch (rule) { + case InferenceRule::kInput: + return "input"; + case InferenceRule::kResolution: + return "resolution"; + case InferenceRule::kFactoring: + return "factoring"; + default: + return "unknown"; + } +} + } // namespace // clauseToString @@ -157,33 +176,18 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) { std::unordered_map var_map; std::string result; - for (size_t i = 0; i < clause.literals.size(); ++i) { + for (size_t i = 0; i < clause.literals_.size(); ++i) { if (i > 0) { result += " ∨ "; } - if (!clause.literals[i].is_positive) { + if (!clause.literals_[i].is_positive_) { result += "¬"; } - result += termToPretty(clause.literals[i].atom, bank, var_map); + result += termToPretty(clause.literals_[i].atom_, bank, var_map); } return result; } -// ruleToString - -static std::string ruleToString(InferenceRule rule) { - switch (rule) { - case InferenceRule::kInput: - return "input"; - case InferenceRule::kResolution: - return "resolution"; - case InferenceRule::kFactoring: - return "factoring"; - default: - return "unknown"; - } -} - // formatProof std::string formatProof(const std::vector& proof, const ClauseStore& store, @@ -191,10 +195,10 @@ std::string formatProof(const std::vector& proof, const ClauseStore& // Build a local renumbering: internal ClauseId → sequential proof step number std::unordered_map id_to_step; for (size_t i = 0; i < proof.size(); ++i) { - id_to_step[proof[i].clause_id] = i + 1; // 1-based + id_to_step[proof[i].clause_id_] = i + 1; // 1-based } - auto localName = [&](ClauseId cid) -> std::string { + auto local_name = [&](ClauseId cid) -> std::string { auto it = id_to_step.find(cid); if (it != id_to_step.end()) { return std::to_string(it->second); @@ -206,17 +210,17 @@ std::string formatProof(const std::vector& proof, const ClauseStore& std::string result; for (size_t i = 0; i < proof.size(); ++i) { const auto& step = proof[i]; - const Clause& c = store.getClause(step.clause_id); + const Clause& c = store.getClause(step.clause_id_); result += std::to_string(i + 1) + ". "; - result += "[" + ruleToString(step.rule) + "] "; + result += "[" + ruleToString(step.rule_) + "] "; result += clauseToString(c, bank); // Show parents for derived clauses - if (step.parent1 != kInvalidId) { - result += " [" + localName(step.parent1); - if (step.parent2 != kInvalidId) { - result += ", " + localName(step.parent2); + if (step.parent1_ != kInvalidId) { + result += " [" + local_name(step.parent1_); + if (step.parent2_ != kInvalidId) { + result += ", " + local_name(step.parent2_); } result += "]"; } diff --git a/src/search/prover.cc b/src/search/prover.cc index 5b68e9d..2c2de40 100644 --- a/src/search/prover.cc +++ b/src/search/prover.cc @@ -18,6 +18,9 @@ #include "atp/search/prover.h" +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" #include "atp/core/types.h" #include "atp/infer/resolution.h" #include "atp/infer/unification.h" @@ -25,16 +28,21 @@ #include "atp/simplify/tautology.h" #include +#include +#include +#include +#include +#include namespace atp { Prover::Prover(TermBank& bank, ClauseStore& store, ProverConfig config) - : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator) {} + : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator_) {} void Prover::addClauses(std::vector clauses) { for (auto& clause : clauses) { - clause.depth = 0; - ClauseId id = store_.addClause(clause); + clause.depth_ = 0; + ClauseId const id = store_.addClause(clause); unprocessed_.push(store_.getClause(id)); } } @@ -44,7 +52,7 @@ ProverResult Prover::prove() { while (!unprocessed_.empty()) { // Resource limits - if (iterations >= config_.max_iterations || store_.size() >= config_.max_clauses) { + if (iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_) { return ProverResult::kTimeout; } ++iterations; @@ -55,7 +63,7 @@ ProverResult Prover::prove() { // 2. Check if given is itself the empty clause if (given.isEmpty()) { - empty_clause_id_ = given.id; + empty_clause_id_ = given.id_; return ProverResult::kTheorem; } @@ -65,7 +73,7 @@ ProverResult Prover::prove() { } bool forward_subsumed = false; - for (ClauseId pid : processed_) { + for (ClauseId const pid : processed_) { if (subsumes(store_.getClause(pid), given)) { forward_subsumed = true; break; @@ -84,14 +92,14 @@ ProverResult Prover::prove() { // 5. Generate new clauses // Inference BEFORE adding given to processed — matches doc §4.6. std::vector new_clauses; - const UnificationConfig uconfig{.enable_occurs_check = config_.enable_occurs_check}; + const UnificationConfig kUconfig{.enable_occurs_check_ = config_.enable_occurs_check_}; // 5a. Resolve given with every processed clause (both directions) - for (ClauseId pid : processed_) { + for (ClauseId const pid : processed_) { const Clause& pc = store_.getClause(pid); - auto resolvents1 = allResolvents(bank_, given, pc, uconfig); - auto resolvents2 = allResolvents(bank_, pc, given, uconfig); + auto resolvents1 = allResolvents(bank_, given, pc, kUconfig); + auto resolvents2 = allResolvents(bank_, pc, given, kUconfig); for (auto& r : resolvents1) { new_clauses.push_back(std::move(r)); @@ -102,13 +110,13 @@ ProverResult Prover::prove() { } // 5b. Factor given (only once) - auto factors = factor(bank_, given, uconfig); + auto factors = factor(bank_, given, kUconfig); for (auto& f : factors) { new_clauses.push_back(std::move(f)); } // 6. Add given to processed AFTER inference - processed_.push_back(given.id); + processed_.push_back(given.id_); // 7. Process new clauses for (auto& nc : new_clauses) { @@ -125,17 +133,17 @@ ProverResult Prover::prove() { } // 7c. Set depth - uint32_t d1 = (nc.parent1 != kInvalidId) ? store_.getClause(nc.parent1).depth : 0; - uint32_t d2 = (nc.parent2 != kInvalidId) ? store_.getClause(nc.parent2).depth : 0; - nc.depth = static_cast(std::max(d1, d2) + 1); + uint32_t const d1 = (nc.parent1_ != kInvalidId) ? store_.getClause(nc.parent1_).depth_ : 0; + uint32_t const d2 = (nc.parent2_ != kInvalidId) ? store_.getClause(nc.parent2_).depth_ : 0; + nc.depth_ = static_cast(std::max(d1, d2) + 1); // 7d. Store the clause (needed for forward subsumption check) - ClauseId nid = store_.addClause(nc); + ClauseId const nid = store_.addClause(nc); const Clause& stored_nc = store_.getClause(nid); // 7e. Forward subsumption on new clause bool new_subsumed = false; - for (ClauseId pid : processed_) { + for (ClauseId const pid : processed_) { if (subsumes(store_.getClause(pid), stored_nc)) { new_subsumed = true; break; diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc index 3756d82..0038ad1 100644 --- a/src/simplify/subsumption.cc +++ b/src/simplify/subsumption.cc @@ -18,16 +18,18 @@ #include "atp/simplify/subsumption.h" +#include "atp/core/clause.h" + namespace atp { bool subsumes(const Clause& general, const Clause& specific) { if (general.size() > specific.size()) { return false; } - for (const auto& lit_g : general.literals) { + for (const auto& lit_g : general.literals_) { bool found = false; - for (const auto& lit_s : specific.literals) { - if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) { + for (const auto& lit_s : specific.literals_) { + if (lit_g.atom_ == lit_s.atom_ && lit_g.is_positive_ == lit_s.is_positive_) { found = true; break; } diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc index 70bdced..e35d874 100644 --- a/src/simplify/tautology.cc +++ b/src/simplify/tautology.cc @@ -18,14 +18,16 @@ #include "atp/simplify/tautology.h" +#include "atp/core/clause.h" + #include namespace atp { bool isTautology(const Clause& clause) { for (size_t i = 0; i < clause.size(); ++i) { for (size_t j = i + 1; j < clause.size(); ++j) { - if (clause.literals[i].atom == clause.literals[j].atom && - clause.literals[i].is_positive != clause.literals[j].is_positive) { + if (clause.literals_[i].atom_ == clause.literals_[j].atom_ && + clause.literals_[i].is_positive_ != clause.literals_[j].is_positive_) { return true; } } -- cgit v1.2.3