Simplify parse_kconfig generated CNF formulas

[linux-conf-perf.git] / scripts / parse_kconfig / cnfbuild.c

diff --git a/scripts/parse_kconfig/cnfbuild.c b/scripts/parse_kconfig/cnfbuild.c
index 398a9345b7d2fbb05d4b814c53993f23a8600f11..26a9265e38d76a06c0160797a5bcd1df2e83c962 100644 (file)
--- 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);
+     */
 }