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