diff options
Diffstat (limited to 'src/search/prover.cc')
| -rw-r--r-- | src/search/prover.cc | 22 |
1 files changed, 7 insertions, 15 deletions
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<Clause> 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<uint16_t>(std::max(d1, d2) + 1); // 7d. Store the clause (needed for forward subsumption check) |