src/solver.c

   1 /*
   2  * Copyright (c) 2007, Novell Inc.
   3  *
   4  * This program is licensed under the BSD license, read LICENSE.BSD
   5  * for further information
   6  */
   7
   8 /*
   9  * solver.c
  10  *
  11  * SAT based dependency solver
  12  */
  13
  14 #include <stdio.h>
  15 #include <stdlib.h>
  16 #include <unistd.h>
  17 #include <string.h>
  18
  19 #include "solver.h"
  20 #include "bitmap.h"
  21 #include "pool.h"
  22 #include "util.h"
  23 #include "evr.h"
  24 #include "policy.h"
  25
  26 #define RULES_BLOCK 63
  27
  28
  29 int
  30 solver_dep_installed(Solver *solv, Id dep)
  31 {
  32   /* disable for now, splitprovides don't work anyway and it breaks
  33      a testcase */
  34 #if 0
  35   Pool *pool = solv->pool;
  36   Id p, *pp;
  37
  38   if (ISRELDEP(dep))
  39     {
  40       Reldep *rd = GETRELDEP(pool, dep);
  41       if (rd->flags == REL_AND)
  42         {
  43           if (!solver_dep_installed(solv, rd->name))
  44             return 0;
  45           return solver_dep_installed(solv, rd->evr);
  46         }
  47       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  48         return solver_dep_installed(solv, rd->evr);
  49     }
  50   FOR_PROVIDES(p, pp, dep)
  51     {
  52       if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
  53         return 1;
  54     }
  55 #endif
  56   return 0;
  57 }
  58
  59
  60 /* this mirrors solver_dep_fulfilled but uses map m instead of the decisionmap */
  61 static inline int
  62 dep_possible(Solver *solv, Id dep, Map *m)
  63 {
  64   Pool *pool = solv->pool;
  65   Id p, *pp;
  66
  67   if (ISRELDEP(dep))
  68     {
  69       Reldep *rd = GETRELDEP(pool, dep);
  70       if (rd->flags == REL_AND)
  71         {
  72           if (!dep_possible(solv, rd->name, m))
  73             return 0;
  74           return dep_possible(solv, rd->evr, m);
  75         }
  76       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  77         return solver_dep_installed(solv, rd->evr);
  78     }
  79   FOR_PROVIDES(p, pp, dep)
  80     {
  81       if (MAPTST(m, p))
  82         return 1;
  83     }
  84   return 0;
  85 }
  86
  87 /*-----------------------------------------------------------------*/
  88
  89 /*
  90  * print rules
  91  */
  92
  93 static void
  94 printruleelement(Solver *solv, Rule *r, Id v)
  95 {
  96   Pool *pool = solv->pool;
  97   Solvable *s;
  98   if (v < 0)
  99     {
 100       s = pool->solvables + -v;
 101       printf("    !%s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), -v);
 102     }
 103   else
 104     {
 105       s = pool->solvables + v;
 106       printf("    %s-%s.%s [%d]", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), v);
 107     }
 108   if (r)
 109     {
 110       if (r->w1 == v)
 111         printf(" (w1)");
 112       if (r->w2 == v)
 113         printf(" (w2)");
 114     }
 115   if (solv->decisionmap[s - pool->solvables] > 0)
 116     printf(" Install.level%d", solv->decisionmap[s - pool->solvables]);
 117   if (solv->decisionmap[s - pool->solvables] < 0)
 118     printf(" Conflict.level%d", -solv->decisionmap[s - pool->solvables]);
 119   if (r && r->w1 == 0)
 120     printf(" (disabled)");
 121   printf("\n");
 122 }
 123
 124
 125 /*
 126  * print rule
 127  */
 128
 129 static void
 130 printrule(Solver *solv, Rule *r)
 131 {
 132   int i;
 133   Id v;
 134
 135   if (r >= solv->rules && r < solv->rules + solv->nrules)   /* r is a solver rule */
 136     printf("Rule #%d:\n", (int)(r - solv->rules));
 137   else
 138     printf("Rule:\n");                 /* r is any rule */
 139   for (i = 0; ; i++)
 140     {
 141       if (i == 0)
 142         v = r->p;
 143       else if (r->d == ID_NULL)
 144         {
 145           if (i == 2)
 146             break;
 147           v = r->w2;
 148         }
 149       else
 150         v = solv->pool->whatprovidesdata[r->d + i - 1];
 151       if (v == ID_NULL)
 152         break;
 153       printruleelement(solv, r, v);
 154     }
 155   printf("    next: %d %d\n", r->n1, r->n2);
 156 }
 157
 158
 159 /*-----------------------------------------------------------------*/
 160
 161 /*
 162  * Rule handling
 163  */
 164
 165 static Pool *unifyrules_sortcmp_data;
 166
 167 /*
 168  * compare rules for unification sort
 169  */
 170
 171 static int
 172 unifyrules_sortcmp(const void *ap, const void *bp)
 173 {
 174   Pool *pool = unifyrules_sortcmp_data;
 175   Rule *a = (Rule *)ap;
 176   Rule *b = (Rule *)bp;
 177   Id *ad, *bd;
 178   int x;
 179
 180   x = a->p - b->p;
 181   if (x)
 182     return x;                          /* p differs */
 183
 184   /* identical p */
 185   if (a->d == 0 && b->d == 0)
 186     return a->w2 - b->w2;              /* assertion: return w2 diff */
 187
 188   if (a->d == 0)                       /* a is assertion, b not */
 189     {
 190       x = a->w2 - pool->whatprovidesdata[b->d];
 191       return x ? x : -1;
 192     }
 193
 194   if (b->d == 0)                       /* b is assertion, a not */
 195     {
 196       x = pool->whatprovidesdata[a->d] - b->w2;
 197       return x ? x : 1;
 198     }
 199
 200   /* compare whatprovidesdata */
 201   ad = pool->whatprovidesdata + a->d;
 202   bd = pool->whatprovidesdata + b->d;
 203   while (*bd)
 204     if ((x = *ad++ - *bd++) != 0)
 205       return x;
 206   return *ad;
 207 }
 208
 209
 210 /*
 211  * unify rules
 212  */
 213
 214 static void
 215 unifyrules(Solver *solv)
 216 {
 217   int i, j;
 218   Rule *ir, *jr;
 219
 220   if (solv->nrules <= 1)               /* nothing to unify */
 221     return;
 222
 223   if (solv->pool->verbose > 3)
 224       printf ("----- unifyrules -----\n");
 225
 226   /* sort rules first */
 227   unifyrules_sortcmp_data = solv->pool;
 228   qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
 229
 230   /* prune rules
 231    * i = unpruned
 232    * j = pruned
 233    */
 234   jr = 0;
 235   for (i = j = 1, ir = solv->rules + 1; i < solv->nrules; i++, ir++)
 236     {
 237       if (jr && !unifyrules_sortcmp(ir, jr))
 238         continue;                      /* prune! */
 239       jr = solv->rules + j++;          /* keep! */
 240       if (ir != jr)
 241         *jr = *ir;
 242     }
 243
 244   /* reduced count from nrules to j rules */
 245   if (solv->pool->verbose) printf("pruned rules from %d to %d\n", solv->nrules, j);
 246
 247   /* adapt rule buffer */
 248   solv->rules = (Rule *)xrealloc(solv->rules, ((solv->nrules + RULES_BLOCK) & ~RULES_BLOCK) * sizeof(Rule));
 249   solv->nrules = j;
 250 #if 1
 251   if (solv->pool->verbose)
 252     {
 253       int binr = 0;
 254       int lits = 0;
 255       Id *dp;
 256       Rule *r;
 257
 258       for (i = 1; i < solv->nrules; i++)
 259         {
 260           r = solv->rules + i;
 261           if (r->d == 0)
 262             binr++;
 263           else
 264             {
 265               dp = solv->pool->whatprovidesdata + r->d;
 266               while (*dp++)
 267                 lits++;
 268             }
 269         }
 270       printf("  binary: %d\n", binr);
 271       printf("  normal: %d, %d literals\n", solv->nrules - 1 - binr, lits);
 272     }
 273 #endif
 274   if (solv->pool->verbose > 3)
 275       printf ("----- unifyrules end -----\n");
 276 }
 277
 278 #if 0
 279
 280 /*
 281  * hash rule
 282  */
 283
 284 static Hashval
 285 hashrule(Solver *solv, Id p, Id d, int n)
 286 {
 287   unsigned int x = (unsigned int)p;
 288   int *dp;
 289
 290   if (n <= 1)
 291     return (x * 37) ^ (unsigned int)d;
 292   dp = solv->pool->whatprovidesdata + d;
 293   while (*dp)
 294     x = (x * 37) ^ (unsigned int)*dp++;
 295   return x;
 296 }
 297 #endif
 298
 299
 300 /*
 301  * add rule
 302  *  p = direct literal; > 0 for learnt, < 0 for installed pkg (rpm)
 303  *  d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
 304  *
 305  *
 306  * A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
 307  *
 308  * p < 0 : rule from rpm (installed pkg)
 309  * d > 0 : Offset in whatprovidesdata (list of providers)
 310  *
 311  * A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
 312  *  d < 0: Id of solvable (e.g. B1)
 313  *
 314  * d == 0: unary rule, assertion => (A) or (-A)
 315  *
 316  *   Install:    p > 0, d = 0   (A)             user requested install
 317  *   Remove:     p < 0, d = 0   (-A)            user requested remove
 318  *   Requires:   p < 0, d > 0   (-A|B1|B2|...)  d: <list of providers for requirement of p>
 319  *   Updates:    p > 0, d > 0   (A|B1|B2|...)   d: <list of updates for solvable p>
 320  *   Conflicts:  p < 0, d < 0   (-A|-B)         either p (conflict issuer) or d (conflict provider)
 321  *   ?           p > 0, d < 0   (A|-B)
 322  *   No-op ?:    p = 0, d = 0   (null)          (used as policy rule placeholder)
 323  */
 324
 325 static Rule *
 326 addrule(Solver *solv, Id p, Id d)
 327 {
 328   Rule *r = 0;
 329   Id *dp = 0;
 330
 331   int n = 0;                           /* number of literals in rule - 1
 332                                           0 = direct assertion (single literal)
 333                                           1 = binary rule
 334                                         */
 335
 336   /* it often happenes that requires lead to adding the same rpm rule
 337    * multiple times, so we prune those duplicates right away to make
 338    * the work for unifyrules a bit easier */
 339
 340   if (solv->nrules && !solv->jobrules)
 341     {
 342       r = solv->rules + solv->nrules - 1;   /* get the last added rule */
 343       if (r->p == p && r->d == d && d != 0)   /* identical and not user requested */
 344         return r;
 345     }
 346
 347   if (d < 0)
 348     {
 349       if (p == d)
 350         return 0;                      /* ignore self conflict */
 351       n = 1;
 352     }
 353   else if (d == 0)                     /* user requested */
 354     n = 0;
 355   else
 356     {
 357       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, n++)
 358         if (*dp == -p)
 359           return 0;                     /* rule is self-fulfilling */
 360       if (n == 1)
 361         d = dp[-1];
 362     }
 363
 364   if (n == 0)                          /* direct assertion */
 365     {
 366       if (!solv->jobrules)
 367         {
 368           /* this is a rpm rule assertion, we do not have to allocate it */
 369           /* it can be identified by a level of 1 and a zero reason */
 370           /* we must not drop those rules from the decisionq when rewinding! */
 371           if (p > 0)
 372             abort();
 373           if (solv->decisionmap[-p] > 0 || solv->decisionmap[-p] < -1)
 374             abort();
 375           if (solv->decisionmap[-p])
 376             return NULL;
 377           queue_push(&solv->decisionq, p);
 378           queue_push(&solv->decisionq_why, 0);
 379           solv->decisionmap[-p] = -1;
 380           return 0;
 381         }
 382     }
 383   else if (n == 1 && p > d)
 384     {
 385       /* smallest literal first so we can find dups */
 386       n = p;
 387       p = d;
 388       d = n;
 389       n = 1;                           /* re-set n, was used as temp var */
 390     }
 391
 392   /* check if the last added rule is exactly the same as what we're looking for. */
 393   if (r && n == 1 && !r->d && r->p == p && r->w2 == d)
 394     return r;
 395
 396   if (r && n > 1 && r->d && r->p == p)
 397     {
 398       Id *dp2;
 399       if (d == r->d)
 400         return r;
 401       dp2 = solv->pool->whatprovidesdata + r->d;
 402       for (dp = solv->pool->whatprovidesdata + d; *dp; dp++, dp2++)
 403         if (*dp != *dp2)
 404           break;
 405       if (*dp == *dp2)
 406         return r;
 407    }
 408
 409   /*
 410    * allocate new rule
 411    */
 412
 413   /* check and extend rule buffer */
 414   if ((solv->nrules & RULES_BLOCK) == 0)
 415     {
 416       solv->rules = (Rule *)xrealloc(solv->rules, (solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
 417     }
 418
 419   r = solv->rules + solv->nrules++;    /* point to rule space */
 420
 421   r->p = p;
 422   if (n == 0)
 423     {
 424       /* direct assertion, no watch needed */
 425       r->d = 0;
 426       r->w1 = p;
 427       r->w2 = 0;
 428     }
 429   else if (n == 1)
 430     {
 431       /* binary rule */
 432       r->d = 0;
 433       r->w1 = p;
 434       r->w2 = d;
 435     }
 436   else
 437     {
 438       r->d = d;
 439       r->w1 = p;
 440       r->w2 = solv->pool->whatprovidesdata[d];
 441     }
 442   r->n1 = 0;
 443   r->n2 = 0;
 444
 445   if (solv->pool->verbose > 3)
 446     {
 447       printf ("  Add rule: ");
 448       printrule (solv, r);
 449     }
 450
 451   return r;
 452 }
 453
 454 static inline void
 455 disablerule(Solver *solv, Rule *r)
 456 {
 457   r->w1 = 0;
 458 }
 459
 460 static inline void
 461 enablerule(Solver *solv, Rule *r)
 462 {
 463   if (r->d == 0 || r->w2 != r->p)
 464     r->w1 = r->p;
 465   else
 466     r->w1 = solv->pool->whatprovidesdata[r->d];
 467 }
 468
 469
 470 /**********************************************************************************/
 471
 472 /* a problem is an item on the solver's problem list. It can either be >0, in that
 473  * case it is a system (upgrade) rule, or it can be <0, which makes it refer to a job
 474  * consisting of multiple job rules.
 475  */
 476
 477 static void
 478 disableproblem(Solver *solv, Id v)
 479 {
 480   Rule *r;
 481   int i;
 482   Id *jp;
 483
 484   if (v > 0)
 485     {
 486       disablerule(solv, solv->rules + v);
 487       return;
 488     }
 489   v = -(v + 1);
 490   jp = solv->ruletojob.elements;
 491   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 492     if (*jp == v)
 493       disablerule(solv, r);
 494 }
 495
 496 static void
 497 enableproblem(Solver *solv, Id v)
 498 {
 499   Rule *r;
 500   int i;
 501   Id *jp;
 502
 503   if (v > 0)
 504     {
 505       enablerule(solv, solv->rules + v);
 506       return;
 507     }
 508   v = -(v + 1);
 509   jp = solv->ruletojob.elements;
 510   for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 511     if (*jp == v)
 512       enablerule(solv, r);
 513 }
 514
 515 static void
 516 printproblem(Solver *solv, Id v)
 517 {
 518   int i;
 519   Rule *r;
 520   Id *jp;
 521
 522   if (v > 0)
 523     printrule(solv, solv->rules + v);
 524   else
 525     {
 526       v = -(v + 1);
 527       printf("JOB %d\n", v);
 528       jp = solv->ruletojob.elements;
 529       for (i = solv->jobrules, r = solv->rules + i; i < solv->systemrules; i++, r++, jp++)
 530         if (*jp == v)
 531           {
 532             printf(" -");
 533             printrule(solv, r);
 534           }
 535       printf("ENDJOB\n");
 536     }
 537 }
 538
 539
 540 /**********************************************************************************/
 541
 542 /* go through system and job rules and add direct assertions
 543  * to the decisionqueue. If we find a conflict, disable rules and
 544  * add them to problem queue.
 545  */
 546 static void
 547 makeruledecisions(Solver *solv)
 548 {
 549   int i, ri;
 550   Rule *r, *rr;
 551   Id v, vv;
 552   int decisionstart;
 553
 554   /* no learnt rules for now */
 555   if (solv->learntrules && solv->learntrules != solv->nrules)
 556     abort();
 557
 558   decisionstart = solv->decisionq.count;
 559   /* the loop is over jobrules, system rules and weak rules */
 560   for (ri = solv->jobrules, r = solv->rules + ri; ri < solv->nrules; ri++, r++)
 561     {
 562       if (!r->w1 || r->w2)
 563         continue;
 564       v = r->p;
 565       vv = v > 0 ? v : -v;
 566       if (solv->decisionmap[vv] == 0)
 567         {
 568           queue_push(&solv->decisionq, v);
 569           queue_push(&solv->decisionq_why, r - solv->rules);
 570           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 571           continue;
 572         }
 573       if (v > 0 && solv->decisionmap[vv] > 0)
 574         continue;
 575       if (v < 0 && solv->decisionmap[vv] < 0)
 576         continue;
 577       /* found a conflict! */
 578       /* if we are weak, just disable ourself */
 579       if (ri >= solv->weakrules)
 580         {
 581           printf("conflict, but I am weak, disabling ");
 582           printrule(solv, r);
 583           r->w1 = 0;
 584           continue;
 585         }
 586       /* only job and system rules left */
 587       for (i = 0; i < solv->decisionq.count; i++)
 588         if (solv->decisionq.elements[i] == -v)
 589           break;
 590       if (i == solv->decisionq.count)
 591         abort();
 592       if (solv->decisionq_why.elements[i] == 0)
 593         {
 594           /* conflict with rpm rule, need only disable our rule */
 595           printf("conflict with rpm rule, disabling rule #%d\n", ri);
 596           if (v < 0 && v != -SYSTEMSOLVABLE)
 597             abort();
 598           queue_push(&solv->problems, 0);
 599           if (v == -SYSTEMSOLVABLE)
 600             queue_push(&solv->problems, 0);     /* sigh, we don't have a rule for that */
 601           else
 602             queue_push(&solv->problems, -v);    /* sigh, we don't have a rule for that */
 603           v = ri;
 604           if (ri < solv->systemrules)
 605             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 606           queue_push(&solv->problems, v);
 607           disableproblem(solv, v);
 608           queue_push(&solv->problems, 0);
 609           continue;
 610         }
 611       /* conflict with another job or system rule */
 612       /* remove old decision */
 613       printf("conflicting system/job rules over literal %d\n", vv);
 614       queue_push(&solv->problems, 0);
 615       queue_push(&solv->problems, solv->decisionq_why.elements[i]);
 616       /* push all of our rules asserting this literal on the problem stack */
 617       for (i = solv->jobrules, rr = solv->rules + i; i < solv->nrules; i++, rr++)
 618         {
 619           if (!rr->w1 || rr->w2)
 620             continue;
 621           if (rr->p != v && rr->p != -v)
 622             continue;
 623           printf(" - disabling rule #%d\n", i);
 624           v = i;
 625           if (i < solv->systemrules)
 626             v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
 627           queue_push(&solv->problems, v);
 628           disableproblem(solv, v);
 629         }
 630       queue_push(&solv->problems, 0);
 631
 632       /* start over */
 633       while (solv->decisionq.count > decisionstart)
 634         {
 635           v = solv->decisionq.elements[--solv->decisionq.count];
 636           --solv->decisionq_why.count;
 637           vv = v > 0 ? v : -v;
 638           solv->decisionmap[vv] = 0;
 639         }
 640       ri = solv->jobrules - 1;
 641       r = solv->rules + ri;
 642     }
 643 }
 644
 645
 646 /* FIXME: bad code ahead, replace as soon as possible */
 647 static void
 648 disableupdaterules(Solver *solv, Queue *job, int jobidx)
 649 {
 650   Pool *pool = solv->pool;
 651   int i, j;
 652   Id how, what, p, *pp;
 653   Solvable *s;
 654   Repo *installed;
 655   Rule *r;
 656   Id lastjob = -1;
 657
 658   installed = solv->installed;
 659   if (!installed)
 660     return;
 661
 662   if (jobidx != -1)
 663     {
 664       how = job->elements[jobidx];
 665       switch(how)
 666         {
 667         case SOLVER_INSTALL_SOLVABLE:
 668         case SOLVER_ERASE_SOLVABLE:
 669         case SOLVER_ERASE_SOLVABLE_NAME:
 670         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 671           break;
 672         default:
 673           return;
 674         }
 675     }
 676   /* go through all enabled job rules */
 677   MAPZERO(&solv->noupdate);
 678   for (i = solv->jobrules; i < solv->systemrules; i++)
 679     {
 680       r = solv->rules + i;
 681       if (!r->w1)       /* disabled? */
 682         continue;
 683       j = solv->ruletojob.elements[i - solv->jobrules];
 684       if (j == lastjob)
 685         continue;
 686       lastjob = j;
 687       how = job->elements[j];
 688       what = job->elements[j + 1];
 689       switch(how)
 690         {
 691         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
 692           s = pool->solvables + what;
 693           FOR_PROVIDES(p, pp, s->name)
 694             {
 695               if (pool->solvables[p].name != s->name)
 696                 continue;
 697               if (pool->solvables[p].repo == installed)
 698                 MAPSET(&solv->noupdate, p - installed->start);
 699             }
 700           break;
 701         case SOLVER_ERASE_SOLVABLE:
 702           s = pool->solvables + what;
 703           if (s->repo == installed)
 704             MAPSET(&solv->noupdate, what - installed->start);
 705           break;
 706         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 707         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 708           FOR_PROVIDES(p, pp, what)
 709             {
 710               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 711                 continue;
 712               if (pool->solvables[p].repo == installed)
 713                 MAPSET(&solv->noupdate, p - installed->start);
 714             }
 715           break;
 716         default:
 717           break;
 718         }
 719     }
 720
 721   /* fixup update rule status */
 722   if (solv->allowuninstall)
 723     return;             /* no update rules at all */
 724
 725   if (jobidx != -1)
 726     {
 727       /* we just disabled job #jobidx. enable all update rules
 728        * that aren't disabled by the remaining job rules */
 729       how = job->elements[jobidx];
 730       what = job->elements[jobidx + 1];
 731       switch(how)
 732         {
 733         case SOLVER_INSTALL_SOLVABLE:
 734           s = pool->solvables + what;
 735           FOR_PROVIDES(p, pp, s->name)
 736             {
 737               if (pool->solvables[p].name != s->name)
 738                 continue;
 739               if (pool->solvables[p].repo != installed)
 740                 continue;
 741               if (MAPTST(&solv->noupdate, p - installed->start))
 742                 continue;
 743               r = solv->rules + solv->systemrules + (p - installed->start);
 744               if (r->w1)
 745                 continue;
 746               enablerule(solv, r);
 747               if (pool->verbose)
 748                 {
 749                   printf("@@@ re-enabling ");
 750                   printrule(solv, r);
 751                 }
 752             }
 753           break;
 754         case SOLVER_ERASE_SOLVABLE:
 755           s = pool->solvables + what;
 756           if (s->repo != installed)
 757             break;
 758           if (MAPTST(&solv->noupdate, what - installed->start))
 759             break;
 760           r = solv->rules + solv->systemrules + (what - installed->start);
 761           if (r->w1)
 762             break;
 763           enablerule(solv, r);
 764           if (pool->verbose)
 765             {
 766               printf("@@@ re-enabling ");
 767               printrule(solv, r);
 768             }
 769           break;
 770         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 771         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 772           FOR_PROVIDES(p, pp, what)
 773             {
 774               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 775                 continue;
 776               if (pool->solvables[p].repo != installed)
 777                 continue;
 778               if (MAPTST(&solv->noupdate, p - installed->start))
 779                 continue;
 780               r = solv->rules + solv->systemrules + (p - installed->start);
 781               if (r->w1)
 782                 continue;
 783               enablerule(solv, r);
 784               if (pool->verbose)
 785                 {
 786                   printf("@@@ re-enabling ");
 787                   printrule(solv, r);
 788                 }
 789             }
 790           break;
 791         default:
 792           break;
 793         }
 794       return;
 795     }
 796
 797   for (i = 0; i < installed->nsolvables; i++)
 798     {
 799       r = solv->rules + solv->systemrules + i;
 800       if (r->w1 && MAPTST(&solv->noupdate, i))
 801         r->w1 = 0;              /* was enabled, need to disable */
 802     }
 803 }
 804
 805
 806 /*
 807  * add (install) rules for solvable
 808  * for unfulfilled requirements, conflicts, obsoletes,....
 809  * "unflag" a resolvable if it is not installable via "addrule(solv, -n, 0)"
 810  */
 811
 812 static void
 813 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
 814 {
 815   Pool *pool = solv->pool;
 816   Repo *installed = solv->installed;
 817   Queue q;
 818   Id qbuf[64];
 819   int i;
 820   int dontfix;
 821   Id req, *reqp;
 822   Id con, *conp;
 823   Id obs, *obsp;
 824   Id rec, *recp;
 825   Id sug, *sugp;
 826   Id p, *pp;
 827   Id *dp;
 828   Id n;
 829
 830   if (solv->pool->verbose > 3)
 831     printf ("----- addrpmrulesforsolvable -----\n");
 832
 833   queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
 834   queue_push(&q, s - pool->solvables);  /* push solvable Id */
 835
 836   while (q.count)
 837     {
 838       /*
 839        * n: Id of solvable
 840        * s: Pointer to solvable
 841        */
 842
 843       n = queue_shift(&q);
 844       if (MAPTST(m, n))                /* continue if already done */
 845         continue;
 846
 847       MAPSET(m, n);
 848       s = pool->solvables + n;         /* s = Solvable in question */
 849
 850       dontfix = 0;
 851       if (installed                     /* Installed system available */
 852           && !solv->fixsystem           /* NOT repair errors in rpm dependency graph */
 853           && s->repo == installed)      /* solvable is installed? */
 854       {
 855         dontfix = 1;                   /* dont care about broken rpm deps */
 856       }
 857
 858       /*-----------------------------------------
 859        * check requires of s
 860        */
 861
 862       if (s->requires)
 863         {
 864           reqp = s->repo->idarraydata + s->requires;
 865           while ((req = *reqp++) != 0) /* go throw all requires */
 866             {
 867               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
 868                 continue;
 869
 870               dp = GET_PROVIDESP(req, p);       /* get providers of req; p is a dummy only */
 871
 872               if (*dp == SYSTEMSOLVABLE)        /* always installed */
 873                 continue;
 874
 875               if (dontfix)
 876                 {
 877                   /* the strategy here is to not insist on dependencies
 878                    * that are already broken. so if we find one provider
 879                    * that was already installed, we know that the
 880                    * dependency was not broken before so we enforce it */
 881                   for (i = 0; (p = dp[i]) != 0; i++)    /* for all providers */
 882                     {
 883                       if (pool->solvables[p].repo == installed)
 884                         break;          /* provider was installed */
 885                     }
 886                   if (!p)               /* previously broken dependency */
 887                     {
 888                       if (pool->verbose)
 889                         printf("ignoring broken requires %s of installed package %s-%s.%s\n", dep2str(pool, req), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
 890                       continue;
 891                     }
 892                 }
 893
 894               if (!*dp)
 895                 {
 896                   /* nothing provides req! */
 897                   if (pool->verbose)
 898                      printf("package %s-%s.%s [%d] is not installable (%s)\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), (Id)(s - pool->solvables), dep2str(pool, req));
 899                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
 900                   if (solv->rc_output)
 901                     printf(">!> !unflag %s-%s.%s[%s]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), repo_name(s->repo));
 902                   continue;
 903                 }
 904
 905               if (pool->verbose > 2)
 906                 {
 907                   printf("  %s-%s.%s requires %s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
 908                   for (i = 0; dp[i]; i++)
 909                     printf("   provided by %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));
 910                 }
 911
 912               /* add 'requires' dependency */
 913               /* rule: (-requestor|provider1|provider2|...|providerN) */
 914               addrule(solv, -n, dp - pool->whatprovidesdata);
 915
 916               /* descend the dependency tree */
 917               for (; *dp; dp++)   /* loop through all providers */
 918                 {
 919                   if (!MAPTST(m, *dp))
 920                     queue_push(&q, *dp);
 921                 }
 922
 923             } /* while, requirements of n */
 924
 925         } /* if, requirements */
 926
 927
 928       /*-----------------------------------------
 929        * check conflicts of s
 930        */
 931
 932       if (s->conflicts)
 933         {
 934           conp = s->repo->idarraydata + s->conflicts;
 935           while ((con = *conp++) != 0)
 936             {
 937               FOR_PROVIDES(p, pp, con)
 938                 {
 939                    /* dontfix: dont care about conflicts with already installed packs */
 940                   if (dontfix && pool->solvables[p].repo == installed)
 941                     continue;
 942                  /* rule: -n|-p: either solvable _or_ provider of conflict */
 943                   addrule(solv, -n, -p);
 944                 }
 945             }
 946         }
 947
 948       /*-----------------------------------------
 949        * check obsoletes if not installed
 950        */
 951       if (!installed || pool->solvables[n].repo != installed)
 952         {                              /* not installed */
 953           if (s->obsoletes)
 954             {
 955               obsp = s->repo->idarraydata + s->obsoletes;
 956               while ((obs = *obsp++) != 0)
 957                 {
 958                   FOR_PROVIDES(p, pp, obs)
 959                     addrule(solv, -n, -p);
 960                 }
 961             }
 962           FOR_PROVIDES(p, pp, s->name)
 963             {
 964               if (s->name == pool->solvables[p].name)
 965                 addrule(solv, -n, -p);
 966             }
 967         }
 968
 969       /*-----------------------------------------
 970        * add recommends to the rule list
 971        */
 972       if (s->recommends)
 973         {
 974           recp = s->repo->idarraydata + s->recommends;
 975           while ((rec = *recp++) != 0)
 976             {
 977               FOR_PROVIDES(p, pp, rec)
 978                 if (!MAPTST(m, p))
 979                   queue_push(&q, p);
 980             }
 981         }
 982       if (s->suggests)
 983         {
 984           sugp = s->repo->idarraydata + s->suggests;
 985           while ((sug = *sugp++) != 0)
 986             {
 987               FOR_PROVIDES(p, pp, sug)
 988                 if (!MAPTST(m, p))
 989                   queue_push(&q, p);
 990             }
 991         }
 992     }
 993   queue_free(&q);
 994 }
 995
 996 static void
 997 addrpmrulesforweak(Solver *solv, Map *m)
 998 {
 999   Pool *pool = solv->pool;
1000   Solvable *s;
1001   Id sup, *supp;
1002   int i, n;
1003
1004   if (pool->verbose) printf("----- addrpmrulesforweak ----- (nrules %d)\n", solv->nrules);
1005   for (i = n = 1; n < pool->nsolvables; i++, n++)
1006     {
1007       if (i == pool->nsolvables)
1008         i = 1;
1009       if (MAPTST(m, i))
1010         continue;
1011       s = pool->solvables + i;
1012       if (!pool_installable(pool, s))
1013         continue;
1014       sup = 0;
1015       if (s->supplements)
1016         {
1017           supp = s->repo->idarraydata + s->supplements;
1018           while ((sup = *supp++) != ID_NULL)
1019             if (dep_possible(solv, sup, m))
1020               break;
1021         }
1022       if (!sup && s->freshens)
1023         {
1024           supp = s->repo->idarraydata + s->freshens;
1025           while ((sup = *supp++) != ID_NULL)
1026             if (dep_possible(solv, sup, m))
1027               break;
1028         }
1029       if (!sup && s->enhances)
1030         {
1031           supp = s->repo->idarraydata + s->enhances;
1032           while ((sup = *supp++) != ID_NULL)
1033             if (dep_possible(solv, sup, m))
1034               break;
1035         }
1036       if (!sup)
1037         continue;
1038       addrpmrulesforsolvable(solv, s, m);
1039       n = 0;
1040     }
1041   if (pool->verbose) printf("----- addrpmrulesforweak ----- done. (nrules%d)\n", solv->nrules);
1042 }
1043
1044 static void
1045 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allowall)
1046 {
1047   Pool *pool = solv->pool;
1048   int i;
1049   Queue qs;
1050   Id qsbuf[64];
1051
1052   if (solv->pool->verbose > 3)
1053     printf ("----- addrpmrulesforupdaters -----\n");
1054
1055   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1056   policy_findupdatepackages(solv, s, &qs, allowall);
1057   if (!MAPTST(m, s - pool->solvables))  /* add rule for s if not already done */
1058     addrpmrulesforsolvable(solv, s, m);
1059   for (i = 0; i < qs.count; i++)
1060     if (!MAPTST(m, qs.elements[i]))
1061       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1062   queue_free(&qs);
1063 }
1064
1065 /*
1066  * add rule for update
1067  *   (A|A1|A2|A3...)  An = update candidates for A
1068  *
1069  * s = (installed) solvable
1070  */
1071
1072 static void
1073 addupdaterule(Solver *solv, Solvable *s, int allowall)
1074 {
1075   /* installed packages get a special upgrade allowed rule */
1076   Pool *pool = solv->pool;
1077   Id d;
1078   Queue qs;
1079   Id qsbuf[64];
1080
1081   if (solv->pool->verbose > 3)
1082     printf ("-----  addupdaterule -----\n");
1083
1084   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1085   policy_findupdatepackages(solv, s, &qs, allowall);
1086   if (qs.count == 0)                   /* no updaters found */
1087     d = 0;
1088   else
1089     d = pool_queuetowhatprovides(pool, &qs);    /* intern computed queue */
1090   queue_free(&qs);
1091   addrule(solv, s - pool->solvables, d);        /* allow update of s */
1092 }
1093
1094
1095 /*-----------------------------------------------------------------*/
1096 /* watches */
1097
1098
1099 /*
1100  * makewatches
1101  *
1102  * initial setup for all watches
1103  */
1104
1105 static void
1106 makewatches(Solver *solv)
1107 {
1108   Rule *r;
1109   int i;
1110   int nsolvables = solv->pool->nsolvables;
1111
1112   xfree(solv->watches);
1113                                        /* lower half for removals, upper half for installs */
1114   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1115 #if 1
1116   /* do it reverse so rpm rules get triggered first */
1117   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1118 #else
1119   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1120 #endif
1121     {
1122       if (!r->w1                       /* rule is disabled */
1123           || !r->w2)                   /* rule is assertion */
1124         continue;
1125
1126       /* see addwatches(solv, r) */
1127       r->n1 = solv->watches[nsolvables + r->w1];
1128       solv->watches[nsolvables + r->w1] = r - solv->rules;
1129
1130       r->n2 = solv->watches[nsolvables + r->w2];
1131       solv->watches[nsolvables + r->w2] = r - solv->rules;
1132     }
1133 }
1134
1135
1136 /*
1137  * add watches (for rule)
1138  */
1139
1140 static void
1141 addwatches(Solver *solv, Rule *r)
1142 {
1143   int nsolvables = solv->pool->nsolvables;
1144
1145   r->n1 = solv->watches[nsolvables + r->w1];
1146   solv->watches[nsolvables + r->w1] = r - solv->rules;
1147
1148   r->n2 = solv->watches[nsolvables + r->w2];
1149   solv->watches[nsolvables + r->w2] = r - solv->rules;
1150 }
1151
1152
1153 /*-----------------------------------------------------------------*/
1154 /* rule propagation */
1155
1156 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1157
1158 /*
1159  * propagate
1160  *
1161  * propagate decision to all rules
1162  */
1163
1164 static Rule *
1165 propagate(Solver *solv, int level)
1166 {
1167   Pool *pool = solv->pool;
1168   Id *rp, *nrp;
1169   Rule *r;
1170   Id p, pkg, ow;
1171   Id *dp;
1172   Id *decisionmap = solv->decisionmap;
1173   Id *watches = solv->watches + pool->nsolvables;
1174
1175   while (solv->propagate_index < solv->decisionq.count)
1176     {
1177       /* negate because our watches trigger if literal goes FALSE */
1178       pkg = -solv->decisionq.elements[solv->propagate_index++];
1179       if (pool->verbose > 3)
1180         {
1181           printf("popagate for decision %d level %d\n", -pkg, level);
1182           printruleelement(solv, 0, -pkg);
1183         }
1184
1185       for (rp = watches + pkg; *rp; rp = nrp)
1186         {
1187           r = solv->rules + *rp;
1188
1189           if (pool->verbose > 3)
1190             {
1191               printf("  watch triggered ");
1192               printrule(solv, r);
1193             }
1194
1195           if (pkg == r->w1)
1196             {
1197               ow = r->w2;
1198               nrp = &r->n1;
1199             }
1200           else
1201             {
1202               ow = r->w1;
1203               nrp = &r->n2;
1204             }
1205           /* if clause is TRUE, nothing to do */
1206           if (DECISIONMAP_TRUE(ow))
1207             continue;
1208
1209           if (r->d)
1210             {
1211               /* not a binary clause, check if we need to move our watch */
1212               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1213                 p = r->p;
1214               else
1215                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1216                   if (p != ow && !DECISIONMAP_TRUE(-p))
1217                     break;
1218               if (p)
1219                 {
1220                   /* p is free to watch, move watch to p */
1221                   if (pool->verbose > 3)
1222                     {
1223                       if (p > 0)
1224                         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));
1225                       else
1226                         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));
1227                     }
1228                   *rp = *nrp;
1229                   nrp = rp;
1230                   if (pkg == r->w1)
1231                     {
1232                       r->w1 = p;
1233                       r->n1 = watches[p];
1234                     }
1235                   else
1236                     {
1237                       r->w2 = p;
1238                       r->n2 = watches[p];
1239                     }
1240                   watches[p] = r - solv->rules;
1241                   continue;
1242                 }
1243             }
1244           /* unit clause found, set other watch to TRUE */
1245           if (DECISIONMAP_TRUE(-ow))
1246             return r;           /* eek, a conflict! */
1247           if (pool->verbose > 2)
1248             {
1249               printf("unit ");
1250               printrule(solv, r);
1251             }
1252           if (ow > 0)
1253             decisionmap[ow] = level;
1254           else
1255             decisionmap[-ow] = -level;
1256           queue_push(&solv->decisionq, ow);
1257           queue_push(&solv->decisionq_why, r - solv->rules);
1258           if (pool->verbose > 3)
1259             {
1260               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1261               if (ow > 0)
1262                 printf("  -> decided to install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1263               else
1264                 printf("  -> decided to conflict %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1265             }
1266         }
1267     }
1268   return 0;     /* all is well */
1269 }
1270
1271
1272 /*-----------------------------------------------------------------*/
1273 /* Analysis */
1274
1275 /*
1276  * analyze
1277  *   and learn
1278  */
1279
1280 static int
1281 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1282 {
1283   Pool *pool = solv->pool;
1284   Queue r;
1285   int rlevel = 1;
1286   Map seen;             /* global? */
1287   Id v, vv, *dp;
1288   int l, i, idx;
1289   int num = 0;
1290   int learnt_why = solv->learnt_pool.count;
1291   Id *decisionmap = solv->decisionmap;
1292
1293   queue_init(&r);
1294
1295   if (pool->verbose > 1) printf("ANALYZE at %d ----------------------\n", level);
1296   map_init(&seen, pool->nsolvables);
1297   idx = solv->decisionq.count;
1298   for (;;)
1299     {
1300       if (pool->verbose > 1) printrule(solv, c);
1301       queue_push(&solv->learnt_pool, c - solv->rules);
1302       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1303       for (i = -1; ; i++)
1304         {
1305           if (i == -1)
1306             v = c->p;
1307           else if (c->d == 0)
1308             v = i ? 0 : c->w2;
1309           else
1310             v = *dp++;
1311           if (v == 0)
1312             break;
1313           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1314               continue;
1315           vv = v > 0 ? v : -v;
1316           if (MAPTST(&seen, vv))
1317             continue;
1318           l = solv->decisionmap[vv];
1319           if (l < 0)
1320             l = -l;
1321           if (l == 1)
1322             {
1323 #if 0
1324               int j;
1325               for (j = 0; j < solv->decisionq.count; j++)
1326                 if (solv->decisionq.elements[j] == v)
1327                   break;
1328               if (j == solv->decisionq.count)
1329                 abort();
1330               queue_push(&rulq, -(j + 1));
1331 #endif
1332               continue;                 /* initial setting */
1333             }
1334           MAPSET(&seen, vv);
1335           if (l == level)
1336             num++;                      /* need to do this one as well */
1337           else
1338             {
1339               queue_push(&r, v);
1340               if (pool->verbose > 3)
1341                 {
1342                   printf("PUSH %d ", v);
1343                   printruleelement(solv, 0, v);
1344                 }
1345               if (l > rlevel)
1346                 rlevel = l;
1347             }
1348         }
1349       if (pool->verbose > 3)
1350         printf("num = %d\n", num);
1351       if (num <= 0)
1352         abort();
1353       for (;;)
1354         {
1355           v = solv->decisionq.elements[--idx];
1356           vv = v > 0 ? v : -v;
1357           if (MAPTST(&seen, vv))
1358             break;
1359         }
1360       c = solv->rules + solv->decisionq_why.elements[idx];
1361       MAPCLR(&seen, vv);
1362       if (--num == 0)
1363         break;
1364     }
1365   *pr = -v;
1366   if (r.count == 0)
1367     *dr = 0;
1368   else if (r.count == 1 && r.elements[0] < 0)
1369     *dr = r.elements[0];
1370   else
1371     *dr = pool_queuetowhatprovides(pool, &r);
1372   if (pool->verbose > 1)
1373     {
1374       printf("learned rule for level %d (am %d)\n", rlevel, level);
1375       printruleelement(solv, 0, -v);
1376       for (i = 0; i < r.count; i++)
1377         {
1378           v = r.elements[i];
1379           printruleelement(solv, 0, v);
1380         }
1381     }
1382   map_free(&seen);
1383   queue_push(&solv->learnt_pool, 0);
1384   if (pool->verbose > 3)
1385     {
1386       for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1387         {
1388           printf("learnt_why ");
1389           printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1390         }
1391     }
1392   if (why)
1393     *why = learnt_why;
1394   return rlevel;
1395 }
1396
1397
1398 /*
1399  * reset_solver
1400  * reset the solver decisions to right after the rpm rules.
1401  * called after rules have been enabled/disabled
1402  */
1403
1404 static void
1405 reset_solver(Solver *solv)
1406 {
1407   int i;
1408   Id v;
1409
1410   /* delete all learnt rules */
1411   solv->nrules = solv->learntrules;
1412   queue_empty(&solv->learnt_why);
1413   queue_empty(&solv->learnt_pool);
1414
1415   /* redo all direct rpm rule decisions */
1416   /* we break at the first decision with a why attached, this is
1417    * either a job/system rule assertion or a propagated decision */
1418   for (i = 0; i < solv->decisionq.count; i++)
1419     {
1420       v = solv->decisionq.elements[i];
1421       solv->decisionmap[v > 0 ? v : -v] = 0;
1422     }
1423   for (i = 0; i < solv->decisionq_why.count; i++)
1424     if (solv->decisionq_why.elements[i])
1425       break;
1426     else
1427       {
1428         v = solv->decisionq.elements[i];
1429         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1430       }
1431
1432   if (solv->pool->verbose > 1)
1433     printf("decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1434
1435   solv->decisionq_why.count = i;
1436   solv->decisionq.count = i;
1437   solv->recommends_index = -1;
1438   solv->propagate_index = 0;
1439
1440   /* redo all job/system decisions */
1441   makeruledecisions(solv);
1442   if (solv->pool->verbose > 1)
1443     printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
1444   /* recreate watches */
1445   makewatches(solv);
1446 }
1447
1448
1449 /*
1450  * analyze_unsolvable_rule
1451  */
1452
1453 static void
1454 analyze_unsolvable_rule(Solver *solv, Rule *r)
1455 {
1456   int i;
1457   Id why = r - solv->rules;
1458   if (solv->pool->verbose > 1)
1459     {
1460       if (why >= solv->jobrules && why < solv->systemrules)
1461         printf("JOB ");
1462       if (why >= solv->systemrules && why < solv->weakrules)
1463         printf("SYSTEM %d ", why - solv->systemrules);
1464       if (why >= solv->weakrules && why < solv->learntrules)
1465         printf("WEAK ");
1466       if (solv->learntrules && why >= solv->learntrules)
1467         printf("LEARNED ");
1468       printrule(solv, r);
1469     }
1470   if (solv->learntrules && why >= solv->learntrules)
1471     {
1472       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1473         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1474       return;
1475     }
1476   /* do not add rpm rules to problem */
1477   if (why < solv->jobrules)
1478     return;
1479   /* turn rule into problem */
1480   if (why >= solv->jobrules && why < solv->systemrules)
1481     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1482   /* return if problem already countains our rule */
1483   if (solv->problems.count)
1484     {
1485       for (i = solv->problems.count - 1; i >= 0; i--)
1486         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1487           break;
1488         else if (solv->problems.elements[i] == why)
1489           return;
1490     }
1491   queue_push(&solv->problems, why);
1492 }
1493
1494
1495 /*
1496  * analyze_unsolvable
1497  *
1498  * return: 1 - disabled some rules, try again
1499  *         0 - hopeless
1500  */
1501
1502 static int
1503 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1504 {
1505   Pool *pool = solv->pool;
1506   Rule *r;
1507   Map seen;             /* global to speed things up? */
1508   Id v, vv, *dp, why;
1509   int l, i, idx;
1510   Id *decisionmap = solv->decisionmap;
1511   int oldproblemcount;
1512   int lastweak;
1513
1514   if (pool->verbose > 1)
1515     printf("ANALYZE UNSOLVABLE ----------------------\n");
1516   oldproblemcount = solv->problems.count;
1517
1518   /* make room for conflicting rule */
1519   queue_push(&solv->problems, 0);
1520   queue_push(&solv->problems, 0);
1521
1522   r = cr;
1523   map_init(&seen, pool->nsolvables);
1524   analyze_unsolvable_rule(solv, r);
1525   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1526   for (i = -1; ; i++)
1527     {
1528       if (i == -1)
1529         v = r->p;
1530       else if (r->d == 0)
1531         v = i ? 0 : r->w2;
1532       else
1533         v = *dp++;
1534       if (v == 0)
1535         break;
1536       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1537           continue;
1538       vv = v > 0 ? v : -v;
1539       l = solv->decisionmap[vv];
1540       if (l < 0)
1541         l = -l;
1542       MAPSET(&seen, vv);
1543     }
1544   idx = solv->decisionq.count;
1545   while (idx > 0)
1546     {
1547       v = solv->decisionq.elements[--idx];
1548       vv = v > 0 ? v : -v;
1549       if (!MAPTST(&seen, vv))
1550         continue;
1551       why = solv->decisionq_why.elements[idx];
1552       if (!why)
1553         {
1554           if (pool->verbose > 3)
1555             {
1556               printf("RPM ");
1557               printruleelement(solv, 0, v);
1558             }
1559           continue;
1560         }
1561       r = solv->rules + why;
1562       analyze_unsolvable_rule(solv, r);
1563       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1564       for (i = -1; ; i++)
1565         {
1566           if (i == -1)
1567             v = r->p;
1568           else if (r->d == 0)
1569             v = i ? 0 : r->w2;
1570           else
1571             v = *dp++;
1572           if (v == 0)
1573             break;
1574           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1575               continue;
1576           vv = v > 0 ? v : -v;
1577           l = solv->decisionmap[vv];
1578           if (l < 0)
1579             l = -l;
1580           MAPSET(&seen, vv);
1581         }
1582     }
1583   map_free(&seen);
1584   queue_push(&solv->problems, 0);       /* mark end of this problem */
1585
1586   lastweak = 0;
1587   if (solv->weakrules != solv->learntrules)
1588     {
1589       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1590         {
1591           why = solv->problems.elements[i];
1592           if (why < solv->weakrules || why >= solv->learntrules)
1593             continue;
1594           if (!lastweak || lastweak < why)
1595             lastweak = why;
1596         }
1597     }
1598   if (lastweak)
1599     {
1600       /* disable last weak rule */
1601       solv->problems.count = oldproblemcount;
1602       r = solv->rules + lastweak;
1603       printf("disabling weak ");
1604       printrule(solv, r);
1605       r->w1 = 0;
1606       reset_solver(solv);
1607       return 1;
1608     }
1609
1610   /* patch conflicting rule data */
1611   if (cr - solv->rules >= solv->learntrules)
1612     {
1613       /* we have to store the rule internals for learnt rules
1614        * as they get freed for every solver run */
1615       solv->problems.elements[oldproblemcount] = cr->p;
1616       solv->problems.elements[oldproblemcount + 1] = cr->d;
1617     }
1618   else
1619     solv->problems.elements[oldproblemcount + 1] = cr - solv->rules;
1620
1621   if (disablerules)
1622     {
1623       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1624         disableproblem(solv, solv->problems.elements[i]);
1625       reset_solver(solv);
1626       return 1;
1627     }
1628   if (pool->verbose)
1629     printf("UNSOLVABLE\n");
1630   return 0;
1631 }
1632
1633
1634 /*-----------------------------------------------------------------*/
1635 /* Decision revert */
1636
1637 /*
1638  * revert
1639  * revert decision at level
1640  */
1641
1642 static void
1643 revert(Solver *solv, int level)
1644 {
1645   Id v, vv;
1646   while (solv->decisionq.count)
1647     {
1648       v = solv->decisionq.elements[solv->decisionq.count - 1];
1649       vv = v > 0 ? v : -v;
1650       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1651         break;
1652       if (solv->pool->verbose > 3)
1653         printf("reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1654       solv->decisionmap[vv] = 0;
1655       solv->decisionq.count--;
1656       solv->decisionq_why.count--;
1657       solv->propagate_index = solv->decisionq.count;
1658     }
1659   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1660     {
1661       solv->branches.count--;
1662       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1663         solv->branches.count--;
1664     }
1665   solv->recommends_index = -1;
1666 }
1667
1668
1669 /*
1670  * watch2onhighest - put watch2 on literal with highest level
1671  */
1672
1673 static inline void
1674 watch2onhighest(Solver *solv, Rule *r)
1675 {
1676   int l, wl = 0;
1677   Id v, *dp;
1678
1679   if (!r->d)
1680     return;     /* binary rule, both watches are set */
1681   dp = solv->pool->whatprovidesdata + r->d;
1682   while ((v = *dp++) != 0)
1683     {
1684       l = solv->decisionmap[v < 0 ? -v : v];
1685       if (l < 0)
1686         l = -l;
1687       if (l > wl)
1688         {
1689           r->w2 = dp[-1];
1690           wl = l;
1691         }
1692     }
1693 }
1694
1695
1696 /*
1697  * setpropagatelearn
1698  *
1699  * add free decision to decision q, increase level
1700  * propagate decision, return if no conflict.
1701  * in conflict case, analyze conflict rule, add resulting
1702  * rule to learnt rule set, make decision from learnt
1703  * rule (always unit) and re-propagate.
1704  */
1705
1706 static int
1707 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1708 {
1709   Rule *r;
1710   Id p, d;
1711   int l, why;
1712
1713   if (decision)
1714     {
1715       level++;
1716       if (decision > 0)
1717         solv->decisionmap[decision] = level;
1718       else
1719         solv->decisionmap[-decision] = -level;
1720       queue_push(&solv->decisionq, decision);
1721       queue_push(&solv->decisionq_why, 0);
1722     }
1723   for (;;)
1724     {
1725       r = propagate(solv, level);
1726       if (!r)
1727         break;
1728       if (level == 1)
1729         return analyze_unsolvable(solv, r, disablerules);
1730       printf("conflict with rule #%d\n", (int)(r - solv->rules));
1731       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1732       if (l >= level || l <= 0)
1733         abort();
1734       printf("reverting decisions (level %d -> %d)\n", level, l);
1735       level = l;
1736       revert(solv, level);
1737       r = addrule(solv, p, d);       /* p requires d */
1738       if (!r)
1739         abort();
1740       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1741         {
1742           printf("%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1743           abort();
1744         }
1745       queue_push(&solv->learnt_why, why);
1746       if (d)
1747         {
1748           /* at least 2 literals, needs watches */
1749           watch2onhighest(solv, r);
1750           addwatches(solv, r);
1751         }
1752       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1753       queue_push(&solv->decisionq, p);
1754       queue_push(&solv->decisionq_why, r - solv->rules);
1755       if (solv->pool->verbose > 1)
1756         {
1757           printf("decision: ");
1758           printruleelement(solv, 0, p);
1759           printf("new rule: ");
1760           printrule(solv, r);
1761         }
1762     }
1763   return level;
1764 }
1765
1766
1767 /*
1768  * install best package from the queue. We add an extra package, inst, if
1769  * provided. See comment in weak install section.
1770  */
1771 static int
1772 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1773 {
1774   Pool *pool = solv->pool;
1775   Id p;
1776   int i;
1777
1778   if (dq->count > 1 || inst)
1779     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1780
1781   i = 0;
1782   if (dq->count > 1)
1783     {
1784       /* choose the supplemented one */
1785       for (i = 0; i < dq->count; i++)
1786         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1787           break;
1788       if (i == dq->count)
1789         {
1790           for (i = 1; i < dq->count; i++)
1791             queue_push(&solv->branches, dq->elements[i]);
1792           queue_push(&solv->branches, -level);
1793           i = 0;
1794         }
1795     }
1796   p = dq->elements[i];
1797
1798   if (pool->verbose > 3)
1799     {
1800       Solvable *s = pool->solvables + p;
1801       printf("installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1802     }
1803
1804   return setpropagatelearn(solv, level, p, disablerules);
1805 }
1806
1807
1808 /*-----------------------------------------------------------------*/
1809 /* Main solver interface */
1810
1811
1812 /*
1813  * solver_create
1814  * create solver structure
1815  *
1816  * pool: all available solvables
1817  * installed: installed Solvables
1818  *
1819  *
1820  * Upon solving, rules are created to flag the Solvables
1821  * of the 'installed' Repo as installed.
1822  */
1823
1824 Solver *
1825 solver_create(Pool *pool, Repo *installed)
1826 {
1827   Solver *solv;
1828   solv = (Solver *)xcalloc(1, sizeof(Solver));
1829   solv->pool = pool;
1830   solv->installed = installed;
1831
1832   queue_init(&solv->ruletojob);
1833   queue_init(&solv->decisionq);
1834   queue_init(&solv->decisionq_why);
1835   queue_init(&solv->problems);
1836   queue_init(&solv->suggestions);
1837   queue_init(&solv->learnt_why);
1838   queue_init(&solv->learnt_pool);
1839   queue_init(&solv->branches);
1840
1841   map_init(&solv->recommendsmap, pool->nsolvables);
1842   map_init(&solv->suggestsmap, pool->nsolvables);
1843   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
1844   solv->recommends_index = 0;
1845
1846   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1847   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1848   memset(solv->rules, 0, sizeof(Rule));
1849   solv->nrules = 1;
1850
1851   return solv;
1852 }
1853
1854
1855 /*
1856  * solver_free
1857  */
1858
1859 void
1860 solver_free(Solver *solv)
1861 {
1862   queue_free(&solv->ruletojob);
1863   queue_free(&solv->decisionq);
1864   queue_free(&solv->decisionq_why);
1865   queue_free(&solv->learnt_why);
1866   queue_free(&solv->learnt_pool);
1867   queue_free(&solv->problems);
1868   queue_free(&solv->suggestions);
1869   queue_free(&solv->branches);
1870
1871   map_free(&solv->recommendsmap);
1872   map_free(&solv->suggestsmap);
1873   map_free(&solv->noupdate);
1874   xfree(solv->decisionmap);
1875   xfree(solv->rules);
1876   xfree(solv->watches);
1877   xfree(solv->weaksystemrules);
1878   xfree(solv->obsoletes);
1879   xfree(solv->obsoletes_data);
1880   xfree(solv);
1881 }
1882
1883
1884 /*-------------------------------------------------------*/
1885
1886 /*
1887  * run_solver
1888  *
1889  * all rules have been set up, now actually run the solver
1890  *
1891  */
1892
1893 static void
1894 run_solver(Solver *solv, int disablerules, int doweak)
1895 {
1896   Queue dq;
1897   int systemlevel;
1898   int level, olevel;
1899   Rule *r;
1900   int i, j, n;
1901   Solvable *s;
1902   Pool *pool = solv->pool;
1903   Id p, *dp;
1904
1905   if (pool->verbose > 3)
1906     {
1907       printf("number of rules: %d\n", solv->nrules);
1908       for (i = 0; i < solv->nrules; i++)
1909         printrule(solv, solv->rules + i);
1910     }
1911
1912   /* all new rules are learnt after this point */
1913   solv->learntrules = solv->nrules;
1914   /* crate watches lists */
1915   makewatches(solv);
1916
1917   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
1918
1919   /* start SAT algorithm */
1920   level = 1;
1921   systemlevel = level + 1;
1922   if (pool->verbose) printf("solving...\n");
1923
1924   queue_init(&dq);
1925   for (;;)
1926     {
1927       /*
1928        * propagate
1929        */
1930
1931       if (level == 1)
1932         {
1933           if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
1934           if ((r = propagate(solv, level)) != 0)
1935             {
1936               if (analyze_unsolvable(solv, r, disablerules))
1937                 continue;
1938               queue_free(&dq);
1939               return;
1940             }
1941         }
1942
1943       /*
1944        * installed packages
1945        */
1946
1947       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
1948         {
1949           if (!solv->updatesystem)
1950             {
1951               /* try to keep as many packages as possible */
1952               if (pool->verbose) printf("installing system packages\n");
1953               for (i = solv->installed->start, n = 0; ; i++)
1954                 {
1955                   if (n == solv->installed->nsolvables)
1956                     break;
1957                   if (i == solv->installed->end)
1958                     i = solv->installed->start;
1959                   s = pool->solvables + i;
1960                   if (s->repo != solv->installed)
1961                     continue;
1962                   n++;
1963                   if (solv->decisionmap[i] != 0)
1964                     continue;
1965                   if (pool->verbose > 3)
1966                     printf("keeping %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1967                   olevel = level;
1968                   level = setpropagatelearn(solv, level, i, disablerules);
1969                   if (level == 0)
1970                     {
1971                       queue_free(&dq);
1972                       return;
1973                     }
1974                   if (level <= olevel)
1975                     n = 0;
1976                 }
1977             }
1978           if (solv->weaksystemrules)
1979             {
1980               if (pool->verbose) printf("installing weak system packages\n");
1981               for (i = solv->installed->start; i < solv->installed->end; i++)
1982                 {
1983                   if (pool->solvables[i].repo != solv->installed)
1984                     continue;
1985                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
1986                     continue;
1987                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
1988                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
1989                     continue;
1990                   queue_empty(&dq);
1991                   if (solv->weaksystemrules[i - solv->installed->start])
1992                     {
1993                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
1994                       while ((p = *dp++) != 0)
1995                         {
1996                           if (solv->decisionmap[p] > 0)
1997                             break;
1998                           if (solv->decisionmap[p] == 0)
1999                             queue_push(&dq, p);
2000                         }
2001                       if (p)
2002                         continue;       /* update package already installed */
2003                     }
2004                   if (!dq.count && solv->decisionmap[i] != 0)
2005                     continue;
2006                   olevel = level;
2007                   /* FIXME: i is handled a bit different because we do not want
2008                    * to have it pruned just because it is not recommened.
2009                    * we should not prune installed packages instead */
2010                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2011                   if (level == 0)
2012                     {
2013                       queue_free(&dq);
2014                       return;
2015                     }
2016                   if (level <= olevel)
2017                     break;
2018                 }
2019               if (i < solv->installed->end)
2020                 continue;
2021             }
2022           systemlevel = level;
2023         }
2024
2025       /*
2026        * decide
2027        */
2028
2029       if (pool->verbose) printf("deciding unresolved rules\n");
2030       for (i = 1, n = 1; ; i++, n++)
2031         {
2032           if (n == solv->nrules)
2033             break;
2034           if (i == solv->nrules)
2035             i = 1;
2036           r = solv->rules + i;
2037           if (!r->w1)
2038             continue;
2039           queue_empty(&dq);
2040           if (r->d == 0)
2041             {
2042               /* binary or unary rule */
2043               /* need two positive undecided literals */
2044               if (r->p < 0 || r->w2 <= 0)
2045                 continue;
2046               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2047                 continue;
2048               queue_push(&dq, r->p);
2049               queue_push(&dq, r->w2);
2050             }
2051           else
2052             {
2053               /* make sure that
2054                * all negative literals are installed
2055                * no positive literal is installed
2056                * i.e. the rule is not fulfilled and we
2057                * just need to decide on the positive literals
2058                */
2059               if (r->p < 0)
2060                 {
2061                   if (solv->decisionmap[-r->p] <= 0)
2062                     continue;
2063                 }
2064               else
2065                 {
2066                   if (solv->decisionmap[r->p] > 0)
2067                     continue;
2068                   if (solv->decisionmap[r->p] == 0)
2069                     queue_push(&dq, r->p);
2070                 }
2071               dp = pool->whatprovidesdata + r->d;
2072               while ((p = *dp++) != 0)
2073                 {
2074                   if (p < 0)
2075                     {
2076                       if (solv->decisionmap[-p] <= 0)
2077                         break;
2078                     }
2079                   else
2080                     {
2081                       if (solv->decisionmap[p] > 0)
2082                         break;
2083                       if (solv->decisionmap[p] == 0)
2084                         queue_push(&dq, p);
2085                     }
2086                 }
2087               if (p)
2088                 continue;
2089             }
2090           if (dq.count < 2)
2091             {
2092               /* cannot happen as this means that
2093                * the rule is unit */
2094               printrule(solv, r);
2095               abort();
2096             }
2097           if (pool->verbose > 2)
2098             printrule(solv, r);
2099
2100           olevel = level;
2101           level = selectandinstall(solv, level, &dq, 0, disablerules);
2102           if (level == 0)
2103             {
2104               queue_free(&dq);
2105               return;
2106             }
2107           if (level < systemlevel)
2108             break;
2109           n = 0;
2110         } /* for(), decide */
2111
2112       if (n != solv->nrules)    /* continue if level < systemlevel */
2113         continue;
2114
2115       if (doweak && !solv->problems.count)
2116         {
2117           int qcount;
2118
2119           if (pool->verbose) printf("installing recommended packages\n");
2120           queue_empty(&dq);
2121           for (i = 1; i < pool->nsolvables; i++)
2122             {
2123               if (solv->decisionmap[i] < 0)
2124                 continue;
2125               if (solv->decisionmap[i] > 0)
2126                 {
2127                   Id *recp, rec, *pp, p;
2128                   s = pool->solvables + i;
2129                   /* installed, check for recommends */
2130                   /* XXX need to special case AND ? */
2131                   if (s->recommends)
2132                     {
2133                       recp = s->repo->idarraydata + s->recommends;
2134                       while ((rec = *recp++) != 0)
2135                         {
2136                           qcount = dq.count;
2137                           FOR_PROVIDES(p, pp, rec)
2138                             {
2139                               if (solv->decisionmap[p] > 0)
2140                                 {
2141                                   dq.count = qcount;
2142                                   break;
2143                                 }
2144                               else if (solv->decisionmap[p] == 0)
2145                                 {
2146                                   queue_pushunique(&dq, p);
2147                                 }
2148                             }
2149                         }
2150                     }
2151                 }
2152               else
2153                 {
2154                   s = pool->solvables + i;
2155                   if (!s->supplements && !s->freshens)
2156                     continue;
2157                   if (!pool_installable(pool, s))
2158                     continue;
2159                   if (solver_is_supplementing(solv, s))
2160                     queue_pushunique(&dq, i);
2161                 }
2162             }
2163           if (dq.count)
2164             {
2165               if (dq.count > 1)
2166                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2167               p = dq.elements[0];
2168               s = pool->solvables + p;
2169               if (pool->verbose > 0)
2170                 printf("installing recommended %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2171               level = setpropagatelearn(solv, level, p, 0);
2172               continue;
2173             }
2174         }
2175
2176      if (solv->solution_callback)
2177         {
2178           solv->solution_callback(solv, solv->solution_callback_data);
2179           if (solv->branches.count)
2180             {
2181               int i = solv->branches.count - 1;
2182               int l = -solv->branches.elements[i];
2183               for (; i > 0; i--)
2184                 if (solv->branches.elements[i - 1] < 0)
2185                   break;
2186               p = solv->branches.elements[i];
2187               if (pool->verbose > 0)
2188                 {
2189                   s = pool->solvables + p;
2190                   printf("branching with %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2191                 }
2192               queue_empty(&dq);
2193               for (j = i + 1; j < solv->branches.count; j++)
2194                 queue_push(&dq, solv->branches.elements[j]);
2195               solv->branches.count = i;
2196               level = l;
2197               revert(solv, level);
2198               if (dq.count > 1)
2199                 for (j = 0; j < dq.count; j++)
2200                   queue_push(&solv->branches, dq.elements[j]);
2201               olevel = level;
2202               level = setpropagatelearn(solv, level, p, disablerules);
2203               if (level == 0)
2204                 {
2205                   queue_free(&dq);
2206                   return;
2207                 }
2208               continue;
2209             }
2210           /* all branches done, we're finally finished */
2211           break;
2212         }
2213
2214       /* minimization step */
2215      if (solv->branches.count)
2216         {
2217           int l = 0, lasti = -1, lastl = -1;
2218           p = 0;
2219           for (i = solv->branches.count - 1; i >= 0; i--)
2220             {
2221               p = solv->branches.elements[i];
2222               if (p < 0)
2223                 l = -p;
2224               else if (p > 0 && solv->decisionmap[p] > l + 1)
2225                 {
2226                   lasti = i;
2227                   lastl = l;
2228                 }
2229             }
2230           if (lasti >= 0)
2231             {
2232               /* kill old solvable so that we do not loop */
2233               p = solv->branches.elements[lasti];
2234               solv->branches.elements[lasti] = 0;
2235               s = pool->solvables + p;
2236               if (pool->verbose > 0)
2237                 printf("minimizing %d -> %d with %s-%s.%s\n", solv->decisionmap[p], l, id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2238
2239               level = lastl;
2240               revert(solv, level);
2241               olevel = level;
2242               level = setpropagatelearn(solv, level, p, disablerules);
2243               if (level == 0)
2244                 {
2245                   queue_free(&dq);
2246                   return;
2247                 }
2248               continue;
2249             }
2250         }
2251       break;
2252     }
2253   queue_free(&dq);
2254 }
2255
2256
2257 /*
2258  * refine_suggestion
2259  * at this point, all rules that led to conflicts are disabled.
2260  * we re-enable all rules of a problem set but rule "sug", then
2261  * continue to disable more rules until there as again a solution.
2262  */
2263
2264 /* FIXME: think about conflicting assertions */
2265
2266 static void
2267 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2268 {
2269   Pool *pool = solv->pool;
2270   Rule *r;
2271   int i, j;
2272   Id v;
2273   Queue disabled;
2274   int disabledcnt;
2275
2276   if (pool->verbose)
2277     {
2278       printf("refine_suggestion start\n");
2279       for (i = 0; problem[i]; i++)
2280         {
2281           if (problem[i] == sug)
2282             printf("=> ");
2283           printproblem(solv, problem[i]);
2284         }
2285     }
2286   queue_init(&disabled);
2287   queue_empty(refined);
2288   queue_push(refined, sug);
2289
2290   /* re-enable all problem rules with the exception of "sug" */
2291   revert(solv, 1);
2292   reset_solver(solv);
2293
2294   for (i = 0; problem[i]; i++)
2295     if (problem[i] != sug)
2296       enableproblem(solv, problem[i]);
2297
2298   if (sug < 0)
2299     disableupdaterules(solv, job, -(sug + 1));
2300
2301   for (;;)
2302     {
2303       /* re-enable as many weak rules as possible */
2304       for (i = solv->weakrules; i < solv->learntrules; i++)
2305         {
2306           r = solv->rules + i;
2307           if (!r->w1)
2308             enablerule(solv, r);
2309         }
2310
2311       queue_empty(&solv->problems);
2312       revert(solv, 1);          /* XXX move to reset_solver? */
2313       reset_solver(solv);
2314       run_solver(solv, 0, 0);
2315       if (!solv->problems.count)
2316         {
2317           if (pool->verbose)
2318             printf("no more problems!\n");
2319           if (pool->verbose > 3)
2320             printdecisions(solv);
2321           break;                /* great, no more problems */
2322         }
2323       disabledcnt = disabled.count;
2324       /* skip over problem rule */
2325       for (i = 2; i < solv->problems.count - 1; i++)
2326         {
2327           /* ignore solutions in refined */
2328           v = solv->problems.elements[i];
2329           for (j = 0; problem[j]; j++)
2330             if (problem[j] != sug && problem[j] == v)
2331               break;
2332           if (problem[j])
2333             continue;
2334           queue_push(&disabled, v);
2335         }
2336       if (disabled.count == disabledcnt)
2337         {
2338           /* no solution found, this was an invalid suggestion! */
2339           if (pool->verbose)
2340             printf("no solution found!\n");
2341           refined->count = 0;
2342           break;
2343         }
2344       if (disabled.count == disabledcnt + 1)
2345         {
2346           /* just one suggestion, add it to refined list */
2347           v = disabled.elements[disabledcnt];
2348           queue_push(refined, v);
2349           disableproblem(solv, v);
2350           if (v < 0)
2351             disableupdaterules(solv, job, -(v + 1));
2352         }
2353       else
2354         {
2355           /* more than one solution, disable all */
2356           /* do not push anything on refine list */
2357           if (pool->verbose > 1)
2358             {
2359               printf("more than one solution found:\n");
2360               for (i = disabledcnt; i < disabled.count; i++)
2361                 printproblem(solv, disabled.elements[i]);
2362             }
2363           for (i = disabledcnt; i < disabled.count; i++)
2364             disableproblem(solv, disabled.elements[i]);
2365         }
2366     }
2367   /* all done, get us back into the same state as before */
2368   /* enable refined rules again */
2369   for (i = 0; i < disabled.count; i++)
2370     enableproblem(solv, disabled.elements[i]);
2371   /* disable problem rules again */
2372   for (i = 0; problem[i]; i++)
2373     disableproblem(solv, problem[i]);
2374   if (pool->verbose)
2375     printf("refine_suggestion end\n");
2376 }
2377
2378 static void
2379 problems_to_solutions(Solver *solv, Queue *job)
2380 {
2381   Pool *pool = solv->pool;
2382   Queue problems;
2383   Queue solution;
2384   Queue solutions;
2385   Id *problem;
2386   Id why;
2387   int i, j;
2388
2389   if (!solv->problems.count)
2390     return;
2391   queue_clone(&problems, &solv->problems);
2392   queue_init(&solution);
2393   queue_init(&solutions);
2394   /* copy over problem rule */
2395   queue_push(&solutions, problems.elements[0]);
2396   queue_push(&solutions, problems.elements[1]);
2397   problem = problems.elements + 2;
2398   for (i = 2; i < problems.count; i++)
2399     {
2400       Id v = problems.elements[i];
2401       if (v == 0)
2402         {
2403           /* mark end of this problem */
2404           queue_push(&solutions, 0);
2405           queue_push(&solutions, 0);
2406           if (i + 1 == problems.count)
2407             break;
2408           /* copy over problem rule of next problem */
2409           queue_push(&solutions, problems.elements[i + 1]);
2410           queue_push(&solutions, problems.elements[i + 2]);
2411           i += 2;
2412           problem = problems.elements + i + 1;
2413           continue;
2414         }
2415       refine_suggestion(solv, job, problem, v, &solution);
2416       if (!solution.count)
2417         continue;       /* this solution didn't work out */
2418
2419       for (j = 0; j < solution.count; j++)
2420         {
2421           why = solution.elements[j];
2422 #if 0
2423           printproblem(solv, why);
2424 #endif
2425           if (why < 0)
2426             {
2427               queue_push(&solutions, 0);
2428               queue_push(&solutions, -why);
2429             }
2430           else if (why >= solv->systemrules && why < solv->weakrules)
2431             {
2432               Id p, rp = 0;
2433               p = solv->installed->start + (why - solv->systemrules);
2434               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2435                 {
2436                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2437                   for (; *dp; dp++)
2438                     {
2439                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2440                         continue;
2441                       if (solv->decisionmap[*dp] > 0)
2442                         {
2443                           rp = *dp;
2444                           break;
2445                         }
2446                     }
2447                 }
2448               queue_push(&solutions, p);
2449               queue_push(&solutions, rp);
2450             }
2451           else
2452             abort();
2453         }
2454       /* mark end of this solution */
2455       queue_push(&solutions, 0);
2456       queue_push(&solutions, 0);
2457     }
2458   queue_free(&solution);
2459   queue_free(&problems);
2460   /* copy queue over to solutions */
2461   queue_free(&solv->problems);
2462   queue_clone(&solv->problems, &solutions);
2463   queue_free(&solutions);
2464 }
2465
2466
2467
2468 /*
2469  * printdecisions
2470  */
2471
2472 static const char *
2473 id2rc(Solver *solv, Id id)
2474 {
2475   const char *evr;
2476   if (solv->rc_output != 2)
2477     return "";
2478   evr = id2str(solv->pool, id);
2479   if (*evr < '0' || *evr > '9')
2480     return "0:";
2481   while (*evr >= '0' && *evr <= '9')
2482     evr++;
2483   if (*evr != ':')
2484     return "0:";
2485   return "";
2486 }
2487
2488 void
2489 printdecisions(Solver *solv)
2490 {
2491   Pool *pool = solv->pool;
2492   Repo *installed = solv->installed;
2493   Id p, *obsoletesmap;
2494   int i;
2495   Solvable *s;
2496
2497   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2498   if (installed)
2499     {
2500       for (i = 0; i < solv->decisionq.count; i++)
2501         {
2502           Id *pp, n;
2503
2504           n = solv->decisionq.elements[i];
2505           if (n < 0)
2506             continue;
2507           if (n == SYSTEMSOLVABLE)
2508             continue;
2509           s = pool->solvables + n;
2510           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2511             continue;
2512           FOR_PROVIDES(p, pp, s->name)
2513             if (s->name == pool->solvables[p].name)
2514               {
2515                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2516                   {
2517                     obsoletesmap[p] = n;
2518                     obsoletesmap[n]++;
2519                   }
2520               }
2521         }
2522       for (i = 0; i < solv->decisionq.count; i++)
2523         {
2524           Id obs, *obsp;
2525           Id *pp, n;
2526
2527           n = solv->decisionq.elements[i];
2528           if (n < 0)
2529             continue;
2530           if (n == SYSTEMSOLVABLE)
2531             continue;
2532           s = pool->solvables + n;
2533           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2534             continue;
2535           if (!s->obsoletes)
2536             continue;
2537           obsp = s->repo->idarraydata + s->obsoletes;
2538           while ((obs = *obsp++) != 0)
2539             FOR_PROVIDES(p, pp, obs)
2540               {
2541                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2542                   {
2543                     obsoletesmap[p] = n;
2544                     obsoletesmap[n]++;
2545                   }
2546               }
2547         }
2548     }
2549
2550   if (solv->rc_output)
2551     printf(">!> Solution #1:\n");
2552
2553   int installs = 0, uninstalls = 0, upgrades = 0;
2554
2555   /* print solvables to be erased */
2556
2557   if (installed)
2558     {
2559       for (i = installed->start; i < installed->end; i++)
2560         {
2561           s = pool->solvables + i;
2562           if (s->repo != installed)
2563             continue;
2564           if (solv->decisionmap[i] > 0)
2565             continue;
2566           if (obsoletesmap[i])
2567             continue;
2568           if (solv->rc_output == 2)
2569             printf(">!> remove  %s-%s%s\n", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2570           else if (solv->rc_output)
2571             printf(">!> remove  %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2572           else
2573             printf("erase   %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2574           uninstalls++;
2575         }
2576     }
2577
2578   /* print solvables to be installed */
2579
2580   for (i = 0; i < solv->decisionq.count; i++)
2581     {
2582       int j;
2583       p = solv->decisionq.elements[i];
2584       if (p < 0)
2585         continue;
2586       if (p == SYSTEMSOLVABLE)
2587         continue;
2588       s = pool->solvables + p;
2589       if (installed && s->repo == installed)
2590         continue;
2591
2592       if (!obsoletesmap[p])
2593         {
2594           if (solv->rc_output)
2595             printf(">!> ");
2596           printf("install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2597           if (solv->rc_output != 2)
2598             printf(".%s", id2str(pool, s->arch));
2599           installs++;
2600         }
2601       else if (!solv->rc_output)
2602         {
2603           printf("update  %s-%s.%s  (obsoletes", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2604           for (j = installed->start; j < installed->end; j++)
2605             {
2606               if (obsoletesmap[j] != p)
2607                 continue;
2608               s = pool->solvables + j;
2609               printf(" %s-%s.%s", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2610             }
2611           printf(")");
2612           upgrades++;
2613         }
2614       else
2615         {
2616           Solvable *f, *fn = 0;
2617           for (j = installed->start; j < installed->end; j++)
2618             {
2619               if (obsoletesmap[j] != p)
2620                 continue;
2621               f = pool->solvables + j;
2622               if (fn || f->name != s->name)
2623                 {
2624                   if (solv->rc_output == 2)
2625                     printf(">!> remove  %s-%s%s\n", id2str(pool, f->name), id2rc(solv, f->evr), id2str(pool, f->evr));
2626                   else if (solv->rc_output)
2627                     printf(">!> remove  %s-%s.%s\n", id2str(pool, f->name), id2str(pool, f->evr), id2str(pool, f->arch));
2628                   uninstalls++;
2629                 }
2630               else
2631                 fn = f;
2632             }
2633           if (!fn)
2634             {
2635               printf(">!> install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2636               if (solv->rc_output != 2)
2637                 printf(".%s", id2str(pool, s->arch));
2638               installs++;
2639             }
2640           else
2641             {
2642               if (solv->rc_output == 2)
2643                 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));
2644               else
2645                 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));
2646               upgrades++;
2647             }
2648         }
2649       if (solv->rc_output)
2650         {
2651           Repo *repo = s->repo;
2652           if (repo && strcmp(repo_name(repo), "locales"))
2653             printf("[%s]", repo_name(repo));
2654         }
2655       printf("\n");
2656     }
2657
2658   if (solv->rc_output)
2659     printf(">!> installs=%d, upgrades=%d, uninstalls=%d\n", installs, upgrades, uninstalls);
2660
2661   xfree(obsoletesmap);
2662
2663   if (solv->suggestions.count)
2664     {
2665       printf("\nsuggested packages:\n");
2666       for (i = 0; i < solv->suggestions.count; i++)
2667         {
2668           s = pool->solvables + solv->suggestions.elements[i];
2669           printf("- %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2670         }
2671     }
2672 }
2673
2674 int
2675 printconflicts(Solver *solv, Solvable *s, Id pc)
2676 {
2677   Pool *pool = solv->pool;
2678   Solvable *sc = pool->solvables + pc;
2679   Id p, *pp, con, *conp, obs, *obsp;
2680   int numc = 0;
2681
2682   if (s->conflicts)
2683     {
2684       conp = s->repo->idarraydata + s->conflicts;
2685       while ((con = *conp++) != 0)
2686         {
2687           FOR_PROVIDES(p, pp, con)
2688             {
2689               if (p != pc)
2690                 continue;
2691               printf("packags %s-%s.%s conflicts with %s, which is provided by %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, con), id2str(pool, sc->name), id2str(pool, sc->evr), id2str(pool, sc->arch));
2692               numc++;
2693             }
2694         }
2695     }
2696   if (s->obsoletes && (!solv->installed || s->repo != solv->installed))
2697     {
2698       obsp = s->repo->idarraydata + s->obsoletes;
2699       while ((obs = *obsp++) != 0)
2700         {
2701           FOR_PROVIDES(p, pp, obs)
2702             {
2703               if (p != pc)
2704                 continue;
2705               printf("packags %s-%s.%s obsolets %s, which is provided by %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, obs), id2str(pool, sc->name), id2str(pool, sc->evr), id2str(pool, sc->arch));
2706               numc++;
2707             }
2708         }
2709     }
2710   return numc;
2711 }
2712
2713 void
2714 printprobleminfo(Solver *solv, Id p, Id d, Queue *job, Id firstp, Id firstrp)
2715 {
2716   Pool *pool = solv->pool;
2717   Rule *r;
2718   Solvable *s;
2719   Id what;
2720
2721   if (p != 0)
2722     {
2723       /* learnt rule, ignore for now */
2724       printf("some learnt rule...\n");
2725       return;
2726     }
2727   if (d == 0)
2728     {
2729       /* conflict with system solvable, i.e. could not create rule */
2730       if (firstp)
2731         {
2732           printf("got firstp\n");
2733           abort();
2734         }
2735       what = job->elements[firstrp];
2736       switch (job->elements[firstrp - 1])
2737         {
2738         case SOLVER_INSTALL_SOLVABLE_NAME:
2739           printf("no solvable exists with name %s\n", dep2str(pool, what));
2740           break;
2741         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2742           printf("no solvable provides %s\n", dep2str(pool, what));
2743           break;
2744         default:
2745           printf("unknown  job\n");
2746           abort();
2747         }
2748       return;
2749     }
2750   else if (d < 0)
2751     {
2752       Id req, *reqp, *dp;
2753       int count = 0;
2754       /* conflict with rpm rule, package -d is not installable */
2755       s = pool->solvables + (-d);
2756       if (s->requires)
2757         {
2758           reqp = s->repo->idarraydata + s->requires;
2759           while ((req = *reqp++) != 0)
2760             {
2761               if (req == SOLVABLE_PREREQMARKER)
2762                 continue;
2763               dp = GET_PROVIDESP(req, p);
2764               if (*dp)
2765                 continue;
2766               printf("package %s-%s.%s requires %s, but no package provides it\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
2767               count++;
2768             }
2769         }
2770       if (!count)
2771         printf("package %s-%s.%s is not installable\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2772       return;
2773     }
2774   if (d >= solv->jobrules)
2775     {
2776       r = solv->rules + d;
2777       p = r->p;
2778       d = r->d;
2779       if (p < 0 && d < 0)
2780         {
2781           Solvable *sp, *sd;
2782           sp = pool->solvables + (-p);
2783           sd = pool->solvables + (-d);
2784           printf("package %s-%s.%s cannot be installed with package %s-%s.%s\n", id2str(pool, sp->name), id2str(pool, sp->evr), id2str(pool, sp->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2785           return;
2786         }
2787       printf("some job rule...\n");
2788       printrule(solv, r);
2789       return;
2790     }
2791   r = solv->rules + d;
2792   p = r->p;
2793   if (p >= 0)
2794     abort();
2795   d = r->d;
2796   if (d == 0 && r->w2 < 0)
2797     {
2798       Solvable *sp, *sd;
2799       d = r->w2;
2800       sp = pool->solvables + (-p);
2801       sd = pool->solvables + (-d);
2802       if (sp->name == sd->name)
2803         {
2804           printf("cannot install both %s-%s.%s and %s-%s.%s\n", id2str(pool, sp->name), id2str(pool, sp->evr), id2str(pool, sp->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2805         }
2806       else
2807         {
2808           printconflicts(solv, pool->solvables + (-p), -d);
2809           printconflicts(solv, pool->solvables + (-d), -p);
2810         }
2811     }
2812   else
2813     {
2814       /* find requires of p that corresponds with our rule */
2815       Id req, *reqp, *dp;
2816       s = pool->solvables + (-p);
2817       reqp = s->repo->idarraydata + s->requires;
2818       while ((req = *reqp++) != 0)
2819         {
2820           if (req == SOLVABLE_PREREQMARKER)
2821             continue;
2822           dp = GET_PROVIDESP(req, p);
2823           if (d == 0)
2824             {
2825               if (*dp == r->w2 && dp[1] == 0)
2826                 break;
2827             }
2828           else if (dp - pool->whatprovidesdata == d)
2829             break;
2830         }
2831       if (!req)
2832         {
2833           printf("req not found\n");
2834           abort();
2835         }
2836       printf("package %s-%s.%s requires %s, but none of its providers can be installed\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
2837     }
2838 }
2839
2840 void
2841 printsolutions(Solver *solv, Queue *job)
2842 {
2843   Pool *pool = solv->pool;
2844   int pcnt;
2845   int i;
2846   Id p, d, rp, what;
2847   Solvable *s, *sd;
2848
2849   printf("Encountered problems! Here are the solutions:\n\n");
2850   pcnt = 1;
2851   for (i = 0; i < solv->problems.count; )
2852     {
2853       printf("Problem %d:\n", pcnt++);
2854       printf("====================================\n");
2855       p = solv->problems.elements[i++];
2856       d = solv->problems.elements[i++];
2857       printprobleminfo(solv, p, d, job, solv->problems.elements[i], solv->problems.elements[i + 1]);
2858       printf("\n");
2859       for (;;)
2860         {
2861           if (solv->problems.elements[i] == 0 && solv->problems.elements[i + 1] == 0)
2862             {
2863               /* end of solutions for this problems reached */
2864               i += 2;
2865               break;
2866             }
2867           for (;;)
2868             {
2869               p = solv->problems.elements[i];
2870               rp = solv->problems.elements[i + 1];
2871               i += 2;
2872               if (p == 0 && rp == 0)
2873                 {
2874                   /* end of this solution reached */
2875                   printf("\n");
2876                   break;
2877                 }
2878               if (p == 0)
2879                 {
2880                   /* job, p is index into job queue */
2881                   what = job->elements[rp];
2882                   switch (job->elements[rp - 1])
2883                     {
2884                     case SOLVER_INSTALL_SOLVABLE:
2885                       s = pool->solvables + what;
2886                       if (solv->installed && s->repo == solv->installed)
2887                         printf("- do not keep %s-%s.%s installed\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2888                       else
2889                         printf("- do not install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2890                       break;
2891                     case SOLVER_ERASE_SOLVABLE:
2892                       s = pool->solvables + what;
2893                       if (solv->installed && s->repo == solv->installed)
2894                         printf("- do not deinstall %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2895                       else
2896                         printf("- do not forbid installation of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2897                       break;
2898                     case SOLVER_INSTALL_SOLVABLE_NAME:
2899                       printf("- do not install %s\n", id2str(pool, what));
2900                       break;
2901                     case SOLVER_ERASE_SOLVABLE_NAME:
2902                       printf("- do not deinstall %s\n", id2str(pool, what));
2903                       break;
2904                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2905                       printf("- do not install a solvable providing %s\n", dep2str(pool, what));
2906                       break;
2907                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
2908                       printf("- do not deinstall all solvables providing %s\n", dep2str(pool, what));
2909                       break;
2910                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
2911                       s = pool->solvables + what;
2912                       printf("- do not install most recent version of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool
2913     , s->arch));
2914                       break;
2915                     default:
2916                       printf("- do something different\n");
2917                       break;
2918                     }
2919                 }
2920               else
2921                 {
2922                   /* policy, replace p with rp */
2923                   s = pool->solvables + p;
2924                   sd = rp ? pool->solvables + rp : 0;
2925                   if (sd)
2926                     {
2927                       int gotone = 0;
2928                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr) > 0)
2929                         {
2930                           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));
2931                           gotone = 1;
2932                         }
2933                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(pool, s, sd))
2934                         {
2935                           printf("- allow architecture change 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));
2936                           gotone = 1;
2937                         }
2938                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(pool, s, sd))
2939                         {
2940                           if (sd->vendor)
2941                             printf("- allow vendor change from '%s' (%s-%s.%s) to '%s' (%s-%s.%s)\n", id2str(pool, s->vendor), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->vendor), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2942                           else
2943                             printf("- allow vendor change from '%s' (%s-%s.%s) to no vendor (%s-%s.%s)\n", id2str(pool, s->vendor), id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), id2str(pool, sd->name), id2str(pool, sd->evr), id2str(pool, sd->arch));
2944                           gotone = 1;
2945                         }
2946                       if (!gotone)
2947                         printf("- allow replacement of %s-%s.%s with %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));
2948                     }
2949                   else
2950                     {
2951                       printf("- allow deinstallation of %s-%s.%s [%d]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), (Id)(s - pool->solvables));
2952                     }
2953
2954                 }
2955             }
2956         }
2957     }
2958 }
2959
2960
2961 /* for each installed solvable find which packages with *different* names
2962  * obsolete the solvable.
2963  * this index is used in policy_findupdatepackages if noupdateprovide is set.
2964  */
2965
2966 static void
2967 create_obsolete_index(Solver *solv)
2968 {
2969   Pool *pool = solv->pool;
2970   Solvable *s;
2971   Repo *installed = solv->installed;
2972   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
2973   int i, n;
2974
2975   if (!installed || !installed->nsolvables)
2976     return;
2977   /* create reverse obsoletes map for installed solvables */
2978   solv->obsoletes = obsoletes = xcalloc(installed->end - installed->start, sizeof(Id));
2979   for (i = 1; i < pool->nsolvables; i++)
2980     {
2981       s = pool->solvables + i;
2982       if (s->repo == installed)
2983         continue;
2984       if (!s->obsoletes)
2985         continue;
2986       if (!pool_installable(pool, s))
2987         continue;
2988       obsp = s->repo->idarraydata + s->obsoletes;
2989       while ((obs = *obsp++) != 0)
2990         FOR_PROVIDES(p, pp, obs)
2991           {
2992             if (pool->solvables[p].repo != installed)
2993               continue;
2994             if (pool->solvables[p].name == s->name)
2995               continue;
2996             obsoletes[p - installed->start]++;
2997           }
2998     }
2999   n = 0;
3000   for (i = 0; i < installed->nsolvables; i++)
3001     if (obsoletes[i])
3002       {
3003         n += obsoletes[i] + 1;
3004         obsoletes[i] = n;
3005       }
3006   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
3007   if (pool->verbose) printf("obsoletes data: %d entries\n", n + 1);
3008   for (i = pool->nsolvables - 1; i > 0; i--)
3009     {
3010       s = pool->solvables + i;
3011       if (!s->obsoletes)
3012         continue;
3013       if (!pool_installable(pool, s))
3014         continue;
3015       obsp = s->repo->idarraydata + s->obsoletes;
3016       while ((obs = *obsp++) != 0)
3017         FOR_PROVIDES(p, pp, obs)
3018           {
3019             if (pool->solvables[p].repo != installed)
3020               continue;
3021             if (pool->solvables[p].name == s->name)
3022               continue;
3023             p -= installed->start;
3024             if (obsoletes_data[obsoletes[p]] != i)
3025               obsoletes_data[--obsoletes[p]] = i;
3026           }
3027     }
3028 }
3029
3030
3031 /*-----------------------------------------------------------------*/
3032 /* main() */
3033
3034 /*
3035  *
3036  * solve job queue
3037  *
3038  */
3039
3040 void
3041 solve(Solver *solv, Queue *job)
3042 {
3043   Pool *pool = solv->pool;
3044   Repo *installed = solv->installed;
3045   int i;
3046   Map addedmap;                        /* '1' == have rule for solvable */
3047   Id how, what, p, *pp, d;
3048   Queue q;
3049   Solvable *s;
3050
3051   /* create obsolete index if needed */
3052   if (solv->noupdateprovide)
3053     create_obsolete_index(solv);
3054
3055   /*
3056    * create basic rule set of all involved packages
3057    * use addedmap bitmap to make sure we don't create rules twice
3058    *
3059    */
3060
3061   map_init(&addedmap, pool->nsolvables);
3062   queue_init(&q);
3063
3064   /*
3065    * always install our system solvable
3066    */
3067   MAPSET(&addedmap, SYSTEMSOLVABLE);
3068   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3069   queue_push(&solv->decisionq_why, 0);
3070   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3071
3072   /*
3073    * create rules for all package that could be involved with the solving
3074    * so called: rpm rules
3075    *
3076    */
3077   if (installed)
3078     {
3079       if (pool->verbose > 3)
3080         printf ("*** create rules for installed solvables ***\n");
3081       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3082         if (s->repo == installed)
3083           addrpmrulesforsolvable(solv, s, &addedmap);
3084       if (pool->verbose > 3)
3085         printf ("*** create rules for updaters of installed solvables ***\n");
3086       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3087         if (s->repo == installed)
3088           addrpmrulesforupdaters(solv, s, &addedmap, 1);
3089     }
3090
3091   if (solv->pool->verbose > 3)
3092     printf ("*** create rpm rules for packages involved with a job ***\n");
3093   for (i = 0; i < job->count; i += 2)
3094     {
3095       how = job->elements[i];
3096       what = job->elements[i + 1];
3097
3098       switch(how)
3099         {
3100         case SOLVER_INSTALL_SOLVABLE:
3101           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3102           break;
3103         case SOLVER_INSTALL_SOLVABLE_NAME:
3104         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3105           FOR_PROVIDES(p, pp, what)
3106             {
3107               /* if by name, ensure that the name matches */
3108               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3109                 continue;
3110               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3111             }
3112           break;
3113         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3114           /* dont allow downgrade */
3115           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3116           break;
3117         }
3118     }
3119
3120   if (solv->pool->verbose > 3)
3121     printf ("*** create rpm rules for recommended/suggested packages ***\n");
3122   if (solv->pool->verbose > 3)
3123       printf ("*** Add rules for week dependencies ***\n");
3124
3125
3126   addrpmrulesforweak(solv, &addedmap);
3127
3128 #if 1
3129   if (pool->verbose)
3130     {
3131       int possible = 0, installable = 0;
3132       for (i = 1; i < pool->nsolvables; i++)
3133         {
3134           if (pool_installable(pool, pool->solvables + i))
3135             installable++;
3136           if (MAPTST(&addedmap, i))
3137             possible++;
3138         }
3139       printf("%d of %d installable solvables considered for solving\n", possible, installable);
3140     }
3141 #endif
3142
3143   /*
3144    * first pass done, we now have all the rpm rules we need.
3145    * unify existing rules before going over all job rules and
3146    * policy rules.
3147    * at this point the system is always solvable,
3148    * as an empty system (remove all packages) is a valid solution
3149    */
3150
3151   unifyrules(solv);     /* remove duplicate rpm rules */
3152
3153   if (pool->verbose) printf("Decisions based on %d rpm rules.\n", solv->decisionq.count);
3154
3155   /*
3156    * now add all job rules
3157    */
3158
3159   if (solv->pool->verbose > 3)
3160       printf ("*** Add JOB rules ***\n");
3161
3162   solv->jobrules = solv->nrules;
3163
3164   for (i = 0; i < job->count; i += 2)
3165     {
3166       how = job->elements[i];
3167       what = job->elements[i + 1];
3168       switch(how)
3169         {
3170         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3171           s = pool->solvables + what;
3172           if (solv->rc_output)
3173             {
3174               printf(">!> Installing %s from channel %s\n", id2str(pool, s->name), repo_name(s->repo));
3175             }
3176           if (pool->verbose)
3177             printf("job: install solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3178           addrule(solv, what, 0);                       /* install by Id */
3179           queue_push(&solv->ruletojob, i);
3180           break;
3181         case SOLVER_ERASE_SOLVABLE:
3182           s = pool->solvables + what;
3183           if (pool->verbose)
3184             printf("job: erase solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3185           addrule(solv, -what, 0);                      /* remove by Id */
3186           queue_push(&solv->ruletojob, i);
3187           break;
3188         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3189         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3190           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_NAME)
3191             printf("job: install name %s\n", id2str(pool, what));
3192           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3193             printf("job: install provides %s\n", dep2str(pool, what));
3194           queue_empty(&q);
3195           FOR_PROVIDES(p, pp, what)
3196             {
3197               /* if by name, ensure that the name matches */
3198               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3199                 continue;
3200               queue_push(&q, p);
3201             }
3202           if (!q.count)
3203             {
3204               /* no provider, make this an impossible rule */
3205               queue_push(&q, -SYSTEMSOLVABLE);
3206             }
3207
3208           p = queue_shift(&q);         /* get first provider */
3209           if (!q.count)
3210             d = 0;                     /* single provider ? -> make assertion */
3211           else
3212             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3213           addrule(solv, p, d);         /* add 'requires' rule */
3214           queue_push(&solv->ruletojob, i);
3215           break;
3216         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3217         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3218           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_NAME)
3219             printf("job: erase name %s\n", id2str(pool, what));
3220           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3221             printf("job: erase provides %s\n", dep2str(pool, what));
3222           FOR_PROVIDES(p, pp, what)
3223             {
3224               /* if by name, ensure that the name matches */
3225               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3226                 continue;
3227               addrule(solv, -p, 0);  /* add 'remove' rule */
3228               queue_push(&solv->ruletojob, i);
3229             }
3230           break;
3231         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3232           s = pool->solvables + what;
3233           if (pool->verbose)
3234             printf("job: update %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3235           addupdaterule(solv, s, 0);
3236           queue_push(&solv->ruletojob, i);
3237           break;
3238         }
3239     }
3240
3241   if (solv->ruletojob.count != solv->nrules - solv->jobrules)
3242     abort();
3243
3244   /*
3245    * now add system rules
3246    *
3247    */
3248
3249  if (solv->pool->verbose > 3)
3250      printf ("*** Add system rules ***\n");
3251
3252
3253   solv->systemrules = solv->nrules;
3254
3255   /*
3256    * create rules for updating installed solvables
3257    *
3258    */
3259
3260   if (installed && !solv->allowuninstall)
3261     {                                  /* loop over all installed solvables */
3262       /* we create all update rules, but disable some later on depending on the job */
3263       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3264         if (s->repo == installed)
3265           addupdaterule(solv, s, 0);
3266         else
3267           addupdaterule(solv, 0, 0);    /* create dummy rule */
3268       /* consistency check: we added a rule for _every_ system solvable */
3269       if (solv->nrules - solv->systemrules != installed->end - installed->start)
3270         abort();
3271     }
3272
3273   /* create special weak system rules */
3274   /* those are used later on to keep a version of the installed packages in
3275      best effort mode */
3276   if (installed && installed->nsolvables)
3277     {
3278       solv->weaksystemrules = xcalloc(installed->end - installed->start, sizeof(Id));
3279       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3280         if (s->repo == installed)
3281           {
3282             policy_findupdatepackages(solv, s, &q, 1);
3283             if (q.count)
3284               solv->weaksystemrules[i - installed->start] = pool_queuetowhatprovides(pool, &q);
3285           }
3286     }
3287
3288   /* free unneeded memory */
3289   map_free(&addedmap);
3290   queue_free(&q);
3291
3292   solv->weakrules = solv->nrules;
3293
3294   /* try real hard to keep packages installed */
3295   if (0)
3296     {
3297       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3298         if (s->repo == installed)
3299           {
3300             /* FIXME: can't work with refine_suggestion! */
3301             /* need to always add the rule but disable it */
3302             if (MAPTST(&solv->noupdate, i - installed->start))
3303               continue;
3304             d = solv->weaksystemrules[i - installed->start];
3305             addrule(solv, i, d);
3306           }
3307     }
3308
3309   /*
3310    * solve !
3311    *
3312    */
3313
3314   disableupdaterules(solv, job, -1);
3315   makeruledecisions(solv);
3316
3317   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
3318
3319   run_solver(solv, 1, 1);
3320
3321   /* find suggested packages */
3322   if (!solv->problems.count)
3323     {
3324       Id sug, *sugp, p, *pp;
3325
3326       /* create map of all suggests that are still open */
3327       solv->recommends_index = -1;
3328       MAPZERO(&solv->suggestsmap);
3329       for (i = 0; i < solv->decisionq.count; i++)
3330         {
3331           p = solv->decisionq.elements[i];
3332           if (p < 0)
3333             continue;
3334           s = pool->solvables + p;
3335           if (s->suggests)
3336             {
3337               sugp = s->repo->idarraydata + s->suggests;
3338               while ((sug = *sugp++) != 0)
3339                 {
3340                   FOR_PROVIDES(p, pp, sug)
3341                     if (solv->decisionmap[p] > 0)
3342                       break;
3343                   if (p)
3344                     continue;   /* already fulfilled */
3345                   FOR_PROVIDES(p, pp, sug)
3346                     MAPSET(&solv->suggestsmap, p);
3347                 }
3348             }
3349         }
3350       for (i = 1; i < pool->nsolvables; i++)
3351         {
3352           if (solv->decisionmap[i] != 0)
3353             continue;
3354           s = pool->solvables + i;
3355           if (!MAPTST(&solv->suggestsmap, i))
3356             {
3357               if (!s->enhances)
3358                 continue;
3359               if (!pool_installable(pool, s))
3360                 continue;
3361               if (!solver_is_enhancing(solv, s))
3362                 continue;
3363             }
3364           queue_push(&solv->suggestions, i);
3365         }
3366       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3367     }
3368
3369   if (solv->problems.count)
3370     problems_to_solutions(solv, job);
3371 }
3372