#include <libintl.h>
#include <unistd.h>
#include <getopt.h>
+#include <inttypes.h>
#include "kconfig/lkc.h"
#include "lcp_utils.h"
#include <vector>
+#include <map>
using namespace std;
);
}
+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.sat_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;
+ sym->lcp.variable = 1;
}
fclose(f);
}
-void write_dimacs_cnf(const char *cnf)
-{
- FILE *f = fopen(cnf, "w");
-
- if (!f) {
- perror(cnf);
- exit(EXIT_FAILURE);
- }
-
- fclose(f);
-}
-
struct SatLiteral {
struct symbol *sym;
struct expr *expr;
SatLiteral(struct expr *e) : sym(nullptr), expr(e) {}
};
-struct SatClause {
- // TODO
+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>
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 = {};
+
+ void expr2literal(struct expr *e);
+
public:
SatData() {
+ symbols2literals();
+ expressions2literals();
+ expressions2clauses();
+ }
+
+ void symbols2literals() {
int i;
struct symbol *sym;
for_all_symbols(i, sym) {
if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
literals.push_back(SatLiteral(sym));
- sym->lcp = new lcp_symbol;
- memset(sym->lcp, 0, sizeof(*sym->lcp));
- sym->lcp->sat_id = literals.count();
+ sym->lcp.sat_id = literals.count();
}
}
}
+ void expressions2literals() {
+ int i;
+ struct symbol *sym;
+ struct property *prop;
+
+ for_all_symbols(i, sym) {
+ if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
+ 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 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;
+ 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:
+ case E_LTH:
+ case E_LEQ:
+ case E_GTH:
+ case E_GEQ: {
+ fprintf(stderr, "Comparison operators not implemented\n");
+ //exit(EXIT_FAILURE);
+ 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) {
int i;
FILE *f = fopen(cnf, "w");
for (i = 1; i <= literals.count(); i++) {
SatLiteral &l = literals[i];
- if (l.sym)
- fprintf(f, "c SYM %d %s\n", l.sym->lcp->sat_id, l.sym->name);
- if (l.sym && 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);
+ 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);
+ }
+ if (l.expr) {
+ char *tmp = expr_to_string(l.expr);
+ fprintf(f, "c EXPR %d %s\n", l.expr->lcp.sat_id, tmp);
+ free(tmp);
+ }
+ }
+ for (auto clause: clauses) {
+ for (sat_id id: clause)
+ 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<SatExpr, sat_id>(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<SatExpr, sat_id>(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<SatExpr, sat_id>(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)
{
textdomain(PACKAGE);
conf_parse_path(kconfig);
- SatData sat_data;
-
if (baseconf)
conf_read(baseconf);
+ SatData sat_data;
+
if (varfile)
read_varfile(varfile);
if (dump)
do_dump();
-
if (cnf) {
sat_data.write_dimacs_cnf(cnf);
}
projects / linux-conf-perf.git / blobdiff