kconfig2sat/kconfig2sat.cc

   1 #include <stdio.h>
   2 #include <stdlib.h>
   3 #include <string.h>
   4 #include <locale.h>
   5 #include <stdbool.h>
   6 #include <libintl.h>
   7 #include <unistd.h>
   8 #include <getopt.h>
   9 #include <inttypes.h>
  10
  11 #include "kconfig/lkc.h"
  12 #include "lcp_utils.h"
  13
  14 #include <vector>
  15 #include <map>
  16 #include <memory>
  17 #include <deque>
  18
  19 using namespace std;
  20
  21 int verbosity = 0;
  22
  23 enum options {
  24         OPT__START = 256,
  25         OPT_BASECONFIG,
  26         OPT_CNF,
  27         OPT_DOT,
  28         OPT_DUMP,
  29         OPT_ENV,
  30         OPT_HELP,
  31         OPT_KCONFIG,
  32         OPT_VARFILE,
  33         OPT_VAROPTION,
  34         OPT_VERBOSE,
  35 };
  36
  37 void print_help()
  38 {
  39         printf("Usage: kconfig2sat [options/actions]\n"
  40                "\n"
  41                "Options:\n"
  42                "  -b, --baseconf <.config>  Linux .config file with base configuration\n"
  43                "  --env <.conf.mk>          Set env. variables such as ARCH from .conf.mk\n"
  44                "  -k, --kconfig <Kconfig>   Kconfig file (with path)\n"
  45                "  --varfile <file>          File listing variable options (one option per line)\n"
  46                "\n"
  47                "Actions:\n"
  48                "  --dump                    Dump internal data (for debugging)\n"
  49                "  --cnf <file>              Generate CNF representation to <file>\n"
  50                 );
  51 }
  52
  53 typedef unique_ptr<char> upchar;
  54
  55 upchar expr_to_string(struct expr *e);
  56
  57 upchar sym_to_string(struct symbol *sym)
  58 {
  59         char *ret;
  60
  61         if (sym->name)
  62                 asprintf(&ret, sym->name);
  63         else
  64                 asprintf(&ret, "NONAME%d", sym->lcp.id);
  65         return upchar(ret);
  66 }
  67
  68 upchar expr_binop_to_string(struct expr *e, const char *op_str)
  69 {
  70         upchar l = expr_to_string(e->left.expr);
  71         upchar r = expr_to_string(e->right.expr);
  72         char *ret;
  73
  74         asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
  75         return upchar(ret);
  76 }
  77
  78 upchar expr_comp_to_string(struct expr *e, const char *op_str)
  79 {
  80         upchar l = sym_to_string(e->left.sym);
  81         upchar r = sym_to_string(e->right.sym);
  82         char *ret;
  83
  84         asprintf(&ret, "(%s %s %s)", l.get(), op_str, r.get());
  85         return upchar(ret);
  86 }
  87
  88 upchar expr_to_string(struct expr *e)
  89 {
  90         char *ret = NULL;
  91
  92         if (!e)
  93                 return NULL;
  94
  95         switch (e->type) {
  96         case E_NONE:
  97                 asprintf(&ret, "()%" PRIdPTR, (intptr_t)(e->right.expr));
  98                 return upchar(ret);
  99         case E_OR:
 100                 return expr_binop_to_string(e, "||");
 101         case E_AND:
 102                 return expr_binop_to_string(e, "&&");
 103         case E_NOT:
 104                 asprintf(&ret, "!%s", expr_to_string(e->left.expr).get());
 105                 break;
 106         case E_EQUAL:
 107                 return expr_comp_to_string(e, "==");
 108         case E_UNEQUAL:
 109                 return expr_comp_to_string(e, "!=");
 110         case E_LTH:
 111                 return expr_comp_to_string(e, "<");
 112         case E_LEQ:
 113                 return expr_comp_to_string(e, "<=");
 114         case E_GTH:
 115                 return expr_comp_to_string(e, ">");
 116         case E_GEQ:
 117                 return expr_comp_to_string(e, ">=");
 118         case E_LIST:
 119                 fprintf(stderr, "LIST not implemented\n");
 120                 exit(EXIT_FAILURE);
 121                 break;
 122         case E_SYMBOL:
 123                 return sym_to_string(e->left.sym);
 124         case E_RANGE:
 125                 fprintf(stderr, "RANGE not implemented\n");
 126                 exit(EXIT_FAILURE);
 127                 break;
 128         }
 129
 130         return upchar(ret);
 131 }
 132
 133
 134
 135 void dump_symbol(struct symbol *sym)
 136 {
 137         struct property *prop;
 138         upchar name = sym_to_string(sym);
 139         const char *type = sym_type_name(sym->type);
 140         const char *prompt = NULL;
 141         char flags[256] = "fl(";
 142         char val = '.';
 143
 144         if (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) {
 145                 switch (sym->curr.tri) {
 146                 case no:  val = 'n'; break;
 147                 case mod: val = 'm'; break;
 148                 case yes: val = 'y'; break;
 149                 }
 150         }
 151
 152 #define FLAG(f) do { if (sym->flags & (SYMBOL_##f)) strcat(flags, #f " "); } while (0)
 153         FLAG(CONST);
 154         FLAG(CHECK);
 155         FLAG(CHOICE);
 156         FLAG(CHOICEVAL);
 157         FLAG(VALID);
 158         FLAG(OPTIONAL);
 159         FLAG(WRITE);
 160         FLAG(CHANGED);
 161         FLAG(AUTO);
 162         FLAG(CHECKED);
 163         FLAG(WARNED);
 164         FLAG(DEF_USER);
 165         FLAG(DEF_AUTO);
 166         FLAG(DEF3);
 167         FLAG(DEF4);
 168         if (flags[3])
 169                 flags[strlen(flags)-1] = ')'; /* Replace trailing space */
 170 #undef FLAG
 171
 172         for_all_properties(sym, prop, P_PROMPT) {
 173                 prompt = prop->text;
 174         }
 175
 176         printf("%-40s %c %-8s %-50s %s\n", name.get(), val, type, flags, prompt);
 177
 178         if (verbosity > 0) {
 179                 if (sym->dir_dep.expr)
 180                         printf("    depends %s\n", expr_to_string(sym->dir_dep.expr).get());
 181
 182                 for_all_properties(sym, prop, P_SELECT) {
 183                         assert(prop->expr->type == E_SYMBOL);
 184                         printf("    selects %s if %s\n", prop->expr->left.sym->name,
 185                                expr_to_string(prop->visible.expr).get());
 186                 }
 187         }
 188 }
 189
 190 void do_dump()
 191 {
 192     int i;
 193     struct symbol *sym;
 194     for_all_symbols(i, sym) {
 195             dump_symbol(sym);
 196     }
 197 }
 198
 199 void mark_symbol_variable(const char *sym_name, const char *file, int lineno)
 200 {
 201         struct symbol *sym = sym_find(sym_name);
 202         if (!sym) {
 203                 fprintf(stderr, "%s:%d: Error: Invalid symbol: %s\n", file, lineno, sym_name);
 204                 exit(EXIT_FAILURE);
 205         }
 206 //      if (!(sym->flags & SYMBOL_WRITE)) {
 207 //              fprintf(stderr, "%s:%d: Error: Symbol %s not visible\n", varfile, lineno, sym_name);
 208 //              exit(EXIT_FAILURE);
 209 //      }
 210         if (sym->flags & (SYMBOL_CHOICEVAL | SYMBOL_CHOICE)) {
 211                 fprintf(stderr, "%s:%d: Error: Choice values not yet supported: %s", file, lineno, sym_name);
 212                 exit(EXIT_FAILURE);
 213         }
 214         struct property *prop;
 215         const char *prompt = NULL;
 216         for_all_properties(sym, prop, P_PROMPT) {
 217                 prompt = prop->text;
 218         }
 219         if (!prompt) {
 220                 fprintf(stderr, "%s:%d: Warning: Symbol %s is internal (has no prompt)\n", file, lineno, sym_name);
 221         }
 222         sym->lcp.variable = 1;
 223 }
 224
 225 void read_varfile(const char *varfile)
 226 {
 227         FILE *f = fopen(varfile, "r");
 228         char line[1000];
 229
 230         if (!f) {
 231                 perror(varfile);
 232                 exit(EXIT_FAILURE);
 233         }
 234
 235         int lineno = 0;
 236         while (fgets(line, sizeof(line), f)) {
 237                 char *p = line;
 238                 lineno++;
 239
 240                 if (line[0] == '#')
 241                         continue;
 242                 if (strncmp(line, CONFIG_, strlen(CONFIG_)) == 0)
 243                         p += strlen(CONFIG_);
 244
 245                 const char *sym_name = strtok(p, " =\n");
 246                 mark_symbol_variable(sym_name, varfile, lineno);
 247         }
 248         fclose(f);
 249 }
 250
 251 void set_all_symbols_variable()
 252 {
 253         int i;
 254         struct symbol *sym;
 255
 256         for_all_symbols(i, sym) {
 257                 if (!(sym->flags & (SYMBOL_CONST | SYMBOL_AUTO)))
 258                         sym->lcp.variable = 1;
 259         }
 260 }
 261
 262 struct SatLiteral {
 263         struct symbol *sym;
 264         struct expr *expr;
 265         int dot_printed:1;
 266
 267         SatLiteral(struct symbol *s) : sym(s), expr(nullptr) { assert(sym->lcp.variable && sym->lcp.id); }
 268         SatLiteral(struct expr *e)   : sym(nullptr), expr(e) { assert(expr->lcp.variable && expr->lcp.id); }
 269         sat_id id() const { return sym ? sym->lcp.id : expr->lcp.id; }
 270         upchar name() const {
 271                 char *ret;
 272                 if (sym) {
 273                         assert(sym->name); // TODO
 274                         asprintf(&ret, "%s", sym->name);
 275                 } else if (expr) {
 276                         asprintf(&ret, "expr%d", expr->lcp.id);
 277                 }
 278                 return upchar(ret);
 279         }
 280 };
 281
 282 typedef vector<sat_id> SatClause;
 283
 284 struct Implication: public SatClause {
 285         Implication(sat_id a, sat_id b) : SatClause{-a, b} {}
 286 };
 287
 288 struct SatExpr {
 289         sat_id left, right;
 290         enum expr_type op;
 291
 292         SatExpr(sat_id l, enum expr_type o, sat_id r)
 293                 : left(l), right(r), op(o) {}
 294         bool operator<(const SatExpr &o) const { return tie(left, right, op) < tie(o.left, o.right, o.op); }
 295 };
 296
 297 class SatLiterals : protected vector<struct SatLiteral>
 298 {
 299 public:
 300         using vector<struct SatLiteral>::begin;
 301         using vector<struct SatLiteral>::end;
 302         using vector<struct SatLiteral>::push_back;
 303         SatLiterals() { reserve(20000); }
 304         int count() const { return size(); }
 305         const SatLiteral &operator[](size_type i) const { return at(i-1); }
 306         SatLiteral &last() { return *(--end()); }
 307         bool test_set_dot_printed(struct symbol *sym) const {
 308                 auto l = (*this)[sym->lcp.id];
 309                 bool ret = l.dot_printed;
 310                 l.dot_printed = 1;
 311                 return ret;
 312         }
 313         bool test_set_dot_printed(struct expr *e) const {
 314                 auto l = (*this)[e->lcp.id];
 315                 bool ret = l.dot_printed;
 316                 l.dot_printed = 1;
 317                 return ret;
 318         }
 319 };
 320
 321 /*
 322  * bool FOO!=n => FOO
 323  * bool FOO!=y => !FOO
 324  * bool FOO==n => !FOO
 325  * bool FOO==y => FOO
 326  */
 327 struct expr *expr_eliminate_eq_yn(struct expr *e)
 328 {
 329         if (!e)
 330                 return NULL;
 331         switch (e->type) {
 332         case E_AND:
 333         case E_OR:
 334         case E_NOT:
 335                 e->left.expr = expr_eliminate_eq_yn(e->left.expr);
 336                 e->right.expr = expr_eliminate_eq_yn(e->right.expr);
 337                 break;
 338         case E_UNEQUAL:
 339                 // UNKNOWN symbols sometimes occur in dependency -
 340                 // e.g. ACPI_VIDEO on arm (the symbol is only defined
 341                 // for ACPI platforms (x86) but some drivers refer to
 342                 // it.
 343                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 344                         if (e->right.sym == &symbol_no) {
 345                                 // FOO!=n -> FOO
 346                                 e->type = E_SYMBOL;
 347                                 e->right.sym = NULL;
 348                         } else if (e->right.sym == &symbol_yes) {
 349                                 // FOO!=y -> !FOO
 350                                 e->type = E_SYMBOL;
 351                                 e->right.sym = NULL;
 352                                 e = expr_alloc_one(E_NOT, e);
 353                         }
 354                 }
 355                 break;
 356         case E_EQUAL:
 357                 if (e->left.sym->type == S_TRISTATE || e->left.sym->type == S_BOOLEAN || e->left.sym->type == S_UNKNOWN) {
 358                         if (e->right.sym == &symbol_yes) {
 359                                 // FOO==y -> FOO
 360                                 e->type = E_SYMBOL;
 361                                 e->right.sym = NULL;
 362                         } else if (e->right.sym == &symbol_no) {
 363                                 // FOO==n -> !FOO
 364                                 e->type = E_SYMBOL;
 365                                 e->right.sym = NULL;
 366                                 e = expr_alloc_one(E_NOT, e);
 367                         }
 368                 }
 369                 break;
 370         default:
 371                 ;
 372         }
 373         return e;
 374 }
 375
 376 bool mark_variable_expressions(struct expr *e)
 377 {
 378         if (!e)
 379                 return false;
 380
 381         switch (e->type) {
 382         case E_SYMBOL:
 383                 return (e->lcp.variable = e->left.sym->lcp.variable);
 384         case E_NONE:
 385                 fprintf(stderr, "NONE not implemented\n");
 386                 exit(EXIT_FAILURE);
 387                 break;
 388         case E_NOT:
 389                 if (mark_variable_expressions(e->left.expr))
 390                         return (e->lcp.variable = 1);
 391                 else
 392                         return false;
 393         case E_OR:
 394         case E_AND: {
 395                 mark_variable_expressions(e->left.expr);
 396                 mark_variable_expressions(e->right.expr);
 397
 398                 if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
 399                         return (e->lcp.variable = 1);
 400                 } else if (!e->left.expr->lcp.variable && !e->right.expr->lcp.variable) {
 401                         return (e->lcp.variable = 0);
 402                 } else {
 403                         tristate val;
 404
 405                         if (e->left.expr->lcp.variable) {
 406                                 val = expr_calc_value(e->right.expr);
 407                         } else if (e->right.expr->lcp.variable) {
 408                                 val = expr_calc_value(e->left.expr);
 409                         }
 410                         if ((e->type == E_OR && val == yes) ||
 411                             (e->type == E_AND && val == no))
 412                                 return (e->lcp.variable = 0);
 413                         else
 414                                 return (e->lcp.variable = 1);
 415                 }
 416                 __builtin_unreachable();
 417         }
 418         case E_EQUAL:
 419         case E_UNEQUAL:
 420                 if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
 421                         return (e->lcp.variable = 1);
 422                 } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 423                         fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
 424                         exit(EXIT_FAILURE);
 425                 } else
 426                         return false;
 427         case E_LTH:
 428         case E_LEQ:
 429         case E_GTH:
 430         case E_GEQ:
 431                 if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 432                         fprintf(stderr, "Comparison of variable symbols not implemented\n");
 433                         exit(EXIT_FAILURE);
 434                 } else
 435                         return false;
 436                 break;
 437         case E_LIST:
 438                 fprintf(stderr, "LIST not implemented\n");
 439                 exit(EXIT_FAILURE);
 440                 break;
 441         case E_RANGE:
 442                 fprintf(stderr, "RANGE not implemented\n");
 443                 exit(EXIT_FAILURE);
 444                 break;
 445         }
 446         fprintf(stderr, "Unexpected situation in mark_variable_expressions\n");
 447         exit(EXIT_FAILURE);
 448 }
 449
 450 void mark_variable_expressions()
 451 {
 452         int i;
 453         struct symbol *sym;
 454         struct property *prop;
 455
 456         for_all_symbols(i, sym) {
 457                 mark_variable_expressions(sym->dir_dep.expr);
 458                 mark_variable_expressions(sym->rev_dep.expr);
 459                 for_all_properties(sym, prop, P_SELECT) {
 460                         assert(prop->expr->type == E_SYMBOL);
 461                         mark_variable_expressions(prop->visible.expr);
 462                 }
 463         }
 464 }
 465
 466 void check_dep_consistency()
 467 {
 468         int i;
 469         struct symbol *sym;
 470         tristate val;
 471
 472         for_all_symbols(i, sym) {
 473                 if (sym->lcp.variable && sym->dir_dep.expr && !sym->dir_dep.expr->lcp.variable) {
 474                         val = expr_calc_value(sym->dir_dep.expr);
 475                         if (val == no) {
 476                                 fprintf(stderr, "Symbol %s cannot be variable because its dependency is always 'no': %s\n",
 477                                         sym->name, expr_to_string(sym->dir_dep.expr).get());
 478                                 exit(EXIT_FAILURE);
 479                         }
 480                 }
 481                 if (sym->lcp.variable && sym->rev_dep.expr && !sym->rev_dep.expr->lcp.variable) {
 482                         val = expr_calc_value(sym->rev_dep.expr);
 483                         if (val == yes) {
 484                                 fprintf(stderr, "Symbol %s cannot be variable because it is selected by expression that is always 'yes': %s\n",
 485                                         sym->name, expr_to_string(sym->rev_dep.expr).get());
 486                                 exit(EXIT_FAILURE);
 487                         }
 488                 }
 489                 if (!sym->lcp.variable && (sym->type == S_BOOLEAN || sym->type == S_TRISTATE) &&
 490                     sym->curr.tri == no && sym->rev_dep.expr && sym->rev_dep.expr->lcp.variable) {
 491                         fprintf(stderr, "Symbol %s cannot be fixed to 'no', because it is selcted by variable expression '%s'\n",
 492                                 sym->name, expr_to_string(sym->rev_dep.expr).get());
 493                         exit(EXIT_FAILURE);
 494                 }
 495         }
 496 }
 497
 498
 499 class DotWriter {
 500         FILE *f;
 501         void symbol(struct symbol *sym) {
 502                 const char *opts = "";
 503                 if (sym->lcp.variable)
 504                         opts = " [penwidth=3]";
 505                 else
 506                         opts = " [color=gray]";
 507                 fprintf(f, "\"%s\"%s;\n", sym->name, opts);
 508         }
 509         void expr(struct expr *e, upchar name) {
 510                 const char *label = "???";
 511                 switch (e->type) {
 512                 case E_OR:  label = "|"; break;
 513                 case E_AND: label = "&"; break;
 514                 case E_EQUAL: label = "="; break;
 515                 case E_UNEQUAL: label = "!="; break;
 516                 case E_NOT: label = "!"; break;
 517                 case E_SYMBOL:
 518                 case E_NONE:
 519                 case E_RANGE:
 520                 case E_LTH:
 521                 case E_LEQ:
 522                 case E_GTH:
 523                 case E_GEQ:
 524                 case E_LIST:
 525                 default:
 526                         fprintf(stderr, "Expr %d not implemented\n", e->type);
 527                         exit(EXIT_FAILURE);
 528                         break;
 529                 }
 530
 531                 fprintf(f, "\"%s\" [shape=diamond,label=\"%s\"];\n", name.get(), label);
 532         }
 533 public:
 534         DotWriter(const char *file_name) {
 535                 f = fopen(file_name, "w");
 536
 537                 if (!f) {
 538                         perror(file_name);
 539                         exit(EXIT_FAILURE);
 540                 }
 541
 542                 fprintf(f, "digraph conf {\n");
 543                 //fprintf(f, "rankdir=LR;\n");
 544         }
 545         ~DotWriter() {
 546                 fprintf(f, "}\n");
 547                 fclose(f);
 548         }
 549         void literal(SatLiteral &l) {
 550                 if (l.dot_printed)
 551                         return;
 552                 l.dot_printed = 1;
 553                 if (l.sym)
 554                         symbol(l.sym);
 555                 if (l.expr)
 556                         expr(l.expr, l.name());
 557         }
 558         void depends_on(const SatLiteral &l1, const SatLiteral &l2) {
 559                 fprintf(f, "\"%s\" -> \"%s\" [style=bold,label=d];\n", l1.name().get(), l2.name().get());
 560         }
 561         void selects(const SatLiteral &l1, const SatLiteral &l2) {
 562                 fprintf(f, "\"%s\" -> \"%s\" [style=bold,arrowhead=open,label=s];\n", l1.name().get(), l2.name().get());
 563         }
 564         void edge(const SatLiteral &from, const SatLiteral &to) {
 565                 fprintf(f, "\"%s\" -> \"%s\" [arrowhead=empty];\n", from.name().get(), to.name().get());
 566         }
 567 };
 568
 569 class SatData {
 570         SatLiterals literals = {};
 571         vector<SatClause> clauses = {};
 572         map<SatExpr, sat_id> expressions = {};
 573         DotWriter *dot = nullptr;
 574 public:
 575
 576         SatData(const char *dot_fn) {
 577                 if (dot_fn)
 578                         dot = new DotWriter(dot_fn);
 579                 symbols2literals();
 580                 expressions2literals();
 581                 expressions2clauses();
 582                 if (dot)
 583                         delete dot;
 584
 585         }
 586
 587         const SatLiteral &add_literal(struct symbol *sym) {
 588                 sym->lcp.id = literals.count() + 1;
 589                 literals.push_back(SatLiteral(sym));
 590                 if (dot)
 591                         dot->literal(literals.last());
 592                 return literals.last();
 593         }
 594
 595         const SatLiteral &add_literal(struct expr *e) {
 596                 e->lcp.id = literals.count() + 1;
 597                 literals.push_back(SatLiteral(e));
 598                 if (dot)
 599                         dot->literal(literals.last());
 600                 return literals.last();
 601         }
 602
 603         void symbols2literals() {
 604                 int i;
 605                 struct symbol *sym;
 606
 607                 for_all_symbols(i, sym) {
 608                         if (sym->lcp.variable)
 609                                 add_literal(sym);
 610                 }
 611         }
 612
 613         // Assign e->lcp.id to variable literals
 614         sat_id expr2literal(struct expr *e) {
 615                 if (!e || !e->lcp.variable)
 616                         return 0;
 617                 if (e->lcp.id)
 618                         return e->lcp.id;
 619
 620                 switch (e->type) {
 621                 case E_SYMBOL:
 622                         assert(e->left.sym->lcp.id);
 623                         e->lcp.id = e->left.sym->lcp.id;
 624                         break;
 625                 case E_NONE:
 626                         fprintf(stderr, "NONE not implemented\n");
 627                         exit(EXIT_FAILURE);
 628                         break;
 629                 case E_NOT: {
 630                         expr2literal(e->left.expr);
 631
 632                         SatExpr se(e->left.expr->lcp.id, e->type, 0);
 633                         auto it = expressions.find(se);
 634                         if (it == expressions.end()) {
 635                                 auto l = add_literal(e);
 636                                 expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
 637                                 if (dot)
 638                                         dot->edge(literals[e->left.expr->lcp.id], l);
 639                         } else
 640                                 e->lcp.id = it->second;
 641                         break;
 642                 }
 643                 case E_OR:
 644                 case E_AND: {
 645                         expr2literal(e->left.expr);
 646                         expr2literal(e->right.expr);
 647
 648                         if (e->left.expr->lcp.variable && e->right.expr->lcp.variable) {
 649                                 SatExpr se = SatExpr(e->left.expr->lcp.id, e->type, e->right.expr->lcp.id);
 650                                 auto it = expressions.find(se);
 651                                 if (it == expressions.end()) {
 652                                         auto l = add_literal(e);
 653                                         expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
 654                                         if (dot) {
 655                                                 dot->edge(literals[e->left.expr->lcp.id], l);
 656                                                 dot->edge(literals[e->right.expr->lcp.id], l);
 657                                         }
 658                                 } else
 659                                         e->lcp.id = it->second;
 660                         } else {
 661                                 if (e->left.expr->lcp.variable) {
 662                                         e->lcp.id = e->left.expr->lcp.id;
 663                                 } else if (e->right.expr->lcp.variable) {
 664                                         e->lcp.id = e->right.expr->lcp.id;
 665                                 }
 666                         }
 667                         break;
 668                 }
 669                 case E_EQUAL:
 670                 case E_UNEQUAL: {
 671                         if (e->left.sym->lcp.variable && e->right.sym->lcp.variable) {
 672                                 SatExpr se(e->left.sym->lcp.id, e->type, e->right.sym->lcp.id);
 673                                 auto it = expressions.find(se);
 674                                 if (it == expressions.end()) {
 675                                         auto l = add_literal(e);
 676                                         expressions.insert(pair<SatExpr, sat_id>(se, l.id()));
 677                                         if (dot) {
 678                                                 dot->edge(literals[e->left.sym->lcp.id], l);
 679                                                 dot->edge(literals[e->right.sym->lcp.id], l);
 680                                         }
 681                                 } else
 682                                         e->lcp.id = it->second;
 683                         } else if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 684                                 fprintf(stderr, "Comparison with fixed symbol not yet supported!\n");
 685                                 exit(EXIT_FAILURE);
 686                         }
 687                         break;
 688                 }
 689                 case E_LTH:
 690                 case E_LEQ:
 691                 case E_GTH:
 692                 case E_GEQ:
 693                         if (e->left.sym->lcp.variable || e->right.sym->lcp.variable) {
 694                                 fprintf(stderr, "Comparison of variable symbols not implemented\n");
 695                                 exit(EXIT_FAILURE);
 696                         }
 697                         break;
 698                 case E_LIST:
 699                         fprintf(stderr, "LIST not implemented\n");
 700                         exit(EXIT_FAILURE);
 701                         break;
 702                 case E_RANGE:
 703                         fprintf(stderr, "RANGE not implemented\n");
 704                         exit(EXIT_FAILURE);
 705                         break;
 706                 }
 707                 assert(e->lcp.id);
 708                 return e->lcp.id;
 709         }
 710
 711         void expressions2literals() {
 712                 int i;
 713                 struct symbol *sym;
 714                 struct expr *e;
 715                 sat_id id;
 716                 const SatLiteral *syml;
 717
 718                 for_all_symbols(i, sym) {
 719                         if (sym->lcp.variable &&
 720                             (sym->type == S_BOOLEAN || sym->type == S_TRISTATE)) {
 721                                 syml = &literals[sym->lcp.id];
 722                                 // Direct dependencies
 723                                 //sym->dir_dep.expr = expr_eliminate_eq_yn(sym->dir_dep.expr);
 724                                 e = sym->dir_dep.expr;
 725                                 id = expr2literal(e);
 726                                 if (id) {
 727                                         clauses.push_back(Implication(sym->lcp.id, id));
 728                                         if (dot)
 729                                                 dot->depends_on(*syml, literals[id]);
 730                                 }
 731
 732                                 // Reverse dependecies
 733                                 e = sym->rev_dep.expr;
 734                                 id = expr2literal(e);
 735                                 if (id) {
 736                                         clauses.push_back(Implication(id, sym->lcp.id));
 737                                         if (dot)
 738                                                 dot->selects(literals[id], *syml);
 739                                 }
 740                         }
 741                 }
 742         }
 743
 744         // Tseitin Transformation - see
 745         // https://en.wikipedia.org/wiki/Tseitin_transformation or
 746         // http://fmv.jku.at/biere/talks/Biere-TPTPA11.pdf, slide 27.
 747         void expressions2clauses() {
 748                 for (auto expr: expressions) {
 749                         SatExpr e = expr.first;
 750                         sat_id e_id = expr.second;
 751                         assert(e_id);
 752                         if (e.left == 0 || (e.right == 0 && e.op != E_NOT)) {
 753                                 upchar tmp(expr_to_string(literals[e_id].expr));
 754                                 printf("Unexpected sat_id == 0 in %s\n", tmp.get());
 755                                 //exit(1);
 756                         }
 757                         switch (e.op) {
 758                         case E_SYMBOL:
 759                         case E_NONE:
 760                                 assert(0);
 761                                 break;
 762                         case E_NOT:
 763                                 clauses.push_back(SatClause{  e_id,  e.left });
 764                                 clauses.push_back(SatClause{ -e_id, -e.left });
 765                                 break;
 766                         case E_OR:
 767                                 clauses.push_back(SatClause{ -e.left,  e_id });
 768                                 clauses.push_back(SatClause{ -e.right, e_id });
 769                                 clauses.push_back(SatClause{ -e_id,    e.left, e.right });
 770                                 break;
 771                         case E_AND:
 772                                 clauses.push_back(SatClause{ -e_id, e.left });
 773                                 clauses.push_back(SatClause{ -e_id, e.right });
 774                                 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
 775                                 break;
 776                         case E_EQUAL:
 777                                 clauses.push_back(SatClause{ -e_id, -e.left, e.right });
 778                                 clauses.push_back(SatClause{ -e_id, -e.right, e.left });
 779                                 clauses.push_back(SatClause{ -e.left, -e.right, e_id });
 780                                 clauses.push_back(SatClause{ e.left, e.right, e_id });
 781                                 break;
 782                         case E_UNEQUAL:
 783                                 clauses.push_back(SatClause{ -e_id, -e.left, -e.right });
 784                                 clauses.push_back(SatClause{ -e_id, e.right, e.left });
 785                                 clauses.push_back(SatClause{ -e.left, e.right, e_id });
 786                                 clauses.push_back(SatClause{ e.left, -e.right, e_id });
 787                                 break;
 788                         case E_LTH:
 789                         case E_LEQ:
 790                         case E_GTH:
 791                         case E_GEQ: {
 792                                 struct expr *e = literals[e_id].expr;
 793                                 upchar tmp(expr_to_string(e));
 794                                 tristate val = expr_calc_value(e);
 795                                 //fprintf(stderr, "Comparison operators not implemented %s = %d\n", tmp.get(), val);
 796                                 //exit(EXIT_FAILURE);
 797                                 clauses.push_back(SatClause{ val == yes ? e_id : -e_id });
 798                                 break;
 799                         }
 800                         case E_LIST:
 801                                 fprintf(stderr, "LIST not implemented\n");
 802                                 exit(EXIT_FAILURE);
 803                                 break;
 804                         case E_RANGE:
 805                                 fprintf(stderr, "RANGE not implemented\n");
 806                                 exit(EXIT_FAILURE);
 807                                 break;
 808                         }
 809                 }
 810
 811         }
 812
 813         void write_dimacs_cnf(const char *cnf) {
 814                 FILE *f = fopen(cnf, "w");
 815
 816                 if (!f) {
 817                         perror(cnf);
 818                         exit(EXIT_FAILURE);
 819                 }
 820
 821                 fprintf(f, "p cnf %d %lu\n", literals.count(), clauses.size());
 822
 823                 for (auto l: literals) {
 824                         if (l.sym)
 825                                 fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
 826                         if (l.expr)
 827                                 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
 828                 }
 829                 for (auto clause: clauses) {
 830                         for (sat_id id: clause) {
 831                                 assert(id != 0);
 832                                 fprintf(f, "%d ", id);
 833                         }
 834                         fprintf(f, "0\n");
 835                 }
 836                 fclose(f);
 837         }
 838         void write_dimacs_cnf_single(const char *cnf, const char *sym_name) {
 839                 FILE *f = fopen((string(cnf)+"-single-"+sym_name).c_str(), "w");
 840
 841                 if (!f) {
 842                         perror(cnf);
 843                         exit(EXIT_FAILURE);
 844                 }
 845
 846                 fprintf(f, "p cnf %d %lu\n", 2*literals.count(), 2*clauses.size() + 2*literals.count());
 847
 848                 for (auto l: literals) {
 849                         if (l.sym)
 850                                 fprintf(f, "c SYM %d %s\n", l.sym->lcp.id, l.sym->name);
 851                         if (l.expr)
 852                                 fprintf(f, "c EXPR %d %s\n", l.expr->lcp.id, expr_to_string(l.expr).get());
 853                 }
 854                 for (auto clause: clauses) {
 855                         for (sat_id id: clause) {
 856                                 assert(id != 0);
 857                                 fprintf(f, "%d ", id);
 858                         }
 859                         fprintf(f, "0\n");
 860
 861                         for (sat_id id: clause) {
 862                                 fprintf(f, "%d ", id > 0 ? id + literals.count() : id - literals.count());
 863                         }
 864                         fprintf(f, "0\n");
 865                 }
 866                 fprintf(f, "c Equivalence\n");
 867                 for (auto l: literals) {
 868                         if (l.sym && strcmp(sym_name, l.sym->name) != 0) {
 869                                 fprintf(f, "%d %d 0\n", -l.id(), l.id() + literals.count());
 870                                 fprintf(f, "%d %d 0\n", -l.id() - literals.count(), l.id());
 871                         } else {
 872                                 fprintf(f, "%d 0\n", +l.id());
 873                                 fprintf(f, "%d 0\n", -l.id() - literals.count());
 874                         }
 875                 }
 876                 fclose(f);
 877         }
 878
 879         void write_dimacs_cnf_all_single(const char *cnf) {
 880                 for (auto l: literals)
 881                         if (l.sym)
 882                                 write_dimacs_cnf_single(cnf, l.sym->name);
 883         }
 884 };
 885
 886 int main(int argc, char **argv)
 887 {
 888         int c;
 889
 890         char *baseconf = NULL;
 891         char *cnf = NULL;
 892         char *dot = NULL;
 893         char *kconfig = NULL;
 894         char *varfile = NULL;
 895         int  dump = false;
 896         deque<string> varopts;
 897
 898         while (1) {
 899                 int option_index = 0;
 900                 static struct option long_options[] = {
 901                         {"baseconf",    required_argument, 0,     OPT_BASECONFIG },
 902                         {"cnf",         required_argument, 0,     OPT_CNF },
 903                         {"dot",         required_argument, 0,     OPT_DOT },
 904                         {"env",         required_argument, 0,     OPT_ENV },
 905                         {"dump",        no_argument,       &dump, true },
 906                         {"help",        no_argument,       0,     OPT_HELP },
 907                         {"kconfig",     required_argument, 0,     OPT_KCONFIG },
 908                         {"varfile",     required_argument, 0,     OPT_VARFILE },
 909                         {"varopt",      required_argument, 0,     OPT_VAROPTION },
 910                         {"verbose",     no_argument,       0,     OPT_VERBOSE },
 911                         {0,             0,                 0,     0 }
 912                 };
 913
 914                 c = getopt_long(argc, argv, "b:hk:v",
 915                                 long_options, &option_index);
 916                 if (c == -1)
 917                         break;
 918
 919                 switch (c) {
 920                 case 0: /* long option with flag != NULL */
 921                         break;
 922                 case 'b':
 923                 case OPT_BASECONFIG:
 924                         baseconf = optarg;
 925                         break;
 926                 case OPT_CNF:
 927                         cnf = optarg;
 928                         break;
 929                 case OPT_DOT:
 930                         dot = optarg;
 931                         break;
 932                 case OPT_ENV:
 933                         set_missing_env(optarg);
 934                         break;
 935                 case 'h':
 936                 case OPT_HELP:
 937                         print_help();
 938                         exit(EXIT_SUCCESS);
 939                 case 'k':
 940                 case OPT_KCONFIG:
 941                         kconfig = optarg;
 942                         break;
 943                 case 'v':
 944                 case OPT_VERBOSE:
 945                         verbosity++;
 946                         break;
 947                 case OPT_VARFILE:
 948                         varfile = optarg;
 949                         break;
 950                 case OPT_VAROPTION:
 951                         varopts.push_back(string(optarg));
 952                         break;
 953                 case '?':
 954                 default:
 955                         print_help();
 956                         exit(EXIT_FAILURE);
 957                         printf("?? getopt returned character code 0%o ??\n", c);
 958                 }
 959         }
 960
 961         if (optind < argc) {
 962                 fprintf(stderr, "Unexpected option '%s'\n", argv[optind]);
 963                 print_help();
 964                 exit(EXIT_FAILURE);
 965         }
 966
 967
 968         if (kconfig == NULL) {
 969                 fprintf(stderr, "--kconfig option missing\n");
 970                 exit(EXIT_FAILURE);
 971         }
 972
 973         setlocale(LC_ALL, "");
 974         bindtextdomain(PACKAGE, LOCALEDIR);
 975         textdomain(PACKAGE);
 976
 977         conf_parse_path(kconfig);
 978         if (baseconf)
 979                 conf_read(baseconf);
 980
 981         if (!varfile && varopts.empty())
 982                 set_all_symbols_variable();
 983         else {
 984                 if (varfile)
 985                         read_varfile(varfile);
 986                 if (!varopts.empty())
 987                         for (auto o: varopts)
 988                                 mark_symbol_variable(o.c_str(), NULL, 0);
 989         }
 990
 991         mark_variable_expressions();
 992         check_dep_consistency();
 993
 994         SatData sat_data(dot);
 995
 996         if (dump)
 997                 do_dump();
 998
 999         if (cnf)
1000                 sat_data.write_dimacs_cnf(cnf);
1001         if (cnf)
1002                 sat_data.write_dimacs_cnf_all_single(cnf);
1003
1004         return EXIT_SUCCESS;
1005 }