From 7408740374f46b24edd53d421dbc270d2fca1293 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
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/search/prover.cc | 16 ++++++++--------
 1 file changed, 8 insertions(+), 8 deletions(-)

(limited to 'src/search')

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()) {
-- 
cgit v1.2.3