]> rtime.felk.cvut.cz Git - linux-conf-perf.git/blobdiff - kconfig2sat/kconfig2sat.cc
kconfig2sat: More work
[linux-conf-perf.git] / kconfig2sat / kconfig2sat.cc
index ed214eff819a0428ab13f6ba294cb17b55e0e8c8..356de0fde17a57d47c590325ca22cbf6196930ce 100644 (file)
@@ -6,10 +6,17 @@
 #include <libintl.h>
 #include <unistd.h>
 #include <getopt.h>
+#include <inttypes.h>
 
 #include "kconfig/lkc.h"
 #include "lcp_utils.h"
 
+#include <vector>
+#include <map>
+#include <memory>
+
+using namespace std;
+
 int verbosity = 0;
 
 enum options {
@@ -41,12 +48,100 @@ void print_help()
                 );
 }
 
+char *expr_to_string(struct expr *e);
+
+char *sym_to_string(struct symbol *sym)
+{
+       char *ret;
+
+       if (sym->name)
+               asprintf(&ret, sym->name);
+       else
+               asprintf(&ret, "NONAME%d", sym->lcp.id);
+       return ret;
+}
+
+char *expr_binop_to_string(struct expr *e, const char *op_str)
+{
+       char *l = expr_to_string(e->left.expr);
+       char *r = expr_to_string(e->right.expr);
+       char *ret;
+
+       asprintf(&ret, "(%s %s %s)", l, op_str, r);
+       free(l);
+       free(r);
+       return ret;
+}
+
+char *expr_comp_to_string(struct expr *e, const char *op_str)
+{
+       char *l = sym_to_string(e->left.sym);
+       char *r = sym_to_string(e->right.sym);
+       char *ret;
+
+       asprintf(&ret, "(%s %s %s)", l, op_str, r);
+       free(l);
+       free(r);
+       return ret;
+}
+
+char *expr_to_string(struct expr *e)
+{
+       char *ret = NULL;
+       char *tmp;
+
+       if (!e)
+               return NULL;
+
+       switch (e->type) {
+       case E_NONE:
+               asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr));
+               return ret;
+       case E_OR:
+               return expr_binop_to_string(e, "||");
+       case E_AND:
+               return expr_binop_to_string(e, "&&");
+       case E_NOT:
+               tmp = expr_to_string(e->left.expr);
+               asprintf(&ret, "!%s", tmp);
+               free(tmp);
+               return ret;
+       case E_EQUAL:
+               return expr_comp_to_string(e, "==");
+       case E_UNEQUAL:
+               return expr_comp_to_string(e, "!=");
+       case E_LTH:
+               return expr_comp_to_string(e, "<");
+       case E_LEQ:
+               return expr_comp_to_string(e, "<=");
+       case E_GTH:
+               return expr_comp_to_string(e, ">");
+       case E_GEQ:
+               return expr_comp_to_string(e, ">=");
+       case E_LIST:
+               fprintf(stderr, "LIST not implemented\n");
+               exit(EXIT_FAILURE);
+               break;
+       case E_SYMBOL:
+               return sym_to_string(e->left.sym);
+       case E_RANGE:
+               fprintf(stderr, "RANGE not implemented\n");
+               exit(EXIT_FAILURE);
+               break;
+       }
+
+       return ret;
+}
+
+
+
 void dump_symbol(struct symbol *sym)
 {
        struct property *prop;
-       const char *name = sym->name;
+       const char *name = sym_to_string(sym);
        const char *type = sym_type_name(sym->type);
        const char *prompt = NULL;
+       char *tmp;
        char flags[256] = "fl(";
        char val = '.';
 
@@ -83,6 +178,22 @@ void dump_symbol(struct symbol *sym)
        }
 
        printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
+
+       if (verbosity > 0) {
+               if (sym->dir_dep.expr) {
+                       tmp = expr_to_string(sym->dir_dep.expr);
+                       printf("    depends %s\n", tmp);
+                       free(tmp);
+               }
+
+               for_all_properties(sym, prop, P_SELECT) {
+                       assert(prop->expr->type == E_SYMBOL);
+                       tmp = expr_to_string(prop->visible.expr);
+                       printf("    selects %s if %s\n", prop->expr->left.sym->name, tmp);
+                       free(tmp);
+
+               }
+       }
 }
 
 void do_dump()
@@ -134,9 +245,332 @@ void read_varfile(const char *varfile)
                if (!prompt) {
                        fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
                }
+               sym->lcp.variable = 1;
        }
+       fclose(f);
 }
 
+struct SatLiteral {
+       struct symbol *sym;
+       struct expr *expr;
+
+       SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
+       SatLiteral(struct expr *e)   : sym(nullptr), expr(e) {}
+       bool has_fixed_value() const { return sym && !sym->lcp.variable; }
+       sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; }
+       bool value() const { assert(sym); return sym->curr.tri == yes; }
+};
+
+typedef vector<sat_id> SatClause;
+
+struct SatExpr {
+       sat_id left, right;
+       enum expr_type op;
+
+       SatExpr(int l, enum expr_type o, int r)
+               : left(l), right(r), op(o) {}
+       bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
+};
+
+class SatLiterals : public vector<struct SatLiteral>
+{
+public:
+       int fixed = {0};
+       SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
+       int count() const { return size() - 1; }
+};
+
+
+/*
+ * bool FOO!=n => FOO
+ * bool FOO!=y => !FOO
+ * bool FOO==n => !FOO
+ * bool FOO==y => FOO
+ */
+struct expr *expr_eliminate_eq_yn(struct expr *e)
+{
+       if (!e)
+               return NULL;
+       switch (e->type) {
+       case E_AND:
+       case E_OR:
+       case E_NOT:
+               e->left.expr = expr_eliminate_eq_yn(e->left.expr);
+               e->right.expr = expr_eliminate_eq_yn(e->right.expr);
+               break;
+       case E_UNEQUAL:
+               // UNKNOWN symbols sometimes occur in dependency -
+               // e.g. ACPI_VIDEO on arm (the symbol is only defined
+               // for ACPI platforms (x86) but some drivers refer to
+               // it.
+               if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
+                       if (e->right.sym == &symbol_no) {
+                               // FOO!=n -> FOO
+                               e->type = E_SYMBOL;
+                               e->right.sym = NULL;
+                       } else if (e->right.sym == &symbol_yes) {
+                               // FOO!=y -> !FOO
+                               e->type = E_SYMBOL;
+                               e->right.sym = NULL;
+                               e = expr_alloc_one(E_NOT, e);
+                       }
+               }
+               break;
+       case E_EQUAL:
+               if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
+                       if (e->right.sym == &symbol_yes) {
+                               // FOO==y -> FOO
+                               e->type = E_SYMBOL;
+                               e->right.sym = NULL;
+                       } else if (e->right.sym == &symbol_no) {
+                               // FOO==n -> !FOO
+                               e->type = E_SYMBOL;
+                               e->right.sym = NULL;
+                               e = expr_alloc_one(E_NOT, e);
+                       }
+               }
+               break;
+       default:
+               ;
+       }
+       return e;
+}
+
+
+class SatData {
+       SatLiterals literals = {};
+       vector<SatClause> clauses = {};
+       map<SatExpr, sat_id> expressions = {};
+
+public:
+
+       SatData() {
+               symbols2literals();
+               expressions2literals();
+               symbols2clauses();
+               expressions2clauses();
+       }
+
+       void add_symbol_literal(struct symbol *sym) {
+               literals.push_back(SatLiteral(sym));
+               sym->lcp.id = literals.count();
+       }
+
+       void symbols2literals() {
+               int i;
+               struct symbol *sym;
+
+               symbol_yes.type = S_TRISTATE;
+               symbol_no.type  = S_TRISTATE;
+               symbol_mod.type = S_TRISTATE;
+
+               add_symbol_literal(&symbol_yes);
+               add_symbol_literal(&symbol_no);
+               add_symbol_literal(&symbol_mod);
+
+               for_all_symbols(i, sym) {
+                       if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE || sym->type == S_UNKNOWN) {
+                               add_symbol_literal(sym);
+                       }
+               }
+       }
+
+       void expr2literal(struct expr *e) {
+               if (!e || e->lcp.id)
+                       return;
+
+               switch (e->type) {
+               case E_SYMBOL:
+                       e->lcp.id = e->left.sym->lcp.id;
+                       break;
+               case E_NONE:
+                       fprintf(stderr, "NONE not implemented\n");
+                       exit(EXIT_FAILURE);
+                       break;
+               case E_NOT: {
+                       expr2literal(e->left.expr);
+
+                       SatExpr se(e->left.expr->lcp.id, e->type, 0);
+                       auto it = expressions.find(se);
+                       if (it == expressions.end()) {
+                               literals.push_back(SatLiteral(e));
+                               expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
+                               e->lcp.id = literals.count();
+                       } else
+                               e->lcp.id = it->second;
+                       break;
+               }
+               case E_OR:
+               case E_AND: {
+                       expr2literal(e->left.expr);
+                       expr2literal(e->right.expr);
+
+                       SatExpr se(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id);
+                       auto it = expressions.find(se);
+                       if (it == expressions.end()) {
+                               literals.push_back(SatLiteral(e));
+                               expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
+                               e->lcp.id = literals.count();
+                       } else
+                               e->lcp.id = it->second;
+                       break;
+               }
+               case E_EQUAL:
+               case E_UNEQUAL:
+               case E_LTH:
+               case E_LEQ:
+               case E_GTH:
+               case E_GEQ: {
+                       SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id);
+                       auto it = expressions.find(se);
+                       if (it == expressions.end()) {
+                               literals.push_back(SatLiteral(e));
+                               expressions.insert(pair<SatExpr, sat_id>(se, literals.count()));
+                               e->lcp.id = literals.count();
+                       } else
+                               e->lcp.id = it->second;
+                       break;
+               }
+               case E_LIST:
+                       fprintf(stderr, "LIST not implemented\n");
+                       exit(EXIT_FAILURE);
+                       break;
+               case E_RANGE:
+                       fprintf(stderr, "RANGE not implemented\n");
+                       exit(EXIT_FAILURE);
+                       break;
+               }
+       }
+
+       void expressions2literals() {
+               int i;
+               struct symbol *sym;
+               struct property *prop;
+
+               for_all_symbols(i, sym) {
+                       if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
+                               assert(sym->lcp.id);
+                               if (sym->flags & SYMBOL_VALID && !sym->lcp.variable)
+                                       clauses.push_back(SatClause{ sym->curr.tri == yes ? sym->lcp.id : -sym->lcp.id });
+
+                               sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
+                               expr2literal(sym->dir_dep.expr);
+
+                               for_all_properties(sym, prop, P_SELECT) {
+                                       assert(prop->expr->type == E_SYMBOL);
+                                       prop->visible.expr = expr_eliminate_eq_yn(prop->visible.expr);
+                                       expr2literal(prop->visible.expr);
+                               }
+                       }
+               }
+       }
+
+       void symbols2clauses() {
+               for (auto lit: literals)
+                       if (lit.sym && lit.has_fixed_value())
+                               clauses.push_back(SatClause{ lit.value() ? lit.id() : -lit.id() });
+       }
+
+       void expressions2clauses() {
+               // Tseitin Transformation - see https://en.wikipedia.org/wiki/Tseitin_transformation
+               // or http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
+               for (auto expr: expressions) {
+                       SatExpr e = expr.first;
+                       sat_id e_id = expr.second;
+                       assert(e_id);
+                       if (e.left == 0 || (e.right == 0 && e.op != E_NOT)) {
+                               unique_ptr<char> tmp(expr_to_string(literals[e_id].expr));
+                               printf("Unexpected sat_id == 0 in %s\n", tmp.get());
+                               //exit(1);
+                       }
+                       switch (e.op) {
+                       case E_SYMBOL:
+                       case E_NONE:
+                               assert(0);
+                               break;
+                       case E_NOT:
+                               clauses.push_back(SatClause{  e_id,  e.left });
+                               clauses.push_back(SatClause{ -e_id, -e.left });
+                               break;
+                       case E_OR:
+                               clauses.push_back(SatClause{ -e.left,  e_id });
+                               clauses.push_back(SatClause{ -e.right, e_id });
+                               clauses.push_back(SatClause{ -e_id,    e.left, e.right });
+                               break;
+                       case E_AND:
+                               clauses.push_back(SatClause{ -e_id, e.left });
+                               clauses.push_back(SatClause{ -e_id, e.right });
+                               clauses.push_back(SatClause{ -e.left, -e.right, e_id });
+                               break;
+                       case E_EQUAL:
+                               clauses.push_back(SatClause{ -e_id, -e.left, e.right });
+                               clauses.push_back(SatClause{ -e_id, -e.right, e.left });
+                               clauses.push_back(SatClause{ -e.left, -e.right, e_id });
+                               clauses.push_back(SatClause{ e.left, e.right, e_id });
+                               break;
+                       case E_UNEQUAL:
+                               clauses.push_back(SatClause{ -e_id, -e.left, -e.right });
+                               clauses.push_back(SatClause{ -e_id, e.right, e.left });
+                               clauses.push_back(SatClause{ -e.left, e.right, e_id });
+                               clauses.push_back(SatClause{ e.left, -e.right, e_id });
+                               break;
+                       case E_LTH:
+                       case E_LEQ:
+                       case E_GTH:
+                       case E_GEQ: {
+                               struct expr *e = literals[e_id].expr;
+                               unique_ptr<char> tmp(expr_to_string(e));
+                               tristate val = expr_calc_value(e);
+                               //fprintf(stderr, "Comparison operators not implemented %s = %d\n", tmp.get(), val);
+                               //exit(EXIT_FAILURE);
+                               clauses.push_back(SatClause{ val == yes ? e_id : -e_id });
+                               break;
+                       }
+                       case E_LIST:
+                               fprintf(stderr, "LIST not implemented\n");
+                               exit(EXIT_FAILURE);
+                               break;
+                       case E_RANGE:
+                               fprintf(stderr, "RANGE not implemented\n");
+                               exit(EXIT_FAILURE);
+                               break;
+                       }
+               }
+
+       }
+
+       void write_dimacs_cnf(const char *cnf) {
+               FILE *f = fopen(cnf, "w");
+
+               if (!f) {
+                       perror(cnf);
+                       exit(EXIT_FAILURE);
+               }
+
+               fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
+
+               for (auto l: literals) {
+                       if (l.sym) {
+                               char val = l.has_fixed_value() ? (l.value() ? 'y' : 'n') : '?';
+                               fprintf(f, "c SYM %d %s = %c\n", l.sym->lcp.id, l.sym->name, val);
+                       }
+                       if (l.expr) {
+                               char *tmp = expr_to_string(l.expr);
+                               fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, tmp);
+                               free(tmp);
+                       }
+               }
+               for (auto clause: clauses) {
+                       for (sat_id id: clause) {
+                               assert(id != 0);
+                               fprintf(f, "%d ", id);
+                       }
+                       fprintf(f, "0\n");
+               }
+               fclose(f);
+       }
+};
+
 int main(int argc, char **argv)
 {
        int c;
@@ -220,306 +654,20 @@ int main(int argc, char **argv)
        textdomain(PACKAGE);
 
        conf_parse_path(kconfig);
-
        if (baseconf)
                conf_read(baseconf);
 
+       SatData sat_data;
+
        if (varfile)
                read_varfile(varfile);
 
        if (dump)
                do_dump();
 
-//     char *rules_file, *symbol_map_file, *variable_count_file;
-//     asprintf(&rules_file, "%s/%s", folder, DEFAULT_RULES_FILE);
-//     asprintf(&symbol_map_file, "%s/%s", folder, DEFAULT_SYMBOL_MAP_FILE);
-//     asprintf(&variable_count_file, "%s/%s", folder,
-//              DEFAULT_VARIABLE_COUNT_FILE);
-//     output_init(rules_file, symbol_map_file);
-
-//     build_symlist();
-//     cpy_dep();
-
-//     output_write_variable_count(variable_count_file,
-//                                 gsymlist->lastsym - 1, gsymlist->pos);
-
-//     output_finish();
-       return EXIT_SUCCESS;
-}
-
-#if 0
-
-void build_symlist() {
-    int i;
-    struct symbol *sym;
-    struct property *prop;
-    for_all_symbols(i, sym) {
-        if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
-            if (sym->name == NULL)
-                asprintf(&sym->name, "NONAMEGEN%d", noname_num++);
-
-            symlist_add(gsymlist, sym->name);
-        }
-    }
-    symlist_closesym(gsymlist);
-}
-
-/* TODO: Split to smaller functions with meaningful names */
-void cpy_dep() {
-    int i;
-    struct symbol *sym;
-    struct property *prop;
-    struct symlist_el *el;
-    unsigned el_id;
-    struct boolexpr *boolsym;
-    for_all_symbols(i, sym) {
-        if (sym->type != S_BOOLEAN && sym->type != S_TRISTATE)
-           continue;
-       el_id = symlist_id(gsymlist, sym->name);
-       el = &(gsymlist->array[el_id - 1]);
-       boolsym = boolexpr_sym(gsymlist, sym, false, NULL);
-       Iprintf("Processing: %s\n", sym->name);
-       // Visibility
-       for_all_prompts(sym, prop) {
-           Dprintf(" Prompt: %s\n", prop->text);
-           if (prop->visible.expr != NULL) {
-               doutput_expr(prop->visible.expr);
-               struct boolexpr *vis =
-                   boolexpr_kconfig(gsymlist, prop->visible.expr,
-                                    false, NULL);
-               if (el->vis == NULL) {
-                   el->vis = vis;
-               } else {
-                   el->vis = boolexpr_or(el->vis, vis);
-               }
-           } else if (el->vis == NULL) {
-               el->vis = boolexpr_true();
-           }
-       }
-       if (el->vis == NULL)
-           el->vis = boolexpr_false();
-       // Symbol is choice.. special treatment required
-       if (sym_is_choice(sym)) {
-           Dprintf(" Is Choice\n");
-           goto choice_exception;
-       }
-       // Default value
-       struct boolexpr **defexpr = NULL;
-       size_t defexpr_size = 0;
-       int z;
-       bool exitdef = false;
-       for_all_defaults(sym, prop) {
-           Dprintf(" Default value:\n");
-           doutput_expr(prop->expr);
-           struct boolexpr *def =
-               boolexpr_kconfig(gsymlist, prop->expr, true, NULL);
-           struct boolexpr *vis;
-           if (prop->visible.expr != NULL)
-               vis = boolexpr_kconfig(gsymlist, prop->visible.expr,
-                                      false, NULL);
-           else
-               vis = boolexpr_true();
-           if (vis->type != BT_TRUE) {
-               defexpr = realloc(defexpr,
-                                 ++defexpr_size * sizeof(struct boolexpr *));
-               defexpr[defexpr_size - 1] = boolexpr_copy(vis);
-           } else {
-               ++defexpr_size;
-               exitdef = true;
-           }
-           def = boolexpr_and(def, vis);
-           for (z = 0; z < ((int)defexpr_size - 1); z++) {
-               def = boolexpr_and(def, boolexpr_not(
-                                      boolexpr_copy(defexpr[z])));
-           }
-           if (el->def == NULL)
-               el->def = def;
-           else
-               el->def = boolexpr_or(el->def, def);
-           if (exitdef)
-               break;
-       }
-       if (defexpr != NULL) {
-           for (z = 0; z < defexpr_size - 1; z++) {
-               boolexpr_free(defexpr[z]);
-           }
-           free(defexpr);
-       }
-       if (el->def == NULL)
-           el->def = boolexpr_false();
-       // Dependency expression
-       if (sym->dir_dep.expr != NULL) {
-           Dprintf(" Dependency:\n");
-           doutput_expr(sym->dir_dep.expr);
-           el->dep =
-               boolexpr_kconfig(gsymlist, sym->dir_dep.expr, false, NULL);
-       } else
-           el->dep = boolexpr_true();
-       // Reverse dependency expression
-       if (sym->rev_dep.expr != NULL) {
-           Dprintf(" Reverse dependency:\n");
-           doutput_expr(sym->rev_dep.expr);
-           el->rev_dep =
-               boolexpr_kconfig(gsymlist, sym->rev_dep.expr, false, NULL);
-       } else
-           el->rev_dep = boolexpr_false();
-
-       if (el->dep->type != BT_FALSE && el->dep->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->dep);
-       if (el->rev_dep->type != BT_FALSE
-           && el->rev_dep->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->rev_dep);
-       if (el->def->type != BT_FALSE && el->def->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->def);
-       if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->vis);
-       // (!sym || dep) && (sym || !rev_dep) &&
-       // && (sym || !dep || !def || vis) &&
-       // (!sym || rev_dep || def || vis)
-       if (el->dep->type != BT_TRUE) {
-           output_rules_symbol(-1 * boolsym->id);
-           if (el->dep->type != BT_FALSE) {
-               output_rules_symbol(el->dep->id);
-           }
-           output_rules_endterm();
-       }
-       if (el->rev_dep->type != BT_FALSE) {
-           output_rules_symbol(boolsym->id);
-           if (el->rev_dep->type != BT_TRUE) {
-               output_rules_symbol(-1 * el->rev_dep->id);
-           }
-           output_rules_endterm();
-       }
-       if (el->dep->type != BT_FALSE && el->def->type != BT_FALSE
-           && el->vis->type != BT_TRUE) {
-           output_rules_symbol(boolsym->id);
-           if (el->dep->type != BT_TRUE) {
-               output_rules_symbol(-1 * el->dep->id);
-           }
-           if (el->def->type != BT_TRUE) {
-               output_rules_symbol(-1 * el->def->id);
-           }
-           if (el->vis->type != BT_FALSE) {
-               output_rules_symbol(el->vis->id);
-           }
-           output_rules_endterm();
-       }
-       if (el->rev_dep->type != BT_TRUE && el->def->type != BT_TRUE
-           && el->vis->type != BT_TRUE) {
-           output_rules_symbol(-1 * boolsym->id);
-           if (el->rev_dep->type != BT_FALSE) {
-               output_rules_symbol(el->rev_dep->id);
-           }
-           if (el->def->type != BT_FALSE) {
-               output_rules_symbol(el->def->id);
-           }
-           if (el->vis->type != BT_FALSE) {
-               output_rules_symbol(el->vis->id);
-           }
-           output_rules_endterm();
+       if (cnf) {
+               sat_data.write_dimacs_cnf(cnf);
        }
 
-       boolexpr_free(el->def);
-       boolexpr_free(el->vis);
-       boolexpr_free(el->dep);
-       boolexpr_free(el->rev_dep);
-
-       continue;
-
-    choice_exception:
-       // Add exclusive rules for choice symbol
-       if (sym->rev_dep.expr != NULL) {
-           Dprintf(" Dependency:\n");
-           doutput_expr(sym->rev_dep.expr);
-           el->rev_dep =
-               boolexpr_kconfig(gsymlist, sym->rev_dep.expr, true, NULL);
-       } else
-           el->rev_dep = boolexpr_true();
-       for_all_choices(sym, prop) {
-           struct symbol *symw;
-           struct expr *exprw;
-           unsigned *symx = NULL;
-           size_t symx_size = 0;
-           int x, y;
-           expr_list_for_each_sym(prop->expr, exprw, symw) {
-               symx_size++;
-               symx = realloc(symx, symx_size * sizeof(unsigned));
-               symx[symx_size - 1] = symlist_id(gsymlist, symw->name);
-               output_rules_symbol(symx[symx_size - 1]);
-           }
-           output_rules_symbol(-(int)
-                               el_id);
-           output_rules_endterm();
-           for (x = 0; x < symx_size - 1; x++) {
-               for (y = x + 1; y < symx_size; y++) {
-                   output_rules_symbol(-(int)
-                                       symx[x]);
-                   output_rules_symbol(-(int)
-                                       symx[y]);
-                   output_rules_endterm();
-               }
-           }
-           free(symx);
-           symx = NULL;
-       }
-       if (el->rev_dep->type != BT_FALSE && el->rev_dep->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->rev_dep);
-       if (el->vis->type != BT_FALSE && el->vis->type != BT_TRUE)
-           cnf_boolexpr(gsymlist, el->vis);
-       // (!sym || rev_dep) && (!sym || !rev_dep || vis)
-       // For nonoptional per list symbol add:
-       // (sym || !rev_dep || !vis || !dir_dep_of_list))
-       if (el->rev_dep->type != BT_TRUE) {
-           output_rules_symbol(-1 * boolsym->id);
-           if (el->rev_dep->type != BT_FALSE) {
-               output_rules_symbol(el->rev_dep->id);
-           }
-           output_rules_endterm();
-       }
-       if (el->rev_dep->type != BT_FALSE && el->vis->type != BT_TRUE) {
-           output_rules_symbol(-1 * boolsym->id);
-           if (el->rev_dep->type != BT_TRUE) {
-               output_rules_symbol(-1 * el->rev_dep->id);
-           }
-           if (el->vis != BT_FALSE) {
-               output_rules_symbol(el->vis->id);
-           }
-           output_rules_endterm();
-       }
-       if (!sym_is_optional(sym)) {
-           for_all_choices(sym, prop) {
-               struct symbol *symw;
-               struct expr *exprw;
-               expr_list_for_each_sym(prop->expr, exprw, symw) {
-                   struct boolexpr *wdep;
-                   if (symw->dir_dep.expr != NULL) {
-                       struct symbol *settrue[] = {sym, NULL};
-                       wdep =
-                           boolexpr_kconfig(gsymlist, symw->dir_dep.expr,
-                                            false, settrue);
-                   } else
-                       wdep = boolexpr_true();
-                   cnf_boolexpr(gsymlist, wdep);
-                   if (el->rev_dep->type != BT_FALSE
-                       && el->vis->type != BT_FALSE
-                       && wdep->type != BT_FALSE) {
-                       output_rules_symbol(boolsym->id);
-                       if (el->rev_dep->type != BT_TRUE) {
-                           output_rules_symbol(-1 * el->rev_dep->id);
-                       }
-                       if (el->vis->type != BT_TRUE) {
-                           output_rules_symbol(-1 * el->vis->id);
-                       }
-                       if (wdep->type != BT_TRUE
-                           && wdep->id != boolsym->id) {
-                           output_rules_symbol(-1 * wdep->id);
-                       }
-                       output_rules_endterm();
-                   }
-               }
-           }
-       }
-    }
+       return EXIT_SUCCESS;
 }
-
-#endif