From 485c55bcca5ad0480cf3c73b006a98e26ccc3f52 Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Karel=20Ko=C4=8D=C3=AD?= Date: Fri, 17 Jul 2015 11:41:50 +0200 Subject: 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. --- scripts/parse_kconfig/cnfbuild.c | 33 +++++++++++++++++---------------- 1 file changed, 17 insertions(+), 16 deletions(-) (limited to 'scripts/parse_kconfig/cnfbuild.c') 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); + */ } -- cgit v1.2.3