#include <vector>
#include <map>
+#include <memory>
using namespace std;
OPT__START = 256,
OPT_BASECONFIG,
OPT_CNF,
+ OPT_DOT,
OPT_DUMP,
OPT_ENV,
OPT_HELP,
);
}
-char *expr_to_string(struct expr *e);
+typedef unique_ptr<char> upchar;
-char *sym_to_string(struct symbol *sym)
+upchar expr_to_string(struct expr *e);
+
+upchar 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;
+ asprintf(&ret, "NONAME%d", sym->lcp.id);
+ return upchar(ret);
}
-char *expr_binop_to_string(struct expr *e, const char *op_str)
+upchar 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);
+ upchar l = expr_to_string(e->left.expr);
+ upchar r = expr_to_string(e->right.expr);
char *ret;
- asprintf(&ret, "(%s %s %s)", l, op_str, r);
- free(l);
- free(r);
- return ret;
+ asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
+ return upchar(ret);
}
-char *expr_comp_to_string(struct expr *e, const char *op_str)
+upchar 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);
+ upchar l = sym_to_string(e->left.sym);
+ upchar r = sym_to_string(e->right.sym);
char *ret;
- asprintf(&ret, "(%s %s %s)", l, op_str, r);
- free(l);
- free(r);
- return ret;
+ asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
+ return upchar(ret);
}
-char *expr_to_string(struct expr *e)
+upchar 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;
+ return upchar(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;
+ asprintf(&ret, "!%s", expr_to_string(e->left.expr).get());
+ break;
case E_EQUAL:
return expr_comp_to_string(e, "==");
case E_UNEQUAL:
break;
}
- return ret;
+ return upchar(ret);
}
void dump_symbol(struct symbol *sym)
{
struct property *prop;
- const char *name = sym_to_string(sym);
+ upchar 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 = '.';
prompt = prop->text;
}
- printf("%-40s %c %-8s %-50s %s\n", name, val, type, flags, prompt);
+ printf("%-40s %c %-8s %-50s %s\n", name.get(), 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);
- }
+ if (sym->dir_dep.expr)
+ printf(" depends %s\n", expr_to_string(sym->dir_dep.expr).get());
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);
-
+ printf(" selects %s if %s\n", prop->expr->left.sym->name,
+ expr_to_string(prop->visible.expr).get());
}
}
}
char *p = line;
lineno++;
+ if (line[0] == '#')
+ continue;
if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
p += strlen(CONFIG_);
const char *sym_name = strtok(p, " =\n");
struct symbol *sym = sym_find(sym_name);
if (!sym) {
- fprintf(stderr, "%s:%d: Invalid symbol: %s\n", varfile, lineno, sym_name);
- exit(EXIT_FAILURE);
- }
- if (!(sym->flags & SYMBOL_WRITE)) {
- fprintf(stderr, "%s:%d: Symbol %s not visible\n", varfile, lineno, sym_name);
+ fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", varfile, lineno, sym_name);
exit(EXIT_FAILURE);
}
+// if (!(sym->flags & SYMBOL_WRITE)) {
+// fprintf(stderr, "%s:%d: Error: Symbol %s not visible\n", varfile, lineno, sym_name);
+// exit(EXIT_FAILURE);
+// }
if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
- fprintf(stderr, "%s:%d: Choice values not yet supported: %s", varfile, lineno, sym_name);
+ fprintf(stderr, "%s:%d: Error: Choice values not yet supported: %s", varfile, lineno, sym_name);
exit(EXIT_FAILURE);
}
struct property *prop;
fclose(f);
}
+void set_all_symbols_variable()
+{
+ int i;
+ struct symbol *sym;
+
+ for_all_symbols(i, sym) {
+ if (!(sym->flags & (SYMBOL_CONST | SYMBOL_AUTO)))
+ sym->lcp.variable = 1;
+ }
+}
+
struct SatLiteral {
struct symbol *sym;
struct expr *expr;
-
- SatLiteral(struct symbol *s) : sym(s), expr(nullptr) {}
- SatLiteral(struct expr *e) : sym(nullptr), expr(e) {}
+ int dot_printed:1;
+
+ SatLiteral(struct symbol *s) : sym(s), expr(nullptr) { assert(sym->lcp.variable && sym->lcp.id); }
+ SatLiteral(struct expr *e) : sym(nullptr), expr(e) { assert(expr->lcp.variable && expr->lcp.id); }
+ sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; }
+ upchar name() const {
+ char *ret;
+ if (sym) {
+ assert(sym->name); // TODO
+ asprintf(&ret, "%s", sym->name);
+ } else if (expr) {
+ asprintf(&ret, "expr%d", expr->lcp.id);
+ }
+ return upchar(ret);
+ }
};
typedef vector<sat_id> SatClause;
+struct Implication: public SatClause {
+ Implication(sat_id a, sat_id b) : SatClause{-a, b} {}
+};
+
struct SatExpr {
sat_id left, right;
enum expr_type op;
- SatExpr(int l, enum expr_type o, int r)
+ SatExpr(sat_id l, enum expr_type o, sat_id r)
: left(l), right(r), op(o) {}
+ //SatExpr(enum expr_type o) : left(0), right(0), op(o) { assert(o == E_NONE); }
bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
};
-class SatLiterals : public vector<struct SatLiteral>
+class SatLiterals : protected vector<struct SatLiteral>
{
public:
- int fixed = {0};
- SatLiterals() { push_back(SatLiteral((struct symbol*)nullptr)); reserve(20000); }
- int count() const { return size() - 1; }
+ using vector<struct SatLiteral>::begin;
+ using vector<struct SatLiteral>::end;
+ using vector<struct SatLiteral>::push_back;
+ SatLiterals() { reserve(20000); }
+ int count() const { return size(); }
+ const SatLiteral &operator[](size_type i) const { return at(i-1); }
+ const SatLiteral &last() const { return *(--end()); }
+ bool test_set_dot_printed(struct symbol *sym) const {
+ auto l = (*this)[sym->lcp.id];
+ bool ret = l.dot_printed;
+ l.dot_printed = 1;
+ return ret;
+ }
+ bool test_set_dot_printed(struct expr *e) const {
+ auto l = (*this)[e->lcp.id];
+ bool ret = l.dot_printed;
+ l.dot_printed = 1;
+ return ret;
+ }
};
-
/*
* bool FOO!=n => FOO
* bool FOO!=y => !FOO
return e;
}
+bool mark_variable_expressions(struct expr *e)
+{
+ if (!e)
+ return false;
+
+ switch (e->type) {
+ case E_SYMBOL:
+ return (e->lcp.variable = e->left.sym->lcp.variable);
+ case E_NONE:
+ fprintf(stderr, "NONE not implemented\n");
+ exit(EXIT_FAILURE);
+ break;
+ case E_NOT:
+ if (mark_variable_expressions(e->left.expr))
+ return (e->lcp.variable = 1);
+ else
+ return false;
+ case E_OR:
+ case E_AND: {
+ mark_variable_expressions(e->left.expr);
+ mark_variable_expressions(e->right.expr);
+
+ if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
+ return (e->lcp.variable = 1);
+ } else if (!e->left.expr->lcp.variable && !e->right.expr->lcp.variable) {
+ return (e->lcp.variable = 0);
+ } else {
+ tristate val;
+
+ if (e->left.expr->lcp.variable) {
+ val = expr_calc_value(e->right.expr);
+ } else if (e->right.expr->lcp.variable) {
+ val = expr_calc_value(e->left.expr);
+ }
+ if ((e->type == E_OR && val == yes) ||
+ (e->type == E_AND && val == no))
+ return (e->lcp.variable = 0);
+ else
+ return (e->lcp.variable = 1);
+ }
+ __builtin_unreachable();
+ }
+ case E_EQUAL:
+ case E_UNEQUAL:
+ if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
+ return (e->lcp.variable = 1);
+ } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
+ fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
+ exit(EXIT_FAILURE);
+ } else
+ return false;
+ case E_LTH:
+ case E_LEQ:
+ case E_GTH:
+ case E_GEQ:
+ if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
+ fprintf(stderr, "Comparison of variable symbols not implemented\n");
+ exit(EXIT_FAILURE);
+ } else
+ return false;
+ 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;
+ }
+ fprintf(stderr, "Unexpected situation in mark_variable_expressions\n");
+ exit(EXIT_FAILURE);
+}
+
+void mark_variable_expressions()
+{
+ int i;
+ struct symbol *sym;
+ struct property *prop;
+
+ for_all_symbols(i, sym) {
+ mark_variable_expressions(sym->dir_dep.expr);
+ mark_variable_expressions(sym->rev_dep.expr);
+ for_all_properties(sym, prop, P_SELECT) {
+ assert(prop->expr->type == E_SYMBOL);
+ mark_variable_expressions(prop->visible.expr);
+ }
+ }
+}
+
+void check_dep_consistency()
+{
+ int i;
+ struct symbol *sym;
+ tristate val;
+
+ for_all_symbols(i, sym) {
+ if (sym->lcp.variable && sym->dir_dep.expr && !sym->dir_dep.expr->lcp.variable) {
+ val = expr_calc_value(sym->dir_dep.expr);
+ if (val == no) {
+ fprintf(stderr, "Symbol %s cannot be variable because its dependency is always 'no': %s\n",
+ sym->name, expr_to_string(sym->dir_dep.expr).get());
+ exit(EXIT_FAILURE);
+ }
+ }
+ if (sym->lcp.variable && sym->rev_dep.expr && !sym->rev_dep.expr->lcp.variable) {
+ val = expr_calc_value(sym->rev_dep.expr);
+ if (val == yes) {
+ fprintf(stderr, "Symbol %s cannot be variable because it is selected by expression that is always 'yes': %s\n",
+ sym->name, expr_to_string(sym->rev_dep.expr).get());
+ exit(EXIT_FAILURE);
+ }
+ }
+ if (!sym->lcp.variable && (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) &&
+ sym->curr.tri == no && sym->rev_dep.expr && sym->rev_dep.expr->lcp.variable) {
+ fprintf(stderr, "Symbol %s cannot be fixed to 'no', because it is selcted by variable expression '%s'\n",
+ sym->name, expr_to_string(sym->rev_dep.expr).get());
+ exit(EXIT_FAILURE);
+ }
+ }
+}
+
+
+class DotWriter {
+ FILE *f;
+public:
+ DotWriter(const char *file_name) {
+ f = fopen(file_name, "w");
+
+ if (!f) {
+ perror(file_name);
+ exit(EXIT_FAILURE);
+ }
+
+ fprintf(f, "digraph conf {\n");
+ //fprintf(f, "rankdir=LR;\n");
+ }
+ ~DotWriter() {
+ fprintf(f, "}\n");
+ fclose(f);
+ }
+ void symbol(struct symbol *sym) {
+// if (sym->lcp.dot_printed)
+// return;
+// sym->lcp.dot_printed = 1;
+
+ const char *opts = "";
+ if (sym->lcp.variable)
+ opts = " [penwidth=3]";
+ else
+ opts = " [color=gray]";
+ fprintf(f, "\"%s\"%s;\n", sym->name, opts);
+ }
+ void expr(const SatLiteral &l) {
+ assert(l.expr);
+ const char *label = "???";
+// if (sym->lcp.dot_printed)
+// return;
+// sym->lcp.dot_printed = 1;
+ switch (l.expr->type) {
+ case E_OR: label = "|"; break;
+ case E_AND: label = "&"; break;
+ case E_EQUAL: label = "="; break;
+ case E_UNEQUAL: label = "!="; break;
+ case E_NOT: label = "!"; break;
+ case E_SYMBOL:
+ case E_NONE:
+ case E_RANGE:
+ case E_LTH:
+ case E_LEQ:
+ case E_GTH:
+ case E_GEQ:
+ case E_LIST:
+ default:
+ fprintf(stderr, "Expr %d not implemented\n", l.expr->type);
+ exit(EXIT_FAILURE);
+ break;
+ }
+
+ fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", l.name().get(), label);
+ }
+ void depends_on(const SatLiteral &l1, const SatLiteral &l2) {
+ fprintf(f, "\"%s\" -> \"%s\" [style=bold,label=d];\n", l1.name().get(), l2.name().get());
+ }
+ void selects(const SatLiteral &l1, const SatLiteral &l2) {
+ fprintf(f, "\"%s\" -> \"%s\" [style=bold,arrowhead=open,label=s];\n", l1.name().get(), l2.name().get());
+ }
+ void edge(const SatLiteral &from, const SatLiteral &to) {
+ fprintf(f, "\"%s\" -> \"%s\" [arrowhead=empty];\n", from.name().get(), to.name().get());
+ }
+};
class SatData {
SatLiterals literals = {};
vector<SatClause> clauses = {};
map<SatExpr, sat_id> expressions = {};
-
- void expr2literal(struct expr *e);
-
+ DotWriter *dot = nullptr;
public:
- SatData() {
+ SatData(const char *dot_fn) {
+ if (dot_fn)
+ dot = new DotWriter(dot_fn);
symbols2literals();
expressions2literals();
expressions2clauses();
+ if (dot)
+ delete dot;
+
+ }
+
+ const SatLiteral &add_literal(struct symbol *sym) {
+ sym->lcp.id = literals.count() + 1;
+ literals.push_back(SatLiteral(sym));
+ if (dot)
+ dot->symbol(sym);
+ return literals.last();
+ }
+
+ const SatLiteral &add_literal(struct expr *e) {
+ e->lcp.id = literals.count() + 1;
+ literals.push_back(SatLiteral(e));
+ if (dot)
+ dot->expr(literals.last());
+ return literals.last();
}
void symbols2literals() {
struct symbol *sym;
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->lcp.variable)
+ add_literal(sym);
+ }
+ }
+
+ // Assign e->lcp.id to variable literals
+ sat_id expr2literal(struct expr *e) {
+ if (!e || !e->lcp.variable)
+ return 0;
+ if (e->lcp.id)
+ return e->lcp.id;
+
+ switch (e->type) {
+ case E_SYMBOL:
+ assert(e->left.sym->lcp.id);
+ 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()) {
+ auto l = add_literal(e);
+ expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
+ if (dot)
+ dot->edge(literals[e->left.expr->lcp.id], l);
+ } else
+ e->lcp.id = it->second;
+ break;
+ }
+ case E_OR:
+ case E_AND: {
+ expr2literal(e->left.expr);
+ expr2literal(e->right.expr);
+
+ if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
+ SatExpr se = SatExpr(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id);
+ auto it = expressions.find(se);
+ if (it == expressions.end()) {
+ auto l = add_literal(e);
+ expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
+ if (dot) {
+ dot->edge(literals[e->left.expr->lcp.id], l);
+ dot->edge(literals[e->right.expr->lcp.id], l);
+ }
+ } else
+ e->lcp.id = it->second;
+ } else {
+ if (e->left.expr->lcp.variable) {
+ e->lcp.id = e->left.expr->lcp.id;
+ } else if (e->right.expr->lcp.variable) {
+ e->lcp.id = e->right.expr->lcp.id;
+ }
}
+ break;
+ }
+ case E_EQUAL:
+ case E_UNEQUAL: {
+ if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
+ SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id);
+ auto it = expressions.find(se);
+ if (it == expressions.end()) {
+ auto l = add_literal(e);
+ expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
+ if (dot) {
+ dot->edge(literals[e->left.sym->lcp.id], l);
+ dot->edge(literals[e->right.sym->lcp.id], l);
+ }
+ } else
+ e->lcp.id = it->second;
+ } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
+ fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
+ exit(EXIT_FAILURE);
+ }
+ break;
+ }
+ case E_LTH:
+ case E_LEQ:
+ case E_GTH:
+ case E_GEQ:
+ if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
+ fprintf(stderr, "Comparison of variable symbols 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;
}
+ assert(e->lcp.id);
+ return e->lcp.id;
}
void expressions2literals() {
int i;
struct symbol *sym;
- struct property *prop;
+ struct expr *e;
+ sat_id id;
+ const SatLiteral *syml;
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);
+ if (sym->lcp.variable &&
+ (sym->type == S_BOOLEAN || sym->type == S_TRISTATE)) {
+ syml = &literals[sym->lcp.id];
+ // Direct dependencies
+ //sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
+ e = sym->dir_dep.expr;
+ id = expr2literal(e);
+ if (id) {
+ clauses.push_back(Implication(sym->lcp.id, id));
+ if (dot)
+ dot->depends_on(*syml, literals[id]);
+ }
+
+ // Reverse dependecies
+ e = sym->rev_dep.expr;
+ id = expr2literal(e);
+ if (id) {
+ clauses.push_back(Implication(id, sym->lcp.id));
+ if (dot)
+ dot->selects(literals[id], *syml);
}
}
}
}
+ // Tseitin Transformation - see
+ // https://en.wikipedia.org/wiki/Tseitin_transformation or
+ // http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
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)) {
+ upchar 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:
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;
+ upchar 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:
}
void write_dimacs_cnf(const char *cnf) {
- int i;
FILE *f = fopen(cnf, "w");
if (!f) {
exit(EXIT_FAILURE);
}
- fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size() + literals.fixed);
+ fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size());
- 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->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 l: literals) {
+ if (l.sym)
+ fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+ if (l.expr)
+ fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
}
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<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;
- }
-}
+// void print_dot_oper(FILE *f, struct expr *e, const char *parent, const char *label) {
+// char *expr_name;
+// asprintf(&expr_name, "expr%d", e->lcp.id);
+// fprintf(f, "\"%s\" -> \"%s\";\n", parent, expr_name);
+
+// fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", expr_name, label);
+// print_dot_expr(f, e->left.expr, expr_name, "l", "");
+// print_dot_expr(f, e->right.expr, expr_name, "r", "");
+// free(expr_name);
+// }
+
+// void print_dot_expr(FILE *f, struct expr *e, const char *parent,
+// const char *suffix, const char *edge_opts) {
+// if (e->lcp.dot_printed ||
+// !e->lcp.variable)
+// return;
+// e->lcp.dot_printed = 1;
+// if (e) {
+// switch (e->type) {
+// case E_NONE:
+// break;
+// case E_OR:
+// print_dot_oper(f, e, parent, "|");
+// break;
+// case E_AND:
+// print_dot_oper(f, e, parent, "&");
+// break;
+// case E_NOT:
+// print_dot_expr(f, e->left.expr, parent, suffix, "arrowhead=odot");
+// break;
+// case E_EQUAL:
+// print_dot_oper(f, e, parent, "=");
+// break;
+// case E_UNEQUAL:
+// print_dot_oper(f, e, parent, "!=");
+// break;
+// case E_LIST:
+// fprintf(stderr, "LIST not implemented\n");
+// exit(EXIT_FAILURE);
+// break;
+// case E_SYMBOL: {
+// if (e->left.sym->name) {
+// fprintf(f, "\"%s\" -> \"%s\" [%s];\n", parent, e->left.sym->name, edge_opts);
+// print_dot_symbol(f, e->left.sym);
+// }
+// break;
+// }
+// case E_RANGE:
+// fprintf(stderr, "RANGE not implemented\n");
+// exit(EXIT_FAILURE);
+// break;
+// case E_LTH:
+// case E_LEQ:
+// case E_GTH:
+// case E_GEQ:
+// break;
+// }
+// }
+// }
+
+// void print_dot_symbol(FILE *f, struct symbol *sym) {
+// if (!sym->lcp.variable ||
+// sym->lcp.dot_printed)
+// return;
+// sym->lcp.dot_printed = 1;
+
+// const char *opts = "";
+// if (sym->lcp.variable)
+// opts = " [penwidth=3]";
+// else
+// opts = " [color=gray]";
+// fprintf(f, "\"%s\"%s;\n", sym->name, opts);
+// if (sym->dir_dep.expr)
+// print_dot_expr(f, sym->dir_dep.expr, sym->name, "", "");
+
+// struct property *prop;
+// for_all_properties(sym, prop, P_SELECT) {
+// assert(prop->expr->type == E_SYMBOL);
+// print_dot_expr(f, prop->expr, sym->name, "", "label=\"selects\"");
+// if (prop->visible.expr && prop->visible.expr->lcp.variable) {
+// printf("Not implemented %s\n", expr_to_string(prop->visible.expr).get());
+// }
+// }
+// }
+
+
+// void write_dot(const char *dot) {
+// int i;
+// FILE *f = fopen(dot, "w");
+
+// if (!f) {
+// perror(dot);
+// exit(EXIT_FAILURE);
+// }
+
+// fprintf(f, "digraph conf {\n");
+
+// struct symbol *sym;
+// for_all_symbols(i, sym)
+// print_dot_symbol(f, sym);
+// fprintf(f, "}\n");
+// fclose(f);
+// }
+};
int main(int argc, char **argv)
{
char *baseconf = NULL;
char *cnf = NULL;
+ char *dot = NULL;
char *kconfig = NULL;
char *varfile = NULL;
int dump = false;
static struct option long_options[] = {
{"baseconf", required_argument, 0, OPT_BASECONFIG },
{"cnf", required_argument, 0, OPT_CNF },
+ {"dot", required_argument, 0, OPT_DOT },
{"env", required_argument, 0, OPT_ENV },
{"dump", no_argument, &dump, true },
{"help", no_argument, 0, OPT_HELP },
case OPT_CNF:
cnf = optarg;
break;
+ case OPT_DOT:
+ dot = optarg;
+ break;
case OPT_ENV:
set_missing_env(optarg);
break;
if (baseconf)
conf_read(baseconf);
- SatData sat_data;
-
if (varfile)
read_varfile(varfile);
+ else
+ set_all_symbols_variable();
+
+ mark_variable_expressions();
+ check_dep_consistency();
+
+ SatData sat_data(dot);
if (dump)
do_dump();
- if (cnf) {
+ if (cnf)
sat_data.write_dimacs_cnf(cnf);
- }
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
projects / linux-conf-perf.git / blobdiff