aboutsummaryrefslogtreecommitdiff
path: root/src/proof/proof_trace.cc
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-04 04:56:51 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-04 04:56:51 +0800
commit7408740374f46b24edd53d421dbc270d2fca1293 (patch)
treea8a7cd6b6f932487c5b9bd560e60cd6cc3732f03 /src/proof/proof_trace.cc
parent0d7c8177171be1d0c077e468ee743697dd8c6914 (diff)
downloadratp-7408740374f46b24edd53d421dbc270d2fca1293.tar.gz
ratp-7408740374f46b24edd53d421dbc270d2fca1293.tar.xz
feat: implement command-line interface and add end-to-end propositional logic test suite
Diffstat (limited to 'src/proof/proof_trace.cc')
-rw-r--r--src/proof/proof_trace.cc10
1 files changed, 5 insertions, 5 deletions
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) {