You cannot select more than 25 topics
Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
85 lines
1.8 KiB
C++
85 lines
1.8 KiB
C++
#include "cnf.hpp"
|
|
|
|
#include <filesystem>
|
|
#include <fstream>
|
|
#include <iostream>
|
|
#include <sstream>
|
|
#include <stdexcept>
|
|
|
|
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;
|
|
}
|