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