From cc440e2674697afc967e081cf91e03f149333502 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Thu, 2 Apr 2026 04:10:53 +0800 Subject: Initial commit: Build project architecture, define interfaces, write documentation, with the help of Claude --- proofsearch/tests/CMakeLists.txt | 27 +++++++++++++++++++++++++++ 1 file changed, 27 insertions(+) create mode 100644 proofsearch/tests/CMakeLists.txt (limited to 'proofsearch/tests/CMakeLists.txt') diff --git a/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt new file mode 100644 index 0000000..d841595 --- /dev/null +++ b/proofsearch/tests/CMakeLists.txt @@ -0,0 +1,27 @@ +# ─── GoogleTest ─────────────────────────────────────────────────────────────── +include(FetchContent) +FetchContent_Declare( + googletest + GIT_REPOSITORY https://github.com/google/googletest.git + GIT_TAG v1.14.0 +) +# Prevent GoogleTest from overriding our compiler/linker options +set(gtest_force_shared_crt ON CACHE BOOL "" FORCE) +FetchContent_MakeAvailable(googletest) + +include(GoogleTest) + +# ─── Helper: define a test target ──────────────────────────────────────────── +function(atp_add_test TEST_NAME TEST_SOURCE) + add_executable(${TEST_NAME} ${TEST_SOURCE}) + target_link_libraries(${TEST_NAME} PRIVATE atp_core GTest::gtest_main) + gtest_discover_tests(${TEST_NAME}) +endfunction() + +# ─── Test Targets ──────────────────────────────────────────────────────────── +atp_add_test(test_term_bank test_term_bank.cc) +atp_add_test(test_unification test_unification.cc) +atp_add_test(test_clausifier test_clausifier.cc) +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) -- cgit v1.2.3 From 2713bbcb4044ca18eb3071a8efea7ad097a6693b Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 03:02:48 +0800 Subject: feat: implement clause subsumption and tautology detection logic with associated unit tests --- proofsearch/CMakeLists.txt | 1 + proofsearch/include/atp/simplify/subsumption.h | 2 + proofsearch/src/simplify/subsumption.cc | 23 +++ proofsearch/src/simplify/tautology.cc | 34 +++++ proofsearch/tests/CMakeLists.txt | 1 + proofsearch/tests/test_simplify.cc | 189 +++++++++++++++++++++++++ 6 files changed, 250 insertions(+) create mode 100644 proofsearch/src/simplify/tautology.cc create mode 100644 proofsearch/tests/test_simplify.cc (limited to 'proofsearch/tests/CMakeLists.txt') diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt index edeb6b7..1b6473e 100644 --- a/proofsearch/CMakeLists.txt +++ b/proofsearch/CMakeLists.txt @@ -77,6 +77,7 @@ set(ATP_SOURCES src/infer/resolution.cc src/index/discrim_tree.cc src/simplify/subsumption.cc + src/simplify/tautology.cc src/search/prover.cc src/proof/proof_trace.cc src/rewrite/ordering.cc diff --git a/proofsearch/include/atp/simplify/subsumption.h b/proofsearch/include/atp/simplify/subsumption.h index ee7a83e..c39b586 100644 --- a/proofsearch/include/atp/simplify/subsumption.h +++ b/proofsearch/include/atp/simplify/subsumption.h @@ -52,4 +52,6 @@ class SubsumptionEngine { // TODO: Phase 5 implementation }; +bool subsumes(const Clause& general, const Clause& specific); + } // namespace atp diff --git a/proofsearch/src/simplify/subsumption.cc b/proofsearch/src/simplify/subsumption.cc index b62ffd0..cf243c9 100644 --- a/proofsearch/src/simplify/subsumption.cc +++ b/proofsearch/src/simplify/subsumption.cc @@ -16,4 +16,27 @@ * along with this program. If not, see . */ +#include "atp/simplify/subsumption.h" + +namespace atp { + + bool subsumes(const Clause& general, const Clause& specific) { + if (general.size() > specific.size()) { + return false; + } + for (const auto& lit_g : general.literals) { + bool found = false; + for (const auto& lit_s : specific.literals) { + if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) { + found = true; + break; + } + } + if (!found) { + return false; + } + } + return true; + } +} diff --git a/proofsearch/src/simplify/tautology.cc b/proofsearch/src/simplify/tautology.cc new file mode 100644 index 0000000..d41ecd7 --- /dev/null +++ b/proofsearch/src/simplify/tautology.cc @@ -0,0 +1,34 @@ +/* + * 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 . + */ + +#include "atp/simplify/tautology.h" +#include + + namespace atp { + bool isTautology(const Clause& clause) { + for (size_t i = 0; i < clause.size(); ++i) { + for (size_t j = i + 1; j < clause.size(); ++j) { + if (clause.literals[i].atom == clause.literals[j].atom && + clause.literals[i].is_positive != clause.literals[j].is_positive) { + return true; + } + } + } + return false; + } +} \ No newline at end of file diff --git a/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt index d841595..864c0ad 100644 --- a/proofsearch/tests/CMakeLists.txt +++ b/proofsearch/tests/CMakeLists.txt @@ -25,3 +25,4 @@ atp_add_test(test_clausifier test_clausifier.cc) 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) diff --git a/proofsearch/tests/test_simplify.cc b/proofsearch/tests/test_simplify.cc new file mode 100644 index 0000000..07875de --- /dev/null +++ b/proofsearch/tests/test_simplify.cc @@ -0,0 +1,189 @@ +/* + * 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 . + */ + +#include + +#include "atp/core/clause.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/simplify/subsumption.h" +#include "atp/simplify/tautology.h" + +namespace atp { +namespace { + +class SimplifyTest : public ::testing::Test { + protected: + SymbolTable symbols; + TermBank bank{symbols}; + + SymbolId sym_a{}, sym_b{}, sym_c{}; + SymbolId sym_P{}, sym_Q{}, sym_R{}; + SymbolId sym_X{}; + + TermId a{}, b{}, c{}, X{}; + + void SetUp() override { + sym_a = symbols.intern("a", SymbolKind::kConstant); + sym_b = symbols.intern("b", SymbolKind::kConstant); + sym_c = symbols.intern("c", SymbolKind::kConstant); + sym_P = symbols.intern("P", SymbolKind::kPredicate, 1); + sym_Q = symbols.intern("Q", SymbolKind::kPredicate, 1); + sym_R = symbols.intern("R", SymbolKind::kPredicate, 2); + sym_X = symbols.intern("X", SymbolKind::kVariable); + + a = bank.makeTerm(sym_a, {}); + b = bank.makeTerm(sym_b, {}); + c = bank.makeTerm(sym_c, {}); + X = bank.makeVar(sym_X); + } + + TermId P(TermId arg) { return bank.makeTerm(sym_P, {{arg}}); } + TermId Q(TermId arg) { return bank.makeTerm(sym_Q, {{arg}}); } + TermId R(TermId a1, TermId a2) { return bank.makeTerm(sym_R, {{a1, a2}}); } + + Literal pos(TermId atom) { return {.atom = atom, .is_positive = true}; } + Literal neg(TermId atom) { return {.atom = atom, .is_positive = false}; } + + Clause makeClause(std::vector lits) { + Clause cl; + cl.literals = std::move(lits); + return cl; + } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Tautology Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(SimplifyTest, TautologyComplementaryLiterals) { + // {P(a), ¬P(a)} → tautology + Clause cl = makeClause({pos(P(a)), neg(P(a))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, TautologyWithExtraLiterals) { + // {Q(b), P(a), ¬P(a)} → tautology + Clause cl = makeClause({pos(Q(b)), pos(P(a)), neg(P(a))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologySamePolarity) { + // {P(a), P(a)} → NOT tautology (same polarity) + Clause cl = makeClause({pos(P(a)), pos(P(a))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyDifferentAtoms) { + // {P(a), ¬P(b)} → NOT tautology (different atoms) + Clause cl = makeClause({pos(P(a)), neg(P(b))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyDifferentPredicates) { + // {P(a), ¬Q(a)} → NOT tautology (different predicates) + Clause cl = makeClause({pos(P(a)), neg(Q(a))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyEmptyClause) { + Clause cl = makeClause({}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologySingleLiteral) { + Clause cl = makeClause({pos(P(a))}); + EXPECT_FALSE(isTautology(cl)); +} + +TEST_F(SimplifyTest, TautologyVariableAtom) { + // {P(X), ¬P(X)} → tautology (same variable term) + Clause cl = makeClause({pos(P(X)), neg(P(X))}); + EXPECT_TRUE(isTautology(cl)); +} + +TEST_F(SimplifyTest, NotTautologyVarVsConst) { + // {P(X), ¬P(a)} → NOT tautology (syntactically different) + Clause cl = makeClause({pos(P(X)), neg(P(a))}); + EXPECT_FALSE(isTautology(cl)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Subsumption Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(SimplifyTest, SubsumesSubset) { + // {P(a)} subsumes {P(a), Q(b)} + Clause gen = makeClause({pos(P(a))}); + Clause spec = makeClause({pos(P(a)), pos(Q(b))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesIdentical) { + // {P(a), Q(b)} subsumes {P(a), Q(b)} + Clause c1 = makeClause({pos(P(a)), pos(Q(b))}); + Clause c2 = makeClause({pos(P(a)), pos(Q(b))}); + EXPECT_TRUE(subsumes(c1, c2)); +} + +TEST_F(SimplifyTest, SubsumesEmptyClause) { + // {} subsumes everything + Clause empty = makeClause({}); + Clause cl = makeClause({pos(P(a)), neg(Q(b))}); + EXPECT_TRUE(subsumes(empty, cl)); +} + +TEST_F(SimplifyTest, SubsumesNotLarger) { + // {P(a), Q(b)} does NOT subsume {P(a)} + Clause gen = makeClause({pos(P(a)), pos(Q(b))}); + Clause spec = makeClause({pos(P(a))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesRequiresSamePolarity) { + // {P(a)} does NOT subsume {¬P(a)} + Clause gen = makeClause({pos(P(a))}); + Clause spec = makeClause({neg(P(a))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesRequiresSameAtom) { + // {P(a)} does NOT subsume {P(b)} + Clause gen = makeClause({pos(P(a))}); + Clause spec = makeClause({pos(P(b))}); + EXPECT_FALSE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesNegativeLiterals) { + // {¬P(a)} subsumes {¬P(a), Q(b)} + Clause gen = makeClause({neg(P(a))}); + Clause spec = makeClause({neg(P(a)), pos(Q(b))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +TEST_F(SimplifyTest, SubsumesOrderIndependent) { + // {Q(b), P(a)} subsumes {P(a), Q(b), R(a,b)} regardless of order + Clause gen = makeClause({pos(Q(b)), pos(P(a))}); + Clause spec = makeClause({pos(P(a)), pos(Q(b)), pos(R(a, b))}); + EXPECT_TRUE(subsumes(gen, spec)); +} + +} // namespace +} // namespace atp -- cgit v1.2.3 From 9b7cca2bf9783f104dcc549cd68d0a8f62088a6b Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 04:53:55 +0800 Subject: feat: implement proof trace extraction and add proof trace test --- proofsearch/include/atp/proof/proof_trace.h | 19 +-- proofsearch/src/proof/proof_trace.cc | 135 +++++++++++++++++ proofsearch/tests/CMakeLists.txt | 2 + proofsearch/tests/test_proof_trace.cc | 218 ++++++++++++++++++++++++++++ 4 files changed, 365 insertions(+), 9 deletions(-) create mode 100644 proofsearch/tests/test_proof_trace.cc (limited to 'proofsearch/tests/CMakeLists.txt') diff --git a/proofsearch/include/atp/proof/proof_trace.h b/proofsearch/include/atp/proof/proof_trace.h index cda6c5b..a80a327 100644 --- a/proofsearch/include/atp/proof/proof_trace.h +++ b/proofsearch/include/atp/proof/proof_trace.h @@ -16,14 +16,10 @@ * along with this program. If not, see . */ - #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 extractProof(const ClauseStore& store, ClauseId empty_clause_id, - const TermBank& bank); +/// Returns steps in topological order: axioms first, empty clause last. +std::vector 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& proof, const TermBank& bank); +std::string formatProof(const std::vector& proof, + const ClauseStore& store, const TermBank& bank); } // namespace atp diff --git a/proofsearch/src/proof/proof_trace.cc b/proofsearch/src/proof/proof_trace.cc index b62ffd0..b1b4343 100644 --- a/proofsearch/src/proof/proof_trace.cc +++ b/proofsearch/src/proof/proof_trace.cc @@ -16,4 +16,139 @@ * along with this program. If not, see . */ +#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 +#include +#include +#include +#include + +namespace atp { + +// ─── extractProof ──────────────────────────────────────────────────────────── +// DFS from empty clause back to axioms, collect all participating clauses, +// then reverse for topological order (axioms first). + +std::vector extractProof(const ClauseStore& store, ClauseId empty_clause_id) { + std::vector steps; + std::unordered_set visited; + std::stack 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& 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/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt index 864c0ad..eea0ceb 100644 --- a/proofsearch/tests/CMakeLists.txt +++ b/proofsearch/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/proofsearch/tests/test_proof_trace.cc b/proofsearch/tests/test_proof_trace.cc new file mode 100644 index 0000000..d7ff246 --- /dev/null +++ b/proofsearch/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 . + */ + +#include + +#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 + +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 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 -- cgit v1.2.3 From a26a9311ed6cc34860092252d1750428b741b116 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Wed, 8 Apr 2026 03:23:16 +0800 Subject: feat: enhance clang-tidy configuration and improve code quality across multiple files --- proofsearch/.clang-tidy | 8 ++ proofsearch/CMakeLists.txt | 13 +- proofsearch/include/atp/core/term_bank.h | 11 +- proofsearch/include/atp/frontend/tptp_parser.h | 2 +- proofsearch/include/atp/search/prover.h | 9 ++ proofsearch/src/core/term_bank.cc | 2 +- proofsearch/src/frontend/tptp_parser.cc | 57 ++++---- proofsearch/src/infer/resolution.cc | 2 +- proofsearch/src/infer/substitution.cc | 9 +- proofsearch/src/main.cc | 16 +-- proofsearch/src/proof/proof_trace.cc | 50 ++++--- proofsearch/src/search/prover.cc | 177 ++++++++++++------------- proofsearch/tests/CMakeLists.txt | 1 + 13 files changed, 198 insertions(+), 159 deletions(-) (limited to 'proofsearch/tests/CMakeLists.txt') diff --git a/proofsearch/.clang-tidy b/proofsearch/.clang-tidy index 227c129..412e8a8 100644 --- a/proofsearch/.clang-tidy +++ b/proofsearch/.clang-tidy @@ -10,11 +10,13 @@ Checks: > -bugprone-easily-swappable-parameters, clang-analyzer-*, cppcoreguidelines-*, + -cppcoreguidelines-avoid-const-or-ref-data-members, -cppcoreguidelines-avoid-magic-numbers, -cppcoreguidelines-pro-type-reinterpret-cast, -cppcoreguidelines-pro-bounds-pointer-arithmetic, -cppcoreguidelines-owning-memory, misc-*, + -misc-no-recursion, -misc-non-private-member-variables-in-classes, modernize-*, -modernize-use-trailing-return-type, @@ -46,6 +48,12 @@ CheckOptions: value: CamelCase - key: readability-identifier-naming.ConstantPrefix value: k + - key: readability-identifier-naming.LocalConstantCase + value: lower_case + - key: readability-identifier-naming.LocalConstantPrefix + value: '' + - key: readability-identifier-naming.LocalConstantSuffix + value: '' - key: readability-identifier-naming.EnumConstantCase value: CamelCase - key: readability-identifier-naming.EnumConstantPrefix diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt index 1b6473e..2257766 100644 --- a/proofsearch/CMakeLists.txt +++ b/proofsearch/CMakeLists.txt @@ -12,8 +12,8 @@ set(CMAKE_CXX_EXTENSIONS OFF) # Export compile_commands.json for clang-tidy and IDE support set(CMAKE_EXPORT_COMPILE_COMMANDS ON) -# ─── Compiler Warnings ────────────────────────────────────────────────────── -add_compile_options( +# ─── Compiler Warnings ────────────────────────── +set(ATP_PROJECT_WARNING_FLAGS -Wall -Wextra -Wpedantic -Wshadow -Wnon-virtual-dtor -Wold-style-cast -Wcast-align -Wunused @@ -34,7 +34,6 @@ option(ATP_ENABLE_CLANG_TIDY "Enable clang-tidy static analysis" OFF) if(ATP_ENABLE_CLANG_TIDY) find_program(CLANG_TIDY_EXE NAMES clang-tidy) if(CLANG_TIDY_EXE) - set(CMAKE_CXX_CLANG_TIDY "${CLANG_TIDY_EXE}") message(STATUS "clang-tidy found: ${CLANG_TIDY_EXE}") else() message(WARNING "clang-tidy requested but not found") @@ -91,10 +90,18 @@ add_library(atp_core STATIC ${ATP_SOURCES}) target_include_directories(atp_core PUBLIC ${PROJECT_SOURCE_DIR}/include ) +target_compile_options(atp_core PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) +if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE) + set_property(TARGET atp_core PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}") +endif() # ─── Main Executable ──────────────────────────────────────────────────────── add_executable(atp src/main.cc) target_link_libraries(atp PRIVATE atp_core) +target_compile_options(atp PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) +if(ATP_ENABLE_CLANG_TIDY AND CLANG_TIDY_EXE) + set_property(TARGET atp PROPERTY CXX_CLANG_TIDY "${CLANG_TIDY_EXE}") +endif() # ─── Tests ─────────────────────────────────────────────────────────────────── option(ATP_BUILD_TESTS "Build unit tests" ON) diff --git a/proofsearch/include/atp/core/term_bank.h b/proofsearch/include/atp/core/term_bank.h index 3339ceb..ca12759 100644 --- a/proofsearch/include/atp/core/term_bank.h +++ b/proofsearch/include/atp/core/term_bank.h @@ -39,7 +39,7 @@ class TermBank { public: /// TermBank needs the SymbolTable to distinguish variables from constants /// (both have 0 args, but SymbolKind differs). - explicit TermBank(const SymbolTable& symbols) : symbols_(symbols) {} + explicit TermBank(SymbolTable& symbols) : symbols_(&symbols) {} /// Create or retrieve a term. Returns the canonical TermId. TermId makeTerm(SymbolId symbol, std::span args); @@ -57,7 +57,8 @@ class TermBank { [[nodiscard]] size_t size() const; /// Access the underlying SymbolTable. - [[nodiscard]] const SymbolTable& symbols() const { return symbols_; } + [[nodiscard]] const SymbolTable& symbols() const { return *symbols_; } + [[nodiscard]] SymbolTable& mutableSymbols() { return *symbols_; } private: struct TermKey { @@ -70,14 +71,14 @@ class TermBank { struct TermKeyHash { size_t operator()(const TermKey& key) const { size_t seed = std::hash{}(key.symbol_); - for (const TermId kArg : key.args_) { - seed ^= std::hash{}(kArg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); + for (const TermId arg : key.args_) { + seed ^= std::hash{}(arg) + 0x9e3779b9 + (seed << 6) + (seed >> 2); } return seed; } }; - const SymbolTable& symbols_; + SymbolTable* symbols_; std::vector terms_; std::unordered_map term_to_id_; }; diff --git a/proofsearch/include/atp/frontend/tptp_parser.h b/proofsearch/include/atp/frontend/tptp_parser.h index 89eab6b..68a5564 100644 --- a/proofsearch/include/atp/frontend/tptp_parser.h +++ b/proofsearch/include/atp/frontend/tptp_parser.h @@ -59,7 +59,7 @@ FormulaRole parseRole(std::string_view role_str); /// A parsed TPTP formula with its name and role. struct AnnotatedFormula { std::string name_; ///< Formula name (e.g., "axiom1") - FormulaRole role_; ///< Semantic role + FormulaRole role_ = FormulaRole::kPlain; ///< Semantic role std::unique_ptr formula_; ///< The FOL formula (for fof(...)) std::vector clauses_; ///< Direct clauses (for cnf(...)) bool is_cnf_ = false; ///< true if input was cnf(), false if fof() diff --git a/proofsearch/include/atp/search/prover.h b/proofsearch/include/atp/search/prover.h index c1246ae..65ec7f0 100644 --- a/proofsearch/include/atp/search/prover.h +++ b/proofsearch/include/atp/search/prover.h @@ -72,6 +72,15 @@ class Prover { [[nodiscard]] const ClauseStore& clauseStore() const { return store_; } private: + [[nodiscard]] bool hitResourceLimit(size_t iterations) const; + [[nodiscard]] Clause popGivenClause(); + [[nodiscard]] bool isForwardSubsumedByProcessed(const Clause& clause) const; + [[nodiscard]] bool shouldSkipGiven(const Clause& given) const; + void applyBackwardSubsumption(const Clause& given); + [[nodiscard]] std::vector generateNewClauses(const Clause& given) const; + [[nodiscard]] uint16_t computeDepth(const Clause& clause) const; + [[nodiscard]] std::optional processNewClauses(std::vector new_clauses); + TermBank& bank_; ClauseStore& store_; ProverConfig config_; diff --git a/proofsearch/src/core/term_bank.cc b/proofsearch/src/core/term_bank.cc index 2e117b3..0dc166f 100644 --- a/proofsearch/src/core/term_bank.cc +++ b/proofsearch/src/core/term_bank.cc @@ -53,7 +53,7 @@ const Term& TermBank::getTerm(TermId id) const { bool TermBank::isVariable(TermId id) const { assert(id < terms_.size() && "TermId out of bounds!"); - return symbols_.isVariable(terms_[id].symbol_id_); + return symbols_->isVariable(terms_[id].symbol_id_); } size_t TermBank::size() const { diff --git a/proofsearch/src/frontend/tptp_parser.cc b/proofsearch/src/frontend/tptp_parser.cc index ddf8aad..10190b8 100644 --- a/proofsearch/src/frontend/tptp_parser.cc +++ b/proofsearch/src/frontend/tptp_parser.cc @@ -42,31 +42,31 @@ namespace atp { FormulaRole parseRole(std::string_view role_str) { if (role_str == "axiom") { return FormulaRole::kAxiom; -} + } if (role_str == "hypothesis") { return FormulaRole::kHypothesis; -} + } if (role_str == "definition") { return FormulaRole::kDefinition; -} + } if (role_str == "assumption") { return FormulaRole::kAssumption; -} + } if (role_str == "lemma") { return FormulaRole::kLemma; -} + } if (role_str == "theorem") { return FormulaRole::kTheorem; -} + } if (role_str == "conjecture") { return FormulaRole::kConjecture; -} + } if (role_str == "negated_conjecture") { return FormulaRole::kNegatedConjecture; -} + } if (role_str == "plain") { return FormulaRole::kPlain; -} + } return FormulaRole::kPlain; } @@ -215,7 +215,7 @@ class TptpParser { SymbolTable& symbols_; Token current_token_{}; std::vector tokens_; - std::unordered_map variable_cache_{}; + std::unordered_map variable_cache_; void advance() { current_token_ = lexer_.nextToken(); } @@ -252,27 +252,28 @@ class TptpParser { TermId const var_id = bank_.makeVar(sym); variable_cache_[name] = var_id; return var_id; - } // Check if this is a function/predicate (has args) or a constant (no parens) - if (current_token_.type_ == TokenType::kLParen) { - advance(); // consume '(' - std::vector args; - if (current_token_.type_ != TokenType::kRParen) { + } + + // Check if this is a function/predicate (has args) or a constant (no parens) + if (current_token_.type_ == TokenType::kLParen) { + advance(); // consume '(' + std::vector args; + if (current_token_.type_ != TokenType::kRParen) { + args.push_back(parseTerm()); + while (current_token_.type_ == TokenType::kComma) { + advance(); args.push_back(parseTerm()); - while (current_token_.type_ == TokenType::kComma) { - advance(); - args.push_back(parseTerm()); - } } - expect(TokenType::kRParen); - SymbolId sym = symbols_.intern(name, SymbolKind::kFunction, - static_cast(args.size())); - return bank_.makeTerm(sym, args); - } else { - // Constant: no parentheses (e.g., a, b, h0, s0) - SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0); - return bank_.makeTerm(sym, {}); } - + expect(TokenType::kRParen); + const SymbolId sym = symbols_.intern(name, SymbolKind::kFunction, + static_cast(args.size())); + return bank_.makeTerm(sym, args); + } + + // Constant: no parentheses (e.g., a, b, h0, s0) + const SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0); + return bank_.makeTerm(sym, {}); } Literal parseLiteral() { diff --git a/proofsearch/src/infer/resolution.cc b/proofsearch/src/infer/resolution.cc index 82e59b7..5fb0d4a 100644 --- a/proofsearch/src/infer/resolution.cc +++ b/proofsearch/src/infer/resolution.cc @@ -98,7 +98,7 @@ std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, // Rename c2's variables to avoid clashes with c1 // Use a static counter — safe for single-threaded prover static uint32_t var_counter = 0; - auto& symbols = const_cast(bank.symbols()); + auto& symbols = bank.mutableSymbols(); Clause c2r = renameVariables(c2, bank, symbols, var_counter); // Unify the complementary atoms diff --git a/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc index 8710fb0..584008b 100644 --- a/proofsearch/src/infer/substitution.cc +++ b/proofsearch/src/infer/substitution.cc @@ -22,6 +22,7 @@ #include "atp/core/term_bank.h" #include "atp/core/types.h" +#include #include namespace atp { @@ -107,12 +108,8 @@ bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const } const Term& t = bank.getTerm(term); - for (TermId const arg : t.args_) { - if (occursIn(var, arg, bank)) { - return true; - } - } - return false; + return std::any_of(t.args_.begin(), t.args_.end(), + [&](TermId arg) { return occursIn(var, arg, bank); }); } void Substitution::clear() { diff --git a/proofsearch/src/main.cc b/proofsearch/src/main.cc index 81dbc91..c683d39 100644 --- a/proofsearch/src/main.cc +++ b/proofsearch/src/main.cc @@ -43,7 +43,7 @@ int main(int argc, char* argv[]) { return EXIT_FAILURE; } - const std::string kFilepath = argv[1]; + const std::string filepath = argv[1]; try { // 1. Initialize core modules @@ -52,9 +52,9 @@ int main(int argc, char* argv[]) { atp::ClauseStore store; // 2. Parse TPTP input - auto problem = atp::parseTptpFile(kFilepath, bank, symbols); + auto problem = atp::parseTptpFile(filepath, bank, symbols); - std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << kFilepath + std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << filepath << "\n"; // 3. Prepare clauses for proving @@ -70,23 +70,23 @@ int main(int argc, char* argv[]) { // 5. Output result (SZS format) switch (result) { case atp::ProverResult::kTheorem: { - std::cout << "% SZS status Theorem for " << kFilepath << "\n\n"; + 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 " << kFilepath << "\n"; + std::cout << "% SZS output start Proof for " << filepath << "\n"; std::cout << atp::formatProof(proof, store, bank); - std::cout << "% SZS output end Proof for " << kFilepath << "\n"; + std::cout << "% SZS output end Proof for " << filepath << "\n"; } break; } case atp::ProverResult::kSaturation: - std::cout << "% SZS status Satisfiable for " << kFilepath << "\n"; + std::cout << "% SZS status Satisfiable for " << filepath << "\n"; break; case atp::ProverResult::kTimeout: - std::cout << "% SZS status Timeout for " << kFilepath << "\n"; + std::cout << "% SZS status Timeout for " << filepath << "\n"; break; } diff --git a/proofsearch/src/proof/proof_trace.cc b/proofsearch/src/proof/proof_trace.cc index a0d5a11..5fa4b04 100644 --- a/proofsearch/src/proof/proof_trace.cc +++ b/proofsearch/src/proof/proof_trace.cc @@ -26,7 +26,6 @@ #include "atp/core/types.h" #include -#include #include #include #include @@ -47,20 +46,20 @@ std::vector extractProof(const ClauseStore& store, ClauseId empty_cla worklist.push(empty_clause_id); while (!worklist.empty()) { - const ClauseId kCid = worklist.top(); + const ClauseId cid = worklist.top(); worklist.pop(); - if (kCid == kInvalidId) { + if (cid == kInvalidId) { continue; } - if (visited.contains(kCid)) { + if (visited.contains(cid)) { continue; } - visited.insert(kCid); + visited.insert(cid); - const Clause& c = store.getClause(kCid); + const Clause& c = store.getClause(cid); steps.push_back({ - .clause_id_ = kCid, + .clause_id_ = cid, .rule_ = c.rule_, .parent1_ = c.parent1_, .parent2_ = c.parent2_, @@ -105,15 +104,32 @@ namespace { /// Generate a human-readable variable name from an index. /// 0→X, 1→Y, 2→Z, 3→W, 4→V, 5→U, 6→X1, 7→Y1, ... std::string prettyVarName(size_t index) { - static constexpr std::array kBaseNames = {'X', 'Y', 'Z', 'W', 'V', 'U'}; - static constexpr size_t kBaseCount = kBaseNames.size(); + constexpr size_t kBaseCount = 6; + const size_t base_index = index % kBaseCount; + const char base = [&]() { + switch (base_index) { + case 0: + return 'X'; + case 1: + return 'Y'; + case 2: + return 'Z'; + case 3: + return 'W'; + case 4: + return 'V'; + case 5: + return 'U'; + default: + return 'X'; + } + }(); - const char kBase = kBaseNames[index % kBaseCount]; - const size_t kSuffix = index / kBaseCount; - if (kSuffix == 0) { - return std::string{kBase}; + const size_t suffix = index / kBaseCount; + if (suffix == 0) { + return std::string{base}; } - return std::string{kBase} + std::to_string(kSuffix); + return std::string{base} + std::to_string(suffix); } /// Pretty-print a term, renaming variables to readable names. @@ -125,9 +141,9 @@ std::string termToPretty(TermId id, const TermBank& bank, if (it != var_map.end()) { return it->second; } - const std::string kName = prettyVarName(var_map.size()); - var_map[id] = kName; - return kName; + const std::string name = prettyVarName(var_map.size()); + var_map[id] = name; + return name; } const Term& t = bank.getTerm(id); diff --git a/proofsearch/src/search/prover.cc b/proofsearch/src/search/prover.cc index 2c2de40..f3f8bb0 100644 --- a/proofsearch/src/search/prover.cc +++ b/proofsearch/src/search/prover.cc @@ -47,114 +47,113 @@ void Prover::addClauses(std::vector clauses) { } } +bool Prover::hitResourceLimit(size_t iterations) const { + return iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_; +} + +Clause Prover::popGivenClause() { + Clause given = unprocessed_.top(); + unprocessed_.pop(); + return given; +} + +bool Prover::isForwardSubsumedByProcessed(const Clause& clause) const { + return std::ranges::any_of(processed_, + [&](ClauseId pid) { return subsumes(store_.getClause(pid), clause); }); +} + +bool Prover::shouldSkipGiven(const Clause& given) const { + return isTautology(given) || isForwardSubsumedByProcessed(given); +} + +void Prover::applyBackwardSubsumption(const Clause& given) { + std::erase_if(processed_, [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); }); +} + +std::vector Prover::generateNewClauses(const Clause& given) const { + std::vector new_clauses; + const UnificationConfig uconfig{.enable_occurs_check_ = config_.enable_occurs_check_}; + + for (ClauseId const pid : processed_) { + const Clause& pc = store_.getClause(pid); + + auto resolvents1 = allResolvents(bank_, given, pc, uconfig); + auto resolvents2 = allResolvents(bank_, pc, given, uconfig); + + for (auto& r : resolvents1) { + new_clauses.push_back(std::move(r)); + } + for (auto& r : resolvents2) { + new_clauses.push_back(std::move(r)); + } + } + + auto factors = factor(bank_, given, uconfig); + for (auto& f : factors) { + new_clauses.push_back(std::move(f)); + } + + return new_clauses; +} + +uint16_t Prover::computeDepth(const Clause& clause) const { + uint32_t const d1 = (clause.parent1_ != kInvalidId) ? store_.getClause(clause.parent1_).depth_ : 0; + uint32_t const d2 = (clause.parent2_ != kInvalidId) ? store_.getClause(clause.parent2_).depth_ : 0; + return static_cast(std::max(d1, d2) + 1); +} + +std::optional Prover::processNewClauses(std::vector new_clauses) { + for (auto& nc : new_clauses) { + if (nc.isEmpty()) { + return store_.addClause(std::move(nc)); + } + + if (isTautology(nc)) { + continue; + } + + nc.depth_ = computeDepth(nc); + + ClauseId const nid = store_.addClause(nc); + const Clause& stored_nc = store_.getClause(nid); + if (isForwardSubsumedByProcessed(stored_nc)) { + continue; + } + + unprocessed_.push(stored_nc); + } + + return std::nullopt; +} + ProverResult Prover::prove() { size_t iterations = 0; while (!unprocessed_.empty()) { - // Resource limits - if (iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_) { + if (hitResourceLimit(iterations)) { return ProverResult::kTimeout; } ++iterations; - // 1. Select the best clause from unprocessed - Clause given = unprocessed_.top(); - unprocessed_.pop(); + Clause given = popGivenClause(); - // 2. Check if given is itself the empty clause if (given.isEmpty()) { empty_clause_id_ = given.id_; return ProverResult::kTheorem; } - // 3. Forward redundancy checks - if (isTautology(given)) { - continue; - } - - bool forward_subsumed = false; - for (ClauseId const pid : processed_) { - if (subsumes(store_.getClause(pid), given)) { - forward_subsumed = true; - break; - } - } - if (forward_subsumed) { + if (shouldSkipGiven(given)) { continue; } - // 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 - // Inference BEFORE adding given to processed — matches doc §4.6. - std::vector new_clauses; - const UnificationConfig kUconfig{.enable_occurs_check_ = config_.enable_occurs_check_}; - - // 5a. Resolve given with every processed clause (both directions) - for (ClauseId const pid : processed_) { - const Clause& pc = store_.getClause(pid); - - auto resolvents1 = allResolvents(bank_, given, pc, kUconfig); - auto resolvents2 = allResolvents(bank_, pc, given, kUconfig); - - for (auto& r : resolvents1) { - new_clauses.push_back(std::move(r)); - } - for (auto& r : resolvents2) { - new_clauses.push_back(std::move(r)); - } - } - - // 5b. Factor given (only once) - auto factors = factor(bank_, given, kUconfig); - for (auto& f : factors) { - new_clauses.push_back(std::move(f)); - } - - // 6. Add given to processed AFTER inference + applyBackwardSubsumption(given); + std::vector new_clauses = generateNewClauses(given); processed_.push_back(given.id_); - // 7. Process new clauses - for (auto& nc : new_clauses) { - // 7a. Check for empty clause → proof found! - if (nc.isEmpty()) { - ClauseId eid = store_.addClause(std::move(nc)); - empty_clause_id_ = eid; - return ProverResult::kTheorem; - } - - // 7b. Skip tautologies - if (isTautology(nc)) { - continue; - } - - // 7c. Set depth - uint32_t const d1 = (nc.parent1_ != kInvalidId) ? store_.getClause(nc.parent1_).depth_ : 0; - uint32_t const d2 = (nc.parent2_ != kInvalidId) ? store_.getClause(nc.parent2_).depth_ : 0; - nc.depth_ = static_cast(std::max(d1, d2) + 1); - - // 7d. Store the clause (needed for forward subsumption check) - ClauseId const nid = store_.addClause(nc); - const Clause& stored_nc = store_.getClause(nid); - - // 7e. Forward subsumption on new clause - bool new_subsumed = false; - for (ClauseId const pid : processed_) { - if (subsumes(store_.getClause(pid), stored_nc)) { - new_subsumed = true; - break; - } - } - if (new_subsumed) { - continue; - } - - // 7f. Enqueue - unprocessed_.push(stored_nc); + const std::optional derived_empty = processNewClauses(std::move(new_clauses)); + if (derived_empty.has_value()) { + empty_clause_id_ = derived_empty; + return ProverResult::kTheorem; } } diff --git a/proofsearch/tests/CMakeLists.txt b/proofsearch/tests/CMakeLists.txt index eea0ceb..184357b 100644 --- a/proofsearch/tests/CMakeLists.txt +++ b/proofsearch/tests/CMakeLists.txt @@ -15,6 +15,7 @@ include(GoogleTest) function(atp_add_test TEST_NAME TEST_SOURCE) add_executable(${TEST_NAME} ${TEST_SOURCE}) target_link_libraries(${TEST_NAME} PRIVATE atp_core GTest::gtest_main) + target_compile_options(${TEST_NAME} PRIVATE ${ATP_PROJECT_WARNING_FLAGS}) gtest_discover_tests(${TEST_NAME}) endfunction() -- cgit v1.2.3