feat: implement command-line interface and add end-to-end propositional logic test suite

5 files changed, 275 insertions, 13 deletions

diff --git a/data/simple_propositional.p b/data/simple_propositional.p
new file mode 100644
index 0000000..283c326
--- /dev/null
+++ b/data/simple_propositional.p
@@ -0,0 +1,5 @@
+% Simple propositional-style test
+% P(a) and (P(X) → Q(X)) and ¬Q(a) should be unsatisfiable.
+cnf(fact, axiom, p(a)).
+cnf(rule, axiom, ~p(X) | q(X)).
+cnf(goal, negated_conjecture, ~q(a)).
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 <https://www.gnu.org/licenses/>.
  */
 
+/// @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 <cstdlib>
+#include <iostream>
+#include <string>
+
+int main(int argc, char* argv[]) {
+    if (argc < 2) {
+        std::cerr << "Usage: atp <file.p>\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<ProofStep> 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<ProofStep>& 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<Clause> 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()) {
diff --git a/tests/test_end_to_end.cc b/tests/test_end_to_end.cc
new file mode 100644
index 0000000..7997d83
--- /dev/null
+++ b/tests/test_end_to_end.cc
@@ -0,0 +1,184 @@
+/*
+ * richard-atp-engine: A saturation-based automated theorem prover for first-order logic.
+ * Copyright (C) 2026 Richard Qin
+ *
+ * This program is free software: you can redistribute it and/or modify
+ * it under the terms of the GNU General Public License as published by
+ * the Free Software Foundation, either version 3 of the License, or
+ * (at your option) any later version.
+ *
+ * This program is distributed in the hope that it will be useful,
+ * but WITHOUT ANY WARRANTY; without even the implied warranty of
+ * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
+ * GNU General Public License for more details.
+ *
+ * You should have received a copy of the GNU General Public License
+ * along with this program.  If not, see <https://www.gnu.org/licenses/>.
+ */
+
+/// @file test_end_to_end.cc
+/// @brief End-to-end tests: TPTP string → parse → prove → verify result.
+
+#include <gtest/gtest.h>
+
+#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 <string>
+
+namespace atp {
+namespace {
+
+/// Helper: parse a TPTP string and run the prover, return the result.
+struct E2EResult {
+    ProverResult result;
+    std::string proof_output;
+};
+
+E2EResult runProver(const std::string& tptp_input) {
+    SymbolTable symbols;
+    TermBank bank(symbols);
+    ClauseStore store;
+
+    auto problem = parseTptpString(tptp_input, bank, symbols);
+    auto clauses = prepareForProving(problem, bank, symbols);
+
+    Prover prover(bank, store);
+    prover.addClauses(std::move(clauses));
+    ProverResult result = prover.prove();
+
+    std::string proof_output;
+    if (result == ProverResult::kTheorem) {
+        auto eid = prover.getEmptyClauseId();
+        if (eid.has_value()) {
+            auto proof = extractProof(store, *eid);
+            proof_output = formatProof(proof, store, bank);
+        }
+    }
+
+    return {result, proof_output};
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Simple Propositional
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, SimplePropositional) {
+    auto [result, proof] = runProver(R"(
+        cnf(fact, axiom, p(a)).
+        cnf(rule, axiom, ~p(X) | q(X)).
+        cnf(goal, negated_conjecture, ~q(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+    EXPECT_FALSE(proof.empty());
+    // Proof should contain the key elements
+    EXPECT_NE(proof.find("p(a)"), std::string::npos) << proof;
+    EXPECT_NE(proof.find("q(a)"), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Trivial: direct contradiction
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, DirectContradiction) {
+    auto [result, proof] = runProver(R"(
+        cnf(pos, axiom, p(a)).
+        cnf(neg, negated_conjecture, ~p(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Satisfiable: no contradiction possible
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, Satisfiable) {
+    auto [result, proof] = runProver(R"(
+        cnf(a1, axiom, p(a)).
+        cnf(a2, axiom, q(b)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kSaturation);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Three-step chain
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, ThreeStepChain) {
+    auto [result, proof] = runProver(R"(
+        cnf(a1, axiom, p(a)).
+        cnf(a2, axiom, ~p(X) | q(X)).
+        cnf(a3, axiom, ~q(X) | r(X)).
+        cnf(goal, negated_conjecture, ~r(a)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem);
+    EXPECT_NE(proof.find("r(a)"), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Proof output format
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, ProofOutputContainsAllSteps) {
+    auto [result, proof] = runProver(R"(
+        cnf(fact, axiom, p(a)).
+        cnf(rule, axiom, ~p(X) | q(X)).
+        cnf(goal, negated_conjecture, ~q(a)).
+    )");
+
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    // Must contain [input] lines for axioms
+    EXPECT_NE(proof.find("[input]"), std::string::npos) << proof;
+    // Must contain [resolution] for derived clauses
+    EXPECT_NE(proof.find("[resolution]"), std::string::npos) << proof;
+    // Must contain empty clause marker
+    std::string empty_marker = "□";
+    EXPECT_NE(proof.find(empty_marker), std::string::npos) << proof;
+    // Must contain [from cX, cY] provenance
+    EXPECT_NE(proof.find("[from c"), std::string::npos) << proof;
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// Monkey and Banana Problem (the flagship test!)
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST(EndToEnd, MonkeyBanana) {
+    auto [result, proof] = runProver(R"(
+        % Initial state
+        cnf(init_state, axiom, state(a, b, c, h0, s0)).
+
+        % Action: Go(X)
+        cnf(action_go, axiom, ~state(M, B, G, h0, S) | state(X, B, G, h0, do(go(X), S))).
+
+        % Action: Push(X)
+        cnf(action_push, axiom, ~state(M, M, G, h0, S) | state(X, X, G, h0, do(push(X), S))).
+
+        % Action: Climb
+        cnf(action_climb, axiom, ~state(M, M, G, h0, S) | state(M, M, G, h1, do(climb, S))).
+
+        % Action: Down
+        cnf(action_down, axiom, ~state(M, B, G, h1, S) | state(M, B, G, h0, do(down, S))).
+
+        % Action: Reach
+        cnf(action_reach, axiom, ~state(G, G, G, h1, S) | goal_reached(do(reach, S))).
+
+        % Negated goal
+        cnf(negated_goal, negated_conjecture, ~goal_reached(S)).
+    )");
+
+    EXPECT_EQ(result, ProverResult::kTheorem)
+        << "ATP should prove the monkey can get the banana!\n"
+        << "Proof output:\n" << proof;
+}
+
+}  // namespace
+}  // namespace atp