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/proof/proof_trace.cc | 114 ++++++++++++++++++++++++----------------------- 1 file changed, 59 insertions(+), 55 deletions(-) (limited to 'src/proof') 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 += "]"; } -- cgit v1.2.3