kconfig2sat: Prepare for DIMACS CNF generation

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

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index ed214eff819a0428ab13f6ba294cb17b55e0e8c8..c47daac95f9473a9f7147bcc9cd977b56181cec9 100644 (file)
--- a/kconfig2sat/kconfig2sat.cc
+++ b/kconfig2sat/kconfig2sat.cc
@@ -10,6 +10,10 @@
 #include "kconfig/lkc.h"
 #include "lcp_utils.h"
 
+#include <vector>
+
+using namespace std;
+
 int verbosity = 0;
 
 enum options {
@@ -134,9 +138,85 @@ void read_varfile(const char *varfile)
                if (!prompt) {
                        fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
                }
+               sym->lcp->variable = 1;
        }
+       fclose(f);
 }
 
+void write_dimacs_cnf(const char *cnf)
+{
+       FILE *f = fopen(cnf, "w");
+
+       if (!f) {
+               perror(cnf);
+               exit(EXIT_FAILURE);
+       }
+
+       fclose(f);
+}
+
+struct SatLiteral {
+       struct symbol *sym;
+       struct expr *expr;
+
+       SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
+       SatLiteral(struct expr *e)   : sym(nullptr), expr(e) {}
+};
+
+struct SatClause {
+       // TODO
+};
+
+class SatLiterals : public vector<struct SatLiteral>
+{
+public:
+       int fixed = {0};
+       SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
+       int count() const { return size() - 1; }
+};
+
+class SatData {
+       SatLiterals literals = {};
+       vector<SatClause> clauses = {};
+public:
+
+       SatData() {
+               int i;
+               struct symbol *sym;
+
+               for_all_symbols(i, sym) {
+                       if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
+                               literals.push_back(SatLiteral(sym));
+                               sym->lcp = new lcp_symbol;
+                               memset(sym->lcp, 0, sizeof(*sym->lcp));
+                               sym->lcp->sat_id = literals.count();
+                       }
+               }
+       }
+
+       void write_dimacs_cnf(const char *cnf) {
+               int i;
+               FILE *f = fopen(cnf, "w");
+
+               if (!f) {
+                       perror(cnf);
+                       exit(EXIT_FAILURE);
+               }
+
+               fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
+
+               for (i = 1; i <= literals.count(); i++) {
+                       SatLiteral &l = literals[i];
+                       if (l.sym)
+                               fprintf(f, "c SYM %d %s\n", l.sym->lcp->sat_id, l.sym->name);
+                       if (l.sym && l.sym->flags & SYMBOL_VALID && !l.sym->lcp->variable)
+                               fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp->sat_id : -l.sym->lcp->sat_id);
+               }
+               fclose(f);
+       }
+};
+
+
 int main(int argc, char **argv)
 {
        int c;
@@ -220,6 +300,7 @@ int main(int argc, char **argv)
        textdomain(PACKAGE);
 
        conf_parse_path(kconfig);
+       SatData sat_data;
 
        if (baseconf)
                conf_read(baseconf);
@@ -230,20 +311,11 @@ int main(int argc, char **argv)
        if (dump)
                do_dump();
 
-//     char *rules_file, *symbol_map_file, *variable_count_file;
-//     asprintf(&rules_file, "%s/%s", folder, DEFAULT_RULES_FILE);
-//     asprintf(&symbol_map_file, "%s/%s", folder, DEFAULT_SYMBOL_MAP_FILE);
-//     asprintf(&variable_count_file, "%s/%s", folder,
-//              DEFAULT_VARIABLE_COUNT_FILE);
-//     output_init(rules_file, symbol_map_file);
 
-//     build_symlist();
-//     cpy_dep();
-
-//     output_write_variable_count(variable_count_file,
-//                                 gsymlist->lastsym - 1, gsymlist->pos);
+       if (cnf) {
+               sat_data.write_dimacs_cnf(cnf);
+       }
 
-//     output_finish();
        return EXIT_SUCCESS;
 }