diff mbox series

[v4,06/12] kconfig: Add files for building constraints

Message ID 20240710065255.10338-7-ole0811sch@gmail.com (mailing list archive)
State New
Headers show
Series kconfig: Add support for conflict resolution | expand

Commit Message

Ole Schuerks July 10, 2024, 6:52 a.m. UTC
These files translate the Kconfig-model into propositional logic and store
the constraints for each symbol in the corresponding struct.

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@kernel.org>
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>
Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
---
 scripts/kconfig/cf_constraints.c | 1720 ++++++++++++++++++++++++++++++
 scripts/kconfig/cf_constraints.h |   26 +
 2 files changed, 1746 insertions(+)
 create mode 100644 scripts/kconfig/cf_constraints.c
 create mode 100644 scripts/kconfig/cf_constraints.h

Comments

Masahiro Yamada Aug. 12, 2024, 8:49 a.m. UTC | #1
On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@gmail.com> wrote:
>
> These files translate the Kconfig-model into propositional logic and store
> the constraints for each symbol in the corresponding struct.
>
> 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@kernel.org>
> 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>
> Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
> ---
>  scripts/kconfig/cf_constraints.c | 1720 ++++++++++++++++++++++++++++++
>  scripts/kconfig/cf_constraints.h |   26 +
>  2 files changed, 1746 insertions(+)
>  create mode 100644 scripts/kconfig/cf_constraints.c
>  create mode 100644 scripts/kconfig/cf_constraints.h
>
> diff --git a/scripts/kconfig/cf_constraints.c b/scripts/kconfig/cf_constraints.c
> new file mode 100644
> index 000000000000..1c02a4b47383
> --- /dev/null
> +++ b/scripts/kconfig/cf_constraints.c
> @@ -0,0 +1,1720 @@
> +// SPDX-License-Identifier: GPL-2.0
> +/*
> + * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
> + */
> +
> +#include "cf_defs.h"
> +#include "expr.h"
> +#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_utils.h"
> +#include "internal.h"
> +#include "cf_expr.h"
> +#include "cf_constraints.h"
> +
> +#define KCR_CMP false
> +#define NPC_OPTIMISATION true
> +
> +static void init_constraints(struct cfdata *data);
> +static void get_constraints_bool(struct cfdata *data);
> +static void get_constraints_select(struct cfdata *data);
> +static void get_constraints_nonbool(struct cfdata *data);
> +
> +static void build_tristate_constraint_clause(struct symbol *sym,
> +                                            struct cfdata *data);
> +
> +static void add_selects_kcr(struct symbol *sym, struct cfdata *data);
> +static void add_selects(struct symbol *sym, struct cfdata *data);
> +
> +static void add_dependencies_bool(struct symbol *sym, struct cfdata *data);
> +static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data);
> +static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data);
> +
> +static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data);
> +static void add_choice_dependencies(struct symbol *sym, struct cfdata *data);
> +static void add_choice_constraints(struct symbol *sym, struct cfdata *data);
> +static void add_invisible_constraints(struct symbol *sym, struct cfdata *data);
> +static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data);
> +static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data);
> +static void sym_add_nonbool_values_from_default_range(struct symbol *sym,
> +                                                     struct cfdata *data);
> +static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data);
> +static void sym_add_nonbool_prompt_constraint(struct symbol *sym,
> +                                             struct cfdata *data);
> +
> +static struct default_map *create_default_map_entry(struct fexpr *val,
> +                                                   struct pexpr *e);
> +static struct defm_list *get_defaults(struct symbol *sym, struct cfdata *data);
> +static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data);
> +static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data);
> +static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data);
> +static long sym_get_range_val(struct symbol *sym, int base);
> +
> +/* -------------------------------------- */
> +
> +/*
> + * build the constraints for each symbol
> + */
> +void get_constraints(struct cfdata *data)
> +{
> +       printd("Building constraints...");
> +
> +       init_constraints(data);
> +       get_constraints_bool(data);
> +       get_constraints_select(data);
> +       get_constraints_nonbool(data);
> +}
> +
> +/*
> + * need to go through the constraints once to find all "known values"
> + * for the non-Boolean symbols (and add them to sym->nb_vals for the given
> + * symbols).
> + * expr_calculate_pexpr_both and get_defaults have the side effect of creating
> + * known values.
> + */
> +static void init_constraints(struct cfdata *data)
> +{
> +       struct symbol *sym;
> +       struct property *p;
> +
> +       for_all_symbols(sym) {
> +               struct property *prompt;
> +
> +               if (sym->type == S_UNKNOWN)
> +                       continue;
> +
> +               if (sym_is_boolean(sym)) {
> +                       for_all_properties(sym, p, P_SELECT)
> +                               pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
> +                                                         data));
> +
> +                       for_all_properties(sym, p, P_IMPLY)
> +                               pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
> +                                                         data));



Does 'imply' give any constraint?








> +               }
> +
> +               if (sym->dir_dep.expr)
> +                       pexpr_put(expr_calculate_pexpr_both(sym->dir_dep.expr, data));
> +
> +               prompt = sym_get_prompt(sym);
> +               if (prompt != NULL && prompt->visible.expr) {
> +                       pexpr_put(expr_calculate_pexpr_both(prompt->visible.expr, data));
> +                       defm_list_destruct(get_defaults(sym, data));
> +               }
> +
> +               if (sym_is_nonboolean(sym)) {
> +                       const char *curr;
> +
> +                       for_all_defaults(sym, p) {
> +                               if (p == NULL)
> +                                       continue;
> +
> +                               sym_create_nonbool_fexpr(
> +                                       sym, p->expr->left.sym->name, data);
> +                       }
> +                       for_all_properties(sym, p, P_RANGE) {
> +                               if (p == NULL)
> +                                       continue;
> +
> +                               sym_create_nonbool_fexpr(
> +                                       sym, p->expr->left.sym->name, data);
> +                               sym_create_nonbool_fexpr(
> +                                       sym, p->expr->right.sym->name, data);
> +                       }
> +                       curr = sym_get_string_value(sym);
> +                       if (strcmp(curr, "") != 0)
> +                               sym_create_nonbool_fexpr(sym, (char *)curr,
> +                                                        data);
> +               }
> +
> +               if (sym->type == S_HEX || sym->type == S_INT)
> +                       sym_add_nonbool_values_from_default_range(sym, data);
> +       }
> +}
> +
> +/*
> + *  build constraints for boolean symbols
> + */
> +static void get_constraints_bool(struct cfdata *data)
> +{
> +       struct symbol *sym;
> +
> +       for_all_symbols(sym) {
> +               if (!sym_is_boolean(sym))
> +                       continue;
> +
> +               /* build tristate constraints */
> +               if (sym->type == S_TRISTATE)
> +                       build_tristate_constraint_clause(sym, data);
> +
> +               /* build constraints for select statements
> +                * need to treat choice symbols separately
> +                */
> +               if (!KCR_CMP) {
> +                       add_selects(sym, data);
> +               } else {
> +                       if (sym->rev_dep.expr && !sym_is_choice(sym) &&
> +                           !sym_is_choice_value(sym))
> +                               add_selects_kcr(sym, data);
> +               }
> +
> +               /* build constraints for dependencies for booleans */
> +               if (sym->dir_dep.expr && !sym_is_choice(sym) &&
> +                   !sym_is_choice_value(sym)) {
> +                       if (!KCR_CMP)
> +                               add_dependencies_bool(sym, data);
> +                       else
> +                               add_dependencies_bool_kcr(sym, data);
> +               }
> +
> +               /* build constraints for choice prompts */
> +               if (sym_is_choice(sym))
> +                       add_choice_prompt_cond(sym, data);
> +
> +               /* build constraints for dependencies (choice symbols and options) */
> +               if (sym_is_choice(sym) || sym_is_choice_value(sym))
> +                       add_choice_dependencies(sym, data);
> +
> +               /* build constraints for the choice groups */
> +               if (sym_is_choice(sym))
> +                       add_choice_constraints(sym, data);
> +
> +               /* build invisible constraints */
> +               add_invisible_constraints(sym, data);
> +       }
> +}
> +
> +/*
> + * build the constraints for select-variables
> + * skip non-Booleans, choice symbols/options och symbols without rev_dir
> + */
> +static void get_constraints_select(struct cfdata *data)
> +{
> +       struct symbol *sym;
> +
> +       for_all_symbols(sym) {
> +               struct pexpr *sel_y, *sel_m;
> +               struct pexpr *c1, *c2;
> +
> +               if (KCR_CMP)
> +                       continue;
> +
> +               if (!sym_is_boolean(sym))
> +                       continue;
> +
> +               if (sym_is_choice(sym) || sym_is_choice_value(sym))
> +                       continue;
> +
> +               if (!sym->rev_dep.expr)
> +                       continue;
> +
> +               if (sym->list_sel_y == NULL)
> +                       continue;
> +
> +               sel_y = pexpr_implies(pexf(sym->fexpr_sel_y),
> +                                          pexf(sym->fexpr_y), data,
> +                                          PEXPR_ARGX);
> +               sym_add_constraint(sym, sel_y, data);
> +
> +               c1 = pexpr_implies(pexf(sym->fexpr_sel_y), sym->list_sel_y,
> +                                       data, PEXPR_ARG1);
> +               sym_add_constraint(sym, c1, data);
> +
> +               /* only continue for tristates */
> +               if (sym->type == S_BOOLEAN)
> +                       continue;
> +
> +               sel_m = pexpr_implies(pexf(sym->fexpr_sel_m),
> +                                          sym_get_fexpr_both(sym, data), data,
> +                                          PEXPR_ARGX);
> +               sym_add_constraint(sym, sel_m, data);
> +
> +               c2 = pexpr_implies(pexf(sym->fexpr_sel_m), sym->list_sel_m,
> +                                       data, PEXPR_ARG1);
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(sel_y, sel_m, c1, c2);
> +       }
> +}
> +
> +/*
> + * build constraints for non-booleans
> + */
> +static void get_constraints_nonbool(struct cfdata *data)
> +{
> +       struct symbol *sym;
> +
> +       for_all_symbols(sym) {
> +               if (!sym_is_nonboolean(sym))
> +                       continue;
> +
> +               /* the symbol must have a value, if there is a prompt */
> +               if (sym_has_prompt(sym))
> +                       sym_add_nonbool_prompt_constraint(sym, data);
> +
> +               /* build the range constraints for int/hex */
> +               if (sym->type == S_HEX || sym->type == S_INT)
> +                       sym_add_range_constraints(sym, data);
> +
> +               /* build constraints for dependencies for non-booleans */
> +               if (sym->dir_dep.expr)
> +                       add_dependencies_nonbool(sym, data);
> +
> +               /* build invisible constraints */
> +               add_invisible_constraints(sym, data);
> +
> +               /* exactly one of the symbols must be true */
> +               sym_nonbool_at_least_1(sym, data);
> +               sym_nonbool_at_most_1(sym, data);
> +       }
> +}
> +
> +/*
> + * enforce tristate constraints
> + */
> +static void build_tristate_constraint_clause(struct symbol *sym,
> +                                            struct cfdata *data)
> +{
> +       struct pexpr *X, *X_m, *modules, *c;
> +
> +       if (sym->type != S_TRISTATE)
> +               return;
> +
> +       X = pexf(sym->fexpr_y);
> +       X_m = pexf(sym->fexpr_m);
> +       modules = pexf(modules_sym->fexpr_y);
> +
> +       /* -X v -X_m */
> +       c = pexpr_or(pexpr_not_share(X, data), pexpr_not_share(X_m, data),
> +                         data, PEXPR_ARGX);
> +       sym_add_constraint(sym, c, data);
> +
> +       /* X_m -> MODULES */
> +       if (modules_sym->fexpr_y != NULL) {
> +               struct pexpr *c2 = pexpr_implies_share(X_m, modules, data);
> +
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(c2);
> +       }
> +       PEXPR_PUT(X, X_m, modules, c);
> +}
> +
> +/*
> + * build the select constraints
> + * - RDep(X) implies X
> + */
> +static void add_selects_kcr(struct symbol *sym, struct cfdata *data)
> +{
> +       struct pexpr *rdep_y = expr_calculate_pexpr_y(sym->rev_dep.expr, data);
> +       struct pexpr *c1 = pexpr_implies(rdep_y, pexf(sym->fexpr_y), data,
> +                                             PEXPR_ARG2);
> +
> +       struct pexpr *rdep_both =
> +               expr_calculate_pexpr_both(sym->rev_dep.expr, data);
> +       struct pexpr *c2 = pexpr_implies(
> +               rdep_both, sym_get_fexpr_both(sym, data), data, PEXPR_ARG2);
> +
> +       sym_add_constraint(sym, c1, data);
> +       sym_add_constraint(sym, c2, data);
> +       PEXPR_PUT(rdep_y, c1, rdep_both, c2);
> +}
> +
> +/*
> + * build the select constraints simplified
> + * - RDep(X) implies X
> + */
> +static void add_selects(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *p;
> +
> +       if (!sym_is_boolean(sym))
> +               return;
> +
> +       for_all_properties(sym, p, P_SELECT) {
> +               struct symbol *selected = p->expr->left.sym;
> +               struct pexpr *cond_y, *cond_both;
> +
> +               if (selected->type == S_UNKNOWN)
> +                       continue;
> +
> +               if (!selected->rev_dep.expr)
> +                       continue;
> +
> +               if (p->visible.expr) {
> +                       cond_y = expr_calculate_pexpr_y(p->visible.expr, data);
> +                       cond_both = expr_calculate_pexpr_both(p->visible.expr,
> +                                                             data);
> +               } else {
> +                       cond_y = pexf(data->constants->const_true);
> +                       cond_both = pexf(data->constants->const_true);
> +               }
> +
> +               if (selected->type == S_BOOLEAN) {
> +                       /* imply that symbol is selected to y */
> +                       struct pexpr *e1 = pexpr_and(
> +                               cond_both, sym_get_fexpr_both(sym, data), data,
> +                               PEXPR_ARG2);
> +                       struct pexpr *c1 = pexpr_implies(
> +                               e1, pexf(selected->fexpr_sel_y), data,
> +                               PEXPR_ARG2);
> +
> +                       sym_add_constraint(selected, c1, data);
> +
> +                       if (selected->list_sel_y == NULL)
> +                               selected->list_sel_y = pexpr_get(e1);
> +                       else
> +                               selected->list_sel_y =
> +                                       pexpr_or(selected->list_sel_y, e1, data,
> +                                                PEXPR_ARG1);
> +                       PEXPR_PUT(e1, c1);
> +               }
> +
> +               if (selected->type == S_TRISTATE) {
> +                       struct pexpr *e2, *e3, *c2, *c3;
> +
> +                       /* imply that symbol is selected to y */
> +                       e2 = pexpr_and(cond_y, pexf(sym->fexpr_y), data,
> +                                           PEXPR_ARG2);
> +                       c2 = pexpr_implies(e2, pexf(selected->fexpr_sel_y),
> +                                               data, PEXPR_ARG2);
> +                       sym_add_constraint(selected, c2, data);
> +
> +                       if (selected->list_sel_y == NULL)
> +                               selected->list_sel_y = pexpr_get(e2);
> +                       else
> +                               selected->list_sel_y =
> +                                       pexpr_or(selected->list_sel_y, e2,
> +                                                     data, PEXPR_ARG1);
> +
> +                       /* imply that symbol is selected to m */
> +                       e3 = pexpr_and(cond_both,
> +                                           sym_get_fexpr_both(sym, data), data,
> +                                           PEXPR_ARG2);
> +                       c3 = pexpr_implies(e3, pexf(selected->fexpr_sel_m),
> +                                               data, PEXPR_ARG2);
> +                       sym_add_constraint(selected, c3, data);
> +
> +                       if (selected->list_sel_m == NULL)
> +                               selected->list_sel_m = pexpr_get(e3);
> +                       else
> +                               selected->list_sel_m =
> +                                       pexpr_or(selected->list_sel_m, e3,
> +                                                     data, PEXPR_ARG1);
> +                       PEXPR_PUT(e2, c2, e3, c3);
> +               }
> +               PEXPR_PUT(cond_y, cond_both);
> +       }
> +}
> +
> +/*
> + * build the dependency constraints for booleans
> + *  - X implies Dep(X) or RDep(X)
> + */
> +static void add_dependencies_bool(struct symbol *sym, struct cfdata *data)
> +{
> +       struct pexpr *dep_both;
> +       struct pexpr *visible_m;
> +       struct pexpr *visible_y;
> +       struct pexpr *visible_both;
> +       struct property *prompt;
> +       struct pexpr *has_prompt;
> +       struct pexpr *sel_y;
> +
> +       if (!sym_is_boolean(sym) || !sym->dir_dep.expr)
> +               return;
> +
> +       prompt = sym_get_prompt(sym);
> +       if (!prompt) {
> +               visible_m = pexf(data->constants->const_false);
> +               visible_y = pexpr_get(visible_m);
> +               visible_both = pexpr_get(visible_m);
> +       } else if (prompt->expr == NULL) {
> +               visible_m = pexf(data->constants->const_true);
> +               visible_y = pexpr_get(visible_m);
> +               visible_both = pexpr_get(visible_m);
> +       } else {
> +               visible_m = expr_calculate_pexpr_m(prompt->expr, data);
> +               visible_y = expr_calculate_pexpr_y(prompt->expr, data);
> +               visible_both = pexpr_or_share(visible_y, visible_m, data);
> +       }
> +
> +       dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
> +
> +       sel_y = sym->rev_dep.expr ? pexf(sym->fexpr_sel_y) :
> +                                   pexf(data->constants->const_false);
> +       has_prompt = pexpr_get(visible_both);
> +       has_prompt = pexpr_and(
> +                       has_prompt,
> +                       pexpr_not(pexpr_and_share(sel_y, visible_m, data),
> +                               data),
> +                       data, PEXPR_ARGX);
> +
> +       if (sym->type == S_TRISTATE) {
> +               struct pexpr *c1;
> +               struct pexpr *c2;
> +               struct pexpr *dep_y =
> +                       expr_calculate_pexpr_y(sym->dir_dep.expr, data);
> +               struct pexpr *sel_both = sym_get_fexpr_sel_both(sym, data);
> +               struct pexpr *cond_y1;
> +               struct pexpr *cond_y2;
> +               struct pexpr *cond_y;
> +               struct pexpr *cond_m1;
> +               struct pexpr *cond_m2;
> +               struct pexpr *cond_m;
> +
> +               cond_y1 = pexpr_implies(pexpr_not_share(has_prompt, data),
> +                                      pexpr_or_share(dep_y, sel_y, data), data,
> +                                      PEXPR_ARGX);
> +               cond_y2 = pexpr_implies_share(has_prompt, visible_y, data);
> +               cond_y = pexpr_and_share(cond_y1, cond_y2, data);
> +               cond_m1 =
> +                       pexpr_implies(pexpr_not_share(has_prompt, data),
> +                                     pexpr_or_share(dep_both, sel_both, data),
> +                                     data, PEXPR_ARGX);
> +               cond_m2 = pexpr_implies(has_prompt,
> +                                       pexpr_not_share(sel_y, data), data,
> +                                       PEXPR_ARG2);
> +               cond_m = pexpr_and_share(cond_m1, cond_m2, data);
> +               c1 = pexpr_implies(pexf(sym->fexpr_y), cond_y, data,
> +                                  PEXPR_ARG1);
> +               c2 = pexpr_implies(pexf(sym->fexpr_m), cond_m, data,
> +                                  PEXPR_ARG1);
> +
> +               sym_add_constraint(sym, c1, data);
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(c1, c2, dep_y, sel_both, cond_y1,
> +                         cond_y2, cond_y, cond_m1, cond_m2, cond_m);
> +       } else if (sym->type == S_BOOLEAN) {
> +               struct pexpr *cond1;
> +               struct pexpr *cond2;
> +               struct pexpr *c;
> +
> +               cond1 = pexpr_implies(pexpr_not_share(has_prompt, data),
> +                                     pexpr_or(dep_both, pexf(sym->fexpr_m),
> +                                              data, PEXPR_ARG2),
> +                                     data, PEXPR_ARGX);
> +               cond2 = pexpr_implies_share(has_prompt, visible_y, data);
> +               c = pexpr_implies(pexf(sym->fexpr_y),
> +                                 pexpr_and_share(cond1, cond2, data), data,
> +                                 PEXPR_ARGX);
> +
> +               sym_add_constraint(sym, c, data);
> +               PEXPR_PUT(c, cond1, cond2);
> +       }
> +       PEXPR_PUT(dep_both, has_prompt, sel_y, visible_y, visible_m, visible_both);
> +}
> +
> +/*
> + * build the dependency constraints for booleans (KCR)
> + *  - X implies Dep(X) or RDep(X)
> + */
> +static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data)
> +{
> +       struct pexpr *dep_both, *sel_both;
> +
> +       if (!sym_is_boolean(sym) || !sym->dir_dep.expr)
> +               return;
> +
> +       dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
> +
> +       sel_both = sym->rev_dep.expr ?
> +                          expr_calculate_pexpr_both(sym->rev_dep.expr, data) :
> +                          pexf(data->constants->const_false);
> +
> +       if (sym->type == S_TRISTATE) {
> +               struct pexpr *c1;
> +               struct pexpr *c2;
> +               {
> +                       struct pexpr *dep_y =
> +                               expr_calculate_pexpr_y(sym->dir_dep.expr, data);
> +                       struct pexpr *sel_y =
> +                               sym->rev_dep.expr ?
> +                                       expr_calculate_pexpr_y(
> +                                               sym->rev_dep.expr, data) :
> +                                       pexf(data->constants->const_false);
> +                       c1 = pexpr_implies(pexf(sym->fexpr_y),
> +                                               pexpr_or(dep_y, sel_y,
> +                                                             data, PEXPR_ARGX),
> +                                               data, PEXPR_ARGX);
> +               }
> +               c2 = pexpr_implies(pexf(sym->fexpr_m),
> +                                       pexpr_or_share(dep_both, sel_both,
> +                                                      data),
> +                                       data, PEXPR_ARGX);
> +
> +               sym_add_constraint(sym, c1, data);
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(c1, c2);
> +       } else if (sym->type == S_BOOLEAN) {
> +               struct pexpr *c = pexpr_implies(
> +                       pexf(sym->fexpr_y),
> +                       pexpr_or_share(dep_both, sel_both, data), data,
> +                       PEXPR_ARGX);
> +
> +               sym_add_constraint(sym, c, data);
> +               PEXPR_PUT(c);
> +       }
> +
> +       PEXPR_PUT(dep_both, sel_both);
> +}
> +
> +/*
> + * build the dependency constraints for non-booleans
> + *
> + * sym is not 'n' implies `sym->dir_dep`
> + */
> +static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data)
> +{
> +       struct pexpr *dep_both;
> +       struct pexpr *nb_vals; // "sym is set to some value" / "sym is not 'n'"
> +       struct fexpr_node *node;
> +       struct pexpr *c;
> +
> +       if (!sym_is_nonboolean(sym) || !sym->dir_dep.expr || sym->rev_dep.expr)
> +               return;
> +
> +       dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
> +
> +       nb_vals = pexf(data->constants->const_false);
> +       /* can skip the first non-boolean value, since this is 'n' */
> +       fexpr_list_for_each(node, sym->nb_vals) {
> +               if (node->prev == NULL)
> +                       continue;
> +
> +               nb_vals = pexpr_or(nb_vals, pexf(node->elem), data,
> +                                       PEXPR_ARGX);
> +       }
> +
> +       c = pexpr_implies(nb_vals, dep_both, data, PEXPR_ARGX);
> +       sym_add_constraint(sym, c, data);
> +       pexpr_put(c);
> +}
> +
> +/*
> + * build the constraints for the choice prompt
> + */
> +static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prompt;
> +       struct pexpr *promptCondition;
> +       struct pexpr *fe_both;
> +       struct pexpr *pr_cond;
> +       struct pexpr *req_cond;
> +
> +       if (!sym_is_boolean(sym))
> +               return;
> +
> +       prompt = sym_get_prompt(sym);
> +       if (prompt == NULL)
> +               return;
> +
> +       promptCondition =
> +               prompt->visible.expr ?
> +                       expr_calculate_pexpr_both(prompt->visible.expr, data) :
> +                       pexf(data->constants->const_true);
> +       fe_both = sym_get_fexpr_both(sym, data);
> +       req_cond = pexpr_implies_share(promptCondition, fe_both, data);
> +       sym_add_constraint(sym, req_cond, data);
> +       pr_cond = pexpr_implies_share(fe_both, promptCondition, data);
> +       sym_add_constraint(sym, pr_cond, data);
> +       PEXPR_PUT(promptCondition, fe_both, req_cond, pr_cond);
> +}
> +
> +/*
> + * build constraints for dependencies (choice symbols and options)
> + */
> +static void add_choice_dependencies(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prompt;
> +       struct expr *to_parse;
> +       struct pexpr *dep_both;
> +
> +       if (!sym_is_choice(sym) || !sym_is_choice_value(sym))
> +               return;
> +
> +       prompt = sym_get_prompt(sym);
> +       if (prompt == NULL)
> +               return;
> +
> +       if (sym_is_choice(sym)) {
> +               if (!prompt->visible.expr)
> +                       return;
> +               to_parse = prompt->visible.expr;
> +       } else {
> +               if (!sym->dir_dep.expr)
> +                       return;
> +               to_parse = sym->dir_dep.expr;
> +       }
> +
> +       dep_both = expr_calculate_pexpr_both(to_parse, data);
> +
> +       if (sym->type == S_TRISTATE) {
> +               struct pexpr *dep_y = expr_calculate_pexpr_y(to_parse, data);
> +               struct pexpr *c1 = pexpr_implies(pexf(sym->fexpr_y), dep_y,
> +                                                     data, PEXPR_ARG1);
> +               struct pexpr *c2 = pexpr_implies(
> +                       pexf(sym->fexpr_m), dep_both, data, PEXPR_ARG1);
> +
> +               sym_add_constraint_eq(sym, c1, data);
> +               sym_add_constraint_eq(sym, c2, data);
> +               PEXPR_PUT(dep_y, c1, c2);
> +       } else if (sym->type == S_BOOLEAN) {
> +               struct pexpr *c = pexpr_implies(
> +                       pexf(sym->fexpr_y), dep_both, data, PEXPR_ARG1);
> +
> +               sym_add_constraint_eq(sym, c, data);
> +               pexpr_put(c);
> +       }
> +       pexpr_put(dep_both);
> +}
> +
> +/*
> + * build constraints for the choice groups
> + */
> +static void add_choice_constraints(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prompt;
> +       struct symbol *choice, *choice2;
> +       struct sym_node *node, *node2;
> +       struct sym_list *items, *promptItems;
> +       struct pexpr *c1;
> +       struct menu *menu_ptr, *choiceval_menu;
> +
> +       if (!sym_is_boolean(sym))
> +               return;
> +
> +       prompt = sym_get_prompt(sym);
> +       if (prompt == NULL)
> +               return;
> +
> +       /* create list of all choice options */
> +       items = sym_list_init();
> +       /* create list of choice options with a prompt */
> +       promptItems = sym_list_init();
> +
> +       for_all_choices(sym, choiceval_menu, menu_ptr) {
> +               choice = choiceval_menu->sym;
> +
> +               sym_list_add(items, choice);
> +               if (sym_get_prompt(choice) != NULL)
> +                       sym_list_add(promptItems, choice);
> +       }
> +
> +       /* if the choice is set to yes, at least one child must be set to yes */
> +       c1 = NULL;
> +       sym_list_for_each(node, promptItems) {
> +               choice = node->elem;
> +               c1 = node->prev == NULL ?
> +                            pexf(choice->fexpr_y) :
> +                            pexpr_or(c1, pexf(choice->fexpr_y), data,
> +                                          PEXPR_ARGX);
> +       }
> +       if (c1 != NULL) {
> +               struct pexpr *c2 = pexpr_implies(pexf(sym->fexpr_y), c1,
> +                                                     data, PEXPR_ARG1);
> +
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(c1, c2);
> +       }
> +
> +       /* every choice option (even those without a prompt) implies the choice */
> +       sym_list_for_each(node, items) {
> +               choice = node->elem;
> +               c1 = pexpr_implies(sym_get_fexpr_both(choice, data),
> +                                       sym_get_fexpr_both(sym, data), data,
> +                                       PEXPR_ARGX);
> +               sym_add_constraint(sym, c1, data);
> +               pexpr_put(c1);
> +       }
> +
> +       /* choice options can only select mod, if the entire choice is mod */
> +       if (sym->type == S_TRISTATE) {
> +               sym_list_for_each(node, items) {
> +                       choice = node->elem;
> +                       if (choice->type == S_TRISTATE) {
> +                               c1 = pexpr_implies(pexf(choice->fexpr_m),
> +                                                       pexf(sym->fexpr_m),
> +                                                       data, PEXPR_ARGX);
> +                               sym_add_constraint(sym, c1, data);
> +                               pexpr_put(c1);
> +                       }
> +               }
> +       }
> +
> +       /* tristate options cannot be m, if the choice symbol is boolean */
> +       if (sym->type == S_BOOLEAN) {
> +               sym_list_for_each(node, items) {
> +                       choice = node->elem;
> +                       if (choice->type == S_TRISTATE) {
> +                               struct pexpr *e = pexpr_not(pexf(choice->fexpr_m),
> +                                                      data);
> +                               sym_add_constraint(sym, e, data);
> +                               pexpr_put(e);
> +                       }
> +               }
> +       }
> +
> +       /* all choice options are mutually exclusive for yes */
> +       sym_list_for_each(node, promptItems) {
> +               choice = node->elem;
> +               for (struct sym_node *node2 = node->next; node2 != NULL;
> +                    node2 = node2->next) {
> +                       choice2 = node2->elem;
> +                       c1 = pexpr_or(
> +                               pexpr_not(pexf(choice->fexpr_y), data),
> +                               pexpr_not(pexf(choice2->fexpr_y), data),
> +                               data, PEXPR_ARGX);
> +                       sym_add_constraint(sym, c1, data);
> +                       pexpr_put(c1);
> +               }
> +       }
> +
> +       /* if one choice option with a prompt is set to yes,
> +        * then no other option may be set to mod
> +        */
> +       if (sym->type == S_TRISTATE) {
> +               sym_list_for_each(node, promptItems) {
> +                       struct sym_list *tmp;
> +
> +                       choice = node->elem;
> +
> +                       tmp = sym_list_init();
> +                       for (struct sym_node *node2 = node->next; node2 != NULL;
> +                            node2 = node2->next) {
> +                               choice2 = node2->elem;
> +                               if (choice2->type == S_TRISTATE)
> +                                       sym_list_add(tmp, choice2);
> +                       }
> +                       if (tmp->size == 0)
> +                               continue;
> +
> +                       sym_list_for_each(node2, tmp) {
> +                               choice2 = node2->elem;
> +                               if (node2->prev == NULL)
> +                                       c1 = pexpr_not(
> +                                               pexf(choice2->fexpr_m), data);
> +                               else
> +                                       c1 = pexpr_and(
> +                                               c1,
> +                                               pexpr_not(
> +                                                       pexf(choice2->fexpr_m),
> +                                                       data),
> +                                               data, PEXPR_ARGX);
> +                       }
> +                       c1 = pexpr_implies(pexf(choice->fexpr_y), c1, data,
> +                                               PEXPR_ARGX);
> +                       sym_add_constraint(sym, c1, data);
> +                       pexpr_put(c1);
> +               }
> +       }
> +       sym_list_free(promptItems);
> +       sym_list_free(items);
> +}
> +
> +/*
> + * build the constraints for invisible options such as defaults
> + */
> +static void add_invisible_constraints(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prompt = sym_get_prompt(sym);
> +       struct pexpr *promptCondition_both, *promptCondition_yes, *noPromptCond;
> +       struct pexpr *npc;
> +       struct defm_list *defaults;
> +       struct pexpr *default_y, *default_m, *default_both;
> +
> +       /* no constraints for the prompt, nothing to do here */
> +       if (prompt != NULL && !prompt->visible.expr)
> +               return;
> +
> +       if (prompt == NULL) {
> +               promptCondition_both = pexf(data->constants->const_false);
> +               promptCondition_yes = pexf(data->constants->const_false);
> +               noPromptCond = pexf(data->constants->const_true);
> +       } else {
> +               struct property *p;
> +
> +               promptCondition_both = pexf(data->constants->const_false);
> +               promptCondition_yes = pexf(data->constants->const_false);
> +
> +               /* some symbols have multiple prompts */
> +               for_all_prompts(sym, p) {
> +                       promptCondition_both =
> +                               pexpr_or(promptCondition_both,
> +                                             expr_calculate_pexpr_both(
> +                                                     p->visible.expr, data),
> +                                             data, PEXPR_ARGX);
> +                       promptCondition_yes = pexpr_or(
> +                               promptCondition_yes,
> +                               expr_calculate_pexpr_y(p->visible.expr, data),
> +                               data, PEXPR_ARGX);
> +               }
> +               noPromptCond = pexpr_not_share(promptCondition_both, data);
> +       }
> +
> +       if (NPC_OPTIMISATION) {
> +               struct fexpr *npc_fe =
> +                       fexpr_create(data->sat_variable_nr++, FE_NPC, "");
> +
> +               if (sym_is_choice(sym))
> +                       str_append(&npc_fe->name, "Choice_");
> +
> +               str_append(&npc_fe->name, sym_get_name(sym));
> +               str_append(&npc_fe->name, "_NPC");
> +               sym->noPromptCond = npc_fe;
> +               fexpr_add_to_satmap(npc_fe, data);
> +
> +               npc = pexf(npc_fe);
> +
> +               if (!sym_is_choice_value(sym) && !sym_is_choice(sym)) {
> +                       struct pexpr *c =
> +                               pexpr_implies_share(noPromptCond, npc, data);
> +                       sym_add_constraint(sym, c, data);
> +                       pexpr_put(c);
> +               }
> +       } else {
> +               npc = pexpr_get(noPromptCond);
> +       }
> +
> +       defaults = get_defaults(sym, data);
> +       default_y = get_default_y(defaults, data);
> +       default_m = get_default_m(defaults, data);
> +       default_both = pexpr_or_share(default_y, default_m, data);
> +
> +       /* tristate elements are only selectable as yes, if they are visible as yes */
> +       if (sym->type == S_TRISTATE) {
> +               struct pexpr *e1 = pexpr_implies(
> +                       promptCondition_both,
> +                       pexpr_implies(pexf(sym->fexpr_y),
> +                                          promptCondition_yes, data,
> +                                          PEXPR_ARG1),
> +                       data, PEXPR_ARG2);
> +
> +               sym_add_constraint(sym, e1, data);
> +               pexpr_put(e1);
> +       }
> +
> +       /* if invisible and off by default, then a symbol can only be deactivated by its reverse
> +        * dependencies
> +        */
> +       if (sym->type == S_TRISTATE) {
> +               struct pexpr *sel_y, *sel_m, *sel_both;
> +               struct pexpr *c1, *c2, *c3;
> +               struct pexpr *d1, *d2, *d3;
> +               struct pexpr *e1, *e2, *e3;
> +
> +               if (sym->fexpr_sel_y != NULL) {
> +                       sel_y = pexpr_implies(pexf(sym->fexpr_y),
> +                                                  pexf(sym->fexpr_sel_y), data,
> +                                                  PEXPR_ARGX);
> +                       sel_m = pexpr_implies(pexf(sym->fexpr_m),
> +                                                  pexf(sym->fexpr_sel_m), data,
> +                                                  PEXPR_ARGX);
> +                       sel_both = pexpr_implies(
> +                               pexf(sym->fexpr_y),
> +                               pexpr_or(pexf(sym->fexpr_sel_m),
> +                                             pexf(sym->fexpr_sel_y), data,
> +                                             PEXPR_ARGX),
> +                               data, PEXPR_ARGX);
> +               } else {
> +                       sel_y = pexpr_not(pexf(sym->fexpr_y), data);
> +                       sel_m = pexpr_not(pexf(sym->fexpr_m), data);
> +                       sel_both = pexpr_get(sel_y);
> +               }
> +
> +               c1 = pexpr_implies(pexpr_not_share(default_y, data), sel_y,
> +                                       data, PEXPR_ARG1);
> +               c2 = pexpr_implies(pexf(modules_sym->fexpr_y), c1, data,
> +                                       PEXPR_ARG1);
> +               c3 = pexpr_implies_share(npc, c2, data);
> +               sym_add_constraint(sym, c3, data);
> +
> +               d1 = pexpr_implies(pexpr_not_share(default_m, data), sel_m,
> +                                       data, PEXPR_ARG1);
> +               d2 = pexpr_implies(pexf(modules_sym->fexpr_y), d1, data,
> +                                       PEXPR_ARG1);
> +               d3 = pexpr_implies_share(npc, d2, data);
> +               sym_add_constraint(sym, d3, data);
> +
> +               e1 = pexpr_implies(pexpr_not_share(default_both, data),
> +                                       sel_both, data, PEXPR_ARG1);
> +               e2 = pexpr_implies(
> +                       pexpr_not(pexf(modules_sym->fexpr_y), data), e1,
> +                       data, PEXPR_ARG1);
> +               e3 = pexpr_implies_share(npc, e2, data);
> +               sym_add_constraint(sym, e3, data);
> +               PEXPR_PUT(sel_y, sel_m, sel_both, c1, c2, c3, d1, d2, d3, e1,
> +                         e2, e3);
> +       } else if (sym->type == S_BOOLEAN) {
> +               struct pexpr *sel_y;
> +               struct pexpr *e1, *e2;
> +
> +               if (sym->fexpr_sel_y != NULL)
> +                       sel_y = pexpr_implies(pexf(sym->fexpr_y),
> +                                                  pexf(sym->fexpr_sel_y), data,
> +                                                  PEXPR_ARGX);
> +               else
> +                       sel_y = pexpr_not(pexf(sym->fexpr_y), data);
> +
> +               e1 = pexpr_implies(pexpr_not_share(default_both, data),
> +                                       sel_y, data, PEXPR_ARG1);
> +               e2 = pexpr_implies_share(npc, e1, data);
> +
> +               sym_add_constraint_eq(sym, e2, data);
> +               PEXPR_PUT(sel_y, e1, e2);
> +       } else {
> +               /* if non-boolean is invisible and no default's condition is
> +                * fulfilled, then the symbol is not set
> +                */
> +               struct pexpr *default_any = get_default_any(sym, data);
> +               struct pexpr *e1 = pexf(data->constants->const_true);
> +               struct pexpr *e2, *e3;
> +
> +               /* e1 = "sym is not set" */
> +               for (struct fexpr_node *node = sym->nb_vals->head->next;
> +                    node != NULL; node = node->next)
> +                       e1 = pexpr_and(
> +                               e1, pexpr_not(pexf(node->elem), data),
> +                               data, PEXPR_ARGX);
> +
> +               e2 = pexpr_implies(pexpr_not_share(default_any, data), e1,
> +                                       data, PEXPR_ARG1);
> +               e3 = pexpr_implies_share(npc, e2, data);
> +
> +               sym_add_constraint(sym, e3, data);
> +               PEXPR_PUT(default_any, e1, e2, e3);
> +       }
> +
> +       /* if invisible and on by default, then a symbol can only be deactivated by its
> +        * dependencies
> +        */
> +       if (defaults->size == 0) {
> +               // nothing to do
> +       } else if (sym->type == S_TRISTATE) {
> +               struct pexpr *e1;
> +               struct pexpr *e2;
> +
> +               e1 = pexpr_implies(npc,
> +                                       pexpr_implies(default_y,
> +                                                          pexf(sym->fexpr_y),
> +                                                          data, PEXPR_ARG2),
> +                                       data, PEXPR_ARG2);
> +               sym_add_constraint(sym, e1, data);
> +
> +               e2 = pexpr_implies(
> +                       npc,
> +                       pexpr_implies(default_m,
> +                                          sym_get_fexpr_both(sym, data),
> +                                          data, PEXPR_ARG2),
> +                       data, PEXPR_ARG2);
> +               sym_add_constraint(sym, e2, data);
> +               PEXPR_PUT(e1, e2);
> +       } else if (sym->type == S_BOOLEAN) {
> +               struct pexpr *c;
> +               struct pexpr *c2;
> +
> +               c = pexpr_implies(default_both, pexf(sym->fexpr_y), data,
> +                                      PEXPR_ARG2);
> +
> +               // TODO tristate choice hack
> +
> +               c2 = pexpr_implies_share(npc, c, data);
> +               sym_add_constraint(sym, c2, data);
> +               PEXPR_PUT(c, c2);
> +       } else {
> +               /* if non-boolean invisible, then it assumes the correct
> +                * default (if any).
> +                */
> +               struct defm_node *node;
> +               struct pexpr *cond, *c;
> +               struct fexpr *f;
> +
> +               defm_list_for_each(node, defaults) {
> +                       f = node->elem->val;
> +                       cond = node->elem->e;
> +                       c = pexpr_implies(npc,
> +                                              pexpr_implies(cond, pexf(f), data, PEXPR_ARG2),
> +                                              data, PEXPR_ARG2);
> +                       sym_add_constraint(sym, c, data);
> +                       pexpr_put(c);
> +               }
> +       }
> +
> +       PEXPR_PUT(promptCondition_yes, promptCondition_both, noPromptCond, npc,
> +                 default_y, default_m, default_both);
> +       defm_list_destruct(defaults);
> +}
> +
> +/*
> + * add the known values from the default and range properties
> + */
> +static void sym_add_nonbool_values_from_default_range(struct symbol *sym,
> +                                                     struct cfdata *data)
> +{
> +       struct property *p;
> +
> +       for_all_defaults(sym, p) {
> +               if (p == NULL)
> +                       continue;
> +
> +               /* add the value to known values, if it doesn't exist yet */
> +               sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data);
> +       }
> +
> +       for_all_properties(sym, p, P_RANGE) {
> +               if (p == NULL)
> +                       continue;
> +
> +               /* add the values to known values, if they don't exist yet */
> +               sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data);
> +               sym_create_nonbool_fexpr(sym, p->expr->right.sym->name, data);
> +       }
> +}
> +
> +/*
> + * build the range constraints for int/hex:
> + * For each range and each value in `sym->nb_vals` that's not in the range:
> + *     If the range's condition is fulfilled, then sym can't have this value.
> + */
> +static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prop;
> +       struct pexpr *prevs;
> +       struct pexpr *propCond;
> +       struct pexpr_list *prevCond; // list of all conditions of the ranges
> +               // from the previous iterations
> +       prevCond = pexpr_list_init();
> +
> +       for_all_properties(sym, prop, P_RANGE) {
> +               int base;
> +               long long range_min, range_max, tmp;
> +               struct fexpr_node *node;
> +
> +               if (prop == NULL)
> +                       continue;
> +
> +               prevs = pexf(data->constants->const_true);
> +               propCond = prop_get_condition(prop, data);
> +
> +               // construct prevs as "none of the previous ranges' conditions
> +               // were fulfilled but this range's condition is"
> +               if (prevCond->size == 0) {
> +                       pexpr_put(prevs);
> +                       prevs = pexpr_get(propCond);
> +;
> +               } else {
> +                       struct pexpr_node *node;
> +
> +                       pexpr_list_for_each(node, prevCond)
> +                               prevs = pexpr_and(pexpr_not_share(node->elem,
> +                                                                 data),
> +                                                 prevs, data, PEXPR_ARGX);
> +
> +                       prevs = pexpr_and(propCond, prevs, data,
> +                                              PEXPR_ARG2);
> +               }
> +               pexpr_list_add(prevCond, pexpr_get(propCond));
> +
> +               switch (sym->type) {
> +               case S_INT:
> +                       base = 10;
> +                       break;
> +               case S_HEX:
> +                       base = 16;
> +                       break;
> +               default:
> +                       return;
> +               }
> +
> +               range_min = sym_get_range_val(prop->expr->left.sym, base);
> +               range_max = sym_get_range_val(prop->expr->right.sym, base);
> +
> +               /* can skip the first non-boolean value, since this is 'n' */
> +               fexpr_list_for_each(node, sym->nb_vals) {
> +                       struct pexpr *not_nb_val;
> +                       struct pexpr *c;
> +
> +                       if (node->prev == NULL)
> +                               continue;
> +
> +                       tmp = strtoll(str_get(&node->elem->nb_val), NULL, base);
> +
> +                       /* known value is in range, nothing to do here */
> +                       if (tmp >= range_min && tmp <= range_max)
> +                               continue;
> +
> +                       not_nb_val = pexpr_not(pexf(node->elem), data);
> +                       c = pexpr_implies_share(prevs, not_nb_val, data);
> +                       sym_add_constraint(sym, c, data);
> +                       PEXPR_PUT(not_nb_val, c);
> +               }
> +               PEXPR_PUT(prevs, propCond);
> +       }
> +
> +       pexpr_list_free_put(prevCond);
> +
> +}
> +
> +/*
> + * at least 1 of the known values for a non-boolean symbol must be true
> + */
> +static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data)
> +{
> +       struct pexpr *e = NULL;
> +       struct fexpr_node *node;
> +
> +       if (!sym_is_nonboolean(sym))
> +               return;
> +
> +       fexpr_list_for_each(node, sym->nb_vals) {
> +               if (node->prev == NULL)
> +                       e = pexf(node->elem);
> +               else
> +                       e = pexpr_or(e, pexf(node->elem), data, PEXPR_ARGX);
> +       }
> +       sym_add_constraint(sym, e, data);
> +       pexpr_put(e);
> +}
> +
> +/*
> + * at most 1 of the known values for a non-boolean symbol can be true
> + */
> +static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data)
> +{
> +       struct fexpr_node *node1;
> +
> +       if (!sym_is_nonboolean(sym))
> +               return;
> +
> +       /* iterate over all subsets of sym->nb_vals of size 2 */
> +       fexpr_list_for_each(node1, sym->nb_vals) {
> +               struct pexpr *e1 = pexf(node1->elem);
> +
> +               for (struct fexpr_node *node2 = node1->next; node2 != NULL;
> +                    node2 = node2->next) {
> +                       struct pexpr *e2 = pexf(node2->elem);
> +                       struct pexpr *e = pexpr_or(pexpr_not_share(e1, data),
> +                                                  pexpr_not_share(e2, data),
> +                                                  data, PEXPR_ARGX);
> +
> +                       sym_add_constraint(sym, e, data);
> +                       PEXPR_PUT(e, e2);
> +               }
> +               pexpr_put(e1);
> +       }
> +}
> +
> +/*
> + * a visible prompt for a non-boolean implies a value for the symbol
> + */
> +static void sym_add_nonbool_prompt_constraint(struct symbol *sym,
> +                                             struct cfdata *data)
> +{
> +       struct property *prompt;
> +       struct pexpr *promptCondition;
> +       struct pexpr *n;
> +       struct pexpr *c = NULL;
> +
> +       prompt = sym_get_prompt(sym);
> +       if (prompt == NULL)
> +               return;
> +
> +       promptCondition = prop_get_condition(prompt, data);
> +       n = pexf(sym_get_nonbool_fexpr(sym, "n"));
> +
> +       if (n->type != PE_SYMBOL || n->left.fexpr == NULL)
> +               goto cleanup;
> +
> +       c = pexpr_implies(promptCondition, pexpr_not_share(n, data), data,
> +                         PEXPR_ARG2);
> +
> +       sym_add_constraint(sym, c, data);
> +
> +cleanup:
> +       PEXPR_PUT(n, promptCondition, c);
> +}
> +
> +static struct default_map *create_default_map_entry(struct fexpr *val,
> +                                                   struct pexpr *e)
> +{
> +       struct default_map *map = malloc(sizeof(struct default_map));
> +
> +       pexpr_get(e);
> +       map->val = val;
> +       map->e = e;
> +
> +       return map;
> +}
> +
> +/**
> + * findDefaultEntry()
> + * @val: Value that the entry must have
> + * @defaults: List of defaults to search in
> + * @constants: To get ``constants->const_false`` from
> + *
> + * Finds an entry in @defaults whose &default_map.val attribute is the same
> + * pointer as the @val argument.
> + *
> + * Return: The condition &default_map.e of the found entry, or
> + * ``pexf(constants->const_false)`` if none was found. To be pexpr_put() by the
> + * caller.
> + */
> +static struct pexpr *findDefaultEntry(struct fexpr *val,
> +                                     struct defm_list *defaults,
> +                                     struct constants *constants)
> +{
> +       struct defm_node *node;
> +
> +       defm_list_for_each(node, defaults) {
> +               if (val == node->elem->val) {
> +                       pexpr_get(node->elem->e);
> +                       return node->elem->e;
> +               }
> +       }
> +
> +       return pexf(constants->const_false);
> +}
> +
> +/*
> + * accumulated during execution of add_defaults(), a disjunction of the
> + * conditions for all default props of a symbol
> + */
> +static struct pexpr *covered;
> +
> +static bool is_tri_as_num(struct symbol *sym)
> +{
> +       if (!sym->name)
> +               return false;
> +
> +       return !strcmp(sym->name, "0")
> +               || !strcmp(sym->name, "1")
> +               || !strcmp(sym->name, "2");
> +}
> +
> +/**
> + * add_to_default_map() - Add to or update an entry in a default list
> + * @entry: Will be consumed by this function, i.e. the caller should and need
> + * only access @entry via @defaults.
> + */
> +static void add_to_default_map(struct defm_list *defaults,
> +                              struct default_map *entry, struct symbol *sym)
> +{
> +       /* as this is a map, the entry must be replaced if it already exists */
> +       if (sym_is_boolean(sym)) {
> +               struct default_map *map;
> +               struct defm_node *node;
> +
> +               defm_list_for_each(node, defaults) {
> +                       map = node->elem;
> +                       if (map->val->sym == entry->val->sym) {
> +                               pexpr_put(map->e);
> +                               map->e = entry->e;
> +                               free(entry);
> +                               return;
> +                       }
> +               }
> +               defm_list_add(defaults, entry);
> +       } else {
> +               struct default_map *map;
> +               struct defm_node *node;
> +
> +               defm_list_for_each(node, defaults) {
> +                       map = node->elem;
> +                       if (map->val->satval == entry->val->satval) {
> +                               pexpr_put(map->e);
> +                               map->e = entry->e;
> +                               free(entry);
> +                               return;
> +                       }
> +               }
> +               defm_list_add(defaults, entry);
> +       }
> +}
> +
> +/**
> + * updateDefaultList() - Update a default list with a new value-condition pair
> + * @val: The value whose condition will be updated
> + * @newCond: The condition of the default prop. Does not include the condition
> + * that the earlier default's conditions are not fulfilled.
> + * @result: the default list
> + * @sym: the symbol that the defaults belong to
> + *
> + * Update the condition that @val will be used for @sym by considering the next
> + * default property, whose condition is given by @newCond.
> + */
> +static void updateDefaultList(struct fexpr *val, struct pexpr *newCond,
> +                             struct defm_list *result, struct symbol *sym,
> +                             struct cfdata *data)
> +{
> +       // The current condition of @val deduced from the previous default props
> +       struct pexpr *prevCond = findDefaultEntry(val, result, data->constants);
> +       // New combined condition for @val
> +       struct pexpr *condUseVal =
> +               pexpr_or(prevCond,
> +                        pexpr_and(newCond, pexpr_not_share(covered, data),
> +                                  data, PEXPR_ARG2),
> +                        data, PEXPR_ARG2);
> +       add_to_default_map(result, create_default_map_entry(val, condUseVal),
> +                          sym);
> +       covered = pexpr_or(covered, newCond, data, PEXPR_ARG1);
> +       PEXPR_PUT(prevCond, condUseVal);
> +}
> +
> +/**
> + * add_defaults() - Generate list of default values and their conditions
> + * @defaults: List of the default properties
> + * @ctx: Additional condition that needs to be fulfilled for any default. May be
> + * NULL.
> + * @result: List that will be filled
> + * @sym: Symbol that the defaults belong to
> + *
> + * Creates a map from values that @sym can assume to the conditions under which
> + * they will be assumed. Without @ctx, this will only consider the conditions
> + * directly associated with the defaults, e.g. sym->dir_dep would not be
> + * considered.
> + *
> + * As a side effect, the &symbol->nb_vals of @sym will be added for
> + * all default values (as well as the @symbol->nb_vals of other symbols @sym has
> + * as default (recursively)).
> + */
> +static void add_defaults(struct prop_list *defaults, struct expr *ctx,
> +                        struct defm_list *result, struct symbol *sym,
> +                        struct cfdata *data)
> +{
> +       struct prop_node *node;
> +       struct property *p;
> +       struct expr *expr;
> +
> +       prop_list_for_each(node, defaults) {
> +               p = node->elem;
> +               /* calculate expr as whether the default's condition (and the
> +                * one inherited from ctx) is fulfilled
> +                */
> +               if (p->visible.expr) {
> +                       if (ctx == NULL)
> +                               expr = expr_copy(p->visible.expr);
> +                       else
> +                               expr = expr_alloc_and(
> +                                       expr_copy(p->visible.expr),
> +                                       expr_copy(ctx));
> +               } else {
> +                       if (ctx == NULL)
> +                               expr = expr_alloc_symbol(&symbol_yes);
> +                       else
> +                               expr = expr_alloc_and(
> +                                       expr_alloc_symbol(&symbol_yes),
> +                                       expr_copy(ctx));
> +               }
> +
> +               /* if tristate and def.value = y */
> +               if (p->expr->type == E_SYMBOL && sym->type == S_TRISTATE &&
> +                   p->expr->left.sym == &symbol_yes) {
> +                       struct pexpr *expr_y =
> +                               expr_calculate_pexpr_y(expr, data);
> +                       struct pexpr *expr_m =
> +                               expr_calculate_pexpr_m(expr, data);
> +
> +                       updateDefaultList(data->constants->symbol_yes_fexpr,
> +                                         expr_y, result, sym, data);
> +                       updateDefaultList(data->constants->symbol_mod_fexpr,
> +                                         expr_m, result, sym, data);
> +                       PEXPR_PUT(expr_y, expr_m);
> +               }
> +               /* if def.value = n/m/y */
> +               else if (p->expr->type == E_SYMBOL &&
> +                        sym_is_tristate_constant(p->expr->left.sym) &&
> +                        sym_is_boolean(sym)) {
> +                       struct fexpr *s;
> +                       struct pexpr *expr_both =
> +                               expr_calculate_pexpr_both(expr, data);
> +
> +                       if (p->expr->left.sym == &symbol_yes)
> +                               s = data->constants->symbol_yes_fexpr;
> +                       else if (p->expr->left.sym == &symbol_mod)
> +                               s = data->constants->symbol_mod_fexpr;
> +                       else
> +                               s = data->constants->symbol_no_fexpr;
> +
> +                       updateDefaultList(s, expr_both, result, sym, data);
> +                       pexpr_put(expr_both);
> +               }
> +               /* if def.value = n/m/y, but written as 0/1/2 for a boolean */
> +               else if (sym_is_boolean(sym) && p->expr->type == E_SYMBOL &&
> +                        p->expr->left.sym->type == S_UNKNOWN &&
> +                        is_tri_as_num(p->expr->left.sym)) {
> +                       struct fexpr *s;
> +                       struct pexpr *expr_both =
> +                               expr_calculate_pexpr_both(expr, data);
> +
> +                       if (!strcmp(p->expr->left.sym->name, "0"))
> +                               s = data->constants->symbol_no_fexpr;
> +                       else if (!strcmp(p->expr->left.sym->name, "1"))
> +                               s = data->constants->symbol_mod_fexpr;
> +                       else
> +                               s = data->constants->symbol_yes_fexpr;
> +
> +                       updateDefaultList(s, expr_both, result, sym, data);
> +                       pexpr_put(expr_both);
> +               }
> +               /* if def.value = non-boolean constant */
> +               else if (expr_is_nonbool_constant(p->expr)) {
> +                       struct fexpr *s = sym_get_or_create_nonbool_fexpr(
> +                               sym, p->expr->left.sym->name, data);
> +                       struct pexpr *expr_both =
> +                               expr_calculate_pexpr_both(expr, data);
> +
> +                       updateDefaultList(s, expr_both, result, sym, data);
> +                       pexpr_put(expr_both);
> +               }
> +               /* any expression which evaluates to n/m/y for a tristate */
> +               else if (sym->type == S_TRISTATE) {
> +                       struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr),
> +                                                           expr_copy(expr));
> +                       struct pexpr *expr_y =
> +                               expr_calculate_pexpr_y(e_tmp, data);
> +                       struct pexpr *expr_m =
> +                               expr_calculate_pexpr_m(e_tmp, data);
> +
> +                       updateDefaultList(data->constants->symbol_yes_fexpr,
> +                                         expr_y, result, sym, data);
> +                       updateDefaultList(data->constants->symbol_mod_fexpr,
> +                                         expr_m, result, sym, data);
> +                       PEXPR_PUT(expr_y, expr_m);
> +                       expr_free(e_tmp);
> +               }
> +               /* if non-boolean && def.value = non-boolean symbol */
> +               else if (p->expr->type == E_SYMBOL && sym_is_nonboolean(sym) &&
> +                        sym_is_nonboolean(p->expr->left.sym)) {
> +                       struct prop_list *nb_sym_defaults = prop_list_init();
> +                       struct property *p_tmp;
> +
> +                       /* Add defaults of other symbol as possible defaults for
> +                        * this symbol
> +                        */
> +                       for_all_defaults(p->expr->left.sym, p_tmp)
> +                               prop_list_add(nb_sym_defaults, p_tmp);
> +
> +                       add_defaults(nb_sym_defaults, expr, result, sym, data);
> +                       prop_list_free(nb_sym_defaults);
> +               }
> +               /* any expression which evaluates to n/m/y */
> +               else {
> +                       struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr),
> +                                                           expr_copy(expr));
> +                       struct pexpr *expr_both =
> +                               expr_calculate_pexpr_both(e_tmp, data);
> +
> +                       updateDefaultList(data->constants->symbol_yes_fexpr,
> +                                         expr_both, result, sym, data);
> +
> +                       pexpr_put(expr_both);
> +                       expr_free(e_tmp);
> +               }
> +               expr_free(expr);
> +       }
> +}
> +
> +/**
> + * get_defaults() - Generate list of default values and their conditions
> + * @sym: Symbol whose defaults we want to look at
> + *
> + * Creates a map from values that @sym can assume to the conditions under which
> + * they will be assumed. This will only consider the conditions
> + * directly associated with the defaults, e.g. sym->dir_dep would not be
> + * considered.
> + *
> + * As a side effect, the &symbol->nb_vals of @sym will be added for
> + * all default values (as well as the @symbol->nb_vals of other symbols @sym has
> + * as default (recursively)).
> + */
> +static struct defm_list *get_defaults(struct symbol *sym, struct cfdata *data)
> +{
> +       struct defm_list *result = defm_list_init();
> +       struct prop_list *defaults; /* list of default props of sym */
> +       struct property *p;
> +
> +       covered = pexf(data->constants->const_false);
> +
> +       defaults = prop_list_init();
> +       for_all_defaults(sym, p)
> +               prop_list_add(defaults, p);
> +
> +       add_defaults(defaults, NULL, result, sym, data);
> +       prop_list_free(defaults);
> +       pexpr_put(covered);
> +
> +       return result;
> +}
> +
> +/*
> + * return the condition for "y", False if it doesn't exist
> + */
> +static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data)
> +{
> +       struct default_map *entry;
> +       struct defm_node *node;
> +
> +       defm_list_for_each(node, list) {
> +               entry = node->elem;
> +               if (entry->val->type == FE_SYMBOL &&
> +                   entry->val->sym == &symbol_yes) {
> +                       pexpr_get(entry->e);
> +                       return entry->e;
> +               }
> +       }
> +
> +       return pexf(data->constants->const_false);
> +}
> +
> +/*
> + * return the condition for "m", False if it doesn't exist
> + */
> +static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data)
> +{
> +       struct default_map *entry;
> +       struct defm_node *node;
> +
> +       defm_list_for_each(node, list) {
> +               entry = node->elem;
> +               if (entry->val->type == FE_SYMBOL &&
> +                   entry->val->sym == &symbol_mod) {
> +                       pexpr_get(entry->e);
> +                       return entry->e;
> +               }
> +       }
> +
> +       return pexf(data->constants->const_false);
> +}
> +
> +/*
> + * return the constraint when _some_ default value will be applied
> + */
> +static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data)
> +{
> +       struct property *prop;
> +       struct expr *e;
> +       struct pexpr *p;
> +
> +       if (!sym_is_nonboolean(sym))
> +               return NULL;
> +
> +       p = pexf(data->constants->const_false);
> +       for_all_defaults(sym, prop) {
> +               if (prop->visible.expr)
> +                       e = expr_copy(prop->visible.expr);
> +               else
> +                       e = expr_alloc_symbol(&symbol_yes);
> +
> +               if (expr_can_evaluate_to_mod(e))
> +                       p = pexpr_or(p, expr_calculate_pexpr_both(e, data),
> +                                    data, PEXPR_ARGX);
> +
> +               p = pexpr_or(p, expr_calculate_pexpr_y(e, data), data,
> +                            PEXPR_ARGX);
> +
> +               expr_free(e);
> +       }
> +
> +       return p;
> +}
> +
> +/*
> + * get the value for the range
> + */
> +static long sym_get_range_val(struct symbol *sym, int base)
> +{
> +       sym_calc_value(sym);
> +       switch (sym->type) {
> +       case S_INT:
> +               base = 10;
> +               break;
> +       case S_HEX:
> +               base = 16;
> +               break;
> +       default:
> +               break;
> +       }
> +       return strtol(sym->curr.val, NULL, base);
> +}
> +
> +/*
> + * count the number of all constraints
> + */
> +unsigned int count_counstraints(void)
> +{
> +       unsigned int c = 0;
> +       struct symbol *sym;
> +
> +       for_all_symbols(sym) {
> +               if (sym->type == S_UNKNOWN)
> +                       continue;
> +
> +               c += sym->constraints->size;
> +       }
> +
> +       return c;
> +}
> +
> +/*
> + * add a constraint for a symbol
> + */
> +void sym_add_constraint(struct symbol *sym, struct pexpr *constraint,
> +                       struct cfdata *data)
> +{
> +       if (!constraint)
> +               return;
> +
> +       /* no need to add that */
> +       if (constraint->type == PE_SYMBOL &&
> +           constraint->left.fexpr == data->constants->const_true)
> +               return;
> +
> +       /* this should never happen */
> +       if (constraint->type == PE_SYMBOL &&
> +           constraint->left.fexpr == data->constants->const_false)
> +               perror("Adding const_false.");
> +
> +       pexpr_list_add(sym->constraints, pexpr_get(constraint));
> +
> +       if (!pexpr_is_nnf(constraint))
> +               pexpr_print("Not NNF:", constraint, -1);
> +}
> +
> +/*
> + * add a constraint for a symbol, but check for duplicate constraints
> + */
> +void sym_add_constraint_eq(struct symbol *sym, struct pexpr *constraint,
> +                          struct cfdata *data)
> +{
> +       struct pexpr_node *node;
> +
> +       if (!constraint)
> +               return;
> +
> +       /* no need to add that */
> +       if (constraint->type == PE_SYMBOL &&
> +           constraint->left.fexpr == data->constants->const_true)
> +               return;
> +
> +       /* this should never happen */
> +       if (constraint->type == PE_SYMBOL &&
> +           constraint->left.fexpr == data->constants->const_false)
> +               perror("Adding const_false.");
> +
> +       /* check the constraints for the same symbol */
> +       pexpr_list_for_each(node, sym->constraints)
> +               if (pexpr_eq(constraint, node->elem, data))
> +                       return;
> +
> +       pexpr_list_add(sym->constraints, pexpr_get(constraint));
> +
> +       if (!pexpr_is_nnf(constraint))
> +               pexpr_print("Not NNF:", constraint, -1);
> +}
> diff --git a/scripts/kconfig/cf_constraints.h b/scripts/kconfig/cf_constraints.h
> new file mode 100644
> index 000000000000..97a18eaf11ca
> --- /dev/null
> +++ b/scripts/kconfig/cf_constraints.h
> @@ -0,0 +1,26 @@
> +/* SPDX-License-Identifier: GPL-2.0 */
> +/*
> + * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
> + */
> +
> +#ifndef CF_CONSTRAINTS_H
> +#define CF_CONSTRAINTS_H
> +
> +#include "cf_defs.h"
> +#include "expr.h"
> +
> +/* build the constraints for each symbol */
> +void get_constraints(struct cfdata *data);
> +
> +/* count the number of all constraints */
> +unsigned int count_counstraints(void);
> +
> +/* add a constraint for a symbol */
> +void sym_add_constraint(struct symbol *sym, struct pexpr *constraint, struct cfdata *data);
> +
> +void sym_add_constraint_fexpr(struct symbol *sym, struct fexpr *constraint);
> +
> +/* add a constraint for a symbol, but check for duplicate constraints */
> +void sym_add_constraint_eq(struct symbol *sym, struct pexpr *constraint, struct cfdata *data);
> +
> +#endif
> --
> 2.39.2
>


--
Best Regards

Masahiro Yamada
Masahiro Yamada Aug. 12, 2024, 10 a.m. UTC | #2
On Mon, Aug 12, 2024 at 5:49 PM Masahiro Yamada <masahiroy@kernel.org> wrote:
>
> On Wed, Jul 10, 2024 at 3:54 PM Ole Schuerks <ole0811sch@gmail.com> wrote:
> >
> > These files translate the Kconfig-model into propositional logic and store
> > the constraints for each symbol in the corresponding struct.
> >
> > 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@kernel.org>
> > 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>
> > Signed-off-by: Ole Schuerks <ole0811sch@gmail.com>
> > ---
> >  scripts/kconfig/cf_constraints.c | 1720 ++++++++++++++++++++++++++++++
> >  scripts/kconfig/cf_constraints.h |   26 +
> >  2 files changed, 1746 insertions(+)
> >  create mode 100644 scripts/kconfig/cf_constraints.c
> >  create mode 100644 scripts/kconfig/cf_constraints.h
> >
> > diff --git a/scripts/kconfig/cf_constraints.c b/scripts/kconfig/cf_constraints.c
> > new file mode 100644
> > index 000000000000..1c02a4b47383
> > --- /dev/null
> > +++ b/scripts/kconfig/cf_constraints.c
> > @@ -0,0 +1,1720 @@
> > +// SPDX-License-Identifier: GPL-2.0
> > +/*
> > + * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
> > + */
> > +
> > +#include "cf_defs.h"
> > +#include "expr.h"
> > +#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_utils.h"
> > +#include "internal.h"
> > +#include "cf_expr.h"
> > +#include "cf_constraints.h"
> > +
> > +#define KCR_CMP false
> > +#define NPC_OPTIMISATION true
> > +
> > +static void init_constraints(struct cfdata *data);
> > +static void get_constraints_bool(struct cfdata *data);
> > +static void get_constraints_select(struct cfdata *data);
> > +static void get_constraints_nonbool(struct cfdata *data);
> > +
> > +static void build_tristate_constraint_clause(struct symbol *sym,
> > +                                            struct cfdata *data);
> > +
> > +static void add_selects_kcr(struct symbol *sym, struct cfdata *data);
> > +static void add_selects(struct symbol *sym, struct cfdata *data);
> > +
> > +static void add_dependencies_bool(struct symbol *sym, struct cfdata *data);
> > +static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data);
> > +static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data);
> > +
> > +static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data);
> > +static void add_choice_dependencies(struct symbol *sym, struct cfdata *data);
> > +static void add_choice_constraints(struct symbol *sym, struct cfdata *data);
> > +static void add_invisible_constraints(struct symbol *sym, struct cfdata *data);
> > +static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data);
> > +static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data);
> > +static void sym_add_nonbool_values_from_default_range(struct symbol *sym,
> > +                                                     struct cfdata *data);
> > +static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data);
> > +static void sym_add_nonbool_prompt_constraint(struct symbol *sym,
> > +                                             struct cfdata *data);
> > +
> > +static struct default_map *create_default_map_entry(struct fexpr *val,
> > +                                                   struct pexpr *e);
> > +static struct defm_list *get_defaults(struct symbol *sym, struct cfdata *data);
> > +static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data);
> > +static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data);
> > +static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data);
> > +static long sym_get_range_val(struct symbol *sym, int base);
> > +
> > +/* -------------------------------------- */
> > +
> > +/*
> > + * build the constraints for each symbol
> > + */
> > +void get_constraints(struct cfdata *data)
> > +{
> > +       printd("Building constraints...");
> > +
> > +       init_constraints(data);
> > +       get_constraints_bool(data);
> > +       get_constraints_select(data);
> > +       get_constraints_nonbool(data);
> > +}
> > +
> > +/*
> > + * need to go through the constraints once to find all "known values"
> > + * for the non-Boolean symbols (and add them to sym->nb_vals for the given
> > + * symbols).
> > + * expr_calculate_pexpr_both and get_defaults have the side effect of creating
> > + * known values.
> > + */
> > +static void init_constraints(struct cfdata *data)
> > +{
> > +       struct symbol *sym;
> > +       struct property *p;
> > +
> > +       for_all_symbols(sym) {
> > +               struct property *prompt;
> > +
> > +               if (sym->type == S_UNKNOWN)
> > +                       continue;
> > +
> > +               if (sym_is_boolean(sym)) {
> > +                       for_all_properties(sym, p, P_SELECT)
> > +                               pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
> > +                                                         data));
> > +
> > +                       for_all_properties(sym, p, P_IMPLY)
> > +                               pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
> > +                                                         data));
>
>
>
> Does 'imply' give any constraint?


I take back this comment.

'imply' does give a constraint when the implied symbol has
no prompt.
diff mbox series

Patch

diff --git a/scripts/kconfig/cf_constraints.c b/scripts/kconfig/cf_constraints.c
new file mode 100644
index 000000000000..1c02a4b47383
--- /dev/null
+++ b/scripts/kconfig/cf_constraints.c
@@ -0,0 +1,1720 @@ 
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
+ */
+
+#include "cf_defs.h"
+#include "expr.h"
+#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_utils.h"
+#include "internal.h"
+#include "cf_expr.h"
+#include "cf_constraints.h"
+
+#define KCR_CMP false
+#define NPC_OPTIMISATION true
+
+static void init_constraints(struct cfdata *data);
+static void get_constraints_bool(struct cfdata *data);
+static void get_constraints_select(struct cfdata *data);
+static void get_constraints_nonbool(struct cfdata *data);
+
+static void build_tristate_constraint_clause(struct symbol *sym,
+					     struct cfdata *data);
+
+static void add_selects_kcr(struct symbol *sym, struct cfdata *data);
+static void add_selects(struct symbol *sym, struct cfdata *data);
+
+static void add_dependencies_bool(struct symbol *sym, struct cfdata *data);
+static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data);
+static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data);
+
+static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data);
+static void add_choice_dependencies(struct symbol *sym, struct cfdata *data);
+static void add_choice_constraints(struct symbol *sym, struct cfdata *data);
+static void add_invisible_constraints(struct symbol *sym, struct cfdata *data);
+static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data);
+static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data);
+static void sym_add_nonbool_values_from_default_range(struct symbol *sym,
+						      struct cfdata *data);
+static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data);
+static void sym_add_nonbool_prompt_constraint(struct symbol *sym,
+					      struct cfdata *data);
+
+static struct default_map *create_default_map_entry(struct fexpr *val,
+						    struct pexpr *e);
+static struct defm_list *get_defaults(struct symbol *sym, struct cfdata *data);
+static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data);
+static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data);
+static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data);
+static long sym_get_range_val(struct symbol *sym, int base);
+
+/* -------------------------------------- */
+
+/*
+ * build the constraints for each symbol
+ */
+void get_constraints(struct cfdata *data)
+{
+	printd("Building constraints...");
+
+	init_constraints(data);
+	get_constraints_bool(data);
+	get_constraints_select(data);
+	get_constraints_nonbool(data);
+}
+
+/*
+ * need to go through the constraints once to find all "known values"
+ * for the non-Boolean symbols (and add them to sym->nb_vals for the given
+ * symbols).
+ * expr_calculate_pexpr_both and get_defaults have the side effect of creating
+ * known values.
+ */
+static void init_constraints(struct cfdata *data)
+{
+	struct symbol *sym;
+	struct property *p;
+
+	for_all_symbols(sym) {
+		struct property *prompt;
+
+		if (sym->type == S_UNKNOWN)
+			continue;
+
+		if (sym_is_boolean(sym)) {
+			for_all_properties(sym, p, P_SELECT)
+				pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
+							  data));
+
+			for_all_properties(sym, p, P_IMPLY)
+				pexpr_put(expr_calculate_pexpr_both(p->visible.expr,
+							  data));
+		}
+
+		if (sym->dir_dep.expr)
+			pexpr_put(expr_calculate_pexpr_both(sym->dir_dep.expr, data));
+
+		prompt = sym_get_prompt(sym);
+		if (prompt != NULL && prompt->visible.expr) {
+			pexpr_put(expr_calculate_pexpr_both(prompt->visible.expr, data));
+			defm_list_destruct(get_defaults(sym, data));
+		}
+
+		if (sym_is_nonboolean(sym)) {
+			const char *curr;
+
+			for_all_defaults(sym, p) {
+				if (p == NULL)
+					continue;
+
+				sym_create_nonbool_fexpr(
+					sym, p->expr->left.sym->name, data);
+			}
+			for_all_properties(sym, p, P_RANGE) {
+				if (p == NULL)
+					continue;
+
+				sym_create_nonbool_fexpr(
+					sym, p->expr->left.sym->name, data);
+				sym_create_nonbool_fexpr(
+					sym, p->expr->right.sym->name, data);
+			}
+			curr = sym_get_string_value(sym);
+			if (strcmp(curr, "") != 0)
+				sym_create_nonbool_fexpr(sym, (char *)curr,
+							 data);
+		}
+
+		if (sym->type == S_HEX || sym->type == S_INT)
+			sym_add_nonbool_values_from_default_range(sym, data);
+	}
+}
+
+/*
+ *  build constraints for boolean symbols
+ */
+static void get_constraints_bool(struct cfdata *data)
+{
+	struct symbol *sym;
+
+	for_all_symbols(sym) {
+		if (!sym_is_boolean(sym))
+			continue;
+
+		/* build tristate constraints */
+		if (sym->type == S_TRISTATE)
+			build_tristate_constraint_clause(sym, data);
+
+		/* build constraints for select statements
+		 * need to treat choice symbols separately
+		 */
+		if (!KCR_CMP) {
+			add_selects(sym, data);
+		} else {
+			if (sym->rev_dep.expr && !sym_is_choice(sym) &&
+			    !sym_is_choice_value(sym))
+				add_selects_kcr(sym, data);
+		}
+
+		/* build constraints for dependencies for booleans */
+		if (sym->dir_dep.expr && !sym_is_choice(sym) &&
+		    !sym_is_choice_value(sym)) {
+			if (!KCR_CMP)
+				add_dependencies_bool(sym, data);
+			else
+				add_dependencies_bool_kcr(sym, data);
+		}
+
+		/* build constraints for choice prompts */
+		if (sym_is_choice(sym))
+			add_choice_prompt_cond(sym, data);
+
+		/* build constraints for dependencies (choice symbols and options) */
+		if (sym_is_choice(sym) || sym_is_choice_value(sym))
+			add_choice_dependencies(sym, data);
+
+		/* build constraints for the choice groups */
+		if (sym_is_choice(sym))
+			add_choice_constraints(sym, data);
+
+		/* build invisible constraints */
+		add_invisible_constraints(sym, data);
+	}
+}
+
+/*
+ * build the constraints for select-variables
+ * skip non-Booleans, choice symbols/options och symbols without rev_dir
+ */
+static void get_constraints_select(struct cfdata *data)
+{
+	struct symbol *sym;
+
+	for_all_symbols(sym) {
+		struct pexpr *sel_y, *sel_m;
+		struct pexpr *c1, *c2;
+
+		if (KCR_CMP)
+			continue;
+
+		if (!sym_is_boolean(sym))
+			continue;
+
+		if (sym_is_choice(sym) || sym_is_choice_value(sym))
+			continue;
+
+		if (!sym->rev_dep.expr)
+			continue;
+
+		if (sym->list_sel_y == NULL)
+			continue;
+
+		sel_y = pexpr_implies(pexf(sym->fexpr_sel_y),
+					   pexf(sym->fexpr_y), data,
+					   PEXPR_ARGX);
+		sym_add_constraint(sym, sel_y, data);
+
+		c1 = pexpr_implies(pexf(sym->fexpr_sel_y), sym->list_sel_y,
+					data, PEXPR_ARG1);
+		sym_add_constraint(sym, c1, data);
+
+		/* only continue for tristates */
+		if (sym->type == S_BOOLEAN)
+			continue;
+
+		sel_m = pexpr_implies(pexf(sym->fexpr_sel_m),
+					   sym_get_fexpr_both(sym, data), data,
+					   PEXPR_ARGX);
+		sym_add_constraint(sym, sel_m, data);
+
+		c2 = pexpr_implies(pexf(sym->fexpr_sel_m), sym->list_sel_m,
+					data, PEXPR_ARG1);
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(sel_y, sel_m, c1, c2);
+	}
+}
+
+/*
+ * build constraints for non-booleans
+ */
+static void get_constraints_nonbool(struct cfdata *data)
+{
+	struct symbol *sym;
+
+	for_all_symbols(sym) {
+		if (!sym_is_nonboolean(sym))
+			continue;
+
+		/* the symbol must have a value, if there is a prompt */
+		if (sym_has_prompt(sym))
+			sym_add_nonbool_prompt_constraint(sym, data);
+
+		/* build the range constraints for int/hex */
+		if (sym->type == S_HEX || sym->type == S_INT)
+			sym_add_range_constraints(sym, data);
+
+		/* build constraints for dependencies for non-booleans */
+		if (sym->dir_dep.expr)
+			add_dependencies_nonbool(sym, data);
+
+		/* build invisible constraints */
+		add_invisible_constraints(sym, data);
+
+		/* exactly one of the symbols must be true */
+		sym_nonbool_at_least_1(sym, data);
+		sym_nonbool_at_most_1(sym, data);
+	}
+}
+
+/*
+ * enforce tristate constraints
+ */
+static void build_tristate_constraint_clause(struct symbol *sym,
+					     struct cfdata *data)
+{
+	struct pexpr *X, *X_m, *modules, *c;
+
+	if (sym->type != S_TRISTATE)
+		return;
+
+	X = pexf(sym->fexpr_y);
+	X_m = pexf(sym->fexpr_m);
+	modules = pexf(modules_sym->fexpr_y);
+
+	/* -X v -X_m */
+	c = pexpr_or(pexpr_not_share(X, data), pexpr_not_share(X_m, data),
+			  data, PEXPR_ARGX);
+	sym_add_constraint(sym, c, data);
+
+	/* X_m -> MODULES */
+	if (modules_sym->fexpr_y != NULL) {
+		struct pexpr *c2 = pexpr_implies_share(X_m, modules, data);
+
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(c2);
+	}
+	PEXPR_PUT(X, X_m, modules, c);
+}
+
+/*
+ * build the select constraints
+ * - RDep(X) implies X
+ */
+static void add_selects_kcr(struct symbol *sym, struct cfdata *data)
+{
+	struct pexpr *rdep_y = expr_calculate_pexpr_y(sym->rev_dep.expr, data);
+	struct pexpr *c1 = pexpr_implies(rdep_y, pexf(sym->fexpr_y), data,
+					      PEXPR_ARG2);
+
+	struct pexpr *rdep_both =
+		expr_calculate_pexpr_both(sym->rev_dep.expr, data);
+	struct pexpr *c2 = pexpr_implies(
+		rdep_both, sym_get_fexpr_both(sym, data), data, PEXPR_ARG2);
+
+	sym_add_constraint(sym, c1, data);
+	sym_add_constraint(sym, c2, data);
+	PEXPR_PUT(rdep_y, c1, rdep_both, c2);
+}
+
+/*
+ * build the select constraints simplified
+ * - RDep(X) implies X
+ */
+static void add_selects(struct symbol *sym, struct cfdata *data)
+{
+	struct property *p;
+
+	if (!sym_is_boolean(sym))
+		return;
+
+	for_all_properties(sym, p, P_SELECT) {
+		struct symbol *selected = p->expr->left.sym;
+		struct pexpr *cond_y, *cond_both;
+
+		if (selected->type == S_UNKNOWN)
+			continue;
+
+		if (!selected->rev_dep.expr)
+			continue;
+
+		if (p->visible.expr) {
+			cond_y = expr_calculate_pexpr_y(p->visible.expr, data);
+			cond_both = expr_calculate_pexpr_both(p->visible.expr,
+							      data);
+		} else {
+			cond_y = pexf(data->constants->const_true);
+			cond_both = pexf(data->constants->const_true);
+		}
+
+		if (selected->type == S_BOOLEAN) {
+			/* imply that symbol is selected to y */
+			struct pexpr *e1 = pexpr_and(
+				cond_both, sym_get_fexpr_both(sym, data), data,
+				PEXPR_ARG2);
+			struct pexpr *c1 = pexpr_implies(
+				e1, pexf(selected->fexpr_sel_y), data,
+				PEXPR_ARG2);
+
+			sym_add_constraint(selected, c1, data);
+
+			if (selected->list_sel_y == NULL)
+				selected->list_sel_y = pexpr_get(e1);
+			else
+				selected->list_sel_y =
+					pexpr_or(selected->list_sel_y, e1, data,
+						 PEXPR_ARG1);
+			PEXPR_PUT(e1, c1);
+		}
+
+		if (selected->type == S_TRISTATE) {
+			struct pexpr *e2, *e3, *c2, *c3;
+
+			/* imply that symbol is selected to y */
+			e2 = pexpr_and(cond_y, pexf(sym->fexpr_y), data,
+					    PEXPR_ARG2);
+			c2 = pexpr_implies(e2, pexf(selected->fexpr_sel_y),
+						data, PEXPR_ARG2);
+			sym_add_constraint(selected, c2, data);
+
+			if (selected->list_sel_y == NULL)
+				selected->list_sel_y = pexpr_get(e2);
+			else
+				selected->list_sel_y =
+					pexpr_or(selected->list_sel_y, e2,
+						      data, PEXPR_ARG1);
+
+			/* imply that symbol is selected to m */
+			e3 = pexpr_and(cond_both,
+					    sym_get_fexpr_both(sym, data), data,
+					    PEXPR_ARG2);
+			c3 = pexpr_implies(e3, pexf(selected->fexpr_sel_m),
+						data, PEXPR_ARG2);
+			sym_add_constraint(selected, c3, data);
+
+			if (selected->list_sel_m == NULL)
+				selected->list_sel_m = pexpr_get(e3);
+			else
+				selected->list_sel_m =
+					pexpr_or(selected->list_sel_m, e3,
+						      data, PEXPR_ARG1);
+			PEXPR_PUT(e2, c2, e3, c3);
+		}
+		PEXPR_PUT(cond_y, cond_both);
+	}
+}
+
+/*
+ * build the dependency constraints for booleans
+ *  - X implies Dep(X) or RDep(X)
+ */
+static void add_dependencies_bool(struct symbol *sym, struct cfdata *data)
+{
+	struct pexpr *dep_both;
+	struct pexpr *visible_m;
+	struct pexpr *visible_y;
+	struct pexpr *visible_both;
+	struct property *prompt;
+	struct pexpr *has_prompt;
+	struct pexpr *sel_y;
+
+	if (!sym_is_boolean(sym) || !sym->dir_dep.expr)
+		return;
+
+	prompt = sym_get_prompt(sym);
+	if (!prompt) {
+		visible_m = pexf(data->constants->const_false);
+		visible_y = pexpr_get(visible_m);
+		visible_both = pexpr_get(visible_m);
+	} else if (prompt->expr == NULL) {
+		visible_m = pexf(data->constants->const_true);
+		visible_y = pexpr_get(visible_m);
+		visible_both = pexpr_get(visible_m);
+	} else {
+		visible_m = expr_calculate_pexpr_m(prompt->expr, data);
+		visible_y = expr_calculate_pexpr_y(prompt->expr, data);
+		visible_both = pexpr_or_share(visible_y, visible_m, data);
+	}
+
+	dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
+
+	sel_y = sym->rev_dep.expr ? pexf(sym->fexpr_sel_y) :
+				    pexf(data->constants->const_false);
+	has_prompt = pexpr_get(visible_both);
+	has_prompt = pexpr_and(
+			has_prompt,
+			pexpr_not(pexpr_and_share(sel_y, visible_m, data),
+				data),
+			data, PEXPR_ARGX);
+
+	if (sym->type == S_TRISTATE) {
+		struct pexpr *c1;
+		struct pexpr *c2;
+		struct pexpr *dep_y =
+			expr_calculate_pexpr_y(sym->dir_dep.expr, data);
+		struct pexpr *sel_both = sym_get_fexpr_sel_both(sym, data);
+		struct pexpr *cond_y1;
+		struct pexpr *cond_y2;
+		struct pexpr *cond_y;
+		struct pexpr *cond_m1;
+		struct pexpr *cond_m2;
+		struct pexpr *cond_m;
+
+		cond_y1 = pexpr_implies(pexpr_not_share(has_prompt, data),
+				       pexpr_or_share(dep_y, sel_y, data), data,
+				       PEXPR_ARGX);
+		cond_y2 = pexpr_implies_share(has_prompt, visible_y, data);
+		cond_y = pexpr_and_share(cond_y1, cond_y2, data);
+		cond_m1 =
+			pexpr_implies(pexpr_not_share(has_prompt, data),
+				      pexpr_or_share(dep_both, sel_both, data),
+				      data, PEXPR_ARGX);
+		cond_m2 = pexpr_implies(has_prompt,
+					pexpr_not_share(sel_y, data), data,
+					PEXPR_ARG2);
+		cond_m = pexpr_and_share(cond_m1, cond_m2, data);
+		c1 = pexpr_implies(pexf(sym->fexpr_y), cond_y, data,
+				   PEXPR_ARG1);
+		c2 = pexpr_implies(pexf(sym->fexpr_m), cond_m, data,
+				   PEXPR_ARG1);
+
+		sym_add_constraint(sym, c1, data);
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(c1, c2, dep_y, sel_both, cond_y1,
+			  cond_y2, cond_y, cond_m1, cond_m2, cond_m);
+	} else if (sym->type == S_BOOLEAN) {
+		struct pexpr *cond1;
+		struct pexpr *cond2;
+		struct pexpr *c;
+
+		cond1 = pexpr_implies(pexpr_not_share(has_prompt, data),
+				      pexpr_or(dep_both, pexf(sym->fexpr_m),
+					       data, PEXPR_ARG2),
+				      data, PEXPR_ARGX);
+		cond2 = pexpr_implies_share(has_prompt, visible_y, data);
+		c = pexpr_implies(pexf(sym->fexpr_y),
+				  pexpr_and_share(cond1, cond2, data), data,
+				  PEXPR_ARGX);
+
+		sym_add_constraint(sym, c, data);
+		PEXPR_PUT(c, cond1, cond2);
+	}
+	PEXPR_PUT(dep_both, has_prompt, sel_y, visible_y, visible_m, visible_both);
+}
+
+/*
+ * build the dependency constraints for booleans (KCR)
+ *  - X implies Dep(X) or RDep(X)
+ */
+static void add_dependencies_bool_kcr(struct symbol *sym, struct cfdata *data)
+{
+	struct pexpr *dep_both, *sel_both;
+
+	if (!sym_is_boolean(sym) || !sym->dir_dep.expr)
+		return;
+
+	dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
+
+	sel_both = sym->rev_dep.expr ?
+			   expr_calculate_pexpr_both(sym->rev_dep.expr, data) :
+			   pexf(data->constants->const_false);
+
+	if (sym->type == S_TRISTATE) {
+		struct pexpr *c1;
+		struct pexpr *c2;
+		{
+			struct pexpr *dep_y =
+				expr_calculate_pexpr_y(sym->dir_dep.expr, data);
+			struct pexpr *sel_y =
+				sym->rev_dep.expr ?
+					expr_calculate_pexpr_y(
+						sym->rev_dep.expr, data) :
+					pexf(data->constants->const_false);
+			c1 = pexpr_implies(pexf(sym->fexpr_y),
+						pexpr_or(dep_y, sel_y,
+							      data, PEXPR_ARGX),
+						data, PEXPR_ARGX);
+		}
+		c2 = pexpr_implies(pexf(sym->fexpr_m),
+					pexpr_or_share(dep_both, sel_both,
+						       data),
+					data, PEXPR_ARGX);
+
+		sym_add_constraint(sym, c1, data);
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(c1, c2);
+	} else if (sym->type == S_BOOLEAN) {
+		struct pexpr *c = pexpr_implies(
+			pexf(sym->fexpr_y),
+			pexpr_or_share(dep_both, sel_both, data), data,
+			PEXPR_ARGX);
+
+		sym_add_constraint(sym, c, data);
+		PEXPR_PUT(c);
+	}
+
+	PEXPR_PUT(dep_both, sel_both);
+}
+
+/*
+ * build the dependency constraints for non-booleans
+ *
+ * sym is not 'n' implies `sym->dir_dep`
+ */
+static void add_dependencies_nonbool(struct symbol *sym, struct cfdata *data)
+{
+	struct pexpr *dep_both;
+	struct pexpr *nb_vals; // "sym is set to some value" / "sym is not 'n'"
+	struct fexpr_node *node;
+	struct pexpr *c;
+
+	if (!sym_is_nonboolean(sym) || !sym->dir_dep.expr || sym->rev_dep.expr)
+		return;
+
+	dep_both = expr_calculate_pexpr_both(sym->dir_dep.expr, data);
+
+	nb_vals = pexf(data->constants->const_false);
+	/* can skip the first non-boolean value, since this is 'n' */
+	fexpr_list_for_each(node, sym->nb_vals) {
+		if (node->prev == NULL)
+			continue;
+
+		nb_vals = pexpr_or(nb_vals, pexf(node->elem), data,
+					PEXPR_ARGX);
+	}
+
+	c = pexpr_implies(nb_vals, dep_both, data, PEXPR_ARGX);
+	sym_add_constraint(sym, c, data);
+	pexpr_put(c);
+}
+
+/*
+ * build the constraints for the choice prompt
+ */
+static void add_choice_prompt_cond(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prompt;
+	struct pexpr *promptCondition;
+	struct pexpr *fe_both;
+	struct pexpr *pr_cond;
+	struct pexpr *req_cond;
+
+	if (!sym_is_boolean(sym))
+		return;
+
+	prompt = sym_get_prompt(sym);
+	if (prompt == NULL)
+		return;
+
+	promptCondition =
+		prompt->visible.expr ?
+			expr_calculate_pexpr_both(prompt->visible.expr, data) :
+			pexf(data->constants->const_true);
+	fe_both = sym_get_fexpr_both(sym, data);
+	req_cond = pexpr_implies_share(promptCondition, fe_both, data);
+	sym_add_constraint(sym, req_cond, data);
+	pr_cond = pexpr_implies_share(fe_both, promptCondition, data);
+	sym_add_constraint(sym, pr_cond, data);
+	PEXPR_PUT(promptCondition, fe_both, req_cond, pr_cond);
+}
+
+/*
+ * build constraints for dependencies (choice symbols and options)
+ */
+static void add_choice_dependencies(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prompt;
+	struct expr *to_parse;
+	struct pexpr *dep_both;
+
+	if (!sym_is_choice(sym) || !sym_is_choice_value(sym))
+		return;
+
+	prompt = sym_get_prompt(sym);
+	if (prompt == NULL)
+		return;
+
+	if (sym_is_choice(sym)) {
+		if (!prompt->visible.expr)
+			return;
+		to_parse = prompt->visible.expr;
+	} else {
+		if (!sym->dir_dep.expr)
+			return;
+		to_parse = sym->dir_dep.expr;
+	}
+
+	dep_both = expr_calculate_pexpr_both(to_parse, data);
+
+	if (sym->type == S_TRISTATE) {
+		struct pexpr *dep_y = expr_calculate_pexpr_y(to_parse, data);
+		struct pexpr *c1 = pexpr_implies(pexf(sym->fexpr_y), dep_y,
+						      data, PEXPR_ARG1);
+		struct pexpr *c2 = pexpr_implies(
+			pexf(sym->fexpr_m), dep_both, data, PEXPR_ARG1);
+
+		sym_add_constraint_eq(sym, c1, data);
+		sym_add_constraint_eq(sym, c2, data);
+		PEXPR_PUT(dep_y, c1, c2);
+	} else if (sym->type == S_BOOLEAN) {
+		struct pexpr *c = pexpr_implies(
+			pexf(sym->fexpr_y), dep_both, data, PEXPR_ARG1);
+
+		sym_add_constraint_eq(sym, c, data);
+		pexpr_put(c);
+	}
+	pexpr_put(dep_both);
+}
+
+/*
+ * build constraints for the choice groups
+ */
+static void add_choice_constraints(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prompt;
+	struct symbol *choice, *choice2;
+	struct sym_node *node, *node2;
+	struct sym_list *items, *promptItems;
+	struct pexpr *c1;
+	struct menu *menu_ptr, *choiceval_menu;
+
+	if (!sym_is_boolean(sym))
+		return;
+
+	prompt = sym_get_prompt(sym);
+	if (prompt == NULL)
+		return;
+
+	/* create list of all choice options */
+	items = sym_list_init();
+	/* create list of choice options with a prompt */
+	promptItems = sym_list_init();
+
+	for_all_choices(sym, choiceval_menu, menu_ptr) {
+		choice = choiceval_menu->sym;
+
+		sym_list_add(items, choice);
+		if (sym_get_prompt(choice) != NULL)
+			sym_list_add(promptItems, choice);
+	}
+
+	/* if the choice is set to yes, at least one child must be set to yes */
+	c1 = NULL;
+	sym_list_for_each(node, promptItems) {
+		choice = node->elem;
+		c1 = node->prev == NULL ?
+			     pexf(choice->fexpr_y) :
+			     pexpr_or(c1, pexf(choice->fexpr_y), data,
+					   PEXPR_ARGX);
+	}
+	if (c1 != NULL) {
+		struct pexpr *c2 = pexpr_implies(pexf(sym->fexpr_y), c1,
+						      data, PEXPR_ARG1);
+
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(c1, c2);
+	}
+
+	/* every choice option (even those without a prompt) implies the choice */
+	sym_list_for_each(node, items) {
+		choice = node->elem;
+		c1 = pexpr_implies(sym_get_fexpr_both(choice, data),
+					sym_get_fexpr_both(sym, data), data,
+					PEXPR_ARGX);
+		sym_add_constraint(sym, c1, data);
+		pexpr_put(c1);
+	}
+
+	/* choice options can only select mod, if the entire choice is mod */
+	if (sym->type == S_TRISTATE) {
+		sym_list_for_each(node, items) {
+			choice = node->elem;
+			if (choice->type == S_TRISTATE) {
+				c1 = pexpr_implies(pexf(choice->fexpr_m),
+							pexf(sym->fexpr_m),
+							data, PEXPR_ARGX);
+				sym_add_constraint(sym, c1, data);
+				pexpr_put(c1);
+			}
+		}
+	}
+
+	/* tristate options cannot be m, if the choice symbol is boolean */
+	if (sym->type == S_BOOLEAN) {
+		sym_list_for_each(node, items) {
+			choice = node->elem;
+			if (choice->type == S_TRISTATE) {
+				struct pexpr *e = pexpr_not(pexf(choice->fexpr_m),
+						       data);
+				sym_add_constraint(sym, e, data);
+				pexpr_put(e);
+			}
+		}
+	}
+
+	/* all choice options are mutually exclusive for yes */
+	sym_list_for_each(node, promptItems) {
+		choice = node->elem;
+		for (struct sym_node *node2 = node->next; node2 != NULL;
+		     node2 = node2->next) {
+			choice2 = node2->elem;
+			c1 = pexpr_or(
+				pexpr_not(pexf(choice->fexpr_y), data),
+				pexpr_not(pexf(choice2->fexpr_y), data),
+				data, PEXPR_ARGX);
+			sym_add_constraint(sym, c1, data);
+			pexpr_put(c1);
+		}
+	}
+
+	/* if one choice option with a prompt is set to yes,
+	 * then no other option may be set to mod
+	 */
+	if (sym->type == S_TRISTATE) {
+		sym_list_for_each(node, promptItems) {
+			struct sym_list *tmp;
+
+			choice = node->elem;
+
+			tmp = sym_list_init();
+			for (struct sym_node *node2 = node->next; node2 != NULL;
+			     node2 = node2->next) {
+				choice2 = node2->elem;
+				if (choice2->type == S_TRISTATE)
+					sym_list_add(tmp, choice2);
+			}
+			if (tmp->size == 0)
+				continue;
+
+			sym_list_for_each(node2, tmp) {
+				choice2 = node2->elem;
+				if (node2->prev == NULL)
+					c1 = pexpr_not(
+						pexf(choice2->fexpr_m), data);
+				else
+					c1 = pexpr_and(
+						c1,
+						pexpr_not(
+							pexf(choice2->fexpr_m),
+							data),
+						data, PEXPR_ARGX);
+			}
+			c1 = pexpr_implies(pexf(choice->fexpr_y), c1, data,
+						PEXPR_ARGX);
+			sym_add_constraint(sym, c1, data);
+			pexpr_put(c1);
+		}
+	}
+	sym_list_free(promptItems);
+	sym_list_free(items);
+}
+
+/*
+ * build the constraints for invisible options such as defaults
+ */
+static void add_invisible_constraints(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prompt = sym_get_prompt(sym);
+	struct pexpr *promptCondition_both, *promptCondition_yes, *noPromptCond;
+	struct pexpr *npc;
+	struct defm_list *defaults;
+	struct pexpr *default_y, *default_m, *default_both;
+
+	/* no constraints for the prompt, nothing to do here */
+	if (prompt != NULL && !prompt->visible.expr)
+		return;
+
+	if (prompt == NULL) {
+		promptCondition_both = pexf(data->constants->const_false);
+		promptCondition_yes = pexf(data->constants->const_false);
+		noPromptCond = pexf(data->constants->const_true);
+	} else {
+		struct property *p;
+
+		promptCondition_both = pexf(data->constants->const_false);
+		promptCondition_yes = pexf(data->constants->const_false);
+
+		/* some symbols have multiple prompts */
+		for_all_prompts(sym, p) {
+			promptCondition_both =
+				pexpr_or(promptCondition_both,
+					      expr_calculate_pexpr_both(
+						      p->visible.expr, data),
+					      data, PEXPR_ARGX);
+			promptCondition_yes = pexpr_or(
+				promptCondition_yes,
+				expr_calculate_pexpr_y(p->visible.expr, data),
+				data, PEXPR_ARGX);
+		}
+		noPromptCond = pexpr_not_share(promptCondition_both, data);
+	}
+
+	if (NPC_OPTIMISATION) {
+		struct fexpr *npc_fe =
+			fexpr_create(data->sat_variable_nr++, FE_NPC, "");
+
+		if (sym_is_choice(sym))
+			str_append(&npc_fe->name, "Choice_");
+
+		str_append(&npc_fe->name, sym_get_name(sym));
+		str_append(&npc_fe->name, "_NPC");
+		sym->noPromptCond = npc_fe;
+		fexpr_add_to_satmap(npc_fe, data);
+
+		npc = pexf(npc_fe);
+
+		if (!sym_is_choice_value(sym) && !sym_is_choice(sym)) {
+			struct pexpr *c =
+				pexpr_implies_share(noPromptCond, npc, data);
+			sym_add_constraint(sym, c, data);
+			pexpr_put(c);
+		}
+	} else {
+		npc = pexpr_get(noPromptCond);
+	}
+
+	defaults = get_defaults(sym, data);
+	default_y = get_default_y(defaults, data);
+	default_m = get_default_m(defaults, data);
+	default_both = pexpr_or_share(default_y, default_m, data);
+
+	/* tristate elements are only selectable as yes, if they are visible as yes */
+	if (sym->type == S_TRISTATE) {
+		struct pexpr *e1 = pexpr_implies(
+			promptCondition_both,
+			pexpr_implies(pexf(sym->fexpr_y),
+					   promptCondition_yes, data,
+					   PEXPR_ARG1),
+			data, PEXPR_ARG2);
+
+		sym_add_constraint(sym, e1, data);
+		pexpr_put(e1);
+	}
+
+	/* if invisible and off by default, then a symbol can only be deactivated by its reverse
+	 * dependencies
+	 */
+	if (sym->type == S_TRISTATE) {
+		struct pexpr *sel_y, *sel_m, *sel_both;
+		struct pexpr *c1, *c2, *c3;
+		struct pexpr *d1, *d2, *d3;
+		struct pexpr *e1, *e2, *e3;
+
+		if (sym->fexpr_sel_y != NULL) {
+			sel_y = pexpr_implies(pexf(sym->fexpr_y),
+						   pexf(sym->fexpr_sel_y), data,
+						   PEXPR_ARGX);
+			sel_m = pexpr_implies(pexf(sym->fexpr_m),
+						   pexf(sym->fexpr_sel_m), data,
+						   PEXPR_ARGX);
+			sel_both = pexpr_implies(
+				pexf(sym->fexpr_y),
+				pexpr_or(pexf(sym->fexpr_sel_m),
+					      pexf(sym->fexpr_sel_y), data,
+					      PEXPR_ARGX),
+				data, PEXPR_ARGX);
+		} else {
+			sel_y = pexpr_not(pexf(sym->fexpr_y), data);
+			sel_m = pexpr_not(pexf(sym->fexpr_m), data);
+			sel_both = pexpr_get(sel_y);
+		}
+
+		c1 = pexpr_implies(pexpr_not_share(default_y, data), sel_y,
+					data, PEXPR_ARG1);
+		c2 = pexpr_implies(pexf(modules_sym->fexpr_y), c1, data,
+					PEXPR_ARG1);
+		c3 = pexpr_implies_share(npc, c2, data);
+		sym_add_constraint(sym, c3, data);
+
+		d1 = pexpr_implies(pexpr_not_share(default_m, data), sel_m,
+					data, PEXPR_ARG1);
+		d2 = pexpr_implies(pexf(modules_sym->fexpr_y), d1, data,
+					PEXPR_ARG1);
+		d3 = pexpr_implies_share(npc, d2, data);
+		sym_add_constraint(sym, d3, data);
+
+		e1 = pexpr_implies(pexpr_not_share(default_both, data),
+					sel_both, data, PEXPR_ARG1);
+		e2 = pexpr_implies(
+			pexpr_not(pexf(modules_sym->fexpr_y), data), e1,
+			data, PEXPR_ARG1);
+		e3 = pexpr_implies_share(npc, e2, data);
+		sym_add_constraint(sym, e3, data);
+		PEXPR_PUT(sel_y, sel_m, sel_both, c1, c2, c3, d1, d2, d3, e1,
+			  e2, e3);
+	} else if (sym->type == S_BOOLEAN) {
+		struct pexpr *sel_y;
+		struct pexpr *e1, *e2;
+
+		if (sym->fexpr_sel_y != NULL)
+			sel_y = pexpr_implies(pexf(sym->fexpr_y),
+						   pexf(sym->fexpr_sel_y), data,
+						   PEXPR_ARGX);
+		else
+			sel_y = pexpr_not(pexf(sym->fexpr_y), data);
+
+		e1 = pexpr_implies(pexpr_not_share(default_both, data),
+					sel_y, data, PEXPR_ARG1);
+		e2 = pexpr_implies_share(npc, e1, data);
+
+		sym_add_constraint_eq(sym, e2, data);
+		PEXPR_PUT(sel_y, e1, e2);
+	} else {
+		/* if non-boolean is invisible and no default's condition is
+		 * fulfilled, then the symbol is not set
+		 */
+		struct pexpr *default_any = get_default_any(sym, data);
+		struct pexpr *e1 = pexf(data->constants->const_true);
+		struct pexpr *e2, *e3;
+
+		/* e1 = "sym is not set" */
+		for (struct fexpr_node *node = sym->nb_vals->head->next;
+		     node != NULL; node = node->next)
+			e1 = pexpr_and(
+				e1, pexpr_not(pexf(node->elem), data),
+				data, PEXPR_ARGX);
+
+		e2 = pexpr_implies(pexpr_not_share(default_any, data), e1,
+					data, PEXPR_ARG1);
+		e3 = pexpr_implies_share(npc, e2, data);
+
+		sym_add_constraint(sym, e3, data);
+		PEXPR_PUT(default_any, e1, e2, e3);
+	}
+
+	/* if invisible and on by default, then a symbol can only be deactivated by its
+	 * dependencies
+	 */
+	if (defaults->size == 0) {
+		// nothing to do
+	} else if (sym->type == S_TRISTATE) {
+		struct pexpr *e1;
+		struct pexpr *e2;
+
+		e1 = pexpr_implies(npc,
+					pexpr_implies(default_y,
+							   pexf(sym->fexpr_y),
+							   data, PEXPR_ARG2),
+					data, PEXPR_ARG2);
+		sym_add_constraint(sym, e1, data);
+
+		e2 = pexpr_implies(
+			npc,
+			pexpr_implies(default_m,
+					   sym_get_fexpr_both(sym, data),
+					   data, PEXPR_ARG2),
+			data, PEXPR_ARG2);
+		sym_add_constraint(sym, e2, data);
+		PEXPR_PUT(e1, e2);
+	} else if (sym->type == S_BOOLEAN) {
+		struct pexpr *c;
+		struct pexpr *c2;
+
+		c = pexpr_implies(default_both, pexf(sym->fexpr_y), data,
+				       PEXPR_ARG2);
+
+		// TODO tristate choice hack
+
+		c2 = pexpr_implies_share(npc, c, data);
+		sym_add_constraint(sym, c2, data);
+		PEXPR_PUT(c, c2);
+	} else {
+		/* if non-boolean invisible, then it assumes the correct
+		 * default (if any).
+		 */
+		struct defm_node *node;
+		struct pexpr *cond, *c;
+		struct fexpr *f;
+
+		defm_list_for_each(node, defaults) {
+			f = node->elem->val;
+			cond = node->elem->e;
+			c = pexpr_implies(npc,
+					       pexpr_implies(cond, pexf(f), data, PEXPR_ARG2),
+					       data, PEXPR_ARG2);
+			sym_add_constraint(sym, c, data);
+			pexpr_put(c);
+		}
+	}
+
+	PEXPR_PUT(promptCondition_yes, promptCondition_both, noPromptCond, npc,
+		  default_y, default_m, default_both);
+	defm_list_destruct(defaults);
+}
+
+/*
+ * add the known values from the default and range properties
+ */
+static void sym_add_nonbool_values_from_default_range(struct symbol *sym,
+						      struct cfdata *data)
+{
+	struct property *p;
+
+	for_all_defaults(sym, p) {
+		if (p == NULL)
+			continue;
+
+		/* add the value to known values, if it doesn't exist yet */
+		sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data);
+	}
+
+	for_all_properties(sym, p, P_RANGE) {
+		if (p == NULL)
+			continue;
+
+		/* add the values to known values, if they don't exist yet */
+		sym_create_nonbool_fexpr(sym, p->expr->left.sym->name, data);
+		sym_create_nonbool_fexpr(sym, p->expr->right.sym->name, data);
+	}
+}
+
+/*
+ * build the range constraints for int/hex:
+ * For each range and each value in `sym->nb_vals` that's not in the range:
+ *	If the range's condition is fulfilled, then sym can't have this value.
+ */
+static void sym_add_range_constraints(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prop;
+	struct pexpr *prevs;
+	struct pexpr *propCond;
+	struct pexpr_list *prevCond; // list of all conditions of the ranges
+		// from the previous iterations
+	prevCond = pexpr_list_init();
+
+	for_all_properties(sym, prop, P_RANGE) {
+		int base;
+		long long range_min, range_max, tmp;
+		struct fexpr_node *node;
+
+		if (prop == NULL)
+			continue;
+
+		prevs = pexf(data->constants->const_true);
+		propCond = prop_get_condition(prop, data);
+
+		// construct prevs as "none of the previous ranges' conditions
+		// were fulfilled but this range's condition is"
+		if (prevCond->size == 0) {
+			pexpr_put(prevs);
+			prevs = pexpr_get(propCond);
+;
+		} else {
+			struct pexpr_node *node;
+
+			pexpr_list_for_each(node, prevCond)
+				prevs = pexpr_and(pexpr_not_share(node->elem,
+								  data),
+						  prevs, data, PEXPR_ARGX);
+
+			prevs = pexpr_and(propCond, prevs, data,
+					       PEXPR_ARG2);
+		}
+		pexpr_list_add(prevCond, pexpr_get(propCond));
+
+		switch (sym->type) {
+		case S_INT:
+			base = 10;
+			break;
+		case S_HEX:
+			base = 16;
+			break;
+		default:
+			return;
+		}
+
+		range_min = sym_get_range_val(prop->expr->left.sym, base);
+		range_max = sym_get_range_val(prop->expr->right.sym, base);
+
+		/* can skip the first non-boolean value, since this is 'n' */
+		fexpr_list_for_each(node, sym->nb_vals) {
+			struct pexpr *not_nb_val;
+			struct pexpr *c;
+
+			if (node->prev == NULL)
+				continue;
+
+			tmp = strtoll(str_get(&node->elem->nb_val), NULL, base);
+
+			/* known value is in range, nothing to do here */
+			if (tmp >= range_min && tmp <= range_max)
+				continue;
+
+			not_nb_val = pexpr_not(pexf(node->elem), data);
+			c = pexpr_implies_share(prevs, not_nb_val, data);
+			sym_add_constraint(sym, c, data);
+			PEXPR_PUT(not_nb_val, c);
+		}
+		PEXPR_PUT(prevs, propCond);
+	}
+
+	pexpr_list_free_put(prevCond);
+
+}
+
+/*
+ * at least 1 of the known values for a non-boolean symbol must be true
+ */
+static void sym_nonbool_at_least_1(struct symbol *sym, struct cfdata *data)
+{
+	struct pexpr *e = NULL;
+	struct fexpr_node *node;
+
+	if (!sym_is_nonboolean(sym))
+		return;
+
+	fexpr_list_for_each(node, sym->nb_vals) {
+		if (node->prev == NULL)
+			e = pexf(node->elem);
+		else
+			e = pexpr_or(e, pexf(node->elem), data, PEXPR_ARGX);
+	}
+	sym_add_constraint(sym, e, data);
+	pexpr_put(e);
+}
+
+/*
+ * at most 1 of the known values for a non-boolean symbol can be true
+ */
+static void sym_nonbool_at_most_1(struct symbol *sym, struct cfdata *data)
+{
+	struct fexpr_node *node1;
+
+	if (!sym_is_nonboolean(sym))
+		return;
+
+	/* iterate over all subsets of sym->nb_vals of size 2 */
+	fexpr_list_for_each(node1, sym->nb_vals) {
+		struct pexpr *e1 = pexf(node1->elem);
+
+		for (struct fexpr_node *node2 = node1->next; node2 != NULL;
+		     node2 = node2->next) {
+			struct pexpr *e2 = pexf(node2->elem);
+			struct pexpr *e = pexpr_or(pexpr_not_share(e1, data),
+						   pexpr_not_share(e2, data),
+						   data, PEXPR_ARGX);
+
+			sym_add_constraint(sym, e, data);
+			PEXPR_PUT(e, e2);
+		}
+		pexpr_put(e1);
+	}
+}
+
+/*
+ * a visible prompt for a non-boolean implies a value for the symbol
+ */
+static void sym_add_nonbool_prompt_constraint(struct symbol *sym,
+					      struct cfdata *data)
+{
+	struct property *prompt;
+	struct pexpr *promptCondition;
+	struct pexpr *n;
+	struct pexpr *c = NULL;
+
+	prompt = sym_get_prompt(sym);
+	if (prompt == NULL)
+		return;
+
+	promptCondition = prop_get_condition(prompt, data);
+	n = pexf(sym_get_nonbool_fexpr(sym, "n"));
+
+	if (n->type != PE_SYMBOL || n->left.fexpr == NULL)
+		goto cleanup;
+
+	c = pexpr_implies(promptCondition, pexpr_not_share(n, data), data,
+			  PEXPR_ARG2);
+
+	sym_add_constraint(sym, c, data);
+
+cleanup:
+	PEXPR_PUT(n, promptCondition, c);
+}
+
+static struct default_map *create_default_map_entry(struct fexpr *val,
+						    struct pexpr *e)
+{
+	struct default_map *map = malloc(sizeof(struct default_map));
+
+	pexpr_get(e);
+	map->val = val;
+	map->e = e;
+
+	return map;
+}
+
+/**
+ * findDefaultEntry()
+ * @val: Value that the entry must have
+ * @defaults: List of defaults to search in
+ * @constants: To get ``constants->const_false`` from
+ *
+ * Finds an entry in @defaults whose &default_map.val attribute is the same
+ * pointer as the @val argument.
+ *
+ * Return: The condition &default_map.e of the found entry, or
+ * ``pexf(constants->const_false)`` if none was found. To be pexpr_put() by the
+ * caller.
+ */
+static struct pexpr *findDefaultEntry(struct fexpr *val,
+				      struct defm_list *defaults,
+				      struct constants *constants)
+{
+	struct defm_node *node;
+
+	defm_list_for_each(node, defaults) {
+		if (val == node->elem->val) {
+			pexpr_get(node->elem->e);
+			return node->elem->e;
+		}
+	}
+
+	return pexf(constants->const_false);
+}
+
+/*
+ * accumulated during execution of add_defaults(), a disjunction of the
+ * conditions for all default props of a symbol
+ */
+static struct pexpr *covered;
+
+static bool is_tri_as_num(struct symbol *sym)
+{
+	if (!sym->name)
+		return false;
+
+	return !strcmp(sym->name, "0")
+		|| !strcmp(sym->name, "1")
+		|| !strcmp(sym->name, "2");
+}
+
+/**
+ * add_to_default_map() - Add to or update an entry in a default list
+ * @entry: Will be consumed by this function, i.e. the caller should and need
+ * only access @entry via @defaults.
+ */
+static void add_to_default_map(struct defm_list *defaults,
+			       struct default_map *entry, struct symbol *sym)
+{
+	/* as this is a map, the entry must be replaced if it already exists */
+	if (sym_is_boolean(sym)) {
+		struct default_map *map;
+		struct defm_node *node;
+
+		defm_list_for_each(node, defaults) {
+			map = node->elem;
+			if (map->val->sym == entry->val->sym) {
+				pexpr_put(map->e);
+				map->e = entry->e;
+				free(entry);
+				return;
+			}
+		}
+		defm_list_add(defaults, entry);
+	} else {
+		struct default_map *map;
+		struct defm_node *node;
+
+		defm_list_for_each(node, defaults) {
+			map = node->elem;
+			if (map->val->satval == entry->val->satval) {
+				pexpr_put(map->e);
+				map->e = entry->e;
+				free(entry);
+				return;
+			}
+		}
+		defm_list_add(defaults, entry);
+	}
+}
+
+/**
+ * updateDefaultList() - Update a default list with a new value-condition pair
+ * @val: The value whose condition will be updated
+ * @newCond: The condition of the default prop. Does not include the condition
+ * that the earlier default's conditions are not fulfilled.
+ * @result: the default list
+ * @sym: the symbol that the defaults belong to
+ *
+ * Update the condition that @val will be used for @sym by considering the next
+ * default property, whose condition is given by @newCond.
+ */
+static void updateDefaultList(struct fexpr *val, struct pexpr *newCond,
+			      struct defm_list *result, struct symbol *sym,
+			      struct cfdata *data)
+{
+	// The current condition of @val deduced from the previous default props
+	struct pexpr *prevCond = findDefaultEntry(val, result, data->constants);
+	// New combined condition for @val
+	struct pexpr *condUseVal =
+		pexpr_or(prevCond,
+			 pexpr_and(newCond, pexpr_not_share(covered, data),
+				   data, PEXPR_ARG2),
+			 data, PEXPR_ARG2);
+	add_to_default_map(result, create_default_map_entry(val, condUseVal),
+			   sym);
+	covered = pexpr_or(covered, newCond, data, PEXPR_ARG1);
+	PEXPR_PUT(prevCond, condUseVal);
+}
+
+/**
+ * add_defaults() - Generate list of default values and their conditions
+ * @defaults: List of the default properties
+ * @ctx: Additional condition that needs to be fulfilled for any default. May be
+ * NULL.
+ * @result: List that will be filled
+ * @sym: Symbol that the defaults belong to
+ *
+ * Creates a map from values that @sym can assume to the conditions under which
+ * they will be assumed. Without @ctx, this will only consider the conditions
+ * directly associated with the defaults, e.g. sym->dir_dep would not be
+ * considered.
+ *
+ * As a side effect, the &symbol->nb_vals of @sym will be added for
+ * all default values (as well as the @symbol->nb_vals of other symbols @sym has
+ * as default (recursively)).
+ */
+static void add_defaults(struct prop_list *defaults, struct expr *ctx,
+			 struct defm_list *result, struct symbol *sym,
+			 struct cfdata *data)
+{
+	struct prop_node *node;
+	struct property *p;
+	struct expr *expr;
+
+	prop_list_for_each(node, defaults) {
+		p = node->elem;
+		/* calculate expr as whether the default's condition (and the
+		 * one inherited from ctx) is fulfilled
+		 */
+		if (p->visible.expr) {
+			if (ctx == NULL)
+				expr = expr_copy(p->visible.expr);
+			else
+				expr = expr_alloc_and(
+					expr_copy(p->visible.expr),
+					expr_copy(ctx));
+		} else {
+			if (ctx == NULL)
+				expr = expr_alloc_symbol(&symbol_yes);
+			else
+				expr = expr_alloc_and(
+					expr_alloc_symbol(&symbol_yes),
+					expr_copy(ctx));
+		}
+
+		/* if tristate and def.value = y */
+		if (p->expr->type == E_SYMBOL && sym->type == S_TRISTATE &&
+		    p->expr->left.sym == &symbol_yes) {
+			struct pexpr *expr_y =
+				expr_calculate_pexpr_y(expr, data);
+			struct pexpr *expr_m =
+				expr_calculate_pexpr_m(expr, data);
+
+			updateDefaultList(data->constants->symbol_yes_fexpr,
+					  expr_y, result, sym, data);
+			updateDefaultList(data->constants->symbol_mod_fexpr,
+					  expr_m, result, sym, data);
+			PEXPR_PUT(expr_y, expr_m);
+		}
+		/* if def.value = n/m/y */
+		else if (p->expr->type == E_SYMBOL &&
+			 sym_is_tristate_constant(p->expr->left.sym) &&
+			 sym_is_boolean(sym)) {
+			struct fexpr *s;
+			struct pexpr *expr_both =
+				expr_calculate_pexpr_both(expr, data);
+
+			if (p->expr->left.sym == &symbol_yes)
+				s = data->constants->symbol_yes_fexpr;
+			else if (p->expr->left.sym == &symbol_mod)
+				s = data->constants->symbol_mod_fexpr;
+			else
+				s = data->constants->symbol_no_fexpr;
+
+			updateDefaultList(s, expr_both, result, sym, data);
+			pexpr_put(expr_both);
+		}
+		/* if def.value = n/m/y, but written as 0/1/2 for a boolean */
+		else if (sym_is_boolean(sym) && p->expr->type == E_SYMBOL &&
+			 p->expr->left.sym->type == S_UNKNOWN &&
+			 is_tri_as_num(p->expr->left.sym)) {
+			struct fexpr *s;
+			struct pexpr *expr_both =
+				expr_calculate_pexpr_both(expr, data);
+
+			if (!strcmp(p->expr->left.sym->name, "0"))
+				s = data->constants->symbol_no_fexpr;
+			else if (!strcmp(p->expr->left.sym->name, "1"))
+				s = data->constants->symbol_mod_fexpr;
+			else
+				s = data->constants->symbol_yes_fexpr;
+
+			updateDefaultList(s, expr_both, result, sym, data);
+			pexpr_put(expr_both);
+		}
+		/* if def.value = non-boolean constant */
+		else if (expr_is_nonbool_constant(p->expr)) {
+			struct fexpr *s = sym_get_or_create_nonbool_fexpr(
+				sym, p->expr->left.sym->name, data);
+			struct pexpr *expr_both =
+				expr_calculate_pexpr_both(expr, data);
+
+			updateDefaultList(s, expr_both, result, sym, data);
+			pexpr_put(expr_both);
+		}
+		/* any expression which evaluates to n/m/y for a tristate */
+		else if (sym->type == S_TRISTATE) {
+			struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr),
+							    expr_copy(expr));
+			struct pexpr *expr_y =
+				expr_calculate_pexpr_y(e_tmp, data);
+			struct pexpr *expr_m =
+				expr_calculate_pexpr_m(e_tmp, data);
+
+			updateDefaultList(data->constants->symbol_yes_fexpr,
+					  expr_y, result, sym, data);
+			updateDefaultList(data->constants->symbol_mod_fexpr,
+					  expr_m, result, sym, data);
+			PEXPR_PUT(expr_y, expr_m);
+			expr_free(e_tmp);
+		}
+		/* if non-boolean && def.value = non-boolean symbol */
+		else if (p->expr->type == E_SYMBOL && sym_is_nonboolean(sym) &&
+			 sym_is_nonboolean(p->expr->left.sym)) {
+			struct prop_list *nb_sym_defaults = prop_list_init();
+			struct property *p_tmp;
+
+			/* Add defaults of other symbol as possible defaults for
+			 * this symbol
+			 */
+			for_all_defaults(p->expr->left.sym, p_tmp)
+				prop_list_add(nb_sym_defaults, p_tmp);
+
+			add_defaults(nb_sym_defaults, expr, result, sym, data);
+			prop_list_free(nb_sym_defaults);
+		}
+		/* any expression which evaluates to n/m/y */
+		else {
+			struct expr *e_tmp = expr_alloc_and(expr_copy(p->expr),
+							    expr_copy(expr));
+			struct pexpr *expr_both =
+				expr_calculate_pexpr_both(e_tmp, data);
+
+			updateDefaultList(data->constants->symbol_yes_fexpr,
+					  expr_both, result, sym, data);
+
+			pexpr_put(expr_both);
+			expr_free(e_tmp);
+		}
+		expr_free(expr);
+	}
+}
+
+/**
+ * get_defaults() - Generate list of default values and their conditions
+ * @sym: Symbol whose defaults we want to look at
+ *
+ * Creates a map from values that @sym can assume to the conditions under which
+ * they will be assumed. This will only consider the conditions
+ * directly associated with the defaults, e.g. sym->dir_dep would not be
+ * considered.
+ *
+ * As a side effect, the &symbol->nb_vals of @sym will be added for
+ * all default values (as well as the @symbol->nb_vals of other symbols @sym has
+ * as default (recursively)).
+ */
+static struct defm_list *get_defaults(struct symbol *sym, struct cfdata *data)
+{
+	struct defm_list *result = defm_list_init();
+	struct prop_list *defaults; /* list of default props of sym */
+	struct property *p;
+
+	covered = pexf(data->constants->const_false);
+
+	defaults = prop_list_init();
+	for_all_defaults(sym, p)
+		prop_list_add(defaults, p);
+
+	add_defaults(defaults, NULL, result, sym, data);
+	prop_list_free(defaults);
+	pexpr_put(covered);
+
+	return result;
+}
+
+/*
+ * return the condition for "y", False if it doesn't exist
+ */
+static struct pexpr *get_default_y(struct defm_list *list, struct cfdata *data)
+{
+	struct default_map *entry;
+	struct defm_node *node;
+
+	defm_list_for_each(node, list) {
+		entry = node->elem;
+		if (entry->val->type == FE_SYMBOL &&
+		    entry->val->sym == &symbol_yes) {
+			pexpr_get(entry->e);
+			return entry->e;
+		}
+	}
+
+	return pexf(data->constants->const_false);
+}
+
+/*
+ * return the condition for "m", False if it doesn't exist
+ */
+static struct pexpr *get_default_m(struct defm_list *list, struct cfdata *data)
+{
+	struct default_map *entry;
+	struct defm_node *node;
+
+	defm_list_for_each(node, list) {
+		entry = node->elem;
+		if (entry->val->type == FE_SYMBOL &&
+		    entry->val->sym == &symbol_mod) {
+			pexpr_get(entry->e);
+			return entry->e;
+		}
+	}
+
+	return pexf(data->constants->const_false);
+}
+
+/*
+ * return the constraint when _some_ default value will be applied
+ */
+static struct pexpr *get_default_any(struct symbol *sym, struct cfdata *data)
+{
+	struct property *prop;
+	struct expr *e;
+	struct pexpr *p;
+
+	if (!sym_is_nonboolean(sym))
+		return NULL;
+
+	p = pexf(data->constants->const_false);
+	for_all_defaults(sym, prop) {
+		if (prop->visible.expr)
+			e = expr_copy(prop->visible.expr);
+		else
+			e = expr_alloc_symbol(&symbol_yes);
+
+		if (expr_can_evaluate_to_mod(e))
+			p = pexpr_or(p, expr_calculate_pexpr_both(e, data),
+				     data, PEXPR_ARGX);
+
+		p = pexpr_or(p, expr_calculate_pexpr_y(e, data), data,
+			     PEXPR_ARGX);
+
+		expr_free(e);
+	}
+
+	return p;
+}
+
+/*
+ * get the value for the range
+ */
+static long sym_get_range_val(struct symbol *sym, int base)
+{
+	sym_calc_value(sym);
+	switch (sym->type) {
+	case S_INT:
+		base = 10;
+		break;
+	case S_HEX:
+		base = 16;
+		break;
+	default:
+		break;
+	}
+	return strtol(sym->curr.val, NULL, base);
+}
+
+/*
+ * count the number of all constraints
+ */
+unsigned int count_counstraints(void)
+{
+	unsigned int c = 0;
+	struct symbol *sym;
+
+	for_all_symbols(sym) {
+		if (sym->type == S_UNKNOWN)
+			continue;
+
+		c += sym->constraints->size;
+	}
+
+	return c;
+}
+
+/*
+ * add a constraint for a symbol
+ */
+void sym_add_constraint(struct symbol *sym, struct pexpr *constraint,
+			struct cfdata *data)
+{
+	if (!constraint)
+		return;
+
+	/* no need to add that */
+	if (constraint->type == PE_SYMBOL &&
+	    constraint->left.fexpr == data->constants->const_true)
+		return;
+
+	/* this should never happen */
+	if (constraint->type == PE_SYMBOL &&
+	    constraint->left.fexpr == data->constants->const_false)
+		perror("Adding const_false.");
+
+	pexpr_list_add(sym->constraints, pexpr_get(constraint));
+
+	if (!pexpr_is_nnf(constraint))
+		pexpr_print("Not NNF:", constraint, -1);
+}
+
+/*
+ * add a constraint for a symbol, but check for duplicate constraints
+ */
+void sym_add_constraint_eq(struct symbol *sym, struct pexpr *constraint,
+			   struct cfdata *data)
+{
+	struct pexpr_node *node;
+
+	if (!constraint)
+		return;
+
+	/* no need to add that */
+	if (constraint->type == PE_SYMBOL &&
+	    constraint->left.fexpr == data->constants->const_true)
+		return;
+
+	/* this should never happen */
+	if (constraint->type == PE_SYMBOL &&
+	    constraint->left.fexpr == data->constants->const_false)
+		perror("Adding const_false.");
+
+	/* check the constraints for the same symbol */
+	pexpr_list_for_each(node, sym->constraints)
+		if (pexpr_eq(constraint, node->elem, data))
+			return;
+
+	pexpr_list_add(sym->constraints, pexpr_get(constraint));
+
+	if (!pexpr_is_nnf(constraint))
+		pexpr_print("Not NNF:", constraint, -1);
+}
diff --git a/scripts/kconfig/cf_constraints.h b/scripts/kconfig/cf_constraints.h
new file mode 100644
index 000000000000..97a18eaf11ca
--- /dev/null
+++ b/scripts/kconfig/cf_constraints.h
@@ -0,0 +1,26 @@ 
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * Copyright (C) 2023 Patrick Franz <deltaone@debian.org>
+ */
+
+#ifndef CF_CONSTRAINTS_H
+#define CF_CONSTRAINTS_H
+
+#include "cf_defs.h"
+#include "expr.h"
+
+/* build the constraints for each symbol */
+void get_constraints(struct cfdata *data);
+
+/* count the number of all constraints */
+unsigned int count_counstraints(void);
+
+/* add a constraint for a symbol */
+void sym_add_constraint(struct symbol *sym, struct pexpr *constraint, struct cfdata *data);
+
+void sym_add_constraint_fexpr(struct symbol *sym, struct fexpr *constraint);
+
+/* add a constraint for a symbol, but check for duplicate constraints */
+void sym_add_constraint_eq(struct symbol *sym, struct pexpr *constraint, struct cfdata *data);
+
+#endif