aboutsummaryrefslogtreecommitdiff
path: root/include
diff options
context:
space:
mode:
Diffstat (limited to 'include')
-rw-r--r--include/atp/core/clause.h5
-rw-r--r--include/atp/core/clause_store.h1
-rw-r--r--include/atp/core/literal.h5
-rw-r--r--include/atp/core/symbol_table.h5
-rw-r--r--include/atp/core/term.h12
-rw-r--r--include/atp/core/types.h23
-rw-r--r--include/atp/frontend/tptp_parser.h27
-rw-r--r--include/atp/index/discrim_tree.h1
-rw-r--r--include/atp/infer/resolution.h13
-rw-r--r--include/atp/infer/unification.h1
-rw-r--r--include/atp/normalize/formula.h24
-rw-r--r--include/atp/proof/proof_trace.h4
-rw-r--r--include/atp/rewrite/ordering.h12
-rw-r--r--include/atp/rewrite/paramodulation.h1
-rw-r--r--include/atp/search/clause_queue.h1
-rw-r--r--include/atp/search/prover.h7
-rw-r--r--include/atp/simplify/subsumption.h1
-rw-r--r--include/atp/simplify/tautology.h1
-rw-r--r--include/atp/strategy/calculus.h1
-rw-r--r--include/atp/strategy/inference_rule.h11
-rw-r--r--include/atp/strategy/problem_analyzer.h7
-rw-r--r--include/atp/utils/hash_utils.h1
-rw-r--r--include/atp/utils/logger.h16
23 files changed, 74 insertions, 106 deletions
diff --git a/include/atp/core/clause.h b/include/atp/core/clause.h
index b4d3e68..7e0cbff 100644
--- a/include/atp/core/clause.h
+++ b/include/atp/core/clause.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file clause.h
@@ -25,11 +24,11 @@
/// 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"
+#include <vector>
+
namespace atp {
/// A clause: a disjunction of literals plus provenance for proof reconstruction.
diff --git a/include/atp/core/clause_store.h b/include/atp/core/clause_store.h
index 23db996..5d6562a 100644
--- a/include/atp/core/clause_store.h
+++ b/include/atp/core/clause_store.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file clause_store.h
diff --git a/include/atp/core/literal.h b/include/atp/core/literal.h
index a3192a9..212c281 100644
--- a/include/atp/core/literal.h
+++ b/include/atp/core/literal.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file literal.h
@@ -28,8 +27,8 @@ 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
+ 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 = atom, .is_positive = !is_positive}; }
diff --git a/include/atp/core/symbol_table.h b/include/atp/core/symbol_table.h
index 856c395..30453fc 100644
--- a/include/atp/core/symbol_table.h
+++ b/include/atp/core/symbol_table.h
@@ -16,20 +16,19 @@
* 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 "atp/core/types.h"
+
#include <deque>
#include <string>
#include <string_view>
#include <unordered_map>
-#include "atp/core/types.h"
-
namespace atp {
/// Metadata associated with an interned symbol.
diff --git a/include/atp/core/term.h b/include/atp/core/term.h
index 017882a..2be01e7 100644
--- a/include/atp/core/term.h
+++ b/include/atp/core/term.h
@@ -24,22 +24,20 @@
/// V1 uses vector<TermId> for args.
/// Future: flat arena with contiguous arg storage for cache locality.
-#include <vector>
-
#include "atp/core/types.h"
+#include <vector>
+
namespace atp {
/// A term is a function/predicate application: f(t1, t2, ..., tn).
/// Variables are 0-arity terms whose symbol has SymbolKind::kVariable.
struct Term {
- SymbolId symbol_id; ///< Index into the SymbolTable
- std::vector<TermId> args; ///< Argument sub-term IDs
+ SymbolId symbol_id; ///< Index into the SymbolTable
+ std::vector<TermId> args; ///< Argument sub-term IDs
/// Number of arguments.
- [[nodiscard]] uint16_t arity() const {
- return static_cast<uint16_t>(args.size());
- }
+ [[nodiscard]] uint16_t arity() const { return static_cast<uint16_t>(args.size()); }
};
} // namespace atp
diff --git a/include/atp/core/types.h b/include/atp/core/types.h
index c68e716..23f2322 100644
--- a/include/atp/core/types.h
+++ b/include/atp/core/types.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file types.h
@@ -57,24 +56,24 @@ enum class SymbolKind : uint8_t {
/// 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
+ 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
+ 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
+ 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
+ kTheoryRewrite = 301, ///< Theory-driven rewriting
};
} // namespace atp
diff --git a/include/atp/frontend/tptp_parser.h b/include/atp/frontend/tptp_parser.h
index 075b45e..738d34b 100644
--- a/include/atp/frontend/tptp_parser.h
+++ b/include/atp/frontend/tptp_parser.h
@@ -42,15 +42,15 @@ namespace atp {
/// Role of a TPTP formula.
/// See TPTP spec: https://www.tptp.org/TPTP/SyntaxBNF.html
enum class FormulaRole : uint8_t {
- kAxiom, ///< Background truth
- kHypothesis, ///< Problem-specific assumption
- kDefinition, ///< Symbol definition (can be unfolded)
- kAssumption, ///< Assumed for this proof attempt
- kLemma, ///< Derived intermediate result
- kTheorem, ///< Previously proved statement (used as axiom)
- kConjecture, ///< The statement to prove
- kNegatedConjecture, ///< Already negated conjecture (input was cnf)
- kPlain, ///< No semantic role specified
+ kAxiom, ///< Background truth
+ kHypothesis, ///< Problem-specific assumption
+ kDefinition, ///< Symbol definition (can be unfolded)
+ kAssumption, ///< Assumed for this proof attempt
+ kLemma, ///< Derived intermediate result
+ kTheorem, ///< Previously proved statement (used as axiom)
+ kConjecture, ///< The statement to prove
+ kNegatedConjecture, ///< Already negated conjecture (input was cnf)
+ kPlain, ///< No semantic role specified
};
/// Map a TPTP role string to enum. Returns kPlain for unknown roles.
@@ -82,12 +82,10 @@ struct ParsedProblem {
/// For `fof(...)` entries: Formula AST is built (clausification happens later).
///
/// All symbols are interned into `symbols` and terms into `bank` during parsing.
-ParsedProblem parseTptpFile(const std::string& filepath,
- TermBank& bank, SymbolTable& symbols);
+ParsedProblem parseTptpFile(const std::string& filepath, TermBank& bank, SymbolTable& symbols);
/// Parse a TPTP string (for testing).
-ParsedProblem parseTptpString(const std::string& input,
- TermBank& bank, SymbolTable& symbols);
+ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols);
/// Prepare a parsed problem for proving:
/// 1. Negate conjecture formulas.
@@ -96,7 +94,6 @@ ParsedProblem parseTptpString(const std::string& input,
/// 4. Assign ClauseIds and set provenance to kInput.
///
/// Returns the final clause set ready for the Prover.
-std::vector<Clause> prepareForProving(ParsedProblem& problem,
- TermBank& bank, SymbolTable& symbols);
+std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank, SymbolTable& symbols);
} // namespace atp
diff --git a/include/atp/index/discrim_tree.h b/include/atp/index/discrim_tree.h
index 8cadaa6..c5954d7 100644
--- a/include/atp/index/discrim_tree.h
+++ b/include/atp/index/discrim_tree.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file discrim_tree.h
diff --git a/include/atp/infer/resolution.h b/include/atp/infer/resolution.h
index df9cab3..6e2954d 100644
--- a/include/atp/infer/resolution.h
+++ b/include/atp/infer/resolution.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file resolution.h
@@ -24,32 +23,28 @@
#include "atp/core/clause.h"
#include "atp/core/term_bank.h"
+#include "atp/infer/unification.h"
#include <optional>
#include <vector>
-#include "atp/infer/unification.h"
-
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(TermBank& bank, const Clause& c1, size_t lit_idx1,
- const Clause& c2, size_t lit_idx2,
- const UnificationConfig& uconfig = {});
+std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
+ size_t lit_idx2, const UnificationConfig& uconfig = {});
/// Generate all possible resolvents between two clauses.
std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
const UnificationConfig& uconfig = {});
/// Attempt factoring on a single clause (merge two unifiable literals).
-std::vector<Clause> factor(TermBank& bank, const Clause& c,
- const UnificationConfig& uconfig = {});
+std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig = {});
/// Rename all variables in a clause to fresh ones, avoiding conflicts
/// with variables already in the bank.
Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
uint32_t& next_var_id);
-
} // namespace atp
diff --git a/include/atp/infer/unification.h b/include/atp/infer/unification.h
index f2ea180..9a4b6cc 100644
--- a/include/atp/infer/unification.h
+++ b/include/atp/infer/unification.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file unification.h
diff --git a/include/atp/normalize/formula.h b/include/atp/normalize/formula.h
index 2cd7900..1bcc021 100644
--- a/include/atp/normalize/formula.h
+++ b/include/atp/normalize/formula.h
@@ -35,15 +35,15 @@ namespace atp {
/// AST node types for first-order logic formulas.
enum class FormulaKind : uint8_t {
- kAtom, ///< Predicate application: P(t1, ..., tn)
- kEquality, ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
- 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
+ kAtom, ///< Predicate application: P(t1, ..., tn)
+ kEquality, ///< Equality atom: t1 = t2 (distinguished for equality reasoning)
+ 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.
@@ -77,10 +77,8 @@ struct Formula {
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(SymbolId var,
- std::unique_ptr<Formula> body);
- static std::unique_ptr<Formula> makeExists(SymbolId var,
- std::unique_ptr<Formula> body);
+ static std::unique_ptr<Formula> makeForall(SymbolId var, std::unique_ptr<Formula> body);
+ static std::unique_ptr<Formula> makeExists(SymbolId var, std::unique_ptr<Formula> body);
};
} // namespace atp
diff --git a/include/atp/proof/proof_trace.h b/include/atp/proof/proof_trace.h
index a80a327..28099fe 100644
--- a/include/atp/proof/proof_trace.h
+++ b/include/atp/proof/proof_trace.h
@@ -49,7 +49,7 @@ std::string termToString(TermId id, const TermBank& bank);
std::string clauseToString(const Clause& clause, const TermBank& bank);
/// Format a proof as a human-readable string.
-std::string formatProof(const std::vector<ProofStep>& proof,
- const ClauseStore& store, const TermBank& bank);
+std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
+ const TermBank& bank);
} // namespace atp
diff --git a/include/atp/rewrite/ordering.h b/include/atp/rewrite/ordering.h
index 5696766..195c3c6 100644
--- a/include/atp/rewrite/ordering.h
+++ b/include/atp/rewrite/ordering.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file ordering.h
@@ -34,10 +33,10 @@ 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
+ kLessThan, ///< t1 < t2
+ kEqual, ///< t1 = t2
+ kGreaterThan, ///< t1 > t2
+ kIncomparable, ///< t1 and t2 are incomparable
};
/// Abstract base for term orderings.
@@ -47,8 +46,7 @@ class TermOrdering {
virtual ~TermOrdering() = default;
/// Compare two terms under the ordering.
- [[nodiscard]] virtual OrderResult compare(const TermBank& bank, TermId t1,
- TermId t2) const = 0;
+ [[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
index f43cd7b..9dfbd66 100644
--- a/include/atp/rewrite/paramodulation.h
+++ b/include/atp/rewrite/paramodulation.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file paramodulation.h
diff --git a/include/atp/search/clause_queue.h b/include/atp/search/clause_queue.h
index 828a725..6a8f9fc 100644
--- a/include/atp/search/clause_queue.h
+++ b/include/atp/search/clause_queue.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file clause_queue.h
diff --git a/include/atp/search/prover.h b/include/atp/search/prover.h
index d84a647..6ee22f0 100644
--- a/include/atp/search/prover.h
+++ b/include/atp/search/prover.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file prover.h
@@ -39,9 +38,9 @@ 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
+ kTheorem, ///< Empty clause derived — conjecture is a theorem
+ kSaturation, ///< Search space saturated — cannot prove
+ kTimeout, ///< Resource limit exceeded
};
/// V1 configuration — simple and direct.
diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h
index c39b586..970b6d8 100644
--- a/include/atp/simplify/subsumption.h
+++ b/include/atp/simplify/subsumption.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file subsumption.h
diff --git a/include/atp/simplify/tautology.h b/include/atp/simplify/tautology.h
index 80aa1f9..f17f0c7 100644
--- a/include/atp/simplify/tautology.h
+++ b/include/atp/simplify/tautology.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file tautology.h
diff --git a/include/atp/strategy/calculus.h b/include/atp/strategy/calculus.h
index ee8ee09..e06988e 100644
--- a/include/atp/strategy/calculus.h
+++ b/include/atp/strategy/calculus.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file calculus.h
diff --git a/include/atp/strategy/inference_rule.h b/include/atp/strategy/inference_rule.h
index 1c7dbba..88b6fe0 100644
--- a/include/atp/strategy/inference_rule.h
+++ b/include/atp/strategy/inference_rule.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file inference_rule.h
@@ -62,9 +61,10 @@ class GeneratingRule : public InferenceRuleBase {
/// @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;
+ [[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.
@@ -74,8 +74,7 @@ class SimplifyingRule : public InferenceRuleBase {
/// 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;
+ 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
index b5fdef4..5e6c5cf 100644
--- a/include/atp/strategy/problem_analyzer.h
+++ b/include/atp/strategy/problem_analyzer.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file problem_analyzer.h
@@ -41,10 +40,10 @@ namespace atp {
/// Features detected in the input problem.
struct ProblemFeatures {
- bool has_equality = false; ///< Contains '=' predicate
+ 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)
+ 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;
diff --git a/include/atp/utils/hash_utils.h b/include/atp/utils/hash_utils.h
index 4531fa6..ae31f43 100644
--- a/include/atp/utils/hash_utils.h
+++ b/include/atp/utils/hash_utils.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file hash_utils.h
diff --git a/include/atp/utils/logger.h b/include/atp/utils/logger.h
index 95d3dd2..de77c54 100644
--- a/include/atp/utils/logger.h
+++ b/include/atp/utils/logger.h
@@ -16,7 +16,6 @@
* along with this program. If not, see <https://www.gnu.org/licenses/>.
*/
-
#pragma once
/// @file logger.h
@@ -28,16 +27,15 @@
#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__); \
- } \
+#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_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__)
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-29 02:07:54 +0000