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/main.cc | 20 +++++++++++--------- 1 file changed, 11 insertions(+), 9 deletions(-) (limited to 'src/main.cc') 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; } -- cgit v1.2.3