diff --git a/lib/kcnf.cpp b/lib/kcnf.cpp index 66346e4..3a200c8 100644 --- a/lib/kcnf.cpp +++ b/lib/kcnf.cpp @@ -115,8 +115,8 @@ KCNF KCNF::generate_random(long n, long c, long k) { long long estimated_bytes = c * (sizeof(Clause) + k * sizeof(int)); - if (estimated_bytes > 500 * 1024 * 1024) { // 500MB - throw std::runtime_error("Estimated memory too large"); + if (estimated_bytes > 500 * 1024 * 1024) { // 500MB, you may change this line for yourself if you are happy using more memory. + throw std::runtime_error("Estimated memory too large."); } auto indices = sample_indices(total, c); @@ -148,3 +148,65 @@ bool KCNF::write_dimacs(const std::string& filename) const { return true; } + +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; + + 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"; + } + + 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."); + } + } + } else { + f.k = 0; + } + + return f; +} diff --git a/lib/kcnf.hpp b/lib/kcnf.hpp index c256125..915caaf 100644 --- a/lib/kcnf.hpp +++ b/lib/kcnf.hpp @@ -14,4 +14,5 @@ public: static KCNF generate_random(long n, long c, long k); bool write_dimacs(const std::string& filename) const; + static KCNF read_dimacs(const std::string& filename); };