src/solver.c

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