src/solver.c

   1 /*
   2  * solver.c
   3  *
   4  * SAT based dependency solver
   5  */
   6
   7 #include <stdio.h>
   8 #include <stdlib.h>
   9 #include <unistd.h>
  10 #include <string.h>
  11
  12 #include "solver.h"
  13 #include "bitmap.h"
  14 #include "pool.h"
  15 #include "util.h"
  16 #include "evr.h"
  17
  18 #define RULES_BLOCK 63
  19
  20 static Pool *prune_best_version_arch_sortcmp_data;
  21
  22 /*-----------------------------------------------------------------*/
  23
  24 /*
  25  * prep for prune_best_version_arch
  26  *   sort by name
  27  */
  28
  29 static int
  30 prune_best_version_arch_sortcmp(const void *ap, const void *bp)
  31 {
  32   Pool *pool = prune_best_version_arch_sortcmp_data;
  33   Id a = *(Id *)ap;
  34   Id b = *(Id *)bp;
  35   return pool->solvables[a].name - pool->solvables[b].name;
  36 }
  37
  38
  39 #if 0
  40 static Id
  41 replaces_system(Solver *solv, Id id)
  42 {
  43   Pool *pool = solv->pool;
  44   Source *system = solv->system;
  45   Id *name = pool->solvables[id].name;
  46
  47   FOR_PROVIDES(p, pp, id)
  48     {
  49       s = pool->solvables + p;
  50       if (s->name != name)
  51         continue;
  52       if (p >= system->start && p < system->start + system->nsolvables)
  53         return p;
  54     }
  55 }
  56 #endif
  57
  58 static int
  59 dep_installed(Solver *solv, Id dep)
  60 {
  61   Pool *pool = solv->pool;
  62   Id p, *pp;
  63
  64   if (ISRELDEP(dep))
  65     {
  66       Reldep *rd = GETRELDEP(pool, dep);
  67       if (rd->flags == REL_AND)
  68         {
  69           if (!dep_installed(solv, rd->name))
  70             return 0;
  71           return dep_installed(solv, rd->evr);
  72         }
  73       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  74         return dep_installed(solv, rd->evr);
  75     }
  76   FOR_PROVIDES(p, pp, dep)
  77     {
  78       if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
  79         return 1;
  80     }
  81   return 0;
  82 }
  83
  84 static inline int
  85 dep_fulfilled(Solver *solv, Id dep)
  86 {
  87   Pool *pool = solv->pool;
  88   Id p, *pp;
  89
  90   if (ISRELDEP(dep))
  91     {
  92       Reldep *rd = GETRELDEP(pool, dep);
  93       if (rd->flags == REL_AND)
  94         {
  95           if (!dep_fulfilled(solv, rd->name))
  96             return 0;
  97           return dep_fulfilled(solv, rd->evr);
  98         }
  99       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
 100         return dep_installed(solv, rd->evr);
 101     }
 102   FOR_PROVIDES(p, pp, dep)
 103     {
 104       if (solv->decisionmap[p] > 0)
 105         return 1;
 106     }
 107   return 0;
 108 }
 109
 110 static inline int
 111 dep_possible(Solver *solv, Id dep, Map *m)
 112 {
 113   Pool *pool = solv->pool;
 114   Id p, *pp;
 115
 116   if (ISRELDEP(dep))
 117     {
 118       Reldep *rd = GETRELDEP(pool, dep);
 119       if (rd->flags == REL_AND)
 120         {
 121           if (!dep_possible(solv, rd->name, m))
 122             return 0;
 123           return dep_possible(solv, rd->evr, m);
 124         }
 125       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
 126         return dep_installed(solv, rd->evr);
 127     }
 128   FOR_PROVIDES(p, pp, dep)
 129     {
 130       if (MAPTST(m, p))
 131         return 1;
 132     }
 133   return 0;
 134 }
 135
 136 /*
 137  * prune_to_recommended
 138  *
 139  * XXX: should we prune to requires/suggests that are already
 140  * fulfilled by other packages?
 141  */
 142 static void
 143 prune_to_recommended(Solver *solv, Queue *plist)
 144 {
 145   Pool *pool = solv->pool;
 146   int i, j;
 147   Solvable *s;
 148   Id p, *pp, sup, *supp, rec, *recp, sug, *sugp, enh, *enhp;
 149
 150   if (solv->recommends_index < 0)
 151     {
 152       MAPZERO(&solv->recommendsmap);
 153       MAPZERO(&solv->suggestsmap);
 154       solv->recommends_index = 0;
 155     }
 156   while (solv->recommends_index < solv->decisionq.count)
 157     {
 158       p = solv->decisionq.elements[solv->recommends_index++];
 159       if (p < 0)
 160         continue;
 161       s = pool->solvables + p;
 162       if ((recp = s->recommends) != 0)
 163         while ((rec = *recp++) != 0)
 164           FOR_PROVIDES(p, pp, rec)
 165             MAPSET(&solv->recommendsmap, p);
 166       if ((sugp = s->suggests) != 0)
 167         while ((sug = *sugp++) != 0)
 168           FOR_PROVIDES(p, pp, sug)
 169             MAPSET(&solv->suggestsmap, p);
 170     }
 171   /* prune to recommended/supplemented */
 172   for (i = j = 0; i < plist->count; i++)
 173     {
 174       p = plist->elements[i];
 175       if (MAPTST(&solv->recommendsmap, p))
 176         {
 177           plist->elements[j++] = p;
 178           continue;
 179         }
 180       s = pool->solvables + p;
 181       if (!s->supplements && !s->freshens)
 182         continue;
 183       if ((supp = s->supplements) != 0)
 184         {
 185           while ((sup = *supp++) != 0)
 186             if (dep_fulfilled(solv, sup))
 187               break;
 188           if (!sup)
 189             continue;
 190         }
 191       if ((supp = s->freshens) != 0)
 192         {
 193           while ((sup = *supp++) != 0)
 194             if (dep_fulfilled(solv, sup))
 195               break;
 196           if (!sup)
 197             continue;
 198         }
 199       plist->elements[j++] = s - pool->solvables;
 200     }
 201   if (j)
 202     plist->count = j;
 203
 204   /* prune to suggested/enhanced*/
 205   if (plist->count < 2)
 206     return;
 207   for (i = j = 0; i < plist->count; i++)
 208     {
 209       p = plist->elements[i];
 210       if (MAPTST(&solv->suggestsmap, p))
 211         {
 212           plist->elements[j++] = p;
 213           continue;
 214         }
 215       s = pool->solvables + p;
 216       if (!(enhp = s->enhances))
 217         continue;
 218       while ((enh = *enhp++) != 0)
 219         if (dep_fulfilled(solv, enh))
 220           break;
 221       if (!enh)
 222         continue;
 223       plist->elements[j++] = s - pool->solvables;
 224     }
 225   if (j)
 226     plist->count = j;
 227 }
 228
 229 /*
 230  * prune_best_version_arch
 231  *
 232  * sort list of packages (given through plist) by name and evr
 233  * return result through plist
 234  *
 235  */
 236
 237 /* FIXME: must also look at update packages */
 238
 239 void
 240 prune_best_version_arch(Pool *pool, Queue *plist)
 241 {
 242   Id best = ID_NULL;
 243   int i, j;
 244   Solvable *s;
 245   Id a, bestscore;
 246
 247   if (plist->count < 2)         /* no need to prune for a single entry */
 248     return;
 249   if (pool->verbose) printf("prune_best_version_arch %d\n", plist->count);
 250
 251   /* prune to best architecture */
 252   if (pool->id2arch)
 253     {
 254       bestscore = 0;
 255       for (i = 0; i < plist->count; i++)
 256         {
 257           s = pool->solvables + plist->elements[i];
 258           a = s->arch;
 259           if (a > pool->lastarch)
 260             continue;
 261           a = pool->id2arch[a];
 262           if (!bestscore || (a & 0xffff0000) < bestscore)
 263             bestscore = a & 0xffff0000;
 264         }
 265       for (i = j = 0; i < plist->count; i++)
 266         {
 267           s = pool->solvables + plist->elements[i];
 268           a = s->arch;
 269           if (a > pool->lastarch)
 270             continue;
 271           a = pool->id2arch[a];
 272           /* a == 1 -> noarch */
 273           if (a != 1 && (a & 0xffff0000) != bestscore)
 274             continue;
 275           plist->elements[j++] = plist->elements[i];
 276         }
 277       plist->count = j;
 278       if (j == 0)
 279         return;
 280     }
 281
 282   prune_best_version_arch_sortcmp_data = pool;
 283   /* sort by name first */
 284   qsort(plist->elements, plist->count, sizeof(Id), prune_best_version_arch_sortcmp);
 285
 286   /* now find best 'per name' */
 287   for (i = j = 0; i < plist->count; i++)
 288     {
 289       s = pool->solvables + plist->elements[i];
 290
 291       if (pool->verbose) printf("- %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
 292
 293       if (!best)                       /* if no best yet, the current is best */
 294         {
 295           best = plist->elements[i];
 296           continue;
 297         }
 298
 299       /* name switch: re-init */
 300       if (pool->solvables[best].name != s->name)   /* new name */
 301         {
 302           if (pool->verbose) printf("BEST: %s-%s.%s\n", id2str(pool, pool->solvables[best].name), id2str(pool, pool->solvables[best].evr), id2str(pool, pool->solvables[best].arch));
 303           plist->elements[j++] = best; /* move old best to front */
 304           best = plist->elements[i];   /* take current as new best */
 305           continue;
 306         }
 307
 308       if (pool->solvables[best].evr != s->evr)   /* compare evr */
 309         {
 310           if (evrcmp(pool, pool->solvables[best].evr, s->evr) < 0)
 311             best = plist->elements[i];
 312         }
 313     }
 314
 315   if (best == ID_NULL)
 316     best = plist->elements[0];
 317
 318   /* XXX also check obsoletes! */
 319   if (pool->verbose) printf("BEST: %s-%s.%s\n", id2str(pool, pool->solvables[best].name), id2str(pool, pool->solvables[best].evr), id2str(pool, pool->solvables[best].arch));
 320
 321   plist->elements[j++] = best;
 322   plist->count = j;
 323
 324 }
 325
 326 /*-----------------------------------------------------------------*/
 327
 328 /*
 329  * print rules
 330  */
 331
 332 static void
 333 printruleelement(Solver *solv, Rule *r, Id v)
 334 {
 335   Pool *pool = solv->pool;
 336   Solvable *s;
 337   if (v < 0)
 338     {
 339       s = pool->solvables + -v;
 340       printf("    !%s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), -v);
 341     }
 342   else
 343     {
 344       s = pool->solvables + v;
 345       printf("    %s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), v);
 346     }
 347   if (r)
 348     {
 349       if (r->w1 == v)
 350         printf(" (w1)");
 351       if (r->w2 == v)
 352         printf(" (w2)");
 353     }
 354   if (solv->decisionmap[s - pool->solvables] > 0)
 355     printf(" I.%d", solv->decisionmap[s - pool->solvables]);
 356   if (solv->decisionmap[s - pool->solvables] < 0)
 357     printf(" C.%d", -solv->decisionmap[s - pool->solvables]);
 358   printf("\n");
 359 }
 360
 361
 362 /*
 363  * print rule
 364  */
 365
 366 static void
 367 printrule(Solver *solv, Rule *r)
 368 {
 369   int i;
 370   Id v;
 371
 372   if (r >= solv->rules && r < solv->rules + solv->nrules)   /* r is a solver rule */
 373     printf("Rule #%d:\n", (int)(r - solv->rules));
 374   else
 375     printf("Rule:\n");                 /* r is any rule */
 376   for (i = 0; ; i++)
 377     {
 378       if (i == 0)
 379         v = r->p;
 380       else if (r->d == ID_NULL)
 381         {
 382           if (i == 2)
 383             break;
 384           v = r->w2;
 385         }
 386       else
 387         v = solv->pool->whatprovidesdata[r->d + i - 1];
 388       if (v == ID_NULL)
 389         break;
 390       printruleelement(solv, r, v);
 391     }
 392   printf("    next: %d %d\n", r->n1, r->n2);
 393 }
 394
 395
 396 /*-----------------------------------------------------------------*/
 397
 398 /*
 399  * Rule handling
 400  */
 401
 402 static Pool *unifyrules_sortcmp_data;
 403
 404 /*
 405  * compare rules for unification sort
 406  */
 407
 408 static int
 409 unifyrules_sortcmp(const void *ap, const void *bp)
 410 {
 411   Pool *pool = unifyrules_sortcmp_data;
 412   Rule *a = (Rule *)ap;
 413   Rule *b = (Rule *)bp;
 414   Id *ad, *bd;
 415   int x;
 416
 417   x = a->p - b->p;
 418   if (x)
 419     return x;                          /* p differs */
 420
 421   /* identical p */
 422   if (a->d == 0 && b->d == 0)
 423     return a->w2 - b->w2;              /* assertion: return w2 diff */
 424
 425   if (a->d == 0)                       /* a is assertion, b not */
 426     {
 427       x = a->w2 - pool->whatprovidesdata[b->d];
 428       return x ? x : -1;
 429     }
 430
 431   if (b->d == 0)                       /* b is assertion, a not */
 432     {
 433       x = pool->whatprovidesdata[a->d] - b->w2;
 434       return x ? x : 1;
 435     }
 436
 437   /* compare whatprovidesdata */
 438   ad = pool->whatprovidesdata + a->d;
 439   bd = pool->whatprovidesdata + b->d;
 440   while (*bd)
 441     if ((x = *ad++ - *bd++) != 0)
 442       return x;
 443   return *ad;
 444 }
 445
 446
 447 /*
 448  * unify rules
 449  */
 450
 451 static void
 452 unifyrules(Solver *solv)
 453 {
 454   int i, j;
 455   Rule *ir, *jr;
 456
 457   if (solv->nrules <= 1)               /* nothing to unify */
 458     return;
 459
 460   /* sort rules first */
 461   unifyrules_sortcmp_data = solv->pool;
 462   qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
 463
 464   /* prune rules
 465    * i = unpruned
 466    * j = pruned
 467    */
 468   jr = 0;
 469   for (i = j = 1, ir = solv->rules + 1; i < solv->nrules; i++, ir++)
 470     {
 471       if (jr && !unifyrules_sortcmp(ir, jr))
 472         continue;                      /* prune! */
 473       jr = solv->rules + j++;          /* keep! */
 474       if (ir != jr)
 475         *jr = *ir;
 476     }
 477
 478   /* reduced count from nrules to j rules */
 479   if (solv->pool->verbose) printf("pruned rules from %d to %d\n", solv->nrules, j);
 480
 481   /* adapt rule buffer */
 482   solv->rules = (Rule *)xrealloc(solv->rules, ((solv->nrules + RULES_BLOCK) & ~RULES_BLOCK) * sizeof(Rule));
 483   solv->nrules = j;
 484 #if 1
 485   {
 486     int binr = 0;
 487     int dc = 0;
 488     Id *dp;
 489     Rule *r;
 490
 491     for (i = 1; i < solv->nrules; i++)
 492       {
 493         r = solv->rules + i;
 494         if (r->d == 0)                 /* assertion */
 495           {
 496             binr++;
 497             continue;
 498           }
 499         dp = solv->pool->whatprovidesdata + r->d;
 500         while (*dp++)
 501           dc++;
 502       }
 503     if (solv->pool->verbose)
 504       {
 505         printf("  binary: %d\n", binr);
 506         printf("  normal: %d\n", solv->nrules - 1 - binr);
 507         printf("  normal lits: %d\n", dc);
 508       }
 509   }
 510 #endif
 511 }
 512
 513 #if 0
 514
 515 /*
 516  * hash rule
 517  */
 518
 519 static Hashval
 520 hashrule(Solver *solv, Id p, Id d, int n)
 521 {
 522   unsigned int x = (unsigned int)p;
 523   int *dp;
 524
 525   if (n <= 1)
 526     return (x * 37) ^ (unsigned int)d;
 527   dp = solv->pool->whatprovidesdata + d;
 528   while (*dp)
 529     x = (x * 37) ^ (unsigned int)*dp++;
 530   return x;
 531 }
 532 #endif
 533
 534
 535 /*
 536  * add rule
 537  *  p = direct literal; > 0 for learnt, < 0 for installed pkg (rpm)
 538  *  d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
 539  *
 540  *
 541  * A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
 542  *
 543  * p < 0 : rule from rpm (installed pkg)
 544  * d > 0 : Offset in whatprovidesdata (list of providers)
 545  *
 546  * A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
 547  *  d < 0: Id of solvable (e.g. B1)
 548  *
 549  * d == 0: unary rule, assertion => (A) or (-A)
 550  *
 551  *   Install:    p > 0, d = 0   (A)             user requested install
 552  *   Remove:     p < 0, d = 0   (-A)            user requested remove
 553  *   Requires:   p < 0, d > 0   (-A|B1|B2|...)  d: <list of providers for requirement of p>
 554  *   Updates:    p > 0, d > 0   (A|B1|B2|...)   d: <list of updates for solvable p>
 555  *   Conflicts:  p < 0, d < 0   (-A|-B)         either p (conflict issuer) or d (conflict provider)
 556  *   ?           p > 0, d < 0   (A|-B)
 557  *   No-op ?:    p = 0, d = 0   (null)          (used as policy rule placeholder)
 558  */
 559
 560 static Rule *
 561 addrule(Solver *solv, Id p, Id d)
 562 {
 563   Rule *r = NULL;
 564   Id *dp = NULL;
 565
 566   int n = 0;                           /* number of literals in rule - 1
 567                                           0 = direct assertion (single literal)
 568                                           1 = binary rule
 569                                         */
 570
 571   /* it often happenes that requires lead to adding the same rpm rule
 572    * multiple times, so we prune those duplicates right away to make
 573    * the work for unifyrules a bit easier */
 574
 575   if (solv->nrules && !solv->jobrules)
 576     {
 577       r = solv->rules + solv->nrules - 1;   /* get the last added rule */
 578       if (r->p == p && r->d == d && d != 0)   /* identical and not user requested */
 579         return r;
 580     }
 581
 582   if (d < 0)
 583     {
 584       if (p == d)
 585         return NULL;                   /* ignore self conflict */
 586       n = 1;
 587     }
 588   else if (d == 0)                     /* user requested */
 589     n = 0;
 590   else
 591     {
 592       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, n++)
 593         if (*dp == -p)
 594           return NULL;  /* rule is self-fulfilling */
 595       if (n == 1)
 596         d = dp[-1];
 597     }
 598
 599   if (n == 0)                          /* direct assertion */
 600     {
 601       if (!solv->jobrules)
 602         {
 603           /* this is a rpm rule assertion, we do not have to allocate it */
 604           /* we can identify it by looking at the decision level, it will be 1 */
 605           if (p > 0)                       /*  */
 606             abort();
 607           if (solv->decisionmap[-p] > 0)   /*  */
 608             abort();
 609           if (solv->decisionmap[-p])       /*  */
 610             return NULL;
 611           queuepush(&solv->decisionq, p);
 612           queuepush(&solv->decisionq_why, 0);
 613           solv->decisionmap[-p] = -1;
 614
 615           return NULL;
 616         }
 617     }
 618   else if (n == 1 && p > d)
 619     {
 620       /* smallest literal first so we can find dups */
 621       n = p;
 622       p = d;
 623       d = n;
 624       n = 1;                           /* re-set n, was used as temp var */
 625     }
 626
 627   if (r
 628       && n == 1
 629       && r->p == p
 630       && r->w2 == d)
 631   {
 632     return r;
 633   }
 634
 635   if (r
 636       && r->d
 637       && n > 1
 638       && r->p == p)
 639     {
 640       Id *dp2 = solv->pool->whatprovidesdata + r->d;
 641       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, dp2++)
 642       {
 643         if (*dp != *dp2)
 644           break;
 645       }
 646       if (*dp == *dp2)
 647         return r;
 648    }
 649
 650   /*
 651    * allocate new rule
 652    */
 653
 654   /* check and extend rule buffer */
 655   if ((solv->nrules & RULES_BLOCK) == 0)
 656     {
 657       solv->rules = (Rule *)xrealloc(solv->rules, (solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
 658     }
 659
 660   r = solv->rules + solv->nrules++;    /* point to rule space */
 661
 662   r->p = p;
 663   if (n == 0)
 664     {
 665       /* direct assertion, no watch needed */
 666       r->d = 0;
 667       r->w1 = p;
 668       r->w2 = 0;
 669     }
 670   else if (n == 1)
 671     {
 672       /* binary rule */
 673       r->d = 0;
 674       r->w1 = p;
 675       r->w2 = d;
 676     }
 677   else
 678     {
 679       r->d = d;
 680       r->w1 = p;
 681       r->w2 = solv->pool->whatprovidesdata[d];
 682     }
 683   r->n1 = 0;
 684   r->n2 = 0;
 685
 686   /* we don't add the decision for learnt rules, as the code does that
 687    * right after calling addrule anyway */
 688   if (n == 0
 689       && p
 690       && !solv->learntrules)
 691     {
 692       /* must be system or job rule, as there are only negative unary rpm rules */
 693       Id vv = p > 0 ? p : -p;
 694       if (solv->decisionmap[vv])
 695         {
 696           int i;
 697           if (solv->decisionmap[vv] > 0 && p > 0)
 698             return r;
 699           if (solv->decisionmap[vv] < 0 && p < 0)
 700             return r;
 701           /* direct conflict! */
 702           for (i = 0; i < solv->decisionq.count; i++)
 703             if (solv->decisionq.elements[i] == -p)
 704               break;
 705           if (i == solv->decisionq.count)
 706             abort();
 707           if (solv->decisionq_why.elements[i] == 0)
 708             {
 709               /* conflict with rpm rule */
 710               queuepush(&solv->problems, r - solv->rules);
 711               queuepush(&solv->problems, 0);
 712               r->w1 = 0;        /* disable */
 713               return r;
 714             }
 715           /* conflict with other job or system rule */
 716           queuepush(&solv->problems, solv->decisionq_why.elements[i]);
 717           queuepush(&solv->problems, r - solv->rules);
 718           queuepush(&solv->problems, 0);
 719           r->w1 = 0;    /* disable */
 720           /* also disable conflicting rule */
 721           solv->rules[solv->decisionq_why.elements[i]].w1 = 0;
 722           /* XXX: remove from decisionq! */
 723 printf("XXX remove from decisionq\n");
 724           return r;
 725         }
 726       queuepush(&solv->decisionq, p);
 727       queuepush(&solv->decisionq_why, r - solv->rules);
 728       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? 1 : -1;
 729     }
 730   return r;
 731 }
 732
 733
 734 /*
 735  * add (install) rules for solvable
 736  *
 737  */
 738
 739 static void
 740 addrulesforsolvable(Solver *solv, Solvable *s, Map *m)
 741 {
 742   Pool *pool = solv->pool;
 743   Source *system = solv->system;
 744   Queue q;
 745   Id qbuf[64];
 746   int i;
 747   int dontfix;
 748   Id req, *reqp;
 749   Id con, *conp;
 750   Id obs, *obsp;
 751   Id rec, *recp;
 752   Id p, *pp;
 753   Id *dp;
 754   Id n;
 755
 756   queueinit_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
 757   queuepush(&q, s - pool->solvables);   /* push solvable Id */
 758
 759   while (q.count)
 760     {
 761       /*
 762        * n: Id of solvable
 763        * s: Pointer to solvable
 764        */
 765
 766       n = queueshift(&q);
 767       if (MAPTST(m, n))                /* continue if already done */
 768         continue;
 769
 770       MAPSET(m, n);
 771       s = pool->solvables + n;         /* s = Solvable in question */
 772
 773       dontfix = 0;
 774       if (system
 775           && !solv->fixsystem
 776           && n >= system->start        /* is it installed? */
 777           && n < system->start + system->nsolvables)
 778       {
 779         dontfix = 1;                   /* dont care about broken rpm deps */
 780       }
 781
 782       /*-----------------------------------------
 783        * check requires of s
 784        */
 785
 786       if ((reqp = s->requires) != ID_NULL)
 787         {
 788           while ((req = *reqp++) != ID_NULL)
 789             {
 790               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
 791                 continue;
 792
 793               dp = GET_PROVIDESP(req, p);      /* get providers of req */
 794
 795               if (!*dp                       /* dont care if noone provides rpmlib() */
 796                   && !strncmp(id2str(pool, req), "rpmlib(", 7))
 797                 {
 798                   continue;
 799                 }
 800
 801               if (dontfix)             /* dont care about breakage */
 802                 {
 803                   /* the strategy here is to not insist on dependencies
 804                    * that are already broken. so if we find one provider
 805                    * that was already installed, we know that the
 806                    * dependency was not broken before so we enforce it */
 807                   for (i = 0; dp[i]; i++)       /* for all providers */
 808                     {
 809                       if (dp[i] >= system->start && dp[i] < system->start + system->nsolvables)
 810                         break;         /* provider is installed */
 811                     }
 812                   if (!dp[i])          /* previously broken dependency */
 813                     {
 814                       if (pool->verbose) printf("ignoring broken requires %s of system package %s-%s.%s\n", dep2str(pool, req), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
 815                       continue;
 816                     }
 817                 }
 818
 819               if (!*dp)
 820                 {
 821                   /* nothing provides req! */
 822   #if 1
 823                   if (pool->verbose) printf("package %s-%s.%s [%d] is not installable (%s)\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), s - pool->solvables, dep2str(pool, req));
 824   #endif
 825                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
 826                   if (solv->rc_output)
 827                     printf(">!> !unflag %s-%s.%s[%s]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), source_name(pool_source(pool, s)));
 828                   continue;
 829                 }
 830   #if 0
 831               printf("addrule %s-%s.%s %s %d %d\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req), -n, dp - pool->whatprovidesdata);
 832               for (i = 0; dp[i]; i++)
 833                 printf("  %s-%s.%s\n", id2str(pool, pool->solvables[dp[i]].name), id2str(pool, pool->solvables[dp[i]].evr), id2str(pool, pool->solvables[dp[i]].arch));
 834   #endif
 835               /* add 'requires' dependency */
 836               /* rule: (-requestor|provider1|provider2|...|providerN) */
 837               addrule(solv, -n, dp - pool->whatprovidesdata);
 838
 839               /* descend the dependency tree */
 840               for (; *dp; dp++)   /* loop through all providers */
 841                 {
 842                   if (!MAPTST(m, *dp))
 843                     queuepush(&q, *dp);
 844                 }
 845
 846             } /* while, requirements of n */
 847
 848         } /* if, requirements */
 849
 850
 851       /*-----------------------------------------
 852        * check conflicts of s
 853        */
 854
 855       if ((conp = s->conflicts) != 0)
 856         {
 857           while ((con = *conp++) != 0)
 858             {
 859               FOR_PROVIDES(p, pp, con)
 860                 {
 861                    /* dontfix: dont care about conflicts with already installed packs */
 862                   if (dontfix && p >= system->start && p < system->start + system->nsolvables)
 863                     continue;
 864                  /* rule: -n|-p: either solvable _or_ provider of conflict */
 865                   addrule(solv, -n, -p);
 866                 }
 867             }
 868         }
 869
 870       /*-----------------------------------------
 871        * check obsoletes if not installed
 872        */
 873       if (!system || n < system->start || n >= (system->start + system->nsolvables))
 874         {                              /* not installed */
 875           if ((obsp = s->obsoletes) != 0)
 876             {
 877               while ((obs = *obsp++) != 0)
 878                 {
 879                   FOR_PROVIDES(p, pp, obs)
 880                     addrule(solv, -n, -p);
 881                 }
 882             }
 883           FOR_PROVIDES(p, pp, s->name)
 884             {
 885               if (s->name == pool->solvables[p].name)
 886                 addrule(solv, -n, -p);
 887             }
 888         }
 889
 890       /*-----------------------------------------
 891        * add recommends to the rule list
 892        */
 893       if ((recp = s->recommends) != 0)
 894         while ((rec = *recp++) != 0)
 895           {
 896             FOR_PROVIDES(p, pp, rec)
 897               if (!MAPTST(m, p))
 898                 queuepush(&q, p);
 899           }
 900     }
 901   queuefree(&q);
 902 }
 903
 904 static void
 905 addrulesforsupplements(Solver *solv, Map *m)
 906 {
 907   Pool *pool = solv->pool;
 908   Solvable *s;
 909   Id sup, *supp;
 910   int i, n;
 911
 912   if (pool->verbose) printf("addrulesforsupplements... (%d)\n", solv->nrules);
 913   for (i = n = 1; n < pool->nsolvables; i++, n++)
 914     {
 915       if (i == pool->nsolvables)
 916         i = 1;
 917       if (MAPTST(m, i))
 918         continue;
 919       s = pool->solvables + i;
 920       if (!pool_installable(pool, s))
 921         continue;
 922       sup = 0;
 923       if ((supp = s->supplements) != 0)
 924         while ((sup = *supp++) != ID_NULL)
 925           if (dep_possible(solv, sup, m))
 926             break;
 927       if (!sup && (supp = s->freshens) != 0)
 928         while ((sup = *supp++) != ID_NULL)
 929           if (dep_possible(solv, sup, m))
 930             break;
 931       if (!sup)
 932         continue;
 933       addrulesforsolvable(solv, s, m);
 934       n = 0;
 935     }
 936   if (pool->verbose) printf("done. (%d)\n", solv->nrules);
 937 }
 938
 939 static void
 940 addrulesforenhances(Solver *solv, Map *m)
 941 {
 942   Pool *pool = solv->pool;
 943   int i;
 944   Solvable *s;
 945   Id p, *pp, enh, *enhp, obs, *obsp, con, *conp;
 946
 947   if (pool->verbose) printf("addrulesforenhances... (%d)\n", solv->nrules);
 948   for (i = 1; i < pool->nsolvables; i++)
 949     {
 950       if (MAPTST(m, i))
 951         continue;
 952       s = pool->solvables + i;
 953       if ((enhp = s->enhances) == 0)
 954         continue;
 955       if (!pool_installable(pool, s))
 956         continue;
 957       while ((enh = *enhp++) != ID_NULL)
 958         if (dep_possible(solv, enh, m))
 959           break;
 960       if (!enh)
 961         continue;
 962       if ((conp = s->conflicts) != 0)
 963         while ((con = *conp++) != 0)
 964           FOR_PROVIDES(p, pp, con)
 965             addrule(solv, -i, -p);
 966       if ((obsp = s->obsoletes) != 0)
 967         while ((obs = *obsp++) != ID_NULL)
 968           FOR_PROVIDES(p, pp, obs)
 969             addrule(solv, -i, -p);
 970       FOR_PROVIDES(p, pp, s->name)
 971         if (s->name == pool->solvables[p].name)
 972           addrule(solv, -i, -p);
 973     }
 974 }
 975
 976
 977 static inline int
 978 archchanges(Pool *pool, Solvable *s1, Solvable *s2)
 979 {
 980   Id a1 = s1->arch, a2 = s2->arch;
 981
 982   /* we allow changes to/from noarch */
 983   if (a1 == a2 || a1 == ARCH_NOARCH || a2 == ARCH_NOARCH)
 984     return 0;
 985   if (!pool->id2arch)
 986     return 0;
 987   a1 = a1 <= pool->lastarch ? pool->id2arch[a1] : 0;
 988   a2 = a2 <= pool->lastarch ? pool->id2arch[a2] : 0;
 989   if (((a1 ^ a2) & 0xffff0000) != 0)
 990     return 1;
 991   return 0;
 992 }
 993
 994
 995 static void
 996 findupdatepackages(Solver *solv, Solvable *s, Queue *qs, Map *m, int allowdowngrade, int allowarchchange)
 997 {
 998   /* system packages get a special upgrade allowed rule */
 999   Pool *pool = solv->pool;
1000   Id p, *pp, n, p2, *pp2;
1001   Id obs, *obsp;
1002
1003   QUEUEEMPTY(qs);
1004   /*
1005    * s = solvable ptr
1006    * n = solvable Id
1007    */
1008   n = s - pool->solvables;
1009   if (m && !MAPTST(m, n))       /* add rule for s if not already done */
1010     addrulesforsolvable(solv, s, m);
1011
1012   /*
1013    * look for updates for s
1014    */
1015   FOR_PROVIDES(p, pp, s->name)  /* every provider of s' name */
1016     {
1017       if (p == n)               /* skip itself */
1018         continue;
1019
1020       if (s->name == pool->solvables[p].name)   /* name match */
1021         {
1022           if (!allowdowngrade                   /* consider downgrades ? */
1023               && evrcmp(pool, s->evr, pool->solvables[p].evr) > 0)
1024             continue;
1025           /* XXX */
1026           if (!allowarchchange && archchanges(pool, s, pool->solvables + p))
1027             continue;
1028         }
1029       else if (!solv->noupdateprovide && (obsp = pool->solvables[p].obsoletes) != 0)   /* provides/obsoletes combination ? */
1030         {
1031           while ((obs = *obsp++) != 0)  /* for all obsoletes */
1032             {
1033               FOR_PROVIDES(p2, pp2, obs)   /* and all matching providers of the obsoletes */
1034                 {
1035                   if (p2 == n)          /* match ! */
1036                     break;
1037                 }
1038               if (p2)                   /* match! */
1039                 break;
1040             }
1041           if (!obs)                     /* continue if no match */
1042             continue;
1043           /* here we have 'p' with a matching provides/obsoletes combination
1044            * thus flagging p as a valid update candidate for s
1045            */
1046         }
1047       else
1048         continue;
1049       queuepush(qs, p);
1050
1051       if (m && !MAPTST(m, p))           /* mark p for install if not already done */
1052         addrulesforsolvable(solv, pool->solvables + p, m);
1053     }
1054   if (solv->noupdateprovide && solv->obsoletes && solv->obsoletes[n - solv->system->start])
1055     {
1056       for (pp = solv->obsoletes_data + solv->obsoletes[n - solv->system->start]; (p = *pp++) != 0;)
1057         {
1058           queuepush(qs, p);
1059           if (m && !MAPTST(m, p))               /* mark p for install if not already done */
1060             addrulesforsolvable(solv, pool->solvables + p, m);
1061         }
1062     }
1063 }
1064
1065 /*
1066  * add rule for update
1067  *   (A|A1|A2|A3...)  An = update candidates for A
1068  *
1069  * s = (installed) solvable
1070  * m = 'addedmap', bit set if 'install' rule for solvable exists
1071  */
1072
1073 static void
1074 addupdaterule(Solver *solv, Solvable *s, Map *m, int allowdowngrade, int allowarchchange, int dontaddrule)
1075 {
1076   /* system packages get a special upgrade allowed rule */
1077   Pool *pool = solv->pool;
1078   Id p, d;
1079   Rule *r;
1080   Queue qs;
1081   Id qsbuf[64];
1082
1083   queueinit_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1084   findupdatepackages(solv, s, &qs, m, allowdowngrade, allowarchchange);
1085   p = s - pool->solvables;
1086   if (dontaddrule)      /* we consider update candidates but dont force them */
1087     {
1088       queuefree(&qs);
1089       return;
1090     }
1091
1092   if (qs.count == 0)                   /* no updates found */
1093     {
1094 #if 0
1095       printf("new update rule: must keep %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1096 #endif
1097       addrule(solv, p, 0);              /* request 'install' of s */
1098       queuefree(&qs);
1099       return;
1100     }
1101
1102   d = pool_queuetowhatprovides(pool, &qs);   /* intern computed provider queue */
1103   queuefree(&qs);
1104   r = addrule(solv, p, d);             /* allow update of s */
1105 #if 0
1106   printf("new update rule ");
1107   if (r)
1108     printrule(solv, r);
1109 #endif
1110 }
1111
1112
1113 /*-----------------------------------------------------------------*/
1114 /* watches */
1115
1116
1117 /*
1118  * makewatches
1119  *
1120  * initial setup for all watches
1121  */
1122
1123 static void
1124 makewatches(Solver *solv)
1125 {
1126   Rule *r;
1127   int i;
1128   int nsolvables = solv->pool->nsolvables;
1129
1130   xfree(solv->watches);
1131                                        /* lower half for removals, upper half for installs */
1132   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1133 #if 1
1134   /* do it reverse so rpm rules get triggered first */
1135   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1136 #else
1137   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1138 #endif
1139     {
1140       if (!r->w1                       /* rule is disabled */
1141           || !r->w2)                   /* rule is assertion */
1142         continue;
1143
1144       /* see addwatches(solv, r) */
1145       r->n1 = solv->watches[nsolvables + r->w1];
1146       solv->watches[nsolvables + r->w1] = r - solv->rules;
1147
1148       r->n2 = solv->watches[nsolvables + r->w2];
1149       solv->watches[nsolvables + r->w2] = r - solv->rules;
1150     }
1151 }
1152
1153
1154 /*
1155  * add watches (for rule)
1156  */
1157
1158 static void
1159 addwatches(Solver *solv, Rule *r)
1160 {
1161   int nsolvables = solv->pool->nsolvables;
1162
1163   r->n1 = solv->watches[nsolvables + r->w1];
1164   solv->watches[nsolvables + r->w1] = r - solv->rules;
1165
1166   r->n2 = solv->watches[nsolvables + r->w2];
1167   solv->watches[nsolvables + r->w2] = r - solv->rules;
1168 }
1169
1170
1171 /*-----------------------------------------------------------------*/
1172 /* rule propagation */
1173
1174 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1175
1176 /*
1177  * propagate
1178  *
1179  * propagate decision to all rules
1180  */
1181
1182 static Rule *
1183 propagate(Solver *solv, int level)
1184 {
1185   Pool *pool = solv->pool;
1186   Id *rp, *nrp;
1187   Rule *r;
1188   Id p, pkg, ow;
1189   Id *dp;
1190   Id *decisionmap = solv->decisionmap;
1191   Id *watches = solv->watches + pool->nsolvables;
1192
1193   while (solv->propagate_index < solv->decisionq.count)
1194     {
1195       /* negative because our watches trigger if literal goes FALSE */
1196       pkg = -solv->decisionq.elements[solv->propagate_index++];
1197 #if 0
1198   printf("popagate for decision %d level %d\n", -pkg, level);
1199   printruleelement(solv, 0, -pkg);
1200 #endif
1201       for (rp = watches + pkg; *rp; rp = nrp)
1202         {
1203           r = solv->rules + *rp;
1204 #if 0
1205   printf("  watch triggered ");
1206   printrule(solv, r);
1207 #endif
1208           if (pkg == r->w1)
1209             {
1210               ow = r->w2;
1211               nrp = &r->n1;
1212             }
1213           else
1214             {
1215               ow = r->w1;
1216               nrp = &r->n2;
1217             }
1218           /* if clause is TRUE, nothing to do */
1219           if (DECISIONMAP_TRUE(ow))
1220             continue;
1221
1222           if (r->d)
1223             {
1224               /* not a binary clause, check if we need to move our watch */
1225               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1226                 p = r->p;
1227               else
1228                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1229                   if (p != ow && !DECISIONMAP_TRUE(-p))
1230                     break;
1231               if (p)
1232                 {
1233                   /* p is free to watch, move watch to p */
1234 #if 0
1235                   if (p > 0)
1236                     printf("    -> move w%d to %s-%s.%s\n", (pkg == r->w1 ? 1 : 2), id2str(pool, pool->solvables[p].name), id2str(pool, pool->solvables[p].evr), id2str(pool, pool->solvables[p].arch));
1237                   else
1238                     printf("    -> move w%d to !%s-%s.%s\n", (pkg == r->w1 ? 1 : 2), id2str(pool, pool->solvables[-p].name), id2str(pool, pool->solvables[-p].evr), id2str(pool, pool->solvables[-p].arch));
1239 #endif
1240                   *rp = *nrp;
1241                   nrp = rp;
1242                   if (pkg == r->w1)
1243                     {
1244                       r->w1 = p;
1245                       r->n1 = watches[p];
1246                     }
1247                   else
1248                     {
1249                       r->w2 = p;
1250                       r->n2 = watches[p];
1251                     }
1252                   watches[p] = r - solv->rules;
1253                   continue;
1254                 }
1255             }
1256           /* unit clause found, set other watch to TRUE */
1257           if (DECISIONMAP_TRUE(-ow))
1258             return r;           /* eek, a conflict! */
1259 #if 0
1260           printf("unit ");
1261           printrule(solv, r);
1262 #endif
1263           if (ow > 0)
1264             decisionmap[ow] = level;
1265           else
1266             decisionmap[-ow] = -level;
1267           queuepush(&solv->decisionq, ow);
1268           queuepush(&solv->decisionq_why, r - solv->rules);
1269 #if 0
1270             {
1271               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1272               if (ow > 0)
1273                 printf("  -> decided to install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1274               else
1275                 printf("  -> decided to conflict %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1276             }
1277 #endif
1278         }
1279     }
1280   return 0;     /* all is well */
1281 }
1282
1283
1284 /*-----------------------------------------------------------------*/
1285 /* Analysis */
1286
1287 /*
1288  * analyze
1289  *   and learn
1290  */
1291
1292 static int
1293 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1294 {
1295   Pool *pool = solv->pool;
1296   Queue r;
1297   int rlevel = 1;
1298   Map seen;             /* global? */
1299   Id v, vv, *dp;
1300   int l, i, idx;
1301   int num = 0;
1302   int learnt_why = solv->learnt_pool.count;
1303   Id *decisionmap = solv->decisionmap;
1304
1305   queueinit(&r);
1306
1307   if (pool->verbose) printf("ANALYZE at %d ----------------------\n", level);
1308   mapinit(&seen, pool->nsolvables);
1309   idx = solv->decisionq.count;
1310   for (;;)
1311     {
1312       printrule(solv, c);
1313       queuepush(&solv->learnt_pool, c - solv->rules);
1314       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1315       for (i = -1; ; i++)
1316         {
1317           if (i == -1)
1318             v = c->p;
1319           else if (c->d == 0)
1320             v = i ? 0 : c->w2;
1321           else
1322             v = *dp++;
1323           if (v == 0)
1324             break;
1325           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1326               continue;
1327           vv = v > 0 ? v : -v;
1328           if (MAPTST(&seen, vv))
1329             continue;
1330           l = solv->decisionmap[vv];
1331           if (l < 0)
1332             l = -l;
1333           if (l == 1)
1334             {
1335 #if 0
1336               int j;
1337               for (j = 0; j < solv->decisionq.count; j++)
1338                 if (solv->decisionq.elements[j] == v)
1339                   break;
1340               if (j == solv->decisionq.count)
1341                 abort();
1342               queuepush(&rulq, -(j + 1));
1343 #endif
1344               continue;                 /* initial setting */
1345             }
1346           MAPSET(&seen, vv);
1347           if (l == level)
1348             num++;                      /* need to do this one as well */
1349           else
1350             {
1351               queuepush(&r, v);
1352 #if 0
1353   printf("PUSH %d ", v);
1354   printruleelement(solv, 0, v);
1355 #endif
1356               if (l > rlevel)
1357                 rlevel = l;
1358             }
1359         }
1360 #if 0
1361       printf("num = %d\n", num);
1362 #endif
1363       if (num <= 0)
1364         abort();
1365       for (;;)
1366         {
1367           v = solv->decisionq.elements[--idx];
1368           vv = v > 0 ? v : -v;
1369           if (MAPTST(&seen, vv))
1370             break;
1371         }
1372       c = solv->rules + solv->decisionq_why.elements[idx];
1373       MAPCLR(&seen, vv);
1374       if (--num == 0)
1375         break;
1376     }
1377   *pr = -v;
1378   if (r.count == 0)
1379     *dr = 0;
1380   else if (r.count == 1 && r.elements[0] < 0)
1381     *dr = r.elements[0];
1382   else
1383     *dr = pool_queuetowhatprovides(pool, &r);
1384   if (pool->verbose)
1385     {
1386       printf("learned rule for level %d (am %d)\n", rlevel, level);
1387       printruleelement(solv, 0, -v);
1388       for (i = 0; i < r.count; i++)
1389         {
1390           v = r.elements[i];
1391           printruleelement(solv, 0, v);
1392         }
1393     }
1394   mapfree(&seen);
1395   queuepush(&solv->learnt_pool, 0);
1396 #if 0
1397   for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1398     {
1399       printf("learnt_why ");
1400       printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1401     }
1402 #endif
1403   if (why)
1404     *why = learnt_why;
1405   return rlevel;
1406 }
1407
1408
1409 /*
1410  * reset_solver
1411  * reset the solver decisions to right after the rpm rules
1412  */
1413
1414 static void
1415 reset_solver(Solver *solv)
1416 {
1417   int i;
1418   Id v, vv;
1419   Rule *r;
1420
1421   /* delete all learnt rules */
1422   solv->nrules = solv->learntrules;
1423   QUEUEEMPTY(&solv->learnt_why);
1424   QUEUEEMPTY(&solv->learnt_pool);
1425
1426   /* redo all direct rpm rule decisions */
1427   /* we break at the first decision with a why attached, this is
1428    * either a job/system rule decision of a propagated decision */
1429   for (i = 0; i < solv->decisionq.count; i++)
1430     {
1431       v = solv->decisionq.elements[i];
1432       solv->decisionmap[v > 0 ? v : -v] = 0;
1433     }
1434   for (i = 0; i < solv->decisionq_why.count; i++)
1435     if (solv->decisionq_why.elements[i])
1436       break;
1437     else
1438       {
1439         v = solv->decisionq.elements[i];
1440         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1441       }
1442
1443   if (solv->pool->verbose)
1444     printf("decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1445
1446   solv->decisionq_why.count = i;
1447   solv->decisionq.count = i;
1448   solv->recommends_index = -1;
1449   solv->propagate_index = 0;
1450
1451   /* make direct decisions from enabled unary rules */
1452   for (i = solv->jobrules, r = solv->rules + solv->jobrules; i < solv->nrules; i++, r++)
1453     {
1454       if (!r->w1 || r->w2)
1455         continue;
1456 #if 0
1457       printrule(solv, r);
1458 #endif
1459       v = r->p;
1460       vv = v > 0 ? v : -v;
1461       if (solv->decisionmap[vv])
1462         {
1463           /* do not create conflicts */
1464           if (solv->decisionmap[vv] > 0 && v < 0)
1465             abort();
1466           if (solv->decisionmap[vv] < 0 && v > 0)
1467             abort();
1468         }
1469       queuepush(&solv->decisionq, v);
1470       queuepush(&solv->decisionq_why, r - solv->rules);
1471       solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1472     }
1473   if (solv->pool->verbose)
1474     printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
1475   /* recreate watches */
1476   makewatches(solv);
1477 }
1478
1479
1480 /*
1481  * analyze_unsolvable_rule
1482  */
1483
1484 static void
1485 analyze_unsolvable_rule(Solver *solv, Rule *c, int disablerules)
1486 {
1487   Id why;
1488   int i;
1489
1490   why = c - solv->rules;
1491 #if 0
1492   if (why >= solv->jobrules && why < solv->systemrules)
1493     printf("JOB ");
1494   if (why >= solv->systemrules && why < solv->learntrules)
1495     printf("SYSTEM %d ", why - solv->systemrules);
1496   if (solv->learntrules && why >= solv->learntrules)
1497     printf("LEARNED ");
1498   printrule(solv, c);
1499 #endif
1500   if (solv->learntrules && why >= solv->learntrules)
1501     {
1502       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1503         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], disablerules);
1504       return;
1505     }
1506   if (why >= solv->jobrules && why < solv->learntrules)
1507     {
1508       if (disablerules)
1509         {
1510           /* turn off rule for further analysis */
1511           c->w1 = 0;
1512         }
1513       /* unify problem */
1514       if (solv->problems.count)
1515         {
1516           for (i = solv->problems.count - 1; i >= 0; i--)
1517             if (solv->problems.elements[i] == 0)
1518               break;
1519             else if (solv->problems.elements[i] == why)
1520               return;
1521         }
1522       queuepush(&solv->problems, why);
1523     }
1524 }
1525
1526
1527 /*
1528  * analyze_unsolvable
1529  */
1530
1531 static void
1532 analyze_unsolvable(Solver *solv, Rule *c, int disablerules)
1533 {
1534   Pool *pool = solv->pool;
1535   Map seen;             /* global? */
1536   Id v, vv, *dp, why;
1537   int l, i, idx;
1538   Id *decisionmap = solv->decisionmap;
1539
1540 #if 0
1541   printf("ANALYZE UNSOLVABLE ----------------------\n");
1542 #endif
1543   mapinit(&seen, pool->nsolvables);
1544   analyze_unsolvable_rule(solv, c, disablerules);
1545   dp = c->d ? pool->whatprovidesdata + c->d : 0;
1546   for (i = -1; ; i++)
1547     {
1548       if (i == -1)
1549         v = c->p;
1550       else if (c->d == 0)
1551         v = i ? 0 : c->w2;
1552       else
1553         v = *dp++;
1554       if (v == 0)
1555         break;
1556       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1557           continue;
1558       vv = v > 0 ? v : -v;
1559       l = solv->decisionmap[vv];
1560       if (l < 0)
1561         l = -l;
1562       MAPSET(&seen, vv);
1563     }
1564   idx = solv->decisionq.count;
1565   while (idx > 0)
1566     {
1567       v = solv->decisionq.elements[--idx];
1568       vv = v > 0 ? v : -v;
1569       if (!MAPTST(&seen, vv))
1570         continue;
1571       why = solv->decisionq_why.elements[idx];
1572       if (!why)
1573         {
1574 #if 0
1575           printf("RPM ");
1576           printruleelement(solv, 0, v);
1577 #endif
1578           continue;
1579         }
1580       c = solv->rules + why;
1581       analyze_unsolvable_rule(solv, c, disablerules);
1582       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1583       for (i = -1; ; i++)
1584         {
1585           if (i == -1)
1586             v = c->p;
1587           else if (c->d == 0)
1588             v = i ? 0 : c->w2;
1589           else
1590             v = *dp++;
1591           if (v == 0)
1592             break;
1593           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1594               continue;
1595           vv = v > 0 ? v : -v;
1596           l = solv->decisionmap[vv];
1597           if (l < 0)
1598             l = -l;
1599           MAPSET(&seen, vv);
1600         }
1601     }
1602   mapfree(&seen);
1603   queuepush(&solv->problems, 0);        /* mark end of this problem */
1604   if (disablerules)
1605     reset_solver(solv);
1606 #if 0
1607   printf("analyze_unsolvables done\n");
1608 #endif
1609 }
1610
1611
1612 /*-----------------------------------------------------------------*/
1613 /* Decision revert */
1614
1615 /*
1616  * revert
1617  * revert decision at level
1618  */
1619
1620 static void
1621 revert(Solver *solv, int level)
1622 {
1623   Id v, vv;
1624   while (solv->decisionq.count)
1625     {
1626       v = solv->decisionq.elements[solv->decisionq.count - 1];
1627       vv = v > 0 ? v : -v;
1628       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1629         break;
1630 #if 0
1631       printf("reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1632 #endif
1633       solv->decisionmap[vv] = 0;
1634       solv->decisionq.count--;
1635       solv->decisionq_why.count--;
1636       solv->propagate_index = solv->decisionq.count;
1637     }
1638   solv->recommends_index = -1;
1639 }
1640
1641
1642 /*
1643  * watch2onhighest - put watch2 on literal with highest level
1644  */
1645
1646 static void
1647 watch2onhighest(Solver *solv, Rule *r)
1648 {
1649   int l, wl = 0;
1650   Id v, *dp;
1651
1652   if (!r->d)
1653     return;     /* binary rule, both watches are set */
1654   dp = solv->pool->whatprovidesdata + r->d;
1655   while ((v = *dp++) != 0)
1656     {
1657       l = solv->decisionmap[v < 0 ? -v : v];
1658       if (l < 0)
1659         l = -l;
1660       if (l > wl)
1661         {
1662           r->w2 = dp[-1];
1663           wl = l;
1664         }
1665     }
1666 }
1667
1668
1669 /*
1670  * setpropagatelearn
1671  */
1672
1673 static int
1674 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1675 {
1676   Rule *r;
1677   Id p, d;
1678   int l, why;
1679
1680   if (decision)
1681     {
1682       level++;
1683       if (decision > 0)
1684         solv->decisionmap[decision] = level;
1685       else
1686         solv->decisionmap[-decision] = -level;
1687       queuepush(&solv->decisionq, decision);
1688       queuepush(&solv->decisionq_why, 0);
1689     }
1690   for (;;)
1691     {
1692       r = propagate(solv, level);
1693       if (!r)
1694         break;
1695       if (level == 1)
1696         {
1697           analyze_unsolvable(solv, r, disablerules);
1698           if (disablerules)
1699             return 1;
1700           return 0;
1701         }
1702       printf("conflict with rule #%d\n", (int)(r - solv->rules));
1703       l = analyze(solv, level, r, &p, &d, &why);
1704       if (l >= level || l <= 0)
1705         abort();
1706       printf("reverting decisions (level %d -> %d)\n", level, l);
1707       level = l;
1708       revert(solv, level);
1709       r = addrule(solv, p, d);       /* p requires d */
1710       if (!r)
1711         abort();
1712       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1713         {
1714           printf("%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1715           abort();
1716         }
1717       queuepush(&solv->learnt_why, why);
1718       if (d)
1719         {
1720           /* at least 2 literals, needs watches */
1721           watch2onhighest(solv, r);
1722           addwatches(solv, r);
1723         }
1724       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1725       queuepush(&solv->decisionq, p);
1726       queuepush(&solv->decisionq_why, r - solv->rules);
1727       printf("decision: ");
1728       printruleelement(solv, 0, p);
1729       printf("new rule: ");
1730       printrule(solv, r);
1731     }
1732   return level;
1733 }
1734
1735 /*-----------------------------------------------------------------*/
1736 /* Main solver interface */
1737
1738
1739 /*
1740  * solver_create
1741  * create solver structure
1742  *
1743  * pool: all available solvables
1744  * system: installed Solvables
1745  *
1746  *
1747  * Upon solving, rules are created to flag the Solvables
1748  * of the 'system' Source as installed.
1749  */
1750
1751 Solver *
1752 solver_create(Pool *pool, Source *system)
1753 {
1754   Solver *solv;
1755   solv = (Solver *)xcalloc(1, sizeof(Solver));
1756   solv->pool = pool;
1757   solv->system = system;
1758   pool->verbose = 1;
1759
1760   queueinit(&solv->decisionq);
1761   queueinit(&solv->decisionq_why);
1762   queueinit(&solv->problems);
1763   queueinit(&solv->suggestions);
1764   queueinit(&solv->learnt_why);
1765   queueinit(&solv->learnt_pool);
1766
1767   mapinit(&solv->recommendsmap, pool->nsolvables);
1768   mapinit(&solv->suggestsmap, pool->nsolvables);
1769   solv->recommends_index = 0;
1770
1771   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1772   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1773   memset(solv->rules, 0, sizeof(Rule));
1774   solv->nrules = 1;
1775
1776   return solv;
1777 }
1778
1779
1780 /*
1781  * solver_free
1782  */
1783
1784 void
1785 solver_free(Solver *solv)
1786 {
1787   queuefree(&solv->decisionq);
1788   queuefree(&solv->decisionq_why);
1789   queuefree(&solv->learnt_why);
1790   queuefree(&solv->learnt_pool);
1791   queuefree(&solv->problems);
1792   queuefree(&solv->suggestions);
1793
1794   mapfree(&solv->recommendsmap);
1795   mapfree(&solv->suggestsmap);
1796   xfree(solv->decisionmap);
1797   xfree(solv->rules);
1798   xfree(solv->watches);
1799   xfree(solv->weaksystemrules);
1800   xfree(solv->obsoletes);
1801   xfree(solv->obsoletes_data);
1802   xfree(solv);
1803 }
1804
1805
1806 /*-------------------------------------------------------*/
1807
1808 /*
1809  * run_solver
1810  *
1811  * all rules have been set up, not actually run the solver
1812  *
1813  */
1814
1815 static void
1816 run_solver(Solver *solv, int disablerules, int doweak)
1817 {
1818   Queue dq;
1819   int systemlevel;
1820   int level, olevel;
1821   Rule *r;
1822   int i, n;
1823   Solvable *s;
1824   Pool *pool = solv->pool;
1825   Id p, *dp;
1826
1827 #if 0
1828   printf("number of rules: %d\n", solv->nrules);
1829 {
1830   int i;
1831   for (i = 0; i < solv->nrules; i++)
1832     {
1833       printrule(solv, solv->rules + i);
1834     }
1835 }
1836 #endif
1837
1838   /* all new rules are learnt after this point */
1839   solv->learntrules = solv->nrules;
1840   /* crate watches lists */
1841   makewatches(solv);
1842
1843   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
1844
1845   /* start SAT algorithm */
1846   level = 1;
1847   systemlevel = level + 1;
1848   if (pool->verbose) printf("solving...\n");
1849
1850   queueinit(&dq);
1851   for (;;)
1852     {
1853       /*
1854        * propagate
1855        */
1856
1857       if (level == 1)
1858         {
1859           if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
1860           if ((r = propagate(solv, level)) != 0)
1861             {
1862               analyze_unsolvable(solv, r, disablerules);
1863               if (disablerules)
1864                 continue;
1865               printf("UNSOLVABLE\n");
1866               queuefree(&dq);
1867               return;
1868             }
1869         }
1870
1871       /*
1872        * system packages
1873        */
1874
1875       if (level < systemlevel && solv->system->nsolvables)
1876         {
1877           if (!solv->updatesystem)
1878             {
1879               /* try to keep as many packages as possible */
1880               if (pool->verbose) printf("installing system packages\n");
1881               for (i = solv->system->start, n = 0; ; i++, n++)
1882                 {
1883                   if (n == solv->system->nsolvables)
1884                     break;
1885                   if (i == solv->system->start + solv->system->nsolvables)
1886                     i = solv->system->start;
1887                   s = pool->solvables + i;
1888                   if (solv->decisionmap[i] != 0)
1889                     continue;
1890 #if 0
1891                   printf("system installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1892 #endif
1893                   olevel = level;
1894                   level = setpropagatelearn(solv, level, i, disablerules);
1895                   if (level == 0)
1896                     {
1897                       printf("UNSOLVABLE\n");
1898                       queuefree(&dq);
1899                       return;
1900                     }
1901                   if (level <= olevel)
1902                     n = 0;
1903                 }
1904             }
1905           if (solv->weaksystemrules)
1906             {
1907               if (pool->verbose) printf("installing weak system packages\n");
1908               for (i = solv->system->start, n = 0; ; i++, n++)
1909                 {
1910                   if (n == solv->system->nsolvables)
1911                     break;
1912                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->system->start] == 0))
1913                     continue;
1914                   QUEUEEMPTY(&dq);
1915                   if (solv->decisionmap[i] == 0)
1916                     queuepush(&dq, i);
1917                   if (solv->weaksystemrules[i - solv->system->start])
1918                     {
1919                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->system->start];
1920                       while ((p = *dp++) != 0)
1921                         {
1922                           if (solv->decisionmap[p] > 0)
1923                             break;
1924                           if (solv->decisionmap[p] == 0)
1925                             queuepush(&dq, p);
1926                         }
1927                       if (p)
1928                         continue;       /* rule is already true */
1929                     }
1930                   if (!dq.count)
1931                     continue;
1932
1933                   if (dq.count > 1)
1934                     prune_to_recommended(solv, &dq);
1935                   if (dq.count > 1)
1936                     prune_best_version_arch(pool, &dq);
1937 #if 0
1938                   s = pool->solvables + dq.elements[0];
1939                   printf("weak system installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1940 #endif
1941                   olevel = level;
1942                   level = setpropagatelearn(solv, level, dq.elements[0], disablerules);
1943                   if (level == 0)
1944                     {
1945                       printf("UNSOLVABLE\n");
1946                       queuefree(&dq);
1947                       return;
1948                     }
1949                   if (level <= olevel)
1950                     {
1951                       n = 0;
1952                       break;
1953                     }
1954                 }
1955               if (n != solv->system->nsolvables)
1956                 continue;
1957             }
1958           systemlevel = level;
1959         }
1960
1961       /*
1962        * decide
1963        */
1964
1965       if (pool->verbose) printf("deciding unresolved rules\n");
1966       for (i = 1, n = 1; ; i++, n++)
1967         {
1968           if (n == solv->nrules)
1969             break;
1970           if (i == solv->nrules)
1971             i = 1;
1972           r = solv->rules + i;
1973           if (!r->w1)
1974             continue;
1975           QUEUEEMPTY(&dq);
1976           if (r->d == 0)
1977             {
1978               /* binary or unary rule */
1979               /* need two positive undecided literals */
1980               if (r->p < 0 || r->w2 <= 0)
1981                 continue;
1982               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
1983                 continue;
1984               queuepush(&dq, r->p);
1985               queuepush(&dq, r->w2);
1986             }
1987           else
1988             {
1989               /* make sure that
1990                * all negative literals are installed
1991                * no positive literal is installed
1992                * i.e. the rule is not fulfilled and we
1993                * just need to decide on the positive literals
1994                */
1995               if (r->p < 0)
1996                 {
1997                   if (solv->decisionmap[-r->p] <= 0)
1998                     continue;
1999                 }
2000               else
2001                 {
2002                   if (solv->decisionmap[r->p] > 0)
2003                     continue;
2004                   if (solv->decisionmap[r->p] == 0)
2005                     queuepush(&dq, r->p);
2006                 }
2007               dp = pool->whatprovidesdata + r->d;
2008               while ((p = *dp++) != 0)
2009                 {
2010                   if (p < 0)
2011                     {
2012                       if (solv->decisionmap[-p] <= 0)
2013                         break;
2014                     }
2015                   else
2016                     {
2017                       if (solv->decisionmap[p] > 0)
2018                         break;
2019                       if (solv->decisionmap[p] == 0)
2020                         queuepush(&dq, p);
2021                     }
2022                 }
2023               if (p)
2024                 continue;
2025             }
2026           if (dq.count < 2)
2027             {
2028               /* cannot happen as this means that
2029                * the rule is unit */
2030               printrule(solv, r);
2031               abort();
2032             }
2033           prune_to_recommended(solv, &dq);
2034           if (dq.count > 1)
2035             prune_best_version_arch(pool, &dq);
2036           p = dq.elements[dq.count - 1];
2037           s = pool->solvables + p;
2038 #if 0
2039           printf("installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2040 #endif
2041           olevel = level;
2042           level = setpropagatelearn(solv, level, p, disablerules);
2043           if (level == 0)
2044             {
2045               printf("UNSOLVABLE\n");
2046               queuefree(&dq);
2047               return;
2048             }
2049           if (level < systemlevel)
2050             break;
2051           n = 0;
2052         } /* for(), decide */
2053
2054       if (n != solv->nrules)    /* continue if level < systemlevel */
2055         continue;
2056
2057       if (doweak && !solv->problems.count)
2058         {
2059           int qcount;
2060
2061           if (pool->verbose) printf("installing recommended packages\n");
2062           QUEUEEMPTY(&dq);
2063           for (i = 1; i < pool->nsolvables; i++)
2064             {
2065               if (solv->decisionmap[i] < 0)
2066                 continue;
2067               if (solv->decisionmap[i] > 0)
2068                 {
2069                   Id *recp, rec, *pp, p;
2070                   s = pool->solvables + i;
2071                   /* installed, check for recommends */
2072                   /* XXX need to special case AND ? */
2073                   if ((recp = s->recommends) != 0)
2074                     {
2075                       while ((rec = *recp++) != 0)
2076                         {
2077                           qcount = dq.count;
2078                           FOR_PROVIDES(p, pp, rec)
2079                             {
2080                               if (solv->decisionmap[p] > 0)
2081                                 {
2082                                   dq.count = qcount;
2083                                   break;
2084                                 }
2085                               else if (solv->decisionmap[p] == 0)
2086                                 queuepushunique(&dq, p);
2087                             }
2088                         }
2089                     }
2090                 }
2091               else
2092                 {
2093                   Id *supp, sup;
2094                   s = pool->solvables + i;
2095                   if (!s->supplements && !s->freshens)
2096                     continue;
2097                   if (!pool_installable(pool, s))
2098                     continue;
2099                   if ((supp = s->supplements) != 0)
2100                     {
2101                       while ((sup = *supp++) != 0)
2102                         if (dep_fulfilled(solv, sup))
2103                           break;
2104                       if (!sup)
2105                         continue;
2106                     }
2107                   if ((supp = s->freshens) != 0)
2108                     {
2109                       while ((sup = *supp++) != 0)
2110                         if (dep_fulfilled(solv, sup))
2111                           break;
2112                       if (!sup)
2113                         continue;
2114                     }
2115                   queuepushunique(&dq, i);
2116                 }
2117             }
2118           if (dq.count)
2119             {
2120               prune_best_version_arch(pool, &dq);
2121               p = dq.elements[dq.count - 1];
2122               s = pool->solvables + p;
2123 #if 1
2124               printf("installing recommended %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2125 #endif
2126               level = setpropagatelearn(solv, level, p, 0);
2127               continue;
2128             }
2129         }
2130       break;
2131     }
2132   queuefree(&dq);
2133 }
2134
2135
2136 /*
2137  * refine_suggestion
2138  */
2139
2140 static void
2141 refine_suggestion(Solver *solv, Id *problem, Id sug, Queue *refined)
2142 {
2143   Rule *r;
2144   int i, j;
2145   Id v;
2146   Queue disabled;
2147   int disabledcnt;
2148
2149   printf("refine_suggestion start\n");
2150   queueinit(&disabled);
2151   QUEUEEMPTY(refined);
2152   queuepush(refined, sug);
2153
2154   /* re-enable all rules but rule "sug" of the problem */
2155   revert(solv, 1);
2156   reset_solver(solv);
2157   for (i = 0; problem[i]; i++)
2158     {
2159       if (problem[i] == sug)
2160         continue;
2161       r = solv->rules + problem[i];
2162 #if 0
2163       printf("enable ");
2164       printrule(solv, r);
2165 #endif
2166       if (r->w2 == 0)
2167         {
2168           /* direct assertion */
2169           v = r->p > 0 ? r->p : -r->p;
2170           if (solv->decisionmap[v])
2171             {
2172               if ((solv->decisionmap[v] > 0 && r->p < 0) ||
2173                   (solv->decisionmap[v] < 0 && r->p > 0))
2174                 {
2175                   printf("direct assertion failure, no solution found!\n");
2176                   while (--i >= 0)
2177                     {
2178                       r = solv->rules + problem[i];
2179                       r->w1 = 0;
2180                     }
2181                   return;
2182                 }
2183             }
2184         }
2185       if (r->d == 0 || r->w2 != r->p)
2186         r->w1 = r->p;
2187       else
2188         r->w1 = solv->pool->whatprovidesdata[r->d];
2189     }
2190   reset_solver(solv);
2191   for (;;)
2192     {
2193       QUEUEEMPTY(&solv->problems);
2194       run_solver(solv, 0, 0);
2195       if (!solv->problems.count)
2196         {
2197           printf("no more problems!\n");
2198 #if 0
2199           printdecisions(solv);
2200 #endif
2201           break;                /* great, no more problems */
2202         }
2203       disabledcnt = disabled.count;
2204       for (i = 0; i < solv->problems.elements[i]; i++)
2205         {
2206           /* ignore solutions in refined */
2207           v = solv->problems.elements[i];
2208           for (j = 0; problem[j]; j++)
2209             if (problem[j] != sug && problem[j] == v)
2210               break;
2211           if (problem[j])
2212             continue;
2213           queuepush(&disabled, v);
2214           queuepush(&disabled, 0);      /* room for watch */
2215         }
2216       if (disabled.count == disabledcnt)
2217         {
2218           /* no solution found, this was an invalid suggestion! */
2219           printf("no solution found!\n");
2220           refined->count = 0;
2221           break;
2222         }
2223       if (disabled.count == disabledcnt + 2)
2224         {
2225           /* just one solution, add it to refined list */
2226           queuepush(refined, disabled.elements[disabledcnt]);
2227         }
2228       else
2229         {
2230           printf("##############################################   more than one solution found.\n");
2231 #if 1
2232           for (i = 0; i < solv->problems.elements[i]; i++)
2233             {
2234               printrule(solv, solv->rules + solv->problems.elements[i]);
2235             }
2236           printf("##############################################\n");
2237 #endif
2238           /* more than one solution */
2239           /* for now return */
2240         }
2241       for (i = disabledcnt; i < disabled.count; i += 2)
2242         {
2243           /* disable it */
2244           r = solv->rules + disabled.elements[i];
2245           disabled.elements[i + 1] = r->w1;
2246           r->w1 = 0;
2247 #if 0
2248           printf("disable ");
2249           printrule(solv, r);
2250 #endif
2251         }
2252       revert(solv, 1);          /* XXX move to reset_solver? */
2253       reset_solver(solv);
2254     }
2255   /* enable refined rules again */
2256   for (i = 0; i < disabled.count; i += 2)
2257     {
2258       r = solv->rules + disabled.elements[i];
2259       r->w1 = disabled.elements[i + 1];
2260     }
2261   /* disable problem rules again so that we are in the same state as before */
2262   for (i = 0; problem[i]; i++)
2263     {
2264       r = solv->rules + problem[i];
2265       r->w1 = 0;
2266     }
2267   printf("refine_suggestion end\n");
2268 }
2269
2270
2271 /*
2272  * printdecisions
2273  */
2274
2275 static const char *
2276 id2rc(Solver *solv, Id id)
2277 {
2278   const char *evr;
2279   if (solv->rc_output != 2)
2280     return "";
2281   evr = id2str(solv->pool, id);
2282   if (*evr < '0' || *evr > '9')
2283     return "0:";
2284   while (*evr >= '0' && *evr <= '9')
2285     evr++;
2286   if (*evr != ':')
2287     return "0:";
2288   return "";
2289 }
2290
2291 void
2292 printdecisions(Solver *solv)
2293 {
2294   Pool *pool = solv->pool;
2295   Id p, *obsoletesmap;
2296   int i;
2297   Solvable *s;
2298
2299   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2300   for (i = 0; i < solv->decisionq.count; i++)
2301     {
2302       Id obs, *obsp;
2303       Id *pp, n;
2304
2305       n = solv->decisionq.elements[i];
2306       if (n < 0)
2307         continue;
2308       if (n >= solv->system->start && n < solv->system->start + solv->system->nsolvables)
2309         continue;
2310       s = pool->solvables + n;
2311       if ((obsp = s->obsoletes) != 0)
2312         while ((obs = *obsp++) != 0)
2313           FOR_PROVIDES(p, pp, obs)
2314             {
2315               if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2316                 {
2317                   obsoletesmap[p] = n;
2318                   obsoletesmap[n]++;
2319                 }
2320             }
2321       FOR_PROVIDES(p, pp, s->name)
2322         if (s->name == pool->solvables[p].name)
2323           {
2324             if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2325               {
2326                 obsoletesmap[p] = n;
2327                 obsoletesmap[n]++;
2328               }
2329           }
2330     }
2331
2332   if (solv->rc_output)
2333     printf(">!> Solution #1:\n");
2334
2335   int installs = 0, uninstalls = 0, upgrades = 0;
2336
2337   /* print solvables to be erased */
2338
2339   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2340     {
2341       if (solv->decisionmap[i] > 0)
2342         continue;
2343       if (obsoletesmap[i])
2344         continue;
2345       s = pool->solvables + i;
2346       if (solv->rc_output == 2)
2347         printf(">!> remove  %s-%s%s\n", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2348       else if (solv->rc_output)
2349         printf(">!> remove  %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2350       else
2351         printf("erase   %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2352       uninstalls++;
2353     }
2354
2355   /* print solvables to be installed */
2356
2357   for (i = 0; i < solv->decisionq.count; i++)
2358     {
2359       int j;
2360       p = solv->decisionq.elements[i];
2361       if (p < 0)
2362         continue;
2363       if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2364         continue;
2365       s = pool->solvables + p;
2366
2367       if (!obsoletesmap[p])
2368         {
2369           if (solv->rc_output)
2370             printf(">!> ");
2371           printf("install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2372           if (solv->rc_output != 2)
2373             printf(".%s", id2str(pool, s->arch));
2374           installs++;
2375         }
2376       else if (!solv->rc_output)
2377         {
2378           printf("update  %s-%s.%s  (obsoletes", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2379           for (j = solv->system->start; j < solv->system->start + solv->system->nsolvables; j++)
2380             {
2381               if (obsoletesmap[j] != p)
2382                 continue;
2383               s = pool->solvables + j;
2384               printf(" %s-%s.%s", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2385             }
2386           printf(")");
2387           upgrades++;
2388         }
2389       else
2390         {
2391           Solvable *f, *fn = 0;
2392           for (j = solv->system->start; j < solv->system->start + solv->system->nsolvables; j++)
2393             {
2394               if (obsoletesmap[j] != p)
2395                 continue;
2396               f = pool->solvables + j;
2397               if (fn || f->name != s->name)
2398                 {
2399                   if (solv->rc_output == 2)
2400                     printf(">!> remove  %s-%s%s\n", id2str(pool, f->name), id2rc(solv, f->evr), id2str(pool, f->evr));
2401                   else if (solv->rc_output)
2402                     printf(">!> remove  %s-%s.%s\n", id2str(pool, f->name), id2str(pool, f->evr), id2str(pool, f->arch));
2403                   uninstalls++;
2404                 }
2405               else
2406                 fn = f;
2407             }
2408           if (!fn)
2409             {
2410               printf(">!> install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2411               if (solv->rc_output != 2)
2412                 printf(".%s", id2str(pool, s->arch));
2413               installs++;
2414             }
2415           else
2416             {
2417               if (solv->rc_output == 2)
2418                 printf(">!> upgrade %s-%s => %s-%s%s", id2str(pool, fn->name), id2str(pool, fn->evr), id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2419               else
2420                 printf(">!> upgrade %s-%s.%s => %s-%s.%s", id2str(pool, fn->name), id2str(pool, fn->evr), id2str(pool, fn->arch), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2421               upgrades++;
2422             }
2423         }
2424       if (solv->rc_output)
2425         {
2426           Source *source = pool_source(pool, s);
2427           if (source && strcmp(source_name(source), "locales"))
2428             printf("[%s]", source_name(source));
2429         }
2430       printf("\n");
2431     }
2432
2433   if (solv->rc_output)
2434     printf(">!> installs=%d, upgrades=%d, uninstalls=%d\n", installs, upgrades, uninstalls);
2435
2436   xfree(obsoletesmap);
2437 }
2438
2439 static void
2440 create_obsolete_index(Solver *solv)
2441 {
2442   Pool *pool = solv->pool;
2443   Solvable *s;
2444   Source *system = solv->system;
2445   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
2446   int i, n;
2447
2448   /* create reverse obsoletes map for system solvables */
2449   solv->obsoletes = obsoletes = xcalloc(system->nsolvables, sizeof(Id));
2450   for (i = 1; i < pool->nsolvables; i++)
2451     {
2452       s = pool->solvables + i;
2453       if ((obsp = s->obsoletes) == 0)
2454         continue;
2455       if (!pool_installable(pool, s))
2456         continue;
2457       while ((obs = *obsp++) != 0)
2458         FOR_PROVIDES(p, pp, obs)
2459           {
2460             if (p < system->start || p >= system->start + system->nsolvables)
2461               continue;
2462             if (pool->solvables[p].name == s->name)
2463               continue;
2464             obsoletes[p - system->start]++;
2465           }
2466     }
2467   n = 0;
2468   for (i = 0; i < system->nsolvables; i++)
2469     if (obsoletes[i])
2470       {
2471         n += obsoletes[i] + 1;
2472         obsoletes[i] = n;
2473       }
2474   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
2475   if (pool->verbose) printf("obsoletes data: %d entries\n", n + 1);
2476   for (i = pool->nsolvables - 1; i > 0; i--)
2477     {
2478       s = pool->solvables + i;
2479       if ((obsp = s->obsoletes) == 0)
2480         continue;
2481       if (!pool_installable(pool, s))
2482         continue;
2483       while ((obs = *obsp++) != 0)
2484         FOR_PROVIDES(p, pp, obs)
2485           {
2486             if (p < system->start || p >= system->start + system->nsolvables)
2487               continue;
2488             if (pool->solvables[p].name == s->name)
2489               continue;
2490             p -= system->start;
2491             if (obsoletes_data[obsoletes[p]] != i)
2492               obsoletes_data[--obsoletes[p]] = i;
2493           }
2494     }
2495 }
2496
2497 /*-----------------------------------------------------------------*/
2498 /* main() */
2499
2500 /*
2501  *
2502  * solve job queue
2503  *
2504  */
2505
2506 void
2507 solve(Solver *solv, Queue *job)
2508 {
2509   Pool *pool = solv->pool;
2510   int i;
2511   Map addedmap;                        /* '1' == have rule for solvable */
2512   Map noupdaterule;                    /* '1' == don't update (scheduled for removal) */
2513   Id how, what, p, *pp, d;
2514   Queue q;
2515   Rule *r;
2516   Solvable *s;
2517
2518   /*
2519    * create basic rule set of all involved packages
2520    * as bitmaps
2521    *
2522    */
2523
2524   mapinit(&addedmap, pool->nsolvables);
2525   mapinit(&noupdaterule, pool->nsolvables);
2526
2527   queueinit(&q);
2528
2529   /*
2530    * create rules for installed solvables -> keep them installed
2531    * so called: rpm rules
2532    *
2533    */
2534
2535   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2536     addrulesforsolvable(solv, pool->solvables + i, &addedmap);
2537
2538   /*
2539    * create install rules
2540    *
2541    * two passes, as we want to keep the rpm rules distinct from the job rules
2542    *
2543    */
2544
2545   if (solv->noupdateprovide && solv->system->nsolvables)
2546     create_obsolete_index(solv);
2547
2548   /*
2549    * solvable rules
2550    *  process job rules for solvables
2551    */
2552
2553   for (i = 0; i < job->count; i += 2)
2554     {
2555       how = job->elements[i];
2556       what = job->elements[i + 1];
2557
2558       switch(how)
2559         {
2560         case SOLVER_INSTALL_SOLVABLE:
2561           addrulesforsolvable(solv, pool->solvables + what, &addedmap);
2562           break;
2563         case SOLVER_INSTALL_SOLVABLE_NAME:
2564         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2565           QUEUEEMPTY(&q);
2566           FOR_PROVIDES(p, pp, what)
2567             {
2568                                        /* if by name, ensure that the name matches */
2569               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
2570                 continue;
2571               addrulesforsolvable(solv, pool->solvables + p, &addedmap);
2572             }
2573           break;
2574         case SOLVER_INSTALL_SOLVABLE_UPDATE:
2575           /* dont allow downgrade */
2576           addupdaterule(solv, pool->solvables + what, &addedmap, 0, 0, 1);
2577           break;
2578         }
2579     }
2580
2581   /*
2582    * if unstalls are disallowed, add update rules for every
2583    * installed solvables in the hope to circumvent uninstall
2584    * by upgrading
2585    *
2586    */
2587
2588 #if 0
2589   if (!solv->allowuninstall)
2590     {
2591       /* add update rule for every installed package */
2592       for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2593         addupdaterule(solv, pool->solvables + i, &addedmap, solv->allowdowngrade, solv->allowarchchange, 1);
2594     }
2595 #else  /* this is just to add the needed rpm rules to our set */
2596   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2597     addupdaterule(solv, pool->solvables + i, &addedmap, 1, 1, 1);
2598 #endif
2599
2600   addrulesforsupplements(solv, &addedmap);
2601   addrulesforenhances(solv, &addedmap);         /* do this last */
2602 #if 1
2603   if (pool->verbose)
2604     {
2605       int possible = 0, installable = 0;
2606       for (i = 1; i < pool->nsolvables; i++)
2607         {
2608           if (pool_installable(pool, pool->solvables + i))
2609             installable++;
2610           if (MAPTST(&addedmap, i))
2611             possible++;
2612         }
2613       printf("%d of %d installable solvables used for solving\n", possible, installable);
2614     }
2615 #endif
2616
2617   /*
2618    * first pass done
2619    *
2620    * unify existing rules before going over all job rules
2621    *
2622    */
2623
2624   unifyrules(solv);     /* remove duplicate rpm rules */
2625
2626   /*
2627    * at this point the system is always solvable,
2628    * as an empty system (remove all packages) is a valid solution
2629    */
2630   if (pool->verbose) printf("decisions based on rpms: %d\n", solv->decisionq.count);
2631
2632   /*
2633    * now add all job rules
2634    */
2635
2636   solv->jobrules = solv->nrules;
2637
2638   for (i = 0; i < job->count; i += 2)
2639     {
2640       how = job->elements[i];
2641       what = job->elements[i + 1];
2642       switch(how)
2643         {
2644         case SOLVER_INSTALL_SOLVABLE:                     /* install specific solvable */
2645           if (solv->rc_output) {
2646             Solvable *s = pool->solvables + what;
2647             printf(">!> Installing %s from channel %s\n", id2str(pool, s->name), source_name(pool_source(pool, s)));
2648           }
2649           addrule(solv, what, 0);                         /* install by Id */
2650           break;
2651         case SOLVER_ERASE_SOLVABLE:
2652           addrule(solv, -what, 0);                        /* remove by Id */
2653           MAPSET(&noupdaterule, what);
2654           break;
2655         case SOLVER_INSTALL_SOLVABLE_NAME:                /* install by capability */
2656         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2657           QUEUEEMPTY(&q);
2658           FOR_PROVIDES(p, pp, what)    /* check all providers */
2659             {
2660                                        /* if by name, ensure that the name matches */
2661               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
2662                 continue;
2663               queuepush(&q, p);
2664             }
2665           if (!q.count) {              /* no provider found -> abort */
2666             fprintf(stderr, "Nothing provides '%s'\n", id2str(pool, what));
2667             /* XXX make this a problem! */
2668             return;
2669             abort();
2670           }
2671
2672           p = queueshift(&q);          /* get first provider */
2673           if (!q.count)
2674             d = 0;                     /* single provider ? -> make assertion */
2675           else
2676             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
2677           addrule(solv, p, d);         /* add 'requires' rule */
2678           break;
2679         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
2680         case SOLVER_ERASE_SOLVABLE_PROVIDES:
2681           FOR_PROVIDES(p, pp, what)
2682             {
2683                                        /* if by name, ensure that the name matches */
2684               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
2685                 continue;
2686
2687               addrule(solv, -p, 0);  /* add 'remove' rule */
2688               MAPSET(&noupdaterule, p);
2689             }
2690           break;
2691         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
2692           addupdaterule(solv, pool->solvables + what, &addedmap, 0, 0, 0);
2693           break;
2694         }
2695     }
2696
2697   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
2698
2699   /*
2700    * now add policy rules
2701    *
2702    */
2703
2704   solv->systemrules = solv->nrules;
2705
2706   /*
2707    * create rules for updating installed solvables
2708    *
2709    * (Again ?)
2710    *
2711    */
2712
2713   if (!solv->allowuninstall)
2714     {                                  /* loop over all installed solvables */
2715       for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2716       {
2717         if (!MAPTST(&noupdaterule, i)) /* if not marked as 'noupdate' */
2718           addupdaterule(solv, pool->solvables + i, &addedmap, solv->allowdowngrade, solv->allowarchchange, 0);
2719         else
2720           addrule(solv, 0, 0);          /* place holder */
2721       }
2722       /* consistency check: we added a rule for _every_ system solvable */
2723       if (solv->nrules - solv->systemrules != solv->system->nsolvables)
2724         abort();
2725     }
2726
2727   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
2728
2729   /* create special weak system rules */
2730   if (solv->system->nsolvables)
2731     {
2732       solv->weaksystemrules = xcalloc(solv->system->nsolvables, sizeof(Id));
2733       for (i = 0; i < solv->system->nsolvables; i++)
2734         {
2735           findupdatepackages(solv, pool->solvables + solv->system->start + i, &q, (Map *)0, 1, 1);
2736           if (q.count)
2737             solv->weaksystemrules[i] = pool_queuetowhatprovides(pool, &q);
2738         }
2739     }
2740
2741   /* free unneeded memory */
2742   mapfree(&addedmap);
2743   mapfree(&noupdaterule);
2744   queuefree(&q);
2745
2746   /*
2747    * solve !
2748    *
2749    */
2750
2751   run_solver(solv, 1, 1);
2752
2753   /* find suggested packages */
2754   if (!solv->problems.count)
2755     {
2756       Id sug, *sugp, enh, *enhp, req, *reqp, p, *pp;
2757
2758       /* create map of all suggests that are still open */
2759       solv->recommends_index = -1;
2760       MAPZERO(&solv->suggestsmap);
2761       for (i = 0; i < solv->decisionq.count; i++)
2762         {
2763           p = solv->decisionq.elements[i];
2764           if (p < 0)
2765             continue;
2766           s = pool->solvables + p;
2767           if ((sugp = s->suggests) != 0)
2768             while ((sug = *sugp++) != 0)
2769               {
2770                 FOR_PROVIDES(p, pp, sug)
2771                   if (solv->decisionmap[p] > 0)
2772                     break;
2773                 if (p)
2774                   continue;     /* already fulfilled */
2775                 FOR_PROVIDES(p, pp, sug)
2776                   MAPSET(&solv->suggestsmap, p);
2777               }
2778         }
2779       for (i = 1; i < pool->nsolvables; i++)
2780         {
2781           if (solv->decisionmap[i] != 0)
2782             continue;
2783           s = pool->solvables + i;
2784           if (!MAPTST(&solv->suggestsmap, i))
2785             {
2786               if ((enhp = s->enhances) == 0)
2787                 continue;
2788               if (!pool_installable(pool, s))
2789                 continue;
2790               while ((enh = *enhp++) != 0)
2791                 if (dep_fulfilled(solv, enh))
2792                   break;
2793               if (!enh)
2794                 continue;
2795             }
2796           /* check if installation is possible at all */
2797           if ((reqp = s->requires) != 0)
2798             {
2799               while ((req = *reqp++) != 0)
2800                 {
2801                   if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
2802                     continue;
2803                   FOR_PROVIDES(p, pp, req)
2804                     if (solv->decisionmap[p] >= 0)
2805                       break;
2806                   if (!p && !strncmp(id2str(pool, req), "rpmlib(", 7))
2807                     continue;
2808                   if (!p)
2809                     break;              /* no provider installable! */
2810                 }
2811               if (req)
2812                 continue;
2813             }
2814           queuepush(&solv->suggestions, i);
2815         }
2816       prune_best_version_arch(pool, &solv->suggestions);
2817     }
2818
2819   /*
2820    *
2821    * print solver result
2822    *
2823    */
2824
2825   if (pool->verbose) printf("-------------------------------------------------------------\n");
2826
2827   if (solv->problems.count)
2828     {
2829       Queue problems;
2830       Queue solution;
2831       Id *problem;
2832       Id why;
2833       int j;
2834
2835       if (!pool->verbose)
2836         return;
2837       clonequeue(&problems, &solv->problems);
2838       queueinit(&solution);
2839       printf("Encountered problems! Here are the solutions:\n");
2840       problem = problems.elements;
2841       for (i = 0; i < problems.count; i++)
2842         {
2843           Id v = problems.elements[i];
2844           if (v == 0)
2845             {
2846               printf("====================================\n");
2847               problem = problems.elements + i + 1;
2848               continue;
2849             }
2850           refine_suggestion(solv, problem, v, &solution);
2851           for (j = 0; j < solution.count; j++)
2852             {
2853               r = solv->rules + solution.elements[j];
2854               why = solution.elements[j];
2855 #if 0
2856               printrule(solv, r);
2857 #endif
2858               if (why >= solv->jobrules && why < solv->systemrules)
2859                 {
2860                   /* do a sloppy job of analyzing the job rule */
2861                   if (r->p > 0)
2862                     {
2863                       s = pool->solvables + r->p;
2864                       printf("- do not install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2865                     }
2866                   else
2867                     {
2868                       s = pool->solvables - r->p;
2869                       printf("- do not erase %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2870                     }
2871                 }
2872               else if (why >= solv->systemrules && why < solv->learntrules)
2873                 {
2874                   Solvable *sd = 0;
2875                   s = pool->solvables + solv->system->start + (why - solv->systemrules);
2876                   if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2877                     {
2878                       Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2879                       for (; *dp; dp++)
2880                         {
2881                           if (*dp >= solv->system->start && *dp < solv->system->start + solv->system->nsolvables)
2882                             continue;
2883                           if (solv->decisionmap[*dp] > 0)
2884                             {
2885                               sd = pool->solvables + *dp;
2886                               break;
2887                             }
2888                         }
2889                     }
2890                   if (sd)
2891                     {
2892                       printf("- allow downgrade of %s-%s.%s to %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2893                     }
2894                   else
2895                     {
2896                       printf("- allow deinstallation of %s-%s.%s [%d]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), s - pool->solvables);
2897                     }
2898                 }
2899               else
2900                 {
2901                   abort();
2902                 }
2903             }
2904           printf("------------------------------------\n");
2905         }
2906       return;
2907     }
2908
2909   printdecisions(solv);
2910   if (solv->suggestions.count)
2911     {
2912       printf("\nsuggested packages:\n");
2913       for (i = 0; i < solv->suggestions.count; i++)
2914         {
2915           s = pool->solvables + solv->suggestions.elements[i];
2916           printf("- %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2917         }
2918     }
2919 }
2920
2921
2922 // EOF