src/solver.c

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