diff --git a/lib/cnf.cpp b/lib/cnf.cpp new file mode 100644 index 0000000..6b5d9cf --- /dev/null +++ b/lib/cnf.cpp @@ -0,0 +1,84 @@ +#include "cnf.hpp" + +#include +#include +#include +#include +#include + +namespace fs = std::filesystem; + +const fs::path CNF_DIR = "./CNF"; + +bool CNF::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 << " "; + } + out << "0\n"; + } + + return true; +} + +CNF CNF::read_dimacs(const std::string& filename) { + CNF 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; + + 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"; + } + + return f; +} diff --git a/lib/cnf.hpp b/lib/cnf.hpp new file mode 100644 index 0000000..7c4649e --- /dev/null +++ b/lib/cnf.hpp @@ -0,0 +1,17 @@ +#pragma once + +#include +#include + +using Clause = std::vector; + +class CNF { +public: + long n = 0; + std::vector clauses; + + virtual ~CNF() = default; + + virtual bool write_dimacs(const std::string& filename) const; + static CNF read_dimacs(const std::string& filename); +}; diff --git a/lib/kcnf.hpp b/lib/kcnf.hpp index 915caaf..9a8f2c1 100644 --- a/lib/kcnf.hpp +++ b/lib/kcnf.hpp @@ -1,18 +1,13 @@ #pragma once -#include -#include +#include "cnf.hpp" -using Clause = std::vector; // makes it nicer to read - -class KCNF { +class KCNF : public CNF { public: - long n = 0; long k = 0; - std::vector clauses; static KCNF generate_random(long n, long c, long k); - bool write_dimacs(const std::string& filename) const; + bool write_dimacs(const std::string& filename) const override; static KCNF read_dimacs(const std::string& filename); };