}
fclose(f);
}
+ void write_dimacs_cnf_single(const char *cnf, const char *sym_name) {
+ FILE *f = fopen((string(cnf)+"-single-"+sym_name).c_str(), "w");
+ if (!f) {
+ perror(cnf);
+ exit(EXIT_FAILURE);
+ }
+
+ fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.count());
+
+ for (auto l: literals) {
+ if (l.sym)
+ fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+ if (l.expr)
+ fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
+ }
+ for (auto clause: clauses) {
+ for (sat_id id: clause) {
+ assert(id != 0);
+ fprintf(f, "%d ", id);
+ }
+ fprintf(f, "0\n");
+
+ for (sat_id id: clause) {
+ fprintf(f, "%d ", id > 0 ? id + literals.count() : id - literals.count());
+ }
+ fprintf(f, "0\n");
+ }
+ fprintf(f, "c Equivalence\n");
+ for (auto l: literals) {
+ if (l.sym && strcmp(sym_name, l.sym->name) != 0) {
+ fprintf(f, "%d %d 0\n", -l.id(), l.id() + literals.count());
+ fprintf(f, "%d %d 0\n", -l.id() - literals.count(), l.id());
+ } else {
+ fprintf(f, "%d 0\n", +l.id());
+ fprintf(f, "%d 0\n", -l.id() - literals.count());
+ }
+ }
+ fclose(f);
+ }
+
+ void write_dimacs_cnf_all_single(const char *cnf) {
+ for (auto l: literals)
+ if (l.sym)
+ write_dimacs_cnf_single(cnf, l.sym->name);
+ }
};
int main(int argc, char **argv)
if (cnf)
sat_data.write_dimacs_cnf(cnf);
+ if (cnf)
+ sat_data.write_dimacs_cnf_all_single(cnf);
return EXIT_SUCCESS;
}