diff options
Diffstat (limited to 'include')
26 files changed, 1451 insertions, 0 deletions
diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h new file mode 100644 index 0000000..b4d3e68 --- /dev/null +++ b/include/atp/core/clause.h @@ -0,0 +1,53 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file clause.h +/// @brief A clause is a disjunction of literals, with provenance tracking. +/// +/// NOTE: V1 uses std::vector<Literal> for simplicity. +/// Future optimization: migrate to a Clause Arena with contiguous storage. + +#include <vector> + +#include "atp/core/literal.h" +#include "atp/core/types.h" + +namespace atp { + +/// A clause: a disjunction of literals plus provenance for proof reconstruction. +struct Clause { + ClauseId id = kInvalidId; + std::vector<Literal> literals; + + // Provenance (for proof trace) + InferenceRule rule = InferenceRule::kInput; + ClauseId parent1 = kInvalidId; + ClauseId parent2 = kInvalidId; + uint16_t depth = 0; ///< Derivation depth (for BFS scheduling) + + /// True if the clause has no literals (contradiction). + [[nodiscard]] bool isEmpty() const { return literals.empty(); } + + /// Number of literals. + [[nodiscard]] size_t size() const { return literals.size(); } +}; + +} // namespace atp diff --git a/include/atp/core/clause_store.h b/include/atp/core/clause_store.h new file mode 100644 index 0000000..6e220cc --- /dev/null +++ b/include/atp/core/clause_store.h @@ -0,0 +1,62 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file clause_store.h +/// @brief Central clause storage — owns all clauses, assigns ClauseIds. +/// +/// Extracted from Prover to separate storage responsibility from search logic. +/// This enables swapping search strategies (OTTER loop / DISCOUNT loop) +/// without touching clause lifecycle management. + +#include "atp/core/clause.h" +#include "atp/core/types.h" + +#include <functional> +#include <vector> + +namespace atp { + +/// Central clause store. Owns all clauses and assigns unique ClauseIds. +/// All modules access clauses through this store via ClauseId references. +class ClauseStore { + public: + ClauseStore() = default; + + /// Add a clause, assign it a ClauseId, and return the ID. + ClauseId addClause(Clause clause); + + /// Access a clause by its ID. UB if id is out of range. + [[nodiscard]] const Clause& getClause(ClauseId id) const; + + /// Mutable access (for marking clauses as deleted, etc.) + [[nodiscard]] Clause& getMutableClause(ClauseId id); + + /// Total number of stored clauses. + [[nodiscard]] size_t size() const; + + /// Iterate over all clauses with a visitor. + void forEach(const std::function<void(const Clause&)>& visitor) const; + + private: + std::vector<Clause> clauses_; +}; + +} // namespace atp diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h new file mode 100644 index 0000000..1b4f65c --- /dev/null +++ b/include/atp/core/literal.h @@ -0,0 +1,40 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file literal.h +/// @brief A literal is a (possibly negated) atomic formula. + +#include "atp/core/types.h" + +namespace atp { + +/// A literal: a polarity flag plus the TermId of the atom. +struct Literal { + TermId atom; ///< TermId of the predicate application + bool is_positive; ///< true = positive, false = negated + + /// Complement: flip polarity, same atom. + [[nodiscard]] Literal complement() const { return {atom, !is_positive}; } + + bool operator==(const Literal& other) const = default; +}; + +} // namespace atp diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h new file mode 100644 index 0000000..ed27a4d --- /dev/null +++ b/include/atp/core/symbol_table.h @@ -0,0 +1,68 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file symbol_table.h +/// @brief Bidirectional mapping between symbol names and SymbolIds, +/// with kind and sort metadata. + +#include <string> +#include <string_view> + +#include "atp/core/types.h" + +namespace atp { + +/// Metadata associated with an interned symbol. +struct SymbolInfo { + std::string name; + SymbolKind kind = SymbolKind::kFunction; + uint16_t arity = 0; + SortId sort = kUnsorted; ///< Result sort (for sorted logic) +}; + +/// Interns symbol names so that each unique string is stored exactly once. +/// Also tracks symbol metadata (kind, arity, sort). +/// Thread-safety: NOT thread-safe (single-threaded prover design). +class SymbolTable { + public: + SymbolTable() = default; + + /// Intern a symbol name with metadata. Returns existing ID if already present. + SymbolId intern(std::string_view name, SymbolKind kind, uint16_t arity = 0, + SortId sort = kUnsorted); + + /// Look up the name for a given SymbolId. UB if id is out of range. + [[nodiscard]] std::string_view getName(SymbolId id) const; + + /// Look up full metadata for a SymbolId. + [[nodiscard]] const SymbolInfo& getInfo(SymbolId id) const; + + /// Check if a symbol is a variable. + [[nodiscard]] bool isVariable(SymbolId id) const; + + /// Number of interned symbols. + [[nodiscard]] size_t size() const; + + private: + // TODO: Phase 1 implementation +}; + +} // namespace atp diff --git a/include/atp/core/term.h b/include/atp/core/term.h new file mode 100644 index 0000000..e1edfcf --- /dev/null +++ b/include/atp/core/term.h @@ -0,0 +1,43 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file term.h +/// @brief Core Term data structure — hash-consed, immutable. + +#include <span> + +#include "atp/core/types.h" + +namespace atp { + +/// A term is a function/predicate application: f(t1, t2, ..., tn). +/// Stored in a flat arena; args are contiguous TermIds following the header. +/// Variables are represented as terms with a special symbol range. +struct Term { + SymbolId symbol_id; ///< Index into the SymbolTable + uint16_t arity; ///< Number of arguments + + /// Access the argument TermIds (stored immediately after this struct in the arena). + [[nodiscard]] std::span<const TermId> args() const; + [[nodiscard]] std::span<TermId> mutableArgs(); +}; + +} // namespace atp diff --git a/include/atp/core/term_bank.h b/include/atp/core/term_bank.h new file mode 100644 index 0000000..a121f8a --- /dev/null +++ b/include/atp/core/term_bank.h @@ -0,0 +1,57 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file term_bank.h +/// @brief Hash-consing term pool — guarantees structural sharing. + +#include "atp/core/term.h" +#include "atp/core/types.h" + +#include <span> + +namespace atp { + +/// Global term pool with hash-consing. +/// Every structurally identical term maps to the same TermId. +class TermBank { + public: + TermBank() = default; + + /// Create or retrieve a term. Returns the canonical TermId. + TermId makeTerm(SymbolId symbol, std::span<const TermId> args); + + /// Create a variable term. + TermId makeVar(SymbolId var_symbol); + + /// Look up a term by its ID. + [[nodiscard]] const Term& getTerm(TermId id) const; + + /// Check if a TermId represents a variable. + [[nodiscard]] bool isVariable(TermId id) const; + + /// Total number of unique terms stored. + [[nodiscard]] size_t size() const; + + private: + // TODO: Phase 1 implementation — flat arena + hash index +}; + +} // namespace atp diff --git a/include/atp/core/types.h b/include/atp/core/types.h new file mode 100644 index 0000000..c68e716 --- /dev/null +++ b/include/atp/core/types.h @@ -0,0 +1,80 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file types.h +/// @brief Core type aliases for the ATP engine. + +#include <cstdint> + +namespace atp { + +/// Unique identifier for an interned symbol (predicate/function/constant name). +using SymbolId = uint32_t; + +/// Unique identifier for a term in the Term Bank (hash-consed). +using TermId = uint32_t; + +/// Unique identifier for a clause in the Clause Store. +using ClauseId = uint32_t; + +/// Unique identifier for a sort/type (for sorted logic). +using SortId = uint16_t; + +/// Sentinel value indicating an invalid / unassigned ID. +inline constexpr uint32_t kInvalidId = UINT32_MAX; + +/// Default sort (unsorted logic). +inline constexpr SortId kUnsorted = 0; + +/// Symbol kind — distinguishes variables from function/predicate symbols. +enum class SymbolKind : uint8_t { + kVariable, ///< Universally quantified variable + kConstant, ///< 0-arity function symbol (constant) + kFunction, ///< Function symbol (arity >= 1) + kPredicate, ///< Predicate symbol (returns bool) + kSkolem, ///< Skolem function/constant (introduced by Skolemization) +}; + +/// Inference rule that produced a clause. +/// Deliberately uses uint16_t for extensibility toward algebra/analysis rules. +enum class InferenceRule : uint16_t { + // ── Core resolution rules ── + kInput = 0, ///< Original input clause (axiom / negated conjecture) + kResolution = 1, ///< Binary resolution + kFactoring = 2, ///< Factoring + + // ── Equality rules (algebra) ── + kParamodulation = 100, ///< Paramodulation (equality resolution) + kDemodulation = 101, ///< Demodulation (simplification by rewriting) + kEqualityResolution = 102, ///< s != t resolved with unifier + kEqualityFactoring = 103, ///< Factoring with equality + + // ── Simplification rules ── + kSubsumption = 200, ///< Removed by subsumption + kTautologyElim = 201, ///< Removed as tautology + kPureLiteralElim = 202, ///< Pure literal elimination + + // ── Theory rules (analysis, arithmetic) ── + kTheoryResolution = 300, ///< Theory-specific resolution + kTheoryRewrite = 301, ///< Theory-driven rewriting +}; + +} // namespace atp diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h new file mode 100644 index 0000000..f43f020 --- /dev/null +++ b/include/atp/frontend/tptp_parser.h @@ -0,0 +1,52 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file tptp_parser.h +/// @brief Bridge from ANTLR4-generated parse tree to internal Formula AST. + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/normalize/formula.h" + +#include <string> +#include <vector> + +namespace atp { + +/// Role of a TPTP formula (axiom, hypothesis, conjecture, etc.) +enum class FormulaRole : uint8_t { + kAxiom, + kHypothesis, + kConjecture, + kNegatedConjecture, +}; + +/// A parsed TPTP formula with its name and role. +struct AnnotatedFormula { + std::string name; + FormulaRole role; + std::unique_ptr<Formula> formula; +}; + +/// Parse a TPTP file and return the annotated formulas. +std::vector<AnnotatedFormula> parseTptpFile(const std::string& filepath, TermBank& bank); + +} // namespace atp diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h new file mode 100644 index 0000000..8cadaa6 --- /dev/null +++ b/include/atp/index/discrim_tree.h @@ -0,0 +1,77 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file discrim_tree.h +/// @brief Perfect Discrimination Tree for fast term indexing. +/// +/// Used by subsumption and resolution to quickly find candidate clauses +/// whose literals unify with a query term. Supports three query modes: +/// - Unifiable: find terms that can be unified with the query +/// - Instances: find terms that are instances of the query (more specific) +/// - Generalizations: find terms that are generalizations of the query (more general) + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +#include <vector> + +namespace atp { + +/// A match result from the discrimination tree. +struct IndexMatch { + ClauseId clause_id; + size_t lit_index; +}; + +/// A discrimination tree index over terms. +/// Supports insertion and three types of retrieval queries. +class DiscrimTree { + public: + explicit DiscrimTree(const TermBank& bank); + + /// Insert a term (identified by its TermId) with an associated clause/literal ref. + void insert(TermId term, ClauseId clause_id, size_t lit_index); + + /// Retrieve all entries whose indexed term is unifiable with `query`. + [[nodiscard]] std::vector<IndexMatch> queryUnifiable(TermId query) const; + + /// Retrieve all entries whose indexed term is an instance of `query`. + /// (query is more general, indexed term is more specific) + [[nodiscard]] std::vector<IndexMatch> queryInstances(TermId query) const; + + /// Retrieve all entries whose indexed term is a generalization of `query`. + /// (indexed term is more general, query is more specific) + /// This is the key operation for forward subsumption. + [[nodiscard]] std::vector<IndexMatch> queryGeneralizations(TermId query) const; + + /// Remove all entries for a given clause. + void removeClause(ClauseId clause_id); + + /// Number of indexed entries. + [[nodiscard]] size_t size() const; + + private: + const TermBank& bank_; + // TODO: Phase 3 implementation — trie node arena +}; + +} // namespace atp diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h new file mode 100644 index 0000000..2d73b06 --- /dev/null +++ b/include/atp/infer/resolution.h @@ -0,0 +1,44 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file resolution.h +/// @brief Binary resolution and factoring inference rules. + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" + +#include <optional> +#include <vector> + +namespace atp { + +/// Attempt binary resolution between two clauses on the specified literal indices. +/// @return The resolvent clause if resolution succeeds, std::nullopt otherwise. +std::optional<Clause> resolve(const TermBank& bank, const Clause& c1, size_t lit_idx1, + const Clause& c2, size_t lit_idx2); + +/// Generate all possible resolvents between two clauses. +std::vector<Clause> allResolvents(const TermBank& bank, const Clause& c1, const Clause& c2); + +/// Attempt factoring on a single clause (merge two unifiable literals). +std::vector<Clause> factor(const TermBank& bank, const Clause& c); + +} // namespace atp diff --git a/include/atp/infer/substitution.h b/include/atp/infer/substitution.h new file mode 100644 index 0000000..f9f562a --- /dev/null +++ b/include/atp/infer/substitution.h @@ -0,0 +1,54 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file substitution.h +/// @brief Variable binding map: Var -> Term. + +#include "atp/core/types.h" + +#include <vector> + +namespace atp { + +/// A substitution is a mapping from variable TermIds to their bound TermIds. +/// Designed as a short-lived, stack-allocated object during unification. +class Substitution { + public: + Substitution() = default; + + /// Bind a variable to a term. Returns false if already bound to something different. + bool bind(TermId var, TermId term); + + /// Look up what a variable is 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; + + /// Clear all bindings. + void clear(); + + private: + // TODO: Phase 2 implementation + std::vector<std::pair<TermId, TermId>> bindings_; +}; + +} // namespace atp diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h new file mode 100644 index 0000000..7d91aaf --- /dev/null +++ b/include/atp/infer/unification.h @@ -0,0 +1,40 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file unification.h +/// @brief Most General Unifier (MGU) computation. + +#include "atp/core/term_bank.h" +#include "atp/infer/substitution.h" + +namespace atp { + +/// Configuration for the unification algorithm. +struct UnificationConfig { + bool enable_occurs_check = false; ///< Set true for sound but slower unification +}; + +/// Attempt to unify two terms, producing a most general unifier. +/// @return true if unification succeeds, with the MGU in `subst`. +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, + const UnificationConfig& config = {}); + +} // namespace atp diff --git a/include/atp/normalize/clausifier.h b/include/atp/normalize/clausifier.h new file mode 100644 index 0000000..1ff4d27 --- /dev/null +++ b/include/atp/normalize/clausifier.h @@ -0,0 +1,38 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file clausifier.h +/// @brief Converts FOL formulas to Clause Normal Form (CNF). +/// +/// Pipeline: eliminate ↔/→ → NNF → Skolemize → distribute ∨ over ∧ → flatten. + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/normalize/formula.h" + +#include <vector> + +namespace atp { + +/// Convert a first-order formula into a set of clauses (CNF). +std::vector<Clause> clausify(const Formula& formula, TermBank& bank); + +} // namespace atp diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h new file mode 100644 index 0000000..ccf1302 --- /dev/null +++ b/include/atp/normalize/formula.h @@ -0,0 +1,74 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file formula.h +/// @brief First-order logic formula AST (pre-clausification). + +#include "atp/core/types.h" + +#include <memory> +#include <string> +#include <vector> + +namespace atp { + +/// AST node types for first-order logic formulas. +enum class FormulaKind : uint8_t { + kAtom, ///< Predicate application: P(t1, ..., tn) + kNot, ///< Negation: ¬F + kAnd, ///< Conjunction: F ∧ G + kOr, ///< Disjunction: F ∨ G + kImplies, ///< Implication: F → G + kIff, ///< Biconditional: F ↔ G + kForall, ///< Universal: ∀x. F + kExists, ///< Existential: ∃x. F +}; + +/// A first-order logic formula node. +struct Formula { + FormulaKind kind; + + // For kAtom: the predicate term + TermId atom = kInvalidId; + + // For quantifiers: the bound variable name + std::string var_name; + + // Sub-formulas (1 for Not/Quantifiers, 2 for binary connectives) + std::vector<std::unique_ptr<Formula>> children; + + static std::unique_ptr<Formula> makeAtom(TermId atom); + static std::unique_ptr<Formula> makeNot(std::unique_ptr<Formula> child); + static std::unique_ptr<Formula> makeAnd(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeOr(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeImplies(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeIff(std::unique_ptr<Formula> lhs, + std::unique_ptr<Formula> rhs); + static std::unique_ptr<Formula> makeForall(std::string var, + std::unique_ptr<Formula> body); + static std::unique_ptr<Formula> makeExists(std::string var, + std::unique_ptr<Formula> body); +}; + +} // namespace atp diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h new file mode 100644 index 0000000..cda6c5b --- /dev/null +++ b/include/atp/proof/proof_trace.h @@ -0,0 +1,54 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#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" +#include "atp/core/term_bank.h" + +#include <string> +#include <vector> + +namespace atp { + +/// A single step in a reconstructed proof. +struct ProofStep { + ClauseId clause_id; + 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<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_clause_id, + const TermBank& bank); + +/// Format a proof as a human-readable string. +std::string formatProof(const std::vector<ProofStep>& proof, const TermBank& bank); + +} // namespace atp diff --git a/include/atp/rewrite/ordering.h b/include/atp/rewrite/ordering.h new file mode 100644 index 0000000..5696766 --- /dev/null +++ b/include/atp/rewrite/ordering.h @@ -0,0 +1,54 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file ordering.h +/// @brief Term orderings for equality reasoning (KBO, LPO). +/// +/// Term orderings are the foundation of equality-based theorem proving. +/// They ensure that rewriting always terminates by enforcing a well-founded +/// ordering on terms. Required by paramodulation, demodulation, and +/// ordered resolution. + +#include "atp/core/term_bank.h" +#include "atp/core/types.h" + +namespace atp { + +/// Ordering comparison result. +enum class OrderResult : uint8_t { + kLessThan, ///< t1 < t2 + kEqual, ///< t1 = t2 + kGreaterThan, ///< t1 > t2 + kIncomparable, ///< t1 and t2 are incomparable +}; + +/// Abstract base for term orderings. +/// Concrete implementations: KBO (Knuth-Bendix), LPO (Lexicographic Path). +class TermOrdering { + public: + virtual ~TermOrdering() = default; + + /// Compare two terms under the ordering. + [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1, + TermId t2) const = 0; +}; + +} // namespace atp diff --git a/include/atp/rewrite/paramodulation.h b/include/atp/rewrite/paramodulation.h new file mode 100644 index 0000000..f43cd7b --- /dev/null +++ b/include/atp/rewrite/paramodulation.h @@ -0,0 +1,48 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file paramodulation.h +/// @brief Paramodulation inference rule for equality reasoning. +/// +/// Paramodulation replaces a subterm in one clause with an equal term +/// from an equation in another clause. Combined with term orderings, +/// this gives a complete calculus for first-order logic with equality +/// (the Superposition calculus). + +#include "atp/core/clause.h" +#include "atp/core/term_bank.h" +#include "atp/rewrite/ordering.h" + +#include <vector> + +namespace atp { + +/// Generate all paramodulants between two clauses. +/// Uses the term ordering to restrict to ordered paramodulation (superposition). +std::vector<Clause> paramodulate(const TermBank& bank, const Clause& c1, const Clause& c2, + const TermOrdering& ordering); + +/// Simplify a clause by demodulation (rewriting with unit equalities). +/// Returns true if the clause was modified. +bool demodulate(TermBank& bank, Clause& clause, const Clause& unit_eq, + const TermOrdering& ordering); + +} // namespace atp diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h new file mode 100644 index 0000000..828a725 --- /dev/null +++ b/include/atp/search/clause_queue.h @@ -0,0 +1,44 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file clause_queue.h +/// @brief Priority queue for the Given Clause Loop. + +#include "atp/core/clause.h" + +#include <functional> + +namespace atp { + +/// Comparison function type for clause ordering. +using ClauseComparator = std::function<bool(const Clause& a, const Clause& b)>; + +/// BFS comparator: prioritize shallower derivation depth. +inline bool bfsCompare(const Clause& a, const Clause& b) { + return a.depth > b.depth; // min-heap by depth +} + +/// Weight comparator: prioritize shorter (fewer literals) clauses. +inline bool weightCompare(const Clause& a, const Clause& b) { + return a.literals.size() > b.literals.size(); // min-heap by literal count +} + +} // namespace atp diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h new file mode 100644 index 0000000..308e044 --- /dev/null +++ b/include/atp/search/prover.h @@ -0,0 +1,81 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file prover.h +/// @brief The Given Clause Loop — main saturation-based proof search. +/// +/// V1: Uses a simple ProverConfig with hardcoded resolution + factoring. +/// V2: Will be refactored to accept a Calculus object from strategy/ module +/// for dynamic algorithm loading per problem type. + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" +#include "atp/search/clause_queue.h" + +#include <optional> +#include <vector> + +namespace atp { + +/// Result of a proof attempt. +enum class ProverResult : uint8_t { + kTheorem, ///< Empty clause derived — conjecture is a theorem + kSaturation, ///< Search space saturated — cannot prove + kTimeout, ///< Resource limit exceeded +}; + +/// V1 configuration — simple and direct. +/// Future: replaced by strategy::Calculus for dynamic rule loading. +struct ProverConfig { + ClauseComparator comparator = bfsCompare; + size_t max_clauses = 100000; ///< Safety limit + size_t max_iterations = 500000; ///< Safety limit + bool enable_occurs_check = false; +}; + +/// Main prover class implementing the Given Clause Loop. +/// V1: hardcodes resolution + factoring + subsumption. +/// V2: will accept a Calculus object for pluggable inference rules. +class Prover { + public: + Prover(TermBank& bank, ClauseStore& store, ProverConfig config = {}); + + /// Add initial clauses (axioms + negated conjecture). + void addClauses(std::vector<Clause> clauses); + + /// Run the proof search. + ProverResult prove(); + + /// After a successful proof, retrieve the empty clause ID. + [[nodiscard]] std::optional<ClauseId> getEmptyClauseId() const; + + /// Access the underlying clause store. + [[nodiscard]] const ClauseStore& clauseStore() const { return store_; } + + private: + TermBank& bank_; + ClauseStore& store_; + ProverConfig config_; + // TODO: Phase 5 implementation — Unprocessed queue + Processed set +}; + +} // namespace atp diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h new file mode 100644 index 0000000..ee7a83e --- /dev/null +++ b/include/atp/simplify/subsumption.h @@ -0,0 +1,55 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file subsumption.h +/// @brief Forward and backward subsumption checks (backed by discrimination tree). + +#include "atp/core/clause.h" +#include "atp/index/discrim_tree.h" + +#include <vector> + +namespace atp { + +/// Subsumption engine: checks if a new clause is subsumed by existing ones +/// (forward) or subsumes existing ones (backward). +class SubsumptionEngine { + public: + explicit SubsumptionEngine(const TermBank& bank); + + /// Returns true if `candidate` is subsumed by any existing clause. + [[nodiscard]] bool isForwardSubsumed(const Clause& candidate) const; + + /// Returns IDs of existing clauses that are subsumed by `new_clause`. + [[nodiscard]] std::vector<ClauseId> backwardSubsumed(const Clause& new_clause) const; + + /// Add a clause to the subsumption index. + void addClause(const Clause& clause); + + /// Remove a clause from the subsumption index. + void removeClause(ClauseId id); + + private: + DiscrimTree index_; + // TODO: Phase 5 implementation +}; + +} // namespace atp diff --git a/include/atp/simplify/tautology.h b/include/atp/simplify/tautology.h new file mode 100644 index 0000000..80aa1f9 --- /dev/null +++ b/include/atp/simplify/tautology.h @@ -0,0 +1,32 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file tautology.h +/// @brief Tautology detection for clauses. + +#include "atp/core/clause.h" + +namespace atp { + +/// Returns true if the clause is a tautology (contains complementary literals). +[[nodiscard]] bool isTautology(const Clause& clause); + +} // namespace atp diff --git a/include/atp/strategy/calculus.h b/include/atp/strategy/calculus.h new file mode 100644 index 0000000..ee8ee09 --- /dev/null +++ b/include/atp/strategy/calculus.h @@ -0,0 +1,68 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file calculus.h +/// @brief A Calculus bundles the exact set of inference rules + heuristics +/// to use for a specific problem class. +/// +/// Think of it as the "algorithm profile" that the Prover loads. +/// Different problems get different calculi: +/// - Pure propositional: resolution + factoring only +/// - FOL without equality: + full unification +/// - FOL with equality: + paramodulation + KBO ordering +/// - Arithmetic: + theory solver integration +/// +/// This is the single point where search space control happens. + +#include "atp/rewrite/ordering.h" +#include "atp/search/clause_queue.h" +#include "atp/strategy/inference_rule.h" + +#include <memory> +#include <string_view> +#include <vector> + +namespace atp { + +/// A Calculus = a complete specification of how to search for a proof. +/// The Prover is parameterized by this — it never hardcodes which rules to use. +struct Calculus { + /// Name for logging (e.g., "superposition", "pure_resolution"). + std::string name; + + /// Generating rules (executed in order during the main loop). + std::vector<std::unique_ptr<GeneratingRule>> generating_rules; + + /// Simplifying rules (applied to each new clause before enqueuing). + std::vector<std::unique_ptr<SimplifyingRule>> simplifying_rules; + + /// Clause selection heuristic. + ClauseComparator comparator = bfsCompare; + + /// Term ordering (nullptr if equality reasoning is disabled). + std::unique_ptr<TermOrdering> ordering = nullptr; + + /// Resource limits. + size_t max_clauses = 100000; + size_t max_iterations = 500000; +}; + +} // namespace atp diff --git a/include/atp/strategy/inference_rule.h b/include/atp/strategy/inference_rule.h new file mode 100644 index 0000000..1c7dbba --- /dev/null +++ b/include/atp/strategy/inference_rule.h @@ -0,0 +1,81 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file inference_rule.h +/// @brief Abstract interface for pluggable inference rules. +/// +/// Each inference rule (resolution, factoring, paramodulation, etc.) +/// is a self-contained object that the Prover can selectively load. +/// This prevents search space explosion by only enabling rules relevant +/// to the problem at hand. + +#include "atp/core/clause.h" +#include "atp/core/clause_store.h" +#include "atp/core/term_bank.h" + +#include <string_view> +#include <vector> + +namespace atp { + +/// Abstract base class for all inference rules. +/// The Prover invokes only the rules present in its active calculus. +class InferenceRuleBase { + public: + virtual ~InferenceRuleBase() = default; + + /// Human-readable name for logging and proof output. + [[nodiscard]] virtual std::string_view name() const = 0; + + /// Is this a generating rule (produces new clauses) or simplifying rule + /// (rewrites/deletes existing clauses)? + enum class Kind : uint8_t { kGenerating, kSimplifying }; + [[nodiscard]] virtual Kind kind() const = 0; +}; + +/// Generating inference rule: given a "given clause" and the set of processed +/// clauses, produce new clauses. +class GeneratingRule : public InferenceRuleBase { + public: + [[nodiscard]] Kind kind() const final { return Kind::kGenerating; } + + /// Generate new clauses from the given clause against all processed clauses. + /// @param given The selected clause from the Unprocessed queue. + /// @param processed All previously processed clauses (accessed via store). + /// @param bank The global term bank. + /// @return Newly generated clauses (not yet added to the store). + [[nodiscard]] virtual std::vector<Clause> generate( + const Clause& given, const std::vector<ClauseId>& processed, + const ClauseStore& store, TermBank& bank) const = 0; +}; + +/// Simplifying inference rule: rewrite or delete a clause in-place. +class SimplifyingRule : public InferenceRuleBase { + public: + [[nodiscard]] Kind kind() const final { return Kind::kSimplifying; } + + /// Attempt to simplify a clause. Returns true if the clause was modified. + /// If the clause should be deleted entirely, clear its literals. + virtual bool simplify(Clause& clause, const ClauseStore& store, + TermBank& bank) const = 0; +}; + +} // namespace atp diff --git a/include/atp/strategy/problem_analyzer.h b/include/atp/strategy/problem_analyzer.h new file mode 100644 index 0000000..b5fdef4 --- /dev/null +++ b/include/atp/strategy/problem_analyzer.h @@ -0,0 +1,62 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file problem_analyzer.h +/// @brief Analyzes input clauses and selects the optimal Calculus. +/// +/// Before the Prover starts its main loop, the ProblemAnalyzer inspects +/// the input clause set to determine problem characteristics: +/// - Contains equality? → enable paramodulation +/// - Pure Horn clauses? → use SLD resolution +/// - Contains arithmetic literals? → enable theory solver +/// - Problem size / clause density → tune resource limits +/// +/// This is the "auto mode" that mature ATPs use to avoid loading +/// unnecessary inference rules that would explode the search space. + +#include "atp/core/clause.h" +#include "atp/strategy/calculus.h" + +#include <vector> + +namespace atp { + +/// Features detected in the input problem. +struct ProblemFeatures { + bool has_equality = false; ///< Contains '=' predicate + bool is_purely_propositional = false; ///< No function symbols, no variables + bool is_horn = false; ///< All clauses are Horn clauses + bool has_existential = false; ///< Had existential quantifiers (Skolemized) + size_t num_clauses = 0; + size_t num_predicates = 0; + size_t num_functions = 0; + size_t max_clause_size = 0; + size_t max_term_depth = 0; +}; + +/// Analyze the input clauses and extract problem features. +ProblemFeatures analyzeFeatures(const std::vector<Clause>& clauses, const TermBank& bank); + +/// Select the optimal calculus based on detected features. +/// This is the core strategy dispatch logic. +std::unique_ptr<Calculus> selectCalculus(const ProblemFeatures& features); + +} // namespace atp diff --git a/include/atp/utils/hash_utils.h b/include/atp/utils/hash_utils.h new file mode 100644 index 0000000..4531fa6 --- /dev/null +++ b/include/atp/utils/hash_utils.h @@ -0,0 +1,47 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file hash_utils.h +/// @brief Hash combination utilities. + +#include <cstddef> +#include <cstdint> +#include <functional> + +namespace atp { + +/// Combine a hash with a new value (boost::hash_combine style). +inline void hashCombine(size_t& seed, size_t value) { + seed ^= value + 0x9e3779b9 + (seed << 6) + (seed >> 2); +} + +/// Hash a span of values. +template <typename T> +size_t hashRange(const T* data, size_t count) { + size_t seed = 0; + std::hash<T> hasher; + for (size_t i = 0; i < count; ++i) { + hashCombine(seed, hasher(data[i])); + } + return seed; +} + +} // namespace atp diff --git a/include/atp/utils/logger.h b/include/atp/utils/logger.h new file mode 100644 index 0000000..95d3dd2 --- /dev/null +++ b/include/atp/utils/logger.h @@ -0,0 +1,43 @@ +/* + * 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 <https://www.gnu.org/licenses/>. + */ + + +#pragma once + +/// @file logger.h +/// @brief Minimal high-performance logging macros. + +#include <cstdio> + +#ifndef ATP_LOG_LEVEL +#define ATP_LOG_LEVEL 2 // 0=TRACE, 1=DEBUG, 2=INFO, 3=WARN, 4=ERROR +#endif + +#define ATP_LOG(level, level_str, fmt, ...) \ + do { \ + if constexpr (level >= ATP_LOG_LEVEL) { \ + std::fprintf(stderr, "[%s] " fmt "\n", level_str, \ + ##__VA_ARGS__); \ + } \ + } while (0) + +#define ATP_TRACE(fmt, ...) ATP_LOG(0, "TRACE", fmt, ##__VA_ARGS__) +#define ATP_DEBUG(fmt, ...) ATP_LOG(1, "DEBUG", fmt, ##__VA_ARGS__) +#define ATP_INFO(fmt, ...) ATP_LOG(2, "INFO", fmt, ##__VA_ARGS__) +#define ATP_WARN(fmt, ...) ATP_LOG(3, "WARN", fmt, ##__VA_ARGS__) +#define ATP_ERROR(fmt, ...) ATP_LOG(4, "ERROR", fmt, ##__VA_ARGS__) |