From 5ab3efd522cf0221481684b5bbc9c2ac6bfc9919 Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Tue, 7 Apr 2026 03:59:58 +0800
Subject: refactor: rename struct members to follow trailing underscore naming
 convention across core, search, and frontend components

---
 src/simplify/subsumption.cc | 8 +++++---
 src/simplify/tautology.cc   | 6 ++++--
 2 files changed, 9 insertions(+), 5 deletions(-)

(limited to 'src/simplify')

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;
             }
         }
-- 
cgit v1.2.3