kconfig2sat write PicoSAT output to Linux config

This commit adds support for "--config" option in kconfig2sat program.
Using this option generates Linux configuration. For now only with
standard configuration, no single configurations generated.

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index 222273439eee3353b1132956c75a1d6a4d195678..1fec086097f0154b546190a8563098f415df6a0d 100644 (file)
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -915,19 +915,44 @@ public:
                        picosat_add(sat, 0);
                }
                sat2config(sat, dumpconfig);
+               if (config)
+                       conf_write(config);
        }
 private:
        int sat2config(PicoSAT *sat, int dumpconfig) {
-               if (picosat_sat(sat, -1) == PICOSAT_UNSATISFIABLE) {
+               if (picosat_sat(sat, -1) != PICOSAT_SATISFIABLE) {
                        fprintf(stderr, "No solution found.\n");
                        return 1;
                }
+               int deref;
                for (auto l: literals) {
                        if (!l.sym)
                                continue;
-                       int deref = picosat_deref(sat, l.sym->lcp.id);
+                       l.sym->flags |= SYMBOL_CHANGED;
+                       l.sym->flags &= ~SYMBOL_VALID;
+                       deref = picosat_deref(sat, l.sym->lcp.id);
                        if (dumpconfig)
                                printf("%s=%s\n", l.sym->name, deref == 1 ? "y" : "n");
+                       if (deref == -1) {
+                               l.sym->def[S_DEF_USER].tri = no;
+                       } else if (deref == 1) {
+                               l.sym->def[S_DEF_USER].tri = yes;
+                       } else{
+                               fprintf(stderr, "Unknown return value from picosat, line: %d\n", __LINE__);
+                       }
+               }
+               struct symbol *sym;
+               int i;
+               for_all_symbols(i, sym) {
+                       sym_calc_value(sym);
+               }
+               for (auto l: literals) {
+                       if (!l.sym)
+                               continue;
+                       deref = picosat_deref(sat, l.sym->lcp.id);
+                       if ((deref == -1 && sym_get_tristate_value(l.sym) != no) ||
+                                       (deref == 1 && sym_get_tristate_value(l.sym) != yes))
+                               printf("%s: missmatch\n", l.sym->name);
                }
                return 0;
        }
@@ -1057,7 +1082,7 @@ int main(int argc, char **argv)
                sat_data.write_dimacs_cnf(cnf);
        if (cnf)
                sat_data.write_dimacs_cnf_all_single(cnf);
-       if (config)
+       if (config || dumpconfig)
                sat_data.write_config(dumpconfig, config);
 
        return EXIT_SUCCESS;