kconfig2sat: Fix single-diff problem generation

[linux-conf-perf.git] / kconfig2sat / kconfig2sat.cc

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index aa68bd5a7fea3a646754752defbc159777ecfc14..5108642e44cd209b5b7a18fbd1ef81b8d7d643d6 100644 (file)
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -296,12 +296,25 @@ struct SatExpr {
 
 class SatLiterals : protected vector<struct SatLiteral>
 {
+       unsigned _symbols = 0;
 public:
        using vector<struct SatLiteral>::begin;
        using vector<struct SatLiteral>::end;
-       using vector<struct SatLiteral>::push_back;
+
        SatLiterals() { reserve(20000); }
+       SatLiteral &add(struct symbol *sym) {
+               sym->lcp.id = count() + 1;
+               push_back(SatLiteral(sym));
+               _symbols++;
+               return last();
+       }
+       SatLiteral &add(struct expr *e) {
+               e->lcp.id = count() + 1;
+               push_back(SatLiteral(e));
+               return last();
+       }
        int count() const { return size(); }
+       int symbols() const { return _symbols; }
        const SatLiteral &operator[](size_type i) const { return at(i-1); }
        SatLiteral &last() { return *(--end()); }
        bool test_set_dot_printed(struct symbol *sym) const {
@@ -585,19 +598,17 @@ public:
        }
 
        const SatLiteral &add_literal(struct symbol *sym) {
-               sym->lcp.id = literals.count() + 1;
-               literals.push_back(SatLiteral(sym));
+               SatLiteral &l = literals.add(sym);
                if (dot)
-                       dot->literal(literals.last());
-               return literals.last();
+                       dot->literal(l);
+               return l;
        }
 
        const SatLiteral &add_literal(struct expr *e) {
-               e->lcp.id = literals.count() + 1;
-               literals.push_back(SatLiteral(e));
+               SatLiteral &l = literals.add(e);
                if (dot)
-                       dot->literal(literals.last());
-               return literals.last();
+                       dot->literal(l);
+               return l;
        }
 
        void symbols2literals() {
@@ -822,9 +833,9 @@ public:
 
                for (auto l: literals) {
                        if (l.sym)
-                               fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+                               fprintf(f, "c SYM %d %s\n", l.id(), l.sym->name);
                        if (l.expr)
-                               fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
+                               fprintf(f, "c EXPR %d %s\n", l.id(), expr_to_string(l.expr).get());
                }
                for (auto clause: clauses) {
                        for (sat_id id: clause) {
@@ -843,13 +854,16 @@ public:
                        exit(EXIT_FAILURE);
                }
 
-               fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.count());
+               fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.symbols());
 
                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());
+                               fprintf(f, "c SYM %d,%d %s\n", l.id(), l.id() + literals.count(), l.sym->name);
+                       if (l.expr) {
+                               struct gstr gs = str_new();
+                               expr_gstr_print(l.expr, &gs);
+                               fprintf(f, "c EXPR %d,%d %s\n", l.id(), l.id() + literals.count(), str_get(&gs));
+                       }
                }
                for (auto clause: clauses) {
                        for (sat_id id: clause) {
@@ -865,7 +879,9 @@ public:
                }
                fprintf(f, "c Equivalence\n");
                for (auto l: literals) {
-                       if (l.sym && strcmp(sym_name, l.sym->name) != 0) {
+                       if (!l.sym)
+                               continue;
+                       if (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 {