From bf4f464cec8b6515d9e5131d43847ef9b2fd21d1 Mon Sep 17 00:00:00 2001 From: Richard Qin Date: Sat, 4 Apr 2026 05:21:26 +0800 Subject: style: reformat codebase with consistent indentation --- src/core/clause_store.cc | 1 + src/core/symbol_table.cc | 8 +-- src/core/term_bank.cc | 2 + src/frontend/tptp_parser.cc | 132 ++++++++++++++++++++++----------------- src/index/discrim_tree.cc | 2 - src/infer/resolution.cc | 12 ++-- src/infer/substitution.cc | 1 + src/infer/unification.cc | 90 +++++++++++++------------- src/main.cc | 4 +- src/normalize/clausifier.cc | 2 - src/proof/proof_trace.cc | 29 +++++---- src/rewrite/ordering.cc | 2 - src/rewrite/paramodulation.cc | 2 - src/search/prover.cc | 22 +++---- src/simplify/subsumption.cc | 31 +++++---- src/simplify/tautology.cc | 21 ++++--- src/strategy/problem_analyzer.cc | 2 - 17 files changed, 186 insertions(+), 177 deletions(-) (limited to 'src') diff --git a/src/core/clause_store.cc b/src/core/clause_store.cc index a0adbe6..75959c3 100644 --- a/src/core/clause_store.cc +++ b/src/core/clause_store.cc @@ -17,6 +17,7 @@ */ #include "atp/core/clause_store.h" + #include #include diff --git a/src/core/symbol_table.cc b/src/core/symbol_table.cc index 261805a..42c7dd8 100644 --- a/src/core/symbol_table.cc +++ b/src/core/symbol_table.cc @@ -17,15 +17,16 @@ */ #include "atp/core/symbol_table.h" + #include "atp/core/types.h" + #include #include #include namespace atp { -SymbolId SymbolTable::intern(std::string_view name, SymbolKind kind, uint16_t arity, - SortId sort) { +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; @@ -58,5 +59,4 @@ size_t SymbolTable::size() const { return infos_.size(); } -} // namespace atp - +} // namespace atp diff --git a/src/core/term_bank.cc b/src/core/term_bank.cc index 53b4f0c..8c8ef29 100644 --- a/src/core/term_bank.cc +++ b/src/core/term_bank.cc @@ -17,7 +17,9 @@ */ #include "atp/core/term_bank.h" + #include "atp/core/types.h" + #include namespace atp { diff --git a/src/frontend/tptp_parser.cc b/src/frontend/tptp_parser.cc index df8baeb..2f32522 100644 --- a/src/frontend/tptp_parser.cc +++ b/src/frontend/tptp_parser.cc @@ -17,10 +17,12 @@ */ #include "atp/frontend/tptp_parser.h" + #include "atp/core/clause.h" #include "atp/core/literal.h" #include "atp/core/term_bank.h" #include "atp/core/types.h" + #include #include #include @@ -31,31 +33,29 @@ namespace atp { -FormulaRole parseRole(std::string_view role_str){ - if (role_str == "axiom") return FormulaRole::kAxiom; - if (role_str == "hypothesis") return FormulaRole::kHypothesis; - if (role_str == "definition") return FormulaRole::kDefinition; - if (role_str == "assumption") return FormulaRole::kAssumption; - if (role_str == "lemma") return FormulaRole::kLemma; - if (role_str == "theorem") return FormulaRole::kTheorem; - if (role_str == "conjecture") return FormulaRole::kConjecture; - if (role_str == "negated_conjecture") return FormulaRole::kNegatedConjecture; - if (role_str == "plain") return FormulaRole::kPlain; +FormulaRole parseRole(std::string_view role_str) { + if (role_str == "axiom") + return FormulaRole::kAxiom; + if (role_str == "hypothesis") + return FormulaRole::kHypothesis; + if (role_str == "definition") + return FormulaRole::kDefinition; + if (role_str == "assumption") + return FormulaRole::kAssumption; + if (role_str == "lemma") + return FormulaRole::kLemma; + if (role_str == "theorem") + return FormulaRole::kTheorem; + if (role_str == "conjecture") + return FormulaRole::kConjecture; + if (role_str == "negated_conjecture") + return FormulaRole::kNegatedConjecture; + if (role_str == "plain") + return FormulaRole::kPlain; return FormulaRole::kPlain; } - -enum class TokenType { - kWord, - kLParen, - kRParen, - kOr, - kNot, - kDot, - kComma, - kEOF, - kUnkown -}; +enum class TokenType { kWord, kLParen, kRParen, kOr, kNot, kDot, kComma, kEOF, kUnkown }; struct Token { TokenType type; @@ -65,7 +65,7 @@ struct Token { }; class TptpLexer { -public: + public: explicit TptpLexer(std::string_view input) : source_(input) {} Token next_token() { @@ -80,25 +80,40 @@ public: char c = source_[pos_]; if (std::isalpha(static_cast(c)) || c == '_') { - while (pos_ < source_.size() && (std::isalnum(static_cast(source_[pos_])) || source_[pos_] == '_')) { + while ( + pos_ < source_.size() && + (std::isalnum(static_cast(source_[pos_])) || source_[pos_] == '_')) { advance_char(); } - 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(); switch (c) { - case '(': return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_}; - case ')': return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_}; - case ',': return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_}; - case '.': return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_}; - case '~': return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_}; - case '|': return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_}; - default: return {.type = TokenType::kUnkown, .value = source_.substr(start_pos, 1), .line = line_, .column = column_}; + case '(': + return {.type = TokenType::kLParen, .value = "(", .line = line_, .column = column_}; + case ')': + return {.type = TokenType::kRParen, .value = ")", .line = line_, .column = column_}; + case ',': + return {.type = TokenType::kComma, .value = ",", .line = line_, .column = column_}; + case '.': + return {.type = TokenType::kDot, .value = ".", .line = line_, .column = column_}; + case '~': + return {.type = TokenType::kNot, .value = "~", .line = line_, .column = column_}; + case '|': + return {.type = TokenType::kOr, .value = "|", .line = line_, .column = column_}; + default: + return {.type = TokenType::kUnkown, + .value = source_.substr(start_pos, 1), + .line = line_, + .column = column_}; } } -private: + private: std::string_view source_; size_t pos_ = 0; size_t line_ = 1; @@ -133,8 +148,9 @@ private: }; class TptpParser { -public: - explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols) : lexer_(input), bank_(bank), symbols_(symbols) { + public: + explicit TptpParser(std::string_view input, TermBank& bank, SymbolTable& symbols) + : lexer_(input), bank_(bank), symbols_(symbols) { advance(); } @@ -146,11 +162,11 @@ public: AnnotatedFormula af; af.is_cnf = true; - + af.name = std::string(current_token_.value); expect(TokenType::kWord); expect(TokenType::kComma); - + af.role = parseRole(current_token_.value); expect(TokenType::kWord); expect(TokenType::kComma); @@ -169,14 +185,16 @@ public: variable_cache_.clear(); } else if (current_token_.value == "fof") { - throw std::runtime_error("FOF parsing not implemented. Line " + std::to_string(current_token_.line)); + throw std::runtime_error("FOF parsing not implemented. Line " + + std::to_string(current_token_.line)); } else { - throw std::runtime_error("Unknown declaration: '" + std::string(current_token_.value) + "'"); + throw std::runtime_error("Unknown declaration: '" + + std::string(current_token_.value) + "'"); } } } -private: + private: TptpLexer lexer_; TermBank& bank_; SymbolTable& symbols_; @@ -184,24 +202,25 @@ private: std::unordered_map variable_cache_; - void advance() { - current_token_ = lexer_.next_token(); - } + void advance() { current_token_ = lexer_.next_token(); } 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) + "'"); + 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) { - 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) + "'"); + 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::string_view name = current_token_.value; @@ -253,14 +272,14 @@ private: } }; -ParsedProblem parseTptpString(const std::string &input, TermBank &bank, SymbolTable &symbols){ +ParsedProblem parseTptpString(const std::string& input, TermBank& bank, SymbolTable& symbols) { ParsedProblem problem; TptpParser parser(input, bank, symbols); parser.parseProblem(problem); return problem; } -ParsedProblem parseTptpFile(const std::string &filename, TermBank &bank, SymbolTable &symbols){ +ParsedProblem parseTptpFile(const std::string& filename, TermBank& bank, SymbolTable& symbols) { std::ifstream file(filename, std::ios::binary); if (!file.is_open()) { throw std::runtime_error("Failed to open file: " + filename); @@ -271,12 +290,13 @@ ParsedProblem parseTptpFile(const std::string &filename, TermBank &bank, SymbolT return problem; } -std::vector prepareForProving(ParsedProblem &problem, TermBank &bank, SymbolTable &symbols){ +std::vector prepareForProving(ParsedProblem& problem, TermBank& bank, + SymbolTable& symbols) { std::vector final_clauses; - for (auto& af : problem.formulas){ - if (af.is_cnf){ - for (auto& clause : af.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; @@ -287,4 +307,4 @@ std::vector prepareForProving(ParsedProblem &problem, TermBank &bank, Sy return final_clauses; } -} // namespace atp +} // namespace atp diff --git a/src/index/discrim_tree.cc b/src/index/discrim_tree.cc index b62ffd0..17c63f8 100644 --- a/src/index/discrim_tree.cc +++ b/src/index/discrim_tree.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/src/infer/resolution.cc b/src/infer/resolution.cc index 3c82460..f072b8e 100644 --- a/src/infer/resolution.cc +++ b/src/infer/resolution.cc @@ -17,6 +17,7 @@ */ #include "atp/infer/resolution.h" + #include "atp/core/clause.h" #include "atp/core/symbol_table.h" #include "atp/core/term.h" @@ -34,8 +35,7 @@ namespace atp { namespace { /// Recursively collect all variable TermIds appearing in a term. -void collectVariables(TermId term, const TermBank& bank, - std::unordered_map& seen) { +void collectVariables(TermId term, const TermBank& bank, std::unordered_map& seen) { if (bank.isVariable(term)) { seen[term] = true; return; @@ -84,9 +84,8 @@ Clause renameVariables(const Clause& c, TermBank& bank, SymbolTable& symbols, return renamed; } -std::optional resolve(TermBank& bank, const Clause& c1, size_t lit_idx1, - const Clause& c2, size_t lit_idx2, - const UnificationConfig& uconfig) { +std::optional 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) { return std::nullopt; @@ -142,8 +141,7 @@ std::vector allResolvents(TermBank& bank, const Clause& c1, const Clause return results; } -std::vector factor(TermBank& bank, const Clause& c, - const UnificationConfig& uconfig) { +std::vector factor(TermBank& bank, const Clause& c, const UnificationConfig& uconfig) { std::vector results; for (size_t i = 0; i < c.literals.size(); ++i) { for (size_t j = i + 1; j < c.literals.size(); ++j) { diff --git a/src/infer/substitution.cc b/src/infer/substitution.cc index c570676..a7ce617 100644 --- a/src/infer/substitution.cc +++ b/src/infer/substitution.cc @@ -17,6 +17,7 @@ */ #include "atp/infer/substitution.h" + #include "atp/core/term.h" #include "atp/core/term_bank.h" #include "atp/core/types.h" diff --git a/src/infer/unification.cc b/src/infer/unification.cc index be8a025..66e1af6 100644 --- a/src/infer/unification.cc +++ b/src/infer/unification.cc @@ -16,72 +16,72 @@ * along with this program. If not, see . */ - #include "atp/infer/unification.h" + #include "atp/core/types.h" #include "atp/infer/substitution.h" namespace atp { - bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, +bool unify(const TermBank& bank, TermId t1, TermId t2, Substitution& subst, const UnificationConfig& config) { - t1 = subst.resolve(t1, bank); - t2 = subst.resolve(t2, bank); + t1 = subst.resolve(t1, bank); + t2 = subst.resolve(t2, bank); - if (t1 == t2) { - return true; - } + if (t1 == t2) { + return true; + } - if (bank.isVariable(t1)) { - if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { - return false; - } - subst.bind(t1, t2); - return true; + if (bank.isVariable(t1)) { + if (config.enable_occurs_check && subst.occursIn(t1, t2, bank)) { + return false; } + subst.bind(t1, t2); + return true; + } - if (bank.isVariable(t2)) { - if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { - return false; - } - subst.bind(t2, t1); - return true; + if (bank.isVariable(t2)) { + if (config.enable_occurs_check && subst.occursIn(t2, t1, bank)) { + return false; } + subst.bind(t2, t1); + return true; + } + + const Term& term1 = bank.getTerm(t1); + const Term& term2 = bank.getTerm(t2); - const Term& term1 = bank.getTerm(t1); - const Term& term2 = bank.getTerm(t2); + if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + return false; + } - if (term1.symbol_id != term2.symbol_id || term1.arity() != term2.arity()) { + for (size_t i = 0; i < term1.arity(); ++i) { + if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { return false; } + } - for (size_t i = 0; i < term1.arity(); ++i) { - if (!unify(bank, term1.args[i], term2.args[i], subst, config)) { - return false; - } - } + return true; +} - return true; +TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { + term = subst.resolve(term, bank); + if (bank.isVariable(term)) { + return term; } - TermId applySubstitution(const Substitution& subst, TermId term, TermBank& bank) { - term = subst.resolve(term, bank); - if (bank.isVariable(term)) { - return term; - } - - // IMPORTANT: Copy args and symbol_id BEFORE recursing. - // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. - const Term& t = bank.getTerm(term); - SymbolId sym = t.symbol_id; - std::vector old_args(t.args); // copy! + // IMPORTANT: Copy args and symbol_id BEFORE recursing. + // Recursive calls may call bank.makeTerm() → realloc terms_ → invalidate refs. + const Term& t = bank.getTerm(term); + SymbolId sym = t.symbol_id; + std::vector old_args(t.args); // copy! - std::vector new_args; - new_args.reserve(old_args.size()); - for (TermId arg : old_args) { - new_args.push_back(applySubstitution(subst, arg, bank)); - } - return bank.makeTerm(sym, new_args); + std::vector new_args; + new_args.reserve(old_args.size()); + for (TermId arg : old_args) { + new_args.push_back(applySubstitution(subst, arg, bank)); } + return bank.makeTerm(sym, new_args); +} } // namespace atp \ No newline at end of file diff --git a/src/main.cc b/src/main.cc index bf49c02..bd385d8 100644 --- a/src/main.cc +++ b/src/main.cc @@ -52,8 +52,8 @@ int main(int argc, char* argv[]) { // 2. Parse TPTP input auto problem = atp::parseTptpFile(filepath, bank, symbols); - std::cerr << "% Parsed " << problem.formulas.size() - << " formulas from " << filepath << "\n"; + std::cerr << "% Parsed " << problem.formulas.size() << " formulas from " << filepath + << "\n"; // 3. Prepare clauses for proving auto clauses = atp::prepareForProving(problem, bank, symbols); diff --git a/src/normalize/clausifier.cc b/src/normalize/clausifier.cc index b62ffd0..17c63f8 100644 --- a/src/normalize/clausifier.cc +++ b/src/normalize/clausifier.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/src/proof/proof_trace.cc b/src/proof/proof_trace.cc index 66038ba..183ab2e 100644 --- a/src/proof/proof_trace.cc +++ b/src/proof/proof_trace.cc @@ -17,6 +17,7 @@ */ #include "atp/proof/proof_trace.h" + #include "atp/core/clause.h" #include "atp/core/symbol_table.h" #include "atp/core/term.h" @@ -31,7 +32,7 @@ namespace atp { -// ─── extractProof +// extractProof // DFS from empty clause back to axioms, collect all participating clauses, // then reverse for topological order (axioms first). @@ -72,7 +73,7 @@ std::vector extractProof(const ClauseStore& store, ClauseId empty_cla return steps; } -// ─── termToString (public — raw names) ────────────────────────────────── +// termToString std::string termToString(TermId id, const TermBank& bank) { const Term& t = bank.getTerm(id); @@ -93,7 +94,7 @@ std::string termToString(TermId id, const TermBank& bank) { return result; } -// ─── Pretty variable names ────────────────────────────────────────────── +// Pretty variable names namespace { @@ -145,7 +146,7 @@ std::string termToPretty(TermId id, const TermBank& bank, } // namespace -// ─── clauseToString ───────────────────────────────────────────────────── +// clauseToString std::string clauseToString(const Clause& clause, const TermBank& bank) { if (clause.isEmpty()) { @@ -168,21 +169,25 @@ std::string clauseToString(const Clause& clause, const TermBank& bank) { return result; } -// ─── ruleToString +// 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"; + case InferenceRule::kInput: + return "input"; + case InferenceRule::kResolution: + return "resolution"; + case InferenceRule::kFactoring: + return "factoring"; + default: + return "unknown"; } } -// ─── formatProof +// formatProof -std::string formatProof(const std::vector& proof, - const ClauseStore& store, const TermBank& bank) { +std::string formatProof(const std::vector& proof, const ClauseStore& store, + const TermBank& bank) { // Build a local renumbering: internal ClauseId → sequential proof step number std::unordered_map id_to_step; for (size_t i = 0; i < proof.size(); ++i) { diff --git a/src/rewrite/ordering.cc b/src/rewrite/ordering.cc index b62ffd0..17c63f8 100644 --- a/src/rewrite/ordering.cc +++ b/src/rewrite/ordering.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/src/rewrite/paramodulation.cc b/src/rewrite/paramodulation.cc index b62ffd0..17c63f8 100644 --- a/src/rewrite/paramodulation.cc +++ b/src/rewrite/paramodulation.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - diff --git a/src/search/prover.cc b/src/search/prover.cc index e1b117b..5b68e9d 100644 --- a/src/search/prover.cc +++ b/src/search/prover.cc @@ -17,6 +17,7 @@ */ #include "atp/search/prover.h" + #include "atp/core/types.h" #include "atp/infer/resolution.h" #include "atp/infer/unification.h" @@ -28,10 +29,7 @@ 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 clauses) { for (auto& clause : clauses) { @@ -46,8 +44,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; @@ -81,9 +78,8 @@ ProverResult Prover::prove() { // 4. Backward subsumption // Remove from processed all clauses that are subsumed by given. // Use erase-remove idiom for O(n) scan instead of repeated erase. - std::erase_if(processed_, [&](ClauseId pid) { - return subsumes(given, store_.getClause(pid)); - }); + std::erase_if(processed_, + [&](ClauseId pid) { return subsumes(given, store_.getClause(pid)); }); // 5. Generate new clauses // Inference BEFORE adding given to processed — matches doc §4.6. @@ -129,12 +125,8 @@ 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; + 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(std::max(d1, d2) + 1); // 7d. Store the clause (needed for forward subsumption check) diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc index cf243c9..3756d82 100644 --- a/src/simplify/subsumption.cc +++ b/src/simplify/subsumption.cc @@ -18,25 +18,24 @@ #include "atp/simplify/subsumption.h" - namespace atp { - bool subsumes(const Clause& general, const Clause& specific) { - if (general.size() > specific.size()) { - return false; - } - for (const auto& lit_g : general.literals) { - bool found = false; - for (const auto& lit_s : specific.literals) { - if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) { - found = true; - break; - } - } - if (!found) { - return false; +bool subsumes(const Clause& general, const Clause& specific) { + if (general.size() > specific.size()) { + return false; + } + for (const auto& lit_g : general.literals) { + bool found = false; + for (const auto& lit_s : specific.literals) { + if (lit_g.atom == lit_s.atom && lit_g.is_positive == lit_s.is_positive) { + found = true; + break; } } - return true; + if (!found) { + return false; + } } + return true; } +} // namespace atp diff --git a/src/simplify/tautology.cc b/src/simplify/tautology.cc index d41ecd7..70bdced 100644 --- a/src/simplify/tautology.cc +++ b/src/simplify/tautology.cc @@ -17,18 +17,19 @@ */ #include "atp/simplify/tautology.h" + #include - namespace atp { - bool isTautology(const Clause& clause) { - for (size_t i = 0; i < clause.size(); ++i) { - for (size_t j = i + 1; j < clause.size(); ++j) { - if (clause.literals[i].atom == clause.literals[j].atom && - clause.literals[i].is_positive != clause.literals[j].is_positive) { - return true; - } +namespace atp { +bool isTautology(const Clause& clause) { + for (size_t i = 0; i < clause.size(); ++i) { + for (size_t j = i + 1; j < clause.size(); ++j) { + if (clause.literals[i].atom == clause.literals[j].atom && + clause.literals[i].is_positive != clause.literals[j].is_positive) { + return true; } } - return false; } -} \ No newline at end of file + return false; +} +} // namespace atp \ No newline at end of file diff --git a/src/strategy/problem_analyzer.cc b/src/strategy/problem_analyzer.cc index b62ffd0..17c63f8 100644 --- a/src/strategy/problem_analyzer.cc +++ b/src/strategy/problem_analyzer.cc @@ -15,5 +15,3 @@ * You should have received a copy of the GNU General Public License * along with this program. If not, see . */ - - -- cgit v1.2.3