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