parse_kconfig rewriten

parse_kconfig should now generate full dependency.
It is not transforming whole expression to CNF, but only pairs.

12 files changed, 532 insertions, 899 deletions

diff --git a/scripts/parse_kconfig/Makefile b/scripts/parse_kconfig/Makefile
index 98c8531..4b8a538 100644
--- a/scripts/parse_kconfig/Makefile
+++ b/scripts/parse_kconfig/Makefile
@@ -8,7 +8,8 @@ KCONFIG_PREFIX = ../shared/kconfig
 include $(KCONFIG_PREFIX)/files.mk
 
 SRC  = parse.c \
-	       cnfexpr.c \
+	       boolexpr.c \
+		   cnfbuild.c \
 	       symlist.c \
 	       output.c
 OBJ = $(patsubst %.c,%.o,$(SRC))
diff --git a/scripts/parse_kconfig/boolexpr.c b/scripts/parse_kconfig/boolexpr.c
new file mode 100644
index 0000000..d29d238
--- /dev/null
+++ b/scripts/parse_kconfig/boolexpr.c
@@ -0,0 +1,296 @@
+#include "boolexpr.h"
+
+struct boolexpr *boolexpr_eql(struct symlist *sl, struct symbol *sym1,
+                              struct symbol *sym2);
+
+struct boolexpr *boolexpr_kconfig(struct symlist *sl, struct expr *expr) {
+    struct stck {
+        struct expr *expr;
+        struct boolexpr *bl;
+    };
+    struct expr **back;
+    int back_size = 2, back_pos = -1;
+    back = malloc((unsigned) back_size * sizeof(struct expr *));
+    struct stck *stack;
+    unsigned stack_size = 2;
+    int stack_pos = -1;
+    stack = malloc((unsigned) stack_size * sizeof(struct stck));
+    struct boolexpr *rtn = NULL;
+
+    while (expr != NULL) {
+        if ((back_pos >= 0 && back[back_pos] != expr) || back_pos < 0) {
+            if (++back_pos >= back_size) {
+                back_size *= 2;
+                back =
+                    realloc(back,
+                            (unsigned) back_size * sizeof(struct expr *));
+            }
+            back[back_pos] = expr;
+        }
+        switch (expr->type) {
+        case E_SYMBOL:
+            rtn = boolexpr_sym(sl, expr->left.sym);
+            goto go_up;
+        case E_NOT:
+            if (rtn == NULL)
+                expr = expr->left.expr;
+            else {
+                rtn = boolexpr_not(rtn);
+                goto go_up;
+            }
+            break;
+        case E_OR:
+        case E_AND:
+            if (stack_pos < 0 || stack[stack_pos].expr != expr) {
+                if (rtn == NULL)
+                    expr = expr->left.expr;
+                else {
+                    if (++stack_pos >= stack_size) {
+                        stack_size *= 2;
+                        stack =
+                            realloc(stack,
+                                    stack_size * sizeof(struct stck));
+                    }
+                    stack[stack_pos].expr = expr;
+                    stack[stack_pos].bl = rtn;
+                    expr = expr->right.expr;
+                    rtn = NULL;
+                }
+            } else {
+                if (expr->type == E_OR)
+                    rtn = boolexpr_or(stack[stack_pos].bl, rtn);
+                else
+                    rtn = boolexpr_and(stack[stack_pos].bl, rtn);
+                stack_pos--;
+                goto go_up;
+            }
+            break;
+        case E_EQUAL:
+            rtn = boolexpr_eql(sl, expr->left.sym, expr->right.sym);
+            goto go_up;
+        case E_UNEQUAL:
+            rtn =
+                boolexpr_not(boolexpr_eql
+                             (sl, expr->left.sym, expr->right.sym));
+            goto go_up;
+        default:
+            fprintf(stderr, "ERROR: Unknown expression type.\n");
+        }
+        continue;
+
+      go_up:
+        if (--back_pos >= 0)
+            expr = back[back_pos];
+        else
+            expr = NULL;
+    }
+
+    free(back);
+    free(stack);
+
+    return rtn;
+}
+
+struct boolexpr *boolexpr_true() {
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->type = BT_TRUE;
+    rtn->overusage = 0;
+    rtn->id = 0;
+    return rtn;
+}
+
+struct boolexpr *boolexpr_false() {
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->type = BT_FALSE;
+    rtn->overusage = 0;
+    rtn->id = 0;
+    return rtn;
+}
+
+struct boolexpr *boolexpr_sym(struct symlist *sl, struct symbol *sym) {
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->overusage = 0;
+    rtn->id = symlist_id(sl, sym->name);
+    if (rtn->id != 0)
+        rtn->type = BT_SYM;
+    else
+        rtn->type = BT_FALSE;
+    return rtn;
+}
+
+struct boolexpr *boolexpr_eql(struct symlist *sl, struct symbol *sym1,
+                              struct symbol *sym2) {
+    if (!strcmp(sym2->name, "m")) {
+        struct boolexpr *rtn = malloc(sizeof(struct boolexpr));
+        rtn->overusage = 0;
+        rtn->id = 0;
+        rtn->type = BT_FALSE;
+        return rtn;
+    }
+    if (!strcmp(sym2->name, "n"))
+        return boolexpr_not(boolexpr_sym(sl, sym1));
+    if (!strcmp(sym2->name, "y"))
+        return boolexpr_sym(sl, sym1);
+
+    // sym1 <-> sym2
+    // (!sym1 || sym2) && (sym1 || !sym2)
+    return
+        boolexpr_and(boolexpr_or
+                     (boolexpr_not(boolexpr_sym(sl, sym1)),
+                      boolexpr_sym(sl, sym2)), boolexpr_or(boolexpr_sym(sl,
+                                                                        sym1),
+                                                           boolexpr_not
+                                                           (boolexpr_sym
+                                                            (sl, sym2))));
+}
+
+struct boolexpr *boolexpr_or(struct boolexpr *e1, struct boolexpr *e2) {
+    switch (e1->type) {
+    case BT_TRUE:
+        boolexpr_free(e2);
+        return e1;
+    case BT_FALSE:
+        boolexpr_free(e1);
+        return e2;
+    default:
+        switch (e2->type) {
+        case BT_TRUE:
+            boolexpr_free(e1);
+            return e2;
+        case BT_FALSE:
+            boolexpr_free(e2);
+            return e1;
+        default:
+            break;
+        }
+        break;
+    }
+
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->type = BT_OR;
+    rtn->overusage = 0;
+    rtn->id = 0;
+    rtn->left = e1;
+    rtn->right = e2;
+    return rtn;
+}
+
+struct boolexpr *boolexpr_and(struct boolexpr *e1, struct boolexpr *e2) {
+    switch (e1->type) {
+    case BT_FALSE:
+        boolexpr_free(e2);
+        return e1;
+    case BT_TRUE:
+        boolexpr_free(e1);
+        return e2;
+    default:
+        switch (e2->type) {
+        case BT_FALSE:
+            boolexpr_free(e1);
+            return e2;
+        case BT_TRUE:
+            boolexpr_free(e2);
+            return e1;
+        default:
+            break;
+        }
+        break;
+    }
+
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->type = BT_AND;
+    rtn->overusage = 0;
+    rtn->id = 0;
+    rtn->left = e1;
+    rtn->right = e2;
+    return rtn;
+}
+
+struct boolexpr *boolexpr_not(struct boolexpr *e) {
+    switch (e->type) {
+    case BT_FALSE:
+        e->type = BT_TRUE;
+        return e;
+    case BT_TRUE:
+        e->type = BT_FALSE;
+        return e;
+    default:
+        break;
+    }
+    struct boolexpr *rtn;
+    rtn = malloc(sizeof(struct boolexpr));
+    rtn->type = BT_NOT;
+    rtn->overusage = 0;
+    rtn->id = 0;
+    rtn->left = e;
+    return rtn;
+}
+
+void boolexpr_free(struct boolexpr *e) {
+    struct boolexpr **stack;
+    size_t stack_size = 2, stack_pos = 0;
+    stack = malloc(stack_size * sizeof(struct boolexpr *));
+
+    struct boolexpr *m;
+    while (e != NULL) {
+        m = e;
+        switch (e->type) {
+        case BT_OR:
+        case BT_AND:
+            if (++stack_pos >= stack_size) {
+                stack_size *= 2;
+                stack =
+                    realloc(stack, stack_size * sizeof(struct boolexpr *));
+            }
+            stack[stack_pos - 1] = e->right;
+        case BT_NOT:
+            e = e->left;
+            break;
+        default:
+            if (stack_pos > 0)
+                e = stack[--stack_pos];
+            else
+                e = NULL;
+        }
+        if (m->overusage > 0)
+            m->overusage--;
+        else
+            free(m);
+    }
+    free(stack);
+}
+
+struct boolexpr *boolexpr_copy(struct boolexpr *e) {
+    struct boolexpr **stack;
+    size_t stack_size = 2, stack_pos = 0;
+    stack = malloc(stack_size * sizeof(struct boolexpr *));
+
+    while (e != NULL) {
+        e->overusage++;
+        switch (e->type) {
+        case BT_OR:
+        case BT_AND:
+            if (++stack_pos >= stack_size) {
+                stack_size *= 2;
+                stack =
+                    realloc(stack, stack_size * sizeof(struct boolexpr *));
+            }
+            stack[stack_pos - 1] = e->right;
+        case BT_NOT:
+            e = e->left;
+            break;
+        default:
+            if (stack_pos > 0)
+                e = stack[--stack_pos];
+            else
+                e = NULL;
+        }
+    }
+    free(stack);
+    return e;
+}
diff --git a/scripts/parse_kconfig/boolexpr.h b/scripts/parse_kconfig/boolexpr.h
new file mode 100644
index 0000000..52cd4a6
--- /dev/null
+++ b/scripts/parse_kconfig/boolexpr.h
@@ -0,0 +1,34 @@
+#include <stdlib.h>
+#include <stdbool.h>
+
+#include <kconfig/lkc.h>
+
+#ifndef _BOOLEXPR_H_
+#define _BOOLEXPR_H_
+
+#include "symlist.h"
+
+enum boolexpr_type {
+    BT_SYM, BT_TRUE, BT_FALSE, BT_OR, BT_AND, BT_NOT
+};
+
+struct boolexpr {
+    enum boolexpr_type type;
+    unsigned id;
+    struct boolexpr *left, *right;
+
+    unsigned overusage;
+};
+
+struct boolexpr *boolexpr_kconfig(struct symlist *sl, struct expr *expr);
+
+struct boolexpr *boolexpr_true();
+struct boolexpr *boolexpr_false();
+struct boolexpr *boolexpr_sym(struct symlist *sl, struct symbol *sym);
+struct boolexpr *boolexpr_or(struct boolexpr *e1, struct boolexpr *e2);
+struct boolexpr *boolexpr_and(struct boolexpr *e1, struct boolexpr *e2);
+struct boolexpr *boolexpr_not(struct boolexpr *e);
+struct boolexpr *boolexpr_copy(struct boolexpr *e);
+void boolexpr_free(struct boolexpr *e);
+
+#endif /* _BOOLEXPR_H_ */
diff --git a/scripts/parse_kconfig/cnfbuild.c b/scripts/parse_kconfig/cnfbuild.c
index f9dd15f..398a934 100644
--- a/scripts/parse_kconfig/cnfbuild.c
+++ b/scripts/parse_kconfig/cnfbuild.c
@@ -1,272 +1,143 @@
 #include "cnfbuild.h"
 
-struct cnfexpr *kconfig_expr(struct symlist *sl, struct expr *expr) {
-    struct stck {
-        struct expr *expr;
-        struct cnfexpr *cnf;
-    };
-    struct expr **back;
-    int back_size = 2, back_pos = -1;
-    back = malloc((unsigned) back_size * sizeof(struct expr *));
-    struct stck *stack;
-    int stack_size = 2, stack_pos = -1;
-    stack = malloc((unsigned) stack_size * sizeof(struct stck));
-    struct cnfexpr *rtn = NULL;
+struct stck {
+    struct boolexpr **stack;
+    size_t size, pos;
+};
+
+struct stck *stack_create();
+void stack_push(struct stck *s, struct boolexpr *b);
+struct boolexpr *stack_pop(struct stck *s);
+
+void cnf_and(struct symlist *sl, struct boolexpr *bl);
+void cnf_or(struct symlist *sl, struct boolexpr *bl);
+void cnf_not(struct symlist *sl, struct boolexpr *bl);
+
+void cnf_boolexpr(struct symlist *sl, struct boolexpr *bl) {
+    if (bl->type == BT_TRUE) {
+        // Term is always true. No write required.
+        return;
+    } else if (bl->type == BT_FALSE) {
+        fprintf(stderr,
+                "E: Trying to write false term. This shouldn't happen.\n");
+        exit(6);
+    }
 
-    while (expr != NULL) {
-        if ((back_pos >= 0 && back[back_pos] != expr) || back_pos < 0) {
-            if (++back_pos >= back_size) {
-                back_size *= 2;
-                back =
-                    realloc(back,
-                            (unsigned) back_size * sizeof(struct expr *));
-            }
-            back[back_pos] = expr;
-        }
-        switch (expr->type) {
-        case E_SYMBOL:
-            rtn = cnf_sym(sl, expr->left.sym);
-            goto go_up;
-        case E_NOT:
-            if (rtn == NULL)
-                expr = expr->left.expr;
-            else {
-                rtn = cnf_not(sl, rtn);
-                goto go_up;
+    struct stck *stack = stack_create();
+    while (bl != NULL) {
+        switch (bl->type) {
+        case BT_NOT:
+            if (bl->left->id != 0) {
+                cnf_not(sl, bl);
+                bl = stack_pop(stack);
+            } else {
+                stack_push(stack, bl);
+                bl = bl->left;
             }
             break;
-        case E_OR:
-        case E_AND:
-            if (stack_pos < 0 || stack[stack_pos].expr != expr) {
-                if (rtn == NULL)
-                    expr = expr->left.expr;
-                else {
-                    if (stack_size >= ++stack_pos) {
-                        stack_size *= 2;
-                        stack =
-                            realloc(stack,
-                                    (unsigned) stack_size *
-                                    sizeof(struct stck *));
+        case BT_AND:
+        case BT_OR:
+            if (bl->left->id != 0) {
+                if (bl->right->id != 0) {
+                    if (bl->type == BT_OR) {
+                        cnf_or(sl, bl);
+                        bl = stack_pop(stack);
+                    } else {    /* BT_AND */
+                        cnf_and(sl, bl);
+                        bl = stack_pop(stack);
                     }
-                    stack[stack_pos].expr = expr;
-                    stack[stack_pos].cnf = rtn;
-                    expr = expr->right.expr;
-                    rtn = NULL;
+                } else {
+                    stack_push(stack, bl);
+                    bl = bl->right;
                 }
             } else {
-                if (expr->type == E_OR)
-                    rtn = cnf_or(sl, stack[stack_pos].cnf, rtn);
-                else
-                    rtn = cnf_and(sl, stack[stack_pos].cnf, rtn);
-                stack_pos--;
-                goto go_up;
+                stack_push(stack, bl);
+                bl = bl->left;
             }
             break;
-        case E_EQUAL:
-            rtn = cnf_eql(sl, expr->left.sym, expr->right.sym);
-            goto go_up;
-        case E_UNEQUAL:
-            rtn =
-                cnf_not(sl, cnf_eql(sl, expr->left.sym, expr->right.sym));
-            goto go_up;
         default:
-            fprintf(stderr, "ERROR: Unknown expression type.\n");
+            bl = stack_pop(stack);
+            break;
         }
-        continue;
-
-      go_up:
-        if (--back_pos >= 0)
-            expr = back[back_pos];
-        else
-            expr = NULL;
     }
-
-    free(back);
-    free(stack);
-
-    return rtn;
 }
 
-struct cnfexpr *cnfexpr_true(struct symlist *sl) {
-    struct cnfexpr *rtn;
-    rtn = malloc(sizeof(struct cnfexpr));
-    rtn->type = CT_TRUE;
-    rtn->id = 0;
-    rtn->out = NULL;
+struct stck *stack_create() {
+    struct stck *rtn;
+    rtn = malloc(sizeof(struct stck));
+    rtn->size = 2;
+    rtn->pos = 0;
+    rtn->stack = malloc(rtn->size * sizeof(struct boolexpr *));
     return rtn;
 }
 
-struct cnfexpr *cnfexpr_false(struct symlist *sl) {
-    struct cnfexpr *rtn;
-    rtn = malloc(sizeof(struct cnfexpr));
-    rtn->type = CT_FALSE;
-    rtn->id = 0;
-    rtn->out = NULL;
-    return rtn;
-}
-
-struct cnfexpr *cnf_sym(struct symlist *sl, struct symbol *sym) {
-    struct cnfexpr *rtn;
-    rtn = malloc(sizeof(struct cnfexpr));
-    rtn->type = CT_EXPR;
-    rtn->id = symlist_id(sym->name);
-    rtn->out = NULL;
-    if (rtn->id == 0)
-        rtn->type = CT_FALSE;
-    return rtn;
-}
-
-struct cnfexpr *cnf_eql(struct symlist *sl, struct symbol *sym1,
-                        struct symbol *sym2) {
-    if (!strcmp(sym2->name, "m")) {
-        struct cnfexpr *fls = malloc(sizeof(struct cnfexpr));
-        fls->type = CT_FALSE;
-        return fls;
-    }
-    if (!strcmp(sym2->name, "n"))
-        return cnf_not(sl, cnf_sym(sl, sym1));
-    if (!strcmp(sym2->name, "y"))
-        return cnf_sym(sl, sym1);
-
-    // sym1 <-> sym2
-    // (!sym1 || sym2) && (sym1 || !sym2)
-    return cnf_and(sl,
-                   cnf_or(sl, cnf_not(sl, cnf_sym(sl, sym1)),
-                          cnf_sym(sl, sym2)), cnf_or(sl, cnf_sym(sl,
-                                                                 sym1),
-                                                     cnf_not(sl,
-                                                             cnf_sym
-                                                             (sl, sym2))));
-}
-
-struct cnfexpr *cnf_or(struct symlist *sl, struct cnfexpr *e1,
-                       struct cnfexpr *e2) {
-    switch (e1->type) {
-    case CT_TRUE:
-        cnfexpr_free(e2);
-        return e1;
-    case CT_FALSE:
-        cnfexpr_free(e1);
-        return e2;
-    case CT_EXPR:
-        switch (e2->type) {
-        case CT_TRUE:
-            cnfexpr_free(e1);
-            return e2;
-        case CT_FALSE:
-            cnfexpr_free(e2);
-            return e1;
-        case CT_EXPR:
-            break;
-        }
-        break;
+void stack_push(struct stck *s, struct boolexpr *b) {
+    if (++(s->pos) >= s->size) {
+        s->size *= 2;
+        s->stack = realloc(s->stack, s->size * sizeof(struct boolexpr *));
     }
-
-    unsigned newid = (unsigned) symlist_adddummy(sl);
-    e1->out = output_rules_joinexpr(e1->out, e2->out);
-    if (e1->out == NULL)
-        e1->out = output_rules_newexpr();
-
-    // rtn <-> (e1 || e2)
-    // (!rtn || e1 || e2) && (rtn || !e1) && (rtn || !e2)
-    output_rules_symbol(e1->out, -(int) newid);
-    output_rules_symbol(e1->out, (int) e1->id);
-    output_rules_symbol(e1->out, (int) e2->id);
-    output_rules_endterm(e1->out);
-    output_rules_symbol(e1->out, (int) rtn->id);
-    output_rules_symbol(e1->out, -(int) e1->id);
-    output_rules_endterm(e1->out);
-    output_rules_symbol(e1->out, (int) rtn->id);
-    output_rules_symbol(e1->out, -(int) e2->id);
-    output_rules_endterm(e1->out);
-
-    cnfexpr_free(e2);
-    e1->id = newid;
-    return e1;
+    s->stack[s->pos - 1] = b;
 }
 
-struct cnfexpr *cnf_and(struct symlist *sl, struct cnfexpr *e1,
-                        struct cnfexpr *e2) {
-    switch (e1->type) {
-    case CT_FALSE:
-        cnfexpr_free(e2);
-        return e1;
-    case CT_TRUE:
-        cnfexpr_free(e1);
-        return e2;
-    case CT_EXPR:
-        switch (e2->type) {
-        case CT_FALSE:
-            cnfexpr_free(e1);
-            return e2;
-        case CT_TRUE:
-            cnfexpr_free(e2);
-            return e1;
-        case CT_EXPR:
-            break;
-        }
-        break;
-    }
-
-    unsigned newid = (unsigned) symlist_adddummy(sl);
-    e1->out = output_rules_joinexpr(e1->out, e2->out);
-    if (e1->out == NULL)
-        e1->out = output_rules_newexpr();
-
-    // rtn <-> (e1 && e2)
-    // (rtn || !e1 || !e2) && (!rtn || e1) && (!rtn || e2)
-    output_rules_symbol(e1->out, (int) rtn->id);
-    output_rules_symbol(e1->out, -(int) e1->id);
-    output_rules_symbol(e1->out, -(int) e2->id);
-    output_rules_endterm(e1->out);
-    output_rules_symbol(e1->out, -(int) rtn->id);
-    output_rules_symbol(e1->out, (int) e1->id);
-    output_rules_endterm(e1->out);
-    output_rules_symbol(e1->out, -(int) rtn->id);
-    output_rules_symbol(e1->out, (int) e2->id);
-    output_rules_endterm(e1->out);
-
-    cnfexpr_free(e2);
-    e1->id = newid;
-    return e1;
+inline struct boolexpr *stack_pop(struct stck *s) {
+    if (s->pos > 0)
+        return s->stack[--(s->pos)];
+    else
+        return NULL;
 }
 
-struct cnfexpr *cnf_not(struct symlist *sl, struct cnfexpr *e) {
-    switch (e->type) {
-    case CT_FALSE:
-        e->type = CT_TRUE;
-        return e;
-    case CT_TRUE:
-        e->type = CT_FALSE;
-        return e;
-    case CT_EXPR:
-        break;
-    }
-    unsigned newid = (unsigned) symlist_adddummy(sl);
-
-    // rtn <-> !e
-    // (rtn || e) && (!rtn || !e)
-    output_rules_symbol(e->out, (int) newid);
-    output_rules_symbol(e->out, (int) e->id);
-    output_rules_endterm(e->out);
-    output_rules_symbol(e->out, -(int) newid);
-    output_rules_symbol(e->out, -(int) e->id);
-    output_rules_endterm(e->out);
-
-    e->id = newid;
-    return e;
+void cnf_and(struct symlist *sl, struct boolexpr *bl) {
+    if (bl->id != 0)
+        return;
+    bl->id = symlist_adddummy(sl);
+    // bl->id <-> (bl->left->id && bl->right->id)
+    //
+    // (bl->id || !bl->left->id || !bl->right->id) &&
+    // (!bl->id || bl->left->id) &&
+    // (!bl->id || bl->right->id)
+    output_rules_symbol((int) bl->id);
+    output_rules_symbol(-(int) bl->left->id);
+    output_rules_symbol(-(int) bl->right->id);
+    output_rules_endterm();
+    output_rules_symbol(-(int) bl->id);
+    output_rules_symbol((int) bl->left->id);
+    output_rules_endterm();
+    output_rules_symbol(-(int) bl->id);
+    output_rules_symbol((int) bl->right->id);
+    output_rules_endterm();
 }
 
-struct cnfexpr *cnfexpr_copy(struct cnfexpr *e) {
-    struct cnfexpr *rtn;
-    rtn = malloc(sizeof(struct cnfexpr));
-    rtn->type = e->type;
-    rtn->id = e->id;
-    rtn->out = output_rules_copycnf(e->out);
-    return rtn;
+void cnf_or(struct symlist *sl, struct boolexpr *bl) {
+    if (bl->id != 0)
+        return;
+    bl->id = symlist_adddummy(sl);
+    // bl->id <-> (bl->left->id || bl->right->id)
+    //
+    // (!bl->id || bl->left->id || bl->right->id) &&
+    // (bl->id || !bl->left->id) &&
+    // (bl->id || !bl->right->id)
+    output_rules_symbol(-(int) bl->id);
+    output_rules_symbol((int) bl->left->id);
+    output_rules_symbol((int) bl->right->id);
+    output_rules_endterm();
+    output_rules_symbol((int) bl->id);
+    output_rules_symbol(-(int) bl->left->id);
+    output_rules_endterm();
+    output_rules_symbol((int) bl->id);
+    output_rules_symbol(-(int) bl->right->id);
+    output_rules_endterm();
 }
 
-void cnfexpr_free(struct cnfexpr *e) {
-    output_rules_freexpr(e->out);
-    free(e);
+void cnf_not(struct symlist *sl, struct boolexpr *bl) {
+    if (bl->id != 0)
+        return;
+    bl->id = symlist_adddummy(sl);
+    // bl->id <-> !bl->left->id
+    // (bl->id || bl->left->id) && (!bl->id || !bl->left->id)
+    output_rules_symbol((int) bl->id);
+    output_rules_symbol((int) bl->left->id);
+    output_rules_endterm();
+    output_rules_symbol(-(int) bl->id);
+    output_rules_symbol(-(int) bl->left->id);
+    output_rules_endterm();
 }
diff --git a/scripts/parse_kconfig/cnfbuild.h b/scripts/parse_kconfig/cnfbuild.h
index e042cce..da31dce 100644
--- a/scripts/parse_kconfig/cnfbuild.h
+++ b/scripts/parse_kconfig/cnfbuild.h
@@ -1,36 +1,13 @@
 #include <stdlib.h>
 #include <stdbool.h>
 
-#include "symlist.h"
-#include <kconfig/lkc.h>
-#include "output.h"
-
 #ifndef _CNFBUILD_H_
 #define _CNFBUILD_H_
 
-enum cnfexpr_type {
-    CT_EXPR, CT_FALSE, CT_TRUE
-};
-
-struct cnfexpr {
-    enum cnfexpr_type type;
-    unsigned id;
-    struct output_expr *out;
-};
-
-struct cnfexpr *kconfig_expr(struct symlist *sl, struct expr *expr);
+#include "symlist.h"
+#include "boolexpr.h"
+#include "output.h"
 
-struct cnfexpr *cnfexpr_true(struct symlist *sl);
-struct cnfexpr *cnfexpr_false(struct symlist *sl);
-struct cnfexpr *cnfexpr_sym(struct symlist *sl, struct symbol *sym);
-struct cnfexpr *cnfexpr_eql(struct symlist *sl, struct symbol *sym1,
-                        struct symbol *sym2);
-struct cnfexpr *cnfexpr_or(struct symlist *sl, struct cnfexpr *e1,
-                       struct cnfexpr *e2);
-struct cnfexpr *cnfexpr_and(struct symlist *sl, struct cnfexpr *e1,
-                        struct cnfexpr *e2);
-struct cnfexpr *cnfexpr_not(struct symlist *sl, struct cnfexpr *e);
-struct cnfexpr *cnfexpr_copy(struct cnfexpr *e);
-void cnfexpr_free(struct cnfexpr *e);
+void cnf_boolexpr(struct symlist *sl, struct boolexpr *bl);
 
 #endif /* _CNFBUILD_H_ */
diff --git a/scripts/parse_kconfig/cnfexpr.c b/scripts/parse_kconfig/cnfexpr.c
deleted file mode 100644
index ea0b453..0000000
--- a/scripts/parse_kconfig/cnfexpr.c
+++ /dev/null
@@ -1,412 +0,0 @@
-#include "cnfexpr.h"
-
-struct cnfexpr *cnf_sym(struct symlist *sl, bool not, struct symbol *sym);
-struct cnfexpr *cnf_eql(struct symlist *sl, bool not, struct symbol *sym1,
-                        struct symbol *sym2);
-struct cnfexpr *cnf_or(struct cnfexpr *e1, struct cnfexpr *e2);
-struct cnfexpr *cnf_and(struct cnfexpr *e1, struct cnfexpr *e2);
-struct cnfexpr *cnf_not(struct cnfexpr *el);
-struct cnfexpr *cnf_copy(struct cnfexpr *el);
-void free_cnf(struct cnfexpr *e);
-
-struct cnfexpr *kconfig_cnfexpr(struct symlist *sl, bool nt, bool def,
-                                struct symbol *sym, struct expr *expr) {
-    struct stck {
-        struct expr *expr;
-        struct cnfexpr *cnf;
-    };
-    struct expr **back;
-    int back_size = 2, back_pos = -1;
-    back = malloc((unsigned) back_size * sizeof(struct expr *));
-    struct stck *stack;
-    int stack_size = 2, stack_pos = -1;
-    stack = malloc((unsigned) stack_size * sizeof(struct stck));
-    struct cnfexpr *rtrn = NULL;
-
-    while (expr != NULL) {
-        if ((back_pos >= 0 && back[back_pos] != expr) || back_pos < 0) {
-            if (++back_pos == back_size) {
-                back_size *= 2;
-                back =
-                    realloc(back,
-                            (unsigned) back_size * sizeof(struct expr *));
-            }
-            back[back_pos] = expr;
-        }
-        switch (expr->type) {
-        case E_SYMBOL:
-            rtrn = cnf_sym(sl, nt, expr->left.sym);
-            goto go_up;
-        case E_NOT:
-            nt = !nt;
-            if (rtrn == NULL)
-                expr = expr->left.expr;
-            else
-                goto go_up;
-            break;
-        case E_OR:
-        case E_AND:
-            if (stack_pos < 0 || stack[stack_pos].expr != expr) {
-                if (rtrn == NULL) {
-                    expr = expr->left.expr;
-                } else {
-                    if (stack_size == ++stack_pos) {
-                        stack_size *= 2;
-                        stack =
-                            realloc(stack,
-                                    (unsigned) stack_size *
-                                    sizeof(struct stck));
-                    }
-                    stack[stack_pos].expr = expr;
-                    stack[stack_pos].cnf = rtrn;
-                    expr = expr->right.expr;
-                    rtrn = NULL;
-                }
-            } else {
-                if ((!nt && expr->type == E_OR)
-                    || (nt && expr->type == E_AND))
-                    rtrn = cnf_or(stack[stack_pos].cnf, rtrn);
-                else
-                    rtrn = cnf_and(stack[stack_pos].cnf, rtrn);
-                stack_pos--;
-                goto go_up;
-            }
-            break;
-        case E_EQUAL:
-            rtrn = cnf_eql(sl, nt, expr->left.sym, expr->right.sym);
-            goto go_up;
-        case E_UNEQUAL:
-            rtrn = cnf_eql(sl, !nt, expr->left.sym, expr->right.sym);
-            goto go_up;
-        default:
-            fprintf(stderr, "ERROR: Unknown expression type.\n");
-        }
-        continue;
-
-      go_up:
-        if (--back_pos >= 0)
-            expr = back[back_pos];
-        else
-            expr = NULL;
-    }
-
-    free(back);
-    free(stack);
-
-    struct symlist_el *se = symlist_find(sl, sym->name);
-    if (se->prompt || (nt == true && def == true))
-        rtrn = cnf_or(cnf_sym(sl, !nt, sym), rtrn);
-    else {
-        struct cnfexpr *w12 = cnf_not(cnf_copy(rtrn));
-        struct cnfexpr *w11 = cnf_sym(sl, false, sym);
-        struct cnfexpr *w1 = cnf_or(w11, w12);
-        struct cnfexpr *w22 = rtrn;
-        struct cnfexpr *w21 = cnf_sym(sl, true, sym);
-        struct cnfexpr *w2 = cnf_or(w21, w22);
-        rtrn = cnf_and(w1, w2);
-        /*
-           rtrn =
-           cnf_and(cnf_or
-           (cnf_sym(sl, false, sym), cnf_not(cnf_copy(rtrn))),
-           cnf_or(cnf_sym(sl, true, sym), rtrn));
-         */
-    }
-
-    return rtrn;
-}
-
-void cnf_printf(struct cnfexpr *wcnf) {
-    if (wcnf == NULL) {
-        printf("hey NULL\n");
-        return;
-    }
-    switch (wcnf->type) {
-    case CT_TRUE:
-        printf("True\n");
-        return;
-    case CT_FALSE:
-        printf("False\n");
-        return;
-    case CT_EXPR:
-        break;
-    }
-    unsigned i, r;
-    for (i = 0; i < wcnf->size; i++) {
-        for (r = 0; r < wcnf->sizes[i]; r++) {
-            printf("%d ", wcnf->exprs[i][r]);
-        }
-        if (i < wcnf->size - 1)
-            printf("x ");
-    }
-    printf("\n");
-}
-
-struct cnfexpr *cnf_sym(struct symlist *sl, bool not, struct symbol *sym) {
-    struct cnfexpr *w = malloc(sizeof(struct cnfexpr));
-    struct symlist_el *se = symlist_find(sl, sym->name);
-    if (se == NULL) {
-        if (!not)
-            w->type = CT_FALSE;
-        else
-            w->type = CT_TRUE;
-    } else {
-        w->type = CT_EXPR;
-        w->size = 1;
-        w->sizes = malloc(sizeof(int));
-        w->sizes[0] = 1;
-        w->exprs = malloc(sizeof(int *));
-        w->exprs[0] = malloc(sizeof(int));
-        w->exprs[0][0] = (int) se->id;
-        if (not)
-            w->exprs[0][0] *= -1;
-    }
-    return w;
-}
-
-struct cnfexpr *cnf_eql(struct symlist *sl, bool not, struct symbol *sym1,
-                        struct symbol *sym2) {
-    if (!strcmp(sym2->name, "m")) {
-        struct cnfexpr *fls = malloc(sizeof(struct cnfexpr));
-        if (!not)
-            fls->type = CT_FALSE;
-        else
-            fls->type = CT_TRUE;
-        return fls;
-    }
-    if (!strcmp(sym2->name, "n")) {
-        return cnf_sym(sl, !not, sym1);
-    }
-    if (!strcmp(sym2->name, "y")) {
-        return cnf_sym(sl, not, sym1);
-    }
-
-    struct cnfexpr *w1 = cnf_sym(sl, not, sym1);
-    struct cnfexpr *w2 = cnf_sym(sl, not, sym2);
-    struct cnfexpr *w3 = cnf_sym(sl, !not, sym1);
-    struct cnfexpr *w4 = cnf_sym(sl, !not, sym2);
-    struct cnfexpr *wa = cnf_or(w1, w2);
-    struct cnfexpr *wb = cnf_or(w3, w4);
-    struct cnfexpr *w = cnf_and(wa, wb);
-    return w;
-}
-
-struct cnfexpr *cnf_or(struct cnfexpr *e1, struct cnfexpr *e2) {
-    switch (e1->type) {
-    case CT_TRUE:
-        free_cnf(e2);
-        return e1;
-    case CT_FALSE:
-        free_cnf(e1);
-        return e2;
-    case CT_EXPR:
-        switch (e2->type) {
-        case CT_TRUE:
-            free_cnf(e1);
-            return e2;
-        case CT_FALSE:
-            free_cnf(e2);
-            return e1;
-        case CT_EXPR:
-            break;
-        }
-        break;
-    }
-
-    unsigned oldsize = e1->size;
-    e1->size *= e2->size;
-    e1->sizes = realloc(e1->sizes, e1->size * sizeof(int));
-    e1->exprs = realloc(e1->exprs, e1->size * sizeof(int *));
-    unsigned i1, i2;
-    // Duplicate e2->size times e1
-    for (i2 = 1; i2 < e2->size; i2++) {
-        memcpy(e1->sizes + (i2 * oldsize), e1->sizes,
-               oldsize * sizeof(int));
-        for (i1 = 0; i1 < oldsize; i1++) {
-            e1->exprs[(i2 * oldsize) + i1] =
-                malloc(e1->sizes[i1] * sizeof(int));
-            memcpy(e1->exprs[(i2 * oldsize) + i1], e1->exprs[i1],
-                   e1->sizes[i1] * sizeof(int));
-        }
-    }
-    unsigned oldsizes;
-    // Append e2->exprs to e1->exprs
-    for (i2 = 0; i2 < e2->size; i2++) {
-        for (i1 = 0; i1 < oldsize; i1++) {
-            oldsizes = e1->sizes[(i2 * oldsize) + i1];
-            e1->sizes[(i2 * oldsize) + i1] += e2->sizes[i2];
-            e1->exprs[(i2 * oldsize) + i1] =
-                realloc(e1->exprs[(i2 * oldsize) + i1],
-                        e1->sizes[(i2 * oldsize) + i1] * sizeof(int));
-            memcpy(e1->exprs[(i2 * oldsize) + i1] + oldsizes,
-                   e2->exprs[i2], e2->sizes[i2] * sizeof(int));
-        }
-    }
-    free_cnf(e2);
-    return e1;
-}
-
-struct cnfexpr *cnf_and(struct cnfexpr *e1, struct cnfexpr *e2) {
-    switch (e1->type) {
-    case CT_FALSE:
-        free_cnf(e2);
-        return e1;
-    case CT_TRUE:
-        free_cnf(e1);
-        return e2;
-    case CT_EXPR:
-        switch (e2->type) {
-        case CT_FALSE:
-            free_cnf(e1);
-            return e2;
-        case CT_TRUE:
-            free_cnf(e2);
-            return e1;
-        case CT_EXPR:
-            break;
-        }
-        break;
-    }
-
-    unsigned oldsize = e1->size;
-    e1->size += e2->size;
-    e1->sizes = realloc(e1->sizes, e1->size * sizeof(int));
-    e1->exprs = realloc(e1->exprs, e1->size * sizeof(int *));
-    memcpy(e1->sizes + oldsize, e2->sizes, e2->size * sizeof(int));
-    unsigned i;
-    for (i = 0; i < e2->size; i++) {
-        e1->exprs[oldsize + i] = malloc(e2->sizes[i] * sizeof(int));
-        memcpy(e1->exprs[oldsize + i], e2->exprs[i],
-               e2->sizes[i] * sizeof(int));
-    }
-    free_cnf(e2);
-    return e1;
-}
-
-struct cnfexpr *cnf_not_dissolve(struct cnfexpr *expr, unsigned i) {
-    struct cnfexpr *w;
-    unsigned y;
-    w = malloc(sizeof(struct cnfexpr));
-    w->type = CT_EXPR;
-    w->size = expr->sizes[i];
-    w->exprs = malloc(w->size * sizeof(int *));
-    w->sizes = malloc(w->size * sizeof(unsigned));
-    for (y = 0; y < w->size; y++) {
-        w->sizes[y] = 1;
-        w->exprs[y] = malloc(sizeof(int));
-        w->exprs[y][0] = -1 * expr->exprs[i][y];
-    }
-    return w;
-}
-
-struct cnfexpr *cnf_not(struct cnfexpr *expr) {
-    switch (expr->type) {
-    case CT_TRUE:
-        expr->type = CT_FALSE;
-        return expr;
-    case CT_FALSE:
-        expr->type = CT_TRUE;
-        return expr;
-    case CT_EXPR:
-        break;
-    }
-    struct cnfexpr *rtrn, *w;
-    unsigned i = 0;
-    rtrn = cnf_not_dissolve(expr, 0);
-    for (i = 1; i < expr->size; i++) {
-        w = cnf_not_dissolve(expr, i);
-        rtrn = cnf_or(rtrn, w);
-    }
-    return rtrn;
-}
-
-struct cnfexpr *cnf_copy(struct cnfexpr *el) {
-    struct cnfexpr *rtrn;
-    rtrn = malloc(sizeof(struct cnfexpr));
-    rtrn->type = el->type;
-    rtrn->size = el->size;
-    if (el->type != CT_EXPR)
-        return rtrn;
-    rtrn->sizes = malloc(rtrn->size * sizeof(int));
-    memcpy(rtrn->sizes, el->sizes, rtrn->size * sizeof(int));
-    rtrn->exprs = malloc(rtrn->size * sizeof(int *));
-    unsigned i;
-    for (i = 0; i < rtrn->size; i++) {
-        rtrn->exprs[i] = malloc(rtrn->sizes[i] * sizeof(int));
-        memcpy(rtrn->exprs[i], el->exprs[i], rtrn->sizes[i] * sizeof(int));
-    }
-    return rtrn;
-}
-
-void free_cnf(struct cnfexpr *e) {
-    if (e->type != CT_EXPR) {
-        free(e);
-        return;
-    }
-    unsigned i;
-    for (i = 0; i < e->size; i++) {
-        free(e->exprs[i]);
-    }
-    free(e->exprs);
-    free(e->sizes);
-    free(e);
-}
-
-
-struct boolexp *printf_original(struct symlist *sl, struct expr *expr) {
-    switch (expr->type) {
-    case E_OR:
-        printf("  OR\n");
-        printf_original(sl, expr->left.expr);
-        printf_original(sl, expr->right.expr);
-        break;
-    case E_AND:
-        printf("  AND\n");
-        printf_original(sl, expr->left.expr);
-        printf_original(sl, expr->right.expr);
-        break;
-    case E_NOT:
-        printf("  NOT\n");
-        printf_original(sl, expr->left.expr);
-        break;
-    case E_EQUAL:
-        printf("  = ");
-        printf("%s ", expr->left.sym->name);
-        if (!strcmp("y", expr->right.sym->name))
-            printf("YES\n");
-        else if (!strcmp("n", expr->right.sym->name))
-            printf("NO\n");
-        else if (!strcmp("m", expr->right.sym->name))
-            printf("MODULE\n");
-        else
-            printf("%s\n", expr->left.sym->name);
-        break;
-    case E_UNEQUAL:
-        printf("  != ");
-        printf("%s ", expr->left.sym->name);
-        if (!strcmp("y", expr->right.sym->name))
-            printf("YES\n");
-        else if (!strcmp("n", expr->right.sym->name))
-            printf("NO\n");
-        else
-            printf("OTHER %s\n", expr->right.sym->name);
-        break;
-    case E_LIST:
-        printf("  list\n");
-        break;
-    case E_SYMBOL:
-        printf("  symbol");
-        if (expr->left.sym->name != NULL)
-            printf(": %s", expr->left.sym->name);
-        printf("\n");
-        break;
-    case E_RANGE:
-        printf("  range\n");
-        break;
-    case E_NONE:
-        printf("  none\n");
-        break;
-    default:
-        printf("  ERROR\n");
-        break;
-    }
-}
diff --git a/scripts/parse_kconfig/cnfexpr.h b/scripts/parse_kconfig/cnfexpr.h
deleted file mode 100644
index 685ad9b..0000000
--- a/scripts/parse_kconfig/cnfexpr.h
+++ /dev/null
@@ -1,27 +0,0 @@
-#ifndef _CNFEXPR_H_
-#define _CNFEXPR_H_
-
-#include <stdlib.h>
-#include <stdbool.h>
-#include <stdio.h>
-#include "symlist.h"
-#include <kconfig/lkc.h>
-
-enum cnfexpr_type {
-    CT_EXPR, CT_FALSE, CT_TRUE
-};
-
-struct cnfexpr {
-    enum cnfexpr_type type;
-    int **exprs;
-    unsigned *sizes;
-    unsigned size;
-};
-
-struct cnfexpr *kconfig_cnfexpr(struct symlist *sl, bool nt, bool def,
-                                struct symbol *sym, struct expr *expr);
-void cnf_printf(struct cnfexpr *);
-
-struct boolexp *printf_original(struct symlist *sl, struct expr *expr);
-
-#endif /* _CNFEXPR_H_ */
diff --git a/scripts/parse_kconfig/output.c b/scripts/parse_kconfig/output.c
index 3863139..47442ce 100644
--- a/scripts/parse_kconfig/output.c
+++ b/scripts/parse_kconfig/output.c
@@ -17,118 +17,22 @@ void output_finish(void) {
 
 
 // Functions for symbol_map
-void output_push_symbol(int id, char *name) {
+void output_push_symbol(unsigned id, char *name) {
     fprintf(fsymmap, "%d:%s\n", id, name);
 }
 
 // Functions for rules
-struct output_expr *output_rules_newexpr(void) {
-    struct output_expr *rtn;
-    rtn = malloc(sizeof(struct output_expr));
-    rtn->terms_size = 1;
-    rtn->terms_pos = 0;
-    rtn->terms = malloc(rtn->terms_size * sizeof(int *));
-    rtn->terms_sizes = malloc(rtn->terms_size * sizeof(size_t));
-
-    rtn->w_term_size = 1;
-    rtn->w_term_pos = 0;
-    rtn->w_term = malloc(rtn->w_term_size * sizeof(int));
-
-    return rtn;
-}
-
-void output_rules_symbol(struct output_expr *ex, int id) {
-    if (++(ex->w_term_pos) >= ex->w_term_size) {
-        ex->w_term_size *= 2;
-        ex->w_term = realloc(ex->w_term, ex->w_term_size * sizeof(int));
-    }
-    ex->w_term[ex->w_term_pos - 1] = id;
-}
-
-void output_rules_endterm(struct output_expr *ex) {
-    if (ex->w_term_pos <= 0)
-        return;
-    if (++(ex->terms_pos) >= ex->terms_size) {
-        ex->terms_size *= 2;
-        ex->terms = realloc(ex->terms, ex->terms_size * sizeof(int *));
-        ex->terms_sizes =
-            realloc(ex->terms_sizes, ex->terms_size * sizeof(size_t));
-    }
-    ex->terms_sizes[ex->terms_pos - 1] = ex->w_term_pos;
-    ex->terms[ex->terms_pos - 1] = malloc(ex->w_term_pos * sizeof(int));
-    memcpy(ex->terms[ex->terms_pos - 1], ex->w_term,
-           ex->w_term_pos * sizeof(int));
-    ex->w_term_pos = 0;
-}
-
-struct output_expr *output_rules_joinexpr(struct output_expr *ex1,
-                                          struct output_expr *ex2) {
-    if (ex1 == NULL)
-        if (ex2 == NULL)
-            return NULL;
-        else
-            return ex2;
-    if (ex2 == NULL)
-        return ex1;
-
-    if ((ex1->terms_pos + ex2->terms_pos) >= ex1->terms_size) {
-        ex1->terms_size += ex2->terms_pos;
-        ex1->terms = realloc(ex1->terms, ex1->terms_size * sizeof(int *));
-        ex1->terms_sizes =
-            realloc(ex1->terms_sizes, ex1->terms_size * sizeof(size_t));
-    }
-    memcpy(ex1->terms + ex1->terms_pos - 1, ex2->terms,
-           ex2->terms_pos * sizeof(int *));
-    memcpy(ex1->terms_sizes + ex1->terms_size - 1, ex2->terms_sizes,
-           ex2->terms_pos * sizeof(size_t));
-    ex1->terms_pos += ex2->terms_pos;
-
-    ex1->w_term_pos = 0;
-    free(ex2->terms);
-    free(ex2->terms_sizes);
-    free(ex2);
-    return ex1;
-}
-
-struct output_expr *output_rules_copycnf(struct output_expr *ex) {
-    struct output_expr *rtn;
-    rtn = malloc(sizeof(struct output_expr));
-    rtn->terms_size = ex->terms_size;
-    rtn->terms_pos = ex->terms_pos;
-    rtn->terms_sizes = malloc(rtn->terms_size * sizeof(size_t));
-    memcpy(rtn->terms_sizes, ex->terms_sizes,
-           rtn->terms_size * sizeof(size_t));
-    rtn->terms = malloc(rtn->terms_size * sizeof(int *));
-    size_t i;
-    for (i = 0; i < rtn->terms_pos; i++) {
-        rtn->terms[i] = malloc(ex->terms_sizes[i] * sizeof(int));
-        memcpy(rtn->terms[i], ex->terms[i],
-               ex->terms_sizes[i] * sizeof(int));
-    }
-
-    ex->w_term_size = 1;
-    ex->w_term_pos = 0;
-    ex->w_term = malloc(ex->w_term_size * sizeof(int));
-    return rtn;
+void output_rules_symbol(int id) {
+    fprintf(frules, "%d ", id);
 }
 
-void output_rules_freexpr(struct output_expr *ex) {
-    size_t i;
-    for (i = 0; i < ex->terms_pos; i++) {
-        free(ex->terms[i]);
-    }
-    free(ex->terms);
-    free(ex->terms_sizes);
-    free(ex->w_term);
-    free(ex);
+void output_rules_endterm(void) {
+    fprintf(frules, "\n");
 }
 
-void output_rules_writexpr(struct output_expr *ex) {
-    size_t i, y;
-    for (i = 0; i < ex->terms_pos; i++) {
-        for (y = 0; y < ex->terms_sizes[i]; y++) {
-            fprintf(frules, "%d ", ex->terms[i][y]);
-        }
-        fprintf(frules, "\n");
-    }
+void output_write_variable_count(char *var_file, int count) {
+    FILE *f;
+    f = fopen(var_file, "w");
+    fprintf(f, "%d", count);
+    fclose(f);
 }
diff --git a/scripts/parse_kconfig/output.h b/scripts/parse_kconfig/output.h
index a1b43aa..de8f672 100644
--- a/scripts/parse_kconfig/output.h
+++ b/scripts/parse_kconfig/output.h
@@ -1,35 +1,23 @@
-#ifndef _OUTPUT_H_
-#define _OUTPUT_H_
-
 #include <stdlib.h>
 #include <stdio.h>
 
-#include "symlist.h"
 #include <build_files.h>
 
+#ifndef _OUTPUT_H_
+#define _OUTPUT_H_
+
+#include "symlist.h"
+
 int output_init(char *rules_file, char *symbolmap_file);
 void output_finish(void);
 
 // Functions for symbol_map
-void output_push_symbol(int id, char *name);
+void output_push_symbol(unsigned id, char *name);
 
 // Functions for rules
-struct output_expr {
-    int **terms;
-    size_t *terms_sizes;
-    size_t terms_size, terms_pos;
-
-    int *w_term;
-    size_t w_term_size, w_term_pos;
-};
-
-struct output_expr *output_rules_newexpr(void);
-void output_rules_symbol(struct output_expr *ex, int id);
-void output_rules_endterm(struct output_expr *ex);
-struct output_expr *output_rules_joinexpr(struct output_expr *ex1,
-                                          struct output_expr *ex2);
-struct output_expr *output_rules_copycnf(struct output_expr *ex);
-void output_rules_freexpr(struct output_expr *ex);
-void output_rules_writexpr(struct output_expr *ex);
+void output_rules_symbol(int id);
+void output_rules_endterm(void);
 
+// Functions for variable_count
+void output_write_variable_count(char *var_file, int count);
 #endif /* _OUTPUT_H_ */
diff --git a/scripts/parse_kconfig/parse.c b/scripts/parse_kconfig/parse.c
index e464159..1a6fc92 100644
--- a/scripts/parse_kconfig/parse.c
+++ b/scripts/parse_kconfig/parse.c
@@ -6,6 +6,7 @@
 #include <libintl.h>
 
 #include <kconfig/lkc.h>
+#include "boolexpr.h"
 #include "symlist.h"
 #include "output.h"
 #include "macros.h"
@@ -53,19 +54,25 @@ int main(int argc, char **argv) {
 
     gsymlist = symlist_create();
 
-    char *rules_file, *symbol_map_file;
+    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);
+
+    output_finish();
     return 0;
 }
 
 void build_symlist() {
     int i;
     struct symbol *sym;
+    struct property *prop;
     for_all_symbols(i, sym) {
         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
             if (sym->name == NULL) {
@@ -74,17 +81,18 @@ void build_symlist() {
             }
             symlist_add(gsymlist, sym->name);
         }
-        struct property *prop;
         for_all_prompts(sym, prop) {
             gsymlist->array[gsymlist->pos - 1].prompt = true;
             break;
         }
     }
+    symlist_closesym(gsymlist);
 }
 
 void cpy_dep() {
     int i;
     struct symbol *sym;
+    struct property *prop;
     struct symlist_el *el;
     unsigned el_id;
     for_all_symbols(i, sym) {
@@ -93,56 +101,59 @@ void cpy_dep() {
             el = &(gsymlist->array[el_id - 1]);
 
             for_all_defaults(sym, prop) {
-                gsymlist->array[gsymlist->pos - 1].def = true;
-                struct cnfexpr *def =
-                    kconfig_cnfexpr(gsymlist, prop->expr);
+                struct boolexpr *def =
+                    boolexpr_kconfig(gsymlist, prop->expr);
                 if (el->def == NULL) {
-                    gsymlist->array[gsymlist->pos - 1].def = def;
+                    el->def = def;
                 } else {
-                    gsymlist->array[gsymlist->pos - 1].def =
-                        cnfexpr_or(gsymlist,
-                                   gsymlist->array[gsymlist->pos - 1].def,
-                                   def);
+                    el->def = boolexpr_or(el->def, def);
                 }
             }
             if (el->def == NULL)
-                el->cnfexpr_false(gsymlist);
+                el->def = boolexpr_false();
             if (sym->dir_dep.expr != NULL)
-                el->dep = kconfig_cnfexpr(gsymlist, sym->dir_dep.expr);
+                el->dep = boolexpr_kconfig(gsymlist, sym->dir_dep.expr);
             else
-                el->dep = cnfexpr_true(gsymlist);
+                el->dep = boolexpr_true();
             if (sym->rev_dep.expr != NULL)
-                el->re_be = kconfig_cnfexpr(gsymlist, sym->rev_dep.expr);
+                el->rev_dep =
+                    boolexpr_kconfig(gsymlist, sym->rev_dep.expr);
             else
-                el->rev_dep = cnfexpr_false(gsymlist);
-
-            if (el->prompt) {
-                struct cnfexpr *pw =
-                    cnfexpr_and(gsymlist,
-                                cnfexpr_or(gsymlist,
-                                           cnfexpr_not(gsymlist,
-                                                       cnfexpr_sym
-                                                       (gsymlist,
-                                                        sym->name)),
-                                           el->dep), cnfexpr_or(gsymlist,
-                                                                cnfexpr_not
-                                                                (gsymlist,
-                                                                 el->
-                                                                 rev_dep),
-                                                                cnfexpr_sym
-                                                                (gsymlist,
-                                                                 sym->
-                                                                 name)));
-                switch (pw->type) {
-                    case CT_EXPR:
-                        break;
-                    case CT_TRUE:
-                        break;
-                    case CT_FALSE:
-                        break;
-                }
-            } else {
+                el->rev_dep = boolexpr_false();
+
+            struct boolexpr *pw;
+            Iprintf("Workig: %s\n", sym->name);
+            struct boolexpr *boolsym = boolexpr_sym(gsymlist, sym);
+            boolexpr_copy(boolsym);
+            struct boolexpr *boolsym_not = boolexpr_not(boolsym);
+            if (!el->prompt) {
+                boolexpr_copy(boolsym);
+                boolexpr_copy(boolsym_not);
+                boolexpr_copy(el->def);
+                boolexpr_copy(el->dep);
+                boolexpr_copy(el->rev_dep);
+            }
+            // (!sym || dep) && (sym || !rev_dep)
+            struct boolexpr *w1 = boolexpr_or(boolsym_not, el->dep);
+            struct boolexpr *w2 =
+                boolexpr_or(boolsym, boolexpr_not(el->rev_dep));
+            pw = boolexpr_and(w1, w2);
+
+            if (!el->prompt) {
+                // && (sym || !dep || !def) &&
+                // (!sym || rev_dep || def)
+                struct boolexpr *w31 =
+                    boolexpr_or(boolsym, boolexpr_not(el->dep));
+                struct boolexpr *w3 =
+                    boolexpr_or(w31, boolexpr_not(el->def));
+                struct boolexpr *w41 =
+                    boolexpr_or(boolsym_not, el->rev_dep);
+                struct boolexpr *w4 = boolexpr_or(w41, el->def);
+                pw = boolexpr_and(pw, w3);
+                pw = boolexpr_and(pw, w4);
             }
+            cnf_boolexpr(gsymlist, pw);
+            boolexpr_free(pw);
         }
     }
 }
diff --git a/scripts/parse_kconfig/symlist.c b/scripts/parse_kconfig/symlist.c
index f5f42ab..042a950 100644
--- a/scripts/parse_kconfig/symlist.c
+++ b/scripts/parse_kconfig/symlist.c
@@ -22,6 +22,7 @@ void symlist_add(struct symlist *sl, char *name) {
     sl->array[sl->pos].def_size = 0;
     sl->array[sl->pos].dep = NULL;
     sl->array[sl->pos].rev_dep = NULL;
+    output_push_symbol((unsigned) sl->pos, name);
     sl->pos++;
 }
 
@@ -46,6 +47,10 @@ struct symlist_el *symlist_find(struct symlist *sl, char *name) {
 
 // TODO faster implementation? Maybe binary search tree?
 size_t symlist_id(struct symlist * sl, char *name) {
+    if (name == NULL) {
+        printf("Aha\n");
+        return 0;
+    }
     size_t i = 0;
     while (i < sl->pos) {
         if (!strcmp(name, sl->array[i].name))
@@ -55,20 +60,6 @@ size_t symlist_id(struct symlist * sl, char *name) {
     return 0;
 }
 
-void symlist_print(struct symlist *sl) {
-    /*
-       size_t i;
-       for (i = 0; i < sl->pos; i++) {
-       printf("%d:%s\n", sl->array[i].id, sl->array[i].name);
-       if (sl->array[i].be != NULL) {
-       printf("  ");
-       cnf_printf(sl->array[i].be);
-       printf("\n");
-       }
-       }
-     */
-}
-
 void symlist_free(struct symlist *sl) {
     free(sl->array);
     free(sl);
diff --git a/scripts/parse_kconfig/symlist.h b/scripts/parse_kconfig/symlist.h
index 7d24bd1..85f473e 100644
--- a/scripts/parse_kconfig/symlist.h
+++ b/scripts/parse_kconfig/symlist.h
@@ -4,12 +4,12 @@
 #include <string.h>
 #include <search.h>
 
-#include "cnfbuild.h"
-#include "output.h"
-
 #ifndef _SYMLIST_H_
 #define _SYMLIST_H_
 
+#include "cnfbuild.h"
+#include "output.h"
+
 struct symlist_el {
     char *name;
     bool prompt;
@@ -31,7 +31,6 @@ void symlist_closesym(struct symlist *sl);
 unsigned symlist_adddummy(struct symlist *sl);
 struct symlist_el *symlist_find(struct symlist *sl, char *name);
 size_t symlist_id(struct symlist *sl, char *name);
-void symlist_print(struct symlist *sl);
 void symlist_free(struct symlist *sl);
 
 #endif /* _SYMLIST_H_ */