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   /*
 960    * look for updates for s
 961    */
 962   FOR_PROVIDES(p, pp, s->name)  /* every provider of s' name */
 963     {
 964       if (p == n)               /* skip itself */
 965         continue;
 966
 967       if (s->name == pool->solvables[p].name)   /* name match */
 968         {
 969           if (!allowdowngrade                   /* consider downgrades ? */
 970               && evrcmp(pool, s->evr, pool->solvables[p].evr) > 0)
 971             continue;
 972           /* XXX */
 973           if (!allowarchchange && archchanges(pool, s, pool->solvables + p))
 974             continue;
 975         }
 976       else if (!solv->noupdateprovide && (obsp = pool->solvables[p].obsoletes) != 0)   /* provides/obsoletes combination ? */
 977         {
 978           while ((obs = *obsp++) != 0)  /* for all obsoletes */
 979             {
 980               FOR_PROVIDES(p2, pp2, obs)   /* and all matching providers of the obsoletes */
 981                 {
 982                   if (p2 == n)          /* match ! */
 983                     break;
 984                 }
 985               if (p2)                   /* match! */
 986                 break;
 987             }
 988           if (!obs)                     /* continue if no match */
 989             continue;
 990           /* here we have 'p' with a matching provides/obsoletes combination
 991            * thus flagging p as a valid update candidate for s
 992            */
 993         }
 994       else
 995         continue;
 996       queuepush(qs, p);
 997
 998       if (m && !MAPTST(m, p))           /* mark p for install if not already done */
 999         addrulesforsolvable(solv, pool->solvables + p, m);
1000     }
1001   if (solv->noupdateprovide && solv->obsoletes && solv->obsoletes[n - solv->system->start])
1002     {
1003       for (pp = solv->obsoletes_data + solv->obsoletes[n - solv->system->start]; (p = *pp++) != 0;)
1004         {
1005           queuepush(qs, p);
1006           if (m && !MAPTST(m, p))               /* mark p for install if not already done */
1007             addrulesforsolvable(solv, pool->solvables + p, m);
1008         }
1009     }
1010 }
1011
1012 /*
1013  * add rule for update
1014  *   (A|A1|A2|A3...)  An = update candidates for A
1015  *
1016  * s = (installed) solvable
1017  * m = 'addedmap', bit set if 'install' rule for solvable exists
1018  */
1019
1020 static void
1021 addupdaterule(Solver *solv, Solvable *s, Map *m, int allowdowngrade, int allowarchchange, int dontaddrule)
1022 {
1023   /* system packages get a special upgrade allowed rule */
1024   Pool *pool = solv->pool;
1025   Id p, d;
1026   Rule *r;
1027   Queue qs;
1028   Id qsbuf[64];
1029
1030   queueinit_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1031   findupdatepackages(solv, s, &qs, m, allowdowngrade, allowarchchange);
1032   p = s - pool->solvables;
1033   if (dontaddrule)      /* we consider update candidates but dont force them */
1034     {
1035       queuefree(&qs);
1036       return;
1037     }
1038
1039   if (qs.count == 0)                   /* no updates found */
1040     {
1041 #if 0
1042       printf("new update rule: must keep %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1043 #endif
1044       addrule(solv, p, 0);              /* request 'install' of s */
1045       queuefree(&qs);
1046       return;
1047     }
1048
1049   d = pool_queuetowhatprovides(pool, &qs);   /* intern computed provider queue */
1050   queuefree(&qs);
1051   r = addrule(solv, p, d);             /* allow update of s */
1052 #if 0
1053   printf("new update rule ");
1054   if (r)
1055     printrule(solv, r);
1056 #endif
1057 }
1058
1059
1060 /*-----------------------------------------------------------------*/
1061 /* watches */
1062
1063
1064 /*
1065  * makewatches
1066  *
1067  * initial setup for all watches
1068  */
1069
1070 static void
1071 makewatches(Solver *solv)
1072 {
1073   Rule *r;
1074   int i;
1075   int nsolvables = solv->pool->nsolvables;
1076
1077   xfree(solv->watches);
1078                                        /* lower half for removals, upper half for installs */
1079   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1080 #if 1
1081   /* do it reverse so rpm rules get triggered first */
1082   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1083 #else
1084   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1085 #endif
1086     {
1087       if (!r->w1                       /* rule is disabled */
1088           || !r->w2)                   /* rule is assertion */
1089         continue;
1090
1091       /* see addwatches(solv, r) */
1092       r->n1 = solv->watches[nsolvables + r->w1];
1093       solv->watches[nsolvables + r->w1] = r - solv->rules;
1094
1095       r->n2 = solv->watches[nsolvables + r->w2];
1096       solv->watches[nsolvables + r->w2] = r - solv->rules;
1097     }
1098 }
1099
1100
1101 /*
1102  * add watches (for rule)
1103  */
1104
1105 static void
1106 addwatches(Solver *solv, Rule *r)
1107 {
1108   int nsolvables = solv->pool->nsolvables;
1109
1110   r->n1 = solv->watches[nsolvables + r->w1];
1111   solv->watches[nsolvables + r->w1] = r - solv->rules;
1112
1113   r->n2 = solv->watches[nsolvables + r->w2];
1114   solv->watches[nsolvables + r->w2] = r - solv->rules;
1115 }
1116
1117
1118 /*-----------------------------------------------------------------*/
1119 /* rule propagation */
1120
1121 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1122
1123 /*
1124  * propagate
1125  *
1126  * propagate decision to all rules
1127  */
1128
1129 static Rule *
1130 propagate(Solver *solv, int level)
1131 {
1132   Pool *pool = solv->pool;
1133   Id *rp, *nrp;
1134   Rule *r;
1135   Id p, pkg, ow;
1136   Id *dp;
1137   Id *decisionmap = solv->decisionmap;
1138   Id *watches = solv->watches + pool->nsolvables;
1139
1140   while (solv->propagate_index < solv->decisionq.count)
1141     {
1142       /* negative because our watches trigger if literal goes FALSE */
1143       pkg = -solv->decisionq.elements[solv->propagate_index++];
1144 #if 0
1145   printf("popagate for decision %d level %d\n", -pkg, level);
1146   printruleelement(solv, 0, -pkg);
1147 #endif
1148       for (rp = watches + pkg; *rp; rp = nrp)
1149         {
1150           r = solv->rules + *rp;
1151 #if 0
1152   printf("  watch triggered ");
1153   printrule(solv, r);
1154 #endif
1155           if (pkg == r->w1)
1156             {
1157               ow = r->w2;
1158               nrp = &r->n1;
1159             }
1160           else
1161             {
1162               ow = r->w1;
1163               nrp = &r->n2;
1164             }
1165           /* if clause is TRUE, nothing to do */
1166           if (DECISIONMAP_TRUE(ow))
1167             continue;
1168
1169           if (r->d)
1170             {
1171               /* not a binary clause, check if we need to move our watch */
1172               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1173                 p = r->p;
1174               else
1175                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1176                   if (p != ow && !DECISIONMAP_TRUE(-p))
1177                     break;
1178               if (p)
1179                 {
1180                   /* p is free to watch, move watch to p */
1181 #if 0
1182                   if (p > 0)
1183                     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));
1184                   else
1185                     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));
1186 #endif
1187                   *rp = *nrp;
1188                   nrp = rp;
1189                   if (pkg == r->w1)
1190                     {
1191                       r->w1 = p;
1192                       r->n1 = watches[p];
1193                     }
1194                   else
1195                     {
1196                       r->w2 = p;
1197                       r->n2 = watches[p];
1198                     }
1199                   watches[p] = r - solv->rules;
1200                   continue;
1201                 }
1202             }
1203           /* unit clause found, set other watch to TRUE */
1204           if (DECISIONMAP_TRUE(-ow))
1205             return r;           /* eek, a conflict! */
1206 #if 0
1207           printf("unit ");
1208           printrule(solv, r);
1209 #endif
1210           if (ow > 0)
1211             decisionmap[ow] = level;
1212           else
1213             decisionmap[-ow] = -level;
1214           queuepush(&solv->decisionq, ow);
1215           queuepush(&solv->decisionq_why, r - solv->rules);
1216 #if 0
1217             {
1218               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1219               if (ow > 0)
1220                 printf("  -> decided to install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1221               else
1222                 printf("  -> decided to conflict %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1223             }
1224 #endif
1225         }
1226     }
1227   return 0;     /* all is well */
1228 }
1229
1230
1231 /*-----------------------------------------------------------------*/
1232 /* Analysis */
1233
1234 /*
1235  * analyze
1236  *   and learn
1237  */
1238
1239 static int
1240 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1241 {
1242   Pool *pool = solv->pool;
1243   Queue r;
1244   int rlevel = 1;
1245   Map seen;             /* global? */
1246   Id v, vv, *dp;
1247   int l, i, idx;
1248   int num = 0;
1249   int learnt_why = solv->learnt_pool.count;
1250   Id *decisionmap = solv->decisionmap;
1251
1252   queueinit(&r);
1253
1254   if (pool->verbose) printf("ANALYZE at %d ----------------------\n", level);
1255   mapinit(&seen, pool->nsolvables);
1256   idx = solv->decisionq.count;
1257   for (;;)
1258     {
1259       printrule(solv, c);
1260       queuepush(&solv->learnt_pool, c - solv->rules);
1261       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1262       for (i = -1; ; i++)
1263         {
1264           if (i == -1)
1265             v = c->p;
1266           else if (c->d == 0)
1267             v = i ? 0 : c->w2;
1268           else
1269             v = *dp++;
1270           if (v == 0)
1271             break;
1272           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1273               continue;
1274           vv = v > 0 ? v : -v;
1275           if (MAPTST(&seen, vv))
1276             continue;
1277           l = solv->decisionmap[vv];
1278           if (l < 0)
1279             l = -l;
1280           if (l == 1)
1281             {
1282 #if 0
1283               int j;
1284               for (j = 0; j < solv->decisionq.count; j++)
1285                 if (solv->decisionq.elements[j] == v)
1286                   break;
1287               if (j == solv->decisionq.count)
1288                 abort();
1289               queuepush(&rulq, -(j + 1));
1290 #endif
1291               continue;                 /* initial setting */
1292             }
1293           MAPSET(&seen, vv);
1294           if (l == level)
1295             num++;                      /* need to do this one as well */
1296           else
1297             {
1298               queuepush(&r, v);
1299 #if 0
1300   printf("PUSH %d ", v);
1301   printruleelement(solv, 0, v);
1302 #endif
1303               if (l > rlevel)
1304                 rlevel = l;
1305             }
1306         }
1307 #if 0
1308       printf("num = %d\n", num);
1309 #endif
1310       if (num <= 0)
1311         abort();
1312       for (;;)
1313         {
1314           v = solv->decisionq.elements[--idx];
1315           vv = v > 0 ? v : -v;
1316           if (MAPTST(&seen, vv))
1317             break;
1318         }
1319       c = solv->rules + solv->decisionq_why.elements[idx];
1320       MAPCLR(&seen, vv);
1321       if (--num == 0)
1322         break;
1323     }
1324   *pr = -v;
1325   if (r.count == 0)
1326     *dr = 0;
1327   else if (r.count == 1 && r.elements[0] < 0)
1328     *dr = r.elements[0];
1329   else
1330     *dr = pool_queuetowhatprovides(pool, &r);
1331   if (pool->verbose)
1332     {
1333       printf("learned rule for level %d (am %d)\n", rlevel, level);
1334       printruleelement(solv, 0, -v);
1335       for (i = 0; i < r.count; i++)
1336         {
1337           v = r.elements[i];
1338           printruleelement(solv, 0, v);
1339         }
1340     }
1341   mapfree(&seen);
1342   queuepush(&solv->learnt_pool, 0);
1343 #if 0
1344   for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1345     {
1346       printf("learnt_why ");
1347       printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1348     }
1349 #endif
1350   if (why)
1351     *why = learnt_why;
1352   return rlevel;
1353 }
1354
1355
1356 /*
1357  * reset_solver
1358  * reset the solver decisions to right after the rpm rules
1359  */
1360
1361 static void
1362 reset_solver(Solver *solv)
1363 {
1364   int i;
1365   Id v;
1366   Rule *r;
1367
1368   /* delete all learnt rules */
1369   solv->nrules = solv->learntrules;
1370   QUEUEEMPTY(&solv->learnt_why);
1371   QUEUEEMPTY(&solv->learnt_pool);
1372
1373   /* redo all direct decision without the disabled rules */
1374   for (i = 0; i < solv->decisionq.count; i++)
1375     {
1376       v = solv->decisionq.elements[i];
1377       solv->decisionmap[v > 0 ? v : -v] = 0;
1378     }
1379   for (i = 0; i < solv->decisionq_why.count; i++)
1380     if (solv->decisionq_why.elements[i])
1381       break;
1382     else
1383       {
1384         v = solv->decisionq.elements[i];
1385         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1386       }
1387
1388   if (solv->pool->verbose)
1389     printf("decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1390
1391   solv->decisionq_why.count = i;
1392   solv->decisionq.count = i;
1393   solv->recommends_index = -1;
1394   if (i < solv->propagate_index)
1395     solv->propagate_index = i;
1396   /* make direct decisions from enabled unary rules */
1397   for (i = solv->jobrules, r = solv->rules + solv->jobrules; i < solv->nrules; i++, r++)
1398     {
1399       if (!r->w1 || r->w2)
1400         continue;
1401 #if 0
1402       printrule(solv, r);
1403 #endif
1404       v = r->p;
1405       queuepush(&solv->decisionq, v);
1406       queuepush(&solv->decisionq_why, r - solv->rules);
1407       solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1408     }
1409   if (solv->pool->verbose)
1410     printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
1411   /* recreate watches */
1412   makewatches(solv);
1413 }
1414
1415
1416 /*
1417  * analyze_unsolvable_rule
1418  */
1419
1420 static void
1421 analyze_unsolvable_rule(Solver *solv, Rule *c, int disablerules)
1422 {
1423   Id why;
1424   int i;
1425
1426   why = c - solv->rules;
1427 #if 0
1428   if (why >= solv->jobrules && why < solv->systemrules)
1429     printf("JOB ");
1430   if (why >= solv->systemrules && why < solv->learntrules)
1431     printf("SYSTEM %d ", why - solv->systemrules);
1432   if (solv->learntrules && why >= solv->learntrules)
1433     printf("LEARNED ");
1434   printrule(solv, c);
1435 #endif
1436   if (solv->learntrules && why >= solv->learntrules)
1437     {
1438       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1439         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], disablerules);
1440       return;
1441     }
1442   if (why >= solv->jobrules && why < solv->learntrules)
1443     {
1444       if (disablerules)
1445         {
1446           /* turn off rule for further analysis */
1447           c->w1 = 0;
1448         }
1449       /* unify problem */
1450       if (solv->problems.count)
1451         {
1452           for (i = solv->problems.count - 1; i >= 0; i--)
1453             if (solv->problems.elements[i] == 0)
1454               break;
1455             else if (solv->problems.elements[i] == why)
1456               return;
1457         }
1458       queuepush(&solv->problems, why);
1459     }
1460 }
1461
1462
1463 /*
1464  * analyze_unsolvable
1465  */
1466
1467 static void
1468 analyze_unsolvable(Solver *solv, Rule *c, int disablerules)
1469 {
1470   Pool *pool = solv->pool;
1471   Map seen;             /* global? */
1472   Id v, vv, *dp, why;
1473   int l, i, idx;
1474   Id *decisionmap = solv->decisionmap;
1475
1476 #if 0
1477   printf("ANALYZE UNSOLVABLE ----------------------\n");
1478 #endif
1479   mapinit(&seen, pool->nsolvables);
1480   analyze_unsolvable_rule(solv, c, disablerules);
1481   dp = c->d ? pool->whatprovidesdata + c->d : 0;
1482   for (i = -1; ; i++)
1483     {
1484       if (i == -1)
1485         v = c->p;
1486       else if (c->d == 0)
1487         v = i ? 0 : c->w2;
1488       else
1489         v = *dp++;
1490       if (v == 0)
1491         break;
1492       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1493           continue;
1494       vv = v > 0 ? v : -v;
1495       l = solv->decisionmap[vv];
1496       if (l < 0)
1497         l = -l;
1498       MAPSET(&seen, vv);
1499     }
1500   idx = solv->decisionq.count;
1501   while (idx > 0)
1502     {
1503       v = solv->decisionq.elements[--idx];
1504       vv = v > 0 ? v : -v;
1505       if (!MAPTST(&seen, vv))
1506         continue;
1507       why = solv->decisionq_why.elements[idx];
1508       if (!why)
1509         {
1510 #if 0
1511           printf("RPM ");
1512           printruleelement(solv, 0, v);
1513 #endif
1514           continue;
1515         }
1516       c = solv->rules + why;
1517       analyze_unsolvable_rule(solv, c, disablerules);
1518       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1519       for (i = -1; ; i++)
1520         {
1521           if (i == -1)
1522             v = c->p;
1523           else if (c->d == 0)
1524             v = i ? 0 : c->w2;
1525           else
1526             v = *dp++;
1527           if (v == 0)
1528             break;
1529           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1530               continue;
1531           vv = v > 0 ? v : -v;
1532           l = solv->decisionmap[vv];
1533           if (l < 0)
1534             l = -l;
1535           MAPSET(&seen, vv);
1536         }
1537     }
1538   mapfree(&seen);
1539   queuepush(&solv->problems, 0);        /* mark end of this problem */
1540   if (disablerules)
1541     reset_solver(solv);
1542 #if 0
1543   printf("analyze_unsolvables done\n");
1544 #endif
1545 }
1546
1547
1548 /*-----------------------------------------------------------------*/
1549 /* Decision revert */
1550
1551 /*
1552  * revert
1553  * revert decision at level
1554  */
1555
1556 static void
1557 revert(Solver *solv, int level)
1558 {
1559   Id v, vv;
1560   while (solv->decisionq.count)
1561     {
1562       v = solv->decisionq.elements[solv->decisionq.count - 1];
1563       vv = v > 0 ? v : -v;
1564       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1565         break;
1566 #if 0
1567       printf("reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1568 #endif
1569       solv->decisionmap[vv] = 0;
1570       solv->decisionq.count--;
1571       solv->decisionq_why.count--;
1572       solv->propagate_index = solv->decisionq.count;
1573     }
1574   solv->recommends_index = -1;
1575 }
1576
1577
1578 /*
1579  * watch2onhighest
1580  */
1581
1582 static void
1583 watch2onhighest(Solver *solv, Rule *r)
1584 {
1585   int l, wl = 0;
1586   Id v, *dp;
1587
1588   if (!r->d)
1589     return;     /* binary rule, both watches are set */
1590   dp = solv->pool->whatprovidesdata + r->d;
1591   while ((v = *dp++) != 0)
1592     {
1593       l = solv->decisionmap[v < 0 ? -v : v];
1594       if (l < 0)
1595         l = -l;
1596       if (l > wl)
1597         {
1598           r->w2 = dp[-1];
1599           wl = l;
1600         }
1601     }
1602 }
1603
1604
1605 /*
1606  * setpropagatelearn
1607  */
1608
1609 static int
1610 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1611 {
1612   Rule *r;
1613   Id p, d;
1614   int l, why;
1615
1616   if (decision)
1617     {
1618       level++;
1619       if (decision > 0)
1620         solv->decisionmap[decision] = level;
1621       else
1622         solv->decisionmap[-decision] = -level;
1623       queuepush(&solv->decisionq, decision);
1624       queuepush(&solv->decisionq_why, 0);
1625     }
1626   for (;;)
1627     {
1628       r = propagate(solv, level);
1629       if (!r)
1630         break;
1631       if (level == 1)
1632         {
1633           analyze_unsolvable(solv, r, disablerules);
1634           if (disablerules)
1635             return 1;
1636           return 0;
1637         }
1638       printf("conflict with rule #%d\n", (int)(r - solv->rules));
1639       l = analyze(solv, level, r, &p, &d, &why);
1640       if (l >= level || l <= 0)
1641         abort();
1642       printf("reverting decisions (level %d -> %d)\n", level, l);
1643       level = l;
1644       revert(solv, level);
1645       r = addrule(solv, p, d);       /* p requires d */
1646       if (!r)
1647         abort();
1648       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1649         {
1650           printf("%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1651           abort();
1652         }
1653       queuepush(&solv->learnt_why, why);
1654       if (d)
1655         {
1656           /* at least 2 literals, needs watches */
1657           watch2onhighest(solv, r);
1658           addwatches(solv, r);
1659         }
1660       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1661       queuepush(&solv->decisionq, p);
1662       queuepush(&solv->decisionq_why, r - solv->rules);
1663       printf("decision: ");
1664       printruleelement(solv, 0, p);
1665       printf("new rule: ");
1666       printrule(solv, r);
1667     }
1668   return level;
1669 }
1670
1671 /*-----------------------------------------------------------------*/
1672 /* Main solver interface */
1673
1674
1675 /*
1676  * solver_create
1677  * create solver structure
1678  *
1679  * pool: all available solvables
1680  * system: installed Solvables
1681  *
1682  *
1683  * Upon solving, rules are created to flag the Solvables
1684  * of the 'system' Source as installed.
1685  */
1686
1687 Solver *
1688 solver_create(Pool *pool, Source *system)
1689 {
1690   Solver *solv;
1691   solv = (Solver *)xcalloc(1, sizeof(Solver));
1692   solv->pool = pool;
1693   solv->system = system;
1694   pool->verbose = 1;
1695
1696   queueinit(&solv->decisionq);
1697   queueinit(&solv->decisionq_why);
1698   queueinit(&solv->problems);
1699   queueinit(&solv->learnt_why);
1700   queueinit(&solv->learnt_pool);
1701
1702   mapinit(&solv->recommends, pool->nsolvables);
1703   mapinit(&solv->suggests, pool->nsolvables);
1704   solv->recommends_index = 0;
1705
1706   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1707   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1708   memset(solv->rules, 0, sizeof(Rule));
1709   solv->nrules = 1;
1710
1711   return solv;
1712 }
1713
1714
1715 /*
1716  * solver_free
1717  */
1718
1719 void
1720 solver_free(Solver *solv)
1721 {
1722   queuefree(&solv->decisionq);
1723   queuefree(&solv->decisionq_why);
1724   queuefree(&solv->learnt_why);
1725   queuefree(&solv->learnt_pool);
1726   mapfree(&solv->recommends);
1727   mapfree(&solv->suggests);
1728   xfree(solv->decisionmap);
1729   xfree(solv->rules);
1730   xfree(solv->watches);
1731   xfree(solv->weaksystemrules);
1732   xfree(solv->obsoletes);
1733   xfree(solv->obsoletes_data);
1734   xfree(solv);
1735 }
1736
1737
1738 /*
1739  * reenablerule
1740  *
1741  * r->w1 was set to 0, now find proper value for w1
1742  */
1743
1744 static void
1745 reenablerule(Solver *solv, Rule *r)
1746 {
1747   int i;
1748   Id v, l, good;
1749
1750   if (!r->w2)                          /* not a rule, but an assertion */
1751     {
1752       r->w1 = r->p;
1753       return;
1754     }
1755   if (!r->d)
1756     {
1757       if (r->w2 != r->p)
1758         r->w1 = r->p;
1759       else
1760         r->w2 = r->d;                  /* mls: shouldn't this be r->w1 ? */
1761       return;
1762     }
1763   good = 0;
1764                                        /* put it on the first not-false literal */
1765   for (i = -1; ; i++)
1766     {
1767       if (i == -1)
1768         v = r->p;
1769       else
1770         v = solv->pool->whatprovidesdata[r->d + i];
1771       if (!v)
1772         {
1773           printrule(solv, r);
1774           abort();
1775         }
1776       if (v == r->w2)
1777         continue;
1778       l = solv->decisionmap[v > 0 ? v : -v];
1779       if (!l || (v < 0 && l < 0) || (v > 0 && l > 0))
1780         break;
1781     }
1782   r->w1 = v;
1783 }
1784
1785
1786 /*-------------------------------------------------------*/
1787
1788 /*
1789  * run_solver
1790  *
1791  * all rules have been set up, not actually run the solver
1792  *
1793  */
1794
1795 static void
1796 run_solver(Solver *solv, int disablerules, int doweak)
1797 {
1798   Queue dq;
1799   int systemlevel;
1800   int level, olevel;
1801   Rule *r;
1802   int i, n;
1803   Solvable *s;
1804   Pool *pool = solv->pool;
1805   Id p, *dp;
1806
1807 #if 0
1808   printf("number of rules: %d\n", solv->nrules);
1809 {
1810   int i;
1811   for (i = 0; i < solv->nrules; i++)
1812     {
1813       printrule(solv, solv->rules + i);
1814     }
1815 }
1816 #endif
1817
1818   /* all new rules are learnt after this point */
1819   solv->learntrules = solv->nrules;
1820   /* crate watches lists */
1821   makewatches(solv);
1822
1823   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
1824
1825   /* start SAT algorithm */
1826   level = 1;
1827   systemlevel = level + 1;
1828   if (pool->verbose) printf("solving...\n");
1829
1830   queueinit(&dq);
1831   for (;;)
1832     {
1833       /*
1834        * propagate
1835        */
1836
1837       if (level == 1)
1838         {
1839           if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
1840           if ((r = propagate(solv, level)) != 0)
1841             {
1842               analyze_unsolvable(solv, r, disablerules);
1843               if (disablerules)
1844                 continue;
1845               printf("UNSOLVABLE\n");
1846               queuefree(&dq);
1847               return;
1848             }
1849         }
1850
1851       /*
1852        * system packages
1853        */
1854
1855       if (level < systemlevel && solv->system->nsolvables)
1856         {
1857           if (!solv->updatesystem)
1858             {
1859               /* try to keep as many packages as possible */
1860               if (pool->verbose) printf("installing system packages\n");
1861               for (i = solv->system->start, n = 0; ; i++, n++)
1862                 {
1863                   if (n == solv->system->nsolvables)
1864                     break;
1865                   if (i == solv->system->start + solv->system->nsolvables)
1866                     i = solv->system->start;
1867                   s = pool->solvables + i;
1868                   if (solv->decisionmap[i] != 0)
1869                     continue;
1870 #if 0
1871                   printf("system installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1872 #endif
1873                   olevel = level;
1874                   level = setpropagatelearn(solv, level, i, disablerules);
1875                   if (level == 0)
1876                     {
1877                       printf("UNSOLVABLE\n");
1878                       queuefree(&dq);
1879                       return;
1880                     }
1881                   if (level <= olevel)
1882                     n = 0;
1883                 }
1884             }
1885           if (solv->weaksystemrules)
1886             {
1887               if (pool->verbose) printf("installing weak system packages\n");
1888               for (i = solv->system->start, n = 0; ; i++, n++)
1889                 {
1890                   if (n == solv->system->nsolvables)
1891                     break;
1892                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->system->start] == 0))
1893                     continue;
1894                   QUEUEEMPTY(&dq);
1895                   if (solv->decisionmap[i] == 0)
1896                     queuepush(&dq, i);
1897                   if (solv->weaksystemrules[i - solv->system->start])
1898                     {
1899                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->system->start];
1900                       while ((p = *dp++) != 0)
1901                         {
1902                           if (solv->decisionmap[p] > 0)
1903                             break;
1904                           if (solv->decisionmap[p] == 0)
1905                             queuepush(&dq, p);
1906                         }
1907                       if (p)
1908                         continue;       /* rule is already true */
1909                     }
1910                   if (!dq.count)
1911                     continue;
1912
1913                   if (dq.count > 1)
1914                     prune_to_recommended(solv, &dq);
1915                   if (dq.count > 1)
1916                     prune_best_version_arch(pool, &dq);
1917 #if 0
1918                   s = pool->solvables + dq.elements[0];
1919                   printf("weak system installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1920 #endif
1921                   olevel = level;
1922                   level = setpropagatelearn(solv, level, dq.elements[0], disablerules);
1923                   if (level == 0)
1924                     {
1925                       printf("UNSOLVABLE\n");
1926                       queuefree(&dq);
1927                       return;
1928                     }
1929                   if (level <= olevel)
1930                     {
1931                       n = 0;
1932                       break;
1933                     }
1934                 }
1935               if (n != solv->system->nsolvables)
1936                 continue;
1937             }
1938           systemlevel = level;
1939         }
1940
1941       /*
1942        * decide
1943        */
1944
1945       if (pool->verbose) printf("deciding unresolved rules\n");
1946       for (i = 1, n = 1; ; i++, n++)
1947         {
1948           if (n == solv->nrules)
1949             break;
1950           if (i == solv->nrules)
1951             i = 1;
1952           r = solv->rules + i;
1953           if (!r->w1)
1954             continue;
1955           QUEUEEMPTY(&dq);
1956           if (r->d == 0)
1957             {
1958               /* binary or unary rule */
1959               /* need two positive undecided literals */
1960               if (r->p < 0 || r->w2 <= 0)
1961                 continue;
1962               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
1963                 continue;
1964               queuepush(&dq, r->p);
1965               queuepush(&dq, r->w2);
1966             }
1967           else
1968             {
1969               /* make sure that
1970                * all negative literals are installed
1971                * no positive literal is installed
1972                * i.e. the rule is not fulfilled and we
1973                * just need to decide on the positive literals
1974                */
1975               if (r->p < 0)
1976                 {
1977                   if (solv->decisionmap[-r->p] <= 0)
1978                     continue;
1979                 }
1980               else
1981                 {
1982                   if (solv->decisionmap[r->p] > 0)
1983                     continue;
1984                   if (solv->decisionmap[r->p] == 0)
1985                     queuepush(&dq, r->p);
1986                 }
1987               dp = pool->whatprovidesdata + r->d;
1988               while ((p = *dp++) != 0)
1989                 {
1990                   if (p < 0)
1991                     {
1992                       if (solv->decisionmap[-p] <= 0)
1993                         break;
1994                     }
1995                   else
1996                     {
1997                       if (solv->decisionmap[p] > 0)
1998                         break;
1999                       if (solv->decisionmap[p] == 0)
2000                         queuepush(&dq, p);
2001                     }
2002                 }
2003               if (p)
2004                 continue;
2005             }
2006           if (dq.count < 2)
2007             {
2008               /* cannot happen as this means that
2009                * the rule is unit */
2010               printrule(solv, r);
2011               abort();
2012             }
2013           prune_to_recommended(solv, &dq);
2014           if (dq.count > 1)
2015             prune_best_version_arch(pool, &dq);
2016           p = dq.elements[dq.count - 1];
2017           s = pool->solvables + p;
2018 #if 0
2019           printf("installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2020 #endif
2021           olevel = level;
2022           level = setpropagatelearn(solv, level, p, disablerules);
2023           if (level == 0)
2024             {
2025               printf("UNSOLVABLE\n");
2026               queuefree(&dq);
2027               return;
2028             }
2029           if (level < systemlevel)
2030             break;
2031           if (level <= olevel)
2032             n = 0;
2033         } /* for(), decide */
2034
2035       if (n != solv->nrules)    /* continue if level < systemlevel */
2036         continue;
2037
2038       if (doweak && !solv->problems.count)
2039         {
2040           int qcount;
2041
2042           if (pool->verbose) printf("installing recommended packages\n");
2043           QUEUEEMPTY(&dq);
2044           for (i = 1; i < pool->nsolvables; i++)
2045             {
2046               if (solv->decisionmap[i] < 0)
2047                 continue;
2048               if (solv->decisionmap[i] > 0)
2049                 {
2050                   Id *recp, rec, *pp, p;
2051                   s = pool->solvables + i;
2052                   /* installed, check for recommends */
2053                   /* XXX need to special case AND ? */
2054                   if ((recp = s->recommends) != 0)
2055                     {
2056                       while ((rec = *recp++) != 0)
2057                         {
2058                           qcount = dq.count;
2059                           FOR_PROVIDES(p, pp, rec)
2060                             {
2061                               if (solv->decisionmap[p] > 0)
2062                                 {
2063                                   dq.count = qcount;
2064                                   break;
2065                                 }
2066                               else if (solv->decisionmap[p] == 0)
2067                                 queuepushunique(&dq, p);
2068                             }
2069                         }
2070                     }
2071                 }
2072               else
2073                 {
2074                   Id *supp, sup;
2075                   s = pool->solvables + i;
2076                   if (!s->supplements && !s->freshens)
2077                     continue;
2078                   if (s->arch == ARCH_SRC || s->arch == ARCH_NOSRC)
2079                     continue;
2080                   if (pool->id2arch && (s->arch > pool->lastarch || !pool->id2arch[s->arch]))
2081                     continue;
2082                   if ((supp = s->supplements) != 0)
2083                     {
2084                       while ((sup = *supp++) != 0)
2085                         if (dep_fulfilled(solv, sup))
2086                           break;
2087                       if (!sup)
2088                         continue;
2089                     }
2090                   if ((supp = s->freshens) != 0)
2091                     {
2092                       while ((sup = *supp++) != 0)
2093                         if (dep_fulfilled(solv, sup))
2094                           break;
2095                       if (!sup)
2096                         continue;
2097                     }
2098                   queuepushunique(&dq, i);
2099                 }
2100             }
2101           if (dq.count)
2102             {
2103               prune_best_version_arch(pool, &dq);
2104               p = dq.elements[dq.count - 1];
2105               s = pool->solvables + p;
2106 #if 1
2107               printf("installing recommended %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2108 #endif
2109               level = setpropagatelearn(solv, level, p, 0);
2110               continue;
2111             }
2112         }
2113       break;
2114     }
2115   queuefree(&dq);
2116 }
2117
2118
2119 /*
2120  * refine_suggestion
2121  */
2122
2123 static void
2124 refine_suggestion(Solver *solv, Id *problem, Id sug, Queue *refined)
2125 {
2126   Rule *r;
2127   int i, j;
2128   Id v;
2129   Queue disabled;
2130   int disabledcnt;
2131
2132   printf("refine_suggestion start\n");
2133   queueinit(&disabled);
2134   QUEUEEMPTY(refined);
2135   queuepush(refined, sug);
2136
2137   /* re-enable all rules but rule "sug" of the problem */
2138   for (i = 0; problem[i]; i++)
2139     {
2140       if (problem[i] == sug)
2141         continue;
2142       r = solv->rules + problem[i];
2143 #if 0
2144       printf("enable ");
2145       printrule(solv, r);
2146 #endif
2147       reenablerule(solv, r);
2148     }
2149   for (;;)
2150     {
2151       revert(solv, 1);          /* XXX move to reset_solver? */
2152       reset_solver(solv);
2153       QUEUEEMPTY(&solv->problems);
2154       run_solver(solv, 0, 0);
2155       if (!solv->problems.count)
2156         {
2157           printf("no more problems!\n");
2158 #if 0
2159           printdecisions(solv);
2160 #endif
2161           break;                /* great, no more problems */
2162         }
2163       disabledcnt = disabled.count;
2164       for (i = 0; i < solv->problems.elements[i]; i++)
2165         {
2166           /* ignore solutions in refined */
2167           v = solv->problems.elements[i];
2168           for (j = 0; problem[j]; j++)
2169             if (problem[j] != sug && problem[j] == v)
2170               break;
2171           if (problem[j])
2172             continue;
2173           queuepush(&disabled, v);
2174         }
2175       if (disabled.count == disabledcnt)
2176         {
2177           /* no solution found, this was an invalid suggestion! */
2178           printf("no solution found!\n");
2179           for (i = 0; i < refined->count; i++)
2180             reenablerule(solv, solv->rules + refined->elements[i]);
2181           refined->count = 0;
2182           break;
2183         }
2184       if (disabled.count == disabledcnt + 1)
2185         {
2186           /* just one solution, add it to refined list */
2187           queuepush(refined, disabled.elements[disabledcnt]);
2188         }
2189       else
2190         {
2191           printf("##############################################   more than one solution found.\n");
2192 #if 1
2193           for (i = 0; i < solv->problems.elements[i]; i++)
2194             {
2195               printrule(solv, solv->rules + solv->problems.elements[i]);
2196             }
2197           printf("##############################################\n");
2198 #endif
2199           /* more than one solution */
2200           /* for now return */
2201         }
2202       for (i = disabledcnt; i < disabled.count; i++)
2203         {
2204           r = solv->rules + disabled.elements[i];;
2205           /* disable it */
2206           r->w1 = 0;
2207 #if 0
2208           printf("disable ");
2209           printrule(solv, r);
2210 #endif
2211         }
2212     }
2213   /* enable refined rules again */
2214   for (i = 0; i < disabled.count; i++)
2215     reenablerule(solv, solv->rules + disabled.elements[i]);
2216   /* disable problem rules again so that we are in the same state as before */
2217   for (i = 0; problem[i]; i++)
2218     {
2219       r = solv->rules + problem[i];
2220       r->w1 = 0;
2221     }
2222   printf("refine_suggestion end\n");
2223 }
2224
2225
2226 /*
2227  * printdecisions
2228  */
2229
2230 static const char *
2231 id2rc(Solver *solv, Id id)
2232 {
2233   const char *evr;
2234   if (solv->rc_output != 2)
2235     return "";
2236   evr = id2str(solv->pool, id);
2237   if (*evr < '0' || *evr > '9')
2238     return "0:";
2239   while (*evr >= '0' && *evr <= '9')
2240     evr++;
2241   if (*evr != ':')
2242     return "0:";
2243   return "";
2244 }
2245
2246 void
2247 printdecisions(Solver *solv)
2248 {
2249   Pool *pool = solv->pool;
2250   Id p, *obsoletesmap;
2251   int i;
2252   Solvable *s;
2253
2254   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2255   for (i = 0; i < solv->decisionq.count; i++)
2256     {
2257       Id obs, *obsp;
2258       Id *pp, n;
2259
2260       n = solv->decisionq.elements[i];
2261       if (n < 0)
2262         continue;
2263       if (n >= solv->system->start && n < solv->system->start + solv->system->nsolvables)
2264         continue;
2265       s = pool->solvables + n;
2266       if ((obsp = s->obsoletes) != 0)
2267         while ((obs = *obsp++) != 0)
2268           FOR_PROVIDES(p, pp, obs)
2269             {
2270               if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2271                 {
2272                   obsoletesmap[p] = n;
2273                   obsoletesmap[n]++;
2274                 }
2275             }
2276       FOR_PROVIDES(p, pp, s->name)
2277         if (s->name == pool->solvables[p].name)
2278           {
2279             if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2280               {
2281                 obsoletesmap[p] = n;
2282                 obsoletesmap[n]++;
2283               }
2284           }
2285     }
2286
2287   if (solv->rc_output)
2288     printf(">!> Solution #1:\n");
2289
2290   int installs = 0, uninstalls = 0, upgrades = 0;
2291
2292   /* print solvables to be erased */
2293
2294   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2295     {
2296       if (solv->decisionmap[i] > 0)
2297         continue;
2298       if (obsoletesmap[i])
2299         continue;
2300       s = pool->solvables + i;
2301       if (solv->rc_output == 2)
2302         printf(">!> remove  %s-%s%s\n", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2303       else if (solv->rc_output)
2304         printf(">!> remove  %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2305       else
2306         printf("erase   %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2307       uninstalls++;
2308     }
2309
2310   /* print solvables to be installed */
2311
2312   for (i = 0; i < solv->decisionq.count; i++)
2313     {
2314       int j;
2315       p = solv->decisionq.elements[i];
2316       if (p < 0)
2317         continue;
2318       if (p >= solv->system->start && p < solv->system->start + solv->system->nsolvables)
2319         continue;
2320       s = pool->solvables + p;
2321
2322       if (!obsoletesmap[p])
2323         {
2324           if (solv->rc_output)
2325             printf(">!> ");
2326           printf("install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2327           if (solv->rc_output != 2)
2328             printf(".%s", id2str(pool, s->arch));
2329           installs++;
2330         }
2331       else if (!solv->rc_output)
2332         {
2333           printf("update  %s-%s.%s  (obsoletes", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2334           for (j = solv->system->start; j < solv->system->start + solv->system->nsolvables; j++)
2335             {
2336               if (obsoletesmap[j] != p)
2337                 continue;
2338               s = pool->solvables + j;
2339               printf(" %s-%s.%s", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2340             }
2341           printf(")");
2342           upgrades++;
2343         }
2344       else
2345         {
2346           Solvable *f, *fn = 0;
2347           for (j = solv->system->start; j < solv->system->start + solv->system->nsolvables; j++)
2348             {
2349               if (obsoletesmap[j] != p)
2350                 continue;
2351               f = pool->solvables + j;
2352               if (fn || f->name != s->name)
2353                 {
2354                   if (solv->rc_output == 2)
2355                     printf(">!> remove  %s-%s%s\n", id2str(pool, f->name), id2rc(solv, f->evr), id2str(pool, f->evr));
2356                   else if (solv->rc_output)
2357                     printf(">!> remove  %s-%s.%s\n", id2str(pool, f->name), id2str(pool, f->evr), id2str(pool, f->arch));
2358                   uninstalls++;
2359                 }
2360               else
2361                 fn = f;
2362             }
2363           if (!fn)
2364             {
2365               printf(">!> install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2366               if (solv->rc_output != 2)
2367                 printf(".%s", id2str(pool, s->arch));
2368               installs++;
2369             }
2370           else
2371             {
2372               if (solv->rc_output == 2)
2373                 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));
2374               else
2375                 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));
2376               upgrades++;
2377             }
2378         }
2379       if (solv->rc_output)
2380         {
2381           Source *source = pool_source(pool, s);
2382           if (source && strcmp(source_name(source), "locales"))
2383             printf("[%s]", source_name(source));
2384         }
2385       printf("\n");
2386     }
2387
2388   if (solv->rc_output)
2389     printf(">!> installs=%d, upgrades=%d, uninstalls=%d\n", installs, upgrades, uninstalls);
2390
2391   xfree(obsoletesmap);
2392 }
2393
2394 static void
2395 create_obsolete_index(Solver *solv)
2396 {
2397   Pool *pool = solv->pool;
2398   Solvable *s;
2399   Source *system = solv->system;
2400   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
2401   int i, n;
2402
2403   /* create reverse obsoletes map for system solvables */
2404   solv->obsoletes = obsoletes = xcalloc(system->nsolvables, sizeof(Id));
2405   for (i = 1; i < pool->nsolvables; i++)
2406     {
2407       s = pool->solvables + i;
2408       if ((obsp = s->obsoletes) == 0)
2409         continue;
2410       while ((obs = *obsp++) != 0)
2411         FOR_PROVIDES(p, pp, obs)
2412           {
2413             if (p < system->start || p >= system->start + system->nsolvables)
2414               continue;
2415             if (pool->solvables[p].name == s->name)
2416               continue;
2417             obsoletes[p - system->start]++;
2418           }
2419     }
2420   n = 0;
2421   for (i = 0; i < system->nsolvables; i++)
2422     if (obsoletes[i])
2423       {
2424         n += obsoletes[i] + 1;
2425         obsoletes[i] = n;
2426       }
2427   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
2428   if (pool->verbose) printf("obsoletes data: %d entries\n", n + 1);
2429   for (i = pool->nsolvables - 1; i > 0; i--)
2430     {
2431       s = pool->solvables + i;
2432       if ((obsp = s->obsoletes) == 0)
2433         continue;
2434       while ((obs = *obsp++) != 0)
2435         FOR_PROVIDES(p, pp, obs)
2436           {
2437             if (p < system->start || p >= system->start + system->nsolvables)
2438               continue;
2439             if (pool->solvables[p].name == s->name)
2440               continue;
2441             p -= system->start;
2442             if (obsoletes_data[obsoletes[p]] != i)
2443               obsoletes_data[--obsoletes[p]] = i;
2444           }
2445     }
2446 }
2447
2448 /*-----------------------------------------------------------------*/
2449 /* main() */
2450
2451 /*
2452  *
2453  * solve job queue
2454  *
2455  */
2456
2457 void
2458 solve(Solver *solv, Queue *job)
2459 {
2460   Pool *pool = solv->pool;
2461   int i;
2462   Map addedmap;                        /* '1' == have rule for solvable */
2463   Map noupdaterule;                    /* '1' == don't update (scheduled for removal) */
2464   Id how, what, p, *pp, d;
2465   Queue q;
2466   Rule *r;
2467   Solvable *s;
2468
2469   /*
2470    * create basic rule set of all involved packages
2471    * as bitmaps
2472    *
2473    */
2474
2475   mapinit(&addedmap, pool->nsolvables);
2476   mapinit(&noupdaterule, pool->nsolvables);
2477
2478   queueinit(&q);
2479
2480   /*
2481    * create rules for installed solvables -> keep them installed
2482    * so called: rpm rules
2483    *
2484    */
2485
2486   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2487     addrulesforsolvable(solv, pool->solvables + i, &addedmap);
2488
2489   /*
2490    * create install rules
2491    *
2492    * two passes, as we want to keep the rpm rules distinct from the job rules
2493    *
2494    */
2495
2496   if (solv->noupdateprovide && solv->system->nsolvables)
2497     create_obsolete_index(solv);
2498
2499   /*
2500    * solvable rules
2501    *  process job rules for solvables
2502    */
2503
2504   for (i = 0; i < job->count; i += 2)
2505     {
2506       how = job->elements[i];
2507       what = job->elements[i + 1];
2508
2509       switch(how)
2510         {
2511         case SOLVER_INSTALL_SOLVABLE:
2512           addrulesforsolvable(solv, pool->solvables + what, &addedmap);
2513           break;
2514         case SOLVER_INSTALL_SOLVABLE_NAME:
2515         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2516           QUEUEEMPTY(&q);
2517           FOR_PROVIDES(p, pp, what)
2518             {
2519                                        /* if by name, ensure that the name matches */
2520               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
2521                 continue;
2522               addrulesforsolvable(solv, pool->solvables + p, &addedmap);
2523             }
2524           break;
2525         case SOLVER_INSTALL_SOLVABLE_UPDATE:
2526           /* dont allow downgrade */
2527           addupdaterule(solv, pool->solvables + what, &addedmap, 0, 0, 1);
2528           break;
2529         }
2530     }
2531
2532   /*
2533    * if unstalls are disallowed, add update rules for every
2534    * installed solvables in the hope to circumvent uninstall
2535    * by upgrading
2536    *
2537    */
2538
2539 #if 0
2540   if (!solv->allowuninstall)
2541     {
2542       /* add update rule for every installed package */
2543       for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2544         addupdaterule(solv, pool->solvables + i, &addedmap, solv->allowdowngrade, solv->allowarchchange, 1);
2545     }
2546 #else  /* this is just to add the needed rpm rules to our set */
2547   for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2548     addupdaterule(solv, pool->solvables + i, &addedmap, 1, 1, 1);
2549 #endif
2550
2551   addrulesforsupplements(solv, &addedmap);
2552
2553   /*
2554    * first pass done
2555    *
2556    * unify existing rules before going over all job rules
2557    *
2558    */
2559
2560   unifyrules(solv);     /* remove duplicate rpm rules */
2561
2562   /*
2563    * at this point the system is always solvable,
2564    * as an empty system (remove all packages) is a valid solution
2565    */
2566   if (pool->verbose) printf("decisions based on rpms: %d\n", solv->decisionq.count);
2567
2568   /*
2569    * now add all job rules
2570    */
2571
2572   solv->jobrules = solv->nrules;
2573
2574   for (i = 0; i < job->count; i += 2)
2575     {
2576       how = job->elements[i];
2577       what = job->elements[i + 1];
2578       switch(how)
2579         {
2580         case SOLVER_INSTALL_SOLVABLE:                     /* install specific solvable */
2581           if (solv->rc_output) {
2582             Solvable *s = pool->solvables + what;
2583             printf(">!> Installing %s from channel %s\n", id2str(pool, s->name), source_name(pool_source(pool, s)));
2584           }
2585           addrule(solv, what, 0);                         /* install by Id */
2586           break;
2587         case SOLVER_ERASE_SOLVABLE:
2588           addrule(solv, -what, 0);                        /* remove by Id */
2589           MAPSET(&noupdaterule, what);
2590           break;
2591         case SOLVER_INSTALL_SOLVABLE_NAME:                /* install by capability */
2592         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2593           QUEUEEMPTY(&q);
2594           FOR_PROVIDES(p, pp, what)    /* check all providers */
2595             {
2596                                        /* if by name, ensure that the name matches */
2597               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
2598                 continue;
2599               queuepush(&q, p);
2600             }
2601           if (!q.count) {              /* no provider found -> abort */
2602             fprintf(stderr, "Nothing provides '%s'\n", id2str(pool, what));
2603             /* XXX make this a problem! */
2604             return;
2605             abort();
2606           }
2607
2608           p = queueshift(&q);          /* get first provider */
2609           if (!q.count)
2610             d = 0;                     /* single provider ? -> make assertion */
2611           else
2612             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
2613           addrule(solv, p, d);         /* add 'requires' rule */
2614           break;
2615         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
2616         case SOLVER_ERASE_SOLVABLE_PROVIDES:
2617           FOR_PROVIDES(p, pp, what)
2618             {
2619                                        /* if by name, ensure that the name matches */
2620               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
2621                 continue;
2622
2623               addrule(solv, -p, 0);  /* add 'remove' rule */
2624               MAPSET(&noupdaterule, p);
2625             }
2626           break;
2627         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
2628           addupdaterule(solv, pool->solvables + what, &addedmap, 0, 0, 0);
2629           break;
2630         }
2631     }
2632
2633   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
2634
2635   /*
2636    * now add policy rules
2637    *
2638    */
2639
2640   solv->systemrules = solv->nrules;
2641
2642   /*
2643    * create rules for updating installed solvables
2644    *
2645    * (Again ?)
2646    *
2647    */
2648
2649   if (!solv->allowuninstall)
2650     {                                  /* loop over all installed solvables */
2651       for (i = solv->system->start; i < solv->system->start + solv->system->nsolvables; i++)
2652       {
2653         if (!MAPTST(&noupdaterule, i)) /* if not marked as 'noupdate' */
2654           addupdaterule(solv, pool->solvables + i, &addedmap, solv->allowdowngrade, solv->allowarchchange, 0);
2655         else
2656           addrule(solv, 0, 0);          /* place holder */
2657       }
2658       /* consistency check: we added a rule for _every_ system solvable */
2659       if (solv->nrules - solv->systemrules != solv->system->nsolvables)
2660         abort();
2661     }
2662
2663   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
2664
2665   /* create special weak system rules */
2666   if (solv->system->nsolvables)
2667     {
2668       solv->weaksystemrules = xcalloc(solv->system->nsolvables, sizeof(Id));
2669       for (i = 0; i < solv->system->nsolvables; i++)
2670         {
2671           findupdatepackages(solv, pool->solvables + solv->system->start + i, &q, (Map *)0, 1, 1);
2672           if (q.count)
2673             solv->weaksystemrules[i] = pool_queuetowhatprovides(pool, &q);
2674         }
2675     }
2676
2677   /* free unneeded memory */
2678   mapfree(&addedmap);
2679   mapfree(&noupdaterule);
2680   queuefree(&q);
2681
2682   /*
2683    * solve !
2684    *
2685    */
2686
2687   run_solver(solv, 1, 1);
2688
2689   /*
2690    *
2691    * print solver result
2692    *
2693    */
2694
2695   if (pool->verbose) printf("-------------------------------------------------------------\n");
2696
2697   if (solv->problems.count)
2698     {
2699       Queue problems;
2700       Queue solution;
2701       Id *problem;
2702       Id why;
2703       int j;
2704
2705       if (!pool->verbose)
2706         return;
2707       clonequeue(&problems, &solv->problems);
2708       queueinit(&solution);
2709       printf("Encountered problems! Here are the solutions:\n");
2710       problem = problems.elements;
2711       for (i = 0; i < problems.count; i++)
2712         {
2713           Id v = problems.elements[i];
2714           if (v == 0)
2715             {
2716               printf("====================================\n");
2717               problem = problems.elements + i + 1;
2718               continue;
2719             }
2720           refine_suggestion(solv, problem, v, &solution);
2721           for (j = 0; j < solution.count; j++)
2722             {
2723               r = solv->rules + solution.elements[j];
2724               why = solution.elements[j];
2725 #if 0
2726               printrule(solv, r);
2727 #endif
2728               if (why >= solv->jobrules && why < solv->systemrules)
2729                 {
2730                   /* do a sloppy job of analyzing the job rule */
2731                   if (r->p > 0)
2732                     {
2733                       s = pool->solvables + r->p;
2734                       printf("- do not install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2735                     }
2736                   else
2737                     {
2738                       s = pool->solvables - r->p;
2739                       printf("- do not erase %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2740                     }
2741                 }
2742               else if (why >= solv->systemrules && why < solv->learntrules)
2743                 {
2744                   Solvable *sd = 0;
2745                   s = pool->solvables + solv->system->start + (why - solv->systemrules);
2746                   if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2747                     {
2748                       Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2749                       for (; *dp; dp++)
2750                         if (solv->decisionmap[*dp] > 0)
2751                           {
2752                             sd = pool->solvables + *dp;
2753                             break;
2754                           }
2755                     }
2756                   if (sd)
2757                     {
2758                       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));
2759                     }
2760                   else
2761                     {
2762                       printf("- allow deinstallation of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2763                     }
2764                 }
2765               else
2766                 {
2767                   abort();
2768                 }
2769             }
2770           printf("------------------------------------\n");
2771         }
2772       return;
2773     }
2774
2775   printdecisions(solv);
2776 }
2777
2778
2779 // EOF