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/CMakeLists.txt | 102 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 102 insertions(+) create mode 100644 proofsearch/CMakeLists.txt (limited to 'proofsearch/CMakeLists.txt') diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt new file mode 100644 index 0000000..2cf69db --- /dev/null +++ b/proofsearch/CMakeLists.txt @@ -0,0 +1,102 @@ +cmake_minimum_required(VERSION 3.20) +project(atp_engine + VERSION 0.1.0 + LANGUAGES CXX +) + +# ─── C++ Standard ──────────────────────────────────────────────────────────── +set(CMAKE_CXX_STANDARD 20) +set(CMAKE_CXX_STANDARD_REQUIRED ON) +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( + -Wall -Wextra -Wpedantic + -Wshadow -Wnon-virtual-dtor + -Wold-style-cast -Wcast-align -Wunused + -Woverloaded-virtual -Wconversion -Wsign-conversion + -Wnull-dereference -Wdouble-promotion + -Wformat=2 -Wimplicit-fallthrough +) + +# ─── Sanitizers (Debug builds) ─────────────────────────────────────────────── +option(ATP_ENABLE_SANITIZERS "Enable ASan + UBSan in Debug builds" ON) +if(ATP_ENABLE_SANITIZERS AND CMAKE_BUILD_TYPE STREQUAL "Debug") + add_compile_options(-fsanitize=address,undefined -fno-omit-frame-pointer) + add_link_options(-fsanitize=address,undefined) +endif() + +# ─── clang-tidy Integration ───────────────────────────────────────────────── +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") + endif() +endif() + +# ─── clang-format Custom Target ───────────────────────────────────────────── +find_program(CLANG_FORMAT_EXE NAMES clang-format) +if(CLANG_FORMAT_EXE) + file(GLOB_RECURSE ALL_CXX_SOURCES + ${PROJECT_SOURCE_DIR}/src/*.cc + ${PROJECT_SOURCE_DIR}/include/*.h + ${PROJECT_SOURCE_DIR}/tests/*.cc + ) + add_custom_target(format + COMMAND ${CLANG_FORMAT_EXE} -i ${ALL_CXX_SOURCES} + COMMENT "Running clang-format on all source files" + VERBATIM + ) + add_custom_target(format-check + COMMAND ${CLANG_FORMAT_EXE} --dry-run --Werror ${ALL_CXX_SOURCES} + COMMENT "Checking clang-format compliance" + VERBATIM + ) + message(STATUS "clang-format found: ${CLANG_FORMAT_EXE}") + message(STATUS " Use 'cmake --build . --target format' to auto-format") + message(STATUS " Use 'cmake --build . --target format-check' to check format") +else() + message(WARNING "clang-format not found, format targets disabled") +endif() + +# ─── Source Files ──────────────────────────────────────────────────────────── +set(ATP_SOURCES + src/core/symbol_table.cc + src/core/term_bank.cc + src/core/clause_store.cc + src/normalize/clausifier.cc + src/infer/unification.cc + src/infer/resolution.cc + src/index/discrim_tree.cc + src/simplify/subsumption.cc + src/search/prover.cc + src/proof/proof_trace.cc + src/rewrite/ordering.cc + src/rewrite/paramodulation.cc + src/strategy/problem_analyzer.cc + src/frontend/tptp_parser.cc +) + +# ─── Core Library ──────────────────────────────────────────────────────────── +add_library(atp_core STATIC ${ATP_SOURCES}) +target_include_directories(atp_core PUBLIC + ${PROJECT_SOURCE_DIR}/include +) + +# ─── Main Executable ──────────────────────────────────────────────────────── +add_executable(atp src/main.cc) +target_link_libraries(atp PRIVATE atp_core) + +# ─── Tests ─────────────────────────────────────────────────────────────────── +option(ATP_BUILD_TESTS "Build unit tests" ON) +if(ATP_BUILD_TESTS) + enable_testing() + add_subdirectory(tests) +endif() -- cgit v1.2.3 From df6c2f124fce4cecd42da806a003afdf3a922c09 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Fri, 3 Apr 2026 14:21:40 +0800 Subject: feat: implement substitution logic and unify/applySubstitution functions for term resolution --- proofsearch/CMakeLists.txt | 1 + proofsearch/include/atp/infer/substitution.h | 42 +++- proofsearch/include/atp/infer/unification.h | 4 + proofsearch/src/infer/substitution.cc | 119 ++++++++++ proofsearch/src/infer/unification.cc | 68 ++++++ proofsearch/tests/test_unification.cc | 337 +++++++++++++++++++++++++++ 6 files changed, 561 insertions(+), 10 deletions(-) create mode 100644 proofsearch/src/infer/substitution.cc (limited to 'proofsearch/CMakeLists.txt') diff --git a/proofsearch/CMakeLists.txt b/proofsearch/CMakeLists.txt index 2cf69db..edeb6b7 100644 --- a/proofsearch/CMakeLists.txt +++ b/proofsearch/CMakeLists.txt @@ -72,6 +72,7 @@ set(ATP_SOURCES src/core/term_bank.cc src/core/clause_store.cc src/normalize/clausifier.cc + src/infer/substitution.cc src/infer/unification.cc src/infer/resolution.cc src/index/discrim_tree.cc diff --git a/proofsearch/include/atp/infer/substitution.h b/proofsearch/include/atp/infer/substitution.h index f9f562a..671f6d7 100644 --- a/proofsearch/include/atp/infer/substitution.h +++ b/proofsearch/include/atp/infer/substitution.h @@ -16,39 +16,61 @@ * along with this program. If not, see . */ - #pragma once /// @file substitution.h /// @brief Variable binding map: Var -> Term. +/// +/// Short-lived object created during unification, applied to build resolvents, +/// then discarded. Never stored long-term. +#include "atp/core/term_bank.h" #include "atp/core/types.h" -#include +#include namespace atp { -/// A substitution is a mapping from variable TermIds to their bound TermIds. -/// Designed as a short-lived, stack-allocated object during unification. +/// A substitution σ maps variable TermIds to their bound TermIds. +/// +/// Example: σ = { X → f(a), Y → Z } +/// lookup(X) = f(a) (direct binding) +/// resolve(X) = f(a) (same — f(a) is not a variable) +/// resolve(Y) = Z (if Z is unbound, stops at Z) +/// resolve(Y) = f(b) (if Z → f(b) also in σ, walks the chain) class Substitution { public: Substitution() = default; - /// Bind a variable to a term. Returns false if already bound to something different. + /// Bind a variable to a term. Returns false if already bound to a different term. bool bind(TermId var, TermId term); - /// Look up what a variable is bound to. Returns kInvalidId if unbound. + /// Look up what a variable is directly bound to. Returns kInvalidId if unbound. [[nodiscard]] TermId lookup(TermId var) const; - /// Walk the binding chain to the final bound value. - [[nodiscard]] TermId resolve(TermId id) const; + /// Walk the binding chain to the final value. + /// If var → Y → f(a), returns f(a). + /// Requires TermBank to check whether intermediate values are variables. + [[nodiscard]] TermId resolve(TermId id, const TermBank& bank) const; + + /// Apply this substitution to a term recursively, creating new terms in the bank. + /// Free (unbound) variables are left as-is. + [[nodiscard]] TermId apply(TermId term, TermBank& bank) const; + + /// Check if a variable occurs anywhere inside a term (for occurs check). + [[nodiscard]] bool occursIn(TermId var, TermId term, const TermBank& bank) const; /// Clear all bindings. void clear(); + /// Number of bindings. + [[nodiscard]] size_t size() const { return bindings_.size(); } + + /// Check if empty. + [[nodiscard]] bool empty() const { return bindings_.empty(); } + private: - // TODO: Phase 2 implementation - std::vector> bindings_; + std::unordered_map bindings_; }; } // namespace atp diff --git a/proofsearch/include/atp/infer/unification.h b/proofsearch/include/atp/infer/unification.h index 7d91aaf..f2ea180 100644 --- a/proofsearch/include/atp/infer/unification.h +++ b/proofsearch/include/atp/infer/unification.h @@ -37,4 +37,8 @@ struct UnificationConfig { bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, const UnificationConfig& config = {}); +/// Apply a substitution to a term recursively, creating new terms in the bank. +/// Free (unbound) variables are left unchanged. +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank); + } // namespace atp diff --git a/proofsearch/src/infer/substitution.cc b/proofsearch/src/infer/substitution.cc new file mode 100644 index 0000000..c570676 --- /dev/null +++ b/proofsearch/src/infer/substitution.cc @@ -0,0 +1,119 @@ +/* + * 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/infer/substitution.h" +#include "atp/core/term.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +namespace atp { + +bool Substitution::bind(TermId var, TermId term) { + auto [it, inserted] = bindings_.emplace(var, term); + if (!inserted) { + // Already bound — succeed only if bound to the same term + return it->second == term; + } + return true; +} + +TermId Substitution::lookup(TermId var) const { + auto it = bindings_.find(var); + if (it != bindings_.end()) { + return it->second; + } + return kInvalidId; +} + +TermId Substitution::resolve(TermId id, const TermBank& bank) const { + // Walk the chain: X → Y → Z → f(a) + // Stop when we hit a non-variable or an unbound variable. + while (bank.isVariable(id)) { + auto it = bindings_.find(id); + if (it == bindings_.end()) { + break; // Unbound variable — stop here + } + id = it->second; + } + return id; +} + +TermId Substitution::apply(TermId term, TermBank& bank) const { + // First, resolve through variable chain + term = resolve(term, bank); + + if (bank.isVariable(term)) { + // Free variable (unbound) — leave as-is + return term; + } + + // IMPORTANT: Copy symbol_id and args BEFORE recursing. + // Recursive apply() calls may trigger bank.makeTerm() → realloc → dangling ref. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! + + if (old_args.empty()) { + // Constant or 0-arity — no substitution needed + return term; + } + + // Recursively apply to all arguments + std::vector new_args; + new_args.reserve(old_args.size()); + bool changed = false; + for (TermId arg : old_args) { + TermId new_arg = apply(arg, bank); + new_args.push_back(new_arg); + if (new_arg != arg) { + changed = true; + } + } + + if (!changed) { + return term; + } + + return bank.makeTerm(sym, new_args); +} + +bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const { + term = resolve(term, bank); + + if (var == term) { + return true; + } + + if (bank.isVariable(term)) { + return false; // Different unbound variable + } + + const Term& t = bank.getTerm(term); + for (TermId arg : t.args) { + if (occursIn(var, arg, bank)) { + return true; + } + } + return false; +} + +void Substitution::clear() { + bindings_.clear(); +} + +} // namespace atp \ No newline at end of file diff --git a/proofsearch/src/infer/unification.cc b/proofsearch/src/infer/unification.cc index b62ffd0..be8a025 100644 --- a/proofsearch/src/infer/unification.cc +++ b/proofsearch/src/infer/unification.cc @@ -17,3 +17,71 @@ */ +#include "atp/infer/unification.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" + +namespace atp { + + bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config) { + t1 = subst.resolve(t1, bank); + t2 = subst.resolve(t2, bank); + + if (t1 == t2) { + return true; + } + + if (bank.isVariable(t1)) { + if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { + return false; + } + subst.bind(t1, t2); + return true; + } + + if (bank.isVariable(t2)) { + if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { + return false; + } + subst.bind(t2, t1); + return true; + } + + const Term& term1 = bank.getTerm(t1); + const Term& term2 = bank.getTerm(t2); + + if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + return false; + } + + for (size_t i = 0; i < term1.arity(); ++i) { + if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { + return false; + } + } + + return true; + } + + TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { + term = subst.resolve(term, bank); + if (bank.isVariable(term)) { + return term; + } + + // IMPORTANT: Copy args and symbol_id BEFORE recursing. + // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! + + std::vector new_args; + new_args.reserve(old_args.size()); + for (TermId arg : old_args) { + new_args.push_back(applySubstitution(subst, arg, bank)); + } + return bank.makeTerm(sym, new_args); + } + +} // namespace atp \ No newline at end of file diff --git a/proofsearch/tests/test_unification.cc b/proofsearch/tests/test_unification.cc index b62ffd0..3ee6f00 100644 --- a/proofsearch/tests/test_unification.cc +++ b/proofsearch/tests/test_unification.cc @@ -16,4 +16,341 @@ * along with this program. If not, see . */ +#include +#include "atp/core/symbol_table.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" +#include "atp/infer/substitution.h" +#include "atp/infer/unification.h" + +namespace atp { +namespace { + +// ═══════════════════════════════════════════════════════════════════════════ +// Test Fixture +// ═══════════════════════════════════════════════════════════════════════════ + +class UnificationTest : public ::testing::Test { + protected: + SymbolTable symbols; + TermBank bank{symbols}; + + // Symbols + SymbolId sym_a{}, sym_b{}, sym_c{}; + SymbolId sym_f{}, sym_g{}, sym_h{}; + SymbolId sym_P{}; + SymbolId sym_X{}, sym_Y{}, sym_Z{}; + + // Terms (created in SetUp) + TermId a{}, b{}, c{}; + TermId X{}, Y{}, Z{}; + + 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_f = symbols.intern("f", SymbolKind::kFunction, 1); + sym_g = symbols.intern("g", SymbolKind::kFunction, 2); + sym_h = symbols.intern("h", SymbolKind::kFunction, 1); + sym_P = symbols.intern("P", SymbolKind::kPredicate, 2); + sym_X = symbols.intern("X", SymbolKind::kVariable); + sym_Y = symbols.intern("Y", SymbolKind::kVariable); + sym_Z = symbols.intern("Z", SymbolKind::kVariable); + + a = bank.makeTerm(sym_a, {}); + b = bank.makeTerm(sym_b, {}); + c = bank.makeTerm(sym_c, {}); + X = bank.makeVar(sym_X); + Y = bank.makeVar(sym_Y); + Z = bank.makeVar(sym_Z); + } + + // Helper: make f(arg) + TermId f(TermId arg) { return bank.makeTerm(sym_f, {{arg}}); } + // Helper: make g(arg1, arg2) + TermId g(TermId a1, TermId a2) { return bank.makeTerm(sym_g, {{a1, a2}}); } + // Helper: make h(arg) + TermId h(TermId arg) { return bank.makeTerm(sym_h, {{arg}}); } + // Helper: make P(arg1, arg2) + TermId P(TermId a1, TermId a2) { return bank.makeTerm(sym_P, {{a1, a2}}); } +}; + +// ═══════════════════════════════════════════════════════════════════════════ +// Substitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, SubstBindAndLookup) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_EQ(subst.lookup(X), a); + EXPECT_EQ(subst.lookup(Y), kInvalidId); // unbound +} + +TEST_F(UnificationTest, SubstBindSameTermSucceeds) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_TRUE(subst.bind(X, a)); // same binding → OK +} + +TEST_F(UnificationTest, SubstBindDifferentTermFails) { + Substitution subst; + EXPECT_TRUE(subst.bind(X, a)); + EXPECT_FALSE(subst.bind(X, b)); // different binding → fail +} + +TEST_F(UnificationTest, SubstResolveChain) { + // X → Y → a + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, SubstResolveUnbound) { + Substitution subst; + EXPECT_EQ(subst.resolve(X, bank), X); // unbound → returns itself +} + +TEST_F(UnificationTest, SubstResolveNonVariable) { + Substitution subst; + EXPECT_EQ(subst.resolve(a, bank), a); // constant → returns itself +} + +TEST_F(UnificationTest, SubstApplySimple) { + // σ = {X → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, a); + TermId fx = f(X); + TermId result = subst.apply(fx, bank); + TermId expected = f(a); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyLeavesUnbound) { + // σ = {X → a} apply to g(X, Y) → g(a, Y) + Substitution subst; + subst.bind(X, a); + TermId gxy = g(X, Y); + TermId result = subst.apply(gxy, bank); + TermId expected = g(a, Y); + EXPECT_EQ(result, expected); +} + +TEST_F(UnificationTest, SubstApplyNested) { + // σ = {X → f(a)} apply to g(X, b) → g(f(a), b) + Substitution subst; + subst.bind(X, f(a)); + TermId result = subst.apply(g(X, b), bank); + EXPECT_EQ(result, g(f(a), b)); +} + +TEST_F(UnificationTest, SubstOccursIn) { + Substitution subst; + // X occurs in f(X) + EXPECT_TRUE(subst.occursIn(X, f(X), bank)); + // X occurs in g(a, f(X)) + EXPECT_TRUE(subst.occursIn(X, g(a, f(X)), bank)); + // X does NOT occur in f(a) + EXPECT_FALSE(subst.occursIn(X, f(a), bank)); + // X does NOT occur in Y (different variable) + EXPECT_FALSE(subst.occursIn(X, Y, bank)); +} + +TEST_F(UnificationTest, SubstClearAndSize) { + Substitution subst; + EXPECT_TRUE(subst.empty()); + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(subst.size(), 2); + subst.clear(); + EXPECT_TRUE(subst.empty()); + EXPECT_EQ(subst.lookup(X), kInvalidId); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Unification Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, UnifyIdenticalConstants) { + Substitution subst; + EXPECT_TRUE(unify(bank, a, a, subst)); + EXPECT_TRUE(subst.empty()); +} + +TEST_F(UnificationTest, UnifyDifferentConstants) { + Substitution subst; + EXPECT_FALSE(unify(bank, a, b, subst)); +} + +TEST_F(UnificationTest, UnifyVarWithConstant) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, a, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyConstantWithVar) { + // Symmetric: unify(a, X) should also work + Substitution subst; + EXPECT_TRUE(unify(bank, a, X, subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyTwoVariables) { + Substitution subst; + EXPECT_TRUE(unify(bank, X, Y, subst)); + // One should be bound to the other + TermId rx = subst.resolve(X, bank); + TermId ry = subst.resolve(Y, bank); + EXPECT_EQ(rx, ry); +} + +TEST_F(UnificationTest, UnifyCompoundTerms) { + // f(X) =? f(a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(X), f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyMultipleArgs) { + // g(X, Y) =? g(a, b) → {X → a, Y → b} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(a, b), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), b); +} + +TEST_F(UnificationTest, UnifyConflictingBindings) { + // g(X, X) =? g(a, b) → fails (X can't be both a and b) + Substitution subst; + EXPECT_FALSE(unify(bank, g(X, X), g(a, b), subst)); +} + +TEST_F(UnificationTest, UnifyConsistentRepeatedVar) { + // g(X, X) =? g(a, a) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, X), g(a, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyDifferentHeadSymbols) { + // f(X) =? h(X) → fails + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), h(X), subst)); +} + +TEST_F(UnificationTest, UnifyDifferentArity) { + // f(X) =? g(X, Y) → fails (arity 1 vs 2) + Substitution subst; + EXPECT_FALSE(unify(bank, f(X), g(X, Y), subst)); +} + +TEST_F(UnificationTest, UnifyNestedTerms) { + // f(g(X, a)) =? f(Y) → {Y → g(X, a)} + Substitution subst; + EXPECT_TRUE(unify(bank, f(g(X, a)), f(Y), subst)); + EXPECT_EQ(subst.resolve(Y, bank), g(X, a)); +} + +TEST_F(UnificationTest, UnifyVarWithCompound) { + // X =? f(a) → {X → f(a)} + Substitution subst; + EXPECT_TRUE(unify(bank, X, f(a), subst)); + EXPECT_EQ(subst.resolve(X, bank), f(a)); +} + +TEST_F(UnificationTest, UnifyDeepNesting) { + // f(f(f(X))) =? f(f(f(a))) → {X → a} + Substitution subst; + EXPECT_TRUE(unify(bank, f(f(f(X))), f(f(f(a))), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); +} + +TEST_F(UnificationTest, UnifyChainedVariables) { + // g(X, Y) =? g(Y, a) → {X → Y, Y → a} effectively X → a + Substitution subst; + EXPECT_TRUE(unify(bank, g(X, Y), g(Y, a), subst)); + EXPECT_EQ(subst.resolve(X, bank), a); + EXPECT_EQ(subst.resolve(Y, bank), a); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// Occurs Check Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, OccursCheckBlocks) { + // X =? f(X) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDisabledAllows) { + // X =? f(X) without occurs check → succeeds (unsound but fast) + Substitution subst; + UnificationConfig config{.enable_occurs_check = false}; + EXPECT_TRUE(unify(bank, X, f(X), subst, config)); +} + +TEST_F(UnificationTest, OccursCheckDeep) { + // X =? f(g(X, a)) with occurs check → fails + Substitution subst; + UnificationConfig config{.enable_occurs_check = true}; + EXPECT_FALSE(unify(bank, X, f(g(X, a)), subst, config)); +} + +// ═══════════════════════════════════════════════════════════════════════════ +// applySubstitution Tests +// ═══════════════════════════════════════════════════════════════════════════ + +TEST_F(UnificationTest, ApplySubstitutionSimple) { + Substitution subst; + subst.bind(X, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, ApplySubstitutionNested) { + Substitution subst; + subst.bind(X, a); + subst.bind(Y, b); + EXPECT_EQ(applySubstitution(subst, g(f(X), Y), bank), g(f(a), b)); +} + +TEST_F(UnificationTest, ApplySubstitutionPreservesUnbound) { + Substitution subst; + subst.bind(X, a); + // Y is unbound → stays as Y + EXPECT_EQ(applySubstitution(subst, g(X, Y), bank), g(a, Y)); +} + +TEST_F(UnificationTest, ApplySubstitutionToConstant) { + Substitution subst; + subst.bind(X, a); + // Constant is unchanged + EXPECT_EQ(applySubstitution(subst, b, bank), b); +} + +TEST_F(UnificationTest, ApplySubstitutionChain) { + // σ = {X → Y, Y → a} apply to f(X) → f(a) + Substitution subst; + subst.bind(X, Y); + subst.bind(Y, a); + EXPECT_EQ(applySubstitution(subst, f(X), bank), f(a)); +} + +TEST_F(UnificationTest, UnifyThenApply) { + // Full round-trip: unify P(X, f(Y)) with P(a, f(b)), then apply + Substitution subst; + TermId lhs = P(X, f(Y)); + TermId rhs = P(a, f(b)); + ASSERT_TRUE(unify(bank, lhs, rhs, subst)); + + EXPECT_EQ(applySubstitution(subst, lhs, bank), P(a, f(b))); + EXPECT_EQ(applySubstitution(subst, rhs, bank), P(a, f(b))); + // Both sides should produce the same term after applying the MGU + EXPECT_EQ(applySubstitution(subst, lhs, bank), + applySubstitution(subst, rhs, bank)); +} + +} // namespace +} // namespace atp -- 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/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 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/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