aboutsummaryrefslogtreecommitdiff
path: root/proofsearch/src/simplify/subsumption.cc
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/subsumption.cc
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/subsumption.cc')
-rw-r--r--proofsearch/src/simplify/subsumption.cc8
1 files changed, 5 insertions, 3 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;
}