src/solver.c

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