#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 {
);
}
+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 = '.';
}
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()
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;
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