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

---
 include/atp/simplify/subsumption.h | 2 ++
 1 file changed, 2 insertions(+)

(limited to 'include')

diff --git a/include/atp/simplify/subsumption.h b/include/atp/simplify/subsumption.h
index ee7a83e..c39b586 100644
--- a/include/atp/simplify/subsumption.h
+++ b/include/atp/simplify/subsumption.h
@@ -52,4 +52,6 @@ class SubsumptionEngine {
     // TODO: Phase 5 implementation
 };
 
+bool subsumes(const Clause& general, const Clause& specific);
+
 }  // namespace atp
-- 
cgit v1.2.3