kconfig2sat: Cleanup

diff --git a/kconfig2sat/kconfig2sat.cc b/kconfig2sat/kconfig2sat.cc
index 07c9c83836d1443bc1a66baad6cb74ac2fdb44d3..f014419f182f0f9e64a42413ade9f41e354ff096 100644 (file)
--- 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)