kconfig2sat: Preliminary support for generating pairs of "single-diff" configurations

i.e. configurations which differ in just one option.

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index f014419f182f0f9e64a42413ade9f41e354ff096..aa68bd5a7fea3a646754752defbc159777ecfc14 100644 (file)
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -835,7 +835,52 @@ public:
                }
                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)
@@ -953,6 +998,8 @@ 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;
 }