kconfig2sat: Prepare for DIMACS CNF generation

diff --git a/kconfig2sat/Makefile b/kconfig2sat/Makefile
index 5eb687102d66f631d19e3c47572ee489256bf0bd..218dba67b452076e61d497f94cd12be04d2fb864 100644 (file)
--- a/kconfig2sat/Makefile
+++ b/kconfig2sat/Makefile
@@ -17,11 +17,11 @@ OBJ_CC = $(patsubst %.cc,%.o,$(filter %.cc,$(SRC)))
 kconfig2sat: $(OBJ_CC) $(OBJ_C)
        g++ $(CXXFLAGS) $(CFLAGS) -o $@ $^
 
-%.o: %.c
-       gcc -c $(CFLAGS) -o $@ $^
+%.o: %.c *.h kconfig/*.h
+       gcc -c $(CFLAGS) -o $@ $<
 
-%.o: %.cc
-       g++ -c $(CXXFLAGS) $(CFLAGS) -o $@ $^
+%.o: %.cc *.h kconfig/*.h
+       g++ -c $(CXXFLAGS) $(CFLAGS) -o $@ $<
 
 %.hash.c: %.gperf
        gperf -t --output-file $@ -a -C -E -g -k '1,3,$$' -p -t $<

diff --git a/kconfig2sat/kconfig/expr.h b/kconfig2sat/kconfig/expr.h
index 973b6f73336829a6290a0d2bb15a841086d9a18c..a8f8361f1b2e846d7d5b5bf8b2a8527dfc35abd6 100644 (file)
--- a/kconfig2sat/kconfig/expr.h
+++ b/kconfig2sat/kconfig/expr.h
@@ -16,6 +16,7 @@ extern "C" {
 #ifndef __cplusplus
 #include <stdbool.h>
 #endif
+#include "../lcp_data.h"
 
 struct file {
        struct file *next;
@@ -42,6 +43,8 @@ union expr_data {
 struct expr {
        enum expr_type type;
        union expr_data left, right;
+
+       struct lcp_expr *lcp;
 };
 
 #define EXPR_OR(dep1, dep2)    (((dep1)>(dep2))?(dep1):(dep2))
@@ -85,6 +88,8 @@ struct symbol {
        struct property *prop;
        struct expr_value dir_dep;
        struct expr_value rev_dep;
+
+       struct lcp_symbol *lcp;
 };
 
 #define for_all_symbols(i, sym) for (i = 0; i < SYMBOL_HASHSIZE; i++) for (sym = symbol_hash[i]; sym; sym = sym->next) if (sym->type != S_OTHER)

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;
 }
 

diff --git a/kconfig2sat/lcp_data.h b/kconfig2sat/lcp_data.h
new file mode 100644 (file)
index 0000000..251112a
--- /dev/null
+++ b/kconfig2sat/lcp_data.h
@@ -0,0 +1,19 @@
+#ifndef LCP_DATA_H
+#define LCP_DATA_H
+
+#include "kconfig/expr.h"
+
+/* linux-conf-perf data structures extensions */
+
+struct lcp_symbol {
+       int sat_id;
+       int variable:1;
+};
+
+struct lcp_expr {
+       int sat_id;
+};
+
+
+
+#endif