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 (!dep_installed(solv, rd->name))
  44             return 0;
  45           return dep_installed(solv, rd->evr);
  46         }
  47       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  48         return dep_installed(solv, rd->evr);
  49     }
  50   FOR_PROVIDES(p, pp, dep)
  51     {
  52       if (p >= solv->installed->start && p < solv->installed->start + solv->installed->nsolvables)
  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 (p >= installed->start && p < installed->start + installed->nsolvables)
 698                 MAPSET(&solv->noupdate, p - installed->start);
 699             }
 700           break;
 701         case SOLVER_ERASE_SOLVABLE:
 702           if (what >= installed->start && what < installed->start + installed->nsolvables)
 703             MAPSET(&solv->noupdate, what - installed->start);
 704           break;
 705         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 706         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 707           FOR_PROVIDES(p, pp, what)
 708             {
 709               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 710                 continue;
 711               if (p >= installed->start && p < installed->start + installed->nsolvables)
 712                 MAPSET(&solv->noupdate, p - installed->start);
 713             }
 714           break;
 715         default:
 716           break;
 717         }
 718     }
 719
 720   /* fixup update rule status */
 721   if (solv->allowuninstall)
 722     return;             /* no update rules at all */
 723
 724   if (jobidx != -1)
 725     {
 726       /* re just disabled job #jobidx. enable all update rules
 727        * that aren't disabled by the remaining job rules */
 728       how = job->elements[jobidx];
 729       what = job->elements[jobidx + 1];
 730       switch(how)
 731         {
 732         case SOLVER_INSTALL_SOLVABLE:
 733           s = pool->solvables + what;
 734           FOR_PROVIDES(p, pp, s->name)
 735             {
 736               if (pool->solvables[p].name != s->name)
 737                 continue;
 738               if (p < installed->start || p >= installed->start + installed->nsolvables)
 739                 continue;
 740               if (MAPTST(&solv->noupdate, p - installed->start))
 741                 continue;
 742               r = solv->rules + solv->systemrules + (p - installed->start);
 743               if (r->w1)
 744                 continue;
 745               if (r->d == 0 || r->w2 != r->p)
 746                 r->w1 = r->p;
 747               else
 748                 r->w1 = solv->pool->whatprovidesdata[r->d];
 749               if (pool->verbose)
 750                 {
 751                   printf("@@@ re-enabling ");
 752                   printrule(solv, r);
 753                 }
 754             }
 755           break;
 756         case SOLVER_ERASE_SOLVABLE:
 757           if (what < installed->start || what >= installed->start + installed->nsolvables)
 758             break;
 759           if (MAPTST(&solv->noupdate, what - installed->start))
 760             break;
 761           r = solv->rules + solv->systemrules + (what - installed->start);
 762           if (r->w1)
 763             break;
 764           if (r->d == 0 || r->w2 != r->p)
 765             r->w1 = r->p;
 766           else
 767             r->w1 = solv->pool->whatprovidesdata[r->d];
 768           if (pool->verbose)
 769             {
 770               printf("@@@ re-enabling ");
 771               printrule(solv, r);
 772             }
 773           break;
 774         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
 775         case SOLVER_ERASE_SOLVABLE_PROVIDES:
 776           FOR_PROVIDES(p, pp, what)
 777             {
 778               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
 779                 continue;
 780               if (p < installed->start || p >= installed->start + installed->nsolvables)
 781                 continue;
 782               if (MAPTST(&solv->noupdate, p - installed->start))
 783                 continue;
 784               r = solv->rules + solv->systemrules + (p - installed->start);
 785               if (r->w1)
 786                 continue;
 787               if (r->d == 0 || r->w2 != r->p)
 788                 r->w1 = r->p;
 789               else
 790                 r->w1 = solv->pool->whatprovidesdata[r->d];
 791               if (pool->verbose)
 792                 {
 793                   printf("@@@ re-enabling ");
 794                   printrule(solv, r);
 795                 }
 796             }
 797           break;
 798         default:
 799           break;
 800         }
 801       return;
 802     }
 803
 804   for (i = 0; i < installed->nsolvables; i++)
 805     {
 806       r = solv->rules + solv->systemrules + i;
 807       if (r->w1 && MAPTST(&solv->noupdate, i))
 808         r->w1 = 0;              /* was enabled, need to disable */
 809     }
 810 }
 811
 812
 813 /*
 814  * add (install) rules for solvable
 815  * for unfulfilled requirements, conflicts, obsoletes,....
 816  * "unflag" a resolvable if it is not installable via "addrule(solv, -n, 0)"
 817  */
 818
 819 static void
 820 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
 821 {
 822   Pool *pool = solv->pool;
 823   Repo *installed = solv->installed;
 824   Queue q;
 825   Id qbuf[64];
 826   int i;
 827   int dontfix;
 828   Id req, *reqp;
 829   Id con, *conp;
 830   Id obs, *obsp;
 831   Id rec, *recp;
 832   Id sug, *sugp;
 833   Id p, *pp;
 834   Id *dp;
 835   Id n;
 836
 837   if (solv->pool->verbose > 3)
 838     printf ("----- addrpmrulesforsolvable -----\n");
 839
 840   queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
 841   queue_push(&q, s - pool->solvables);  /* push solvable Id */
 842
 843   while (q.count)
 844     {
 845       /*
 846        * n: Id of solvable
 847        * s: Pointer to solvable
 848        */
 849
 850       n = queue_shift(&q);
 851       if (MAPTST(m, n))                /* continue if already done */
 852         continue;
 853
 854       MAPSET(m, n);
 855       s = pool->solvables + n;         /* s = Solvable in question */
 856
 857       dontfix = 0;
 858       if (installed                     /* Installed system available */
 859           && !solv->fixsystem           /* NOT repair errors in rpm dependency graph */
 860           && n >= installed->start      /* is it installed? */
 861           && n < installed->start + installed->nsolvables)
 862       {
 863         dontfix = 1;                   /* dont care about broken rpm deps */
 864       }
 865
 866       /*-----------------------------------------
 867        * check requires of s
 868        */
 869
 870       if (s->requires)
 871         {
 872           reqp = s->repo->idarraydata + s->requires;
 873           while ((req = *reqp++) != 0) /* go throw all requires */
 874             {
 875               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
 876                 continue;
 877
 878               dp = GET_PROVIDESP(req, p);       /* get providers of req; p is a dummy only */
 879
 880               if (*dp == SYSTEMSOLVABLE)        /* always installed */
 881                 continue;
 882
 883               if (dontfix)
 884                 {
 885                   /* the strategy here is to not insist on dependencies
 886                    * that are already broken. so if we find one provider
 887                    * that was already installed, we know that the
 888                    * dependency was not broken before so we enforce it */
 889                   for (i = 0; dp[i]; i++)       /* for all providers */
 890                     {
 891                       if (dp[i] >= installed->start && dp[i] < installed->start + installed->nsolvables)
 892                         break;          /* provider was installed */
 893                     }
 894                   if (!dp[i])           /* previously broken dependency */
 895                     {
 896                       if (pool->verbose)
 897                         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));
 898                       continue;
 899                     }
 900                 }
 901
 902               if (!*dp)
 903                 {
 904                   /* nothing provides req! */
 905                   if (pool->verbose)
 906                      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));
 907                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
 908                   if (solv->rc_output)
 909                     printf(">!> !unflag %s-%s.%s[%s]\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), repo_name(s->repo));
 910                   continue;
 911                 }
 912
 913               if (pool->verbose > 2)
 914                 {
 915                   printf("  %s-%s.%s requires %s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch), dep2str(pool, req));
 916                   for (i = 0; dp[i]; i++)
 917                     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));
 918                 }
 919
 920               /* add 'requires' dependency */
 921               /* rule: (-requestor|provider1|provider2|...|providerN) */
 922               addrule(solv, -n, dp - pool->whatprovidesdata);
 923
 924               /* descend the dependency tree */
 925               for (; *dp; dp++)   /* loop through all providers */
 926                 {
 927                   if (!MAPTST(m, *dp))
 928                     queue_push(&q, *dp);
 929                 }
 930
 931             } /* while, requirements of n */
 932
 933         } /* if, requirements */
 934
 935
 936       /*-----------------------------------------
 937        * check conflicts of s
 938        */
 939
 940       if (s->conflicts)
 941         {
 942           conp = s->repo->idarraydata + s->conflicts;
 943           while ((con = *conp++) != 0)
 944             {
 945               FOR_PROVIDES(p, pp, con)
 946                 {
 947                    /* dontfix: dont care about conflicts with already installed packs */
 948                   if (dontfix && p >= installed->start && p < installed->start + installed->nsolvables)
 949                     continue;
 950                  /* rule: -n|-p: either solvable _or_ provider of conflict */
 951                   addrule(solv, -n, -p);
 952                 }
 953             }
 954         }
 955
 956       /*-----------------------------------------
 957        * check obsoletes if not installed
 958        */
 959       if (!installed || n < installed->start || n >= (installed->start + installed->nsolvables))
 960         {                              /* not installed */
 961           if (s->obsoletes)
 962             {
 963               obsp = s->repo->idarraydata + s->obsoletes;
 964               while ((obs = *obsp++) != 0)
 965                 {
 966                   FOR_PROVIDES(p, pp, obs)
 967                     addrule(solv, -n, -p);
 968                 }
 969             }
 970           FOR_PROVIDES(p, pp, s->name)
 971             {
 972               if (s->name == pool->solvables[p].name)
 973                 addrule(solv, -n, -p);
 974             }
 975         }
 976
 977       /*-----------------------------------------
 978        * add recommends to the rule list
 979        */
 980       if (s->recommends)
 981         {
 982           recp = s->repo->idarraydata + s->recommends;
 983           while ((rec = *recp++) != 0)
 984             {
 985               FOR_PROVIDES(p, pp, rec)
 986                 if (!MAPTST(m, p))
 987                   queue_push(&q, p);
 988             }
 989         }
 990       if (s->suggests)
 991         {
 992           sugp = s->repo->idarraydata + s->suggests;
 993           while ((sug = *sugp++) != 0)
 994             {
 995               FOR_PROVIDES(p, pp, sug)
 996                 if (!MAPTST(m, p))
 997                   queue_push(&q, p);
 998             }
 999         }
1000     }
1001   queue_free(&q);
1002 }
1003
1004 static void
1005 addrpmrulesforweak(Solver *solv, Map *m)
1006 {
1007   Pool *pool = solv->pool;
1008   Solvable *s;
1009   Id sup, *supp;
1010   int i, n;
1011
1012   if (pool->verbose) printf("----- addrpmrulesforweak ----- (nrules %d)\n", solv->nrules);
1013   for (i = n = 1; n < pool->nsolvables; i++, n++)
1014     {
1015       if (i == pool->nsolvables)
1016         i = 1;
1017       if (MAPTST(m, i))
1018         continue;
1019       s = pool->solvables + i;
1020       if (!pool_installable(pool, s))
1021         continue;
1022       sup = 0;
1023       if (s->supplements)
1024         {
1025           supp = s->repo->idarraydata + s->supplements;
1026           while ((sup = *supp++) != ID_NULL)
1027             if (dep_possible(solv, sup, m))
1028               break;
1029         }
1030       if (!sup && s->freshens)
1031         {
1032           supp = s->repo->idarraydata + s->freshens;
1033           while ((sup = *supp++) != ID_NULL)
1034             if (dep_possible(solv, sup, m))
1035               break;
1036         }
1037       if (!sup && s->enhances)
1038         {
1039           supp = s->repo->idarraydata + s->enhances;
1040           while ((sup = *supp++) != ID_NULL)
1041             if (dep_possible(solv, sup, m))
1042               break;
1043         }
1044       if (!sup)
1045         continue;
1046       addrpmrulesforsolvable(solv, s, m);
1047       n = 0;
1048     }
1049   if (pool->verbose) printf("----- addrpmrulesforweak ----- done. (nrules%d)\n", solv->nrules);
1050 }
1051
1052 static void
1053 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allowall)
1054 {
1055   Pool *pool = solv->pool;
1056   int i;
1057   Queue qs;
1058   Id qsbuf[64];
1059
1060   if (solv->pool->verbose > 3)
1061     printf ("----- addrpmrulesforupdaters -----\n");
1062
1063   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1064   policy_findupdatepackages(solv, s, &qs, allowall);
1065   if (!MAPTST(m, s - pool->solvables))  /* add rule for s if not already done */
1066     addrpmrulesforsolvable(solv, s, m);
1067   for (i = 0; i < qs.count; i++)
1068     if (!MAPTST(m, qs.elements[i]))
1069       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1070   queue_free(&qs);
1071 }
1072
1073 /*
1074  * add rule for update
1075  *   (A|A1|A2|A3...)  An = update candidates for A
1076  *
1077  * s = (installed) solvable
1078  */
1079
1080 static void
1081 addupdaterule(Solver *solv, Solvable *s, int allowall)
1082 {
1083   /* installed packages get a special upgrade allowed rule */
1084   Pool *pool = solv->pool;
1085   Id d;
1086   Queue qs;
1087   Id qsbuf[64];
1088
1089   if (solv->pool->verbose > 3)
1090     printf ("-----  addupdaterule -----\n");
1091
1092   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1093   policy_findupdatepackages(solv, s, &qs, allowall);
1094   if (qs.count == 0)                   /* no updaters found */
1095     d = 0;
1096   else
1097     d = pool_queuetowhatprovides(pool, &qs);    /* intern computed queue */
1098   queue_free(&qs);
1099   addrule(solv, s - pool->solvables, d);        /* allow update of s */
1100 }
1101
1102
1103 /*-----------------------------------------------------------------*/
1104 /* watches */
1105
1106
1107 /*
1108  * makewatches
1109  *
1110  * initial setup for all watches
1111  */
1112
1113 static void
1114 makewatches(Solver *solv)
1115 {
1116   Rule *r;
1117   int i;
1118   int nsolvables = solv->pool->nsolvables;
1119
1120   xfree(solv->watches);
1121                                        /* lower half for removals, upper half for installs */
1122   solv->watches = (Id *)xcalloc(2 * nsolvables, sizeof(Id));
1123 #if 1
1124   /* do it reverse so rpm rules get triggered first */
1125   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1126 #else
1127   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1128 #endif
1129     {
1130       if (!r->w1                       /* rule is disabled */
1131           || !r->w2)                   /* rule is assertion */
1132         continue;
1133
1134       /* see addwatches(solv, r) */
1135       r->n1 = solv->watches[nsolvables + r->w1];
1136       solv->watches[nsolvables + r->w1] = r - solv->rules;
1137
1138       r->n2 = solv->watches[nsolvables + r->w2];
1139       solv->watches[nsolvables + r->w2] = r - solv->rules;
1140     }
1141 }
1142
1143
1144 /*
1145  * add watches (for rule)
1146  */
1147
1148 static void
1149 addwatches(Solver *solv, Rule *r)
1150 {
1151   int nsolvables = solv->pool->nsolvables;
1152
1153   r->n1 = solv->watches[nsolvables + r->w1];
1154   solv->watches[nsolvables + r->w1] = r - solv->rules;
1155
1156   r->n2 = solv->watches[nsolvables + r->w2];
1157   solv->watches[nsolvables + r->w2] = r - solv->rules;
1158 }
1159
1160
1161 /*-----------------------------------------------------------------*/
1162 /* rule propagation */
1163
1164 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1165
1166 /*
1167  * propagate
1168  *
1169  * propagate decision to all rules
1170  */
1171
1172 static Rule *
1173 propagate(Solver *solv, int level)
1174 {
1175   Pool *pool = solv->pool;
1176   Id *rp, *nrp;
1177   Rule *r;
1178   Id p, pkg, ow;
1179   Id *dp;
1180   Id *decisionmap = solv->decisionmap;
1181   Id *watches = solv->watches + pool->nsolvables;
1182
1183   while (solv->propagate_index < solv->decisionq.count)
1184     {
1185       /* negate because our watches trigger if literal goes FALSE */
1186       pkg = -solv->decisionq.elements[solv->propagate_index++];
1187       if (pool->verbose > 3)
1188         {
1189           printf("popagate for decision %d level %d\n", -pkg, level);
1190           printruleelement(solv, 0, -pkg);
1191         }
1192
1193       for (rp = watches + pkg; *rp; rp = nrp)
1194         {
1195           r = solv->rules + *rp;
1196
1197           if (pool->verbose > 3)
1198             {
1199               printf("  watch triggered ");
1200               printrule(solv, r);
1201             }
1202
1203           if (pkg == r->w1)
1204             {
1205               ow = r->w2;
1206               nrp = &r->n1;
1207             }
1208           else
1209             {
1210               ow = r->w1;
1211               nrp = &r->n2;
1212             }
1213           /* if clause is TRUE, nothing to do */
1214           if (DECISIONMAP_TRUE(ow))
1215             continue;
1216
1217           if (r->d)
1218             {
1219               /* not a binary clause, check if we need to move our watch */
1220               if (r->p && r->p != ow && !DECISIONMAP_TRUE(-r->p))
1221                 p = r->p;
1222               else
1223                 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1224                   if (p != ow && !DECISIONMAP_TRUE(-p))
1225                     break;
1226               if (p)
1227                 {
1228                   /* p is free to watch, move watch to p */
1229                   if (pool->verbose > 3)
1230                     {
1231                       if (p > 0)
1232                         printf("    -> move w%d to %s-%s.%s\n", (pkg == r->w1 ? 1 : 2), id2str(pool, pool->solvables[p].name), id2str(pool, pool->solvables[p].evr), id2str(pool, pool->solvables[p].arch));
1233                       else
1234                         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));
1235                     }
1236                   *rp = *nrp;
1237                   nrp = rp;
1238                   if (pkg == r->w1)
1239                     {
1240                       r->w1 = p;
1241                       r->n1 = watches[p];
1242                     }
1243                   else
1244                     {
1245                       r->w2 = p;
1246                       r->n2 = watches[p];
1247                     }
1248                   watches[p] = r - solv->rules;
1249                   continue;
1250                 }
1251             }
1252           /* unit clause found, set other watch to TRUE */
1253           if (DECISIONMAP_TRUE(-ow))
1254             return r;           /* eek, a conflict! */
1255           if (pool->verbose > 2)
1256             {
1257               printf("unit ");
1258               printrule(solv, r);
1259             }
1260           if (ow > 0)
1261             decisionmap[ow] = level;
1262           else
1263             decisionmap[-ow] = -level;
1264           queue_push(&solv->decisionq, ow);
1265           queue_push(&solv->decisionq_why, r - solv->rules);
1266           if (pool->verbose > 3)
1267             {
1268               Solvable *s = pool->solvables + (ow > 0 ? ow : -ow);
1269               if (ow > 0)
1270                 printf("  -> decided to install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1271               else
1272                 printf("  -> decided to conflict %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1273             }
1274         }
1275     }
1276   return 0;     /* all is well */
1277 }
1278
1279
1280 /*-----------------------------------------------------------------*/
1281 /* Analysis */
1282
1283 /*
1284  * analyze
1285  *   and learn
1286  */
1287
1288 static int
1289 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *why)
1290 {
1291   Pool *pool = solv->pool;
1292   Queue r;
1293   int rlevel = 1;
1294   Map seen;             /* global? */
1295   Id v, vv, *dp;
1296   int l, i, idx;
1297   int num = 0;
1298   int learnt_why = solv->learnt_pool.count;
1299   Id *decisionmap = solv->decisionmap;
1300
1301   queue_init(&r);
1302
1303   if (pool->verbose > 1) printf("ANALYZE at %d ----------------------\n", level);
1304   map_init(&seen, pool->nsolvables);
1305   idx = solv->decisionq.count;
1306   for (;;)
1307     {
1308       if (pool->verbose > 1) printrule(solv, c);
1309       queue_push(&solv->learnt_pool, c - solv->rules);
1310       dp = c->d ? pool->whatprovidesdata + c->d : 0;
1311       for (i = -1; ; i++)
1312         {
1313           if (i == -1)
1314             v = c->p;
1315           else if (c->d == 0)
1316             v = i ? 0 : c->w2;
1317           else
1318             v = *dp++;
1319           if (v == 0)
1320             break;
1321           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1322               continue;
1323           vv = v > 0 ? v : -v;
1324           if (MAPTST(&seen, vv))
1325             continue;
1326           l = solv->decisionmap[vv];
1327           if (l < 0)
1328             l = -l;
1329           if (l == 1)
1330             {
1331 #if 0
1332               int j;
1333               for (j = 0; j < solv->decisionq.count; j++)
1334                 if (solv->decisionq.elements[j] == v)
1335                   break;
1336               if (j == solv->decisionq.count)
1337                 abort();
1338               queue_push(&rulq, -(j + 1));
1339 #endif
1340               continue;                 /* initial setting */
1341             }
1342           MAPSET(&seen, vv);
1343           if (l == level)
1344             num++;                      /* need to do this one as well */
1345           else
1346             {
1347               queue_push(&r, v);
1348               if (pool->verbose > 3)
1349                 {
1350                   printf("PUSH %d ", v);
1351                   printruleelement(solv, 0, v);
1352                 }
1353               if (l > rlevel)
1354                 rlevel = l;
1355             }
1356         }
1357       if (pool->verbose > 3)
1358         printf("num = %d\n", num);
1359       if (num <= 0)
1360         abort();
1361       for (;;)
1362         {
1363           v = solv->decisionq.elements[--idx];
1364           vv = v > 0 ? v : -v;
1365           if (MAPTST(&seen, vv))
1366             break;
1367         }
1368       c = solv->rules + solv->decisionq_why.elements[idx];
1369       MAPCLR(&seen, vv);
1370       if (--num == 0)
1371         break;
1372     }
1373   *pr = -v;
1374   if (r.count == 0)
1375     *dr = 0;
1376   else if (r.count == 1 && r.elements[0] < 0)
1377     *dr = r.elements[0];
1378   else
1379     *dr = pool_queuetowhatprovides(pool, &r);
1380   if (pool->verbose > 1)
1381     {
1382       printf("learned rule for level %d (am %d)\n", rlevel, level);
1383       printruleelement(solv, 0, -v);
1384       for (i = 0; i < r.count; i++)
1385         {
1386           v = r.elements[i];
1387           printruleelement(solv, 0, v);
1388         }
1389     }
1390   map_free(&seen);
1391   queue_push(&solv->learnt_pool, 0);
1392   if (pool->verbose > 3)
1393     {
1394       for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1395         {
1396           printf("learnt_why ");
1397           printrule(solv, solv->rules + solv->learnt_pool.elements[i]);
1398         }
1399     }
1400   if (why)
1401     *why = learnt_why;
1402   return rlevel;
1403 }
1404
1405
1406 /*
1407  * reset_solver
1408  * reset the solver decisions to right after the rpm rules.
1409  * called after rules have been enabled/disabled
1410  */
1411
1412 static void
1413 reset_solver(Solver *solv)
1414 {
1415   int i;
1416   Id v;
1417
1418   /* delete all learnt rules */
1419   solv->nrules = solv->learntrules;
1420   queue_empty(&solv->learnt_why);
1421   queue_empty(&solv->learnt_pool);
1422
1423   /* redo all direct rpm rule decisions */
1424   /* we break at the first decision with a why attached, this is
1425    * either a job/system rule assertion or a propagated decision */
1426   for (i = 0; i < solv->decisionq.count; i++)
1427     {
1428       v = solv->decisionq.elements[i];
1429       solv->decisionmap[v > 0 ? v : -v] = 0;
1430     }
1431   for (i = 0; i < solv->decisionq_why.count; i++)
1432     if (solv->decisionq_why.elements[i])
1433       break;
1434     else
1435       {
1436         v = solv->decisionq.elements[i];
1437         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1438       }
1439
1440   if (solv->pool->verbose > 1)
1441     printf("decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1442
1443   solv->decisionq_why.count = i;
1444   solv->decisionq.count = i;
1445   solv->recommends_index = -1;
1446   solv->propagate_index = 0;
1447
1448   /* redo all job/system decisions */
1449   makeruledecisions(solv);
1450   if (solv->pool->verbose > 1)
1451     printf("decisions after adding job and system rules: %d\n", solv->decisionq.count);
1452   /* recreate watches */
1453   makewatches(solv);
1454 }
1455
1456
1457 /*
1458  * analyze_unsolvable_rule
1459  */
1460
1461 static void
1462 analyze_unsolvable_rule(Solver *solv, Rule *r)
1463 {
1464   int i;
1465   Id why = r - solv->rules;
1466   if (solv->pool->verbose > 1)
1467     {
1468       if (why >= solv->jobrules && why < solv->systemrules)
1469         printf("JOB ");
1470       if (why >= solv->systemrules && why < solv->weakrules)
1471         printf("SYSTEM %d ", why - solv->systemrules);
1472       if (why >= solv->weakrules && why < solv->learntrules)
1473         printf("WEAK ");
1474       if (solv->learntrules && why >= solv->learntrules)
1475         printf("LEARNED ");
1476       printrule(solv, r);
1477     }
1478   if (solv->learntrules && why >= solv->learntrules)
1479     {
1480       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1481         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1482       return;
1483     }
1484   /* do not add rpm rules to problem */
1485   if (why < solv->jobrules)
1486     return;
1487   /* turn rule into problem */
1488   if (why >= solv->jobrules && why < solv->systemrules)
1489     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1490   /* return if problem already countains our rule */
1491   if (solv->problems.count)
1492     {
1493       for (i = solv->problems.count - 1; i >= 0; i--)
1494         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1495           break;
1496         else if (solv->problems.elements[i] == why)
1497           return;
1498     }
1499   queue_push(&solv->problems, why);
1500 }
1501
1502
1503 /*
1504  * analyze_unsolvable
1505  *
1506  * return: 1 - disabled some rules, try again
1507  *         0 - hopeless
1508  */
1509
1510 static int
1511 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1512 {
1513   Pool *pool = solv->pool;
1514   Rule *r;
1515   Map seen;             /* global to speed things up? */
1516   Id v, vv, *dp, why;
1517   int l, i, idx;
1518   Id *decisionmap = solv->decisionmap;
1519   int oldproblemcount;
1520   int lastweak;
1521
1522   if (pool->verbose > 1)
1523     printf("ANALYZE UNSOLVABLE ----------------------\n");
1524   oldproblemcount = solv->problems.count;
1525
1526   /* make room for conflicting rule */
1527   queue_push(&solv->problems, 0);
1528   queue_push(&solv->problems, 0);
1529
1530   r = cr;
1531   map_init(&seen, pool->nsolvables);
1532   analyze_unsolvable_rule(solv, r);
1533   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1534   for (i = -1; ; i++)
1535     {
1536       if (i == -1)
1537         v = r->p;
1538       else if (r->d == 0)
1539         v = i ? 0 : r->w2;
1540       else
1541         v = *dp++;
1542       if (v == 0)
1543         break;
1544       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1545           continue;
1546       vv = v > 0 ? v : -v;
1547       l = solv->decisionmap[vv];
1548       if (l < 0)
1549         l = -l;
1550       MAPSET(&seen, vv);
1551     }
1552   idx = solv->decisionq.count;
1553   while (idx > 0)
1554     {
1555       v = solv->decisionq.elements[--idx];
1556       vv = v > 0 ? v : -v;
1557       if (!MAPTST(&seen, vv))
1558         continue;
1559       why = solv->decisionq_why.elements[idx];
1560       if (!why)
1561         {
1562           if (pool->verbose > 3)
1563             {
1564               printf("RPM ");
1565               printruleelement(solv, 0, v);
1566             }
1567           continue;
1568         }
1569       r = solv->rules + why;
1570       analyze_unsolvable_rule(solv, r);
1571       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1572       for (i = -1; ; i++)
1573         {
1574           if (i == -1)
1575             v = r->p;
1576           else if (r->d == 0)
1577             v = i ? 0 : r->w2;
1578           else
1579             v = *dp++;
1580           if (v == 0)
1581             break;
1582           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1583               continue;
1584           vv = v > 0 ? v : -v;
1585           l = solv->decisionmap[vv];
1586           if (l < 0)
1587             l = -l;
1588           MAPSET(&seen, vv);
1589         }
1590     }
1591   map_free(&seen);
1592   queue_push(&solv->problems, 0);       /* mark end of this problem */
1593
1594   lastweak = 0;
1595   if (solv->weakrules != solv->learntrules)
1596     {
1597       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1598         {
1599           why = solv->problems.elements[i];
1600           if (why < solv->weakrules || why >= solv->learntrules)
1601             continue;
1602           if (!lastweak || lastweak < why)
1603             lastweak = why;
1604         }
1605     }
1606   if (lastweak)
1607     {
1608       /* disable last weak rule */
1609       solv->problems.count = oldproblemcount;
1610       r = solv->rules + lastweak;
1611       printf("disabling weak ");
1612       printrule(solv, r);
1613       r->w1 = 0;
1614       reset_solver(solv);
1615       return 1;
1616     }
1617
1618   /* patch conflicting rule data */
1619   if (cr - solv->rules >= solv->learntrules)
1620     {
1621       /* we have to store the rule internals for learnt rules
1622        * as they get freed for every solver run */
1623       solv->problems.elements[oldproblemcount] = cr->p;
1624       solv->problems.elements[oldproblemcount + 1] = cr->d;
1625     }
1626   else
1627     solv->problems.elements[oldproblemcount + 1] = cr - solv->rules;
1628
1629   if (disablerules)
1630     {
1631       for (i = oldproblemcount + 2; i < solv->problems.count - 1; i++)
1632         disableproblem(solv, solv->problems.elements[i]);
1633       reset_solver(solv);
1634       return 1;
1635     }
1636   if (pool->verbose)
1637     printf("UNSOLVABLE\n");
1638   return 0;
1639 }
1640
1641
1642 /*-----------------------------------------------------------------*/
1643 /* Decision revert */
1644
1645 /*
1646  * revert
1647  * revert decision at level
1648  */
1649
1650 static void
1651 revert(Solver *solv, int level)
1652 {
1653   Id v, vv;
1654   while (solv->decisionq.count)
1655     {
1656       v = solv->decisionq.elements[solv->decisionq.count - 1];
1657       vv = v > 0 ? v : -v;
1658       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1659         break;
1660       if (solv->pool->verbose > 3)
1661         printf("reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1662       solv->decisionmap[vv] = 0;
1663       solv->decisionq.count--;
1664       solv->decisionq_why.count--;
1665       solv->propagate_index = solv->decisionq.count;
1666     }
1667   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1668     {
1669       solv->branches.count--;
1670       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1671         solv->branches.count--;
1672     }
1673   solv->recommends_index = -1;
1674 }
1675
1676
1677 /*
1678  * watch2onhighest - put watch2 on literal with highest level
1679  */
1680
1681 static inline void
1682 watch2onhighest(Solver *solv, Rule *r)
1683 {
1684   int l, wl = 0;
1685   Id v, *dp;
1686
1687   if (!r->d)
1688     return;     /* binary rule, both watches are set */
1689   dp = solv->pool->whatprovidesdata + r->d;
1690   while ((v = *dp++) != 0)
1691     {
1692       l = solv->decisionmap[v < 0 ? -v : v];
1693       if (l < 0)
1694         l = -l;
1695       if (l > wl)
1696         {
1697           r->w2 = dp[-1];
1698           wl = l;
1699         }
1700     }
1701 }
1702
1703
1704 /*
1705  * setpropagatelearn
1706  *
1707  * add free decision to decision q, increase level
1708  * propagate decision, return if no conflict.
1709  * in conflict case, analyze conflict rule, add resulting
1710  * rule to learnt rule set, make decision from learnt
1711  * rule (always unit) and re-propagate.
1712  */
1713
1714 static int
1715 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1716 {
1717   Rule *r;
1718   Id p, d;
1719   int l, why;
1720
1721   if (decision)
1722     {
1723       level++;
1724       if (decision > 0)
1725         solv->decisionmap[decision] = level;
1726       else
1727         solv->decisionmap[-decision] = -level;
1728       queue_push(&solv->decisionq, decision);
1729       queue_push(&solv->decisionq_why, 0);
1730     }
1731   for (;;)
1732     {
1733       r = propagate(solv, level);
1734       if (!r)
1735         break;
1736       if (level == 1)
1737         return analyze_unsolvable(solv, r, disablerules);
1738       printf("conflict with rule #%d\n", (int)(r - solv->rules));
1739       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1740       if (l >= level || l <= 0)
1741         abort();
1742       printf("reverting decisions (level %d -> %d)\n", level, l);
1743       level = l;
1744       revert(solv, level);
1745       r = addrule(solv, p, d);       /* p requires d */
1746       if (!r)
1747         abort();
1748       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1749         {
1750           printf("%d %d\n", solv->learnt_why.count, (int)(r - solv->rules) - solv->learntrules);
1751           abort();
1752         }
1753       queue_push(&solv->learnt_why, why);
1754       if (d)
1755         {
1756           /* at least 2 literals, needs watches */
1757           watch2onhighest(solv, r);
1758           addwatches(solv, r);
1759         }
1760       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1761       queue_push(&solv->decisionq, p);
1762       queue_push(&solv->decisionq_why, r - solv->rules);
1763       if (solv->pool->verbose > 1)
1764         {
1765           printf("decision: ");
1766           printruleelement(solv, 0, p);
1767           printf("new rule: ");
1768           printrule(solv, r);
1769         }
1770     }
1771   return level;
1772 }
1773
1774
1775 /*
1776  * install best package from the queue. We add an extra package, inst, if
1777  * provided. See comment in weak install section.
1778  */
1779 static int
1780 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1781 {
1782   Pool *pool = solv->pool;
1783   Id p;
1784   int i;
1785
1786   if (dq->count > 1 || inst)
1787     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1788
1789   i = 0;
1790   if (dq->count > 1)
1791     {
1792       /* choose the supplemented one */
1793       for (i = 0; i < dq->count; i++)
1794         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1795           break;
1796       if (i == dq->count)
1797         {
1798           for (i = 1; i < dq->count; i++)
1799             queue_push(&solv->branches, dq->elements[i]);
1800           queue_push(&solv->branches, -level);
1801           i = 0;
1802         }
1803     }
1804   p = dq->elements[i];
1805
1806   if (pool->verbose > 3)
1807     {
1808       Solvable *s = pool->solvables + p;
1809       printf("installing %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1810     }
1811
1812   return setpropagatelearn(solv, level, p, disablerules);
1813 }
1814
1815
1816 /*-----------------------------------------------------------------*/
1817 /* Main solver interface */
1818
1819
1820 /*
1821  * solver_create
1822  * create solver structure
1823  *
1824  * pool: all available solvables
1825  * installed: installed Solvables
1826  *
1827  *
1828  * Upon solving, rules are created to flag the Solvables
1829  * of the 'installed' Repo as installed.
1830  */
1831
1832 Solver *
1833 solver_create(Pool *pool, Repo *installed)
1834 {
1835   Solver *solv;
1836   solv = (Solver *)xcalloc(1, sizeof(Solver));
1837   solv->pool = pool;
1838   solv->installed = installed;
1839
1840   queue_init(&solv->ruletojob);
1841   queue_init(&solv->decisionq);
1842   queue_init(&solv->decisionq_why);
1843   queue_init(&solv->problems);
1844   queue_init(&solv->suggestions);
1845   queue_init(&solv->learnt_why);
1846   queue_init(&solv->learnt_pool);
1847   queue_init(&solv->branches);
1848
1849   map_init(&solv->recommendsmap, pool->nsolvables);
1850   map_init(&solv->suggestsmap, pool->nsolvables);
1851   map_init(&solv->noupdate, installed ? installed->nsolvables : 0);
1852   solv->recommends_index = 0;
1853
1854   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1855   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
1856   memset(solv->rules, 0, sizeof(Rule));
1857   solv->nrules = 1;
1858
1859   return solv;
1860 }
1861
1862
1863 /*
1864  * solver_free
1865  */
1866
1867 void
1868 solver_free(Solver *solv)
1869 {
1870   queue_free(&solv->ruletojob);
1871   queue_free(&solv->decisionq);
1872   queue_free(&solv->decisionq_why);
1873   queue_free(&solv->learnt_why);
1874   queue_free(&solv->learnt_pool);
1875   queue_free(&solv->problems);
1876   queue_free(&solv->suggestions);
1877   queue_free(&solv->branches);
1878
1879   map_free(&solv->recommendsmap);
1880   map_free(&solv->suggestsmap);
1881   map_free(&solv->noupdate);
1882   xfree(solv->decisionmap);
1883   xfree(solv->rules);
1884   xfree(solv->watches);
1885   xfree(solv->weaksystemrules);
1886   xfree(solv->obsoletes);
1887   xfree(solv->obsoletes_data);
1888   xfree(solv);
1889 }
1890
1891
1892 /*-------------------------------------------------------*/
1893
1894 /*
1895  * run_solver
1896  *
1897  * all rules have been set up, now actually run the solver
1898  *
1899  */
1900
1901 static void
1902 run_solver(Solver *solv, int disablerules, int doweak)
1903 {
1904   Queue dq;
1905   int systemlevel;
1906   int level, olevel;
1907   Rule *r;
1908   int i, j, n;
1909   Solvable *s;
1910   Pool *pool = solv->pool;
1911   Id p, *dp;
1912
1913   if (pool->verbose > 3)
1914     {
1915       printf("number of rules: %d\n", solv->nrules);
1916       for (i = 0; i < solv->nrules; i++)
1917         printrule(solv, solv->rules + i);
1918     }
1919
1920   /* all new rules are learnt after this point */
1921   solv->learntrules = solv->nrules;
1922   /* crate watches lists */
1923   makewatches(solv);
1924
1925   if (pool->verbose) printf("initial decisions: %d\n", solv->decisionq.count);
1926
1927   /* start SAT algorithm */
1928   level = 1;
1929   systemlevel = level + 1;
1930   if (pool->verbose) printf("solving...\n");
1931
1932   queue_init(&dq);
1933   for (;;)
1934     {
1935       /*
1936        * propagate
1937        */
1938
1939       if (level == 1)
1940         {
1941           if (pool->verbose) printf("propagating (%d %d)...\n", solv->propagate_index, solv->decisionq.count);
1942           if ((r = propagate(solv, level)) != 0)
1943             {
1944               if (analyze_unsolvable(solv, r, disablerules))
1945                 continue;
1946               queue_free(&dq);
1947               return;
1948             }
1949         }
1950
1951       /*
1952        * installed packages
1953        */
1954
1955       if (level < systemlevel && solv->installed->nsolvables)
1956         {
1957           if (!solv->updatesystem)
1958             {
1959               /* try to keep as many packages as possible */
1960               if (pool->verbose) printf("installing system packages\n");
1961               for (i = solv->installed->start, n = 0; ; i++, n++)
1962                 {
1963                   if (n == solv->installed->nsolvables)
1964                     break;
1965                   if (i == solv->installed->start + solv->installed->nsolvables)
1966                     i = solv->installed->start;
1967                   s = pool->solvables + i;
1968                   if (solv->decisionmap[i] != 0)
1969                     continue;
1970                   if (pool->verbose > 3)
1971                     printf("keeping %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
1972                   olevel = level;
1973                   level = setpropagatelearn(solv, level, i, disablerules);
1974                   if (level == 0)
1975                     {
1976                       queue_free(&dq);
1977                       return;
1978                     }
1979                   if (level <= olevel)
1980                     n = 0;
1981                 }
1982             }
1983           if (solv->weaksystemrules)
1984             {
1985               if (pool->verbose) printf("installing weak system packages\n");
1986               for (i = solv->installed->start, n = 0; ; i++, n++)
1987                 {
1988                   if (n == solv->installed->nsolvables)
1989                     break;
1990                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
1991                     continue;
1992                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
1993                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
1994                     continue;
1995                   queue_empty(&dq);
1996                   if (solv->weaksystemrules[i - solv->installed->start])
1997                     {
1998                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
1999                       while ((p = *dp++) != 0)
2000                         {
2001                           if (solv->decisionmap[p] > 0)
2002                             break;
2003                           if (solv->decisionmap[p] == 0)
2004                             queue_push(&dq, p);
2005                         }
2006                       if (p)
2007                         continue;       /* update package already installed */
2008                     }
2009                   if (!dq.count && solv->decisionmap[i] != 0)
2010                     continue;
2011                   olevel = level;
2012                   /* FIXME: i is handled a bit different because we do not want
2013                    * to have it pruned just because it is not recommened.
2014                    * we should not prune installed packages instead */
2015                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2016                   if (level == 0)
2017                     {
2018                       queue_free(&dq);
2019                       return;
2020                     }
2021                   if (level <= olevel)
2022                     {
2023                       n = 0;
2024                       break;
2025                     }
2026                 }
2027               if (n != solv->installed->nsolvables)
2028                 continue;
2029             }
2030           systemlevel = level;
2031         }
2032
2033       /*
2034        * decide
2035        */
2036
2037       if (pool->verbose) printf("deciding unresolved rules\n");
2038       for (i = 1, n = 1; ; i++, n++)
2039         {
2040           if (n == solv->nrules)
2041             break;
2042           if (i == solv->nrules)
2043             i = 1;
2044           r = solv->rules + i;
2045           if (!r->w1)
2046             continue;
2047           queue_empty(&dq);
2048           if (r->d == 0)
2049             {
2050               /* binary or unary rule */
2051               /* need two positive undecided literals */
2052               if (r->p < 0 || r->w2 <= 0)
2053                 continue;
2054               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2055                 continue;
2056               queue_push(&dq, r->p);
2057               queue_push(&dq, r->w2);
2058             }
2059           else
2060             {
2061               /* make sure that
2062                * all negative literals are installed
2063                * no positive literal is installed
2064                * i.e. the rule is not fulfilled and we
2065                * just need to decide on the positive literals
2066                */
2067               if (r->p < 0)
2068                 {
2069                   if (solv->decisionmap[-r->p] <= 0)
2070                     continue;
2071                 }
2072               else
2073                 {
2074                   if (solv->decisionmap[r->p] > 0)
2075                     continue;
2076                   if (solv->decisionmap[r->p] == 0)
2077                     queue_push(&dq, r->p);
2078                 }
2079               dp = pool->whatprovidesdata + r->d;
2080               while ((p = *dp++) != 0)
2081                 {
2082                   if (p < 0)
2083                     {
2084                       if (solv->decisionmap[-p] <= 0)
2085                         break;
2086                     }
2087                   else
2088                     {
2089                       if (solv->decisionmap[p] > 0)
2090                         break;
2091                       if (solv->decisionmap[p] == 0)
2092                         queue_push(&dq, p);
2093                     }
2094                 }
2095               if (p)
2096                 continue;
2097             }
2098           if (dq.count < 2)
2099             {
2100               /* cannot happen as this means that
2101                * the rule is unit */
2102               printrule(solv, r);
2103               abort();
2104             }
2105           if (pool->verbose > 2)
2106             printrule(solv, r);
2107
2108           olevel = level;
2109           level = selectandinstall(solv, level, &dq, 0, disablerules);
2110           if (level == 0)
2111             {
2112               queue_free(&dq);
2113               return;
2114             }
2115           if (level < systemlevel)
2116             break;
2117           n = 0;
2118         } /* for(), decide */
2119
2120       if (n != solv->nrules)    /* continue if level < systemlevel */
2121         continue;
2122
2123       if (doweak && !solv->problems.count)
2124         {
2125           int qcount;
2126
2127           if (pool->verbose) printf("installing recommended packages\n");
2128           queue_empty(&dq);
2129           for (i = 1; i < pool->nsolvables; i++)
2130             {
2131               if (solv->decisionmap[i] < 0)
2132                 continue;
2133               if (solv->decisionmap[i] > 0)
2134                 {
2135                   Id *recp, rec, *pp, p;
2136                   s = pool->solvables + i;
2137                   /* installed, check for recommends */
2138                   /* XXX need to special case AND ? */
2139                   if (s->recommends)
2140                     {
2141                       recp = s->repo->idarraydata + s->recommends;
2142                       while ((rec = *recp++) != 0)
2143                         {
2144                           qcount = dq.count;
2145                           FOR_PROVIDES(p, pp, rec)
2146                             {
2147                               if (solv->decisionmap[p] > 0)
2148                                 {
2149                                   dq.count = qcount;
2150                                   break;
2151                                 }
2152                               else if (solv->decisionmap[p] == 0)
2153                                 {
2154                                   queue_pushunique(&dq, p);
2155                                 }
2156                             }
2157                         }
2158                     }
2159                 }
2160               else
2161                 {
2162                   s = pool->solvables + i;
2163                   if (!s->supplements && !s->freshens)
2164                     continue;
2165                   if (!pool_installable(pool, s))
2166                     continue;
2167                   if (solver_is_supplementing(solv, s))
2168                     queue_pushunique(&dq, i);
2169                 }
2170             }
2171           if (dq.count)
2172             {
2173               if (dq.count > 1)
2174                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2175               p = dq.elements[0];
2176               s = pool->solvables + p;
2177               if (pool->verbose > 0)
2178                 printf("installing recommended %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2179               level = setpropagatelearn(solv, level, p, 0);
2180               continue;
2181             }
2182         }
2183
2184      if (solv->solution_callback)
2185         {
2186           solv->solution_callback(solv, solv->solution_callback_data);
2187           if (solv->branches.count)
2188             {
2189               int i = solv->branches.count - 1;
2190               int l = -solv->branches.elements[i];
2191               for (; i > 0; i--)
2192                 if (solv->branches.elements[i - 1] < 0)
2193                   break;
2194               p = solv->branches.elements[i];
2195               if (pool->verbose > 0)
2196                 {
2197                   s = pool->solvables + p;
2198                   printf("branching with %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2199                 }
2200               queue_empty(&dq);
2201               for (j = i + 1; j < solv->branches.count; j++)
2202                 queue_push(&dq, solv->branches.elements[j]);
2203               solv->branches.count = i;
2204               level = l;
2205               revert(solv, level);
2206               if (dq.count > 1)
2207                 for (j = 0; j < dq.count; j++)
2208                   queue_push(&solv->branches, dq.elements[j]);
2209               olevel = level;
2210               level = setpropagatelearn(solv, level, p, disablerules);
2211               if (level == 0)
2212                 {
2213                   queue_free(&dq);
2214                   return;
2215                 }
2216               continue;
2217             }
2218           /* all branches done, we're finally finished */
2219           break;
2220         }
2221
2222       /* minimization step */
2223      if (solv->branches.count)
2224         {
2225           int l = 0, lasti = -1, lastl = -1;
2226           p = 0;
2227           for (i = solv->branches.count - 1; i >= 0; i--)
2228             {
2229               p = solv->branches.elements[i];
2230               if (p < 0)
2231                 l = -p;
2232               else if (p > 0 && solv->decisionmap[p] > l + 1)
2233                 {
2234                   lasti = i;
2235                   lastl = l;
2236                 }
2237             }
2238           if (lasti >= 0)
2239             {
2240               /* kill old solvable so that we do not loop */
2241               p = solv->branches.elements[lasti];
2242               solv->branches.elements[lasti] = 0;
2243               s = pool->solvables + p;
2244               if (pool->verbose > 0)
2245                 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));
2246
2247               level = lastl;
2248               revert(solv, level);
2249               olevel = level;
2250               level = setpropagatelearn(solv, level, p, disablerules);
2251               if (level == 0)
2252                 {
2253                   queue_free(&dq);
2254                   return;
2255                 }
2256               continue;
2257             }
2258         }
2259       break;
2260     }
2261   queue_free(&dq);
2262 }
2263
2264
2265 /*
2266  * refine_suggestion
2267  * at this point, all rules that led to conflicts are disabled.
2268  * we re-enable all rules of a problem set but rule "sug", then
2269  * continue to disable more rules until there as again a solution.
2270  */
2271
2272 /* FIXME: think about conflicting assertions */
2273
2274 static void
2275 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2276 {
2277   Pool *pool = solv->pool;
2278   Rule *r;
2279   int i, j;
2280   Id v;
2281   Queue disabled;
2282   int disabledcnt;
2283
2284   if (pool->verbose)
2285     {
2286       printf("refine_suggestion start\n");
2287       for (i = 0; problem[i]; i++)
2288         {
2289           if (problem[i] == sug)
2290             printf("=> ");
2291           printproblem(solv, problem[i]);
2292         }
2293     }
2294   queue_init(&disabled);
2295   queue_empty(refined);
2296   queue_push(refined, sug);
2297
2298   /* re-enable all problem rules with the exception of "sug" */
2299   revert(solv, 1);
2300   reset_solver(solv);
2301
2302   for (i = 0; problem[i]; i++)
2303     if (problem[i] != sug)
2304       enableproblem(solv, problem[i]);
2305
2306   if (sug < 0)
2307     disableupdaterules(solv, job, -(sug + 1));
2308
2309   for (;;)
2310     {
2311       /* re-enable as many weak rules as possible */
2312       for (i = solv->weakrules; i < solv->learntrules; i++)
2313         {
2314           r = solv->rules + i;
2315           if (!r->w1)
2316             enablerule(solv, r);
2317         }
2318
2319       queue_empty(&solv->problems);
2320       revert(solv, 1);          /* XXX move to reset_solver? */
2321       reset_solver(solv);
2322       run_solver(solv, 0, 0);
2323       if (!solv->problems.count)
2324         {
2325           if (pool->verbose)
2326             printf("no more problems!\n");
2327           if (pool->verbose > 3)
2328             printdecisions(solv);
2329           break;                /* great, no more problems */
2330         }
2331       disabledcnt = disabled.count;
2332       /* skip over problem rule */
2333       for (i = 2; i < solv->problems.count - 1; i++)
2334         {
2335           /* ignore solutions in refined */
2336           v = solv->problems.elements[i];
2337           for (j = 0; problem[j]; j++)
2338             if (problem[j] != sug && problem[j] == v)
2339               break;
2340           if (problem[j])
2341             continue;
2342           queue_push(&disabled, v);
2343         }
2344       if (disabled.count == disabledcnt)
2345         {
2346           /* no solution found, this was an invalid suggestion! */
2347           if (pool->verbose)
2348             printf("no solution found!\n");
2349           refined->count = 0;
2350           break;
2351         }
2352       if (disabled.count == disabledcnt + 1)
2353         {
2354           /* just one suggestion, add it to refined list */
2355           v = disabled.elements[disabledcnt];
2356           queue_push(refined, v);
2357           disableproblem(solv, v);
2358           if (v < 0)
2359             disableupdaterules(solv, job, -(v + 1));
2360         }
2361       else
2362         {
2363           /* more than one solution, disable all */
2364           /* do not push anything on refine list */
2365           if (pool->verbose > 1)
2366             {
2367               printf("more than one solution found:\n");
2368               for (i = disabledcnt; i < disabled.count; i++)
2369                 printproblem(solv, disabled.elements[i]);
2370             }
2371           for (i = disabledcnt; i < disabled.count; i++)
2372             disableproblem(solv, disabled.elements[i]);
2373         }
2374     }
2375   /* all done, get us back into the same state as before */
2376   /* enable refined rules again */
2377   for (i = 0; i < disabled.count; i++)
2378     enableproblem(solv, disabled.elements[i]);
2379   /* disable problem rules again */
2380   for (i = 0; problem[i]; i++)
2381     disableproblem(solv, problem[i]);
2382   if (pool->verbose)
2383     printf("refine_suggestion end\n");
2384 }
2385
2386 static void
2387 problems_to_solutions(Solver *solv, Queue *job)
2388 {
2389   Pool *pool = solv->pool;
2390   Queue problems;
2391   Queue solution;
2392   Queue solutions;
2393   Id *problem;
2394   Id why;
2395   int i, j;
2396
2397   if (!solv->problems.count)
2398     return;
2399   queue_clone(&problems, &solv->problems);
2400   queue_init(&solution);
2401   queue_init(&solutions);
2402   /* copy over problem rule */
2403   queue_push(&solutions, problems.elements[0]);
2404   queue_push(&solutions, problems.elements[1]);
2405   problem = problems.elements + 2;
2406   for (i = 2; i < problems.count; i++)
2407     {
2408       Id v = problems.elements[i];
2409       if (v == 0)
2410         {
2411           /* mark end of this problem */
2412           queue_push(&solutions, 0);
2413           queue_push(&solutions, 0);
2414           if (i + 1 == problems.count)
2415             break;
2416           /* copy over problem rule of next problem */
2417           queue_push(&solutions, problems.elements[i + 1]);
2418           queue_push(&solutions, problems.elements[i + 2]);
2419           i += 2;
2420           problem = problems.elements + i + 1;
2421           continue;
2422         }
2423       refine_suggestion(solv, job, problem, v, &solution);
2424       if (!solution.count)
2425         continue;       /* this solution didn't work out */
2426
2427       for (j = 0; j < solution.count; j++)
2428         {
2429           why = solution.elements[j];
2430 #if 0
2431           printproblem(solv, why);
2432 #endif
2433           if (why < 0)
2434             {
2435               queue_push(&solutions, 0);
2436               queue_push(&solutions, -why);
2437             }
2438           else if (why >= solv->systemrules && why < solv->weakrules)
2439             {
2440               Id p, rp = 0;
2441               p = solv->installed->start + (why - solv->systemrules);
2442               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2443                 {
2444                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2445                   for (; *dp; dp++)
2446                     {
2447                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2448                         continue;
2449                       if (solv->decisionmap[*dp] > 0)
2450                         {
2451                           rp = *dp;
2452                           break;
2453                         }
2454                     }
2455                 }
2456               queue_push(&solutions, p);
2457               queue_push(&solutions, rp);
2458             }
2459           else
2460             abort();
2461         }
2462       /* mark end of this solution */
2463       queue_push(&solutions, 0);
2464       queue_push(&solutions, 0);
2465     }
2466   queue_free(&solution);
2467   queue_free(&problems);
2468   /* copy queue over to solutions */
2469   queue_free(&solv->problems);
2470   queue_clone(&solv->problems, &solutions);
2471   queue_free(&solutions);
2472 }
2473
2474
2475
2476 /*
2477  * printdecisions
2478  */
2479
2480 static const char *
2481 id2rc(Solver *solv, Id id)
2482 {
2483   const char *evr;
2484   if (solv->rc_output != 2)
2485     return "";
2486   evr = id2str(solv->pool, id);
2487   if (*evr < '0' || *evr > '9')
2488     return "0:";
2489   while (*evr >= '0' && *evr <= '9')
2490     evr++;
2491   if (*evr != ':')
2492     return "0:";
2493   return "";
2494 }
2495
2496 void
2497 printdecisions(Solver *solv)
2498 {
2499   Pool *pool = solv->pool;
2500   Id p, *obsoletesmap;
2501   int i;
2502   Solvable *s;
2503
2504   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2505   for (i = 0; i < solv->decisionq.count; i++)
2506     {
2507       Id *pp, n;
2508
2509       n = solv->decisionq.elements[i];
2510       if (n < 0)
2511         continue;
2512       if (n == SYSTEMSOLVABLE)
2513         continue;
2514       if (n >= solv->installed->start && n < solv->installed->start + solv->installed->nsolvables)
2515         continue;
2516       s = pool->solvables + n;
2517       FOR_PROVIDES(p, pp, s->name)
2518         if (s->name == pool->solvables[p].name)
2519           {
2520             if (p >= solv->installed->start && p < solv->installed->start + solv->installed->nsolvables && !obsoletesmap[p])
2521               {
2522                 obsoletesmap[p] = n;
2523                 obsoletesmap[n]++;
2524               }
2525           }
2526     }
2527   for (i = 0; i < solv->decisionq.count; i++)
2528     {
2529       Id obs, *obsp;
2530       Id *pp, n;
2531
2532       n = solv->decisionq.elements[i];
2533       if (n < 0)
2534         continue;
2535       if (n == SYSTEMSOLVABLE)
2536         continue;
2537       if (n >= solv->installed->start && n < solv->installed->start + solv->installed->nsolvables)
2538         continue;
2539       s = pool->solvables + n;
2540       if (!s->obsoletes)
2541         continue;
2542       obsp = s->repo->idarraydata + s->obsoletes;
2543       while ((obs = *obsp++) != 0)
2544         FOR_PROVIDES(p, pp, obs)
2545           {
2546             if (p >= solv->installed->start && p < solv->installed->start + solv->installed->nsolvables && !obsoletesmap[p])
2547               {
2548                 obsoletesmap[p] = n;
2549                 obsoletesmap[n]++;
2550               }
2551           }
2552     }
2553
2554   if (solv->rc_output)
2555     printf(">!> Solution #1:\n");
2556
2557   int installs = 0, uninstalls = 0, upgrades = 0;
2558
2559   /* print solvables to be erased */
2560
2561   for (i = solv->installed->start; i < solv->installed->start + solv->installed->nsolvables; i++)
2562     {
2563       if (solv->decisionmap[i] > 0)
2564         continue;
2565       if (obsoletesmap[i])
2566         continue;
2567       s = pool->solvables + i;
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   /* print solvables to be installed */
2578
2579   for (i = 0; i < solv->decisionq.count; i++)
2580     {
2581       int j;
2582       p = solv->decisionq.elements[i];
2583       if (p < 0)
2584         continue;
2585       if (p == SYSTEMSOLVABLE)
2586         continue;
2587       if (p >= solv->installed->start && p < solv->installed->start + solv->installed->nsolvables)
2588         continue;
2589       s = pool->solvables + p;
2590
2591       if (!obsoletesmap[p])
2592         {
2593           if (solv->rc_output)
2594             printf(">!> ");
2595           printf("install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2596           if (solv->rc_output != 2)
2597             printf(".%s", id2str(pool, s->arch));
2598           installs++;
2599         }
2600       else if (!solv->rc_output)
2601         {
2602           printf("update  %s-%s.%s  (obsoletes", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2603           for (j = solv->installed->start; j < solv->installed->start + solv->installed->nsolvables; j++)
2604             {
2605               if (obsoletesmap[j] != p)
2606                 continue;
2607               s = pool->solvables + j;
2608               printf(" %s-%s.%s", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2609             }
2610           printf(")");
2611           upgrades++;
2612         }
2613       else
2614         {
2615           Solvable *f, *fn = 0;
2616           for (j = solv->installed->start; j < solv->installed->start + solv->installed->nsolvables; j++)
2617             {
2618               if (obsoletesmap[j] != p)
2619                 continue;
2620               f = pool->solvables + j;
2621               if (fn || f->name != s->name)
2622                 {
2623                   if (solv->rc_output == 2)
2624                     printf(">!> remove  %s-%s%s\n", id2str(pool, f->name), id2rc(solv, f->evr), id2str(pool, f->evr));
2625                   else if (solv->rc_output)
2626                     printf(">!> remove  %s-%s.%s\n", id2str(pool, f->name), id2str(pool, f->evr), id2str(pool, f->arch));
2627                   uninstalls++;
2628                 }
2629               else
2630                 fn = f;
2631             }
2632           if (!fn)
2633             {
2634               printf(">!> install %s-%s%s", id2str(pool, s->name), id2rc(solv, s->evr), id2str(pool, s->evr));
2635               if (solv->rc_output != 2)
2636                 printf(".%s", id2str(pool, s->arch));
2637               installs++;
2638             }
2639           else
2640             {
2641               if (solv->rc_output == 2)
2642                 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));
2643               else
2644                 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));
2645               upgrades++;
2646             }
2647         }
2648       if (solv->rc_output)
2649         {
2650           Repo *repo = s->repo;
2651           if (repo && strcmp(repo_name(repo), "locales"))
2652             printf("[%s]", repo_name(repo));
2653         }
2654       printf("\n");
2655     }
2656
2657   if (solv->rc_output)
2658     printf(">!> installs=%d, upgrades=%d, uninstalls=%d\n", installs, upgrades, uninstalls);
2659
2660   xfree(obsoletesmap);
2661
2662   if (solv->suggestions.count)
2663     {
2664       printf("\nsuggested packages:\n");
2665       for (i = 0; i < solv->suggestions.count; i++)
2666         {
2667           s = pool->solvables + solv->suggestions.elements[i];
2668           printf("- %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2669         }
2670     }
2671 }
2672
2673 int
2674 printconflicts(Solver *solv, Solvable *s, Id pc)
2675 {
2676   Pool *pool = solv->pool;
2677   Solvable *sc = pool->solvables + pc;
2678   Id p, *pp, con, *conp, obs, *obsp;
2679   int numc = 0;
2680
2681   if (s->conflicts)
2682     {
2683       conp = s->repo->idarraydata + s->conflicts;
2684       while ((con = *conp++) != 0)
2685         {
2686           FOR_PROVIDES(p, pp, con)
2687             {
2688               if (p != pc)
2689                 continue;
2690               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));
2691               numc++;
2692             }
2693         }
2694     }
2695   if (s->obsoletes && (!solv->installed || s - pool->solvables < solv->installed->start || s - pool->solvables >= solv->installed->start + solv->installed->nsolvables))
2696     {
2697       obsp = s->repo->idarraydata + s->obsoletes;
2698       while ((obs = *obsp++) != 0)
2699         {
2700           FOR_PROVIDES(p, pp, obs)
2701             {
2702               if (p != pc)
2703                 continue;
2704               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));
2705               numc++;
2706             }
2707         }
2708     }
2709   return numc;
2710 }
2711
2712 void
2713 printprobleminfo(Solver *solv, Id p, Id d, Queue *job, Id firstp, Id firstrp)
2714 {
2715   Pool *pool = solv->pool;
2716   Rule *r;
2717   Solvable *s;
2718   Id what;
2719
2720   if (p != 0)
2721     {
2722       /* learnt rule, ignore for now */
2723       printf("some learnt rule...\n");
2724       return;
2725     }
2726   if (d == 0)
2727     {
2728       /* conflict with system solvable, i.e. could not create rule */
2729       if (firstp)
2730         {
2731           printf("got firstp\n");
2732           abort();
2733         }
2734       what = job->elements[firstrp];
2735       switch (job->elements[firstrp - 1])
2736         {
2737         case SOLVER_INSTALL_SOLVABLE_NAME:
2738           printf("no solvable exists with name %s\n", dep2str(pool, what));
2739           break;
2740         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2741           printf("no solvable provides %s\n", dep2str(pool, what));
2742           break;
2743         default:
2744           printf("unknown  job\n");
2745           abort();
2746         }
2747       return;
2748     }
2749   else if (d < 0)
2750     {
2751       Id req, *reqp, *dp;
2752       int count = 0;
2753       /* conflict with rpm rule, package -d is not installable */
2754       s = pool->solvables + (-d);
2755       if (s->requires)
2756         {
2757           reqp = s->repo->idarraydata + s->requires;
2758           while ((req = *reqp++) != 0)
2759             {
2760               if (req == SOLVABLE_PREREQMARKER)
2761                 continue;
2762               dp = GET_PROVIDESP(req, p);
2763               if (*dp)
2764                 continue;
2765               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));
2766               count++;
2767             }
2768         }
2769       if (!count)
2770         printf("package %s-%s.%s is not installable\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2771       return;
2772     }
2773   if (d >= solv->jobrules)
2774     {
2775       r = solv->rules + d;
2776       p = r->p;
2777       d = r->d;
2778       if (p < 0 && d < 0)
2779         {
2780           Solvable *sp, *sd;
2781           sp = pool->solvables + (-p);
2782           sd = pool->solvables + (-d);
2783           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));
2784           return;
2785         }
2786       printf("some job rule...\n");
2787       printrule(solv, r);
2788       return;
2789     }
2790   r = solv->rules + d;
2791   p = r->p;
2792   if (p >= 0)
2793     abort();
2794   d = r->d;
2795   if (d == 0 && r->w2 < 0)
2796     {
2797       Solvable *sp, *sd;
2798       d = r->w2;
2799       sp = pool->solvables + (-p);
2800       sd = pool->solvables + (-d);
2801       if (sp->name == sd->name)
2802         {
2803           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));
2804         }
2805       else
2806         {
2807           printconflicts(solv, pool->solvables + (-p), -d);
2808           printconflicts(solv, pool->solvables + (-d), -p);
2809         }
2810     }
2811   else
2812     {
2813       /* find requires of p that corresponds with our rule */
2814       Id req, *reqp, *dp;
2815       s = pool->solvables + (-p);
2816       reqp = s->repo->idarraydata + s->requires;
2817       while ((req = *reqp++) != 0)
2818         {
2819           if (req == SOLVABLE_PREREQMARKER)
2820             continue;
2821           dp = GET_PROVIDESP(req, p);
2822           if (d == 0)
2823             {
2824               if (*dp == r->w2 && dp[1] == 0)
2825                 break;
2826             }
2827           else if (dp - pool->whatprovidesdata == d)
2828             break;
2829         }
2830       if (!req)
2831         {
2832           printf("req not found\n");
2833           abort();
2834         }
2835       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));
2836     }
2837 }
2838
2839 void
2840 printsolutions(Solver *solv, Queue *job)
2841 {
2842   Pool *pool = solv->pool;
2843   int pcnt;
2844   int i;
2845   Id p, d, rp, what;
2846   Solvable *s, *sd;
2847
2848   printf("Encountered problems! Here are the solutions:\n\n");
2849   pcnt = 1;
2850   for (i = 0; i < solv->problems.count; )
2851     {
2852       printf("Problem %d:\n", pcnt++);
2853       printf("====================================\n");
2854       p = solv->problems.elements[i++];
2855       d = solv->problems.elements[i++];
2856       printprobleminfo(solv, p, d, job, solv->problems.elements[i], solv->problems.elements[i + 1]);
2857       printf("\n");
2858       for (;;)
2859         {
2860           if (solv->problems.elements[i] == 0 && solv->problems.elements[i + 1] == 0)
2861             {
2862               /* end of solutions for this problems reached */
2863               i += 2;
2864               break;
2865             }
2866           for (;;)
2867             {
2868               p = solv->problems.elements[i];
2869               rp = solv->problems.elements[i + 1];
2870               i += 2;
2871               if (p == 0 && rp == 0)
2872                 {
2873                   /* end of this solution reached */
2874                   printf("\n");
2875                   break;
2876                 }
2877               if (p == 0)
2878                 {
2879                   /* job, p is index into job queue */
2880                   what = job->elements[rp];
2881                   switch (job->elements[rp - 1])
2882                     {
2883                     case SOLVER_INSTALL_SOLVABLE:
2884                       s = pool->solvables + what;
2885                       if (what >= solv->installed->start && what < solv->installed->start + solv->installed->nsolvables)
2886                         printf("- do not keep %s-%s.%s installed\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2887                       else
2888                         printf("- do not install %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2889                       break;
2890                     case SOLVER_ERASE_SOLVABLE:
2891                       s = pool->solvables + what;
2892                       if (what >= solv->installed->start && what < solv->installed->start + solv->installed->nsolvables)
2893                         printf("- do not deinstall %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2894                       else
2895                         printf("- do not forbid installation of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
2896                       break;
2897                     case SOLVER_INSTALL_SOLVABLE_NAME:
2898                       printf("- do not install %s\n", id2str(pool, what));
2899                       break;
2900                     case SOLVER_ERASE_SOLVABLE_NAME:
2901                       printf("- do not deinstall %s\n", id2str(pool, what));
2902                       break;
2903                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
2904                       printf("- do not install a solvable providing %s\n", dep2str(pool, what));
2905                       break;
2906                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
2907                       printf("- do not deinstall all solvables providing %s\n", dep2str(pool, what));
2908                       break;
2909                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
2910                       s = pool->solvables + what;
2911                       printf("- do not install most recent version of %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool
2912     , s->arch));
2913                       break;
2914                     default:
2915                       printf("- do something different\n");
2916                       break;
2917                     }
2918                 }
2919               else
2920                 {
2921                   /* policy, replace p with rp */
2922                   s = pool->solvables + p;
2923                   sd = rp ? pool->solvables + rp : 0;
2924                   if (sd)
2925                     {
2926                       int gotone = 0;
2927                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr) > 0)
2928                         {
2929                           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));
2930                           gotone = 1;
2931                         }
2932                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(pool, s, sd))
2933                         {
2934                           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));
2935                           gotone = 1;
2936                         }
2937                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(pool, s, sd))
2938                         {
2939                           if (sd->vendor)
2940                             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));
2941                           else
2942                             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));
2943                           gotone = 1;
2944                         }
2945                       if (!gotone)
2946                         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));
2947                     }
2948                   else
2949                     {
2950                       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));
2951                     }
2952
2953                 }
2954             }
2955         }
2956     }
2957 }
2958
2959
2960 /* for each installed solvable find which packages with *different* names
2961  * obsolete the solvable.
2962  * this index is used in policy_findupdatepackages if noupdateprovide is set.
2963  */
2964
2965 static void
2966 create_obsolete_index(Solver *solv)
2967 {
2968   Pool *pool = solv->pool;
2969   Solvable *s;
2970   Repo *installed = solv->installed;
2971   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
2972   int i, n;
2973
2974   /* create reverse obsoletes map for installed solvables */
2975   solv->obsoletes = obsoletes = xcalloc(installed->nsolvables, sizeof(Id));
2976   for (i = 1; i < pool->nsolvables; i++)
2977     {
2978       s = pool->solvables + i;
2979       if (!s->obsoletes)
2980         continue;
2981       if (!pool_installable(pool, s))
2982         continue;
2983       obsp = s->repo->idarraydata + s->obsoletes;
2984       while ((obs = *obsp++) != 0)
2985         FOR_PROVIDES(p, pp, obs)
2986           {
2987             if (p < installed->start || p >= installed->start + installed->nsolvables)
2988               continue;
2989             if (pool->solvables[p].name == s->name)
2990               continue;
2991             obsoletes[p - installed->start]++;
2992           }
2993     }
2994   n = 0;
2995   for (i = 0; i < installed->nsolvables; i++)
2996     if (obsoletes[i])
2997       {
2998         n += obsoletes[i] + 1;
2999         obsoletes[i] = n;
3000       }
3001   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
3002   if (pool->verbose) printf("obsoletes data: %d entries\n", n + 1);
3003   for (i = pool->nsolvables - 1; i > 0; i--)
3004     {
3005       s = pool->solvables + i;
3006       if (!s->obsoletes)
3007         continue;
3008       if (!pool_installable(pool, s))
3009         continue;
3010       obsp = s->repo->idarraydata + s->obsoletes;
3011       while ((obs = *obsp++) != 0)
3012         FOR_PROVIDES(p, pp, obs)
3013           {
3014             if (p < installed->start || p >= installed->start + installed->nsolvables)
3015               continue;
3016             if (pool->solvables[p].name == s->name)
3017               continue;
3018             p -= installed->start;
3019             if (obsoletes_data[obsoletes[p]] != i)
3020               obsoletes_data[--obsoletes[p]] = i;
3021           }
3022     }
3023 }
3024
3025
3026 /*-----------------------------------------------------------------*/
3027 /* main() */
3028
3029 /*
3030  *
3031  * solve job queue
3032  *
3033  */
3034
3035 void
3036 solve(Solver *solv, Queue *job)
3037 {
3038   Pool *pool = solv->pool;
3039   int i;
3040   Map addedmap;                        /* '1' == have rule for solvable */
3041   Id how, what, p, *pp, d;
3042   Queue q;
3043   Solvable *s;
3044
3045   /* create obsolete index if needed */
3046   if (solv->noupdateprovide && solv->installed->nsolvables)
3047     create_obsolete_index(solv);
3048
3049   /*
3050    * create basic rule set of all involved packages
3051    * use addedmap bitmap to make sure we don't create rules twice
3052    *
3053    */
3054
3055   map_init(&addedmap, pool->nsolvables);
3056   queue_init(&q);
3057
3058   /*
3059    * always install our system solvable
3060    */
3061   MAPSET(&addedmap, SYSTEMSOLVABLE);
3062   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3063   queue_push(&solv->decisionq_why, 0);
3064   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3065
3066   /*
3067    * create rules for installed solvables -> keep them installed
3068    * so called: rpm rules
3069    *
3070    */
3071   if (solv->pool->verbose > 3)
3072     printf ("*** create rules for installed solvables -> keep them installed ***\n");
3073   for (i = solv->installed->start; i < solv->installed->start + solv->installed->nsolvables; i++)
3074     addrpmrulesforsolvable(solv, pool->solvables + i, &addedmap);
3075
3076   /*
3077    * create install rules
3078    *
3079    * two passes, as we want to keep the rpm rules distinct from the job rules
3080    *
3081    */
3082
3083   /*
3084    * solvable rules
3085    *  process job rules for solvables
3086    */
3087   if (solv->pool->verbose > 3)
3088     printf ("*** create install rules ***\n");
3089
3090   for (i = 0; i < job->count; i += 2)
3091     {
3092       how = job->elements[i];
3093       what = job->elements[i + 1];
3094
3095       switch(how)
3096         {
3097         case SOLVER_INSTALL_SOLVABLE:
3098           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3099           break;
3100         case SOLVER_INSTALL_SOLVABLE_NAME:
3101         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3102           FOR_PROVIDES(p, pp, what)
3103             {
3104               /* if by name, ensure that the name matches */
3105               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3106                 continue;
3107               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3108             }
3109           break;
3110         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3111           /* dont allow downgrade */
3112           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3113           break;
3114         }
3115     }
3116
3117   for (i = solv->installed->start; i < solv->installed->start + solv->installed->nsolvables; i++)
3118     addrpmrulesforupdaters(solv, pool->solvables + i, &addedmap, 1);
3119
3120   if (solv->pool->verbose > 3)
3121       printf ("*** Add rules for week dependencies ***\n");
3122
3123
3124   addrpmrulesforweak(solv, &addedmap);
3125
3126 #if 1
3127   if (pool->verbose)
3128     {
3129       int possible = 0, installable = 0;
3130       for (i = 1; i < pool->nsolvables; i++)
3131         {
3132           if (pool_installable(pool, pool->solvables + i))
3133             installable++;
3134           if (MAPTST(&addedmap, i))
3135             possible++;
3136         }
3137       printf("%d of %d installable solvables used for solving\n", possible, installable);
3138     }
3139 #endif
3140
3141   /*
3142    * first pass done, we now have all the rpm rules we need.
3143    * unify existing rules before going over all job rules and
3144    * policy rules.
3145    * at this point the system is always solvable,
3146    * as an empty system (remove all packages) is a valid solution
3147    */
3148
3149   unifyrules(solv);     /* remove duplicate rpm rules */
3150
3151   if (pool->verbose) printf("Decisions based on %d rpm rules.\n", solv->decisionq.count);
3152
3153   /*
3154    * now add all job rules
3155    */
3156
3157   if (solv->pool->verbose > 3)
3158       printf ("*** Add JOB rules ***\n");
3159
3160   solv->jobrules = solv->nrules;
3161
3162   for (i = 0; i < job->count; i += 2)
3163     {
3164       how = job->elements[i];
3165       what = job->elements[i + 1];
3166       switch(how)
3167         {
3168         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3169           s = pool->solvables + what;
3170           if (solv->rc_output)
3171             {
3172               printf(">!> Installing %s from channel %s\n", id2str(pool, s->name), repo_name(s->repo));
3173             }
3174           if (pool->verbose)
3175             printf("job: install solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3176           addrule(solv, what, 0);                       /* install by Id */
3177           queue_push(&solv->ruletojob, i);
3178           break;
3179         case SOLVER_ERASE_SOLVABLE:
3180           s = pool->solvables + what;
3181           if (pool->verbose)
3182             printf("job: erase solvable %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3183           addrule(solv, -what, 0);                      /* remove by Id */
3184           queue_push(&solv->ruletojob, i);
3185           break;
3186         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3187         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3188           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_NAME)
3189             printf("job: install name %s\n", id2str(pool, what));
3190           if (pool->verbose && how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3191             printf("job: install provides %s\n", dep2str(pool, what));
3192           queue_empty(&q);
3193           FOR_PROVIDES(p, pp, what)
3194             {
3195               /* if by name, ensure that the name matches */
3196               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3197                 continue;
3198               queue_push(&q, p);
3199             }
3200           if (!q.count)
3201             {
3202               /* no provider, make this an impossible rule */
3203               queue_push(&q, -SYSTEMSOLVABLE);
3204             }
3205
3206           p = queue_shift(&q);         /* get first provider */
3207           if (!q.count)
3208             d = 0;                     /* single provider ? -> make assertion */
3209           else
3210             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3211           addrule(solv, p, d);         /* add 'requires' rule */
3212           queue_push(&solv->ruletojob, i);
3213           break;
3214         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3215         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3216           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_NAME)
3217             printf("job: erase name %s\n", id2str(pool, what));
3218           if (pool->verbose && how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3219             printf("job: erase provides %s\n", dep2str(pool, what));
3220           FOR_PROVIDES(p, pp, what)
3221             {
3222               /* if by name, ensure that the name matches */
3223               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3224                 continue;
3225               addrule(solv, -p, 0);  /* add 'remove' rule */
3226               queue_push(&solv->ruletojob, i);
3227             }
3228           break;
3229         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3230           s = pool->solvables + what;
3231           if (pool->verbose)
3232             printf("job: update %s-%s.%s\n", id2str(pool, s->name), id2str(pool, s->evr), id2str(pool, s->arch));
3233           addupdaterule(solv, s, 0);
3234           queue_push(&solv->ruletojob, i);
3235           break;
3236         }
3237     }
3238
3239   if (solv->ruletojob.count != solv->nrules - solv->jobrules)
3240     abort();
3241
3242   /*
3243    * now add system rules
3244    *
3245    */
3246
3247  if (solv->pool->verbose > 3)
3248      printf ("*** Add system rules ***\n");
3249
3250
3251   solv->systemrules = solv->nrules;
3252
3253   /*
3254    * create rules for updating installed solvables
3255    *
3256    */
3257
3258   if (!solv->allowuninstall)
3259     {                                  /* loop over all installed solvables */
3260       /* we create all update rules, but disable some later on depending on the job */
3261       for (i = solv->installed->start; i < solv->installed->start + solv->installed->nsolvables; i++)
3262         addupdaterule(solv, pool->solvables + i, 0);
3263       /* consistency check: we added a rule for _every_ system solvable */
3264       if (solv->nrules - solv->systemrules != solv->installed->nsolvables)
3265         abort();
3266     }
3267
3268   /* create special weak system rules */
3269   /* those are used later on to keep a version of the installed packages in
3270      best effort mode */
3271   if (solv->installed->nsolvables)
3272     {
3273       solv->weaksystemrules = xcalloc(solv->installed->nsolvables, sizeof(Id));
3274       for (i = 0; i < solv->installed->nsolvables; i++)
3275         {
3276           policy_findupdatepackages(solv, pool->solvables + solv->installed->start + i, &q, 1);
3277           if (q.count)
3278             solv->weaksystemrules[i] = pool_queuetowhatprovides(pool, &q);
3279         }
3280     }
3281
3282   /* free unneeded memory */
3283   map_free(&addedmap);
3284   queue_free(&q);
3285
3286   solv->weakrules = solv->nrules;
3287
3288   /* try real hard to keep packages installed */
3289   if (0)
3290     {
3291       for (i = 0; i < solv->installed->nsolvables; i++)
3292         {
3293           /* FIXME: can't work with refine_suggestion! */
3294           /* need to always add the rule but disable it */
3295           if (MAPTST(&solv->noupdate, i))
3296             continue;
3297           d = solv->weaksystemrules[i];
3298           addrule(solv, solv->installed->start + i, d);
3299         }
3300     }
3301
3302   /*
3303    * solve !
3304    *
3305    */
3306
3307   disableupdaterules(solv, job, -1);
3308   makeruledecisions(solv);
3309
3310   if (pool->verbose) printf("problems so far: %d\n", solv->problems.count);
3311
3312   run_solver(solv, 1, 1);
3313
3314   /* find suggested packages */
3315   if (!solv->problems.count)
3316     {
3317       Id sug, *sugp, p, *pp;
3318
3319       /* create map of all suggests that are still open */
3320       solv->recommends_index = -1;
3321       MAPZERO(&solv->suggestsmap);
3322       for (i = 0; i < solv->decisionq.count; i++)
3323         {
3324           p = solv->decisionq.elements[i];
3325           if (p < 0)
3326             continue;
3327           s = pool->solvables + p;
3328           if (s->suggests)
3329             {
3330               sugp = s->repo->idarraydata + s->suggests;
3331               while ((sug = *sugp++) != 0)
3332                 {
3333                   FOR_PROVIDES(p, pp, sug)
3334                     if (solv->decisionmap[p] > 0)
3335                       break;
3336                   if (p)
3337                     continue;   /* already fulfilled */
3338                   FOR_PROVIDES(p, pp, sug)
3339                     MAPSET(&solv->suggestsmap, p);
3340                 }
3341             }
3342         }
3343       for (i = 1; i < pool->nsolvables; i++)
3344         {
3345           if (solv->decisionmap[i] != 0)
3346             continue;
3347           s = pool->solvables + i;
3348           if (!MAPTST(&solv->suggestsmap, i))
3349             {
3350               if (!s->enhances)
3351                 continue;
3352               if (!pool_installable(pool, s))
3353                 continue;
3354               if (!solver_is_enhancing(solv, s))
3355                 continue;
3356             }
3357           queue_push(&solv->suggestions, i);
3358         }
3359       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3360     }
3361
3362   if (solv->problems.count)
3363     problems_to_solutions(solv, job);
3364 }
3365