[PATCH v4 07/12] kconfig: Add files for handling expressions

[Ole Schuerks]

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.

Co-developed-by: Patrick Franz <deltaone@xxxxxxxxxx>
Signed-off-by: Patrick Franz <deltaone@xxxxxxxxxx>
Co-developed-by: Ibrahim Fayaz <phayax@xxxxxxxxx>
Signed-off-by: Ibrahim Fayaz <phayax@xxxxxxxxx>
Reviewed-by: Luis Chamberlain <mcgrof@xxxxxxxxxx>
Tested-by: Evgeny Groshev <eugene.groshev@xxxxxxxxx>
Suggested-by: Sarah Nadi <nadi@xxxxxxxxxxx>
Suggested-by: Thorsten Berger <thorsten.berger@xxxxxx>
Signed-off-by: Thorsten Berger <thorsten.berger@xxxxxx>
Signed-off-by: Ole Schuerks <ole0811sch@xxxxxxxxx>
---
 scripts/kconfig/cf_expr.c | 2594 +++++++++++++++++++++++++++++++++++++
 scripts/kconfig/cf_expr.h |  296 +++++
 2 files changed, 2890 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..f015f91ec8c6
--- /dev/null
+++ b/scripts/kconfig/cf_expr.c
@@ -0,0 +1,2594 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
+ */
+
+#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 "cf_expr.h"
+#include "cf_defs.h"
+#include "cf_utils.h"
+
+static void create_fexpr_bool(struct symbol *sym, struct cfdata *data);
+static void create_fexpr_nonbool(struct symbol *sym, struct cfdata *data);
+static void create_fexpr_unknown(struct symbol *sym, struct cfdata *data);
+static void create_fexpr_choice(struct symbol *sym, struct cfdata *data);
+
+static void pexpr_print_util(struct pexpr *e, int prevtoken);
+static void pexpr_shallow_copy(struct pexpr *dest, struct pexpr *org, unsigned int ref_count);
+
+static struct pexpr *pexpr_move_wrapper(
+	struct pexpr *a, struct pexpr *b, struct cfdata *data,
+	enum pexpr_move move,
+	struct pexpr *(*func)(struct pexpr *, struct pexpr *, struct cfdata *));
+
+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, struct cfdata *data)
+{
+	if (sym_is_choice(sym))
+		create_fexpr_choice(sym, data);
+	else if (sym_is_boolean(sym))
+		create_fexpr_bool(sym, data);
+	else if (sym_is_nonboolean(sym))
+		create_fexpr_nonbool(sym, data);
+	else
+		create_fexpr_unknown(sym, data);
+}
+
+/*
+ * create the fexpr for symbols with reverse dependencies
+ */
+static void create_fexpr_selected(struct symbol *sym, struct cfdata *data)
+{
+	struct fexpr *fexpr_sel_y;
+	struct fexpr *fexpr_sel_m;
+
+	/* fexpr_sel_y */
+	fexpr_sel_y = fexpr_create(data->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, data);
+
+	sym->fexpr_sel_y = fexpr_sel_y;
+
+	/* fexpr_sel_m */
+	if (sym->type == S_BOOLEAN)
+		return;
+
+	fexpr_sel_m = fexpr_create(data->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, data);
+
+	sym->fexpr_sel_m = fexpr_sel_m;
+}
+
+/*
+ * create the fexpr for a boolean/tristate symbol
+ */
+static void create_fexpr_bool(struct symbol *sym, struct cfdata *data)
+{
+	struct fexpr *fexpr_y;
+	struct fexpr *fexpr_m;
+
+	fexpr_y = fexpr_create(data->sat_variable_nr++, FE_SYMBOL, sym->name);
+	fexpr_y->sym = sym;
+	fexpr_y->tri = yes;
+	fexpr_add_to_satmap(fexpr_y, data);
+
+	sym->fexpr_y = fexpr_y;
+
+
+	if (sym->type == S_TRISTATE) {
+		fexpr_m = fexpr_create(data->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, data);
+	} else {
+		fexpr_m = data->constants->const_false;
+	}
+
+	sym->fexpr_m = fexpr_m;
+
+	if (sym->rev_dep.expr)
+		create_fexpr_selected(sym, data);
+}
+
+/*
+ * create the fexpr for a non-boolean symbol
+ */
+static void create_fexpr_nonbool(struct symbol *sym, struct cfdata *data)
+{
+	/* default values */
+	char int_values[][2] = {"n", "0", "1"};
+	char hex_values[][4] = {"n", "0x0", "0x1"};
+	char string_values[][9] = {"n", "", "nonempty"};
+
+	sym->fexpr_y = data->constants->const_false;
+	sym->fexpr_m = data->constants->const_false;
+	sym->nb_vals = fexpr_list_init();
+
+	for (int i = 0; i < 3; i++) {
+		struct fexpr *e = fexpr_create(data->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, data);
+	}
+}
+
+/*
+ * set fexpr_y and fexpr_m simply to False
+ */
+static void create_fexpr_unknown(struct symbol *sym, struct cfdata *data)
+{
+	sym->fexpr_y = data->constants->const_false;
+	sym->fexpr_m = data->constants->const_false;
+}
+
+/*
+ * create the fexpr for a choice symbol
+ */
+static void create_fexpr_choice(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prompt;
+	char *name, *write, *read;
+	struct fexpr *fexpr_y;
+	struct fexpr *fexpr_m;
+
+	if (!sym_is_boolean(sym))
+		return;
+
+	prompt = sym_get_prompt(sym);
+	if (prompt == NULL) {
+		perror("Choice symbol should have a prompt.");
+		return;
+	}
+
+	name = strdup(prompt->text);
+
+	/* remove spaces */
+	write = name;
+	read = name;
+	do {
+		if (*read != ' ')
+			*write++ = *read;
+	} while (*read++);
+
+	fexpr_y = fexpr_create(data->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, data);
+
+	sym->fexpr_y = fexpr_y;
+
+	if (sym->type == S_TRISTATE) {
+		fexpr_m = fexpr_create(data->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, data);
+	} else {
+		fexpr_m = data->constants->const_false;
+	}
+	sym->fexpr_m = fexpr_m;
+	free(name);
+}
+
+/*
+ * 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, struct cfdata *data)
+{
+	int base;
+	struct pexpr *c;
+	long val;
+	struct fexpr_node *node;
+	struct fexpr *fe;
+
+	if (!sym || !compval)
+		return pexf(data->constants->const_false);
+
+	base = 0;
+	switch (sym->type) {
+	case S_INT:
+		base = 10;
+		break;
+	case S_HEX:
+		base = 16;
+		break;
+	default:
+		break;
+	}
+
+	c = pexf(data->constants->const_false);
+	val = strtol(compval->name, NULL, base);
+	for (node = sym->nb_vals->head->next; node != NULL; node = node->next) {
+		long symval;
+
+		fe = node->elem;
+		symval = strtol(str_get(&fe->nb_val), NULL, base);
+
+		switch (type) {
+		case E_LTH:
+			if (symval < val)
+				c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
+			break;
+		case E_LEQ:
+			if (symval <= val)
+				c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
+			break;
+		case E_GTH:
+			if (symval > val)
+				c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
+			break;
+		case E_GEQ:
+			if (symval >= val)
+				c = pexpr_or(c, pexf(fe), data, PEXPR_ARGX);
+			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, struct cfdata *data)
+{
+	struct pexpr *c;
+
+	if (!left || !right)
+		return pexf(data->constants->const_false);
+
+	if (!sym_is_boolean(left) || !sym_is_boolean(right)) {
+		perror("Comparing 2 symbols that should be boolean.");
+		return pexf(data->constants->const_false);
+	}
+
+	switch (type) {
+	case E_LTH:
+		c = pexpr_and(pexpr_not(sym_get_fexpr_both(left, data), data),
+			      sym_get_fexpr_both(right, data), data,
+			      PEXPR_ARGX);
+		if (left->type == S_TRISTATE)
+			c = pexpr_or(c,
+				     pexpr_and(pexf(left->fexpr_m),
+					       pexf(right->fexpr_y), data,
+					       PEXPR_ARGX),
+				     data, PEXPR_ARGX);
+		break;
+	case E_LEQ:
+		c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y), data,
+			      PEXPR_ARGX);
+		if (left->type == S_TRISTATE)
+			c = pexpr_or(c,
+				     pexpr_and(pexf(left->fexpr_m),
+					       sym_get_fexpr_both(right, data),
+					       data, PEXPR_ARGX),
+				     data, PEXPR_ARGX);
+		c = pexpr_or(c, pexpr_not(sym_get_fexpr_both(left, data), data),
+			     data, PEXPR_ARGX);
+		break;
+	case E_GTH:
+		c = pexpr_and(sym_get_fexpr_both(left, data),
+			      pexpr_not(sym_get_fexpr_both(right, data), data),
+			      data, PEXPR_ARGX);
+		if (right->type == S_TRISTATE)
+			c = pexpr_or(c,
+				     pexpr_and(pexf(left->fexpr_y),
+					       pexf(right->fexpr_m), data,
+					       PEXPR_ARGX),
+				     data, PEXPR_ARGX);
+		break;
+	case E_GEQ:
+		c = pexpr_and(pexf(left->fexpr_y), pexf(right->fexpr_y), data,
+			      PEXPR_ARGX);
+		if (right->type == S_TRISTATE)
+			c = pexpr_or(c,
+				     pexpr_and(sym_get_fexpr_both(left, data),
+					       pexf(right->fexpr_m), data,
+					       PEXPR_ARGX),
+				     data, PEXPR_ARGX);
+		c = pexpr_or(c,
+			     pexpr_not(sym_get_fexpr_both(right, data), data),
+			     data, PEXPR_ARGX);
+		break;
+	default:
+		fprintf(stderr, "Wrong type - %s", __func__);
+		c = pexf(data->constants->const_false);
+	}
+
+	return c;
+}
+/*
+ * calculate, when expr will evaluate to yes or mod
+ */
+struct pexpr *expr_calculate_pexpr_both(struct expr *e, struct cfdata *data)
+{
+	if (!e)
+		return pexf(data->constants->const_false);
+
+	if (!expr_can_evaluate_to_mod(e))
+		return expr_calculate_pexpr_y(e, data);
+
+	switch (e->type) {
+	case E_SYMBOL:
+		return pexpr_or(expr_calculate_pexpr_m(e, data), expr_calculate_pexpr_y(e, data),
+				data, PEXPR_ARGX);
+	case E_AND:
+		return expr_calculate_pexpr_both_and(e->left.expr, e->right.expr, data);
+	case E_OR:
+		return expr_calculate_pexpr_both_or(e->left.expr, e->right.expr, data);
+	case E_NOT:
+		return pexpr_or(expr_calculate_pexpr_m(e, data), expr_calculate_pexpr_y(e, data),
+				data, PEXPR_ARGX);
+	case E_EQUAL:
+		return expr_calculate_pexpr_y_equals(e, data);
+	case E_UNEQUAL:
+		return expr_calculate_pexpr_y_unequals(e, data);
+	case E_LTH:
+	case E_LEQ:
+	case E_GTH:
+	case E_GEQ:
+		return expr_calculate_pexpr_y_comp(e, data);
+	default:
+		// TODO
+		fprintf(stderr, "Unhandled type - %s", __func__);
+		return NULL;
+	}
+}
+
+/*
+ * calculate, when expr will evaluate to yes
+ */
+struct pexpr *expr_calculate_pexpr_y(struct expr *e, struct cfdata *data)
+{
+	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, data);
+	case E_OR:
+		return expr_calculate_pexpr_y_or(e->left.expr, e->right.expr, data);
+	case E_NOT:
+		return expr_calculate_pexpr_y_not(e->left.expr, data);
+	case E_EQUAL:
+		return expr_calculate_pexpr_y_equals(e, data);
+	case E_UNEQUAL:
+		return expr_calculate_pexpr_y_unequals(e, data);
+	case E_LTH:
+	case E_LEQ:
+	case E_GTH:
+	case E_GEQ:
+		return expr_calculate_pexpr_y_comp(e, data);
+	default:
+		fprintf(stderr, "Unhandled type - %s", __func__);
+		return NULL;
+	}
+}
+
+/*
+ * calculate, when expr will evaluate to mod
+ */
+struct pexpr *expr_calculate_pexpr_m(struct expr *e, struct cfdata *data)
+{
+	if (!e)
+		return NULL;
+
+	if (!expr_can_evaluate_to_mod(e))
+		return pexf(data->constants->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, data);
+	case E_OR:
+		return expr_calculate_pexpr_m_or(e->left.expr, e->right.expr, data);
+	case E_NOT:
+		return expr_calculate_pexpr_m_not(e->left.expr, data);
+	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, struct cfdata *data)
+{
+	return pexpr_and(expr_calculate_pexpr_y(a, data),
+			      expr_calculate_pexpr_y(b, data), data,
+			      PEXPR_ARGX);
+}
+
+/*
+ * 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 cfdata *data)
+{
+	struct pexpr *topright =
+		pexpr_not(pexpr_and(expr_calculate_pexpr_y(a, data),
+					      expr_calculate_pexpr_y(b, data),
+					      data, PEXPR_ARGX),
+			       data);
+	struct pexpr *ll_left = pexpr_or(expr_calculate_pexpr_y(a, data),
+					 expr_calculate_pexpr_m(a, data), data,
+					 PEXPR_ARGX);
+	struct pexpr *ll_right = pexpr_or(expr_calculate_pexpr_y(b, data),
+					  expr_calculate_pexpr_m(b, data), data,
+					  PEXPR_ARGX);
+	struct pexpr *topleft = pexpr_and(ll_left, ll_right, data, PEXPR_ARGX);
+
+	return pexpr_and(topleft, topright, data, PEXPR_ARGX);
+}
+
+/*
+ * 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 cfdata *data)
+{
+	struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a, data),
+				      expr_calculate_pexpr_m(a, data), data,
+				      PEXPR_ARGX);
+	struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b, data),
+				       expr_calculate_pexpr_m(b, data), data,
+				       PEXPR_ARGX);
+
+	return pexpr_and(left, right, data, PEXPR_ARGX);
+}
+
+/*
+ * 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,
+					struct cfdata *data)
+{
+	return pexpr_or(expr_calculate_pexpr_y(a, data),
+			     expr_calculate_pexpr_y(b, data), data, PEXPR_ARGX);
+}
+
+/*
+ * 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 cfdata *data)
+{
+	struct pexpr *topright =
+		pexpr_not(expr_calculate_pexpr_y(b, data), data);
+	struct pexpr *lowerleft = pexpr_or(expr_calculate_pexpr_m(a, data),
+						expr_calculate_pexpr_m(b, data),
+						data, PEXPR_ARGX);
+	struct pexpr *topleft = pexpr_and(
+		lowerleft,
+		pexpr_not(expr_calculate_pexpr_y(a, data), data), data,
+		PEXPR_ARGX);
+
+	return pexpr_and(topleft, topright, data, PEXPR_ARGX);
+}
+
+/*
+ * 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 cfdata *data)
+{
+	struct pexpr *left = pexpr_or(expr_calculate_pexpr_y(a, data),
+				      expr_calculate_pexpr_m(a, data), data,
+				      PEXPR_ARGX);
+	struct pexpr *right = pexpr_or(expr_calculate_pexpr_y(b, data),
+				       expr_calculate_pexpr_m(b, data), data,
+				       PEXPR_ARGX);
+
+	return pexpr_or(left, right, data, PEXPR_ARGX);
+}
+
+/*
+ * calculate, when expr of type NOT will evaluate to yes
+ * !(A || A_m)
+ */
+struct pexpr *expr_calculate_pexpr_y_not(struct expr *e, struct cfdata *data)
+{
+	return pexpr_not(pexpr_or(expr_calculate_pexpr_y(e, data),
+					    expr_calculate_pexpr_m(e, data),
+					    data, PEXPR_ARGX),
+			      data);
+}
+
+/*
+ * calculate, when expr of type NOT will evaluate to mod
+ * A_m
+ */
+struct pexpr *expr_calculate_pexpr_m_not(struct expr *e, struct cfdata *data)
+{
+	return expr_calculate_pexpr_m(e, data);
+}
+
+static struct pexpr *equiv_pexpr_share(struct pexpr *a, struct pexpr *b,
+				       struct cfdata *data)
+{
+	struct pexpr *yes = pexpr_and_share(a, b, data);
+	struct pexpr *not = pexpr_and(pexpr_not_share(a, data),
+					   pexpr_not_share(b, data), data,
+					   PEXPR_ARGX);
+
+	return pexpr_or(yes, not, data, PEXPR_ARGX);
+}
+
+static struct pexpr *equiv_pexpr_move(struct pexpr *a, struct pexpr *b,
+				       struct cfdata *data,
+				       enum pexpr_move move)
+{
+	return pexpr_move_wrapper(a, b, data, move, equiv_pexpr_share);
+}
+
+/*
+ * create the fexpr of a non-boolean symbol for a specific value
+ */
+struct fexpr *sym_create_nonbool_fexpr(struct symbol *sym, char *value,
+				       struct cfdata *data)
+{
+	struct fexpr *e;
+	char *s;
+
+	if (!strcmp(value, "")) {
+		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, value);
+
+	/* fexpr already exists */
+	if (e != NULL)
+		return e;
+
+	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(data->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, data);
+
+	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 cfdata *data)
+{
+	struct fexpr *e = sym_get_nonbool_fexpr(sym, value);
+
+	if (e != NULL)
+		return e;
+	else
+		return sym_create_nonbool_fexpr(sym, value, data);
+}
+
+/*
+ * calculate, when expr of type EQUAL will evaluate to yes
+ * Side effect: May create certain values in e->{left,right}.sym.nb_vals
+ */
+struct pexpr *expr_calculate_pexpr_y_equals(struct expr *e, struct cfdata *data)
+{
+	/* 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(data->constants->const_true) :
+			       pexf(data->constants->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(data->constants->const_true) :
+			       pexf(data->constants->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_move(
+			pexf(e->left.sym->fexpr_y), pexf(e->right.sym->fexpr_y),
+			data, PEXPR_ARGX);
+		struct pexpr *mod = equiv_pexpr_move(
+			pexf(e->left.sym->fexpr_m), pexf(e->right.sym->fexpr_m),
+			data, PEXPR_ARGX);
+
+		return pexpr_and(yes, mod, data, PEXPR_ARGX);
+	}
+
+	/* 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, data));
+
+	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, data));
+
+	/* 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(data->constants->const_false);
+	if (sym_is_tristate_constant(e->left.sym) &&
+	    sym_is_nonboolean(e->right.sym))
+		return pexf(data->constants->const_false);
+
+	/* comparing 2 nonboolean symbols */
+	if (sym_is_nonboolean(e->left.sym) && sym_is_nonboolean(e->right.sym)) {
+		struct pexpr *c = pexf(data->constants->const_false);
+		struct fexpr *e1, *e2;
+
+		for (struct fexpr_node *node1 =
+			     e->left.sym->nb_vals->head->next;
+		     node1 != NULL; node1 = node1->next) {
+			e1 = node1->elem;
+			for (struct fexpr_node *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), data,
+							       PEXPR_ARGX),
+						data, PEXPR_ARGX);
+					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(data->constants->const_false);
+	if (sym_is_nonbool_constant(e->left.sym) &&
+	    sym_is_tristate_constant(e->right.sym))
+		return pexf(data->constants->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(data->constants->const_false);
+	if (sym_is_tristate_constant(e->left.sym) &&
+	    e->right.sym->type == S_UNKNOWN)
+		return pexf(data->constants->const_false);
+
+	/* any other comparison is not supported and should not be executed */
+	fprintf(stderr, "Unsupported equality.");
+	print_expr(":", e, 0);
+
+	return pexf(data->constants->const_false);
+}
+
+/*
+ * transform an UNEQUAL into a Not(EQUAL)
+ */
+struct pexpr *expr_calculate_pexpr_y_unequals(struct expr *e, struct cfdata *data)
+{
+	return pexpr_not(expr_calculate_pexpr_y_equals(e, data), data);
+}
+
+struct pexpr *expr_calculate_pexpr_y_comp(struct expr *e, struct cfdata *data)
+{
+	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,
+							       data);
+		}
+		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,
+							       data);
+		}
+
+		/* 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, data);
+
+		return pexf(data->constants->const_false);
+	default:
+		fprintf(stderr, "Unhandled type - %s", __func__);
+		return NULL;
+	}
+}
+
+static struct pexpr *pexpr_move_wrapper(
+	struct pexpr *a, struct pexpr *b, struct cfdata *data,
+	enum pexpr_move move,
+	struct pexpr *(*func)(struct pexpr *, struct pexpr *, struct cfdata *))
+{
+	struct pexpr *retval = func(a, b, data);
+
+	switch (move) {
+	case PEXPR_ARG1:
+		pexpr_put(a);
+		break;
+	case PEXPR_ARG2:
+		pexpr_put(b);
+		break;
+	case PEXPR_ARGX:
+		pexpr_put(a);
+		pexpr_put(b);
+		break;
+	default:
+		fprintf(stderr, "%s: invalid value for @move - %d\n", __func__,
+			move);
+	}
+	return retval;
+}
+
+struct pexpr *pexpr_and(struct pexpr *a, struct pexpr *b, struct cfdata *data, enum pexpr_move move)
+{
+	return pexpr_move_wrapper(a, b, data, move, pexpr_and_share);
+}
+
+/*
+ * macro to create a pexpr of type AND
+ */
+struct pexpr *pexpr_and_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
+{
+	struct pexpr *e;
+
+	/* A && A -> A */
+	if (a == b || pexpr_eq(a, b, data)) {
+		pexpr_get(a);
+		return a;
+	}
+
+	/* simplifications:
+	 * expr && False -> False
+	 * expr && True  -> expr
+	 */
+	if ((a->type == PE_SYMBOL &&
+	     a->left.fexpr == data->constants->const_false) ||
+	    (b->type == PE_SYMBOL &&
+	     b->left.fexpr == data->constants->const_true)) {
+		pexpr_get(a);
+		return a;
+	}
+
+	if ((b->type == PE_SYMBOL &&
+	     b->left.fexpr == data->constants->const_false) ||
+	    (a->type == PE_SYMBOL &&
+	     a->left.fexpr == data->constants->const_true)) {
+		pexpr_get(b);
+		return b;
+	}
+
+	/* (A && B) && C -> A && B if B == C */
+	if (a->type == PE_AND && pexpr_eq(a->right.pexpr, b, data)) {
+		pexpr_get(a);
+		return a;
+	}
+
+	/* A && (B && C) -> B && C if A == B */
+	if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr, data)) {
+		pexpr_get(b);
+		return b;
+	}
+
+	if (a->type == PE_OR && b->type == PE_OR) {
+		e = NULL;
+		/* (A || B) && (C || D) -> A || (B && D) if A == C */
+		if (pexpr_eq(a->left.pexpr, b->left.pexpr, data)) {
+			e = pexpr_or(a->left.pexpr,
+					  pexpr_and_share(a->right.pexpr,
+							  b->right.pexpr, data),
+					  data, PEXPR_ARG2);
+		}
+		/* (A || B) && (C || D) -> B || (A && C) if B == D */
+		else if (pexpr_eq(a->right.pexpr, b->right.pexpr, data)) {
+			e = pexpr_or(a->right.pexpr,
+					  pexpr_and_share(a->left.pexpr,
+							  b->left.pexpr, data),
+					  data, PEXPR_ARG2);
+		}
+		/* (A || B) && (C || D) -> A || (B && C) if A == D */
+		else if (pexpr_eq(a->left.pexpr, b->right.pexpr, data)) {
+			e = pexpr_or(a->left.pexpr,
+					  pexpr_and_share(a->right.pexpr,
+							  b->left.pexpr, data),
+					  data, PEXPR_ARG2);
+		}
+		/* (A || B) && (C || D) -> B || (A && D) if B == C */
+		else if (pexpr_eq(a->right.pexpr, b->left.pexpr, data)) {
+			e = pexpr_or(a->right.pexpr,
+					  pexpr_and_share(a->left.pexpr,
+							  b->right.pexpr, data),
+					  data, PEXPR_ARG2);
+		}
+		if (e)
+			return e;
+	}
+
+	/* general case */
+	e = xcalloc(1, sizeof(*e));
+	pexpr_get(a);
+	pexpr_get(b);
+	pexpr_construct_and(e, a, b, 1);
+	return e;
+}
+
+struct pexpr *pexpr_or(struct pexpr *a, struct pexpr *b, struct cfdata *data, enum pexpr_move move)
+{
+	return pexpr_move_wrapper(a, b, data, move, pexpr_or_share);
+}
+
+/*
+ * macro to create a pexpr of type OR
+ */
+struct pexpr *pexpr_or_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
+{
+	struct pexpr *e;
+	bool cond1, cond2;
+
+	/* A || A  -> A */
+	if (a == b || pexpr_eq(a, b, data)) {
+		pexpr_get(a);
+		return a;
+	}
+
+	/* simplifications:
+	 * A || False -> A
+	 * A || True  -> True
+	 */
+	cond1 = a->type == PE_SYMBOL && a->left.fexpr == data->constants->const_false;
+	cond2 = b->type == PE_SYMBOL && b->left.fexpr == data->constants->const_true;
+	if (cond1 || cond2) {
+		pexpr_get(b);
+		return b;
+	}
+	cond1 = b->type == PE_SYMBOL && b->left.fexpr == data->constants->const_false;
+	cond2 = a->type == PE_SYMBOL && a->left.fexpr == data->constants->const_true;
+	if (cond1 || cond2) {
+		pexpr_get(a);
+		return a;
+	}
+
+	/* A || (B && C) -> A if (A == B || A == C) */
+	if (b->type == PE_AND && (
+		pexpr_eq(a, b->left.pexpr, data) || pexpr_eq(a, b->right.pexpr, data)
+	)) {
+		pexpr_get(a);
+		return a;
+	}
+	/* (A && B) || C -> C if (A == C || B == C) */
+	if (a->type == PE_AND && (
+		pexpr_eq(a->left.pexpr, b, data) || pexpr_eq(a->right.pexpr, b, data)
+	)) {
+		pexpr_get(b);
+		return b;
+	}
+
+	/* -A || B -> True if A == B
+	 * A || -B -> True if A == B
+	 */
+	cond1 = a->type == PE_NOT && pexpr_eq(a->left.pexpr, b, data);
+	cond2 = b->type == PE_NOT && pexpr_eq(a, b->left.pexpr, data);
+	if (cond1 || cond2)
+		return pexf(data->constants->const_true);
+
+	if (a->type == PE_AND && b->type == PE_AND) {
+		e = NULL;
+		/* (A && B) || (C && D) -> A && (B || D) if (A == C) */
+		if (pexpr_eq(a->left.pexpr, b->left.pexpr, data)) {
+			e = pexpr_and(a->left.pexpr,
+				      pexpr_or_share(a->right.pexpr, b->right.pexpr, data), data,
+				      PEXPR_ARG2);
+		}
+		/* (A && B) || (C && D) -> B && (A || C) if (B == D) */
+		if (pexpr_eq(a->right.pexpr, b->right.pexpr, data)) {
+			e = pexpr_and(a->right.pexpr,
+				      pexpr_or_share(a->left.pexpr, b->left.pexpr, data), data,
+				      PEXPR_ARG2);
+		}
+		/* (A && B) || (C && D) -> A && (B || C) if (A == D) */
+		if (pexpr_eq(a->left.pexpr, b->right.pexpr, data)) {
+			e = pexpr_and(a->left.pexpr,
+				      pexpr_or_share(a->right.pexpr, b->left.pexpr, data), data,
+				      PEXPR_ARG2);
+		}
+		/* (A && B) || (C && D) -> B && (A || D) if (B == C) */
+		if (pexpr_eq(a->right.pexpr, b->left.pexpr, data)) {
+			e = pexpr_and(a->right.pexpr,
+				      pexpr_or_share(a->left.pexpr, b->right.pexpr, data), data,
+				      PEXPR_ARG2);
+		}
+		if (e)
+			return e;
+	}
+
+	/* (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, data) ||
+		pexpr_eq(a->left.pexpr, b->right.pexpr, data) ||
+		pexpr_eq(a->right.pexpr, b->left.pexpr, data) ||
+		pexpr_eq(a->right.pexpr, b->right.pexpr, data)
+	)) {
+		pexpr_get(b);
+		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, data) ||
+		pexpr_eq(a->left.pexpr, b->right.pexpr, data) ||
+		pexpr_eq(a->right.pexpr, b->left.pexpr, data) ||
+		pexpr_eq(a->right.pexpr, b->right.pexpr, data)
+	)) {
+		pexpr_get(a);
+		return a;
+	}
+
+	/* general case */
+	e = xcalloc(1, sizeof(*e));
+	pexpr_get(a);
+	pexpr_get(b);
+	pexpr_construct_or(e, a, b, 1);
+
+	return e;
+}
+
+struct pexpr *pexpr_not(struct pexpr *a, struct cfdata *data)
+{
+	struct pexpr *retval = pexpr_not_share(a, data);
+
+	pexpr_put(a);
+	return retval;
+}
+
+/*
+ * Builds NOT(@a)
+ */
+struct pexpr *pexpr_not_share(struct pexpr *a, struct cfdata *data)
+{
+	struct pexpr *ret_val;
+
+	if (a->type == PE_SYMBOL &&
+	    a->left.fexpr == data->constants->const_false)
+		ret_val = pexf(data->constants->const_true);
+	else if (a->type == PE_SYMBOL &&
+	    a->left.fexpr == data->constants->const_true)
+		ret_val = pexf(data->constants->const_false);
+	/* eliminate double negation */
+	else if (a->type == PE_NOT) {
+		ret_val = a->left.pexpr;
+		pexpr_get(ret_val);
+	}
+	/* De Morgan */
+	else if (a->type == PE_AND) {
+		ret_val = xmalloc(sizeof(*ret_val));
+		pexpr_construct_or(ret_val,
+				   pexpr_not_share(a->left.pexpr, data),
+				   pexpr_not_share(a->right.pexpr, data), 1);
+	} else if (a->type == PE_OR) {
+		ret_val = xmalloc(sizeof(*ret_val));
+		pexpr_construct_and(ret_val,
+				    pexpr_not_share(a->left.pexpr, data),
+				    pexpr_not_share(a->right.pexpr, data), 1);
+	} else {
+		ret_val = xmalloc(sizeof(*ret_val));
+		pexpr_get(a);
+		pexpr_construct_not(ret_val, a, 1);
+	}
+
+	return ret_val;
+}
+
+struct pexpr *pexpr_implies(struct pexpr *a, struct pexpr *b, struct cfdata *data,
+			    enum pexpr_move move)
+{
+	return pexpr_move_wrapper(a, b, data, move, pexpr_implies_share);
+}
+
+/*
+ * macro to construct a pexpr for "A implies B"
+ */
+struct pexpr *pexpr_implies_share(struct pexpr *a, struct pexpr *b, struct cfdata *data)
+{
+	/* A => B -> True if A == B */
+	if (a == b || pexpr_eq(a, b, data))
+		return pexf(data->constants->const_true);
+
+	/* (A => B && C) -> (A => C) if A == B */
+	if (b->type == PE_AND && pexpr_eq(a, b->left.pexpr, data))
+		return pexpr_implies_share(a, b->right.pexpr, data);
+	/* (A => B && C) -> (A => B) if A == C */
+	if (b->type == PE_AND && pexpr_eq(a, b->right.pexpr, data))
+		return pexpr_implies_share(a, b->left.pexpr, data);
+
+	/* (A => B || C) -> True if (A == B || A == C) */
+	if (b->type == PE_OR && (
+		pexpr_eq(a, b->left.pexpr, data) || pexpr_eq(a, b->right.pexpr, data)
+	))
+		return pexf(data->constants->const_true);
+
+	/* (A && B => C) -> True if (A == C || B == C) */
+	if (a->type == PE_AND && (
+		pexpr_eq(a->left.pexpr, b, data) || pexpr_eq(a->right.pexpr, b, data)
+	))
+		return pexf(data->constants->const_true);
+
+	return pexpr_or(pexpr_not_share(a, data), b, data, PEXPR_ARG1);
+}
+
+/*
+ * 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, struct cfdata *data)
+{
+	return sym->type == S_TRISTATE ?
+		       pexpr_or(pexf(sym->fexpr_m), pexf(sym->fexpr_y),
+				     data, PEXPR_ARGX) :
+		       pexf(sym->fexpr_y);
+}
+
+/*
+ * return fexpr_sel_both for a symbol
+ */
+struct pexpr *sym_get_fexpr_sel_both(struct symbol *sym, struct cfdata *data)
+{
+	if (!sym->rev_dep.expr)
+		return pexf(data->constants->const_false);
+
+	return sym->type == S_TRISTATE ?
+		       pexpr_or(pexf(sym->fexpr_sel_m),
+				     pexf(sym->fexpr_sel_y), data, PEXPR_ARGX) :
+		       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, struct cfdata *data)
+{
+	return e == data->constants->const_true || e == data->constants->const_false;
+}
+
+/*
+ * add a fexpr to the satmap
+ */
+void fexpr_add_to_satmap(struct fexpr *e, struct cfdata *data)
+{
+	if (e->satval >= data->satmap_size) {
+		data->satmap =
+			xrealloc(data->satmap, data->satmap_size * 2 * sizeof(**data->satmap));
+		data->satmap_size *= 2;
+	}
+
+	data->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, struct cfdata *data)
+{
+	if (!e)
+		return;
+
+	switch (e->type) {
+	case PE_SYMBOL:
+		if (e->left.fexpr == data->constants->const_false) {
+			str_append(s, "0");
+			return;
+		}
+		if (e->left.fexpr == data->constants->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:
+		if (parent != PE_AND)
+			str_append(s, "(");
+		pexpr_as_char(e->left.pexpr, s, PE_AND, data);
+		str_append(s, " && ");
+		pexpr_as_char(e->right.pexpr, s, PE_AND, data);
+		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, data);
+		str_append(s, " || ");
+		pexpr_as_char(e->right.pexpr, s, PE_OR, data);
+		if (parent != PE_OR)
+			str_append(s, ")");
+		return;
+	case PE_NOT:
+		str_append(s, "!");
+		pexpr_as_char(e->left.pexpr, s, PE_NOT, data);
+		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:
+		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(void)
+{
+	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(void)
+{
+	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(void)
+{
+	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 occurrence 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 defm_list (and pexpr_put the conditions of the maps and free the
+ * node->element's)
+ */
+void defm_list_destruct(struct defm_list *list)
+{
+	struct defm_node *node = list->head, *tmp;
+
+	while (node != NULL) {
+		tmp = node->next;
+		pexpr_put(node->elem->e);
+		free(node->elem);
+		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);
+}
+
+/*
+ * free a pexpr_list (and pexpr_put the elements)
+ */
+void pexpr_list_free_put(struct pexpr_list *list)
+{
+	struct pexpr_node *node = list->head, *tmp;
+
+	while (node != NULL) {
+		tmp = node->next;
+		pexpr_put(node->elem);
+		free(node);
+		node = tmp;
+	}
+
+	free(list);
+}
+
+/*
+ * free a prop_list
+ */
+void prop_list_free(struct prop_list *list)
+{
+	struct prop_node *node = list->head, *tmp;
+
+	while (node != NULL) {
+		tmp = node->next;
+		free(node);
+		node = tmp;
+	}
+
+	free(list);
+}
+
+/*
+ * free a sym_list
+ */
+void sym_list_free(struct sym_list *list)
+{
+	struct sym_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 void pexpr_eliminate_yn(struct pexpr *e, struct cfdata *data)
+{
+	struct pexpr *tmp;
+	unsigned int ref_count;
+
+	if (!e)
+		return;
+
+	switch (e->type) {
+	case PE_AND:
+		pexpr_eliminate_yn(e->left.pexpr, data);
+		pexpr_eliminate_yn(e->right.pexpr, data);
+		if (e->left.pexpr->type == PE_SYMBOL) {
+			if (e->left.pexpr->left.fexpr == data->constants->const_false) {
+				pexpr_put(e->left.pexpr);
+				pexpr_put(e->right.pexpr);
+				ref_count = e->ref_count;
+				pexpr_construct_sym(
+					e, data->constants->const_false,
+					ref_count);
+				return;
+			} else if (e->left.pexpr->left.fexpr == data->constants->const_true) {
+				pexpr_put(e->left.pexpr);
+				tmp = e->right.pexpr;
+				ref_count = e->ref_count;
+				pexpr_shallow_copy(e, tmp, ref_count);
+				pexpr_put(tmp);
+				return;
+			}
+		}
+		if (e->right.pexpr->type == PE_SYMBOL) {
+			if (e->right.pexpr->left.fexpr == data->constants->const_false) {
+				pexpr_put(e->left.pexpr);
+				pexpr_put(e->right.pexpr);
+				ref_count = e->ref_count;
+				pexpr_construct_sym(
+					e, data->constants->const_false,
+					ref_count);
+				return;
+			} else if (e->right.pexpr->left.fexpr == data->constants->const_true) {
+				pexpr_put(e->right.pexpr);
+				tmp = e->left.pexpr;
+				ref_count = e->ref_count;
+				pexpr_shallow_copy(e, tmp, ref_count);
+				pexpr_put(tmp);
+				return;
+			}
+		}
+		break;
+	case PE_OR:
+		pexpr_eliminate_yn(e->left.pexpr, data);
+		pexpr_eliminate_yn(e->right.pexpr, data);
+		if (e->left.pexpr->type == PE_SYMBOL) {
+			if (e->left.pexpr->left.fexpr == data->constants->const_false) {
+				pexpr_put(e->left.pexpr);
+				tmp = e->right.pexpr;
+				ref_count = e->ref_count;
+				pexpr_shallow_copy(e, tmp, ref_count);
+				pexpr_put(tmp);
+				return;
+			} else if (e->left.pexpr->left.fexpr == data->constants->const_true) {
+				pexpr_put(e->left.pexpr);
+				pexpr_put(e->right.pexpr);
+				ref_count = e->ref_count;
+				pexpr_construct_sym(
+					e, data->constants->const_true,
+					ref_count);
+				return;
+			}
+		}
+		if (e->right.pexpr->type == PE_SYMBOL) {
+			if (e->right.pexpr->left.fexpr == data->constants->const_false) {
+				pexpr_put(e->right.pexpr);
+				tmp = e->left.pexpr;
+				ref_count = e->ref_count;
+				pexpr_shallow_copy(e, tmp, ref_count);
+				pexpr_put(tmp);
+				return;
+			} else if (e->right.pexpr->left.fexpr == data->constants->const_true) {
+				pexpr_put(e->left.pexpr);
+				pexpr_put(e->right.pexpr);
+				ref_count = e->ref_count;
+				pexpr_construct_sym(e,
+						    data->constants->const_true,
+						    ref_count);
+				return;
+			}
+		}
+	default:
+		break;
+	}
+}
+
+static void pexpr_shallow_copy(struct pexpr *dest, struct pexpr *org, unsigned int ref_count)
+{
+	struct pexpr inter;
+
+	inter.type = org->type;
+	inter.left = org->left;
+	inter.right = org->right;
+	if (org->type == PE_OR || org->type == PE_AND) {
+		pexpr_get(org->left.pexpr);
+		pexpr_get(org->right.pexpr);
+	} else if (org->type == PE_NOT) {
+		pexpr_get(org->left.pexpr);
+	}
+	inter.ref_count = ref_count;
+	*dest = inter;
+}
+
+/*
+ * copy a pexpr
+ */
+struct pexpr *pexpr_deep_copy(const struct pexpr *org)
+{
+	struct pexpr *e;
+
+	if (!org)
+		return NULL;
+
+	e = xmalloc(sizeof(*org));
+	memcpy(e, org, sizeof(*org));
+	e->ref_count = 1;
+	switch (org->type) {
+	case PE_SYMBOL:
+		e->left = org->left;
+		break;
+	case PE_AND:
+	case PE_OR:
+		e->left.pexpr = pexpr_deep_copy(org->left.pexpr);
+		e->right.pexpr = pexpr_deep_copy(org->right.pexpr);
+		break;
+	case PE_NOT:
+		e->left.pexpr = pexpr_deep_copy(org->left.pexpr);
+		break;
+	}
+
+	return e;
+}
+
+/*
+ * free a pexpr
+ */
+void pexpr_free_depr(struct pexpr *e)
+{
+	if (!e)
+		return;
+
+	switch (e->type) {
+	case PE_SYMBOL:
+		break;
+	case PE_AND:
+	case PE_OR:
+		pexpr_free_depr(e->left.pexpr);
+		pexpr_free_depr(e->right.pexpr);
+		break;
+	case PE_NOT:
+		pexpr_free_depr(e->left.pexpr);
+		break;
+	}
+
+	free(e);
+}
+
+/*
+ * Increments ref_count and returns @e
+ */
+struct pexpr *pexpr_get(struct pexpr *e)
+{
+	++e->ref_count;
+	return e;
+}
+
+/*
+ * Decrements ref_count and if it becomes 0, it recursively puts the references
+ * to its children and calls ``free(e)``. If @e == NULL, it does nothing.
+ */
+void pexpr_put(struct pexpr *e)
+{
+	if (!e)
+		return;
+
+	if (e->ref_count == 0) {
+		printd("Invalid call to %s - ref_count is zero\n", __func__);
+		return;
+	}
+
+	--e->ref_count;
+	if (e->ref_count > 0)
+		return;
+
+	switch (e->type) {
+	case PE_SYMBOL:
+		break;
+	case PE_AND:
+	case PE_OR:
+		pexpr_put(e->left.pexpr);
+		pexpr_put(e->right.pexpr);
+		break;
+	case PE_NOT:
+		pexpr_put(e->left.pexpr);
+		break;
+	}
+
+	free(e);
+}
+
+/*
+ * calls pexpr_put for a NULL-terminated array of struct pexpr *
+ */
+void _pexpr_put_list(struct pexpr **es)
+{
+	for (; *es != NULL; es++)
+		pexpr_put(*es);
+}
+
+#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,
+				 struct cfdata *data)
+{
+	/* recurse down to the leaves */
+	if (e1->type == type) {
+		__pexpr_eliminate_eq(type, &e1->left.pexpr, &e2, data);
+		__pexpr_eliminate_eq(type, &e1->right.pexpr, &e2, data);
+		return;
+	}
+	if (e2->type == type) {
+		__pexpr_eliminate_eq(type, &e1, &e2->left.pexpr, data);
+		__pexpr_eliminate_eq(type, &e1, &e2->right.pexpr, data);
+		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 == data->constants->const_true ||
+	     e2->left.fexpr == data->constants->const_false))
+		return;
+	if (!pexpr_eq(e1, e2, data))
+		return;
+
+	/* e1 and e2 are equal leaves. Prepare them for elimination. */
+	trans_count++;
+	pexpr_put(e1);
+	pexpr_put(e2);
+	switch (type) {
+	case PE_AND:
+		e1 = pexf(data->constants->const_true);
+		e2 = pexf(data->constants->const_true);
+		break;
+	case PE_OR:
+		e1 = pexf(data->constants->const_false);
+		e2 = pexf(data->constants->const_false);
+		break;
+	default:
+		break;
+	}
+}
+
+/*
+ * rewrite pexpr ep1 and ep2 to remove operands common to both
+ */
+static void pexpr_eliminate_eq(struct pexpr **ep1, struct pexpr **ep2, struct cfdata *data)
+{
+	if (!e1 || !e2)
+		return;
+
+	switch (e1->type) {
+	case PE_AND:
+	case PE_OR:
+		__pexpr_eliminate_eq(e1->type, ep1, ep2, data);
+	default:
+		break;
+	}
+	if (e1->type != e2->type)
+		switch (e2->type) {
+		case PE_AND:
+		case PE_OR:
+			__pexpr_eliminate_eq(e2->type, ep1, ep2, data);
+		default:
+			break;
+		}
+	pexpr_eliminate_yn(e1, data);
+	pexpr_eliminate_yn(e2, data);
+}
+#undef e1
+#undef e2
+
+/*
+ * check whether 2 pexpr are equal
+ */
+bool pexpr_eq(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
+{
+	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_deep_copy(e1);
+		e2 = pexpr_deep_copy(e2);
+		old_count = trans_count;
+		pexpr_eliminate_eq(&e1, &e2, data);
+		res = (e1->type == PE_SYMBOL && e2->type == PE_SYMBOL &&
+			e1->left.fexpr->satval == e2->left.fexpr->satval);
+		pexpr_put(e1);
+		pexpr_put(e2);
+		trans_count = old_count;
+		return res;
+	case PE_NOT:
+		return pexpr_eq(e1->left.pexpr, e2->left.pexpr, data);
+	}
+
+	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));
+
+	pexpr_construct_sym(pe, fe, 1);
+	return pe;
+}
+
+void pexpr_construct_or(struct pexpr *e, struct pexpr *left,
+			     struct pexpr *right, unsigned int ref_count)
+{
+	e->type = PE_OR;
+	e->left.pexpr = left;
+	e->right.pexpr = right;
+	e->ref_count = ref_count;
+}
+
+void pexpr_construct_and(struct pexpr *e, struct pexpr *left,
+			     struct pexpr *right, unsigned int ref_count)
+{
+	e->type = PE_AND;
+	e->left.pexpr = left;
+	e->right.pexpr = right;
+	e->ref_count = ref_count;
+}
+
+void pexpr_construct_not(struct pexpr *e, struct pexpr *left,
+			  unsigned int ref_count)
+{
+	e->type = PE_NOT;
+	e->left.pexpr = left;
+	e->right.pexpr = NULL;
+	e->ref_count = ref_count;
+}
+
+void pexpr_construct_sym(struct pexpr *e, struct fexpr *left,
+			  unsigned int ref_count)
+{
+	e->type = PE_SYMBOL;
+	e->left.fexpr = left;
+	e->right.pexpr = NULL;
+	e->ref_count = ref_count;
+}
+
+static struct pexpr *pexpr_join_or(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
+{
+	if (pexpr_eq(e1, e2, data))
+		return pexpr_deep_copy(e1);
+	else
+		return NULL;
+}
+
+static struct pexpr *pexpr_join_and(struct pexpr *e1, struct pexpr *e2, struct cfdata *data)
+{
+	if (pexpr_eq(e1, e2, data))
+		return pexpr_deep_copy(e1);
+	else
+		return NULL;
+}
+
+/*
+ * pexpr_eliminate_dups() helper.
+ */
+static void pexpr_eliminate_dups1(enum pexpr_type type, struct pexpr **ep1, struct pexpr **ep2,
+				  struct cfdata *data)
+{
+#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, data);
+		pexpr_eliminate_dups1(type, &e1->right.pexpr, &e2, data);
+		return;
+	}
+	if (e2->type == type) {
+		pexpr_eliminate_dups1(type, &e1, &e2->left.pexpr, data);
+		pexpr_eliminate_dups1(type, &e1, &e2->right.pexpr, data);
+		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, data);
+	default:
+		break;
+	}
+
+	switch (type) {
+	case PE_AND:
+		tmp = pexpr_join_and(e1, e2, data);
+		if (tmp) {
+			pexpr_put(e1);
+			pexpr_put(e2);
+			e1 = pexf(data->constants->const_true);
+			e2 = tmp;
+			trans_count++;
+		}
+		break;
+	case PE_OR:
+		tmp = pexpr_join_or(e1, e2, data);
+		if (tmp) {
+			pexpr_put(e1);
+			pexpr_put(e2);
+			e1 = pexf(data->constants->const_false);
+			e2 = tmp;
+			trans_count++;
+		}
+		break;
+	default:
+		break;
+	}
+
+#undef e1
+#undef e2
+}
+
+/*
+ * eliminate duplicate and redundant operands
+ */
+struct pexpr *pexpr_eliminate_dups(struct pexpr *e, struct cfdata *data)
+{
+	int oldcount;
+
+	if (!e)
+		return e;
+
+	oldcount = trans_count;
+	while (true) {
+		trans_count = 0;
+		switch (e->type) {
+		case PE_AND:
+		case PE_OR:
+			pexpr_eliminate_dups1(e->type, &e, &e, data);
+		default:
+			break;
+		}
+		if (!trans_count)
+			/* no simplification done in this pass. We're done. */
+			break;
+		pexpr_eliminate_yn(e, data);
+	}
+	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..07435ae381e6
--- /dev/null
+++ b/scripts/kconfig/cf_expr.h
@@ -0,0 +1,296 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@xxxxxxxxxx>
+ */
+
+#ifndef CF_EXPR_H
+#define CF_EXPR_H
+
+#include <stdbool.h>
+
+#include "cf_defs.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)
+
+/* call pexpr_put for a list of pexpr's */
+#define PEXPR_PUT(...) _pexpr_put_list((struct pexpr *[]){ __VA_ARGS__, NULL })
+
+/* 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 cfdata *data);
+
+struct pexpr *expr_calculate_pexpr_both(struct expr *e, struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y(struct expr *e, struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_m(struct expr *e, struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_and(struct expr *a, struct expr *b,
+					 struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_m_and(struct expr *a, struct expr *b,
+					 struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_both_and(struct expr *a, struct expr *b,
+					    struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_or(struct expr *a, struct expr *b,
+					struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_m_or(struct expr *a, struct expr *b,
+					struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_both_or(struct expr *a, struct expr *b,
+					   struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_not(struct expr *e, struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_m_not(struct expr *e, struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_equals(struct expr *e,
+					    struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_unequals(struct expr *e,
+					      struct cfdata *data);
+struct pexpr *expr_calculate_pexpr_y_comp(struct expr *e, struct cfdata *data);
+
+/* macro to create a pexpr of type AND */
+struct pexpr *pexpr_and_share(struct pexpr *a, struct pexpr *b,
+			      struct cfdata *data);
+struct pexpr *pexpr_and(struct pexpr *a, struct pexpr *b, struct cfdata *data,
+			enum pexpr_move move);
+
+/* macro to create a pexpr of type OR */
+struct pexpr *pexpr_or_share(struct pexpr *a, struct pexpr *b,
+			     struct cfdata *data);
+struct pexpr *pexpr_or(struct pexpr *a, struct pexpr *b, struct cfdata *data,
+		       enum pexpr_move move);
+
+/* macro to create a pexpr of type NOT */
+struct pexpr *pexpr_not_share(struct pexpr *a, struct cfdata *data);
+struct pexpr *pexpr_not(struct pexpr *a, struct cfdata *data);
+
+/* 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, struct cfdata *data);
+
+/* return fexpr_sel_both for a symbol */
+struct pexpr *sym_get_fexpr_sel_both(struct symbol *sym, struct cfdata *data);
+
+/* create the fexpr of a non-boolean symbol for a specific value */
+struct fexpr *sym_create_nonbool_fexpr(struct symbol *sym, char *value,
+				       struct cfdata *data);
+
+/*
+ * 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, struct cfdata *data);
+
+/* macro to construct a pexpr for "A implies B" */
+struct pexpr *pexpr_implies_share(struct pexpr *a, struct pexpr *b, struct cfdata *data);
+struct pexpr *pexpr_implies(struct pexpr *a, struct pexpr *b, struct cfdata *data,
+			    enum pexpr_move move);
+
+/* 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, struct cfdata *data);
+
+/* add a fexpr to the satmap */
+void fexpr_add_to_satmap(struct fexpr *e, struct cfdata *data);
+
+/* 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, struct cfdata *data);
+
+/* 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 occurrence 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 pexpr_list (and pexpr_put the elements) */
+void pexpr_list_free_put(struct pexpr_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);
+
+/* free a prop_list */
+void prop_list_free(struct prop_list *list);
+
+/* free a defm_list (and pexpr_put the conditions of the maps) */
+void defm_list_destruct(struct defm_list *list);
+
+/* free a sym_list */
+void sym_list_free(struct sym_list *list);
+
+/* check whether 2 pexpr are equal */
+bool pexpr_eq(struct pexpr *e1, struct pexpr *e2, struct cfdata *data);
+
+/* copy a pexpr */
+struct pexpr *pexpr_deep_copy(const struct pexpr *org);
+
+void pexpr_construct_sym(struct pexpr *e, struct fexpr *left,
+			 unsigned int ref_count);
+void pexpr_construct_not(struct pexpr *e, struct pexpr *left,
+			 unsigned int ref_count);
+void pexpr_construct_and(struct pexpr *e, struct pexpr *left,
+			 struct pexpr *right, unsigned int ref_count);
+void pexpr_construct_or(struct pexpr *e, struct pexpr *left,
+			struct pexpr *right, unsigned int ref_count);
+
+/* free a pexpr */
+void pexpr_free_depr(struct pexpr *e);
+
+/* give up a reference to e. Also see struct pexpr. */
+void pexpr_put(struct pexpr *e);
+/* Used by PEXPR_PUT(). Not to be used directly. */
+void _pexpr_put_list(struct pexpr **es);
+
+/* acquire a reference to e. Also see struct pexpr. */
+struct pexpr *pexpr_get(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, struct cfdata *data);
+
+#endif
-- 
2.39.2