aboutsummaryrefslogtreecommitdiff
path: root/src
diff options
context:
space:
mode:
Diffstat (limited to 'src')
-rw-r--r--src/core/clause_store.cc7
-rw-r--r--src/core/symbol_table.cc17
-rw-r--r--src/core/term_bank.cc11
-rw-r--r--src/frontend/tptp_parser.cc198
-rw-r--r--src/infer/resolution.cc84
-rw-r--r--src/infer/substitution.cc12
-rw-r--r--src/infer/unification.cc19
-rw-r--r--src/main.cc20
-rw-r--r--src/proof/proof_trace.cc114
-rw-r--r--src/search/prover.cc42
-rw-r--r--src/simplify/subsumption.cc8
-rw-r--r--src/simplify/tautology.cc6
12 files changed, 297 insertions, 241 deletions
diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc
index 75959c3..f8ee73d 100644
--- a/src/core/clause_store.cc
+++ b/src/core/clause_store.cc
@@ -18,14 +18,19 @@
#include "atp/core/clause_store.h"
+#include "atp/core/clause.h"
+#include "atp/core/types.h"
+
#include <cassert>
+#include <cstddef>
+#include <functional>
#include <utility>
namespace atp {
ClauseId ClauseStore::addClause(Clause clause) {
auto new_id = static_cast<ClauseId>(clauses_.size());
- clause.id = new_id;
+ clause.id_ = new_id;
clauses_.push_back(std::move(clause));
return new_id;
}
diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc
index 42c7dd8..b707132 100644
--- a/src/core/symbol_table.cc
+++ b/src/core/symbol_table.cc
@@ -21,7 +21,9 @@
#include "atp/core/types.h"
#include <cstddef>
+#include <cstdint>
#include <stdexcept>
+#include <string>
#include <string_view>
namespace atp {
@@ -29,22 +31,23 @@ namespace atp {
SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, SortId sort) {
auto it = name_to_id_.find(name);
if (it != name_to_id_.end()) {
- SymbolId id = it->second;
- SymbolInfo& info = infos_[id];
- if (info.kind != kind || info.arity != arity) {
+ SymbolId const id = it->second;
+ SymbolInfo const& info = infos_[id];
+ if (info.kind_ != kind || info.arity_ != arity) {
throw std::runtime_error("Symbol kind or arity mismatch for: " + std::string(name));
}
return id;
}
auto new_id = static_cast<SymbolId>(infos_.size());
- infos_.push_back({.name = std::string(name), .kind = kind, .arity = arity, .sort = sort});
- std::string_view stable_name_view = infos_.back().name;
+ infos_.push_back(SymbolInfo{
+ .name_ = std::string(name), .kind_ = kind, .arity_ = arity, .sort_ = sort});
+ std::string_view const stable_name_view = infos_.back().name_;
name_to_id_.emplace(stable_name_view, new_id);
return new_id;
}
std::string_view SymbolTable::getName(SymbolId id) const {
- return infos_[id].name;
+ return infos_[id].name_;
}
const SymbolInfo& SymbolTable::getInfo(SymbolId id) const {
@@ -52,7 +55,7 @@ const SymbolInfo& SymbolTable::getInfo(SymbolId id) const {
}
bool SymbolTable::isVariable(SymbolId id) const {
- return infos_[id].kind == SymbolKind::kVariable;
+ return infos_[id].kind_ == SymbolKind::kVariable;
}
size_t SymbolTable::size() const {
diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc
index 8c8ef29..2e117b3 100644
--- a/src/core/term_bank.cc
+++ b/src/core/term_bank.cc
@@ -18,20 +18,25 @@
#include "atp/core/term_bank.h"
+#include "atp/core/term.h"
#include "atp/core/types.h"
#include <cassert>
+#include <cstddef>
+#include <span>
+#include <utility>
+#include <vector>
namespace atp {
TermId TermBank::makeTerm(SymbolId symbol, std::span<const TermId> args) {
- TermKey key{.symbol = symbol, .args = {args.begin(), args.end()}};
+ TermKey key{.symbol_ = symbol, .args_ = {args.begin(), args.end()}};
auto it = term_to_id_.find(key);
if (it != term_to_id_.end()) {
return it->second;
}
auto new_id = static_cast<TermId>(terms_.size());
- Term new_term{.symbol_id = symbol, .args = {args.begin(), args.end()}};
+ Term new_term{.symbol_id_ = symbol, .args_ = key.args_};
terms_.push_back(std::move(new_term));
term_to_id_.emplace(std::move(key), new_id);
return new_id;
@@ -48,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/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc
index 2f32522..ddf8aad 100644
--- a/src/frontend/tptp_parser.cc
+++ b/src/frontend/tptp_parser.cc
@@ -20,96 +20,111 @@
#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 <cctype>
+#include <cstddef>
+#include <cstdint>
#include <fstream>
+#include <ios>
+#include <iterator>
#include <stdexcept>
#include <string>
#include <string_view>
#include <unordered_map>
+#include <utility>
#include <vector>
namespace atp {
FormulaRole parseRole(std::string_view role_str) {
- if (role_str == "axiom")
+ if (role_str == "axiom") {
return FormulaRole::kAxiom;
- if (role_str == "hypothesis")
+}
+ if (role_str == "hypothesis") {
return FormulaRole::kHypothesis;
- if (role_str == "definition")
+}
+ if (role_str == "definition") {
return FormulaRole::kDefinition;
- if (role_str == "assumption")
+}
+ if (role_str == "assumption") {
return FormulaRole::kAssumption;
- if (role_str == "lemma")
+}
+ if (role_str == "lemma") {
return FormulaRole::kLemma;
- if (role_str == "theorem")
+}
+ if (role_str == "theorem") {
return FormulaRole::kTheorem;
- if (role_str == "conjecture")
+}
+ if (role_str == "conjecture") {
return FormulaRole::kConjecture;
- if (role_str == "negated_conjecture")
+}
+ if (role_str == "negated_conjecture") {
return FormulaRole::kNegatedConjecture;
- if (role_str == "plain")
+}
+ if (role_str == "plain") {
return FormulaRole::kPlain;
+}
return FormulaRole::kPlain;
}
-enum class TokenType { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown };
+enum class TokenType : std::uint8_t { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown };
struct Token {
- TokenType type;
- std::string_view value;
- size_t line;
- size_t column;
+ TokenType type_{};
+ std::string_view value_;
+ size_t line_{};
+ size_t column_{};
};
class TptpLexer {
public:
explicit TptpLexer(std::string_view input) : source_(input) {}
- Token next_token() {
- skip_whitespace_and_comments();
+ Token nextToken() {
+ skipWhitespaceAndComments();
if (pos_ >= source_.length()) {
- return {.type = TokenType::kEOF, .value = "", .line = line_, .column = column_};
+ return {.type_ = TokenType::kEOF, .value_ = "", .line_ = line_, .column_ = column_};
}
- size_t start_pos = pos_;
- [[maybe_unused]] size_t start_col = column_;
- char c = source_[pos_];
+ size_t const start_pos = pos_;
+ [[maybe_unused]] size_t const start_col = column_;
+ char const c = source_[pos_];
- if (std::isalpha(static_cast<unsigned char>(c)) || c == '_') {
+ if ((std::isalpha(static_cast<unsigned char>(c)) != 0) || c == '_') {
while (
pos_ < source_.size() &&
- (std::isalnum(static_cast<unsigned char>(source_[pos_])) || source_[pos_] == '_')) {
- advance_char();
+ ((std::isalnum(static_cast<unsigned char>(source_[pos_])) != 0) || source_[pos_] == '_')) {
+ advanceChar();
}
- return {.type = TokenType::kWord,
- .value = source_.substr(start_pos, pos_ - start_pos),
- .line = line_,
- .column = column_};
+ return {.type_ = TokenType::kWord,
+ .value_ = source_.substr(start_pos, pos_ - start_pos),
+ .line_ = line_,
+ .column_ = column_};
}
- advance_char();
+ advanceChar();
switch (c) {
case '(':
- return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_};
+ return {.type_ = TokenType::kLParen, .value_ = "(", .line_ = line_, .column_ = column_};
case ')':
- return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_};
+ return {.type_ = TokenType::kRParen, .value_ = ")", .line_ = line_, .column_ = column_};
case ',':
- return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_};
+ return {.type_ = TokenType::kComma, .value_ = ",", .line_ = line_, .column_ = column_};
case '.':
- return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_};
+ return {.type_ = TokenType::kDot, .value_ = ".", .line_ = line_, .column_ = column_};
case '~':
- return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_};
+ return {.type_ = TokenType::kNot, .value_ = "~", .line_ = line_, .column_ = column_};
case '|':
- return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_};
+ return {.type_ = TokenType::kOr, .value_ = "|", .line_ = line_, .column_ = column_};
default:
- return {.type = TokenType::kUnkown,
- .value = source_.substr(start_pos, 1),
- .line = line_,
- .column = column_};
+ return {.type_ = TokenType::kUnkown,
+ .value_ = source_.substr(start_pos, 1),
+ .line_ = line_,
+ .column_ = column_};
}
}
@@ -119,7 +134,7 @@ class TptpLexer {
size_t line_ = 1;
size_t column_ = 1;
- void advance_char() {
+ void advanceChar() {
if (pos_ < source_.size()) {
if (source_[pos_] == '\n') {
line_++;
@@ -131,14 +146,14 @@ class TptpLexer {
}
}
- void skip_whitespace_and_comments() {
+ void skipWhitespaceAndComments() {
while (pos_ < source_.size()) {
- char c = source_[pos_];
- if (std::isspace(static_cast<unsigned char>(c))) {
- advance_char();
+ char const c = source_[pos_];
+ if (std::isspace(static_cast<unsigned char>(c)) != 0) {
+ advanceChar();
} else if (c == '%') {
while (pos_ < source_.size() && source_[pos_] != '\n') {
- advance_char();
+ advanceChar();
}
} else {
break;
@@ -155,41 +170,41 @@ class TptpParser {
}
void parseProblem(ParsedProblem& problem) {
- while (current_token_.type != TokenType::kEOF) {
- if (current_token_.type == TokenType::kWord && current_token_.value == "cnf") {
+ while (current_token_.type_ != TokenType::kEOF) {
+ if (current_token_.type_ == TokenType::kWord && current_token_.value_ == "cnf") {
advance();
expect(TokenType::kLParen);
AnnotatedFormula af;
- af.is_cnf = true;
+ af.is_cnf_ = true;
- af.name = std::string(current_token_.value);
+ af.name_ = std::string(current_token_.value_);
expect(TokenType::kWord);
expect(TokenType::kComma);
- af.role = parseRole(current_token_.value);
+ af.role_ = parseRole(current_token_.value_);
expect(TokenType::kWord);
expect(TokenType::kComma);
Clause clause;
- clause.literals.push_back(parseLiteral());
- while (current_token_.type == TokenType::kOr) {
+ clause.literals_.push_back(parseLiteral());
+ while (current_token_.type_ == TokenType::kOr) {
advance();
- clause.literals.push_back(parseLiteral());
+ clause.literals_.push_back(parseLiteral());
}
- af.clauses.push_back(std::move(clause));
+ af.clauses_.push_back(std::move(clause));
expect(TokenType::kRParen);
expect(TokenType::kDot);
- problem.formulas.push_back(std::move(af));
+ problem.formulas_.push_back(std::move(af));
variable_cache_.clear();
- } else if (current_token_.value == "fof") {
+ } else if (current_token_.value_ == "fof") {
throw std::runtime_error("FOF parsing not implemented. Line " +
- std::to_string(current_token_.line));
+ std::to_string(current_token_.line_));
} else {
throw std::runtime_error("Unknown declaration: '" +
- std::string(current_token_.value) + "'");
+ std::string(current_token_.value_) + "'");
}
}
}
@@ -198,33 +213,33 @@ class TptpParser {
TptpLexer lexer_;
TermBank& bank_;
SymbolTable& symbols_;
- Token current_token_;
+ Token current_token_{};
+ std::vector<Token> tokens_;
+ std::unordered_map<std::string_view, SymbolId> variable_cache_{};
- std::unordered_map<std::string_view, TermId> variable_cache_;
-
- void advance() { current_token_ = lexer_.next_token(); }
+ void advance() { current_token_ = lexer_.nextToken(); }
void expect(TokenType type) {
- if (current_token_.type != type) {
- throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line) +
- ", col " + std::to_string(current_token_.column) +
- ": unexpected token '" + std::string(current_token_.value) +
+ if (current_token_.type_ != type) {
+ throw std::runtime_error("Parse error at line " + std::to_string(current_token_.line_) +
+ ", col " + std::to_string(current_token_.column_) +
+ ": unexpected token '" + std::string(current_token_.value_) +
"'");
}
advance();
}
TermId parseTerm() {
- if (current_token_.type != TokenType::kWord) {
+ if (current_token_.type_ != TokenType::kWord) {
throw std::runtime_error("Expected variable or function name at line " +
- std::to_string(current_token_.line) + ", col " +
- std::to_string(current_token_.column) +
- ": unexpected token '" + std::string(current_token_.value) +
+ std::to_string(current_token_.line_) + ", col " +
+ std::to_string(current_token_.column_) +
+ ": unexpected token '" + std::string(current_token_.value_) +
"'");
}
- std::string_view name = current_token_.value;
- bool is_variable = std::isupper(static_cast<unsigned char>(name[0]));
+ std::string_view const name = current_token_.value_;
+ bool const is_variable = std::isupper(static_cast<unsigned char>(name[0])) != 0;
advance();
if (is_variable) {
@@ -233,18 +248,17 @@ class TptpParser {
if (it != variable_cache_.end()) {
return it->second;
}
- SymbolId sym = symbols_.intern(name, SymbolKind::kVariable);
- TermId var_id = bank_.makeVar(sym);
+ SymbolId const sym = symbols_.intern(name, SymbolKind::kVariable);
+ TermId const var_id = bank_.makeVar(sym);
variable_cache_[name] = var_id;
return var_id;
- } else {
- // Check if this is a function/predicate (has args) or a constant (no parens)
- if (current_token_.type == TokenType::kLParen) {
+ } // Check if this is a function/predicate (has args) or a constant (no parens)
+ if (current_token_.type_ == TokenType::kLParen) {
advance(); // consume '('
std::vector<TermId> args;
- if (current_token_.type != TokenType::kRParen) {
+ if (current_token_.type_ != TokenType::kRParen) {
args.push_back(parseTerm());
- while (current_token_.type == TokenType::kComma) {
+ while (current_token_.type_ == TokenType::kComma) {
advance();
args.push_back(parseTerm());
}
@@ -258,17 +272,17 @@ class TptpParser {
SymbolId sym = symbols_.intern(name, SymbolKind::kConstant, 0);
return bank_.makeTerm(sym, {});
}
- }
+
}
Literal parseLiteral() {
bool is_positive = true;
- if (current_token_.type == TokenType::kNot) {
+ if (current_token_.type_ == TokenType::kNot) {
is_positive = false;
advance();
}
- TermId term = parseTerm();
- return Literal{.atom = term, .is_positive = is_positive};
+ TermId const term = parseTerm();
+ return Literal{.atom_ = term, .is_positive_ = is_positive};
}
};
@@ -284,22 +298,22 @@ ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolT
if (!file.is_open()) {
throw std::runtime_error("Failed to open file: " + filename);
}
- std::string content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
+ std::string const content((std::istreambuf_iterator<char>(file)), std::istreambuf_iterator<char>());
ParsedProblem problem = parseTptpString(content, bank, symbols);
- problem.source_file = filename;
+ problem.source_file_ = filename;
return problem;
}
-std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& bank,
- SymbolTable& symbols) {
+std::vector<Clause> prepareForProving(ParsedProblem& problem, TermBank& /*bank*/,
+ SymbolTable& /*symbols*/) {
std::vector<Clause> final_clauses;
- for (auto& af : problem.formulas) {
- if (af.is_cnf) {
- for (auto& clause : af.clauses) {
- clause.rule = InferenceRule::kInput;
- clause.parent1 = kInvalidId;
- clause.parent2 = kInvalidId;
+ for (auto& af : problem.formulas_) {
+ if (af.is_cnf_) {
+ for (auto& clause : af.clauses_) {
+ clause.rule_ = InferenceRule::kInput;
+ clause.parent1_ = kInvalidId;
+ clause.parent2_ = kInvalidId;
final_clauses.push_back(std::move(clause));
}
}
diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc
index f072b8e..82e59b7 100644
--- a/src/infer/resolution.cc
+++ b/src/infer/resolution.cc
@@ -26,8 +26,12 @@
#include "atp/infer/substitution.h"
#include "atp/infer/unification.h"
+#include <cstddef>
+#include <cstdint>
+#include <optional>
#include <string>
#include <unordered_map>
+#include <utility>
#include <vector>
namespace atp {
@@ -42,7 +46,7 @@ void collectVariables(TermId term, const TermBank& bank, std::unordered_map<Term
}
// Copy args to avoid dangling ref (bank is const here, but be safe)
const Term& t = bank.getTerm(term);
- for (TermId arg : t.args) {
+ for (TermId const arg : t.args_) {
collectVariables(arg, bank, seen);
}
}
@@ -53,8 +57,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
uint32_t& next_var_id) {
// 1. Collect all variables in the clause
std::unordered_map<TermId, bool> var_set;
- for (const auto& lit : c.literals) {
- collectVariables(lit.atom, bank, var_set);
+ for (const auto& lit : c.literals_) {
+ collectVariables(lit.atom_, bank, var_set);
}
if (var_set.empty()) {
@@ -64,22 +68,22 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
// 2. Create fresh variables and build a substitution
Substitution rename_subst;
for (auto& [old_var_id, _] : var_set) {
- std::string fresh_name = "_R" + std::to_string(next_var_id++);
- SymbolId fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
- TermId fresh_var = bank.makeVar(fresh_sym);
+ std::string const fresh_name = "_R" + std::to_string(next_var_id++);
+ SymbolId const fresh_sym = symbols.intern(fresh_name, SymbolKind::kVariable);
+ TermId const fresh_var = bank.makeVar(fresh_sym);
rename_subst.bind(old_var_id, fresh_var);
}
// 3. Apply the renaming substitution to all literals
Clause renamed;
- renamed.id = c.id;
- renamed.rule = c.rule;
- renamed.parent1 = c.parent1;
- renamed.parent2 = c.parent2;
- renamed.depth = c.depth;
- for (const auto& lit : c.literals) {
- TermId new_atom = applySubstitution(rename_subst, lit.atom, bank);
- renamed.literals.push_back({.atom = new_atom, .is_positive = lit.is_positive});
+ renamed.id_ = c.id_;
+ renamed.rule_ = c.rule_;
+ renamed.parent1_ = c.parent1_;
+ renamed.parent2_ = c.parent2_;
+ renamed.depth_ = c.depth_;
+ for (const auto& lit : c.literals_) {
+ TermId const new_atom = applySubstitution(rename_subst, lit.atom_, bank);
+ renamed.literals_.push_back({.atom_ = new_atom, .is_positive_ = lit.is_positive_});
}
return renamed;
}
@@ -87,7 +91,7 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols,
std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, const Clause& c2,
size_t lit_idx2, const UnificationConfig& uconfig) {
// Must have opposite polarity
- if (c1.literals[lit_idx1].is_positive == c2.literals[lit_idx2].is_positive) {
+ if (c1.literals_[lit_idx1].is_positive_ == c2.literals_[lit_idx2].is_positive_) {
return std::nullopt;
}
@@ -99,28 +103,28 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
// Unify the complementary atoms
Substitution subst;
- if (!unify(bank, c1.literals[lit_idx1].atom, c2r.literals[lit_idx2].atom, subst, uconfig)) {
+ if (!unify(bank, c1.literals_[lit_idx1].atom_, c2r.literals_[lit_idx2].atom_, subst, uconfig)) {
return std::nullopt;
}
// Build the resolvent: all literals except the resolved pair, with subst applied
Clause resolvent;
- resolvent.rule = InferenceRule::kResolution;
- resolvent.parent1 = c1.id;
- resolvent.parent2 = c2.id;
+ resolvent.rule_ = InferenceRule::kResolution;
+ resolvent.parent1_ = c1.id_;
+ resolvent.parent2_ = c2.id_;
- for (size_t i = 0; i < c1.literals.size(); ++i) {
+ for (size_t i = 0; i < c1.literals_.size(); ++i) {
if (i != lit_idx1) {
- TermId new_atom = applySubstitution(subst, c1.literals[i].atom, bank);
- resolvent.literals.push_back(
- {.atom = new_atom, .is_positive = c1.literals[i].is_positive});
+ TermId const new_atom = applySubstitution(subst, c1.literals_[i].atom_, bank);
+ resolvent.literals_.push_back(
+ {.atom_ = new_atom, .is_positive_ = c1.literals_[i].is_positive_});
}
}
- for (size_t i = 0; i < c2r.literals.size(); ++i) {
+ for (size_t i = 0; i < c2r.literals_.size(); ++i) {
if (i != lit_idx2) {
- TermId new_atom = applySubstitution(subst, c2r.literals[i].atom, bank);
- resolvent.literals.push_back(
- {.atom = new_atom, .is_positive = c2r.literals[i].is_positive});
+ TermId const new_atom = applySubstitution(subst, c2r.literals_[i].atom_, bank);
+ resolvent.literals_.push_back(
+ {.atom_ = new_atom, .is_positive_ = c2r.literals_[i].is_positive_});
}
}
return resolvent;
@@ -129,9 +133,9 @@ std::optional<Clause> resolve(TermBank& bank, const Clause& c1, size_t lit_idx1,
std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause& c2,
const UnificationConfig& uconfig) {
std::vector<Clause> results;
- for (size_t i = 0; i < c1.literals.size(); ++i) {
- for (size_t j = 0; j < c2.literals.size(); ++j) {
- if (c1.literals[i].is_positive != c2.literals[j].is_positive) {
+ for (size_t i = 0; i < c1.literals_.size(); ++i) {
+ for (size_t j = 0; j < c2.literals_.size(); ++j) {
+ if (c1.literals_[i].is_positive_ != c2.literals_[j].is_positive_) {
if (auto r = resolve(bank, c1, i, c2, j, uconfig)) {
results.push_back(std::move(*r));
}
@@ -143,24 +147,24 @@ std::vector<Clause> allResolvents(TermBank& bank, const Clause& c1, const Clause
std::vector<Clause> factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) {
std::vector<Clause> results;
- for (size_t i = 0; i < c.literals.size(); ++i) {
- for (size_t j = i + 1; j < c.literals.size(); ++j) {
- if (c.literals[i].is_positive != c.literals[j].is_positive) {
+ for (size_t i = 0; i < c.literals_.size(); ++i) {
+ for (size_t j = i + 1; j < c.literals_.size(); ++j) {
+ if (c.literals_[i].is_positive_ != c.literals_[j].is_positive_) {
continue; // Must have same polarity
}
Substitution subst;
- if (!unify(bank, c.literals[i].atom, c.literals[j].atom, subst, uconfig)) {
+ if (!unify(bank, c.literals_[i].atom_, c.literals_[j].atom_, subst, uconfig)) {
continue;
}
// Build factored clause: drop literal j, apply subst to all
Clause factored;
- factored.rule = InferenceRule::kFactoring;
- factored.parent1 = c.id;
- for (size_t k = 0; k < c.literals.size(); ++k) {
+ factored.rule_ = InferenceRule::kFactoring;
+ factored.parent1_ = c.id_;
+ for (size_t k = 0; k < c.literals_.size(); ++k) {
if (k != j) {
- TermId new_atom = applySubstitution(subst, c.literals[k].atom, bank);
- factored.literals.push_back(
- {.atom = new_atom, .is_positive = c.literals[k].is_positive});
+ TermId const new_atom = applySubstitution(subst, c.literals_[k].atom_, bank);
+ factored.literals_.push_back(
+ {.atom_ = new_atom, .is_positive_ = c.literals_[k].is_positive_});
}
}
results.push_back(std::move(factored));
diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc
index a7ce617..8710fb0 100644
--- a/src/infer/substitution.cc
+++ b/src/infer/substitution.cc
@@ -22,6 +22,8 @@
#include "atp/core/term_bank.h"
#include "atp/core/types.h"
+#include <vector>
+
namespace atp {
bool Substitution::bind(TermId var, TermId term) {
@@ -66,8 +68,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const {
// 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<TermId> old_args(t.args); // copy!
+ SymbolId const sym = t.symbol_id_;
+ std::vector<TermId> const old_args(t.args_); // copy!
if (old_args.empty()) {
// Constant or 0-arity — no substitution needed
@@ -78,8 +80,8 @@ TermId Substitution::apply(TermId term, TermBank& bank) const {
std::vector<TermId> new_args;
new_args.reserve(old_args.size());
bool changed = false;
- for (TermId arg : old_args) {
- TermId new_arg = apply(arg, bank);
+ for (TermId const arg : old_args) {
+ TermId const new_arg = apply(arg, bank);
new_args.push_back(new_arg);
if (new_arg != arg) {
changed = true;
@@ -105,7 +107,7 @@ bool Substitution::occursIn(TermId var, TermId term, const TermBank& bank) const
}
const Term& t = bank.getTerm(term);
- for (TermId arg : t.args) {
+ for (TermId const arg : t.args_) {
if (occursIn(var, arg, bank)) {
return true;
}
diff --git a/src/infer/unification.cc b/src/infer/unification.cc
index 66e1af6..c42bf67 100644
--- a/src/infer/unification.cc
+++ b/src/infer/unification.cc
@@ -18,9 +18,14 @@
#include "atp/infer/unification.h"
+#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
#include "atp/core/types.h"
#include "atp/infer/substitution.h"
+#include <cstddef>
+#include <vector>
+
namespace atp {
bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
@@ -33,7 +38,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
}
if (bank.isVariable(t1)) {
- if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) {
+ if (config.enable_occurs_check_ && subst.occursIn(t1, t2, bank)) {
return false;
}
subst.bind(t1, t2);
@@ -41,7 +46,7 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
}
if (bank.isVariable(t2)) {
- if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) {
+ if (config.enable_occurs_check_ && subst.occursIn(t2, t1, bank)) {
return false;
}
subst.bind(t2, t1);
@@ -51,12 +56,12 @@ bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst,
const Term& term1 = bank.getTerm(t1);
const Term& term2 = bank.getTerm(t2);
- if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) {
+ 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)) {
+ if (!unify(bank, term1.args_[i], term2.args_[i], subst, config)) {
return false;
}
}
@@ -73,12 +78,12 @@ TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank)
// 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<TermId> old_args(t.args); // copy!
+ SymbolId const sym = t.symbol_id_;
+ std::vector<TermId> const old_args(t.args_); // copy!
std::vector<TermId> new_args;
new_args.reserve(old_args.size());
- for (TermId arg : old_args) {
+ for (TermId const arg : old_args) {
new_args.push_back(applySubstitution(subst, arg, bank));
}
return bank.makeTerm(sym, new_args);
diff --git a/src/main.cc b/src/main.cc
index bd385d8..81dbc91 100644
--- a/src/main.cc
+++ b/src/main.cc
@@ -27,8 +27,10 @@
#include "atp/search/prover.h"
#include <cstdlib>
+#include <exception>
#include <iostream>
#include <string>
+#include <utility>
int main(int argc, char* argv[]) {
std::cerr << "richard-atp-engine Copyright (C) 2026 Richard Qin\n"
@@ -41,7 +43,7 @@ int main(int argc, char* argv[]) {
return EXIT_FAILURE;
}
- const std::string filepath = argv[1];
+ const std::string kFilepath = argv[1];
try {
// 1. Initialize core modules
@@ -50,9 +52,9 @@ int main(int argc, char* argv[]) {
atp::ClauseStore store;
// 2. Parse TPTP input
- auto problem = atp::parseTptpFile(filepath, bank, symbols);
+ auto problem = atp::parseTptpFile(kFilepath, bank, symbols);
- std::cerr << "% Parsed " << problem.formulas.size() << " formulas from " << filepath
+ std::cerr << "% Parsed " << problem.formulas_.size() << " formulas from " << kFilepath
<< "\n";
// 3. Prepare clauses for proving
@@ -63,28 +65,28 @@ int main(int argc, char* argv[]) {
// 4. Run the prover
atp::Prover prover(bank, store);
prover.addClauses(std::move(clauses));
- atp::ProverResult result = prover.prove();
+ atp::ProverResult const result = prover.prove();
// 5. Output result (SZS format)
switch (result) {
case atp::ProverResult::kTheorem: {
- std::cout << "% SZS status Theorem for " << filepath << "\n\n";
+ std::cout << "% SZS status Theorem for " << kFilepath << "\n\n";
// Extract and print proof
auto eid = prover.getEmptyClauseId();
if (eid.has_value()) {
auto proof = atp::extractProof(store, *eid);
- std::cout << "% SZS output start Proof for " << filepath << "\n";
+ std::cout << "% SZS output start Proof for " << kFilepath << "\n";
std::cout << atp::formatProof(proof, store, bank);
- std::cout << "% SZS output end Proof for " << filepath << "\n";
+ std::cout << "% SZS output end Proof for " << kFilepath << "\n";
}
break;
}
case atp::ProverResult::kSaturation:
- std::cout << "% SZS status Satisfiable for " << filepath << "\n";
+ std::cout << "% SZS status Satisfiable for " << kFilepath << "\n";
break;
case atp::ProverResult::kTimeout:
- std::cout << "% SZS status Timeout for " << filepath << "\n";
+ std::cout << "% SZS status Timeout for " << kFilepath << "\n";
break;
}
diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc
index 183ab2e..a0d5a11 100644
--- a/src/proof/proof_trace.cc
+++ b/src/proof/proof_trace.cc
@@ -19,11 +19,15 @@
#include "atp/proof/proof_trace.h"
#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
#include "atp/core/symbol_table.h"
#include "atp/core/term.h"
+#include "atp/core/term_bank.h"
#include "atp/core/types.h"
#include <algorithm>
+#include <array>
+#include <cstddef>
#include <stack>
#include <string>
#include <unordered_map>
@@ -43,29 +47,29 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
worklist.push(empty_clause_id);
while (!worklist.empty()) {
- ClauseId cid = worklist.top();
+ const ClauseId kCid = worklist.top();
worklist.pop();
- if (cid == kInvalidId) {
+ if (kCid == kInvalidId) {
continue;
}
- if (visited.count(cid) > 0) {
+ if (visited.contains(kCid)) {
continue;
}
- visited.insert(cid);
+ visited.insert(kCid);
- const Clause& c = store.getClause(cid);
+ const Clause& c = store.getClause(kCid);
steps.push_back({
- .clause_id = cid,
- .rule = c.rule,
- .parent1 = c.parent1,
- .parent2 = c.parent2,
+ .clause_id_ = kCid,
+ .rule_ = c.rule_,
+ .parent1_ = c.parent1_,
+ .parent2_ = c.parent2_,
});
// Recurse into parents (axioms have kInvalidId parents, which are
// filtered by the check at the top of the loop)
- worklist.push(c.parent1);
- worklist.push(c.parent2);
+ worklist.push(c.parent1_);
+ worklist.push(c.parent2_);
}
// Reverse: axioms (leaves) first → empty clause (root) last
@@ -77,18 +81,18 @@ std::vector<ProofStep> extractProof(const ClauseStore& store, ClauseId empty_cla
std::string termToString(TermId id, const TermBank& bank) {
const Term& t = bank.getTerm(id);
- std::string name(bank.symbols().getName(t.symbol_id));
+ std::string name(bank.symbols().getName(t.symbol_id_));
- if (t.args.empty()) {
+ if (t.args_.empty()) {
return name;
}
std::string result = name + "(";
- for (size_t i = 0; i < t.args.size(); ++i) {
+ for (size_t i = 0; i < t.args_.size(); ++i) {
if (i > 0) {
result += ",";
}
- result += termToString(t.args[i], bank);
+ result += termToString(t.args_[i], bank);
}
result += ")";
return result;
@@ -101,15 +105,15 @@ 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 const char kBaseNames[] = {'X', 'Y', 'Z', 'W', 'V', 'U'};
- static constexpr size_t kBaseCount = sizeof(kBaseNames);
+ static constexpr std::array<char, 6> kBaseNames = {'X', 'Y', 'Z', 'W', 'V', 'U'};
+ static constexpr size_t kBaseCount = kBaseNames.size();
- char base = kBaseNames[index % kBaseCount];
- size_t suffix = index / kBaseCount;
- if (suffix == 0) {
- return std::string(1, base);
+ const char kBase = kBaseNames[index % kBaseCount];
+ const size_t kSuffix = index / kBaseCount;
+ if (kSuffix == 0) {
+ return std::string{kBase};
}
- return std::string(1, base) + std::to_string(suffix);
+ return std::string{kBase} + std::to_string(kSuffix);
}
/// Pretty-print a term, renaming variables to readable names.
@@ -121,29 +125,44 @@ std::string termToPretty(TermId id, const TermBank& bank,
if (it != var_map.end()) {
return it->second;
}
- std::string name = prettyVarName(var_map.size());
- var_map[id] = name;
- return name;
+ const std::string kName = prettyVarName(var_map.size());
+ var_map[id] = kName;
+ return kName;
}
const Term& t = bank.getTerm(id);
- std::string name(bank.symbols().getName(t.symbol_id));
+ std::string name(bank.symbols().getName(t.symbol_id_));
- if (t.args.empty()) {
+ if (t.args_.empty()) {
return name;
}
std::string result = name + "(";
- for (size_t i = 0; i < t.args.size(); ++i) {
+ for (size_t i = 0; i < t.args_.size(); ++i) {
if (i > 0) {
result += ",";
}
- result += termToPretty(t.args[i], bank, var_map);
+ result += termToPretty(t.args_[i], bank, var_map);
}
result += ")";
return result;
}
+// ruleToString
+
+std::string ruleToString(InferenceRule rule) {
+ switch (rule) {
+ case InferenceRule::kInput:
+ return "input";
+ case InferenceRule::kResolution:
+ return "resolution";
+ case InferenceRule::kFactoring:
+ return "factoring";
+ default:
+ return "unknown";
+ }
+}
+
} // namespace
// clauseToString
@@ -157,33 +176,18 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) {
std::unordered_map<TermId, std::string> var_map;
std::string result;
- for (size_t i = 0; i < clause.literals.size(); ++i) {
+ for (size_t i = 0; i < clause.literals_.size(); ++i) {
if (i > 0) {
result += " ∨ ";
}
- if (!clause.literals[i].is_positive) {
+ if (!clause.literals_[i].is_positive_) {
result += "¬";
}
- result += termToPretty(clause.literals[i].atom, bank, var_map);
+ result += termToPretty(clause.literals_[i].atom_, bank, var_map);
}
return result;
}
-// ruleToString
-
-static std::string ruleToString(InferenceRule rule) {
- switch (rule) {
- case InferenceRule::kInput:
- return "input";
- case InferenceRule::kResolution:
- return "resolution";
- case InferenceRule::kFactoring:
- return "factoring";
- default:
- return "unknown";
- }
-}
-
// formatProof
std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore& store,
@@ -191,10 +195,10 @@ std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore&
// Build a local renumbering: internal ClauseId → sequential proof step number
std::unordered_map<ClauseId, size_t> id_to_step;
for (size_t i = 0; i < proof.size(); ++i) {
- id_to_step[proof[i].clause_id] = i + 1; // 1-based
+ id_to_step[proof[i].clause_id_] = i + 1; // 1-based
}
- auto localName = [&](ClauseId cid) -> std::string {
+ auto local_name = [&](ClauseId cid) -> std::string {
auto it = id_to_step.find(cid);
if (it != id_to_step.end()) {
return std::to_string(it->second);
@@ -206,17 +210,17 @@ std::string formatProof(const std::vector<ProofStep>& proof, const ClauseStore&
std::string result;
for (size_t i = 0; i < proof.size(); ++i) {
const auto& step = proof[i];
- const Clause& c = store.getClause(step.clause_id);
+ const Clause& c = store.getClause(step.clause_id_);
result += std::to_string(i + 1) + ". ";
- result += "[" + ruleToString(step.rule) + "] ";
+ result += "[" + ruleToString(step.rule_) + "] ";
result += clauseToString(c, bank);
// Show parents for derived clauses
- if (step.parent1 != kInvalidId) {
- result += " [" + localName(step.parent1);
- if (step.parent2 != kInvalidId) {
- result += ", " + localName(step.parent2);
+ if (step.parent1_ != kInvalidId) {
+ result += " [" + local_name(step.parent1_);
+ if (step.parent2_ != kInvalidId) {
+ result += ", " + local_name(step.parent2_);
}
result += "]";
}
diff --git a/src/search/prover.cc b/src/search/prover.cc
index 5b68e9d..2c2de40 100644
--- a/src/search/prover.cc
+++ b/src/search/prover.cc
@@ -18,6 +18,9 @@
#include "atp/search/prover.h"
+#include "atp/core/clause.h"
+#include "atp/core/clause_store.h"
+#include "atp/core/term_bank.h"
#include "atp/core/types.h"
#include "atp/infer/resolution.h"
#include "atp/infer/unification.h"
@@ -25,16 +28,21 @@
#include "atp/simplify/tautology.h"
#include <algorithm>
+#include <cstddef>
+#include <cstdint>
+#include <optional>
+#include <utility>
+#include <vector>
namespace atp {
Prover::Prover(TermBank& bank, ClauseStore& store, ProverConfig config)
- : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator) {}
+ : bank_(bank), store_(store), config_(std::move(config)), unprocessed_(config_.comparator_) {}
void Prover::addClauses(std::vector<Clause> clauses) {
for (auto& clause : clauses) {
- clause.depth = 0;
- ClauseId id = store_.addClause(clause);
+ clause.depth_ = 0;
+ ClauseId const id = store_.addClause(clause);
unprocessed_.push(store_.getClause(id));
}
}
@@ -44,7 +52,7 @@ ProverResult Prover::prove() {
while (!unprocessed_.empty()) {
// Resource limits
- if (iterations >= config_.max_iterations || store_.size() >= config_.max_clauses) {
+ if (iterations >= config_.max_iterations_ || store_.size() >= config_.max_clauses_) {
return ProverResult::kTimeout;
}
++iterations;
@@ -55,7 +63,7 @@ ProverResult Prover::prove() {
// 2. Check if given is itself the empty clause
if (given.isEmpty()) {
- empty_clause_id_ = given.id;
+ empty_clause_id_ = given.id_;
return ProverResult::kTheorem;
}
@@ -65,7 +73,7 @@ ProverResult Prover::prove() {
}
bool forward_subsumed = false;
- for (ClauseId pid : processed_) {
+ for (ClauseId const pid : processed_) {
if (subsumes(store_.getClause(pid), given)) {
forward_subsumed = true;
break;
@@ -84,14 +92,14 @@ ProverResult Prover::prove() {
// 5. Generate new clauses
// Inference BEFORE adding given to processed — matches doc §4.6.
std::vector<Clause> new_clauses;
- const UnificationConfig uconfig{.enable_occurs_check = config_.enable_occurs_check};
+ const UnificationConfig kUconfig{.enable_occurs_check_ = config_.enable_occurs_check_};
// 5a. Resolve given with every processed clause (both directions)
- for (ClauseId pid : processed_) {
+ 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);
+ 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));
@@ -102,13 +110,13 @@ ProverResult Prover::prove() {
}
// 5b. Factor given (only once)
- auto factors = factor(bank_, given, uconfig);
+ auto factors = factor(bank_, given, kUconfig);
for (auto& f : factors) {
new_clauses.push_back(std::move(f));
}
// 6. Add given to processed AFTER inference
- processed_.push_back(given.id);
+ processed_.push_back(given.id_);
// 7. Process new clauses
for (auto& nc : new_clauses) {
@@ -125,17 +133,17 @@ ProverResult Prover::prove() {
}
// 7c. Set depth
- uint32_t d1 = (nc.parent1 != kInvalidId) ? store_.getClause(nc.parent1).depth : 0;
- uint32_t d2 = (nc.parent2 != kInvalidId) ? store_.getClause(nc.parent2).depth : 0;
- nc.depth = static_cast<uint16_t>(std::max(d1, d2) + 1);
+ 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<uint16_t>(std::max(d1, d2) + 1);
// 7d. Store the clause (needed for forward subsumption check)
- ClauseId nid = store_.addClause(nc);
+ 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 pid : processed_) {
+ for (ClauseId const pid : processed_) {
if (subsumes(store_.getClause(pid), stored_nc)) {
new_subsumed = true;
break;
diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc
index 3756d82..0038ad1 100644
--- a/src/simplify/subsumption.cc
+++ b/src/simplify/subsumption.cc
@@ -18,16 +18,18 @@
#include "atp/simplify/subsumption.h"
+#include "atp/core/clause.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) {
+ 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) {
+ 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;
}
diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc
index 70bdced..e35d874 100644
--- a/src/simplify/tautology.cc
+++ b/src/simplify/tautology.cc
@@ -18,14 +18,16 @@
#include "atp/simplify/tautology.h"
+#include "atp/core/clause.h"
+
#include <cstddef>
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) {
+ if (clause.literals_[i].atom_ == clause.literals_[j].atom_ &&
+ clause.literals_[i].is_positive_ != clause.literals_[j].is_positive_) {
return true;
}
}
generated by cgit v1.2.3 (git 2.46.0) at 2026-10-29 03:04:57 +0000