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/infer/resolution.cc | 84 +++++++++++++++++++++++++---------------------- src/infer/substitution.cc | 12 ++++--- src/infer/unification.cc | 19 +++++++---- 3 files changed, 63 insertions(+), 52 deletions(-) (limited to 'src/infer') 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); -- cgit v1.2.3