kconfig2sat: Fix single-diff problem generation

We must generate equivalence clauses only for symbol literals. Expression
literals may have different value depending on the "single" variable
symbol.

Therefore, we learn SatLiterals to count the number of symbols so that we
can easily construct the p-line in DIMACS file.

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 {