#include <vector>
#include <map>
#include <memory>
+#include <deque>
using namespace std;
}
}
+void mark_symbol_variable(const char *sym_name, const char *file, int lineno)
+{
+ struct symbol *sym = sym_find(sym_name);
+ if (!sym) {
+ fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", file, 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: Error: Choice values not yet supported: %s", file, lineno, sym_name);
+ exit(EXIT_FAILURE);
+ }
+ struct property *prop;
+ const char *prompt = NULL;
+ for_all_properties(sym, prop, P_PROMPT) {
+ prompt = prop->text;
+ }
+ if (!prompt) {
+ fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", file, lineno, sym_name);
+ }
+ sym->lcp.variable = 1;
+}
+
void read_varfile(const char *varfile)
{
FILE *f = fopen(varfile, "r");
p += strlen(CONFIG_);
const char *sym_name = strtok(p, " =\n");
- struct symbol *sym = sym_find(sym_name);
- if (!sym) {
- 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: Error: Choice values not yet supported: %s", varfile, lineno, sym_name);
- exit(EXIT_FAILURE);
- }
- struct property *prop;
- const char *prompt = NULL;
- for_all_properties(sym, prop, P_PROMPT) {
- prompt = prop->text;
- }
- if (!prompt) {
- fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", varfile, lineno, sym_name);
- }
- sym->lcp.variable = 1;
+ mark_symbol_variable(sym_name, varfile, lineno);
}
fclose(f);
}
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 : protected vector<struct SatLiteral>
{
+ unsigned _symbols = 0;
public:
using vector<struct SatLiteral>::begin;
using vector<struct SatLiteral>::end;
- using vector<struct SatLiteral>::push_back;
+
SatLiterals() { reserve(20000); }
+ SatLiteral &add(struct symbol *sym) {
+ sym->lcp.id = count() + 1;
+ push_back(SatLiteral(sym));
+ _symbols++;
+ return last();
+ }
+ SatLiteral &add(struct expr *e) {
+ e->lcp.id = count() + 1;
+ push_back(SatLiteral(e));
+ return last();
+ }
int count() const { return size(); }
+ int symbols() const { return _symbols; }
const SatLiteral &operator[](size_type i) const { return at(i-1); }
- const SatLiteral &last() const { return *(--end()); }
+ SatLiteral &last() { return *(--end()); }
bool test_set_dot_printed(struct symbol *sym) const {
auto l = (*this)[sym->lcp.id];
bool ret = l.dot_printed;
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]";
opts = " [color=gray]";
fprintf(f, "\"%s\"%s;\n", sym->name, opts);
}
- void expr(const SatLiteral &l) {
- assert(l.expr);
+ void expr(struct expr *e, upchar name) {
const char *label = "???";
-// if (sym->lcp.dot_printed)
-// return;
-// sym->lcp.dot_printed = 1;
- switch (l.expr->type) {
+ switch (e->type) {
case E_OR: label = "|"; break;
case E_AND: label = "&"; break;
case E_EQUAL: label = "="; break;
case E_GEQ:
case E_LIST:
default:
- fprintf(stderr, "Expr %d not implemented\n", l.expr->type);
+ fprintf(stderr, "Expr %d not implemented\n", e->type);
exit(EXIT_FAILURE);
break;
}
- fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", l.name().get(), label);
+ fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", name.get(), label);
+ }
+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 literal(SatLiteral &l) {
+ if (l.dot_printed)
+ return;
+ l.dot_printed = 1;
+ if (l.sym)
+ symbol(l.sym);
+ if (l.expr)
+ expr(l.expr, l.name());
}
void depends_on(const SatLiteral &l1, const SatLiteral &l2) {
fprintf(f, "\"%s\" -> \"%s\" [style=bold,label=d];\n", l1.name().get(), l2.name().get());
}
const SatLiteral &add_literal(struct symbol *sym) {
- sym->lcp.id = literals.count() + 1;
- literals.push_back(SatLiteral(sym));
+ SatLiteral &l = literals.add(sym);
if (dot)
- dot->symbol(sym);
- return literals.last();
+ dot->literal(l);
+ return l;
}
const SatLiteral &add_literal(struct expr *e) {
- e->lcp.id = literals.count() + 1;
- literals.push_back(SatLiteral(e));
+ SatLiteral &l = literals.add(e);
if (dot)
- dot->expr(literals.last());
- return literals.last();
+ dot->literal(l);
+ return l;
}
void symbols2literals() {
for (auto l: literals) {
if (l.sym)
- fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
+ fprintf(f, "c SYM %d %s\n", l.id(), l.sym->name);
if (l.expr)
- fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
+ fprintf(f, "c EXPR %d %s\n", l.id(), expr_to_string(l.expr).get());
+ }
+ for (auto clause: clauses) {
+ for (sat_id id: clause) {
+ assert(id != 0);
+ fprintf(f, "%d ", id);
+ }
+ fprintf(f, "0\n");
+ }
+ fclose(f);
+ }
+ void write_dimacs_cnf_single(const char *cnf, const char *sym_name) {
+ FILE *f = fopen((string(cnf)+"-single-"+sym_name).c_str(), "w");
+
+ if (!f) {
+ perror(cnf);
+ exit(EXIT_FAILURE);
+ }
+
+ fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.symbols());
+
+ for (auto l: literals) {
+ if (l.sym)
+ fprintf(f, "c SYM %d,%d %s\n", l.id(), l.id() + literals.count(), l.sym->name);
+ if (l.expr) {
+ struct gstr gs = str_new();
+ expr_gstr_print(l.expr, &gs);
+ fprintf(f, "c EXPR %d,%d %s\n", l.id(), l.id() + literals.count(), str_get(&gs));
+ }
}
for (auto clause: clauses) {
for (sat_id id: clause) {
fprintf(f, "%d ", id);
}
fprintf(f, "0\n");
+
+ for (sat_id id: clause) {
+ fprintf(f, "%d ", id > 0 ? id + literals.count() : id - literals.count());
+ }
+ fprintf(f, "0\n");
+ }
+ fprintf(f, "c Equivalence\n");
+ for (auto l: literals) {
+ if (!l.sym)
+ continue;
+ if (strcmp(sym_name, l.sym->name) != 0) {
+ fprintf(f, "%d %d 0\n", -l.id(), l.id() + literals.count());
+ fprintf(f, "%d %d 0\n", -l.id() - literals.count(), l.id());
+ } else {
+ fprintf(f, "%d 0\n", +l.id());
+ fprintf(f, "%d 0\n", -l.id() - literals.count());
+ }
}
fclose(f);
}
-// 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);
-// }
+ void write_dimacs_cnf_all_single(const char *cnf) {
+ for (auto l: literals)
+ if (l.sym)
+ write_dimacs_cnf_single(cnf, l.sym->name);
+ }
};
int main(int argc, char **argv)
char *kconfig = NULL;
char *varfile = NULL;
int dump = false;
+ deque<string> varopts;
while (1) {
int option_index = 0;
{"help", no_argument, 0, OPT_HELP },
{"kconfig", required_argument, 0, OPT_KCONFIG },
{"varfile", required_argument, 0, OPT_VARFILE },
-// {"varopt", required_argument, 0, OPT_VAROPTION },
+ {"varopt", required_argument, 0, OPT_VAROPTION },
{"verbose", no_argument, 0, OPT_VERBOSE },
{0, 0, 0, 0 }
};
case OPT_VARFILE:
varfile = optarg;
break;
+ case OPT_VAROPTION:
+ varopts.push_back(string(optarg));
+ break;
case '?':
default:
print_help();
if (baseconf)
conf_read(baseconf);
- if (varfile)
- read_varfile(varfile);
- else
+ if (!varfile && varopts.empty())
set_all_symbols_variable();
+ else {
+ if (varfile)
+ read_varfile(varfile);
+ if (!varopts.empty())
+ for (auto o: varopts)
+ mark_symbol_variable(o.c_str(), NULL, 0);
+ }
mark_variable_expressions();
check_dep_consistency();
if (cnf)
sat_data.write_dimacs_cnf(cnf);
+ if (cnf)
+ sat_data.write_dimacs_cnf_all_single(cnf);
return EXIT_SUCCESS;
}
projects / linux-conf-perf.git / blobdiff