From 7e586bef121a66898c00e150a9273a8c1f2b5956 Mon Sep 17 00:00:00 2001 From: Michal Sojka Date: Sun, 25 Oct 2015 23:52:28 +0100 Subject: [PATCH] kconfig2sat: Cleanup --- kconfig2sat/kconfig2sat.cc | 167 +++++++------------------------------ 1 file changed, 32 insertions(+), 135 deletions(-) diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc index 07c9c83..f014419 100644 --- a/kconfig2sat/kconfig2sat.cc +++ b/kconfig2sat/kconfig2sat.cc @@ -291,7 +291,6 @@ struct SatExpr { 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); } }; @@ -304,7 +303,7 @@ public: 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()); } + SatLiteral &last() { return *(--end()); } bool test_set_dot_printed(struct symbol *sym) const { auto l = (*this)[sym->lcp.id]; bool ret = l.dot_printed; @@ -499,27 +498,7 @@ void check_dep_consistency() 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]"; @@ -527,13 +506,9 @@ public: 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; @@ -548,12 +523,37 @@ public: 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()); @@ -588,7 +588,7 @@ public: sym->lcp.id = literals.count() + 1; literals.push_back(SatLiteral(sym)); if (dot) - dot->symbol(sym); + dot->literal(literals.last()); return literals.last(); } @@ -596,7 +596,7 @@ public: e->lcp.id = literals.count() + 1; literals.push_back(SatLiteral(e)); if (dot) - dot->expr(literals.last()); + dot->literal(literals.last()); return literals.last(); } @@ -836,109 +836,6 @@ public: 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); -// } }; int main(int argc, char **argv) -- 2.39.2