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