From 14677675254bcb0159e1bc5358a41b6fe0f0e574 Mon Sep 17 00:00:00 2001
From: Isabell Pflug <isabell.pflug@floating-in.space>
Date: Wed, 6 May 2026 20:38:21 +0200
Subject: [PATCH] :recycle: Inherit DIMACS writing and reading code too.

---
 lib/kcnf.cpp | 70 ++++++----------------------------------------------
 1 file changed, 8 insertions(+), 62 deletions(-)

diff --git a/lib/kcnf.cpp b/lib/kcnf.cpp
index 3a200c8..b28ac17 100644
--- a/lib/kcnf.cpp
+++ b/lib/kcnf.cpp
@@ -126,79 +126,25 @@ KCNF KCNF::generate_random(long n, long c, long k) {
 }
 
 bool KCNF::write_dimacs(const std::string& filename) const {
-    fs::create_directories(CNF_DIR);
-
-    fs::path path = CNF_DIR / filename;
-    path = path.lexically_normal();
-
-    std::ofstream out(path);
-    if (!out) {
-        std::cerr << "Error: Could not open file " << path << "\n";
-        return false;
-    }
-
-    out << "p cnf " << n << " " << clauses.size() << "\n";
-
     for (const auto& cl : clauses) {
-        for (int lit : cl) {
-            out << lit << " ";
+        if ((long)cl.size() != k) {
+            throw std::runtime_error("Not a k-CNF formula.");
         }
-        out << "0\n";
     }
 
-    return true;
+    return CNF::write_dimacs(filename);
 }
 
 KCNF KCNF::read_dimacs(const std::string& filename) {
-    KCNF f;
-
-    std::ifstream in(filename);
-    if (!in) {
-        throw std::runtime_error("Could not open DIMACS file.");
-    }
-
-    std::string line;
-    long expected_clauses = 0;
-
-    while (std::getline(in, line)) {
-        if (line.empty()) continue;
-
-        if (line[0] == 'c') continue;
-
-        if (line[0] == 'p') {
-            std::istringstream iss(line);
-            std::string tmp, format;
-            iss >> tmp >> format >> f.n >> expected_clauses;
+    CNF base = CNF::read_dimacs(filename);
 
-            if (format != "cnf") {
-                throw std::runtime_error("Unsupported DIMACS format.");
-            }
-            continue;
-        }
-
-        std::istringstream iss(line);
-        Clause cl;
-        int lit;
-
-        while (iss >> lit) {
-            if (lit == 0) break;
-            cl.push_back(lit);
-        }
-
-        if (!cl.empty()) {
-            f.clauses.push_back(cl);
-        }
-    }
-
-    if (expected_clauses != 0 && 
-        f.clauses.size() != (size_t)expected_clauses) {
-        std::cerr << "Warning: Clause count mismatch.\n";
-    }
+    KCNF f;
+    f.n = base.n;
+    f.clauses = std::move(base.clauses);
 
     if (!f.clauses.empty()) {
         f.k = f.clauses[0].size();
-        
-        // check whether actually k-cnf
+
         for (const auto& cl : f.clauses) {
             if ((long)cl.size() != f.k) {
                 throw std::runtime_error("Input is not a k-CNF formula.");