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