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, l1num = 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       /* go through all literals of the rule */
1436       for (i = -1; ; i++)
1437         {
1438           if (i == -1)
1439             v = c->p;
1440           else if (c->d == 0)
1441             v = i ? 0 : c->w2;
1442           else
1443             v = *dp++;
1444           if (v == 0)
1445             break;
1446
1447           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1448             continue;
1449           vv = v > 0 ? v : -v;
1450           if (MAPTST(&seen, vv))
1451             continue;
1452           l = solv->decisionmap[vv];
1453           if (l < 0)
1454             l = -l;
1455           if (l == 1)
1456             {
1457               /* a level 1 literal, mark it for later */
1458 #if 0
1459               int j;
1460               for (j = 0; j < solv->decisionq.count; j++)
1461                 if (solv->decisionq.elements[j] == v)
1462                   break;
1463               if (j == solv->decisionq.count)
1464                 abort();
1465               queue_push(&rulq, -(j + 1));
1466 #endif
1467               MAPSET(&seen, vv);        /* mark for scanning in level 1 phase */
1468               l1num++;
1469               continue;
1470             }
1471           MAPSET(&seen, vv);
1472           if (l == level)
1473             num++;                      /* need to do this one as well */
1474           else
1475             {
1476               queue_push(&r, v);
1477               if (l > rlevel)
1478                 rlevel = l;
1479             }
1480         }
1481       if (num <= 0)
1482         abort();
1483       for (;;)
1484         {
1485           v = solv->decisionq.elements[--idx];
1486           vv = v > 0 ? v : -v;
1487           if (MAPTST(&seen, vv))
1488             break;
1489         }
1490       c = solv->rules + solv->decisionq_why.elements[idx];
1491       MAPCLR(&seen, vv);
1492       if (--num == 0)
1493         break;
1494     }
1495   *pr = -v;     /* so that v doesn't get lost */
1496
1497   /* add involved level 1 rules */
1498   if (l1num)
1499     {
1500       POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1501       idx++;
1502       while (idx)
1503         {
1504           v = solv->decisionq.elements[--idx];
1505           vv = v > 0 ? v : -v;
1506           if (!MAPTST(&seen, vv))
1507             continue;
1508           if (!solv->decisionq_why.elements[idx])
1509             continue;
1510           c = solv->rules + solv->decisionq_why.elements[idx];
1511           IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1512             printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1513           queue_push(&solv->learnt_pool, c - solv->rules);
1514           for (i = -1; ; i++)
1515             {
1516               if (i == -1)
1517                 v = c->p;
1518               else if (c->d == 0)
1519                 v = i ? 0 : c->w2;
1520               else
1521                 v = *dp++;
1522               if (v == 0)
1523                 break;
1524               if (DECISIONMAP_TRUE(v))  /* the one true literal */
1525                 continue;
1526               vv = v > 0 ? v : -v;
1527               l = solv->decisionmap[vv];
1528               if (l != 1 && l != -1)
1529                 continue;
1530               MAPSET(&seen, vv);
1531             }
1532         }
1533     }
1534
1535   if (r.count == 0)
1536     *dr = 0;
1537   else if (r.count == 1 && r.elements[0] < 0)
1538     *dr = r.elements[0];
1539   else
1540     *dr = pool_queuetowhatprovides(pool, &r);
1541   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1542     {
1543       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1544       printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1545       for (i = 0; i < r.count; i++)
1546         printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1547     }
1548   map_free(&seen);
1549   /* push end marker on learnt reasons stack */
1550   queue_push(&solv->learnt_pool, 0);
1551   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1552     {
1553       for (i = learnt_why; solv->learnt_pool.elements[i]; i++)
1554         {
1555           POOL_DEBUG(SAT_DEBUG_ANALYZE, "learnt_why ");
1556           printrule(solv, SAT_DEBUG_ANALYZE, solv->rules + solv->learnt_pool.elements[i]);
1557         }
1558     }
1559   if (why)
1560     *why = learnt_why;
1561   return rlevel;
1562 }
1563
1564
1565 /*
1566  * reset_solver
1567  * reset the solver decisions to right after the rpm rules.
1568  * called after rules have been enabled/disabled
1569  */
1570
1571 static void
1572 reset_solver(Solver *solv)
1573 {
1574   Pool *pool = solv->pool;
1575   int i;
1576   Id v;
1577
1578   enabledisablelearntrules(solv);
1579
1580   /* redo all direct rpm rule decisions */
1581   /* we break at the first decision with a why attached, this is
1582    * either a job/system rule assertion or a propagated decision */
1583   for (i = 0; i < solv->decisionq.count; i++)
1584     {
1585       v = solv->decisionq.elements[i];
1586       solv->decisionmap[v > 0 ? v : -v] = 0;
1587     }
1588   for (i = 0; i < solv->decisionq_why.count; i++)
1589     if (solv->decisionq_why.elements[i])
1590       break;
1591     else
1592       {
1593         v = solv->decisionq.elements[i];
1594         solv->decisionmap[v > 0 ? v : -v] = v > 0 ? 1 : -1;
1595       }
1596
1597   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, i);
1598
1599   solv->decisionq_why.count = i;
1600   solv->decisionq.count = i;
1601   solv->recommends_index = -1;
1602   solv->propagate_index = 0;
1603
1604   /* redo all job/system decisions */
1605   makeruledecisions(solv);
1606   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1607   /* recreate watch chains */
1608   makewatches(solv);
1609 }
1610
1611
1612 /*
1613  * analyze_unsolvable_rule
1614  */
1615
1616 static void
1617 analyze_unsolvable_rule(Solver *solv, Rule *r)
1618 {
1619   Pool *pool = solv->pool;
1620   int i;
1621   Id why = r - solv->rules;
1622   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1623      printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1624   if (solv->learntrules && why >= solv->learntrules)
1625     {
1626       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1627         analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1628       return;
1629     }
1630   /* do not add rpm rules to problem */
1631   if (why < solv->jobrules)
1632     return;
1633   /* turn rule into problem */
1634   if (why >= solv->jobrules && why < solv->systemrules)
1635     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1636   /* return if problem already countains our rule */
1637   if (solv->problems.count)
1638     {
1639       for (i = solv->problems.count - 1; i >= 0; i--)
1640         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1641           break;
1642         else if (solv->problems.elements[i] == why)
1643           return;
1644     }
1645   queue_push(&solv->problems, why);
1646 }
1647
1648
1649 /*
1650  * analyze_unsolvable
1651  *
1652  * return: 1 - disabled some rules, try again
1653  *         0 - hopeless
1654  */
1655
1656 static int
1657 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1658 {
1659   Pool *pool = solv->pool;
1660   Rule *r;
1661   Map seen;             /* global to speed things up? */
1662   Id v, vv, *dp, why;
1663   int l, i, idx;
1664   Id *decisionmap = solv->decisionmap;
1665   int oldproblemcount;
1666   int oldlearntpoolcount;
1667   int lastweak;
1668
1669   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1670   oldproblemcount = solv->problems.count;
1671   oldlearntpoolcount = solv->learnt_pool.count;
1672
1673   /* make room for proof index */
1674   /* must update it later, as analyze_unsolvable_rule would confuse
1675    * it with a rule index if we put the real value in already */
1676   queue_push(&solv->problems, 0);
1677
1678   r = cr;
1679   map_init(&seen, pool->nsolvables);
1680   queue_push(&solv->learnt_pool, r - solv->rules);
1681   analyze_unsolvable_rule(solv, r);
1682   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1683   for (i = -1; ; i++)
1684     {
1685       if (i == -1)
1686         v = r->p;
1687       else if (r->d == 0)
1688         v = i ? 0 : r->w2;
1689       else
1690         v = *dp++;
1691       if (v == 0)
1692         break;
1693       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1694           continue;
1695       vv = v > 0 ? v : -v;
1696       l = solv->decisionmap[vv];
1697       if (l < 0)
1698         l = -l;
1699       MAPSET(&seen, vv);
1700     }
1701   idx = solv->decisionq.count;
1702   while (idx > 0)
1703     {
1704       v = solv->decisionq.elements[--idx];
1705       vv = v > 0 ? v : -v;
1706       if (!MAPTST(&seen, vv))
1707         continue;
1708       why = solv->decisionq_why.elements[idx];
1709       if (!why)
1710         {
1711           /* level 1 and no why, must be an rpm assertion */
1712           IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1713             {
1714               POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "RPM ");
1715               printruleelement(solv, SAT_DEBUG_UNSOLVABLE, 0, v);
1716             }
1717           /* this is the only positive rpm assertion */
1718           if (v == SYSTEMSOLVABLE)
1719             v = -v;
1720           if (v >= 0)
1721             abort();
1722           queue_push(&solv->learnt_pool, v);
1723           continue;
1724         }
1725       r = solv->rules + why;
1726       queue_push(&solv->learnt_pool, why);
1727       analyze_unsolvable_rule(solv, r);
1728       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1729       for (i = -1; ; i++)
1730         {
1731           if (i == -1)
1732             v = r->p;
1733           else if (r->d == 0)
1734             v = i ? 0 : r->w2;
1735           else
1736             v = *dp++;
1737           if (v == 0)
1738             break;
1739           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1740               continue;
1741           vv = v > 0 ? v : -v;
1742           l = solv->decisionmap[vv];
1743           if (l < 0)
1744             l = -l;
1745           MAPSET(&seen, vv);
1746         }
1747     }
1748   map_free(&seen);
1749   queue_push(&solv->problems, 0);       /* mark end of this problem */
1750
1751   lastweak = 0;
1752   if (solv->weakrules != solv->learntrules)
1753     {
1754       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1755         {
1756           why = solv->problems.elements[i];
1757           if (why < solv->weakrules || why >= solv->learntrules)
1758             continue;
1759           if (!lastweak || lastweak < why)
1760             lastweak = why;
1761         }
1762     }
1763   if (lastweak)
1764     {
1765       /* disable last weak rule */
1766       solv->problems.count = oldproblemcount;
1767       solv->learnt_pool.count = oldlearntpoolcount;
1768       r = solv->rules + lastweak;
1769       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling weak ");
1770       printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
1771       disablerule(solv, r);
1772       reset_solver(solv);
1773       return 1;
1774     }
1775
1776   /* finish proof */
1777   queue_push(&solv->learnt_pool, 0);
1778   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1779
1780   if (disablerules)
1781     {
1782       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1783         disableproblem(solv, solv->problems.elements[i]);
1784       reset_solver(solv);
1785       return 1;
1786     }
1787   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1788   return 0;
1789 }
1790
1791
1792 /*-----------------------------------------------------------------*/
1793 /* Decision revert */
1794
1795 /*
1796  * revert
1797  * revert decision at level
1798  */
1799
1800 static void
1801 revert(Solver *solv, int level)
1802 {
1803   Pool *pool = solv->pool;
1804   Id v, vv;
1805   while (solv->decisionq.count)
1806     {
1807       v = solv->decisionq.elements[solv->decisionq.count - 1];
1808       vv = v > 0 ? v : -v;
1809       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1810         break;
1811       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1812       solv->decisionmap[vv] = 0;
1813       solv->decisionq.count--;
1814       solv->decisionq_why.count--;
1815       solv->propagate_index = solv->decisionq.count;
1816     }
1817   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1818     {
1819       solv->branches.count--;
1820       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1821         solv->branches.count--;
1822     }
1823   solv->recommends_index = -1;
1824 }
1825
1826
1827 /*
1828  * watch2onhighest - put watch2 on literal with highest level
1829  */
1830
1831 static inline void
1832 watch2onhighest(Solver *solv, Rule *r)
1833 {
1834   int l, wl = 0;
1835   Id v, *dp;
1836
1837   if (!r->d)
1838     return;     /* binary rule, both watches are set */
1839   dp = solv->pool->whatprovidesdata + r->d;
1840   while ((v = *dp++) != 0)
1841     {
1842       l = solv->decisionmap[v < 0 ? -v : v];
1843       if (l < 0)
1844         l = -l;
1845       if (l > wl)
1846         {
1847           r->w2 = dp[-1];
1848           wl = l;
1849         }
1850     }
1851 }
1852
1853
1854 /*
1855  * setpropagatelearn
1856  *
1857  * add free decision to decision q, increase level
1858  * propagate decision, return if no conflict.
1859  * in conflict case, analyze conflict rule, add resulting
1860  * rule to learnt rule set, make decision from learnt
1861  * rule (always unit) and re-propagate.
1862  */
1863
1864 static int
1865 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1866 {
1867   Pool *pool = solv->pool;
1868   Rule *r;
1869   Id p, d;
1870   int l, why;
1871
1872   if (decision)
1873     {
1874       level++;
1875       if (decision > 0)
1876         solv->decisionmap[decision] = level;
1877       else
1878         solv->decisionmap[-decision] = -level;
1879       queue_push(&solv->decisionq, decision);
1880       queue_push(&solv->decisionq_why, 0);
1881     }
1882   for (;;)
1883     {
1884       r = propagate(solv, level);
1885       if (!r)
1886         break;
1887       if (level == 1)
1888         return analyze_unsolvable(solv, r, disablerules);
1889       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
1890       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1891       if (l >= level || l <= 0)
1892         abort();
1893       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
1894       level = l;
1895       revert(solv, level);
1896       r = addrule(solv, p, d);       /* p requires d */
1897       if (!r)
1898         abort();
1899       if (solv->learnt_why.count != (r - solv->rules) - solv->learntrules)
1900         abort();
1901       queue_push(&solv->learnt_why, why);
1902       if (d)
1903         {
1904           /* at least 2 literals, needs watches */
1905           watch2onhighest(solv, r);
1906           addwatches(solv, r);
1907         }
1908       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1909       queue_push(&solv->decisionq, p);
1910       queue_push(&solv->decisionq_why, r - solv->rules);
1911       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1912         {
1913           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
1914           printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
1915           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
1916           printrule(solv, SAT_DEBUG_ANALYZE, r);
1917         }
1918     }
1919   return level;
1920 }
1921
1922
1923 /*
1924  * install best package from the queue. We add an extra package, inst, if
1925  * provided. See comment in weak install section.
1926  */
1927 static int
1928 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1929 {
1930   Pool *pool = solv->pool;
1931   Id p;
1932   int i;
1933
1934   if (dq->count > 1 || inst)
1935     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1936
1937   i = 0;
1938   if (dq->count > 1)
1939     {
1940       /* choose the supplemented one */
1941       for (i = 0; i < dq->count; i++)
1942         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1943           break;
1944       if (i == dq->count)
1945         {
1946           for (i = 1; i < dq->count; i++)
1947             queue_push(&solv->branches, dq->elements[i]);
1948           queue_push(&solv->branches, -level);
1949           i = 0;
1950         }
1951     }
1952   p = dq->elements[i];
1953
1954   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
1955
1956   return setpropagatelearn(solv, level, p, disablerules);
1957 }
1958
1959
1960 /*-----------------------------------------------------------------*/
1961 /* Main solver interface */
1962
1963
1964 /*
1965  * solver_create
1966  * create solver structure
1967  *
1968  * pool: all available solvables
1969  * installed: installed Solvables
1970  *
1971  *
1972  * Upon solving, rules are created to flag the Solvables
1973  * of the 'installed' Repo as installed.
1974  */
1975
1976 Solver *
1977 solver_create(Pool *pool, Repo *installed)
1978 {
1979   Solver *solv;
1980   solv = (Solver *)xcalloc(1, sizeof(Solver));
1981   solv->pool = pool;
1982   solv->installed = installed;
1983
1984   queue_init(&solv->ruletojob);
1985   queue_init(&solv->decisionq);
1986   queue_init(&solv->decisionq_why);
1987   queue_init(&solv->problems);
1988   queue_init(&solv->suggestions);
1989   queue_init(&solv->learnt_why);
1990   queue_init(&solv->learnt_pool);
1991   queue_init(&solv->branches);
1992
1993   map_init(&solv->recommendsmap, pool->nsolvables);
1994   map_init(&solv->suggestsmap, pool->nsolvables);
1995   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
1996   solv->recommends_index = 0;
1997
1998   solv->decisionmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
1999   solv->rules = (Rule *)xmalloc((solv->nrules + (RULES_BLOCK + 1)) * sizeof(Rule));
2000   memset(solv->rules, 0, sizeof(Rule));
2001   solv->nrules = 1;
2002
2003   return solv;
2004 }
2005
2006
2007 /*
2008  * solver_free
2009  */
2010
2011 void
2012 solver_free(Solver *solv)
2013 {
2014   queue_free(&solv->ruletojob);
2015   queue_free(&solv->decisionq);
2016   queue_free(&solv->decisionq_why);
2017   queue_free(&solv->learnt_why);
2018   queue_free(&solv->learnt_pool);
2019   queue_free(&solv->problems);
2020   queue_free(&solv->suggestions);
2021   queue_free(&solv->branches);
2022
2023   map_free(&solv->recommendsmap);
2024   map_free(&solv->suggestsmap);
2025   map_free(&solv->noupdate);
2026   xfree(solv->decisionmap);
2027   xfree(solv->rules);
2028   xfree(solv->watches);
2029   xfree(solv->weaksystemrules);
2030   xfree(solv->obsoletes);
2031   xfree(solv->obsoletes_data);
2032   xfree(solv);
2033 }
2034
2035
2036 /*-------------------------------------------------------*/
2037
2038 /*
2039  * run_solver
2040  *
2041  * all rules have been set up, now actually run the solver
2042  *
2043  */
2044
2045 static void
2046 run_solver(Solver *solv, int disablerules, int doweak)
2047 {
2048   Queue dq;
2049   int systemlevel;
2050   int level, olevel;
2051   Rule *r;
2052   int i, j, n;
2053   Solvable *s;
2054   Pool *pool = solv->pool;
2055   Id p, *dp;
2056
2057   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2058     {
2059       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2060       for (i = 0; i < solv->nrules; i++)
2061         printrule(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2062     }
2063
2064   /* create watches chains */
2065   makewatches(solv);
2066
2067   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2068
2069   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2070     printdecisions(solv);
2071
2072   /* start SAT algorithm */
2073   level = 1;
2074   systemlevel = level + 1;
2075   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2076
2077   queue_init(&dq);
2078   for (;;)
2079     {
2080       /*
2081        * propagate
2082        */
2083
2084       if (level == 1)
2085         {
2086           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2087           if ((r = propagate(solv, level)) != 0)
2088             {
2089               if (analyze_unsolvable(solv, r, disablerules))
2090                 continue;
2091               queue_free(&dq);
2092               return;
2093             }
2094         }
2095
2096       /*
2097        * installed packages
2098        */
2099
2100       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2101         {
2102           if (!solv->updatesystem)
2103             {
2104               /* try to keep as many packages as possible */
2105               POOL_DEBUG(SAT_DEBUG_STATS, "installing system packages\n");
2106               for (i = solv->installed->start, n = 0; ; i++)
2107                 {
2108                   if (n == solv->installed->nsolvables)
2109                     break;
2110                   if (i == solv->installed->end)
2111                     i = solv->installed->start;
2112                   s = pool->solvables + i;
2113                   if (s->repo != solv->installed)
2114                     continue;
2115                   n++;
2116                   if (solv->decisionmap[i] != 0)
2117                     continue;
2118                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2119                   olevel = level;
2120                   level = setpropagatelearn(solv, level, i, disablerules);
2121                   if (level == 0)
2122                     {
2123                       queue_free(&dq);
2124                       return;
2125                     }
2126                   if (level <= olevel)
2127                     n = 0;
2128                 }
2129             }
2130           if (solv->weaksystemrules)
2131             {
2132               POOL_DEBUG(SAT_DEBUG_STATS, "installing weak system packages\n");
2133               for (i = solv->installed->start; i < solv->installed->end; i++)
2134                 {
2135                   if (pool->solvables[i].repo != solv->installed)
2136                     continue;
2137                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
2138                     continue;
2139                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2140                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2141                     continue;
2142                   queue_empty(&dq);
2143                   if (solv->weaksystemrules[i - solv->installed->start])
2144                     {
2145                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
2146                       while ((p = *dp++) != 0)
2147                         {
2148                           if (solv->decisionmap[p] > 0)
2149                             break;
2150                           if (solv->decisionmap[p] == 0)
2151                             queue_push(&dq, p);
2152                         }
2153                       if (p)
2154                         continue;       /* update package already installed */
2155                     }
2156                   if (!dq.count && solv->decisionmap[i] != 0)
2157                     continue;
2158                   olevel = level;
2159                   /* FIXME: i is handled a bit different because we do not want
2160                    * to have it pruned just because it is not recommened.
2161                    * we should not prune installed packages instead */
2162                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2163                   if (level == 0)
2164                     {
2165                       queue_free(&dq);
2166                       return;
2167                     }
2168                   if (level <= olevel)
2169                     break;
2170                 }
2171               if (i < solv->installed->end)
2172                 continue;
2173             }
2174           systemlevel = level;
2175         }
2176
2177       /*
2178        * decide
2179        */
2180
2181       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2182       for (i = 1, n = 1; ; i++, n++)
2183         {
2184           if (n == solv->nrules)
2185             break;
2186           if (i == solv->nrules)
2187             i = 1;
2188           r = solv->rules + i;
2189           if (!r->w1)
2190             continue;
2191           queue_empty(&dq);
2192           if (r->d == 0)
2193             {
2194               /* binary or unary rule */
2195               /* need two positive undecided literals */
2196               if (r->p < 0 || r->w2 <= 0)
2197                 continue;
2198               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2199                 continue;
2200               queue_push(&dq, r->p);
2201               queue_push(&dq, r->w2);
2202             }
2203           else
2204             {
2205               /* make sure that
2206                * all negative literals are installed
2207                * no positive literal is installed
2208                * i.e. the rule is not fulfilled and we
2209                * just need to decide on the positive literals
2210                */
2211               if (r->p < 0)
2212                 {
2213                   if (solv->decisionmap[-r->p] <= 0)
2214                     continue;
2215                 }
2216               else
2217                 {
2218                   if (solv->decisionmap[r->p] > 0)
2219                     continue;
2220                   if (solv->decisionmap[r->p] == 0)
2221                     queue_push(&dq, r->p);
2222                 }
2223               dp = pool->whatprovidesdata + r->d;
2224               while ((p = *dp++) != 0)
2225                 {
2226                   if (p < 0)
2227                     {
2228                       if (solv->decisionmap[-p] <= 0)
2229                         break;
2230                     }
2231                   else
2232                     {
2233                       if (solv->decisionmap[p] > 0)
2234                         break;
2235                       if (solv->decisionmap[p] == 0)
2236                         queue_push(&dq, p);
2237                     }
2238                 }
2239               if (p)
2240                 continue;
2241             }
2242           if (dq.count < 2)
2243             {
2244               /* cannot happen as this means that
2245                * the rule is unit */
2246               printrule(solv, SAT_FATAL, r);
2247               abort();
2248             }
2249           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2250             {
2251               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2252               printrule(solv, SAT_DEBUG_PROPAGATE, r);
2253             }
2254
2255           olevel = level;
2256           level = selectandinstall(solv, level, &dq, 0, disablerules);
2257           if (level == 0)
2258             {
2259               queue_free(&dq);
2260               return;
2261             }
2262           if (level < systemlevel)
2263             break;
2264           n = 0;
2265         } /* for(), decide */
2266
2267       if (n != solv->nrules)    /* continue if level < systemlevel */
2268         continue;
2269
2270       if (doweak && !solv->problems.count)
2271         {
2272           int qcount;
2273
2274           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2275           if (!REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2276             {
2277               for (i = 0; i < solv->decisionq.count; i++)
2278                 {
2279                   p = solv->decisionq.elements[i];
2280                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2281                     solv->decisionmap[p] = -solv->decisionmap[p];
2282                 }
2283             }
2284           queue_empty(&dq);
2285           for (i = 1; i < pool->nsolvables; i++)
2286             {
2287               if (solv->decisionmap[i] < 0)
2288                 continue;
2289               if (solv->decisionmap[i] > 0)
2290                 {
2291                   Id *recp, rec, *pp, p;
2292                   s = pool->solvables + i;
2293                   /* installed, check for recommends */
2294                   /* XXX need to special case AND ? */
2295                   if (s->recommends)
2296                     {
2297                       recp = s->repo->idarraydata + s->recommends;
2298                       while ((rec = *recp++) != 0)
2299                         {
2300                           qcount = dq.count;
2301                           FOR_PROVIDES(p, pp, rec)
2302                             {
2303                               if (solv->decisionmap[p] > 0)
2304                                 {
2305                                   dq.count = qcount;
2306                                   break;
2307                                 }
2308                               else if (solv->decisionmap[p] == 0)
2309                                 {
2310                                   queue_pushunique(&dq, p);
2311                                 }
2312                             }
2313                         }
2314                     }
2315                 }
2316               else
2317                 {
2318                   s = pool->solvables + i;
2319                   if (!s->supplements && !s->freshens)
2320                     continue;
2321                   if (!pool_installable(pool, s))
2322                     continue;
2323                   if (solver_is_supplementing(solv, s))
2324                     queue_pushunique(&dq, i);
2325                 }
2326             }
2327           if (!REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2328             {
2329               for (i = 0; i < solv->decisionq.count; i++)
2330                 {
2331                   p = solv->decisionq.elements[i];
2332                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2333                     solv->decisionmap[p] = -solv->decisionmap[p];
2334                 }
2335             }
2336           if (dq.count)
2337             {
2338               if (dq.count > 1)
2339                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2340               p = dq.elements[0];
2341               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2342               level = setpropagatelearn(solv, level, p, 0);
2343               continue;
2344             }
2345         }
2346
2347      if (solv->solution_callback)
2348         {
2349           solv->solution_callback(solv, solv->solution_callback_data);
2350           if (solv->branches.count)
2351             {
2352               int i = solv->branches.count - 1;
2353               int l = -solv->branches.elements[i];
2354               for (; i > 0; i--)
2355                 if (solv->branches.elements[i - 1] < 0)
2356                   break;
2357               p = solv->branches.elements[i];
2358               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2359               queue_empty(&dq);
2360               for (j = i + 1; j < solv->branches.count; j++)
2361                 queue_push(&dq, solv->branches.elements[j]);
2362               solv->branches.count = i;
2363               level = l;
2364               revert(solv, level);
2365               if (dq.count > 1)
2366                 for (j = 0; j < dq.count; j++)
2367                   queue_push(&solv->branches, dq.elements[j]);
2368               olevel = level;
2369               level = setpropagatelearn(solv, level, p, disablerules);
2370               if (level == 0)
2371                 {
2372                   queue_free(&dq);
2373                   return;
2374                 }
2375               continue;
2376             }
2377           /* all branches done, we're finally finished */
2378           break;
2379         }
2380
2381       /* minimization step */
2382      if (solv->branches.count)
2383         {
2384           int l = 0, lasti = -1, lastl = -1;
2385           p = 0;
2386           for (i = solv->branches.count - 1; i >= 0; i--)
2387             {
2388               p = solv->branches.elements[i];
2389               if (p < 0)
2390                 l = -p;
2391               else if (p > 0 && solv->decisionmap[p] > l + 1)
2392                 {
2393                   lasti = i;
2394                   lastl = l;
2395                 }
2396             }
2397           if (lasti >= 0)
2398             {
2399               /* kill old solvable so that we do not loop */
2400               p = solv->branches.elements[lasti];
2401               solv->branches.elements[lasti] = 0;
2402               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2403
2404               level = lastl;
2405               revert(solv, level);
2406               olevel = level;
2407               level = setpropagatelearn(solv, level, p, disablerules);
2408               if (level == 0)
2409                 {
2410                   queue_free(&dq);
2411                   return;
2412                 }
2413               continue;
2414             }
2415         }
2416       break;
2417     }
2418   queue_free(&dq);
2419 }
2420
2421
2422 /*
2423  * refine_suggestion
2424  * at this point, all rules that led to conflicts are disabled.
2425  * we re-enable all rules of a problem set but rule "sug", then
2426  * continue to disable more rules until there as again a solution.
2427  */
2428
2429 /* FIXME: think about conflicting assertions */
2430
2431 static void
2432 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2433 {
2434   Pool *pool = solv->pool;
2435   Rule *r;
2436   int i, j;
2437   Id v;
2438   Queue disabled;
2439   int disabledcnt;
2440
2441   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2442     {
2443       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2444       for (i = 0; problem[i]; i++)
2445         {
2446           if (problem[i] == sug)
2447             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2448           printproblem(solv, problem[i]);
2449         }
2450     }
2451   queue_init(&disabled);
2452   queue_empty(refined);
2453   queue_push(refined, sug);
2454
2455   /* re-enable all problem rules with the exception of "sug" */
2456   revert(solv, 1);
2457   reset_solver(solv);
2458
2459   for (i = 0; problem[i]; i++)
2460     if (problem[i] != sug)
2461       enableproblem(solv, problem[i]);
2462
2463   if (sug < 0)
2464     disableupdaterules(solv, job, -(sug + 1));
2465
2466   for (;;)
2467     {
2468       /* re-enable as many weak rules as possible */
2469       for (i = solv->weakrules; i < solv->learntrules; i++)
2470         {
2471           r = solv->rules + i;
2472           if (!r->w1)
2473             enablerule(solv, r);
2474         }
2475
2476       queue_empty(&solv->problems);
2477       revert(solv, 1);          /* XXX move to reset_solver? */
2478       reset_solver(solv);
2479
2480       run_solver(solv, 0, 0);
2481       if (!solv->problems.count)
2482         {
2483           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2484           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2485             printdecisions(solv);
2486           break;                /* great, no more problems */
2487         }
2488       disabledcnt = disabled.count;
2489       /* skip over proof index */
2490       for (i = 1; i < solv->problems.count - 1; i++)
2491         {
2492           /* ignore solutions in refined */
2493           v = solv->problems.elements[i];
2494           if (v == 0)
2495             break;      /* end of problem reached */
2496           for (j = 0; problem[j]; j++)
2497             if (problem[j] != sug && problem[j] == v)
2498               break;
2499           if (problem[j])
2500             continue;
2501           queue_push(&disabled, v);
2502         }
2503       if (disabled.count == disabledcnt)
2504         {
2505           /* no solution found, this was an invalid suggestion! */
2506           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2507           refined->count = 0;
2508           break;
2509         }
2510       if (disabled.count == disabledcnt + 1)
2511         {
2512           /* just one suggestion, add it to refined list */
2513           v = disabled.elements[disabledcnt];
2514           queue_push(refined, v);
2515           disableproblem(solv, v);
2516           if (v < 0)
2517             disableupdaterules(solv, job, -(v + 1));
2518         }
2519       else
2520         {
2521           /* more than one solution, disable all */
2522           /* do not push anything on refine list */
2523           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2524             {
2525               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2526               for (i = disabledcnt; i < disabled.count; i++)
2527                 printproblem(solv, disabled.elements[i]);
2528             }
2529           for (i = disabledcnt; i < disabled.count; i++)
2530             disableproblem(solv, disabled.elements[i]);
2531         }
2532     }
2533   /* all done, get us back into the same state as before */
2534   /* enable refined rules again */
2535   for (i = 0; i < disabled.count; i++)
2536     enableproblem(solv, disabled.elements[i]);
2537   /* disable problem rules again */
2538   for (i = 0; problem[i]; i++)
2539     disableproblem(solv, problem[i]);
2540   disableupdaterules(solv, job, -1);
2541   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2542 }
2543
2544 static void
2545 problems_to_solutions(Solver *solv, Queue *job)
2546 {
2547   Pool *pool = solv->pool;
2548   Queue problems;
2549   Queue solution;
2550   Queue solutions;
2551   Id *problem;
2552   Id why;
2553   int i, j;
2554
2555   if (!solv->problems.count)
2556     return;
2557   queue_clone(&problems, &solv->problems);
2558   queue_init(&solution);
2559   queue_init(&solutions);
2560   /* copy over proof index */
2561   queue_push(&solutions, problems.elements[0]);
2562   problem = problems.elements + 1;
2563   for (i = 1; i < problems.count; i++)
2564     {
2565       Id v = problems.elements[i];
2566       if (v == 0)
2567         {
2568           /* mark end of this problem */
2569           queue_push(&solutions, 0);
2570           queue_push(&solutions, 0);
2571           if (i + 1 == problems.count)
2572             break;
2573           /* copy over proof of next problem */
2574           queue_push(&solutions, problems.elements[i + 1]);
2575           i++;
2576           problem = problems.elements + i + 1;
2577           continue;
2578         }
2579       refine_suggestion(solv, job, problem, v, &solution);
2580       if (!solution.count)
2581         continue;       /* this solution didn't work out */
2582
2583       for (j = 0; j < solution.count; j++)
2584         {
2585           why = solution.elements[j];
2586 #if 0
2587           printproblem(solv, why);
2588 #endif
2589           if (why < 0)
2590             {
2591               queue_push(&solutions, 0);
2592               queue_push(&solutions, -why);
2593             }
2594           else if (why >= solv->systemrules && why < solv->weakrules)
2595             {
2596               Id p, rp = 0;
2597               p = solv->installed->start + (why - solv->systemrules);
2598               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2599                 {
2600                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2601                   for (; *dp; dp++)
2602                     {
2603                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2604                         continue;
2605                       if (solv->decisionmap[*dp] > 0)
2606                         {
2607                           rp = *dp;
2608                           break;
2609                         }
2610                     }
2611                 }
2612               queue_push(&solutions, p);
2613               queue_push(&solutions, rp);
2614             }
2615           else
2616             abort();
2617         }
2618       /* mark end of this solution */
2619       queue_push(&solutions, 0);
2620       queue_push(&solutions, 0);
2621     }
2622   queue_free(&solution);
2623   queue_free(&problems);
2624   /* copy queue over to solutions */
2625   queue_free(&solv->problems);
2626   queue_clone(&solv->problems, &solutions);
2627
2628   /* bring solver back into problem state */
2629   revert(solv, 1);              /* XXX move to reset_solver? */
2630   reset_solver(solv);
2631
2632   if (solv->problems.count != solutions.count)
2633     abort();
2634   queue_free(&solutions);
2635 }
2636
2637 Id
2638 solver_next_problem(Solver *solv, Id problem)
2639 {
2640   Id *pp;
2641   if (problem == 0)
2642     return solv->problems.count ? 1 : 0;
2643   pp = solv->problems.elements + problem;
2644   while (pp[0] || pp[1])
2645     {
2646       /* solution */
2647       pp += 2;
2648       while (pp[0] || pp[1])
2649         pp += 2;
2650       pp += 2;
2651     }
2652   pp += 2;
2653   problem = pp - solv->problems.elements;
2654   if (problem >= solv->problems.count)
2655     return 0;
2656   return problem + 1;
2657 }
2658
2659 Id
2660 solver_next_solution(Solver *solv, Id problem, Id solution)
2661 {
2662   Id *pp;
2663   if (solution == 0)
2664     {
2665       solution = problem;
2666       pp = solv->problems.elements + solution;
2667       return pp[0] || pp[1] ? solution : 0;
2668     }
2669   pp = solv->problems.elements + solution;
2670   while (pp[0] || pp[1])
2671     pp += 2;
2672   pp += 2;
2673   solution = pp - solv->problems.elements;
2674   return pp[0] || pp[1] ? solution : 0;
2675 }
2676
2677 Id
2678 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2679 {
2680   Id *pp;
2681   element = element ? element + 2 : solution;
2682   pp = solv->problems.elements + element;
2683   if (!(pp[0] || pp[1]))
2684     return 0;
2685   *p = pp[0];
2686   *rp = pp[1];
2687   return element;
2688 }
2689
2690
2691 /*
2692  * create obsoletesmap from solver decisions
2693  * required for decision handling
2694  */
2695
2696 Id *
2697 create_obsoletesmap(Solver *solv)
2698 {
2699   Pool *pool = solv->pool;
2700   Repo *installed = solv->installed;
2701   Id p, *obsoletesmap = NULL;
2702   int i;
2703   Solvable *s;
2704
2705   obsoletesmap = (Id *)xcalloc(pool->nsolvables, sizeof(Id));
2706   if (installed)
2707     {
2708       for (i = 0; i < solv->decisionq.count; i++)
2709         {
2710           Id *pp, n;
2711
2712           n = solv->decisionq.elements[i];
2713           if (n < 0)
2714             continue;
2715           if (n == SYSTEMSOLVABLE)
2716             continue;
2717           s = pool->solvables + n;
2718           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2719             continue;
2720           FOR_PROVIDES(p, pp, s->name)
2721             if (s->name == pool->solvables[p].name)
2722               {
2723                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2724                   {
2725                     obsoletesmap[p] = n;
2726                     obsoletesmap[n]++;
2727                   }
2728               }
2729         }
2730       for (i = 0; i < solv->decisionq.count; i++)
2731         {
2732           Id obs, *obsp;
2733           Id *pp, n;
2734
2735           n = solv->decisionq.elements[i];
2736           if (n < 0)
2737             continue;
2738           if (n == SYSTEMSOLVABLE)
2739             continue;
2740           s = pool->solvables + n;
2741           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2742             continue;
2743           if (!s->obsoletes)
2744             continue;
2745           obsp = s->repo->idarraydata + s->obsoletes;
2746           while ((obs = *obsp++) != 0)
2747             FOR_PROVIDES(p, pp, obs)
2748               {
2749                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2750                   {
2751                     obsoletesmap[p] = n;
2752                     obsoletesmap[n]++;
2753                   }
2754               }
2755         }
2756     }
2757   return obsoletesmap;
2758 }
2759
2760 /*
2761  * printdecisions
2762  */
2763
2764
2765 void
2766 printdecisions(Solver *solv)
2767 {
2768   Pool *pool = solv->pool;
2769   Repo *installed = solv->installed;
2770   Id p, *obsoletesmap = create_obsoletesmap( solv );
2771   int i;
2772   Solvable *s;
2773
2774   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions -----\n");
2775
2776   /* print solvables to be erased */
2777
2778   if (installed)
2779     {
2780       FOR_REPO_SOLVABLES(installed, p, s)
2781         {
2782           if (solv->decisionmap[p] >= 0)
2783             continue;
2784           if (obsoletesmap[p])
2785             continue;
2786           POOL_DEBUG(SAT_DEBUG_RESULT, "erase   %s\n", solvable2str(pool, s));
2787         }
2788     }
2789
2790   /* print solvables to be installed */
2791
2792   for (i = 0; i < solv->decisionq.count; i++)
2793     {
2794       int j;
2795       p = solv->decisionq.elements[i];
2796       if (p < 0)
2797         {
2798             IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2799             {
2800               p = -p;
2801               s = pool->solvables + p;
2802               POOL_DEBUG(SAT_DEBUG_SCHUBI, "level of %s is %d\n", solvable2str(pool, s), p);
2803             }
2804             continue;
2805         }
2806       if (p == SYSTEMSOLVABLE)
2807         {
2808             POOL_DEBUG(SAT_DEBUG_SCHUBI, "SYSTEMSOLVABLE\n");
2809             continue;
2810         }
2811       s = pool->solvables + p;
2812       if (installed && s->repo == installed)
2813         continue;
2814
2815       if (!obsoletesmap[p])
2816         {
2817           POOL_DEBUG(SAT_DEBUG_RESULT, "install %s", solvable2str(pool, s));
2818         }
2819       else
2820         {
2821           POOL_DEBUG(SAT_DEBUG_RESULT, "update  %s", solvable2str(pool, s));
2822           POOL_DEBUG(SAT_DEBUG_RESULT, "  (obsoletes");
2823           for (j = installed->start; j < installed->end; j++)
2824             if (obsoletesmap[j] == p)
2825               POOL_DEBUG(SAT_DEBUG_RESULT, " %s", solvable2str(pool, pool->solvables + j));
2826           POOL_DEBUG(SAT_DEBUG_RESULT, ")");
2827         }
2828       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
2829     }
2830
2831   xfree(obsoletesmap);
2832
2833   if (solv->suggestions.count)
2834     {
2835       POOL_DEBUG(SAT_DEBUG_RESULT, "\nsuggested packages:\n");
2836       for (i = 0; i < solv->suggestions.count; i++)
2837         {
2838           s = pool->solvables + solv->suggestions.elements[i];
2839           POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
2840         }
2841     }
2842   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions end -----\n");
2843 }
2844
2845 /* this is basically the reverse of addrpmrulesforsolvable */
2846 SolverProbleminfo
2847 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
2848 {
2849   Pool *pool = solv->pool;
2850   Repo *installed = solv->installed;
2851   Rule *r;
2852   Solvable *s;
2853   int dontfix = 0;
2854   Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
2855
2856   if (rid >= solv->weakrules)
2857     abort();
2858   if (rid >= solv->systemrules)
2859     {
2860       *depp = 0;
2861       *sourcep = solv->installed->start + (rid - solv->systemrules);
2862       *targetp = 0;
2863       return SOLVER_PROBLEM_UPDATE_RULE;
2864     }
2865   if (rid >= solv->jobrules)
2866     {
2867
2868       r = solv->rules + rid;
2869       p = solv->ruletojob.elements[rid - solv->jobrules];
2870       *depp = job->elements[p + 1];
2871       *sourcep = p;
2872       *targetp = job->elements[p];
2873       if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE)
2874         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
2875       return SOLVER_PROBLEM_JOB_RULE;
2876     }
2877   if (rid < 0)
2878     {
2879       /* a rpm rule assertion */
2880       if (rid == -SYSTEMSOLVABLE)
2881         abort();        /* can happen only for job rules */
2882       s = pool->solvables - rid;
2883       if (installed && !solv->fixsystem && s->repo == installed)
2884         dontfix = 1;
2885       if (dontfix)      /* dontfix packages never have a neg assertion */
2886         abort();
2887       /* see why the package is not installable */
2888       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
2889         return SOLVER_PROBLEM_NOT_INSTALLABLE;
2890       /* check requires */
2891       if (!s->requires)
2892         abort();
2893       reqp = s->repo->idarraydata + s->requires;
2894       while ((req = *reqp++) != 0)
2895         {
2896           if (req == SOLVABLE_PREREQMARKER)
2897             continue;
2898           dp = pool_whatprovides(pool, req);
2899           if (*dp == 0)
2900             {
2901               *depp = req;
2902               *sourcep = -rid;
2903               *targetp = 0;
2904               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
2905             }
2906         }
2907       abort();
2908     }
2909   r = solv->rules + rid;
2910   if (r->p >= 0)
2911     abort();    /* not a rpm rule */
2912   if (r->d == 0 && r->w2 == 0)
2913     {
2914       /* an assertion. we don't store them as rpm rules, so
2915        * can't happen */
2916       abort();
2917     }
2918   s = pool->solvables - r->p;
2919   if (installed && !solv->fixsystem && s->repo == installed)
2920     dontfix = 1;
2921   if (r->d == 0 && r->w2 < 0)
2922     {
2923       /* a package conflict */
2924       Solvable *s2 = pool->solvables - r->w2;
2925       int dontfix2 = 0;
2926
2927       if (installed && !solv->fixsystem && s2->repo == installed)
2928         dontfix2 = 1;
2929
2930       /* if both packages have the same name and at least one of them
2931        * is not installed, they conflict */
2932       if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
2933         {
2934           *depp = 0;
2935           *sourcep = -r->p;
2936           *targetp = -r->w2;
2937           return SOLVER_PROBLEM_SAME_NAME;
2938         }
2939
2940       /* check conflicts in both directions */
2941       if (s->conflicts)
2942         {
2943           conp = s->repo->idarraydata + s->conflicts;
2944           while ((con = *conp++) != 0)
2945             {
2946               FOR_PROVIDES(p, pp, con)
2947                 {
2948                   if (dontfix && pool->solvables[p].repo == installed)
2949                     continue;
2950                   if (p != -r->w2)
2951                     continue;
2952                   *depp = con;
2953                   *sourcep = -r->p;
2954                   *targetp = p;
2955                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
2956                 }
2957             }
2958         }
2959       if (s2->conflicts)
2960         {
2961           conp = s2->repo->idarraydata + s2->conflicts;
2962           while ((con = *conp++) != 0)
2963             {
2964               FOR_PROVIDES(p, pp, con)
2965                 {
2966                   if (dontfix2 && pool->solvables[p].repo == installed)
2967                     continue;
2968                   if (p != -r->p)
2969                     continue;
2970                   *depp = con;
2971                   *sourcep = -r->w2;
2972                   *targetp = p;
2973                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
2974                 }
2975             }
2976         }
2977       /* check obsoletes in both directions */
2978       if ((!installed || s->repo != installed) && s->obsoletes)
2979         {
2980           obsp = s->repo->idarraydata + s->obsoletes;
2981           while ((obs = *obsp++) != 0)
2982             {
2983               FOR_PROVIDES(p, pp, obs)
2984                 {
2985                   if (p != -r->w2)
2986                     continue;
2987                   *depp = obs;
2988                   *sourcep = -r->p;
2989                   *targetp = p;
2990                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
2991                 }
2992             }
2993         }
2994       if ((!installed || s2->repo != installed) && s2->obsoletes)
2995         {
2996           obsp = s2->repo->idarraydata + s2->obsoletes;
2997           while ((obs = *obsp++) != 0)
2998             {
2999               FOR_PROVIDES(p, pp, obs)
3000                 {
3001                   if (p != -r->p)
3002                     continue;
3003                   *depp = obs;
3004                   *sourcep = -r->w2;
3005                   *targetp = p;
3006                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3007                 }
3008             }
3009         }
3010       /* all cases checked, can't happen */
3011       abort();
3012     }
3013   /* simple requires */
3014   if (!s->requires)
3015     abort();
3016   reqp = s->repo->idarraydata + s->requires;
3017   while ((req = *reqp++) != 0)
3018     {
3019       if (req == SOLVABLE_PREREQMARKER)
3020         continue;
3021       dp = pool_whatprovides(pool, req);
3022       if (r->d == 0)
3023         {
3024           if (*dp == r->w2 && dp[1] == 0)
3025             break;
3026         }
3027       else if (dp - pool->whatprovidesdata == r->d)
3028         break;
3029     }
3030   if (!req)
3031     abort();
3032   *depp = req;
3033   *sourcep = -r->p;
3034   *targetp = 0;
3035   return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3036 }
3037
3038 static void
3039 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3040 {
3041   Id rid;
3042   Id lreqr, lconr, lsysr, ljobr;
3043   Rule *r;
3044   int reqassert = 0;
3045
3046   lreqr = lconr = lsysr = ljobr = 0;
3047   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3048     {
3049       if (rid >= solv->learntrules)
3050         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3051       else if (rid >= solv->systemrules)
3052         {
3053           if (!*sysrp)
3054             *sysrp = rid;
3055         }
3056       else if (rid >= solv->jobrules)
3057         {
3058           if (!*jobrp)
3059             *jobrp = rid;
3060         }
3061       else if (rid >= 0)
3062         {
3063           r = solv->rules + rid;
3064           if (!r->d && r->w2 < 0)
3065             {
3066               if (!*conrp)
3067                 *conrp = rid;
3068             }
3069           else
3070             {
3071               if (!*reqrp)
3072                 *reqrp = rid;
3073             }
3074         }
3075       else
3076         {
3077           /* assertion, counts as require rule */
3078           /* ignore system solvable as we need useful info */
3079           if (rid == -SYSTEMSOLVABLE)
3080             continue;
3081           if (!*reqrp || !reqassert)
3082             {
3083               *reqrp = rid;
3084               reqassert = 1;
3085             }
3086         }
3087     }
3088   if (!*reqrp && lreqr)
3089     *reqrp = lreqr;
3090   if (!*conrp && lconr)
3091     *conrp = lconr;
3092   if (!*jobrp && ljobr)
3093     *jobrp = ljobr;
3094   if (!*sysrp && lsysr)
3095     *sysrp = lsysr;
3096 }
3097
3098 Id
3099 solver_findproblemrule(Solver *solv, Id problem)
3100 {
3101   Id reqr, conr, sysr, jobr;
3102   Id idx = solv->problems.elements[problem - 1];
3103   reqr = conr = sysr = jobr = 0;
3104   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3105   if (reqr)
3106     return reqr;
3107   if (conr)
3108     return conr;
3109   if (sysr)
3110     return sysr;
3111   if (jobr)
3112     return jobr;
3113   abort();
3114 }
3115
3116 void
3117 printprobleminfo(Solver *solv, Queue *job, Id problem)
3118 {
3119   Pool *pool = solv->pool;
3120   Id probr;
3121   Id dep, source, target;
3122   Solvable *s, *s2;
3123
3124   probr = solver_findproblemrule(solv, problem);
3125   switch (solver_problemruleinfo(solv, job, probr, &dep, &source, &target))
3126     {
3127     case SOLVER_PROBLEM_UPDATE_RULE:
3128       s = pool_id2solvable(pool, source);
3129       POOL_DEBUG(SAT_DEBUG_RESULT, "problem with installed package %s\n", solvable2str(pool, s));
3130       return;
3131     case SOLVER_PROBLEM_JOB_RULE:
3132       POOL_DEBUG(SAT_DEBUG_RESULT, "conflicting requests\n");
3133       return;
3134     case SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP:
3135       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides requested %s\n", dep2str(pool, dep));
3136       return;
3137     case SOLVER_PROBLEM_NOT_INSTALLABLE:
3138       s = pool_id2solvable(pool, source);
3139       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s is not installable\n", solvable2str(pool, s));
3140       return;
3141     case SOLVER_PROBLEM_NOTHING_PROVIDES_DEP:
3142       s = pool_id2solvable(pool, source);
3143       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides %s needed by %s\n", dep2str(pool, dep), solvable2str(pool, s));
3144       return;
3145     case SOLVER_PROBLEM_SAME_NAME:
3146       s = pool_id2solvable(pool, source);
3147       s2 = pool_id2solvable(pool, target);
3148       POOL_DEBUG(SAT_DEBUG_RESULT, "cannot install both %s and %s\n", solvable2str(pool, s), solvable2str(pool, s2));
3149       return;
3150     case SOLVER_PROBLEM_PACKAGE_CONFLICT:
3151       s = pool_id2solvable(pool, source);
3152       s2 = pool_id2solvable(pool, target);
3153       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3154       return;
3155     case SOLVER_PROBLEM_PACKAGE_OBSOLETES:
3156       s = pool_id2solvable(pool, source);
3157       s2 = pool_id2solvable(pool, target);
3158       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s obsoletes %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3159       return;
3160     case SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE:
3161       s = pool_id2solvable(pool, source);
3162       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s requires %s, but none of the providers can be installed\n", solvable2str(pool, s), dep2str(pool, dep));
3163       return;
3164     }
3165 }
3166
3167 void
3168 printsolutions(Solver *solv, Queue *job)
3169 {
3170   Pool *pool = solv->pool;
3171   int pcnt;
3172   Id p, rp, what;
3173   Id problem, solution, element;
3174   Solvable *s, *sd;
3175
3176   POOL_DEBUG(SAT_DEBUG_RESULT, "Encountered problems! Here are the solutions:\n\n");
3177   pcnt = 1;
3178   problem = 0;
3179   while ((problem = solver_next_problem(solv, problem)) != 0)
3180     {
3181       POOL_DEBUG(SAT_DEBUG_RESULT, "Problem %d:\n", pcnt++);
3182       POOL_DEBUG(SAT_DEBUG_RESULT, "====================================\n");
3183       printprobleminfo(solv, job, problem);
3184       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3185       solution = 0;
3186       while ((solution = solver_next_solution(solv, problem, solution)) != 0)
3187         {
3188           element = 0;
3189           while ((element = solver_next_solutionelement(solv, problem, solution, element, &p, &rp)) != 0)
3190             {
3191               if (p == 0)
3192                 {
3193                   /* job, rp is index into job queue */
3194                   what = job->elements[rp];
3195                   switch (job->elements[rp - 1])
3196                     {
3197                     case SOLVER_INSTALL_SOLVABLE:
3198                       s = pool->solvables + what;
3199                       if (solv->installed && s->repo == solv->installed)
3200                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not keep %s installed\n", solvable2str(pool, s));
3201                       else
3202                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", solvable2str(pool, s));
3203                       break;
3204                     case SOLVER_ERASE_SOLVABLE:
3205                       s = pool->solvables + what;
3206                       if (solv->installed && s->repo == solv->installed)
3207                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", solvable2str(pool, s));
3208                       else
3209                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not forbid installation of %s\n", solvable2str(pool, s));
3210                       break;
3211                     case SOLVER_INSTALL_SOLVABLE_NAME:
3212                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", id2str(pool, what));
3213                       break;
3214                     case SOLVER_ERASE_SOLVABLE_NAME:
3215                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", id2str(pool, what));
3216                       break;
3217                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3218                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install a solvable providing %s\n", dep2str(pool, what));
3219                       break;
3220                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
3221                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall all solvables providing %s\n", dep2str(pool, what));
3222                       break;
3223                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
3224                       s = pool->solvables + what;
3225                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install most recent version of %s\n", solvable2str(pool, s));
3226                       break;
3227                     default:
3228                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do something different\n");
3229                       break;
3230                     }
3231                 }
3232               else
3233                 {
3234                   /* policy, replace p with rp */
3235                   s = pool->solvables + p;
3236                   sd = rp ? pool->solvables + rp : 0;
3237                   if (sd)
3238                     {
3239                       int gotone = 0;
3240                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr, EVRCMP_MATCH_RELEASE) > 0)
3241                         {
3242                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow downgrade of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3243                           gotone = 1;
3244                         }
3245                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(pool, s, sd))
3246                         {
3247                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow architecture change of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3248                           gotone = 1;
3249                         }
3250                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(pool, s, sd))
3251                         {
3252                           if (sd->vendor)
3253                             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));
3254                           else
3255                             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));
3256                           gotone = 1;
3257                         }
3258                       if (!gotone)
3259                         POOL_DEBUG(SAT_DEBUG_RESULT, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3260                     }
3261                   else
3262                     {
3263                       POOL_DEBUG(SAT_DEBUG_RESULT, "- allow deinstallation of %s\n", solvable2str(pool, s));
3264                     }
3265
3266                 }
3267             }
3268           POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3269         }
3270     }
3271 }
3272
3273
3274 /* for each installed solvable find which packages with *different* names
3275  * obsolete the solvable.
3276  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3277  */
3278
3279 static void
3280 create_obsolete_index(Solver *solv)
3281 {
3282   Pool *pool = solv->pool;
3283   Solvable *s;
3284   Repo *installed = solv->installed;
3285   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3286   int i, n;
3287
3288   if (!installed || !installed->nsolvables)
3289     return;
3290   /* create reverse obsoletes map for installed solvables */
3291   solv->obsoletes = obsoletes = xcalloc(installed->end - installed->start, sizeof(Id));
3292   for (i = 1; i < pool->nsolvables; i++)
3293     {
3294       s = pool->solvables + i;
3295       if (s->repo == installed)
3296         continue;
3297       if (!s->obsoletes)
3298         continue;
3299       if (!pool_installable(pool, s))
3300         continue;
3301       obsp = s->repo->idarraydata + s->obsoletes;
3302       while ((obs = *obsp++) != 0)
3303         FOR_PROVIDES(p, pp, obs)
3304           {
3305             if (pool->solvables[p].repo != installed)
3306               continue;
3307             if (pool->solvables[p].name == s->name)
3308               continue;
3309             obsoletes[p - installed->start]++;
3310           }
3311     }
3312   n = 0;
3313   for (i = 0; i < installed->nsolvables; i++)
3314     if (obsoletes[i])
3315       {
3316         n += obsoletes[i] + 1;
3317         obsoletes[i] = n;
3318       }
3319   solv->obsoletes_data = obsoletes_data = xcalloc(n + 1, sizeof(Id));
3320   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3321   for (i = pool->nsolvables - 1; i > 0; i--)
3322     {
3323       s = pool->solvables + i;
3324       if (s->repo == installed)
3325         continue;
3326       if (!s->obsoletes)
3327         continue;
3328       if (!pool_installable(pool, s))
3329         continue;
3330       obsp = s->repo->idarraydata + s->obsoletes;
3331       while ((obs = *obsp++) != 0)
3332         FOR_PROVIDES(p, pp, obs)
3333           {
3334             if (pool->solvables[p].repo != installed)
3335               continue;
3336             if (pool->solvables[p].name == s->name)
3337               continue;
3338             p -= installed->start;
3339             if (obsoletes_data[obsoletes[p]] != i)
3340               obsoletes_data[--obsoletes[p]] = i;
3341           }
3342     }
3343 }
3344
3345
3346 /*-----------------------------------------------------------------*/
3347 /* main() */
3348
3349 /*
3350  *
3351  * solve job queue
3352  *
3353  */
3354
3355 void
3356 solver_solve(Solver *solv, Queue *job)
3357 {
3358   Pool *pool = solv->pool;
3359   Repo *installed = solv->installed;
3360   int i;
3361   int oldnrules;
3362   Map addedmap;                /* '1' == have rpm-rules for solvable */
3363   Id how, what, p, *pp, d;
3364   Queue q;
3365   Solvable *s;
3366
3367   /* create whatprovides if not already there */
3368   if (!pool->whatprovides)
3369     pool_createwhatprovides(pool);
3370
3371   /* create obsolete index if needed */
3372   if (solv->noupdateprovide)
3373     create_obsolete_index(solv);
3374
3375   /*
3376    * create basic rule set of all involved packages
3377    * use addedmap bitmap to make sure we don't create rules twice
3378    *
3379    */
3380
3381   map_init(&addedmap, pool->nsolvables);
3382   queue_init(&q);
3383
3384   /*
3385    * always install our system solvable
3386    */
3387   MAPSET(&addedmap, SYSTEMSOLVABLE);
3388   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3389   queue_push(&solv->decisionq_why, 0);
3390   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3391
3392   /*
3393    * create rules for all package that could be involved with the solving
3394    * so called: rpm rules
3395    *
3396    */
3397   if (installed)
3398     {
3399       oldnrules = solv->nrules;
3400       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3401       FOR_REPO_SOLVABLES(installed, p, s)
3402         addrpmrulesforsolvable(solv, s, &addedmap);
3403       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3404       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3405       oldnrules = solv->nrules;
3406       FOR_REPO_SOLVABLES(installed, p, s)
3407         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3408       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3409     }
3410
3411   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3412   oldnrules = solv->nrules;
3413   for (i = 0; i < job->count; i += 2)
3414     {
3415       how = job->elements[i];
3416       what = job->elements[i + 1];
3417
3418       switch(how)
3419         {
3420         case SOLVER_INSTALL_SOLVABLE:
3421           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3422           break;
3423         case SOLVER_INSTALL_SOLVABLE_NAME:
3424         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3425           FOR_PROVIDES(p, pp, what)
3426             {
3427               /* if by name, ensure that the name matches */
3428               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3429                 continue;
3430               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3431             }
3432           break;
3433         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3434           /* dont allow downgrade */
3435           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3436           break;
3437         }
3438     }
3439   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3440
3441   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3442
3443   oldnrules = solv->nrules;
3444   addrpmrulesforweak(solv, &addedmap);
3445   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3446
3447   IF_POOLDEBUG (SAT_DEBUG_STATS)
3448     {
3449       int possible = 0, installable = 0;
3450       for (i = 1; i < pool->nsolvables; i++)
3451         {
3452           if (pool_installable(pool, pool->solvables + i))
3453             installable++;
3454           if (MAPTST(&addedmap, i))
3455             possible++;
3456         }
3457       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving (rules has been generated for)\n", possible, installable);
3458     }
3459
3460   /*
3461    * first pass done, we now have all the rpm rules we need.
3462    * unify existing rules before going over all job rules and
3463    * policy rules.
3464    * at this point the system is always solvable,
3465    * as an empty system (remove all packages) is a valid solution
3466    */
3467
3468   unifyrules(solv);     /* remove duplicate rpm rules */
3469
3470   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3471   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3472     printdecisions (solv);
3473
3474   /*
3475    * now add all job rules
3476    */
3477
3478   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3479
3480   solv->jobrules = solv->nrules;
3481
3482   for (i = 0; i < job->count; i += 2)
3483     {
3484       oldnrules = solv->nrules;
3485
3486       how = job->elements[i];
3487       what = job->elements[i + 1];
3488       switch(how)
3489         {
3490         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3491           s = pool->solvables + what;
3492           POOL_DEBUG(SAT_DEBUG_JOB, "job: install solvable %s\n", solvable2str(pool, s));
3493           addrule(solv, what, 0);                       /* install by Id */
3494           queue_push(&solv->ruletojob, i);
3495           break;
3496         case SOLVER_ERASE_SOLVABLE:
3497           s = pool->solvables + what;
3498           POOL_DEBUG(SAT_DEBUG_JOB, "job: erase solvable %s\n", solvable2str(pool, s));
3499           addrule(solv, -what, 0);                      /* remove by Id */
3500           queue_push(&solv->ruletojob, i);
3501           break;
3502         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3503         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3504           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3505             POOL_DEBUG(SAT_DEBUG_JOB, "job: install name %s\n", id2str(pool, what));
3506           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3507             POOL_DEBUG(SAT_DEBUG_JOB, "job: install provides %s\n", dep2str(pool, what));
3508           queue_empty(&q);
3509           FOR_PROVIDES(p, pp, what)
3510             {
3511               /* if by name, ensure that the name matches */
3512               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3513                 continue;
3514               queue_push(&q, p);
3515             }
3516           if (!q.count)
3517             {
3518               /* no provider, make this an impossible rule */
3519               queue_push(&q, -SYSTEMSOLVABLE);
3520             }
3521
3522           p = queue_shift(&q);         /* get first provider */
3523           if (!q.count)
3524             d = 0;                     /* single provider ? -> make assertion */
3525           else
3526             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3527           addrule(solv, p, d);         /* add 'requires' rule */
3528           queue_push(&solv->ruletojob, i);
3529           break;
3530         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3531         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3532           if (how == SOLVER_ERASE_SOLVABLE_NAME)
3533             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase name %s\n", id2str(pool, what));
3534           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3535             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase provides %s\n", dep2str(pool, what));
3536           FOR_PROVIDES(p, pp, what)
3537             {
3538               /* if by name, ensure that the name matches */
3539               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3540                 continue;
3541               addrule(solv, -p, 0);  /* add 'remove' rule */
3542               queue_push(&solv->ruletojob, i);
3543             }
3544           break;
3545         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3546           s = pool->solvables + what;
3547           POOL_DEBUG(SAT_DEBUG_JOB, "job: update %s\n", solvable2str(pool, s));
3548           addupdaterule(solv, s, 0);
3549           queue_push(&solv->ruletojob, i);
3550           break;
3551         }
3552       IF_POOLDEBUG (SAT_DEBUG_JOB)
3553         {
3554           int j;
3555           if (solv->nrules == oldnrules)
3556             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created");
3557           for (j = oldnrules; j < solv->nrules; j++)
3558             {
3559               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3560               printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3561             }
3562         }
3563     }
3564
3565   if (solv->ruletojob.count != solv->nrules - solv->jobrules)
3566     abort();
3567
3568   /*
3569    * now add system rules
3570    *
3571    */
3572
3573   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add system rules ***\n");
3574
3575
3576   solv->systemrules = solv->nrules;
3577
3578   /*
3579    * create rules for updating installed solvables
3580    *
3581    */
3582
3583   if (installed && !solv->allowuninstall)
3584     {                                  /* loop over all installed solvables */
3585       /* we create all update rules, but disable some later on depending on the job */
3586       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3587         if (s->repo == installed)
3588           addupdaterule(solv, s, 0); /* allowall = 0 */
3589         else
3590           addupdaterule(solv, 0, 0);    /* create dummy rule;  allowall = 0  */
3591       /* consistency check: we added a rule for _every_ system solvable */
3592       if (solv->nrules - solv->systemrules != installed->end - installed->start)
3593         abort();
3594     }
3595
3596   /* create special weak system rules */
3597   /* those are used later on to keep a version of the installed packages in
3598      best effort mode */
3599   if (installed && installed->nsolvables)
3600     {
3601       solv->weaksystemrules = xcalloc(installed->end - installed->start, sizeof(Id));
3602       FOR_REPO_SOLVABLES(installed, p, s)
3603         {
3604           policy_findupdatepackages(solv, s, &q, 1);
3605           if (q.count)
3606             solv->weaksystemrules[p - installed->start] = pool_queuetowhatprovides(pool, &q);
3607         }
3608     }
3609
3610   /* free unneeded memory */
3611   map_free(&addedmap);
3612   queue_free(&q);
3613
3614   solv->weakrules = solv->nrules;
3615
3616   /* try real hard to keep packages installed */
3617   if (0)
3618     {
3619       FOR_REPO_SOLVABLES(installed, p, s)
3620         {
3621           /* FIXME: can't work with refine_suggestion! */
3622           /* need to always add the rule but disable it */
3623           if (MAPTST(&solv->noupdate, p - installed->start))
3624             continue;
3625           d = solv->weaksystemrules[p - installed->start];
3626           addrule(solv, p, d);
3627         }
3628     }
3629
3630   /* all new rules are learnt after this point */
3631   solv->learntrules = solv->nrules;
3632
3633   /*
3634    * solve !
3635    *
3636    */
3637
3638   disableupdaterules(solv, job, -1);
3639   makeruledecisions(solv);
3640
3641   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
3642
3643   run_solver(solv, 1, 1);
3644
3645   /* find suggested packages */
3646   if (!solv->problems.count)
3647     {
3648       Id sug, *sugp, p, *pp;
3649
3650       /* create map of all suggests that are still open */
3651       solv->recommends_index = -1;
3652       MAPZERO(&solv->suggestsmap);
3653       for (i = 0; i < solv->decisionq.count; i++)
3654         {
3655           p = solv->decisionq.elements[i];
3656           if (p < 0)
3657             continue;
3658           s = pool->solvables + p;
3659           if (s->suggests)
3660             {
3661               sugp = s->repo->idarraydata + s->suggests;
3662               while ((sug = *sugp++) != 0)
3663                 {
3664                   FOR_PROVIDES(p, pp, sug)
3665                     if (solv->decisionmap[p] > 0)
3666                       break;
3667                   if (p)
3668                     continue;   /* already fulfilled */
3669                   FOR_PROVIDES(p, pp, sug)
3670                     MAPSET(&solv->suggestsmap, p);
3671                 }
3672             }
3673         }
3674       for (i = 1; i < pool->nsolvables; i++)
3675         {
3676           if (solv->decisionmap[i] != 0)
3677             continue;
3678           s = pool->solvables + i;
3679           if (!MAPTST(&solv->suggestsmap, i))
3680             {
3681               if (!s->enhances)
3682                 continue;
3683               if (!pool_installable(pool, s))
3684                 continue;
3685               if (!solver_is_enhancing(solv, s))
3686                 continue;
3687             }
3688           queue_push(&solv->suggestions, i);
3689         }
3690       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3691     }
3692
3693   if (solv->problems.count)
3694     problems_to_solutions(solv, job);
3695 }
3696