Simplify parse_kconfig generated CNF formulas

Not isn't now generated using additional variable.
All head formulas for all configuration options are now printed directly as formulas. Not build using functions.

1 files changed, 17 insertions, 16 deletions

diff --git a/scripts/parse_kconfig/cnfbuild.c b/scripts/parse_kconfig/cnfbuild.c
index 398a934..26a9265 100644
--- a/scripts/parse_kconfig/cnfbuild.c
+++ b/scripts/parse_kconfig/cnfbuild.c
@@ -14,14 +14,10 @@ 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.
+    if (bl->type == BT_TRUE || bl->type == BT_FALSE)
+        return;
+    if (bl->id != 0)
         return;
-    } else if (bl->type == BT_FALSE) {
-        fprintf(stderr,
-                "E: Trying to write false term. This shouldn't happen.\n");
-        exit(6);
-    }
 
     struct stck *stack = stack_create();
     while (bl != NULL) {
@@ -131,13 +127,18 @@ void cnf_or(struct symlist *sl, struct boolexpr *bl) {
 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();
+    bl->id = -1 * bl->left->id;
+    /*
+       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();
+       output_rules_symbol((int) bl->id);
+       output_rules_symbol((int) bl->left->id);
+     */
 }