feat: implement proof trace extraction and add proof trace test

4 files changed, 365 insertions, 9 deletions

diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h
index cda6c5b..a80a327 100644
--- a/include/atp/proof/proof_trace.h
+++ b/include/atp/proof/proof_trace.h
@@ -16,14 +16,10 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
-
 #pragma once
 
 /// @file proof_trace.h
 /// @brief Proof reconstruction from the empty clause back to axioms.
-///
-/// This module depends only on ClauseStore (not Prover), so it can be
-/// reused with any search strategy.
 
 #include "atp/core/clause.h"
 #include "atp/core/clause_store.h"
@@ -40,15 +36,20 @@ struct ProofStep {
     InferenceRule rule;
     ClauseId parent1;
     ClauseId parent2;
-    std::string description;  ///< Human-readable description
 };
 
 /// Reconstruct the proof trace from the empty clause.
-/// Walks parent pointers via ClauseStore, independent of search strategy.
-std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id,
-                                    const TermBank& bank);
+/// Returns steps in topological order: axioms first, empty clause last.
+std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id);
+
+/// Convert a TermId back to a human-readable string.
+std::string termToString(TermId id, const TermBank& bank);
+
+/// Convert a Clause to a human-readable string.
+std::string clauseToString(const Clause& clause, const TermBank& bank);
 
 /// Format a proof as a human-readable string.
-std::string formatProof(const std::vector<ProofStep>& proof, const TermBank& bank);
+std::string formatProof(const std::vector<ProofStep>& proof,
+                        const ClauseStore& store, const TermBank& bank);
 
 }  // namespace atp
diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index b62ffd0..b1b4343 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -16,4 +16,139 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#include "atp/proof/proof_trace.h"
+#include "atp/core/clause.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term.h"
+#include "atp/core/types.h"
 
+#include <algorithm>
+#include <stack>
+#include <string>
+#include <unordered_set>
+#include <vector>
+
+namespace atp {
+
+// ─── extractProof ────────────────────────────────────────────────────────────
+// DFS from empty clause back to axioms, collect all participating clauses,
+// then reverse for topological order (axioms first).
+
+std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id) {
+    std::vector<ProofStep> steps;
+    std::unordered_set<ClauseId> visited;
+    std::stack<ClauseId> worklist;
+    worklist.push(empty_clause_id);
+
+    while (!worklist.empty()) {
+        ClauseId cid = worklist.top();
+        worklist.pop();
+
+        if (cid == kInvalidId) {
+            continue;
+        }
+        if (visited.count(cid) > 0) {
+            continue;
+        }
+        visited.insert(cid);
+
+        const Clause& c = store.getClause(cid);
+        steps.push_back({
+            .clause_id = cid,
+            .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);
+    }
+
+    // Reverse: axioms (leaves) first → empty clause (root) last
+    std::ranges::reverse(steps);
+    return steps;
+}
+
+// ─── termToString ────────────────────────────────────────────────────────────
+
+std::string termToString(TermId id, const TermBank& bank) {
+    const Term& t = bank.getTerm(id);
+    std::string name(bank.symbols().getName(t.symbol_id));
+
+    if (t.args.empty()) {
+        return name;
+    }
+
+    std::string result = name + "(";
+    for (size_t i = 0; i < t.args.size(); ++i) {
+        if (i > 0) {
+            result += ",";
+        }
+        result += termToString(t.args[i], bank);
+    }
+    result += ")";
+    return result;
+}
+
+// ─── clauseToString ──────────────────────────────────────────────────────────
+
+std::string clauseToString(const Clause& clause, const TermBank& bank) {
+    if (clause.isEmpty()) {
+        return "□";
+    }
+
+    std::string result;
+    for (size_t i = 0; i < clause.literals.size(); ++i) {
+        if (i > 0) {
+            result += " ∨ ";
+        }
+        if (!clause.literals[i].is_positive) {
+            result += "¬";
+        }
+        result += termToString(clause.literals[i].atom, bank);
+    }
+    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<ProofStep>& proof,
+                        const ClauseStore& store, const TermBank& bank) {
+    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);
+
+        result += std::to_string(i + 1) + ". ";
+        result += "[" + ruleToString(step.rule) + "] ";
+        result += "c" + std::to_string(step.clause_id) + ": ";
+        result += clauseToString(c, bank);
+
+        // Show parents for derived clauses
+        if (step.parent1 != kInvalidId) {
+            result += "  [from c" + std::to_string(step.parent1);
+            if (step.parent2 != kInvalidId) {
+                result += ", c" + std::to_string(step.parent2);
+            }
+            result += "]";
+        }
+
+        result += "\n";
+    }
+    return result;
+}
+
+}  // namespace atp
diff --git a/tests/CMakeLists.txt b/tests/CMakeLists.txt
index 864c0ad..eea0ceb 100644
--- a/tests/CMakeLists.txt
+++ b/tests/CMakeLists.txt
@@ -26,3 +26,5 @@ atp_add_test(test_resolution      test_resolution.cc)
 atp_add_test(test_discrim_tree    test_discrim_tree.cc)
 atp_add_test(test_prover          test_prover.cc)
 atp_add_test(test_simplify        test_simplify.cc)
+atp_add_test(test_proof_trace     test_proof_trace.cc)
+atp_add_test(test_end_to_end      test_end_to_end.cc)
diff --git a/tests/test_proof_trace.cc b/tests/test_proof_trace.cc
new file mode 100644
index 0000000..d7ff246
--- /dev/null
+++ b/tests/test_proof_trace.cc
@@ -0,0 +1,218 @@
+/*
+ * 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/>.
+ */
+
+#include <gtest/gtest.h>
+
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/literal.h"
+#include "atp/core/symbol_table.h"
+#include "atp/core/term_bank.h"
+#include "atp/core/types.h"
+#include "atp/proof/proof_trace.h"
+#include "atp/search/prover.h"
+
+#include <string>
+
+namespace atp {
+namespace {
+
+class ProofTraceTest : public ::testing::Test {
+  protected:
+    SymbolTable symbols;
+    TermBank bank{symbols};
+    ClauseStore store;
+
+    SymbolId sym_a{}, sym_b{};
+    SymbolId sym_P{}, sym_Q{};
+    SymbolId sym_X{};
+
+    TermId a_term{}, b_term{}, X_term{};
+
+    void SetUp() override {
+        sym_a = symbols.intern("a", SymbolKind::kConstant);
+        sym_b = symbols.intern("b", SymbolKind::kConstant);
+        sym_P = symbols.intern("P", SymbolKind::kPredicate, 1);
+        sym_Q = symbols.intern("Q", SymbolKind::kPredicate, 1);
+        sym_X = symbols.intern("X", SymbolKind::kVariable);
+
+        a_term = bank.makeTerm(sym_a, {});
+        b_term = bank.makeTerm(sym_b, {});
+        X_term = bank.makeVar(sym_X);
+    }
+
+    TermId P(TermId arg) { return bank.makeTerm(sym_P, {{arg}}); }
+    TermId Q(TermId arg) { return bank.makeTerm(sym_Q, {{arg}}); }
+
+    Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; }
+    Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; }
+
+    Clause makeClause(std::vector<Literal> lits) {
+        Clause cl;
+        cl.literals = std::move(lits);
+        return cl;
+    }
+};
+
+// ═══════════════════════════════════════════════════════════════════════════
+// termToString Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, TermToStringConstant) {
+    EXPECT_EQ(termToString(a_term, bank), "a");
+}
+
+TEST_F(ProofTraceTest, TermToStringVariable) {
+    EXPECT_EQ(termToString(X_term, bank), "X");
+}
+
+TEST_F(ProofTraceTest, TermToStringCompound) {
+    TermId pa = P(a_term);
+    EXPECT_EQ(termToString(pa, bank), "P(a)");
+}
+
+TEST_F(ProofTraceTest, TermToStringNested) {
+    SymbolId sym_f = symbols.intern("f", SymbolKind::kFunction, 1);
+    TermId fa = bank.makeTerm(sym_f, {{a_term}});
+    TermId pfa = P(fa);
+    EXPECT_EQ(termToString(pfa, bank), "P(f(a))");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// clauseToString Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, ClauseToStringEmpty) {
+    Clause empty = makeClause({});
+    EXPECT_EQ(clauseToString(empty, bank), "□");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringSinglePositive) {
+    Clause c = makeClause({pos(P(a_term))});
+    EXPECT_EQ(clauseToString(c, bank), "P(a)");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringSingleNegative) {
+    Clause c = makeClause({neg(P(a_term))});
+    EXPECT_EQ(clauseToString(c, bank), "¬P(a)");
+}
+
+TEST_F(ProofTraceTest, ClauseToStringMultipleLiterals) {
+    Clause c = makeClause({neg(P(X_term)), pos(Q(X_term))});
+    std::string s = clauseToString(c, bank);
+    EXPECT_EQ(s, "¬P(X) ∨ Q(X)");
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// extractProof Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, ExtractProofTrivial) {
+    // Run a trivial proof: {P(a)} + {¬P(a)} → □
+    Prover prover(bank, store);
+    prover.addClauses({
+        makeClause({pos(P(a_term))}),
+        makeClause({neg(P(a_term))})
+    });
+    ProverResult result = prover.prove();
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store, *eid);
+    ASSERT_GE(proof.size(), 3u);  // At least: 2 axioms + 1 empty clause
+
+    // First steps should be axioms (kInput)
+    EXPECT_EQ(proof.front().rule, InferenceRule::kInput);
+    // Last step should be the empty clause
+    EXPECT_EQ(proof.back().clause_id, *eid);
+    // Last step should be resolution
+    EXPECT_EQ(proof.back().rule, InferenceRule::kResolution);
+}
+
+TEST_F(ProofTraceTest, ExtractProofTwoStep) {
+    // {P(a)}, {¬P(X), Q(X)}, {¬Q(a)} → □ in 2 resolution steps
+    Prover prover(bank, store);
+    prover.addClauses({
+        makeClause({pos(P(a_term))}),
+        makeClause({neg(P(X_term)), pos(Q(X_term))}),
+        makeClause({neg(Q(a_term))})
+    });
+    ProverResult result = prover.prove();
+    ASSERT_EQ(result, ProverResult::kTheorem);
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store, *eid);
+    // Should have axioms + intermediate + empty clause
+    ASSERT_GE(proof.size(), 4u);  // 3 axioms + at least 1 intermediate + empty
+
+    // Last step is the empty clause
+    EXPECT_EQ(proof.back().clause_id, *eid);
+}
+
+// ═══════════════════════════════════════════════════════════════════════════
+// formatProof Tests
+// ═══════════════════════════════════════════════════════════════════════════
+
+TEST_F(ProofTraceTest, FormatProofContainsExpectedElements) {
+    Prover prover(bank, store);
+    prover.addClauses({
+        makeClause({pos(P(a_term))}),
+        makeClause({neg(P(a_term))})
+    });
+    prover.prove();
+
+    auto eid = prover.getEmptyClauseId();
+    ASSERT_TRUE(eid.has_value());
+
+    auto proof = extractProof(store, *eid);
+    std::string output = formatProof(proof, store, bank);
+
+    // Should contain key elements
+    EXPECT_NE(output.find("input"), std::string::npos) << output;
+    EXPECT_NE(output.find("resolution"), std::string::npos) << output;
+    EXPECT_NE(output.find("P(a)"), std::string::npos) << output;
+    // Empty clause should appear
+    std::string empty_marker = "□";
+    EXPECT_NE(output.find(empty_marker), std::string::npos) << output;
+}
+
+TEST_F(ProofTraceTest, FormatProofNoParentsForAxioms) {
+    Prover prover(bank, store);
+    prover.addClauses({
+        makeClause({pos(P(a_term))}),
+        makeClause({neg(P(a_term))})
+    });
+    prover.prove();
+
+    auto eid = prover.getEmptyClauseId();
+    auto proof = extractProof(store, *eid);
+    std::string output = formatProof(proof, store, bank);
+
+    // The first line (an axiom) should NOT have "[from ...]"
+    // Find the first newline
+    auto first_line = output.substr(0, output.find('\n'));
+    EXPECT_EQ(first_line.find("[from"), std::string::npos)
+        << "Axiom should not have parent info: " << first_line;
+}
+
+}  // namespace
+}  // namespace atp