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