From 9bd7315c4fbe7556d899d63630e9eca9c6005399 Mon Sep 17 00:00:00 2001 From: Michal Sojka Date: Tue, 20 Oct 2015 11:50:35 +0200 Subject: [PATCH] kconfig2sat: More work --- kconfig2sat/kconfig2sat.cc | 485 +++++++++---------------------------- kconfig2sat/lcp_data.h | 4 +- 2 files changed, 123 insertions(+), 366 deletions(-) diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc index 1f4ea0d..356de0f 100644 --- a/kconfig2sat/kconfig2sat.cc +++ b/kconfig2sat/kconfig2sat.cc @@ -13,6 +13,7 @@ #include #include +#include using namespace std; @@ -56,7 +57,7 @@ char *sym_to_string(struct symbol *sym) if (sym->name) asprintf(&ret, sym->name); else - asprintf(&ret, "NONAME%d", sym->lcp.sat_id); + asprintf(&ret, "NONAME%d", sym->lcp.id); return ret; } @@ -255,6 +256,9 @@ struct SatLiteral { 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 SatClause; @@ -338,28 +342,106 @@ class SatData { vector clauses = {}; map expressions = {}; - void expr2literal(struct expr *e); - 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) { - literals.push_back(SatLiteral(sym)); - sym->lcp.sat_id = literals.count(); + 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(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(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(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; @@ -367,6 +449,10 @@ public: 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); @@ -379,12 +465,24 @@ public: } } + 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 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: @@ -411,12 +509,21 @@ public: 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: { - fprintf(stderr, "Comparison operators not implemented\n"); + struct expr *e = literals[e_id].expr; + unique_ptr 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: @@ -433,7 +540,6 @@ public: } void write_dimacs_cnf(const char *cnf) { - int i; FILE *f = fopen(cnf, "w"); if (!f) { @@ -443,100 +549,28 @@ public: fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed); - for (i = 1; i <= literals.count(); i++) { - SatLiteral &l = literals[i]; + for (auto l: literals) { if (l.sym) { - fprintf(f, "c SYM %d %s\n", l.sym->lcp.sat_id, l.sym->name); - if (l.sym->flags & SYMBOL_VALID && !l.sym->lcp.variable) - fprintf(f, "%d 0\n", l.sym->curr.tri != no ? l.sym->lcp.sat_id : -l.sym->lcp.sat_id); + 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.sat_id, tmp); + fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, tmp); free(tmp); } } for (auto clause: clauses) { - for (sat_id id: clause) + for (sat_id id: clause) { + assert(id != 0); fprintf(f, "%d ", id); + } fprintf(f, "0\n"); } fclose(f); } }; -void none(struct expr *e) -{ -} - -void SatData::expr2literal(struct expr *e) -{ - if (!e || e->lcp.sat_id) - return; - - switch (e->type) { - case E_SYMBOL: - e->lcp.sat_id = e->left.sym->lcp.sat_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.sat_id, e->type, 0); - auto it = expressions.find(se); - if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.sat_id = literals.count(); - } else - e->lcp.sat_id = it->second; - break; - } - case E_OR: - case E_AND: { - expr2literal(e->left.expr); - expr2literal(e->right.expr); - - SatExpr se(e->left.expr->lcp.sat_id, e->type, e->right.expr->lcp.sat_id); - auto it = expressions.find(se); - if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.sat_id = literals.count(); - } else - e->lcp.sat_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.sat_id, e->type, e->right.sym->lcp.sat_id); - auto it = expressions.find(se); - if (it == expressions.end()) { - literals.push_back(SatLiteral(e)); - expressions.insert(pair(se, literals.count())); - e->lcp.sat_id = literals.count(); - } else - e->lcp.sat_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; - } -} - int main(int argc, char **argv) { int c; @@ -637,280 +671,3 @@ int main(int argc, char **argv) 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(); - } - - 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(); - } - } - } - } - } -} - -#endif diff --git a/kconfig2sat/lcp_data.h b/kconfig2sat/lcp_data.h index eba47ab..4953b3f 100644 --- a/kconfig2sat/lcp_data.h +++ b/kconfig2sat/lcp_data.h @@ -8,12 +8,12 @@ typedef int sat_id; /* Id of corresponding SAT literal */ struct lcp_symbol { - sat_id sat_id; + sat_id id; int variable:1; /* SAT literal is variable (i.e. not fixed) */ }; struct lcp_expr { - sat_id sat_id; + sat_id id; }; -- 2.39.2