feat: implement clause subsumption and tautology detection logic with associated unit tests

1 files changed, 23 insertions, 0 deletions

diff --git a/proofsearch/src/simplify/subsumption.cc b/proofsearch/src/simplify/subsumption.cc
index b62ffd0..cf243c9 100644
--- a/proofsearch/src/simplify/subsumption.cc
+++ b/proofsearch/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;
+    }
+}