From 7408740374f46b24edd53d421dbc270d2fca1293 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 04:56:51 +0800 Subject: feat: implement command-line interface and add end-to-end propositional logic test suite --- src/main.cc | 73 ++++++++++++++++++++++++++++++++++++++++++++++++ src/proof/proof_trace.cc | 10 +++---- src/search/prover.cc | 16 +++++------ 3 files changed, 86 insertions(+), 13 deletions(-) (limited to 'src') diff --git a/src/main.cc b/src/main.cc index b62ffd0..45c0185 100644 --- a/src/main.cc +++ b/src/main.cc @@ -16,4 +16,77 @@ * along with this program. If not, see . */ +/// @file main.cc +/// @brief ATP Engine command-line entry point. +#include "atp/core/clause_store.h" +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/frontend/tptp_parser.h" +#include "atp/proof/proof_trace.h" +#include "atp/search/prover.h" + +#include +#include +#include + +int main(int argc, char* argv[]) { + if (argc < 2) { + std::cerr << "Usage: atp \n"; + return EXIT_FAILURE; + } + + const std::string filepath = argv[1]; + + try { + // 1. Initialize core modules + atp::SymbolTable symbols; + atp::TermBank bank(symbols); + atp::ClauseStore store; + + // 2. Parse TPTP input + auto problem = atp::parseTptpFile(filepath, bank, symbols); + + std::cerr << "% Parsed " << problem.formulas.size() + << " formulas from " << filepath << "\n"; + + // 3. Prepare clauses for proving + auto clauses = atp::prepareForProving(problem, bank, symbols); + + std::cerr << "% " << clauses.size() << " clauses prepared for proving\n"; + + // 4. Run the prover + atp::Prover prover(bank, store); + prover.addClauses(std::move(clauses)); + atp::ProverResult result = prover.prove(); + + // 5. Output result (SZS format) + switch (result) { + case atp::ProverResult::kTheorem: { + std::cout << "% SZS status Theorem for " << filepath << "\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 << atp::formatProof(proof, store, bank); + std::cout << "% SZS output end Proof for " << filepath << "\n"; + } + break; + } + case atp::ProverResult::kSaturation: + std::cout << "% SZS status Satisfiable for " << filepath << "\n"; + break; + case atp::ProverResult::kTimeout: + std::cout << "% SZS status Timeout for " << filepath << "\n"; + break; + } + + } catch (const std::exception& e) { + std::cerr << "% Error: " << e.what() << "\n"; + return EXIT_FAILURE; + } + + return EXIT_SUCCESS; +} diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc index b1b4343..fff54a3 100644 --- a/src/proof/proof_trace.cc +++ b/src/proof/proof_trace.cc @@ -30,7 +30,7 @@ namespace atp { -// ─── extractProof ──────────────────────────────────────────────────────────── +// ─── extractProof // DFS from empty clause back to axioms, collect all participating clauses, // then reverse for topological order (axioms first). @@ -71,7 +71,7 @@ std::vector extractProof(const ClauseStore& store, ClauseId empty_cla return steps; } -// ─── termToString ──────────────────────────────────────────────────────────── +// ─── termToString std::string termToString(TermId id, const TermBank& bank) { const Term& t = bank.getTerm(id); @@ -92,7 +92,7 @@ std::string termToString(TermId id, const TermBank& bank) { return result; } -// ─── clauseToString ────────────────────────────────────────────────────────── +// ─── clauseToString std::string clauseToString(const Clause& clause, const TermBank& bank) { if (clause.isEmpty()) { @@ -112,7 +112,7 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) { return result; } -// ─── ruleToString ──────────────────────────────────────────────────────────── +// ─── ruleToString static std::string ruleToString(InferenceRule rule) { switch (rule) { @@ -123,7 +123,7 @@ static std::string ruleToString(InferenceRule rule) { } } -// ─── formatProof ───────────────────────────────────────────────────────────── +// ─── formatProof std::string formatProof(const std::vector& proof, const ClauseStore& store, const TermBank& bank) { diff --git a/src/search/prover.cc b/src/search/prover.cc index 844f6c1..e1b117b 100644 --- a/src/search/prover.cc +++ b/src/search/prover.cc @@ -45,24 +45,24 @@ ProverResult Prover::prove() { size_t iterations = 0; while (!unprocessed_.empty()) { - // ─── Resource limits ────────────────────────────────────────── + // Resource limits if (iterations >= config_.max_iterations || store_.size() >= config_.max_clauses) { return ProverResult::kTimeout; } ++iterations; - // ─── 1. Select the best clause from unprocessed ────────────── + // 1. Select the best clause from unprocessed Clause given = unprocessed_.top(); unprocessed_.pop(); - // ─── 2. Check if given is itself the empty clause ──────────── + // 2. Check if given is itself the empty clause if (given.isEmpty()) { empty_clause_id_ = given.id; return ProverResult::kTheorem; } - // ─── 3. Forward redundancy checks ──────────────────────────── + // 3. Forward redundancy checks if (isTautology(given)) { continue; } @@ -78,14 +78,14 @@ ProverResult Prover::prove() { continue; } - // ─── 4. Backward subsumption ───────────────────────────────── + // 4. Backward subsumption // Remove from processed all clauses that are subsumed by given. // Use erase-remove idiom for O(n) scan instead of repeated erase. std::erase_if(processed_, [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); }); - // ─── 5. Generate new clauses ───────────────────────────────── + // 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}; @@ -111,10 +111,10 @@ ProverResult Prover::prove() { new_clauses.push_back(std::move(f)); } - // ─── 6. Add given to processed AFTER inference ─────────────── + // 6. Add given to processed AFTER inference processed_.push_back(given.id); - // ─── 7. Process new clauses ────────────────────────────────── + // 7. Process new clauses for (auto& nc : new_clauses) { // 7a. Check for empty clause → proof found! if (nc.isEmpty()) { -- cgit v1.2.3