diff options
Diffstat (limited to 'include/atp/proof/proof_trace.h')
| -rw-r--r-- | include/atp/proof/proof_trace.h | 19 |
1 files changed, 10 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 |