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

1 files changed, 73 insertions, 0 deletions

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;
+}