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