src/solver.c

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