All of lore.kernel.org
 help / color / mirror / Atom feed
From: Thorsten Berger <thorsten.berger@rub.de>
To: linux-kbuild@vger.kernel.org
Cc: deltaone@debian.org, phayax@gmail.com,
	Eugene Groshev <eugene.groshev@gmail.com>,
	Sarah Nadi <nadi@ualberta.ca>, Mel Gorman <mgorman@suse.de>,
	"Luis R. Rodriguez" <mcgrof@suse.com>
Subject: [RFC v3 07/12] Add files for handling expressions
Date: Fri, 22 Oct 2021 15:43:10 +0200	[thread overview]
Message-ID: <0aad8a90-2704-4f8b-625c-0ee591109738@rub.de> (raw)
In-Reply-To: <7706ed5e-4771-770a-5cf2-d3c8346fa1dc@rub.de>

Co-developed-by: Patrick Franz <deltaone@debian.org>
Signed-off-by: Patrick Franz <deltaone@debian.org>
Co-developed-by: Ibrahim Fayaz <phayax@gmail.com>
Signed-off-by: Ibrahim Fayaz <phayax@gmail.com>
Reviewed-by: Luis Chamberlain <mcgrof@suse.com>
Tested-by: Evgeny Groshev <eugene.groshev@gmail.com>
Suggested-by: Sarah Nadi <nadi@ualberta.ca>
Suggested-by: Thorsten Berger <thorsten.berger@rub.de>
Signed-off-by: Thorsten Berger <thorsten.berger@rub.de>

To translate the Kconfig-model into propositional logic and resolve
conflicts, we need to handle propostional formulas.
These files contain many functions and macros to deal with
propositional formulas.

---
 scripts/kconfig/cf_expr.c | 2146 +++++++++++++++++++++++++++++++++++++
 scripts/kconfig/cf_expr.h |  237 ++++
 2 files changed, 2383 insertions(+)
 create mode 100644 scripts/kconfig/cf_expr.c
 create mode 100644 scripts/kconfig/cf_expr.h

diff --git a/scripts/kconfig/cf_expr.c b/scripts/kconfig/cf_expr.c
new file mode 100644
index 000000000000..7ca0ff4bc6ad
--- /dev/null
+++ b/scripts/kconfig/cf_expr.c
@@ -0,0 +1,2146 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2021 Patrick Franz <deltaone@debian.org>
+ */
+
+#define _GNU_SOURCE
+#include <assert.h>
+#include <locale.h>
+#include <stdarg.h>
+#include <stdbool.h>
+#include <stdio.h>
+#include <stdlib.h>
+#include <string.h>
+#include <time.h>
+#include <unistd.h>
+
+#include "configfix.h"
+
+static void create_fexpr_bool(struct symbol *sym);
+static void create_fexpr_nonbool(struct symbol *sym);
+static void create_fexpr_unknown(struct symbol *sym);
+static void create_fexpr_choice(struct symbol *sym);
+
+static void pexpr_print_util(struct pexpr *e, int prevtoken);
+
+static int trans_count;
+
+
+/*
+ *  create a fexpr
+ */
+struct fexpr * fexpr_create(int satval, enum fexpr_type type, char *name)
+{
+    struct fexpr *e = xcalloc(1, sizeof(*e));
+    e->satval = satval;
+    e->type = type;
+    e->name = str_new();
+    e->assumption = false;
+    str_append(&e->name, name);
+
+    return e;
+}
+
+/*
+ * create the fexpr for a symbol
+ */
+void sym_create_fexpr(struct symbol *sym)
+{
+    if (sym_is_choice(sym))
+        create_fexpr_choice(sym);
+    else if (sym_is_boolean(sym))
+        create_fexpr_bool(sym);
+    else if (sym_is_nonboolean(sym))
+        create_fexpr_nonbool(sym);
+    else
+        create_fexpr_unknown(sym);
+}
+
+/*
+ * create the fexpr for symbols with reverse dependencies
+ */
+static void create_fexpr_selected(struct symbol *sym)
+{
+    /* fexpr_sel_y */
+    struct fexpr *fexpr_sel_y = fexpr_create(sat_variable_nr++, FE_SELECT, sym->name);
+    str_append(&fexpr_sel_y->name, "_sel_y");
+    fexpr_sel_y->sym = sym;
+    fexpr_add_to_satmap(fexpr_sel_y);
+
+    sym->fexpr_sel_y = fexpr_sel_y;
+
+    /* fexpr_sel_m */
+    if (sym->type == S_BOOLEAN)
+        return;
+    struct fexpr *fexpr_sel_m = fexpr_create(sat_variable_nr++, FE_SELECT, sym->name);
+    str_append(&fexpr_sel_m->name, "_sel_m");
+    fexpr_sel_m->sym = sym;
+    fexpr_add_to_satmap(fexpr_sel_m);
+
+    sym->fexpr_sel_m = fexpr_sel_m;
+}
+
+/*
+ * create the fexpr for a boolean/tristate symbol
+ */
+static void create_fexpr_bool(struct symbol *sym)
+{
+    struct fexpr *fexpr_y = fexpr_create(sat_variable_nr++, FE_SYMBOL, sym->name);
+    fexpr_y->sym = sym;
+    fexpr_y->tri = yes;
+    fexpr_add_to_satmap(fexpr_y);
+
+    sym->fexpr_y = fexpr_y;
+
+    struct fexpr *fexpr_m;
+    if (sym->type == S_TRISTATE) {
+        fexpr_m = fexpr_create(sat_variable_nr++, FE_SYMBOL, sym->name);
+        str_append(&fexpr_m->name, "_MODULE");
+        fexpr_m->sym = sym;
+        fexpr_m->tri = mod;
+        fexpr_add_to_satmap(fexpr_m);
+    } else {
+        fexpr_m = const_false;
+    }
+
+    sym->fexpr_m = fexpr_m;
+
+    if (sym->rev_dep.expr)
+        create_fexpr_selected(sym);
+}
+
+/*
+ * create the fexpr for a non-boolean symbol
+ */
+static void create_fexpr_nonbool(struct symbol *sym)
+{
+    sym->fexpr_y = const_false;
+    sym->fexpr_m = const_false;
+    sym->nb_vals = fexpr_list_init();
+
+    /* default values */
+    char int_values[][2] = {"n", "0", "1"};
+    char hex_values[][4] = {"n", "0x0", "0x1"};
+    char string_values[][9] = {"n", "", "nonempty"};
+
+    int i;
+    for (i = 0; i < 3; i++) {
+        struct fexpr *e = fexpr_create(sat_variable_nr++, FE_NONBOOL, sym->name);
+        e->sym = sym;
+        str_append(&e->name, "=");
+        e->nb_val = str_new();
+
+        switch (sym->type) {
+        case S_INT:
+            str_append(&e->name, int_values[i]);
+            str_append(&e->nb_val, int_values[i]);
+            break;
+        case S_HEX:
+            str_append(&e->name, hex_values[i]);
+            str_append(&e->nb_val, hex_values[i]);
+            break;
+        case S_STRING:
+            str_append(&e->name, string_values[i]);
+            str_append(&e->nb_val, string_values[i]);
+            break;
+        default:
+            break;
+        }
+
+        fexpr_list_add(sym->nb_vals, e);
+        fexpr_add_to_satmap(e);
+    }
+}
+
+
+/*
+ * set fexpr_y and fexpr_m simply to False
+ */
+static void create_fexpr_unknown(struct symbol *sym)
+{
+    sym->fexpr_y = const_false;
+    sym->fexpr_m = const_false;
+}
+
+
+/*
+ * create the fexpr for a choice symbol
+ */
+static void create_fexpr_choice(struct symbol *sym)
+{
+    if (!sym_is_boolean(sym))
+        return;
+
+    struct property *prompt = sym_get_prompt(sym);
+    if (prompt == NULL) {
+        perror("Choice symbol should have a prompt.");
+        return;
+    }
+
+    char *name = strdup(prompt->text);
+
+    /* remove spaces */
+    char *write = name, *read = name;
+    do {
+        if (*read != ' ')
+            *write++ = *read;
+    } while (*read++);
+
+    struct fexpr *fexpr_y = fexpr_create(sat_variable_nr++, FE_CHOICE, "Choice_");
+    str_append(&fexpr_y->name, name);
+    fexpr_y->sym = sym;
+    fexpr_y->tri = yes;
+    fexpr_add_to_satmap(fexpr_y);
+
+    sym->fexpr_y = fexpr_y;
+
+    struct fexpr *fexpr_m;
+    if (sym->type == S_TRISTATE) {
+        fexpr_m = fexpr_create(sat_variable_nr++, FE_CHOICE, "Choice_");
+        str_append(&fexpr_m->name, name);
+        str_append(&fexpr_m->name, "_MODULE");
+        fexpr_m->sym = sym;
+        fexpr_m->tri = mod;
+        fexpr_add_to_satmap(fexpr_m);
+    } else {
+        fexpr_m = const_false;
+    }
+    sym->fexpr_m = fexpr_m;
+}
+
+/*
+ * evaluate an unequality between a non-Boolean symbol and a constant
+ */
+static struct pexpr * expr_eval_unequal_nonbool_const(struct symbol *sym, struct symbol *compval, enum expr_type type)
+{
+    if (!sym || !compval)
+        return pexf(const_false);
+
+    int base = 0;
+    switch (sym->type) {
+    case S_INT:
+        base = 10;
+        break;
+    case S_HEX:
+        base = 16;
+        break;
+    default:
+        break;
+    }
+
+    struct pexpr *c = pexf(const_false);
+    long val = strtol(compval->name, NULL, base);
+
+    struct fexpr_node *node;
+    struct fexpr *fe;
+    for (node = sym->nb_vals->head->next; node != NULL; node = node->next) {
+        fe = node->elem;
+        long symval = strtol(str_get(&fe->nb_val), NULL, base);
+
+        switch (type) {
+        case E_LTH:
+            if (symval < val)
+                c = pexpr_or(c, pexf(fe));
+            break;
+        case E_LEQ:
+            if (symval <= val)
+                c = pexpr_or(c, pexf(fe));
+            break;
+        case E_GTH:
+            if (symval > val)
+                c = pexpr_or(c, pexf(fe));
+            break;
+        case E_GEQ:
+            if (symval >= val)
+                c = pexpr_or(c, pexf(fe));
+            break;
+        default:
+            perror("Illegal unequal.");
+        }
+    }
+
+    return c;
+}
+
+/*
+ * evaluate an unequality between 2 Boolean symbols
+ */
+static struct pexpr * expr_eval_unequal_bool(struct symbol *left, struct symbol *right, enum expr_type type)
+{
+    if (!left || !right)
+        return pexf(const_false);
+
+    if (!sym_is_boolean(left) || !sym_is_boolean(right)) {
+        perror("Comparing 2 symbols that should be boolean.");
+        return pexf(const_false);
+    }
+
+    struct pexpr *c = pexf(const_false);
+    switch (type) {
+    case E_LTH:
+        c = pexpr_and(
+            pexpr_not(sym_get_fexpr_both(left)),
+            sym_get_fexpr_both(right));
+        if (left->type == S_TRISTATE)
+            c = pexpr_or(c,
+                pexpr_and
+                    (pexf(left->fexpr_m),
+                     pexf(right->fexpr_y)));
+        break;
+    case E_LEQ:
+        c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y));
+        if (left->type == S_TRISTATE)
+            c = pexpr_or(c,
+                pexpr_and(
+                    pexf(left->fexpr_m),
+                    sym_get_fexpr_both(right)));
+        c = pexpr_or(c, pexpr_not(sym_get_fexpr_both(left)));
+        break;
+    case E_GTH:
+        c = pexpr_and(
+            sym_get_fexpr_both(left),
+            pexpr_not(sym_get_fexpr_both(right)));
+        if (right->type == S_TRISTATE)
+            c = pexpr_or(c,
+                pexpr_and
+                    (pexf(left->fexpr_y),
+                     pexf(right->fexpr_m)));
+        break;
+    case E_GEQ:
+        c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y));
+        if (right->type == S_TRISTATE)
+            c = pexpr_or(c,
+                pexpr_and(
+                    sym_get_fexpr_both(left),
+                    pexf(right->fexpr_m)));
+        c = pexpr_or(c, pexpr_not(sym_get_fexpr_both(right)));
+        break;
+    default:
+        perror("Wrong type in expr_eval_unequal_bool.");
+    }
+
+    return c;
+}
+/*
+ * calculate, when expr will evaluate to yes or mod
+ */
+struct pexpr * expr_calculate_pexpr_both(struct expr *e)
+{
+    if (!e)
+        return pexf(const_false);
+
+    if (!expr_can_evaluate_to_mod(e))
+        return expr_calculate_pexpr_y(e);
+
+    switch (e->type) {
+    case E_SYMBOL:
+        return pexpr_or(expr_calculate_pexpr_m(e), expr_calculate_pexpr_y(e));
+    case E_AND:
+        return expr_calculate_pexpr_both_and(e->left.expr, e->right.expr);
+    case E_OR:
+        return expr_calculate_pexpr_both_or(e->left.expr, e->right.expr);
+    case E_NOT:
+        return pexpr_or(expr_calculate_pexpr_m(e), expr_calculate_pexpr_y(e));
+    case E_EQUAL:
+        return expr_calculate_pexpr_y_equals(e);
+    case E_UNEQUAL:
+        return expr_calculate_pexpr_y_unequals(e);
+    case E_LTH:
+    case E_LEQ:
+    case E_GTH:
+    case E_GEQ:
+        return expr_calculate_pexpr_y_comp(e);
+    default:
+        // TODO
+        perror("Unhandled type - expr_calculate_pexpr_both");
+        return NULL;
+    }
+}
+
+/*
+ * calculate, when expr will evaluate to yes
+ */
+struct pexpr * expr_calculate_pexpr_y(struct expr *e){
+    if (!e)
+        return NULL;
+
+    switch (e->type) {
+    case E_SYMBOL:
+        return pexf(e->left.sym->fexpr_y);
+    case E_AND:
+        return expr_calculate_pexpr_y_and(e->left.expr, e->right.expr);
+    case E_OR:
+        return expr_calculate_pexpr_y_or(e->left.expr, e->right.expr);
+    case E_NOT:
+        return expr_calculate_pexpr_y_not(e->left.expr);
+    case E_EQUAL:
+        return expr_calculate_pexpr_y_equals(e);
+    case E_UNEQUAL:
+        return expr_calculate_pexpr_y_unequals(e);
+    case E_LTH:
+    case E_LEQ:
+    case E_GTH:
+    case E_GEQ:
+        return expr_calculate_pexpr_y_comp(e);
+    default:
+        perror("Unhandled type - expr_calculate_pexpr_y");
+        return NULL;
+    }
+}
+
+/*
+ * calculate, when expr will evaluate to mod
+ */
+struct pexpr * expr_calculate_pexpr_m(struct expr *e){
+    if (!e)
+        return NULL;
+
+    if (!expr_can_evaluate_to_mod(e))
+        return pexf(const_false);
+
+    switch (e->type) {
+    case E_SYMBOL:
+        return pexf(e->left.sym->fexpr_m);
+    case E_AND:
+        return expr_calculate_pexpr_m_and(e->left.expr, e->right.expr);
+    case E_OR:
+        return expr_calculate_pexpr_m_or(e->left.expr, e->right.expr);
+    case E_NOT:
+        return expr_calculate_pexpr_m_not(e->left.expr);
+    default:
+        perror("Trying to evaluate to mod.");
+        return NULL;
+    }
+}
+
+/*
+ * calculate, when expr of type AND will evaluate to yes
+ * A && B
+ */
+struct pexpr * expr_calculate_pexpr_y_and(struct expr *a, struct expr *b)
+{
+    return pexpr_and(expr_calculate_pexpr_y(a), expr_calculate_pexpr_y(b));
+}
+
+/*
+ * calculate, when expr of type AND will evaluate to mod
+ * (A || A_m) && (B || B_m) && !(A && B)
+ */
+struct pexpr * expr_calculate_pexpr_m_and(struct expr *a, struct expr *b)
+{
+    struct pexpr *topright = pexpr_not(pexpr_and(expr_calculate_pexpr_y(a), expr_calculate_pexpr_y(b)));
+    struct pexpr *ll_left = pexpr_or(expr_calculate_pexpr_y(a), expr_calculate_pexpr_m(a));
+    struct pexpr *ll_right = pexpr_or(expr_calculate_pexpr_y(b), expr_calculate_pexpr_m(b));
+    struct pexpr *topleft = pexpr_and(ll_left, ll_right);
+
+    return pexpr_and(topleft, topright);
+}
+
+/*
+ * calculate, when expr of type AND will evaluate to mod or yes
+ * (A || A_m) && (B || B_m)
+ */
+struct pexpr * expr_calculate_pexpr_both_and(struct expr *a, struct expr *b)
+{
+    struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a), expr_calculate_pexpr_m(a));
+    struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b), expr_calculate_pexpr_m(b));
+    return pexpr_and(left, right);
+}
+
+/*
+ * calculate, when expr of type OR will evaluate to yes
+ * A || B
+ */
+struct pexpr * expr_calculate_pexpr_y_or(struct expr *a, struct expr *b)
+{
+    return pexpr_or(expr_calculate_pexpr_y(a), expr_calculate_pexpr_y(b));
+}
+
+/*
+ * calculate, when expr of type OR will evaluate to mod
+ * (A_m || B_m) && !A && !B
+ */
+struct pexpr * expr_calculate_pexpr_m_or(struct expr *a, struct expr *b)
+{
+    struct pexpr *topright = pexpr_not(expr_calculate_pexpr_y(b));
+    struct pexpr *lowerleft = pexpr_or(expr_calculate_pexpr_m(a), expr_calculate_pexpr_m(b));
+    struct pexpr *topleft = pexpr_and(lowerleft, pexpr_not(expr_calculate_pexpr_y(a)));
+
+    return pexpr_and(topleft, topright);
+}
+
+/*
+ * calculate, when expr of type OR will evaluate to mod or yes
+ * (A_m || A || B_m || B)
+ */
+struct pexpr * expr_calculate_pexpr_both_or(struct expr *a, struct expr *b)
+{
+    struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a), expr_calculate_pexpr_m(a));
+    struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b), expr_calculate_pexpr_m(b));
+    return pexpr_or(left, right);
+}
+
+/*
+ * calculate, when expr of type NOT will evaluate to yes
+ * !(A || A_m)
+ */
+struct pexpr * expr_calculate_pexpr_y_not(struct expr * e)
+{
+    return pexpr_not(pexpr_or(expr_calculate_pexpr_y(e), expr_calculate_pexpr_m(e)));
+}
+
+/*
+ * calculate, when expr of type NOT will evaluate to mod
+ * A_m
+ */
+struct pexpr * expr_calculate_pexpr_m_not(struct expr * e)
+{
+    return expr_calculate_pexpr_m(e);
+}
+
+static struct pexpr * equiv_pexpr(struct pexpr *a, struct pexpr *b)
+{
+    struct pexpr *yes = pexpr_and(a, b);
+    struct pexpr *not = pexpr_and(pexpr_not(a), pexpr_not(b));
+
+    return pexpr_or(yes, not);
+}
+
+/*
+ * create the fexpr of a non-boolean symbol for a specific value
+ */
+struct fexpr * sym_create_nonbool_fexpr(struct symbol *sym, char *value)
+{
+
+    if (!strcmp(value, "")) {
+        if (sym->type == S_STRING)
+            return sym->nb_vals->head->next->elem;
+        else
+            return sym->nb_vals->head->elem;
+    }
+
+    struct fexpr *e = sym_get_nonbool_fexpr(sym, value);
+
+    /* fexpr already exists */
+    if (e != NULL)
+        return e;
+
+    char *s = value;
+    if (sym->type == S_INT && !string_is_number(value)) {
+        struct symbol *tmp = sym_find(value);
+
+        if (tmp != NULL)
+            s = (char *) tmp->curr.val;
+    } else if (sym->type == S_HEX && !string_is_hex(value)) {
+        struct symbol *tmp = sym_find(value);
+
+        if (tmp != NULL)
+            s = (char *) tmp->curr.val;
+    } else if (sym->type == S_STRING) {
+        struct symbol *tmp = sym_find(value);
+
+        if (tmp != NULL)
+            s = (char *) tmp->curr.val;
+    }
+
+    if (!strcmp(s, "")) {
+        if (sym->type == S_STRING)
+            return sym->nb_vals->head->next->elem;
+        else
+            return sym->nb_vals->head->elem;
+    }
+
+    e = sym_get_nonbool_fexpr(sym, s);
+    if (e != NULL)
+        return e;
+
+    e = fexpr_create(sat_variable_nr++, FE_NONBOOL, sym->name);
+    e->sym = sym;
+    str_append(&e->name, "=");
+    str_append(&e->name, s);
+    e->nb_val = str_new();
+    str_append(&e->nb_val, s);
+
+    fexpr_list_add(sym->nb_vals, e);
+    fexpr_add_to_satmap(e);
+
+    return e;
+}
+
+/*
+ * return the fexpr of a non-boolean symbol for a specific value, NULL if non-existent
+ */
+struct fexpr * sym_get_nonbool_fexpr(struct symbol *sym, char *value)
+{
+    struct fexpr_node *e;
+    fexpr_list_for_each(e, sym->nb_vals) {
+        if (strcmp(str_get(&e->elem->nb_val), value) == 0)
+            return e->elem;
+    }
+
+    return NULL;
+}
+
+/*
+ * return the fexpr of a non-boolean symbol for a specific value, if it exists
+ * otherwise create it
+ */
+struct fexpr * sym_get_or_create_nonbool_fexpr(struct symbol *sym, char *value)
+{
+    struct fexpr *e = sym_get_nonbool_fexpr(sym, value);
+
+    if (e != NULL)
+        return e;
+    else
+        return sym_create_nonbool_fexpr(sym, value);
+}
+
+/*
+ * calculate, when expr of type EQUAL will evaluate to yes
+ */
+struct pexpr * expr_calculate_pexpr_y_equals(struct expr *e)
+{
+    /* comparing 2 tristate constants */
+    if (sym_is_tristate_constant(e->left.sym) && sym_is_tristate_constant(e->right.sym))
+        return e->left.sym == e->right.sym ? pexf(const_true) : pexf(const_false);
+
+    /* comparing 2 nonboolean constants */
+    if (sym_is_nonbool_constant(e->left.sym) && sym_is_nonbool_constant(e->right.sym))
+        return strcmp(e->left.sym->name, e->right.sym->name) == 0 ? pexf(const_true) : pexf(const_false);
+
+    /* comparing 2 boolean/tristate incl. yes/mod/no constants */
+    if (sym_is_bool_or_triconst(e->left.sym) && sym_is_bool_or_triconst(e->right.sym)) {
+        struct pexpr *yes = equiv_pexpr(pexf(e->left.sym->fexpr_y), pexf(e->right.sym->fexpr_y));
+        struct pexpr *mod = equiv_pexpr(pexf(e->left.sym->fexpr_m), pexf(e->right.sym->fexpr_m));
+
+        return pexpr_and(yes, mod);
+    }
+
+    /* comparing nonboolean with a constant */
+    if (sym_is_nonboolean(e->left.sym) && sym_is_nonbool_constant(e->right.sym)) {
+        return pexf(sym_get_or_create_nonbool_fexpr(e->left.sym, e->right.sym->name));
+    }
+    if (sym_is_nonbool_constant(e->left.sym) && sym_is_nonboolean(e->right.sym))
+        return pexf(sym_get_or_create_nonbool_fexpr(e->right.sym, e->left.sym->name));
+
+    /* comparing nonboolean with tristate constant, will never be true */
+    if (sym_is_nonboolean(e->left.sym) && sym_is_tristate_constant(e->right.sym))
+        return pexf(const_false);
+    if (sym_is_tristate_constant(e->left.sym) && sym_is_nonboolean(e->right.sym))
+        return pexf(const_false);
+
+    /* comparing 2 nonboolean symbols */
+    if (sym_is_nonboolean(e->left.sym) && sym_is_nonboolean(e->right.sym)) {
+        struct pexpr *c = pexf(const_false);
+        struct fexpr_node *node1, *node2;
+        struct fexpr *e1, *e2;
+        for (node1 = e->left.sym->nb_vals->head->next; node1 != NULL; node1 = node1->next) {
+            e1 = node1->elem;
+            for (node2 = e->right.sym->nb_vals->head->next; node2 != NULL; node2 = node2->next) {
+                e2 = node2->elem;
+                if (!strcmp(str_get(&e1->nb_val), str_get(&e2->nb_val))) {
+                    c = pexpr_or(c, pexpr_and(pexf(e1), pexf(e2)));
+                    break;
+                }
+            }
+        }
+        return c;
+    }
+
+    /* comparing boolean item with nonboolean constant, will never be true */
+    if (sym_is_tristate_constant(e->left.sym) && sym_is_nonbool_constant(e->right.sym))
+        return pexf(const_false);
+    if (sym_is_nonbool_constant(e->left.sym) && sym_is_tristate_constant(e->right.sym))
+        return pexf(const_false);
+
+    /* comparing symbol of type unknown with tristate constant */
+    if (e->left.sym->type == S_UNKNOWN && sym_is_tristate_constant(e->right.sym))
+        return pexf(const_false);
+    if (sym_is_tristate_constant(e->left.sym) && e->right.sym->type == S_UNKNOWN)
+        return pexf(const_false);
+
+    /* any other comparison is not supported and should not be executed */
+    perror("Unsupported equality.");
+    print_expr(":", e, 0);
+
+    return pexf(const_false);
+}
+
+/*
+ * transform an UNEQUAL into a Not(EQUAL)
+ */
+struct pexpr * expr_calculate_pexpr_y_unequals(struct expr *e)
+{
+    return pexpr_not(expr_calculate_pexpr_y_equals(e));
+}
+
+struct pexpr * expr_calculate_pexpr_y_comp(struct expr *e)
+{
+    if (!e)
+        return NULL;
+
+    switch (e->type) {
+    case E_LTH:
+    case E_LEQ:
+    case E_GTH:
+    case E_GEQ:
+        /* compare non-Boolean symbol with constant */
+        if (sym_is_nonboolean(e->left.sym) &&
+            e->right.sym->type == S_UNKNOWN &&
+            string_is_number(e->right.sym->name)
+        ) {
+            return expr_eval_unequal_nonbool_const(e->left.sym, e->right.sym, e->type);
+        }
+        if (sym_is_nonboolean(e->right.sym) &&
+            e->left.sym->type == S_UNKNOWN &&
+            string_is_number(e->left.sym->name)
+        ) {
+            return expr_eval_unequal_nonbool_const(e->right.sym, e->left.sym, e->type);
+        }
+
+        /* compare 2 Boolean symbols */
+        if (sym_is_boolean(e->left.sym) && sym_is_boolean(e->right.sym))
+            return expr_eval_unequal_bool(e->left.sym, e->right.sym, e->type);
+
+        return pexf(const_false);
+    default:
+        perror("Unhandled type - expr_calculate_pexpr_y_comp");
+        return NULL;
+    }
+}
+
+/*
+ * macro to create a pexpr of type AND
+ */
+struct pexpr * pexpr_and(struct pexpr *a, struct pexpr *b)
+{
+    /* simplifications:
+     * expr && False -> False
+     * expr && True  -> expr
+     * expr && expr  -> expr
+     */
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_false)
+        return a;
+
+    if (b->type == PE_SYMBOL && b->left.fexpr == const_false)
+        return b;
+
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_true)
+        return b;
+
+    if (b->type == PE_SYMBOL && b->left.fexpr == const_true)
+        return a;
+
+    /* A && A -> A */
+    if (pexpr_eq(a,b))
+        return a;
+
+    /* (A && B) && C -> A && B if B == C */
+    if (a->type == PE_AND && pexpr_eq(a->right.pexpr, b))
+        return a;
+    /* A && (B && C) -> B && C if A == B */
+    if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr))
+        return b;
+
+    /* (A || B) && (C || D) -> A || (B && D) if A == C */
+    if (a->type == PE_OR && b->type == PE_OR && (
+        pexpr_eq(a->left.pexpr, b->left.pexpr)
+    ))
+        return pexpr_or(a->left.pexpr,
+                pexpr_and(a->right.pexpr, b->right.pexpr));
+    /* (A || B) && (C || D) -> B || (A && C) if B == D */
+    if (a->type == PE_OR && b->type == PE_OR && (
+        pexpr_eq(a->right.pexpr, b->right.pexpr)
+    ))
+        return pexpr_or(a->right.pexpr,
+                pexpr_and(a->left.pexpr, b->left.pexpr));
+    /* (A || B) && (C || D) -> A || (B && C) if A == D */
+    if (a->type == PE_OR && b->type == PE_OR && (
+        pexpr_eq(a->left.pexpr, b->right.pexpr)
+    ))
+        return pexpr_or(a->left.pexpr,
+                pexpr_and(a->right.pexpr, b->left.pexpr));
+    /* (A || B) && (C || D) -> B || (A && D) if B == C */
+    if (a->type == PE_OR && b->type == PE_OR && (
+        pexpr_eq(a->right.pexpr, b->left.pexpr)
+    ))
+        return pexpr_or(a->right.pexpr,
+                pexpr_and(a->left.pexpr, b->right.pexpr));
+
+    struct pexpr *e = xcalloc(1, sizeof(*e));
+    e->type = PE_AND;
+    e->left.pexpr = a;
+    e->right.pexpr = b;
+
+    return e;
+}
+
+/*
+ * macro to create a pexpr of type OR
+ */
+struct pexpr * pexpr_or(struct pexpr *a, struct pexpr *b)
+{
+    /* simplifications:
+     * expr || False -> expr
+     * expr || True  -> True
+     * expr || expr  -> expr
+     */
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_false)
+        return b;
+
+    if (b->type == PE_SYMBOL && b->left.fexpr == const_false)
+        return a;
+
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_true)
+        return a;
+
+    if (b->type == PE_SYMBOL && b->left.fexpr == const_true)
+        return b;
+
+    /* A || A -> A */
+    if (pexpr_eq(a,b))
+        return a;
+
+    /* A || (B && C) -> A if (A == B || A == C) */
+    if (b->type == PE_AND && (
+        pexpr_eq(a, b->left.pexpr) || pexpr_eq(a, b->right.pexpr)
+    ))
+        return a;
+    /* (A && B) || C -> C if (A == C || B == C) */
+    if (a->type == PE_AND && (
+        pexpr_eq(a->left.pexpr, b) || pexpr_eq(a->right.pexpr, b)
+    ))
+        return b;
+
+    /* -A || B -> True if A == B */
+    if (a->type == PE_NOT && pexpr_eq(a->left.pexpr, b))
+        return pexf(const_true);
+    /* A || -B -> True if A == B */
+    if (b->type == PE_NOT && pexpr_eq(a, b->left.pexpr))
+        return pexf(const_true);
+
+    /* (A && B) || (C && D) -> A && (B || D) if (A == C) */
+    if (a->type == PE_AND && b->type == PE_AND &&
+        pexpr_eq(a->left.pexpr, b->left.pexpr)
+    )
+        return pexpr_and(a->left.pexpr,
+                 pexpr_or(a->right.pexpr, b->right.pexpr));
+    /* (A && B) || (C && D) -> B && (A || C) if (B == D) */
+    if (a->type == PE_AND && b->type == PE_AND &&
+        pexpr_eq(a->right.pexpr, b->right.pexpr)
+    )
+        return pexpr_and(a->right.pexpr,
+                 pexpr_or(a->left.pexpr, b->left.pexpr));
+    /* (A && B) || (C && D) -> A && (B || C) if (A == D) */
+    if (a->type == PE_AND && b->type == PE_AND &&
+        pexpr_eq(a->left.pexpr, b->right.pexpr)
+    )
+        return pexpr_and(a->left.pexpr,
+                 pexpr_or(a->right.pexpr, b->left.pexpr));
+    /* (A && B) || (C && D) -> B && (A || D) if (B == C) */
+    if (a->type == PE_AND && b->type == PE_AND &&
+        pexpr_eq(a->right.pexpr, b->left.pexpr)
+    )
+        return pexpr_and(a->right.pexpr,
+                 pexpr_or(a->left.pexpr, b->right.pexpr));
+
+    /* (A && B) || (C || D) -> C || D if
+     * A == C || A == D || B == C || B == D */
+    if (a->type == PE_AND && b->type == PE_OR && (
+        pexpr_eq(a->left.pexpr, b->left.pexpr) ||
+        pexpr_eq(a->left.pexpr, b->right.pexpr) ||
+        pexpr_eq(a->right.pexpr, b->left.pexpr) ||
+        pexpr_eq(a->right.pexpr, b->right.pexpr)
+    ))
+        return b;
+    /* (C || D) || (A && B) -> C || D if
+     * A == C || A == D || B == C || B == D */
+    if (a->type == PE_OR && b->type == PE_AND && (
+        pexpr_eq(a->left.pexpr, b->left.pexpr) ||
+        pexpr_eq(a->left.pexpr, b->right.pexpr) ||
+        pexpr_eq(a->right.pexpr, b->left.pexpr) ||
+        pexpr_eq(a->right.pexpr, b->right.pexpr)
+    ))
+        return a;
+
+    struct pexpr *e = xcalloc(1, sizeof(*e));
+    e->type = PE_OR;
+    e->left.pexpr = a;
+    e->right.pexpr = b;
+
+    return e;
+}
+
+/*
+ * macro to create a pexpr of type NOT
+ */
+struct pexpr * pexpr_not(struct pexpr *a)
+{
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_false)
+        return pexf(const_true);
+    if (a->type == PE_SYMBOL && a->left.fexpr == const_true)
+        return pexf(const_false);
+
+    /* eliminate double negation */
+    if (a->type == PE_NOT)
+        return a->left.pexpr;
+
+    /* De Morgan */
+    if (a->type == PE_AND) {
+        struct pexpr *e = xcalloc(1, sizeof(*e));
+        e->type = PE_OR;
+        e->left.pexpr = pexpr_not(a->left.pexpr);
+        e->right.pexpr = pexpr_not(a->right.pexpr);
+        return e;
+    }
+    if (a->type == PE_OR) {
+        struct pexpr *e = xcalloc(1, sizeof(*e));
+        e->type = PE_AND;
+        e->left.pexpr = pexpr_not(a->left.pexpr);
+        e->right.pexpr = pexpr_not(a->right.pexpr);
+        return e;
+    }
+
+    struct pexpr *e = xcalloc(1, sizeof(*e));
+    e->type = PE_NOT;
+    e->left.pexpr = a;
+    return e;
+}
+
+/*
+ * macro to construct a pexpr for "A implies B"
+ */
+struct pexpr * pexpr_implies(struct pexpr *a, struct pexpr *b)
+{
+    /* A => B -> True if A == B */
+    if (pexpr_eq(a, b))
+        return pexf(const_true);
+
+    /* (A => B && C) -> (A => C) if A == B */
+    if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr))
+        return pexpr_implies(a, b->right.pexpr);
+    /* (A => B && C) -> (A => B) if A == C */
+    if (b->type == PE_AND && pexpr_eq(a, b->right.pexpr))
+        return pexpr_implies(a, b->left.pexpr);
+
+    /* (A => B || C) -> True if (A == B || A == C) */
+    if (b->type == PE_OR && (
+        pexpr_eq(a, b->left.pexpr) || pexpr_eq(a, b->right.pexpr)
+    ))
+        return pexf(const_true);
+
+    /* (A && B => C) -> True if (A == C || B == C) */
+    if (a->type == PE_AND && (
+        pexpr_eq(a->left.pexpr, b) || pexpr_eq(a->right.pexpr, b)
+    ))
+        return pexf(const_true);
+
+    return pexpr_or(pexpr_not(a), b);
+}
+
+/*
+ * check whether a pexpr is in CNF
+ */
+bool pexpr_is_cnf(struct pexpr *e)
+{
+    if (!e)
+        return false;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        return true;
+    case PE_AND:
+        return false;
+    case PE_OR:
+        return pexpr_is_cnf(e->left.pexpr) && pexpr_is_cnf(e->right.pexpr);
+    case PE_NOT:
+        return e->left.pexpr->type == PE_SYMBOL;
+    }
+
+    return false;
+}
+
+/*
+ * check whether a pexpr is in NNF
+ */
+bool pexpr_is_nnf(struct pexpr *e)
+{
+    if (!e)
+        return false;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        return true;
+    case PE_AND:
+    case PE_OR:
+        return pexpr_is_nnf(e->left.pexpr) && pexpr_is_nnf(e->right.pexpr);
+    case PE_NOT:
+        return e->left.pexpr->type == PE_SYMBOL;
+    }
+
+    return false;
+}
+
+/*
+ * return fexpr_both for a symbol
+ */
+struct pexpr * sym_get_fexpr_both(struct symbol *sym)
+{
+    return sym->type == S_TRISTATE ? pexpr_or(pexf(sym->fexpr_m), pexf(sym->fexpr_y)) : pexf(sym->fexpr_y);
+}
+
+/*
+ * return fexpr_sel_both for a symbol
+ */
+struct pexpr * sym_get_fexpr_sel_both(struct symbol *sym)
+{
+    if (!sym->rev_dep.expr)
+        return pexf(const_false);
+
+    return sym->type == S_TRISTATE ? pexpr_or(pexf(sym->fexpr_sel_m), pexf(sym->fexpr_sel_y)) : pexf(sym->fexpr_sel_y);
+}
+
+/*
+ * check, if the fexpr is a symbol, a True/False-constant, a literal symbolizing a non-boolean or a choice symbol
+ */
+bool fexpr_is_symbol(struct fexpr *e)
+{
+    return e->type == FE_SYMBOL || e->type == FE_FALSE || e->type == FE_TRUE || e->type == FE_NONBOOL || e->type == FE_CHOICE || e->type == FE_SELECT || e->type == FE_NPC;
+}
+
+/*
+ * check whether a pexpr is a symbol or a negated symbol
+ */
+bool pexpr_is_symbol(struct pexpr *e)
+{
+    return e->type == PE_SYMBOL || (e->type == PE_NOT && e->left.pexpr->type == PE_SYMBOL);
+}
+
+/*
+ * check whether the fexpr is a constant (true/false)
+ */
+bool fexpr_is_constant(struct fexpr *e)
+{
+    return e == const_true || e == const_false;
+}
+
+/*
+ * add a fexpr to the satmap
+ */
+void fexpr_add_to_satmap(struct fexpr *e)
+{
+    if (e->satval >= satmap_size) {
+        satmap = xrealloc(satmap, satmap_size * 2 * sizeof(*satmap));
+        satmap_size *= 2;
+    }
+
+    satmap[e->satval] = *e;
+}
+
+/*
+ * print a fexpr
+ */
+void fexpr_print(char *tag, struct fexpr *e)
+{
+    if (!e)
+        return;
+
+    printf("%s: %s\n", tag, str_get(&e->name));
+}
+
+/*
+ * write an fexpr into a string (format needed for testing)
+ */
+void fexpr_as_char(struct fexpr *e, struct gstr *s)
+{
+    if (!e)
+        return;
+
+    switch (e->type) {
+    case FE_SYMBOL:
+    case FE_CHOICE:
+    case FE_SELECT:
+    case FE_NPC:
+    case FE_NONBOOL:
+        str_append(s, "definedEx(");
+        str_append(s, str_get(&e->name));
+        str_append(s, ")");
+        return;
+    case FE_FALSE:
+        str_append(s, "0");
+        return;
+    case FE_TRUE:
+        str_append(s, "1");
+        return;
+    default:
+        return;
+    }
+}
+
+/*
+ * write a pexpr into a string
+ */
+void pexpr_as_char(struct pexpr *e, struct gstr *s, int parent)
+{
+    if (!e)
+        return;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        if (e->left.fexpr == const_false) {
+            str_append(s, "0");
+            return;
+        }
+        if (e->left.fexpr == const_true) {
+            str_append(s, "1");
+            return;
+        }
+        str_append(s, "definedEx(");
+        str_append(s, str_get(&e->left.fexpr->name));
+        str_append(s, ")");
+        return;
+    case PE_AND:
+        /* need this hack for the FeatureExpr parser */
+        if (parent != PE_AND)
+            str_append(s, "(");
+        pexpr_as_char(e->left.pexpr, s, PE_AND);
+        str_append(s, " && ");
+        pexpr_as_char(e->right.pexpr, s, PE_AND);
+        if (parent != PE_AND)
+            str_append(s, ")");
+        return;
+    case PE_OR:
+        if (parent != PE_OR)
+            str_append(s, "(");
+        pexpr_as_char(e->left.pexpr, s, PE_OR);
+        str_append(s, " || ");
+        pexpr_as_char(e->right.pexpr, s, PE_OR);
+        if (parent != PE_OR)
+            str_append(s, ")");
+        return;
+    case PE_NOT:
+        str_append(s, "!");
+        pexpr_as_char(e->left.pexpr, s, PE_NOT);
+        return;
+    }
+}
+
+/*
+ * write a pexpr into a string
+ */
+void pexpr_as_char_short(struct pexpr *e, struct gstr *s, int parent)
+{
+    if (!e)
+        return;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        str_append(s, str_get(&e->left.fexpr->name));
+        return;
+    case PE_AND:
+        /* need this hack for the FeatureExpr parser */
+        if (parent != PE_AND)
+            str_append(s, "(");
+        pexpr_as_char_short(e->left.pexpr, s, PE_AND);
+        str_append(s, " && ");
+        pexpr_as_char_short(e->right.pexpr, s, PE_AND);
+        if (parent != PE_AND)
+            str_append(s, ")");
+        return;
+    case PE_OR:
+        if (parent != PE_OR)
+            str_append(s, "(");
+        pexpr_as_char_short(e->left.pexpr, s, PE_OR);
+        str_append(s, " || ");
+        pexpr_as_char_short(e->right.pexpr, s, PE_OR);
+        if (parent != PE_OR)
+            str_append(s, ")");
+        return;
+    case PE_NOT:
+        str_append(s, "!");
+        pexpr_as_char_short(e->left.pexpr, s, PE_NOT);
+        return;
+    }
+}
+
+/*
+ * check whether a pexpr contains a specific fexpr
+ */
+bool pexpr_contains_fexpr(struct pexpr *e, struct fexpr *fe)
+{
+    if (!e)
+        return false;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        return e->left.fexpr->satval == fe->satval;
+    case PE_AND:
+    case PE_OR:
+        return pexpr_contains_fexpr(e->left.pexpr, fe) ||
+            pexpr_contains_fexpr(e->right.pexpr, fe);
+    case PE_NOT:
+        return e->left.pexpr->left.fexpr->satval == fe->satval;
+    }
+
+    return false;
+}
+
+/*
+ * init list of fexpr
+ */
+struct fexpr_list * fexpr_list_init()
+{
+    struct fexpr_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of fexpr_list
+ */
+struct fexl_list * fexl_list_init()
+{
+    struct fexl_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of pexpr
+ */
+struct pexpr_list * pexpr_list_init()
+{
+    struct pexpr_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of symbol_fix
+ */
+struct sfix_list * sfix_list_init(void)
+{
+    struct sfix_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of symbol_fix
+ */
+struct sfl_list * sfl_list_init(void)
+{
+    struct sfl_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of symbol_dvalue
+ */
+struct sdv_list * sdv_list_init(void)
+{
+    struct sdv_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of symbols
+ */
+struct sym_list * sym_list_init(void)
+{
+    struct sym_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of default_maps
+ */
+struct defm_list * defm_list_init(void)
+{
+    struct defm_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * init list of properties
+ */
+struct prop_list *prop_list_init(void)
+{
+    struct prop_list *list = xcalloc(1, sizeof(*list));
+    list->head = NULL;
+    list->tail = NULL;
+    list->size = 0;
+
+    return list;
+}
+
+/*
+ * add element to tail of a fexpr_list
+ */
+void fexpr_list_add(struct fexpr_list *list, struct fexpr *fe)
+{
+    struct fexpr_node *node = xcalloc(1, sizeof(*node));
+    node->elem = fe;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a fexl_list
+ */
+void fexl_list_add(struct fexl_list *list, struct fexpr_list *elem)
+{
+    struct fexl_node *node = xcalloc(1, sizeof(*node));
+    node->elem = elem;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a pexpr_list
+ */
+void pexpr_list_add(struct pexpr_list *list, struct pexpr *e)
+{
+    struct pexpr_node *node = xcalloc(1, sizeof(*node));
+    node->elem = e;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a sfix_list
+ */
+void sfix_list_add(struct sfix_list *list, struct symbol_fix *fix)
+{
+    struct sfix_node *node = xcalloc(1, sizeof(*node));
+    node->elem = fix;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a sfl_list
+ */
+void sfl_list_add(struct sfl_list *list, struct sfix_list *elem)
+{
+    struct sfl_node *node = xcalloc(1, sizeof(*node));
+    node->elem = elem;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a sdv_list
+ */
+void sdv_list_add(struct sdv_list *list, struct symbol_dvalue *sdv)
+{
+    struct sdv_node *node = xcalloc(1, sizeof(*node));
+    node->elem = sdv;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a sym_list
+ */
+void sym_list_add(struct sym_list *list, struct symbol *sym)
+{
+    struct sym_node *node = xcalloc(1, sizeof(*node));
+    node->elem = sym;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a defm_list
+ */
+void defm_list_add(struct defm_list *list, struct default_map *map)
+{
+    struct defm_node *node = xcalloc(1, sizeof(*node));
+    node->elem = map;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * add element to tail of a prop_list
+ */
+void prop_list_add(struct prop_list *list, struct property *prop)
+{
+    struct prop_node *node = xcalloc(1, sizeof(*node));
+    node->elem = prop;
+
+    if (list->size == 0) {
+        list->head = node;
+        list->tail = node;
+    } else {
+        node->prev = list->tail;
+        list->tail = node;
+        node->prev->next = node;
+    }
+
+    list->size++;
+}
+
+/*
+ * delete an element from a fexpr_list
+ */
+void fexpr_list_delete(struct fexpr_list *list, struct fexpr_node *node)
+{
+    if (list->size == 0 || node == NULL)
+        return;
+
+    if (node == list->head)
+        list->head = node->next;
+    else
+        node->prev->next = node->next;
+
+    if (node == list->tail)
+        list->tail = node->prev;
+    else
+        node->next->prev = node->prev;
+
+    list->size--;
+    free(node);
+}
+
+/*
+ * delete an element from a fexpr_list
+ */
+void sfix_list_delete(struct sfix_list *list, struct sfix_node *node)
+{
+    if (list->size == 0 || node == NULL)
+        return;
+
+    if (node == list->head)
+        list->head = node->next;
+    else
+        node->prev->next = node->next;
+
+    if (node == list->tail)
+        list->tail = node->prev;
+    else
+        node->next->prev = node->prev;
+
+    list->size--;
+    free(node);
+}
+
+/*
+ * delete an element from a fexpr_list
+ */
+void pexpr_list_delete(struct pexpr_list *list, struct pexpr_node *node)
+{
+    if (list->size == 0 || node == NULL)
+        return;
+
+    if (node == list->head)
+        list->head = node->next;
+    else
+        node->prev->next = node->next;
+
+    if (node == list->tail)
+        list->tail = node->prev;
+    else
+        node->next->prev = node->prev;
+
+    list->size--;
+    free(node);
+}
+
+/*
+ * delete an element from a fexl_list
+ */
+void fexl_list_delete(struct fexl_list *list, struct fexl_node *node)
+{
+    if (list->size == 0 || node == NULL)
+        return;
+
+    if (node == list->head)
+        list->head = node->next;
+    else
+        node->prev->next = node->next;
+
+    if (node == list->tail)
+        list->tail = node->prev;
+    else
+        node->next->prev = node->prev;
+
+    list->size--;
+    free(node);
+}
+
+/*
+ * delete the first occurence of elem in an fexl_list
+ */
+void fexl_list_delete_elem(struct fexl_list *list, struct fexpr_list *elem)
+{
+    struct fexl_node *node, *to_delete = NULL;
+    fexl_list_for_each(node, list) {
+        if (node->elem == elem) {
+            to_delete = node;
+            break;
+        }
+    }
+
+    if (to_delete != NULL)
+        fexl_list_delete(list, to_delete);
+}
+
+/*
+ * make a shallow copy of a fexpr_list
+ */
+struct fexpr_list * fexpr_list_copy(struct fexpr_list *list)
+{
+    struct fexpr_list *ret = fexpr_list_init();
+    struct fexpr_node *node;
+    fexpr_list_for_each(node, list)
+        fexpr_list_add(ret, node->elem);
+
+    return ret;
+}
+
+/*
+ * make a shallow copy of a fexl_list
+ */
+struct fexl_list * fexl_list_copy(struct fexl_list *list)
+{
+    struct fexl_list *ret = fexl_list_init();
+    struct fexl_node *node;
+    fexl_list_for_each(node, list)
+        fexl_list_add(ret, node->elem);
+
+    return ret;
+}
+
+/*
+ * make a shallow copy of a sdv_list
+ */
+struct sdv_list * sdv_list_copy(struct sdv_list *list)
+{
+    struct sdv_list *ret = sdv_list_init();
+    struct sdv_node *node;
+    sdv_list_for_each(node, list)
+        sdv_list_add(ret, node->elem);
+
+
+    return ret;
+}
+
+/*
+ * make a shallow copy of a sfix_list
+ */
+struct sfix_list * sfix_list_copy(struct sfix_list *list)
+{
+    struct sfix_list *ret = sfix_list_init();
+    struct sfix_node *node;
+    sfix_list_for_each(node, list)
+        sfix_list_add(ret, node->elem);
+
+    return ret;
+}
+
+/*
+ * print a fexpr_list
+ */
+void fexpr_list_print(char *title, struct fexpr_list *list)
+{
+    struct fexpr_node *node;
+    printf("%s: [", title);
+
+    fexpr_list_for_each(node, list) {
+        printf("%s", str_get(&node->elem->name));
+        if (node->next != NULL)
+            printf(", ");
+    }
+
+    printf("]\n");
+}
+
+/*
+ * print a fexl_list
+ */
+void fexl_list_print(char *title, struct fexl_list *list)
+{
+    struct fexl_node *node;
+    printf("%s:\n", title);
+
+    fexl_list_for_each(node, list)
+        fexpr_list_print(":", node->elem);
+}
+
+/*
+ * print a pexpr_list
+ */
+void pexpr_list_print(char *title, struct pexpr_list *list)
+{
+    struct pexpr_node *node;
+    printf("%s: [", title);
+
+    pexpr_list_for_each(node, list) {
+        pexpr_print_util(node->elem, -1);
+        if (node->next != NULL)
+            printf(", ");
+    }
+
+    printf("]\n");
+}
+
+/*
+ * free an fexpr_list
+ */
+void fexpr_list_free(struct fexpr_list *list)
+{
+    struct fexpr_node *node = list->head, *tmp;
+
+    while (node != NULL) {
+        tmp = node->next;
+        free(node);
+        node = tmp;
+    }
+
+    free(list);
+}
+
+/*
+ * free an fexl_list
+ */
+void fexl_list_free(struct fexl_list *list){
+    struct fexl_node *node = list->head, *tmp;
+
+    while (node != NULL) {
+        tmp = node->next;
+        free(node);
+        node = tmp;
+    }
+
+    free(list);
+}
+
+/*
+ * free a sdv_list
+ */
+void sdv_list_free(struct sdv_list *list)
+{
+    struct sdv_node *node = list->head, *tmp;
+
+    while (node != NULL) {
+        tmp = node->next;
+        free(node);
+        node = tmp;
+    }
+
+    free(list);
+}
+
+/*
+ * simplify a pexpr in-place
+ *     pexpr && False -> False
+ *     pexpr && True  -> pexpr
+ *     pexpr || False -> pexpr
+ *     pexpr || True  -> True
+ */
+static struct pexpr * pexpr_eliminate_yn(struct pexpr *e)
+{
+    struct pexpr *tmp;
+
+    if (e) switch (e->type) {
+    case PE_AND:
+        e->left.pexpr = pexpr_eliminate_yn(e->left.pexpr);
+        e->right.pexpr = pexpr_eliminate_yn(e->right.pexpr);
+        if (e->left.pexpr->type == PE_SYMBOL) {
+            if (e->left.pexpr->left.fexpr == const_false) {
+                pexpr_free(e->left.pexpr);
+                pexpr_free(e->right.pexpr);
+                e->type = PE_SYMBOL;
+                e->left.fexpr = const_false;
+                e->right.pexpr = NULL;
+                return e;
+            } else if (e->left.pexpr->left.fexpr == const_true) {
+                free(e->left.pexpr);
+                tmp = e->right.pexpr;
+                *e = *(e->right.pexpr);
+                free(tmp);
+                return e;
+            }
+        }
+        if (e->right.pexpr->type == PE_SYMBOL) {
+            if (e->right.pexpr->left.fexpr == const_false) {
+                pexpr_free(e->left.pexpr);
+                pexpr_free(e->right.pexpr);
+                e->type = PE_SYMBOL;
+                e->left.fexpr = const_false;
+                e->right.fexpr = NULL;
+                return e;
+            } else if (e->right.pexpr->left.fexpr == const_true) {
+                free(e->right.pexpr);
+                tmp = e->left.pexpr;
+                *e = *(e->left.pexpr);
+                free(tmp);
+                return e;
+            }
+        }
+        break;
+    case PE_OR:
+        e->left.pexpr = pexpr_eliminate_yn(e->left.pexpr);
+        e->right.pexpr = pexpr_eliminate_yn(e->right.pexpr);
+        if (e->left.pexpr->type == PE_SYMBOL) {
+            if (e->left.pexpr->left.fexpr == const_false) {
+                free(e->left.pexpr);
+                tmp = e->right.pexpr;
+                *e = *(e->right.pexpr);
+                free(tmp);
+                return e;
+            } else if (e->left.pexpr->left.fexpr == const_true) {
+                pexpr_free(e->left.pexpr);
+                pexpr_free(e->right.pexpr);
+                e->type = PE_SYMBOL;
+                e->left.fexpr = const_true;
+                e->right.pexpr = NULL;
+            }
+        }
+        if (e->right.pexpr->type == PE_SYMBOL) {
+            if (e->right.pexpr->left.fexpr == const_false) {
+                free(e->right.pexpr);
+                tmp = e->left.pexpr;
+                *e = *(e->left.pexpr);
+                free(tmp);
+                return e;
+            } else if (e->right.pexpr->left.fexpr == const_true) {
+                pexpr_free(e->left.pexpr);
+                pexpr_free(e->right.pexpr);
+                e->type = PE_SYMBOL;
+                e->left.fexpr = const_true;
+                e->right.pexpr = NULL;
+                return e;
+            }
+        }
+    default:
+        ;
+    }
+
+    return e;
+}
+
+/*
+ * copy a pexpr
+ */
+struct pexpr * pexpr_copy(const struct pexpr *org)
+{
+    struct pexpr *e;
+
+    if (!org)
+        return NULL;
+
+    e = xmalloc(sizeof(*org));
+    memcpy(e, org, sizeof(*org));
+    switch (org->type) {
+    case PE_SYMBOL:
+        e->left = org->left;
+        break;
+    case PE_AND:
+    case PE_OR:
+        e->left.pexpr = pexpr_copy(org->left.pexpr);
+        e->right.pexpr = pexpr_copy(org->right.pexpr);
+        break;
+    case PE_NOT:
+        e->left.pexpr = pexpr_copy(org->left.pexpr);
+        break;
+    }
+
+    return e;
+}
+
+/*
+ * free a pexpr
+ */
+void pexpr_free(struct pexpr *e)
+{
+    if (!e)
+        return;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        break;
+    case PE_AND:
+    case PE_OR:
+        pexpr_free(e->left.pexpr);
+        pexpr_free(e->right.pexpr);
+        break;
+    case PE_NOT:
+        pexpr_free(e->left.pexpr);
+        break;
+    }
+
+    free(e);
+}
+
+#define e1 (*ep1)
+#define e2 (*ep2)
+/*
+ * pexpr_eliminate_eq() helper
+ */
+static void __pexpr_eliminate_eq(enum pexpr_type type, struct pexpr **ep1, struct pexpr **ep2)
+{
+    /* recurse down to the leaves */
+    if (e1->type == type) {
+        __pexpr_eliminate_eq(type, &e1->left.pexpr, &e2);
+        __pexpr_eliminate_eq(type, &e1->right.pexpr, &e2);
+        return;
+    }
+    if (e2->type == type) {
+        __pexpr_eliminate_eq(type, &e1, &e2->left.pexpr);
+        __pexpr_eliminate_eq(type, &e1, &e2->right.pexpr);
+        return;
+    }
+
+    /* e1 and e2 are leaves. Compare them. */
+    if (e1->type == PE_SYMBOL && e2->type == PE_SYMBOL &&
+        e1->left.fexpr->satval == e2->left.fexpr->satval &&
+        (e1->left.fexpr == const_true || e2->left.fexpr == const_false))
+        return;
+    if (!pexpr_eq(e1, e2))
+        return;
+
+    /* e1 and e2 are equal leaves. Prepare them for elimination. */
+    trans_count++;
+    pexpr_free(e1);
+    pexpr_free(e2);
+    switch (type) {
+    case PE_AND:
+        e1 = pexf(const_true);
+        e2 = pexf(const_true);
+        break;
+    case PE_OR:
+        e1 = pexf(const_false);
+        e2 = pexf(const_false);
+        break;
+    default:
+        ;
+    }
+}
+
+/*
+ * rewrite pexpr ep1 and ep2 to remove operands common to both
+ */
+static void pexpr_eliminate_eq(struct pexpr **ep1, struct pexpr **ep2)
+{
+    if (!e1 || !e2)
+        return;
+
+    switch (e1->type) {
+    case PE_AND:
+    case PE_OR:
+        __pexpr_eliminate_eq(e1->type, ep1, ep2);
+    default:
+        ;
+    }
+    if (e1->type != e2->type) switch (e2->type) {
+    case PE_AND:
+    case PE_OR:
+        __pexpr_eliminate_eq(e2->type, ep1, ep2);
+    default:
+        ;
+    }
+    e1 = pexpr_eliminate_yn(e1);
+    e2 = pexpr_eliminate_yn(e2);
+}
+#undef e1
+#undef e2
+
+/*
+ * check whether 2 pexpr are equal
+ */
+bool pexpr_eq(struct pexpr *e1, struct pexpr *e2)
+{
+    bool res;
+    int old_count;
+
+    if (!e1 || !e2)
+        return false;
+
+    if (e1->type != e2->type)
+        return false;
+
+    switch (e1->type) {
+    case PE_SYMBOL:
+        return e1->left.fexpr->satval == e2->left.fexpr->satval;
+    case PE_AND:
+    case PE_OR:
+        e1 = pexpr_copy(e1);
+        e2 = pexpr_copy(e2);
+        old_count = trans_count;
+        pexpr_eliminate_eq(&e1, &e2);
+        res = (e1->type == PE_SYMBOL && e2->type == PE_SYMBOL &&
+            e1->left.fexpr->satval == e2->left.fexpr->satval);
+        pexpr_free(e1);
+        pexpr_free(e2);
+        trans_count = old_count;
+        return res;
+    case PE_NOT:
+        return pexpr_eq(e1->left.pexpr, e2->left.pexpr);
+    }
+
+    return false;
+}
+
+/*
+ * print a pexpr
+ */
+static void pexpr_print_util(struct pexpr *e, int prevtoken)
+{
+    if (!e)
+        return;
+
+    switch (e->type) {
+    case PE_SYMBOL:
+        printf("%s", str_get(&e->left.fexpr->name));
+        break;
+    case PE_AND:
+        if (prevtoken != PE_AND && prevtoken != -1)
+            printf("(");
+        pexpr_print_util(e->left.pexpr, PE_AND);
+        printf(" && ");
+        pexpr_print_util(e->right.pexpr, PE_AND);
+        if (prevtoken != PE_AND && prevtoken != -1)
+            printf(")");
+        break;
+    case PE_OR:
+        if (prevtoken != PE_OR && prevtoken != -1)
+            printf("(");
+        pexpr_print_util(e->left.pexpr, PE_OR);
+        printf(" || ");
+        pexpr_print_util(e->right.pexpr, PE_OR);
+        if (prevtoken != PE_OR && prevtoken != -1)
+            printf(")");
+        break;
+    case PE_NOT:
+        printf("!");
+        pexpr_print_util(e->left.pexpr, PE_NOT);
+        break;
+    }
+}
+void pexpr_print(char *tag, struct pexpr *e, int prevtoken)
+{
+    printf("%s: ", tag);
+    pexpr_print_util(e, prevtoken);
+    printf("\n");
+}
+
+/*
+ * convert a fexpr to a pexpr
+ */
+struct pexpr * pexf(struct fexpr *fe)
+{
+    struct pexpr *pe = xcalloc(1, sizeof(*pe));
+    pe->type = PE_SYMBOL;
+    pe->left.fexpr = fe;
+    return pe;
+}
+
+static struct pexpr * pexpr_join_or(struct pexpr *e1, struct pexpr *e2)
+{
+    if (pexpr_eq(e1, e2))
+        return pexpr_copy(e1);
+    else
+        return NULL;
+}
+
+static struct pexpr * pexpr_join_and(struct pexpr *e1, struct pexpr *e2)
+{
+    if (pexpr_eq(e1, e2))
+        return pexpr_copy(e1);
+    else
+        return NULL;
+}
+
+/*
+ * pexpr_eliminate_dups() helper.
+ */
+static void pexpr_eliminate_dups1(enum pexpr_type type, struct pexpr **ep1, struct pexpr **ep2)
+{
+#define e1 (*ep1)
+#define e2 (*ep2)
+
+    struct pexpr *tmp;
+
+    /* recurse down to leaves */
+    if (e1->type == type) {
+        pexpr_eliminate_dups1(type, &e1->left.pexpr, &e2);
+        pexpr_eliminate_dups1(type, &e1->right.pexpr, &e2);
+        return;
+    }
+    if (e2->type == type) {
+        pexpr_eliminate_dups1(type, &e1, &e2->left.pexpr);
+        pexpr_eliminate_dups1(type, &e1, &e2->right.pexpr);
+        return;
+    }
+
+    /* e1 and e2 are leaves. Compare them. */
+
+    if (e1 == e2)
+        return;
+
+    switch (e1->type) {
+    case PE_AND:
+    case PE_OR:
+        pexpr_eliminate_dups1(e1->type, &e1, &e1);
+    default:
+        ;
+    }
+
+    switch (type) {
+    case PE_AND:
+        tmp = pexpr_join_and(e1, e2);
+        if (tmp) {
+            pexpr_free(e1);
+            pexpr_free(e2);
+            e1 = pexf(const_true);
+            e2 = tmp;
+            trans_count++;
+        }
+        break;
+    case PE_OR:
+        tmp = pexpr_join_or(e1, e2);
+        if (tmp) {
+            pexpr_free(e1);
+            pexpr_free(e2);
+            e1 = pexf(const_false);
+            e2 = tmp;
+            trans_count++;
+        }
+        break;
+    default:
+        ;
+    }
+
+#undef e1
+#undef e2
+}
+
+/*
+ * eliminate duplicate and redundant operands
+ */
+struct pexpr * pexpr_eliminate_dups(struct pexpr *e)
+{
+    if (!e)
+        return e;
+
+    int oldcount = trans_count;
+    while (true) {
+        trans_count = 0;
+        switch (e->type) {
+        case PE_AND:
+        case PE_OR:
+            pexpr_eliminate_dups1(e->type, &e, &e);
+        default:
+            ;
+        }
+        if (!trans_count)
+            /* no simplification done in this pass. We're done. */
+            break;
+        e = pexpr_eliminate_yn(e);
+    }
+    trans_count = oldcount;
+    return e;
+}
diff --git a/scripts/kconfig/cf_expr.h b/scripts/kconfig/cf_expr.h
new file mode 100644
index 000000000000..cc612866fed4
--- /dev/null
+++ b/scripts/kconfig/cf_expr.h
@@ -0,0 +1,237 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2021 Patrick Franz <deltaone@debian.org>
+ */
+
+#ifndef CF_EXPR_H
+#define CF_EXPR_H
+
+#define fexpr_list_for_each(node, list) \
+    for (node = list->head; node != NULL; node = node->next)
+
+#define fexl_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define pexpr_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define sdv_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define sfix_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define sfl_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define sym_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define defm_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+#define prop_list_for_each(node, list) \
+    fexpr_list_for_each(node, list)
+
+/* create a fexpr */
+struct fexpr * fexpr_create(int satval, enum fexpr_type type, char *name);
+
+/* create the fexpr for a symbol */
+void sym_create_fexpr (struct symbol *sym);
+
+struct pexpr * expr_calculate_pexpr_both(struct expr *e);
+struct pexpr * expr_calculate_pexpr_y(struct expr *e);
+struct pexpr * expr_calculate_pexpr_m(struct expr *e);
+struct pexpr * expr_calculate_pexpr_y_and(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_m_and(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_both_and(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_y_or(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_m_or(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_both_or(struct expr *a, struct expr *b);
+struct pexpr * expr_calculate_pexpr_y_not(struct expr * e);
+struct pexpr * expr_calculate_pexpr_m_not(struct expr *e);
+struct pexpr * expr_calculate_pexpr_y_equals(struct expr *e);
+struct pexpr * expr_calculate_pexpr_y_unequals(struct expr *e);
+struct pexpr * expr_calculate_pexpr_y_comp(struct expr *e);
+
+/* macro to create a pexpr of type AND */
+struct pexpr * pexpr_and(struct pexpr *a, struct pexpr *b);
+
+/* macro to create a pexpr of type OR */
+struct pexpr * pexpr_or(struct pexpr *a, struct pexpr *b);
+
+/* macro to create a pexpr of type NOT */
+struct pexpr * pexpr_not(struct pexpr *a);
+
+/* check whether a pexpr is in CNF */
+bool pexpr_is_cnf(struct pexpr *e);
+
+/* check whether a pexpr is in NNF */
+bool pexpr_is_nnf(struct pexpr *e);
+
+/* return fexpr_both for a symbol */
+struct pexpr * sym_get_fexpr_both(struct symbol *sym);
+
+/* return fexpr_sel_both for a symbol */
+struct pexpr * sym_get_fexpr_sel_both(struct symbol *sym);
+
+/* create the fexpr of a non-boolean symbol for a specific value */
+struct fexpr * sym_create_nonbool_fexpr(struct symbol *sym, char *value);
+
+/* return the fexpr of a non-boolean symbol for a specific value, NULL if non-existent */
+struct fexpr * sym_get_nonbool_fexpr(struct symbol *sym, char *value);
+
+/*
+ * return the fexpr of a non-boolean symbol for a specific value, if it exists
+ * otherwise create it
+ */
+struct fexpr * sym_get_or_create_nonbool_fexpr(struct symbol *sym, char *value);
+
+/* macro to construct a pexpr for "A implies B" */
+struct pexpr * pexpr_implies(struct pexpr *a, struct pexpr *b);
+
+/* check, if the fexpr is a symbol, a True/False-constant, a literal symbolising a non-boolean or a choice symbol */
+bool fexpr_is_symbol(struct fexpr *e);
+
+/* check whether a pexpr is a symbol or a negated symbol */
+bool pexpr_is_symbol(struct pexpr *e);
+
+/* check whether the fexpr is a constant (true/false) */
+bool fexpr_is_constant(struct fexpr *e);
+
+/* add a fexpr to the satmap */
+void fexpr_add_to_satmap(struct fexpr *e);
+
+/* print an fexpr */
+void fexpr_print(char *tag, struct fexpr *e);
+
+/* write an fexpr into a string (format needed for testing) */
+void fexpr_as_char(struct fexpr *e, struct gstr *s);
+
+/* write pn pexpr into a string */
+void pexpr_as_char_short(struct pexpr *e, struct gstr *s, int parent);
+
+/* write an fexpr into a string (format needed for testing) */
+void pexpr_as_char(struct pexpr *e, struct gstr *s, int parent);
+
+/* check whether a pexpr contains a specific fexpr */
+bool pexpr_contains_fexpr(struct pexpr *e, struct fexpr *fe);
+
+/* init list of fexpr */
+struct fexpr_list * fexpr_list_init(void);
+
+/* init list of fexpr_list */
+struct fexl_list * fexl_list_init(void);
+
+/* init list of pexpr */
+struct pexpr_list * pexpr_list_init(void);
+
+/* init list of symbol_fix */
+struct sfix_list * sfix_list_init(void);
+
+/* init list of sfix_list */
+struct sfl_list * sfl_list_init(void);
+
+/* init list of symbol_dvalue */
+struct sdv_list * sdv_list_init(void);
+
+/* init list of symbols */
+struct sym_list * sym_list_init(void);
+
+/* init list of default_maps */
+struct defm_list * defm_list_init(void);
+
+/* init list of properties */
+struct prop_list *prop_list_init(void);
+
+/* add element to tail of a fexpr_list */
+void fexpr_list_add(struct fexpr_list *list, struct fexpr *fe);
+
+/* add element to tail of a fexl_list */
+void fexl_list_add(struct fexl_list *list, struct fexpr_list *elem);
+
+/* add element to tail of a pexpr_list */
+void pexpr_list_add(struct pexpr_list *list, struct pexpr *e);
+
+/* add element to tail of a sfix_list */
+void sfix_list_add(struct sfix_list *list, struct symbol_fix *fix);
+
+/* add element to tail of a sfl_list */
+void sfl_list_add(struct sfl_list *list, struct sfix_list *elem);
+
+/* add element to tail of a sdv_list */
+void sdv_list_add(struct sdv_list *list, struct symbol_dvalue *sdv);
+
+/* add element to tail of a sym_list */
+void sym_list_add(struct sym_list *list, struct symbol *sym);
+
+/* add element to tail of a defm_list */
+void defm_list_add(struct defm_list *list, struct default_map *map);
+
+/* add element to tail of a prop_list */
+void prop_list_add(struct prop_list *list, struct property *prop);
+
+/* delete an element from a fexpr_list */
+void fexpr_list_delete(struct fexpr_list *list, struct fexpr_node *node);
+
+/* delete an element from a fexpr_list */
+void fexl_list_delete(struct fexl_list *list, struct fexl_node *node);
+
+/* delete the first occurence of elem in an fexl_list */
+void fexl_list_delete_elem(struct fexl_list *list, struct fexpr_list *elem);
+
+/* delete an element from a pexpr_list */
+void pexpr_list_delete(struct pexpr_list *list, struct pexpr_node *node);
+
+/* delete an element from a sfix_list */
+void sfix_list_delete(struct sfix_list *list, struct sfix_node *node);
+
+/* make a shallow copy of a fexpr_list */
+struct fexpr_list * fexpr_list_copy(struct fexpr_list *list);
+
+/* make a shallow copy of a fexpr_list */
+struct fexl_list * fexl_list_copy(struct fexl_list *list);
+
+/* make a shallow copy of a sdv_list */
+struct sdv_list * sdv_list_copy(struct sdv_list *list);
+
+/* make a shallow copy of a sfix_list */
+struct sfix_list * sfix_list_copy(struct sfix_list *list);
+
+/* print a fexpr_list */
+void fexpr_list_print(char *title, struct fexpr_list *list);
+
+/* print a fexl_list */
+void fexl_list_print(char *title, struct fexl_list *list);
+
+/* print a pexpr_list */
+void pexpr_list_print(char *title, struct pexpr_list *list);
+
+/* free an fexpr_list */
+void fexpr_list_free(struct fexpr_list *list);
+
+/* free an fexl_list */
+void fexl_list_free(struct fexl_list *list);
+
+/* free a sdv_list */
+void sdv_list_free(struct sdv_list *list);
+
+/* check whether 2 pexpr are equal */
+bool pexpr_eq(struct pexpr *e1, struct pexpr *e2);
+
+/* copy a pexpr */
+struct pexpr * pexpr_copy(const struct pexpr *org);
+
+/* free a pexpr */
+void pexpr_free(struct pexpr *e);
+
+/* print a pexpr  */
+void pexpr_print(char *tag, struct pexpr *e, int prevtoken);
+
+/* convert a fexpr to a pexpr */
+struct pexpr * pexf(struct fexpr *fe);
+
+/* eliminate duplicate and redundant operands */
+struct pexpr * pexpr_eliminate_dups(struct pexpr *e);
+
+#endif
-- 
2.33.0



  parent reply	other threads:[~2021-10-22 13:43 UTC|newest]

Thread overview: 22+ messages / expand[flat|nested]  mbox.gz  Atom feed  top
2021-10-22 13:34 [RFC v3 00/12] kconfig: add support for conflict resolution Thorsten Berger
2021-10-22 13:35 ` [RFC v3 01/12] Add picosat.h Thorsten Berger
2021-10-22 16:57   ` Luis Chamberlain
2021-10-22 13:36 ` [RFC v3 02/12] Add picosat.c (1/3) Thorsten Berger
2021-10-22 16:58   ` Luis Chamberlain
2021-10-22 13:38 ` [RFC v3 03/12] Add picosat.c (2/3) Thorsten Berger
2021-10-22 16:59   ` Luis Chamberlain
2021-10-24  9:05   ` Masahiro Yamada
2021-10-24 23:52     ` Thorsten Berger
2021-10-22 13:39 ` [RFC v3 04/12] Add picosat.c (3/3) Thorsten Berger
2021-10-22 13:40 ` [RFC v3 05/12] Add definitions Thorsten Berger
2021-10-22 16:56   ` Luis Chamberlain
2021-10-22 13:41 ` [RFC v3 06/12] Add files for building constraints Thorsten Berger
2021-10-22 16:56   ` Luis Chamberlain
2021-10-22 13:43 ` Thorsten Berger [this message]
2021-10-22 13:44 ` [RFC v3 08/12] Add files for RangeFix Thorsten Berger
2021-10-22 13:45 ` [RFC v3 09/12] Add files with utility functions Thorsten Berger
2021-10-22 13:46 ` [RFC v3 10/12] Add tools Thorsten Berger
2021-10-22 13:47 ` [RFC v3 11/12] Add xconfig-modifications Thorsten Berger
2021-11-04  9:30   ` Masahiro Yamada
2021-10-22 13:48 ` [RFC v3 12/12] Simplify dependencies for MODULE_SIG_KEY_TYPE_RSA & MODULE_SIG_KEY_TYPE_ECDSA Thorsten Berger
2021-10-22 17:03   ` Luis Chamberlain

Reply instructions:

You may reply publicly to this message via plain-text email
using any one of the following methods:

* Save the following mbox file, import it into your mail client,
  and reply-to-all from there: mbox

  Avoid top-posting and favor interleaved quoting:
  https://en.wikipedia.org/wiki/Posting_style#Interleaved_style

* Reply using the --to, --cc, and --in-reply-to
  switches of git-send-email(1):

  git send-email \
    --in-reply-to=0aad8a90-2704-4f8b-625c-0ee591109738@rub.de \
    --to=thorsten.berger@rub.de \
    --cc=deltaone@debian.org \
    --cc=eugene.groshev@gmail.com \
    --cc=linux-kbuild@vger.kernel.org \
    --cc=mcgrof@suse.com \
    --cc=mgorman@suse.de \
    --cc=nadi@ualberta.ca \
    --cc=phayax@gmail.com \
    /path/to/YOUR_REPLY

  https://kernel.org/pub/software/scm/git/docs/git-send-email.html

* If your mail client supports setting the In-Reply-To header
  via mailto: links, try the mailto: link
Be sure your reply has a Subject: header at the top and a blank line before the message body.
This is an external index of several public inboxes,
see mirroring instructions on how to clone and mirror
all data and code used by this external index.