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