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