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