From 6e974168ecc487d99cbe51df569d52304907900c Mon Sep 17 00:00:00 2001
From: Richard Qin <richard.qin.x@gmail.com>
Date: Sat, 4 Apr 2026 03:02:48 +0800
Subject: feat: implement clause subsumption and tautology detection logic with
 associated unit tests

---
 src/simplify/subsumption.cc | 23 +++++++++++++++++++++++
 1 file changed, 23 insertions(+)

(limited to 'src/simplify/subsumption.cc')

diff --git a/src/simplify/subsumption.cc b/src/simplify/subsumption.cc
index b62ffd0..cf243c9 100644
--- a/src/simplify/subsumption.cc
+++ b/src/simplify/subsumption.cc
@@ -16,4 +16,27 @@
  * along with this program.  If not, see <https://www.gnu.org/licenses/>.
  */
 
+#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;
+            }
+        }
+        return true;
+    }
+}
-- 
cgit v1.2.3