aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/src/simplify
diff options
context:
space:
mode:
authorRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
committerRichard Qin <richard.qin.x@gmail.com>2026-04-07 03:59:58 +0800
commit598f364de0a809747714294326a0193788e0bdfb (patch)
tree1ab77a340ab0930b41ffc6291d06b12d1b302a88 /proofsearch/src/simplify
parent593a94a3c13aff82b31fd6c61e0ae07b97a2e426 (diff)
downloadrcc-project-598f364de0a809747714294326a0193788e0bdfb.tar.gz
rcc-project-598f364de0a809747714294326a0193788e0bdfb.tar.xz
refactor: rename struct members to follow trailing underscore naming convention across core, search, and frontend components
Diffstat (limited to 'proofsearch/src/simplify')
-rw-r--r--proofsearch/src/simplify/subsumption.cc8
-rw-r--r--proofsearch/src/simplify/tautology.cc6
2 files changed, 9 insertions, 5 deletions
diff --git a/proofsearch/src/simplify/subsumption.cc b/proofsearch/src/simplify/subsumption.cc
index 3756d82..0038ad1 100644
--- a/proofsearch/src/simplify/subsumption.cc
+++ b/proofsearch/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/proofsearch/src/simplify/tautology.cc b/proofsearch/src/simplify/tautology.cc
index 70bdced..e35d874 100644
--- a/proofsearch/src/simplify/tautology.cc
+++ b/proofsearch/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;
}
}