src/solver.c

   1 /*
   2  * Copyright (c) 2007-2008, 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 "solver_private.h"
  22 #include "bitmap.h"
  23 #include "pool.h"
  24 #include "util.h"
  25 #include "policy.h"
  26 #include "solverdebug.h"
  27
  28 #define RULES_BLOCK 63
  29
  30 /********************************************************************
  31  *
  32  * dependency check helpers
  33  *
  34  */
  35
  36 /*-------------------------------------------------------------------
  37  * handle split provides
  38  *
  39  * a splitprovides dep looks like
  40  *     namespace:splitprovides(pkg REL_WITH path)
  41  * and is only true if pkg is installed and contains the specified path.
  42  * we also make sure that pkg is selected for an update, otherwise the
  43  * update would always be forced onto the user.
  44  */
  45 int
  46 solver_splitprovides(Solver *solv, Id dep)
  47 {
  48   Pool *pool = solv->pool;
  49   Id p, pp;
  50   Reldep *rd;
  51   Solvable *s;
  52
  53   if (!solv->dosplitprovides || !solv->installed || (!solv->updatemap_all && !solv->updatemap.size))
  54     return 0;
  55   if (!ISRELDEP(dep))
  56     return 0;
  57   rd = GETRELDEP(pool, dep);
  58   if (rd->flags != REL_WITH)
  59     return 0;
  60   FOR_PROVIDES(p, pp, dep)
  61     {
  62       /* here we have packages that provide the correct name and contain the path,
  63        * now do extra filtering */
  64       s = pool->solvables + p;
  65       if (s->repo == solv->installed && s->name == rd->name &&
  66           (solv->updatemap_all || (solv->updatemap.size && MAPTST(&solv->updatemap, p - solv->installed->start))))
  67         return 1;
  68     }
  69   return 0;
  70 }
  71
  72
  73 /*-------------------------------------------------------------------
  74  * solver_dep_installed
  75  */
  76
  77 int
  78 solver_dep_installed(Solver *solv, Id dep)
  79 {
  80 #if 0
  81   Pool *pool = solv->pool;
  82   Id p, pp;
  83
  84   if (ISRELDEP(dep))
  85     {
  86       Reldep *rd = GETRELDEP(pool, dep);
  87       if (rd->flags == REL_AND)
  88         {
  89           if (!solver_dep_installed(solv, rd->name))
  90             return 0;
  91           return solver_dep_installed(solv, rd->evr);
  92         }
  93       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  94         return solver_dep_installed(solv, rd->evr);
  95     }
  96   FOR_PROVIDES(p, pp, dep)
  97     {
  98       if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
  99         return 1;
 100     }
 101 #endif
 102   return 0;
 103 }
 104
 105
 106
 107 /************************************************************************/
 108
 109 /*
 110  * make assertion rules into decisions
 111  *
 112  * Go through rules and add direct assertions to the decisionqueue.
 113  * If we find a conflict, disable rules and add them to problem queue.
 114  */
 115
 116 static void
 117 makeruledecisions(Solver *solv)
 118 {
 119   Pool *pool = solv->pool;
 120   int i, ri, ii;
 121   Rule *r, *rr;
 122   Id v, vv;
 123   int decisionstart;
 124   int record_proof = 1;
 125
 126   /* The system solvable is always installed first */
 127   assert(solv->decisionq.count == 0);
 128   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
 129   queue_push(&solv->decisionq_why, 0);
 130   solv->decisionmap[SYSTEMSOLVABLE] = 1;        /* installed at level '1' */
 131
 132   decisionstart = solv->decisionq.count;
 133   for (ii = 0; ii < solv->ruleassertions.count; ii++)
 134     {
 135       ri = solv->ruleassertions.elements[ii];
 136       r = solv->rules + ri;
 137
 138       if (r->d < 0 || !r->p || r->w2)   /* disabled, dummy or no assertion */
 139         continue;
 140       /* do weak rules in phase 2 */
 141       if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri))
 142         continue;
 143
 144       v = r->p;
 145       vv = v > 0 ? v : -v;
 146
 147       if (!solv->decisionmap[vv])          /* if not yet decided */
 148         {
 149             /*
 150              * decide !
 151              */
 152           queue_push(&solv->decisionq, v);
 153           queue_push(&solv->decisionq_why, r - solv->rules);
 154           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 155           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 156             {
 157               Solvable *s = solv->pool->solvables + vv;
 158               if (v < 0)
 159                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", pool_solvable2str(solv->pool, s));
 160               else
 161                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "installing  %s (assertion)\n", pool_solvable2str(solv->pool, s));
 162             }
 163           continue;
 164         }
 165         /*
 166          * check previous decision: is it sane ?
 167          */
 168
 169       if (v > 0 && solv->decisionmap[vv] > 0)    /* ok to install */
 170         continue;
 171       if (v < 0 && solv->decisionmap[vv] < 0)    /* ok to remove */
 172         continue;
 173
 174         /*
 175          * found a conflict!
 176          *
 177          * The rule (r) we're currently processing says something
 178          * different (v = r->p) than a previous decision (decisionmap[abs(v)])
 179          * on this literal
 180          */
 181
 182       if (ri >= solv->learntrules)
 183         {
 184           /* conflict with a learnt rule */
 185           /* can happen when packages cannot be installed for
 186            * multiple reasons. */
 187           /* we disable the learnt rule in this case */
 188           solver_disablerule(solv, r);
 189           continue;
 190         }
 191
 192         /*
 193          * find the decision which is the "opposite" of the rule
 194          */
 195
 196       for (i = 0; i < solv->decisionq.count; i++)
 197         if (solv->decisionq.elements[i] == -v)
 198           break;
 199       assert(i < solv->decisionq.count);         /* assert that we found it */
 200
 201       /*
 202        * conflict with system solvable ?
 203        */
 204
 205       if (v == -SYSTEMSOLVABLE)
 206         {
 207           /* conflict with system solvable */
 208           if (record_proof)
 209             {
 210               queue_push(&solv->problems, solv->learnt_pool.count);
 211               queue_push(&solv->learnt_pool, ri);
 212               queue_push(&solv->learnt_pool, 0);
 213             }
 214           else
 215             queue_push(&solv->problems, 0);
 216           POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri);
 217           if  (ri >= solv->jobrules && ri < solv->jobrules_end)
 218             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 219           else
 220             v = ri;
 221           queue_push(&solv->problems, v);
 222           queue_push(&solv->problems, 0);
 223           solver_disableproblem(solv, v);
 224           continue;
 225         }
 226
 227       assert(solv->decisionq_why.elements[i] > 0);
 228
 229       /*
 230        * conflict with an rpm rule ?
 231        */
 232
 233       if (solv->decisionq_why.elements[i] < solv->rpmrules_end)
 234         {
 235           /* conflict with rpm rule assertion */
 236           if (record_proof)
 237             {
 238               queue_push(&solv->problems, solv->learnt_pool.count);
 239               queue_push(&solv->learnt_pool, ri);
 240               queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
 241               queue_push(&solv->learnt_pool, 0);
 242             }
 243           else
 244             queue_push(&solv->problems, 0);
 245           assert(v > 0 || v == -SYSTEMSOLVABLE);
 246           POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri);
 247           if (ri >= solv->jobrules && ri < solv->jobrules_end)
 248             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 249           else
 250             v = ri;
 251           queue_push(&solv->problems, v);
 252           queue_push(&solv->problems, 0);
 253           solver_disableproblem(solv, v);
 254           continue;
 255         }
 256
 257       /*
 258        * conflict with another job or update/feature rule
 259        */
 260
 261       /* record proof */
 262       if (record_proof)
 263         {
 264           queue_push(&solv->problems, solv->learnt_pool.count);
 265           queue_push(&solv->learnt_pool, ri);
 266           queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
 267           queue_push(&solv->learnt_pool, 0);
 268         }
 269       else
 270         queue_push(&solv->problems, 0);
 271
 272       POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv);
 273
 274         /*
 275          * push all of our rules (can only be feature or job rules)
 276          * asserting this literal on the problem stack
 277          */
 278
 279       for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++)
 280         {
 281           if (rr->d < 0                          /* disabled */
 282               || rr->w2)                         /*  or no assertion */
 283             continue;
 284           if (rr->p != vv                        /* not affecting the literal */
 285               && rr->p != -vv)
 286             continue;
 287           if (MAPTST(&solv->weakrulemap, i))     /* weak: silently ignore */
 288             continue;
 289
 290           POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
 291
 292           solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + i);
 293
 294           v = i;
 295             /* is is a job rule ? */
 296           if (i >= solv->jobrules && i < solv->jobrules_end)
 297             v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
 298
 299           queue_push(&solv->problems, v);
 300           solver_disableproblem(solv, v);
 301         }
 302       queue_push(&solv->problems, 0);
 303
 304       /*
 305        * start over
 306        * (back up from decisions)
 307        */
 308       while (solv->decisionq.count > decisionstart)
 309         {
 310           v = solv->decisionq.elements[--solv->decisionq.count];
 311           --solv->decisionq_why.count;
 312           vv = v > 0 ? v : -v;
 313           solv->decisionmap[vv] = 0;
 314         }
 315       ii = -1; /* restarts loop at 0 */
 316     }
 317
 318   /*
 319    * phase 2: now do the weak assertions
 320    */
 321   for (ii = 0; ii < solv->ruleassertions.count; ii++)
 322     {
 323       ri = solv->ruleassertions.elements[ii];
 324       r = solv->rules + ri;
 325       if (r->d < 0 || r->w2)                     /* disabled or no assertion */
 326         continue;
 327       if (ri >= solv->learntrules || !MAPTST(&solv->weakrulemap, ri))       /* skip non-weak */
 328         continue;
 329       v = r->p;
 330       vv = v > 0 ? v : -v;
 331       /*
 332        * decide !
 333        * (if not yet decided)
 334        */
 335       if (!solv->decisionmap[vv])
 336         {
 337           queue_push(&solv->decisionq, v);
 338           queue_push(&solv->decisionq_why, r - solv->rules);
 339           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 340           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 341             {
 342               Solvable *s = solv->pool->solvables + vv;
 343               if (v < 0)
 344                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", pool_solvable2str(solv->pool, s));
 345               else
 346                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "installing  %s (weak assertion)\n", pool_solvable2str(solv->pool, s));
 347             }
 348           continue;
 349         }
 350       /*
 351        * previously decided, sane ?
 352        */
 353       if (v > 0 && solv->decisionmap[vv] > 0)
 354         continue;
 355       if (v < 0 && solv->decisionmap[vv] < 0)
 356         continue;
 357
 358       POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling ");
 359       solver_printrule(solv, SOLV_DEBUG_UNSOLVABLE, r);
 360
 361       if (ri >= solv->jobrules && ri < solv->jobrules_end)
 362         v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 363       else
 364         v = ri;
 365       solver_disableproblem(solv, v);
 366       if (v < 0)
 367         solver_reenablepolicyrules(solv, -v);
 368     }
 369 }
 370
 371
 372 /*-------------------------------------------------------------------
 373  * enable/disable learnt rules
 374  *
 375  * we have enabled or disabled some of our rules. We now reenable all
 376  * of our learnt rules except the ones that were learnt from rules that
 377  * are now disabled.
 378  */
 379 static void
 380 enabledisablelearntrules(Solver *solv)
 381 {
 382   Pool *pool = solv->pool;
 383   Rule *r;
 384   Id why, *whyp;
 385   int i;
 386
 387   POOL_DEBUG(SOLV_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n");
 388   for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
 389     {
 390       whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
 391       while ((why = *whyp++) != 0)
 392         {
 393           assert(why > 0 && why < i);
 394           if (solv->rules[why].d < 0)
 395             break;
 396         }
 397       /* why != 0: we found a disabled rule, disable the learnt rule */
 398       if (why && r->d >= 0)
 399         {
 400           IF_POOLDEBUG (SOLV_DEBUG_SOLUTIONS)
 401             {
 402               POOL_DEBUG(SOLV_DEBUG_SOLUTIONS, "disabling ");
 403               solver_printruleclass(solv, SOLV_DEBUG_SOLUTIONS, r);
 404             }
 405           solver_disablerule(solv, r);
 406         }
 407       else if (!why && r->d < 0)
 408         {
 409           IF_POOLDEBUG (SOLV_DEBUG_SOLUTIONS)
 410             {
 411               POOL_DEBUG(SOLV_DEBUG_SOLUTIONS, "re-enabling ");
 412               solver_printruleclass(solv, SOLV_DEBUG_SOLUTIONS, r);
 413             }
 414           solver_enablerule(solv, r);
 415         }
 416     }
 417 }
 418
 419
 420 /********************************************************************/
 421 /* watches */
 422
 423
 424 /*-------------------------------------------------------------------
 425  * makewatches
 426  *
 427  * initial setup for all watches
 428  */
 429
 430 static void
 431 makewatches(Solver *solv)
 432 {
 433   Rule *r;
 434   int i;
 435   int nsolvables = solv->pool->nsolvables;
 436
 437   solv_free(solv->watches);
 438                                        /* lower half for removals, upper half for installs */
 439   solv->watches = solv_calloc(2 * nsolvables, sizeof(Id));
 440 #if 1
 441   /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */
 442   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
 443 #else
 444   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
 445 #endif
 446     {
 447       if (!r->w2)               /* assertions do not need watches */
 448         continue;
 449
 450       /* see addwatches_rule(solv, r) */
 451       r->n1 = solv->watches[nsolvables + r->w1];
 452       solv->watches[nsolvables + r->w1] = r - solv->rules;
 453
 454       r->n2 = solv->watches[nsolvables + r->w2];
 455       solv->watches[nsolvables + r->w2] = r - solv->rules;
 456     }
 457 }
 458
 459
 460 /*-------------------------------------------------------------------
 461  *
 462  * add watches (for a new learned rule)
 463  * sets up watches for a single rule
 464  *
 465  * see also makewatches() above.
 466  */
 467
 468 static inline void
 469 addwatches_rule(Solver *solv, Rule *r)
 470 {
 471   int nsolvables = solv->pool->nsolvables;
 472
 473   r->n1 = solv->watches[nsolvables + r->w1];
 474   solv->watches[nsolvables + r->w1] = r - solv->rules;
 475
 476   r->n2 = solv->watches[nsolvables + r->w2];
 477   solv->watches[nsolvables + r->w2] = r - solv->rules;
 478 }
 479
 480
 481 /********************************************************************/
 482 /*
 483  * rule propagation
 484  */
 485
 486
 487 /* shortcuts to check if a literal (positive or negative) assignment
 488  * evaluates to 'true' or 'false'
 489  */
 490 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
 491 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
 492 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0)
 493
 494 /*-------------------------------------------------------------------
 495  *
 496  * propagate
 497  *
 498  * make decision and propagate to all rules
 499  *
 500  * Evaluate each term affected by the decision (linked through watches)
 501  * If we find unit rules we make new decisions based on them
 502  *
 503  * Everything's fixed there, it's just finding rules that are
 504  * unit.
 505  *
 506  * return : 0 = everything is OK
 507  *          rule = conflict found in this rule
 508  */
 509
 510 static Rule *
 511 propagate(Solver *solv, int level)
 512 {
 513   Pool *pool = solv->pool;
 514   Id *rp, *next_rp;           /* rule pointer, next rule pointer in linked list */
 515   Rule *r;                    /* rule */
 516   Id p, pkg, other_watch;
 517   Id *dp;
 518   Id *decisionmap = solv->decisionmap;
 519
 520   Id *watches = solv->watches + pool->nsolvables;   /* place ptr in middle */
 521
 522   POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "----- propagate -----\n");
 523
 524   /* foreach non-propagated decision */
 525   while (solv->propagate_index < solv->decisionq.count)
 526     {
 527         /*
 528          * 'pkg' was just decided
 529          * negate because our watches trigger if literal goes FALSE
 530          */
 531       pkg = -solv->decisionq.elements[solv->propagate_index++];
 532
 533       IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 534         {
 535           POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
 536           solver_printruleelement(solv, SOLV_DEBUG_PROPAGATE, 0, -pkg);
 537         }
 538
 539       /* foreach rule where 'pkg' is now FALSE */
 540       for (rp = watches + pkg; *rp; rp = next_rp)
 541         {
 542           r = solv->rules + *rp;
 543           if (r->d < 0)
 544             {
 545               /* rule is disabled, goto next */
 546               if (pkg == r->w1)
 547                 next_rp = &r->n1;
 548               else
 549                 next_rp = &r->n2;
 550               continue;
 551             }
 552
 553           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 554             {
 555               POOL_DEBUG(SOLV_DEBUG_PROPAGATE,"  watch triggered ");
 556               solver_printrule(solv, SOLV_DEBUG_PROPAGATE, r);
 557             }
 558
 559             /* 'pkg' was just decided (was set to FALSE)
 560              *
 561              *  now find other literal watch, check clause
 562              *   and advance on linked list
 563              */
 564           if (pkg == r->w1)
 565             {
 566               other_watch = r->w2;
 567               next_rp = &r->n1;
 568             }
 569           else
 570             {
 571               other_watch = r->w1;
 572               next_rp = &r->n2;
 573             }
 574
 575             /*
 576              * This term is already true (through the other literal)
 577              * so we have nothing to do
 578              */
 579           if (DECISIONMAP_TRUE(other_watch))
 580             continue;
 581
 582             /*
 583              * The other literal is FALSE or UNDEF
 584              *
 585              */
 586
 587           if (r->d)
 588             {
 589               /* Not a binary clause, try to move our watch.
 590                *
 591                * Go over all literals and find one that is
 592                *   not other_watch
 593                *   and not FALSE
 594                *
 595                * (TRUE is also ok, in that case the rule is fulfilled)
 596                */
 597               if (r->p                                /* we have a 'p' */
 598                   && r->p != other_watch              /* which is not watched */
 599                   && !DECISIONMAP_FALSE(r->p))        /* and not FALSE */
 600                 {
 601                   p = r->p;
 602                 }
 603               else                                    /* go find a 'd' to make 'true' */
 604                 {
 605                   /* foreach p in 'd'
 606                      we just iterate sequentially, doing it in another order just changes the order of decisions, not the decisions itself
 607                    */
 608                   for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
 609                     {
 610                       if (p != other_watch              /* which is not watched */
 611                           && !DECISIONMAP_FALSE(p))     /* and not FALSE */
 612                         break;
 613                     }
 614                 }
 615
 616               if (p)
 617                 {
 618                   /*
 619                    * if we found some p that is UNDEF or TRUE, move
 620                    * watch to it
 621                    */
 622                   IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 623                     {
 624                       if (p > 0)
 625                         POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), pool_solvid2str(pool, p));
 626                       else
 627                         POOL_DEBUG(SOLV_DEBUG_PROPAGATE,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), pool_solvid2str(pool, -p));
 628                     }
 629
 630                   *rp = *next_rp;
 631                   next_rp = rp;
 632
 633                   if (pkg == r->w1)
 634                     {
 635                       r->w1 = p;
 636                       r->n1 = watches[p];
 637                     }
 638                   else
 639                     {
 640                       r->w2 = p;
 641                       r->n2 = watches[p];
 642                     }
 643                   watches[p] = r - solv->rules;
 644                   continue;
 645                 }
 646               /* search failed, thus all unwatched literals are FALSE */
 647
 648             } /* not binary */
 649
 650             /*
 651              * unit clause found, set literal other_watch to TRUE
 652              */
 653
 654           if (DECISIONMAP_FALSE(other_watch))      /* check if literal is FALSE */
 655             return r;                              /* eek, a conflict! */
 656
 657           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 658             {
 659               POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "   unit ");
 660               solver_printrule(solv, SOLV_DEBUG_PROPAGATE, r);
 661             }
 662
 663           if (other_watch > 0)
 664             decisionmap[other_watch] = level;    /* install! */
 665           else
 666             decisionmap[-other_watch] = -level;  /* remove! */
 667
 668           queue_push(&solv->decisionq, other_watch);
 669           queue_push(&solv->decisionq_why, r - solv->rules);
 670
 671           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
 672             {
 673               if (other_watch > 0)
 674                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "    -> decided to install %s\n", pool_solvid2str(pool, other_watch));
 675               else
 676                 POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "    -> decided to conflict %s\n", pool_solvid2str(pool, -other_watch));
 677             }
 678
 679         } /* foreach rule involving 'pkg' */
 680
 681     } /* while we have non-decided decisions */
 682
 683   POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "----- propagate end-----\n");
 684
 685   return 0;     /* all is well */
 686 }
 687
 688
 689 /********************************************************************/
 690 /* Analysis */
 691
 692 /*-------------------------------------------------------------------
 693  *
 694  * analyze
 695  *   and learn
 696  */
 697
 698 static int
 699 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
 700 {
 701   Pool *pool = solv->pool;
 702   Queue r;
 703   Id r_buf[4];
 704   int rlevel = 1;
 705   Map seen;             /* global? */
 706   Id d, v, vv, *dp, why;
 707   int l, i, idx;
 708   int num = 0, l1num = 0;
 709   int learnt_why = solv->learnt_pool.count;
 710   Id *decisionmap = solv->decisionmap;
 711
 712   queue_init_buffer(&r, r_buf, sizeof(r_buf)/sizeof(*r_buf));
 713
 714   POOL_DEBUG(SOLV_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
 715   map_init(&seen, pool->nsolvables);
 716   idx = solv->decisionq.count;
 717   for (;;)
 718     {
 719       IF_POOLDEBUG (SOLV_DEBUG_ANALYZE)
 720         solver_printruleclass(solv, SOLV_DEBUG_ANALYZE, c);
 721       queue_push(&solv->learnt_pool, c - solv->rules);
 722       d = c->d < 0 ? -c->d - 1 : c->d;
 723       dp = d ? pool->whatprovidesdata + d : 0;
 724       /* go through all literals of the rule */
 725       for (i = -1; ; i++)
 726         {
 727           if (i == -1)
 728             v = c->p;
 729           else if (d == 0)
 730             v = i ? 0 : c->w2;
 731           else
 732             v = *dp++;
 733           if (v == 0)
 734             break;
 735
 736           if (DECISIONMAP_TRUE(v))      /* the one true literal */
 737             continue;
 738           vv = v > 0 ? v : -v;
 739           if (MAPTST(&seen, vv))
 740             continue;
 741           l = solv->decisionmap[vv];
 742           if (l < 0)
 743             l = -l;
 744           MAPSET(&seen, vv);            /* mark that we also need to look at this literal */
 745           if (l == 1)
 746             l1num++;                    /* need to do this one in level1 pass */
 747           else if (l == level)
 748             num++;                      /* need to do this one as well */
 749           else
 750             {
 751               queue_push(&r, v);        /* not level1 or conflict level, add to new rule */
 752               if (l > rlevel)
 753                 rlevel = l;
 754             }
 755         }
 756 l1retry:
 757       if (!num && !--l1num)
 758         break;  /* all level 1 literals done */
 759
 760       /* find the next literal to investigate */
 761       /* (as num + l1num > 0, we know that we'll always find one) */
 762       for (;;)
 763         {
 764           assert(idx > 0);
 765           v = solv->decisionq.elements[--idx];
 766           vv = v > 0 ? v : -v;
 767           if (MAPTST(&seen, vv))
 768             break;
 769         }
 770       MAPCLR(&seen, vv);
 771
 772       if (num && --num == 0)
 773         {
 774           *pr = -v;     /* so that v doesn't get lost */
 775           if (!l1num)
 776             break;
 777           POOL_DEBUG(SOLV_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
 778           /* clear non-l1 bits from seen map */
 779           for (i = 0; i < r.count; i++)
 780             {
 781               v = r.elements[i];
 782               MAPCLR(&seen, v > 0 ? v : -v);
 783             }
 784           /* only level 1 marks left in seen map */
 785           l1num++;      /* as l1retry decrements it */
 786           goto l1retry;
 787         }
 788
 789       why = solv->decisionq_why.elements[idx];
 790       if (why <= 0)     /* just in case, maybe for SYSTEMSOLVABLE */
 791         goto l1retry;
 792       c = solv->rules + why;
 793     }
 794   map_free(&seen);
 795
 796   if (r.count == 0)
 797     *dr = 0;
 798   else if (r.count == 1 && r.elements[0] < 0)
 799     *dr = r.elements[0];
 800   else
 801     *dr = pool_queuetowhatprovides(pool, &r);
 802   IF_POOLDEBUG (SOLV_DEBUG_ANALYZE)
 803     {
 804       POOL_DEBUG(SOLV_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
 805       solver_printruleelement(solv, SOLV_DEBUG_ANALYZE, 0, *pr);
 806       for (i = 0; i < r.count; i++)
 807         solver_printruleelement(solv, SOLV_DEBUG_ANALYZE, 0, r.elements[i]);
 808     }
 809   /* push end marker on learnt reasons stack */
 810   queue_push(&solv->learnt_pool, 0);
 811   if (whyp)
 812     *whyp = learnt_why;
 813   queue_free(&r);
 814   solv->stats_learned++;
 815   return rlevel;
 816 }
 817
 818
 819 /*-------------------------------------------------------------------
 820  *
 821  * solver_reset
 822  *
 823  * reset the solver decisions to right after the rpm rules.
 824  * called after rules have been enabled/disabled
 825  */
 826
 827 void
 828 solver_reset(Solver *solv)
 829 {
 830   Pool *pool = solv->pool;
 831   int i;
 832   Id v;
 833
 834   /* rewind all decisions */
 835   for (i = solv->decisionq.count - 1; i >= 0; i--)
 836     {
 837       v = solv->decisionq.elements[i];
 838       solv->decisionmap[v > 0 ? v : -v] = 0;
 839     }
 840   solv->decisionq_why.count = 0;
 841   solv->decisionq.count = 0;
 842   solv->recommends_index = -1;
 843   solv->propagate_index = 0;
 844   solv->branches.count = 0;
 845
 846   /* adapt learnt rule status to new set of enabled/disabled rules */
 847   enabledisablelearntrules(solv);
 848
 849   /* redo all assertion rule decisions */
 850   makeruledecisions(solv);
 851   POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
 852 }
 853
 854
 855 /*-------------------------------------------------------------------
 856  *
 857  * analyze_unsolvable_rule
 858  */
 859
 860 static void
 861 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp, Map *rseen)
 862 {
 863   Pool *pool = solv->pool;
 864   int i;
 865   Id why = r - solv->rules;
 866
 867   IF_POOLDEBUG (SOLV_DEBUG_UNSOLVABLE)
 868     solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, r);
 869   if (solv->learntrules && why >= solv->learntrules)
 870     {
 871       if (MAPTST(rseen, why - solv->learntrules))
 872         return;
 873       MAPSET(rseen, why - solv->learntrules);
 874       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
 875         if (solv->learnt_pool.elements[i] > 0)
 876           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp, rseen);
 877       return;
 878     }
 879   if (MAPTST(&solv->weakrulemap, why))
 880     if (!*lastweakp || why > *lastweakp)
 881       *lastweakp = why;
 882   /* do not add rpm rules to problem */
 883   if (why < solv->rpmrules_end)
 884     return;
 885   /* turn rule into problem */
 886   if (why >= solv->jobrules && why < solv->jobrules_end)
 887     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
 888   /* normalize dup/infarch rules */
 889   if (why > solv->infarchrules && why < solv->infarchrules_end)
 890     {
 891       Id name = pool->solvables[-solv->rules[why].p].name;
 892       while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name)
 893         why--;
 894     }
 895   if (why > solv->duprules && why < solv->duprules_end)
 896     {
 897       Id name = pool->solvables[-solv->rules[why].p].name;
 898       while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name)
 899         why--;
 900     }
 901
 902   /* return if problem already countains our rule */
 903   if (solv->problems.count)
 904     {
 905       for (i = solv->problems.count - 1; i >= 0; i--)
 906         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
 907           break;
 908         else if (solv->problems.elements[i] == why)
 909           return;
 910     }
 911   queue_push(&solv->problems, why);
 912 }
 913
 914
 915 /*-------------------------------------------------------------------
 916  *
 917  * analyze_unsolvable
 918  *
 919  * return: 1 - disabled some rules, try again
 920  *         0 - hopeless
 921  */
 922
 923 static int
 924 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
 925 {
 926   Pool *pool = solv->pool;
 927   Rule *r;
 928   Map seen;             /* global to speed things up? */
 929   Map rseen;
 930   Id d, v, vv, *dp, why;
 931   int l, i, idx;
 932   Id *decisionmap = solv->decisionmap;
 933   int oldproblemcount;
 934   int oldlearntpoolcount;
 935   Id lastweak;
 936   int record_proof = 1;
 937
 938   POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
 939   solv->stats_unsolvable++;
 940   oldproblemcount = solv->problems.count;
 941   oldlearntpoolcount = solv->learnt_pool.count;
 942
 943   /* make room for proof index */
 944   /* must update it later, as analyze_unsolvable_rule would confuse
 945    * it with a rule index if we put the real value in already */
 946   queue_push(&solv->problems, 0);
 947
 948   r = cr;
 949   map_init(&seen, pool->nsolvables);
 950   map_init(&rseen, solv->learntrules ? solv->nrules - solv->learntrules : 0);
 951   if (record_proof)
 952     queue_push(&solv->learnt_pool, r - solv->rules);
 953   lastweak = 0;
 954   analyze_unsolvable_rule(solv, r, &lastweak, &rseen);
 955   d = r->d < 0 ? -r->d - 1 : r->d;
 956   dp = d ? pool->whatprovidesdata + d : 0;
 957   for (i = -1; ; i++)
 958     {
 959       if (i == -1)
 960         v = r->p;
 961       else if (d == 0)
 962         v = i ? 0 : r->w2;
 963       else
 964         v = *dp++;
 965       if (v == 0)
 966         break;
 967       if (DECISIONMAP_TRUE(v))  /* the one true literal */
 968           continue;
 969       vv = v > 0 ? v : -v;
 970       l = solv->decisionmap[vv];
 971       if (l < 0)
 972         l = -l;
 973       MAPSET(&seen, vv);
 974     }
 975   idx = solv->decisionq.count;
 976   while (idx > 0)
 977     {
 978       v = solv->decisionq.elements[--idx];
 979       vv = v > 0 ? v : -v;
 980       if (!MAPTST(&seen, vv))
 981         continue;
 982       why = solv->decisionq_why.elements[idx];
 983       assert(why > 0);
 984       if (record_proof)
 985         queue_push(&solv->learnt_pool, why);
 986       r = solv->rules + why;
 987       analyze_unsolvable_rule(solv, r, &lastweak, &rseen);
 988       d = r->d < 0 ? -r->d - 1 : r->d;
 989       dp = d ? pool->whatprovidesdata + d : 0;
 990       for (i = -1; ; i++)
 991         {
 992           if (i == -1)
 993             v = r->p;
 994           else if (d == 0)
 995             v = i ? 0 : r->w2;
 996           else
 997             v = *dp++;
 998           if (v == 0)
 999             break;
1000           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1001               continue;
1002           vv = v > 0 ? v : -v;
1003           l = solv->decisionmap[vv];
1004           if (l < 0)
1005             l = -l;
1006           MAPSET(&seen, vv);
1007         }
1008     }
1009   map_free(&seen);
1010   map_free(&rseen);
1011   queue_push(&solv->problems, 0);       /* mark end of this problem */
1012
1013   if (lastweak)
1014     {
1015       Id v;
1016       /* disable last weak rule */
1017       solv->problems.count = oldproblemcount;
1018       solv->learnt_pool.count = oldlearntpoolcount;
1019       if (lastweak >= solv->jobrules && lastweak < solv->jobrules_end)
1020         v = -(solv->ruletojob.elements[lastweak - solv->jobrules] + 1);
1021       else
1022         v = lastweak;
1023       POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "disabling ");
1024       solver_printruleclass(solv, SOLV_DEBUG_UNSOLVABLE, solv->rules + lastweak);
1025       if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end)
1026         solver_disablechoicerules(solv, solv->rules + lastweak);
1027       solver_disableproblem(solv, v);
1028       if (v < 0)
1029         solver_reenablepolicyrules(solv, -v);
1030       solver_reset(solv);
1031       return 1;
1032     }
1033
1034   /* finish proof */
1035   if (record_proof)
1036     {
1037       queue_push(&solv->learnt_pool, 0);
1038       solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1039     }
1040
1041   if (disablerules)
1042     {
1043       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1044         solver_disableproblem(solv, solv->problems.elements[i]);
1045       /* XXX: might want to enable all weak rules again */
1046       solver_reset(solv);
1047       return 1;
1048     }
1049   POOL_DEBUG(SOLV_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1050   return 0;
1051 }
1052
1053
1054 /********************************************************************/
1055 /* Decision revert */
1056
1057 /*-------------------------------------------------------------------
1058  *
1059  * revert
1060  * revert decisionq to a level
1061  */
1062
1063 static void
1064 revert(Solver *solv, int level)
1065 {
1066   Pool *pool = solv->pool;
1067   Id v, vv;
1068   while (solv->decisionq.count)
1069     {
1070       v = solv->decisionq.elements[solv->decisionq.count - 1];
1071       vv = v > 0 ? v : -v;
1072       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1073         break;
1074       POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1075       solv->decisionmap[vv] = 0;
1076       solv->decisionq.count--;
1077       solv->decisionq_why.count--;
1078       solv->propagate_index = solv->decisionq.count;
1079     }
1080   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1081     {
1082       solv->branches.count--;
1083       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1084         solv->branches.count--;
1085     }
1086   solv->recommends_index = -1;
1087 }
1088
1089
1090 /*-------------------------------------------------------------------
1091  *
1092  * watch2onhighest - put watch2 on literal with highest level
1093  */
1094
1095 static inline void
1096 watch2onhighest(Solver *solv, Rule *r)
1097 {
1098   int l, wl = 0;
1099   Id d, v, *dp;
1100
1101   d = r->d < 0 ? -r->d - 1 : r->d;
1102   if (!d)
1103     return;     /* binary rule, both watches are set */
1104   dp = solv->pool->whatprovidesdata + d;
1105   while ((v = *dp++) != 0)
1106     {
1107       l = solv->decisionmap[v < 0 ? -v : v];
1108       if (l < 0)
1109         l = -l;
1110       if (l > wl)
1111         {
1112           r->w2 = dp[-1];
1113           wl = l;
1114         }
1115     }
1116 }
1117
1118
1119 /*-------------------------------------------------------------------
1120  *
1121  * setpropagatelearn
1122  *
1123  * add free decision (solvable to install) to decisionq
1124  * increase level and propagate decision
1125  * return if no conflict.
1126  *
1127  * in conflict case, analyze conflict rule, add resulting
1128  * rule to learnt rule set, make decision from learnt
1129  * rule (always unit) and re-propagate.
1130  *
1131  * returns the new solver level or 0 if unsolvable
1132  *
1133  */
1134
1135 static int
1136 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules, Id ruleid)
1137 {
1138   Pool *pool = solv->pool;
1139   Rule *r;
1140   Id p = 0, d = 0;
1141   int l, why;
1142
1143   assert(ruleid >= 0);
1144   if (decision)
1145     {
1146       level++;
1147       if (decision > 0)
1148         solv->decisionmap[decision] = level;
1149       else
1150         solv->decisionmap[-decision] = -level;
1151       queue_push(&solv->decisionq, decision);
1152       queue_push(&solv->decisionq_why, -ruleid);        /* <= 0 -> free decision */
1153     }
1154   for (;;)
1155     {
1156       r = propagate(solv, level);
1157       if (!r)
1158         break;
1159       if (level == 1)
1160         return analyze_unsolvable(solv, r, disablerules);
1161       POOL_DEBUG(SOLV_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
1162       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1163       assert(l > 0 && l < level);
1164       POOL_DEBUG(SOLV_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
1165       level = l;
1166       revert(solv, level);
1167       r = solver_addrule(solv, p, d);
1168       assert(r);
1169       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
1170       queue_push(&solv->learnt_why, why);
1171       if (d)
1172         {
1173           /* at least 2 literals, needs watches */
1174           watch2onhighest(solv, r);
1175           addwatches_rule(solv, r);
1176         }
1177       else
1178         {
1179           /* learnt rule is an assertion */
1180           queue_push(&solv->ruleassertions, r - solv->rules);
1181         }
1182       /* the new rule is unit by design */
1183       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1184       queue_push(&solv->decisionq, p);
1185       queue_push(&solv->decisionq_why, r - solv->rules);
1186       IF_POOLDEBUG (SOLV_DEBUG_ANALYZE)
1187         {
1188           POOL_DEBUG(SOLV_DEBUG_ANALYZE, "decision: ");
1189           solver_printruleelement(solv, SOLV_DEBUG_ANALYZE, 0, p);
1190           POOL_DEBUG(SOLV_DEBUG_ANALYZE, "new rule: ");
1191           solver_printrule(solv, SOLV_DEBUG_ANALYZE, r);
1192         }
1193     }
1194   return level;
1195 }
1196
1197
1198 /*-------------------------------------------------------------------
1199  *
1200  * select and install
1201  *
1202  * install best package from the queue. We add an extra package, inst, if
1203  * provided. See comment in weak install section.
1204  *
1205  * returns the new solver level or 0 if unsolvable
1206  *
1207  */
1208
1209 static int
1210 selectandinstall(Solver *solv, int level, Queue *dq, int disablerules, Id ruleid)
1211 {
1212   Pool *pool = solv->pool;
1213   Id p;
1214   int i;
1215
1216   if (dq->count > 1)
1217     policy_filter_unwanted(solv, dq, POLICY_MODE_CHOOSE);
1218   if (dq->count > 1)
1219     {
1220       /* XXX: didn't we already do that? */
1221       /* XXX: shouldn't we prefer installed packages? */
1222       /* XXX: move to policy.c? */
1223       /* choose the supplemented one */
1224       for (i = 0; i < dq->count; i++)
1225         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1226           {
1227             dq->elements[0] = dq->elements[i];
1228             dq->count = 1;
1229             break;
1230           }
1231     }
1232   if (dq->count > 1)
1233     {
1234       /* multiple candidates, open a branch */
1235       for (i = 1; i < dq->count; i++)
1236         queue_push(&solv->branches, dq->elements[i]);
1237       queue_push(&solv->branches, -level);
1238     }
1239   p = dq->elements[0];
1240
1241   POOL_DEBUG(SOLV_DEBUG_POLICY, "installing %s\n", pool_solvid2str(pool, p));
1242
1243   return setpropagatelearn(solv, level, p, disablerules, ruleid);
1244 }
1245
1246
1247 /********************************************************************/
1248 /* Main solver interface */
1249
1250
1251 /*-------------------------------------------------------------------
1252  *
1253  * solver_create
1254  * create solver structure
1255  *
1256  * pool: all available solvables
1257  * installed: installed Solvables
1258  *
1259  *
1260  * Upon solving, rules are created to flag the Solvables
1261  * of the 'installed' Repo as installed.
1262  */
1263
1264 Solver *
1265 solver_create(Pool *pool)
1266 {
1267   Solver *solv;
1268   solv = (Solver *)solv_calloc(1, sizeof(Solver));
1269   solv->pool = pool;
1270   solv->installed = pool->installed;
1271
1272   solv->dup_allowdowngrade = 1;
1273   solv->dup_allowarchchange = 1;
1274   solv->dup_allowvendorchange = 1;
1275
1276   queue_init(&solv->ruletojob);
1277   queue_init(&solv->decisionq);
1278   queue_init(&solv->decisionq_why);
1279   queue_init(&solv->problems);
1280   queue_init(&solv->orphaned);
1281   queue_init(&solv->learnt_why);
1282   queue_init(&solv->learnt_pool);
1283   queue_init(&solv->branches);
1284   queue_init(&solv->weakruleq);
1285   queue_init(&solv->ruleassertions);
1286
1287   queue_push(&solv->learnt_pool, 0);    /* so that 0 does not describe a proof */
1288
1289   map_init(&solv->recommendsmap, pool->nsolvables);
1290   map_init(&solv->suggestsmap, pool->nsolvables);
1291   map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
1292   solv->recommends_index = 0;
1293
1294   solv->decisionmap = (Id *)solv_calloc(pool->nsolvables, sizeof(Id));
1295   solv->nrules = 1;
1296   solv->rules = solv_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
1297   memset(solv->rules, 0, sizeof(Rule));
1298
1299   return solv;
1300 }
1301
1302
1303 /*-------------------------------------------------------------------
1304  *
1305  * solver_free
1306  */
1307
1308 void
1309 solver_free(Solver *solv)
1310 {
1311   queue_free(&solv->job);
1312   queue_free(&solv->ruletojob);
1313   queue_free(&solv->decisionq);
1314   queue_free(&solv->decisionq_why);
1315   queue_free(&solv->learnt_why);
1316   queue_free(&solv->learnt_pool);
1317   queue_free(&solv->problems);
1318   queue_free(&solv->solutions);
1319   queue_free(&solv->orphaned);
1320   queue_free(&solv->branches);
1321   queue_free(&solv->weakruleq);
1322   queue_free(&solv->ruleassertions);
1323
1324   map_free(&solv->recommendsmap);
1325   map_free(&solv->suggestsmap);
1326   map_free(&solv->noupdate);
1327   map_free(&solv->weakrulemap);
1328   map_free(&solv->noobsoletes);
1329
1330   map_free(&solv->updatemap);
1331   map_free(&solv->fixmap);
1332   map_free(&solv->dupmap);
1333   map_free(&solv->dupinvolvedmap);
1334   map_free(&solv->droporphanedmap);
1335   map_free(&solv->cleandepsmap);
1336
1337   solv_free(solv->decisionmap);
1338   solv_free(solv->rules);
1339   solv_free(solv->watches);
1340   solv_free(solv->obsoletes);
1341   solv_free(solv->obsoletes_data);
1342   solv_free(solv->multiversionupdaters);
1343   solv_free(solv->choicerules_ref);
1344   solv_free(solv);
1345 }
1346
1347 int
1348 solver_get_flag(Solver *solv, int flag)
1349 {
1350   switch (flag)
1351   {
1352   case SOLVER_FLAG_ALLOW_DOWNGRADE:
1353     return solv->allowdowngrade;
1354   case SOLVER_FLAG_ALLOW_ARCHCHANGE:
1355     return solv->allowarchchange;
1356   case SOLVER_FLAG_ALLOW_VENDORCHANGE:
1357     return solv->allowvendorchange;
1358   case SOLVER_FLAG_ALLOW_UNINSTALL:
1359     return solv->allowuninstall;
1360   case SOLVER_FLAG_NO_UPDATEPROVIDE:
1361     return solv->noupdateprovide;
1362   case SOLVER_FLAG_SPLITPROVIDES:
1363     return solv->dosplitprovides;
1364   case SOLVER_FLAG_IGNORE_RECOMMENDED:
1365     return solv->dontinstallrecommended;
1366   case SOLVER_FLAG_IGNORE_ALREADY_RECOMMENDED:
1367     return solv->ignorealreadyrecommended;
1368   case SOLVER_FLAG_NO_INFARCHCHECK:
1369     return solv->noinfarchcheck;
1370   default:
1371     break;
1372   }
1373   return -1;
1374 }
1375
1376 int
1377 solver_set_flag(Solver *solv, int flag, int value)
1378 {
1379   int old = solver_get_flag(solv, flag);
1380   switch (flag)
1381   {
1382   case SOLVER_FLAG_ALLOW_DOWNGRADE:
1383     solv->allowdowngrade = value;
1384     break;
1385   case SOLVER_FLAG_ALLOW_ARCHCHANGE:
1386     solv->allowarchchange = value;
1387     break;
1388   case SOLVER_FLAG_ALLOW_VENDORCHANGE:
1389     solv->allowvendorchange = value;
1390     break;
1391   case SOLVER_FLAG_ALLOW_UNINSTALL:
1392     solv->allowuninstall = value;
1393     break;
1394   case SOLVER_FLAG_NO_UPDATEPROVIDE:
1395     solv->noupdateprovide = value;
1396     break;
1397   case SOLVER_FLAG_SPLITPROVIDES:
1398     solv->dosplitprovides = value;
1399     break;
1400   case SOLVER_FLAG_IGNORE_RECOMMENDED:
1401     solv->dontinstallrecommended = value;
1402     break;
1403   case SOLVER_FLAG_IGNORE_ALREADY_RECOMMENDED:
1404     solv->ignorealreadyrecommended = value;
1405     break;
1406   case SOLVER_FLAG_NO_INFARCHCHECK:
1407     solv->noinfarchcheck = value;
1408     break;
1409   default:
1410     break;
1411   }
1412   return old;
1413 }
1414
1415
1416 /*-------------------------------------------------------------------
1417  *
1418  * solver_run_sat
1419  *
1420  * all rules have been set up, now actually run the solver
1421  *
1422  */
1423
1424 void
1425 solver_run_sat(Solver *solv, int disablerules, int doweak)
1426 {
1427   Queue dq;             /* local decisionqueue */
1428   Queue dqs;            /* local decisionqueue for supplements */
1429   int systemlevel;
1430   int level, olevel;
1431   Rule *r;
1432   int i, j, n;
1433   Solvable *s;
1434   Pool *pool = solv->pool;
1435   Id p, *dp;
1436   int minimizationsteps;
1437   int installedpos = solv->installed ? solv->installed->start : 0;
1438
1439   IF_POOLDEBUG (SOLV_DEBUG_RULE_CREATION)
1440     {
1441       POOL_DEBUG (SOLV_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
1442       for (i = 1; i < solv->nrules; i++)
1443         solver_printruleclass(solv, SOLV_DEBUG_RULE_CREATION, solv->rules + i);
1444     }
1445
1446   POOL_DEBUG(SOLV_DEBUG_SOLVER, "initial decisions: %d\n", solv->decisionq.count);
1447
1448   /* start SAT algorithm */
1449   level = 1;
1450   systemlevel = level + 1;
1451   POOL_DEBUG(SOLV_DEBUG_SOLVER, "solving...\n");
1452
1453   queue_init(&dq);
1454   queue_init(&dqs);
1455
1456   /*
1457    * here's the main loop:
1458    * 1) propagate new decisions (only needed once)
1459    * 2) fulfill jobs
1460    * 3) try to keep installed packages
1461    * 4) fulfill all unresolved rules
1462    * 5) install recommended packages
1463    * 6) minimalize solution if we had choices
1464    * if we encounter a problem, we rewind to a safe level and restart
1465    * with step 1
1466    */
1467
1468   minimizationsteps = 0;
1469   for (;;)
1470     {
1471       /*
1472        * initial propagation of the assertions
1473        */
1474       if (level == 1)
1475         {
1476           POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
1477           if ((r = propagate(solv, level)) != 0)
1478             {
1479               if (analyze_unsolvable(solv, r, disablerules))
1480                 continue;
1481               level = 0;
1482               break;    /* unsolvable */
1483             }
1484         }
1485
1486       /*
1487        * resolve jobs first
1488        */
1489      if (level < systemlevel)
1490         {
1491           POOL_DEBUG(SOLV_DEBUG_SOLVER, "resolving job rules\n");
1492           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
1493             {
1494               Id l;
1495               if (r->d < 0)             /* ignore disabled rules */
1496                 continue;
1497               queue_empty(&dq);
1498               FOR_RULELITERALS(l, dp, r)
1499                 {
1500                   if (l < 0)
1501                     {
1502                       if (solv->decisionmap[-l] <= 0)
1503                         break;
1504                     }
1505                   else
1506                     {
1507                       if (solv->decisionmap[l] > 0)
1508                         break;
1509                       if (solv->decisionmap[l] == 0)
1510                         queue_push(&dq, l);
1511                     }
1512                 }
1513               if (l || !dq.count)
1514                 continue;
1515               /* prune to installed if not updating */
1516               if (dq.count > 1 && solv->installed && !solv->updatemap_all)
1517                 {
1518                   int j, k;
1519                   for (j = k = 0; j < dq.count; j++)
1520                     {
1521                       Solvable *s = pool->solvables + dq.elements[j];
1522                       if (s->repo == solv->installed)
1523                         {
1524                           dq.elements[k++] = dq.elements[j];
1525                           if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start))
1526                             {
1527                               k = 0;    /* package wants to be updated, do not prune */
1528                               break;
1529                             }
1530                         }
1531                     }
1532                   if (k)
1533                     dq.count = k;
1534                 }
1535               olevel = level;
1536               level = selectandinstall(solv, level, &dq, disablerules, i);
1537               if (level == 0)
1538                 break;
1539               if (level <= olevel)
1540                 break;
1541             }
1542           if (level == 0)
1543             break;      /* unsolvable */
1544           systemlevel = level + 1;
1545           if (i < solv->jobrules_end)
1546             continue;
1547           solv->decisioncnt_update = solv->decisionq.count;
1548           solv->decisioncnt_keep = solv->decisionq.count;
1549         }
1550
1551       /*
1552        * installed packages
1553        */
1554       if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled)
1555         {
1556           Repo *installed = solv->installed;
1557           int pass;
1558
1559           POOL_DEBUG(SOLV_DEBUG_SOLVER, "resolving installed packages\n");
1560           /* we use two passes if we need to update packages
1561            * to create a better user experience */
1562           for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
1563             {
1564               int passlevel = level;
1565               if (pass == 1)
1566                 solv->decisioncnt_keep = solv->decisionq.count;
1567               /* start with installedpos, the position that gave us problems last time */
1568               for (i = installedpos, n = installed->start; n < installed->end; i++, n++)
1569                 {
1570                   Rule *rr;
1571                   Id d;
1572
1573                   if (i == installed->end)
1574                     i = installed->start;
1575                   s = pool->solvables + i;
1576                   if (s->repo != installed)
1577                     continue;
1578
1579                   if (solv->decisionmap[i] > 0)
1580                     continue;
1581                   if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start))
1582                     continue;           /* updates first */
1583                   r = solv->rules + solv->updaterules + (i - installed->start);
1584                   rr = r;
1585                   if (!rr->p || rr->d < 0)      /* disabled -> look at feature rule */
1586                     rr -= solv->installed->end - solv->installed->start;
1587                   if (!rr->p)           /* identical to update rule? */
1588                     rr = r;
1589                   if (!rr->p)
1590                     continue;           /* orpaned package */
1591
1592                   /* XXX: noupdate check is probably no longer needed, as all jobs should
1593                    * already be satisfied */
1594                   /* Actually we currently still need it because of erase jobs */
1595                   /* if noupdate is set we do not look at update candidates */
1596                   queue_empty(&dq);
1597                   if (!MAPTST(&solv->noupdate, i - installed->start) && (solv->decisionmap[i] < 0 || solv->updatemap_all || (solv->updatemap.size && MAPTST(&solv->updatemap, i - installed->start)) || rr->p != i))
1598                     {
1599                       if (solv->noobsoletes.size && solv->multiversionupdaters
1600                              && (d = solv->multiversionupdaters[i - installed->start]) != 0)
1601                         {
1602                           /* special multiversion handling, make sure best version is chosen */
1603                           queue_push(&dq, i);
1604                           while ((p = pool->whatprovidesdata[d++]) != 0)
1605                             if (solv->decisionmap[p] >= 0)
1606                               queue_push(&dq, p);
1607                           policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE);
1608                           p = dq.elements[0];
1609                           if (p != i && solv->decisionmap[p] == 0)
1610                             {
1611                               rr = solv->rules + solv->featurerules + (i - solv->installed->start);
1612                               if (!rr->p)               /* update rule == feature rule? */
1613                                 rr = rr - solv->featurerules + solv->updaterules;
1614                               dq.count = 1;
1615                             }
1616                           else
1617                             dq.count = 0;
1618                         }
1619                       else
1620                         {
1621                           /* update to best package */
1622                           FOR_RULELITERALS(p, dp, rr)
1623                             {
1624                               if (solv->decisionmap[p] > 0)
1625                                 {
1626                                   dq.count = 0;         /* already fulfilled */
1627                                   break;
1628                                 }
1629                               if (!solv->decisionmap[p])
1630                                 queue_push(&dq, p);
1631                             }
1632                         }
1633                     }
1634                   /* install best version */
1635                   if (dq.count)
1636                     {
1637                       olevel = level;
1638                       level = selectandinstall(solv, level, &dq, disablerules, rr - solv->rules);
1639                       if (level == 0)
1640                         {
1641                           queue_free(&dq);
1642                           queue_free(&dqs);
1643                           return;
1644                         }
1645                       if (level <= olevel)
1646                         {
1647                           if (level == 1 || level < passlevel)
1648                             break;      /* trouble */
1649                           if (level < olevel)
1650                             n = installed->start;       /* redo all */
1651                           i--;
1652                           n--;
1653                           continue;
1654                         }
1655                     }
1656                   /* if still undecided keep package */
1657                   if (solv->decisionmap[i] == 0)
1658                     {
1659                       olevel = level;
1660                       if (solv->cleandepsmap.size && MAPTST(&solv->cleandepsmap, i - installed->start))
1661                         {
1662                           POOL_DEBUG(SOLV_DEBUG_POLICY, "cleandeps erasing %s\n", pool_solvid2str(pool, i));
1663                           level = setpropagatelearn(solv, level, -i, disablerules, 0);
1664                         }
1665                       else
1666                         {
1667                           POOL_DEBUG(SOLV_DEBUG_POLICY, "keeping %s\n", pool_solvid2str(pool, i));
1668                           level = setpropagatelearn(solv, level, i, disablerules, r - solv->rules);
1669                         }
1670                       if (level == 0)
1671                         break;
1672                       if (level <= olevel)
1673                         {
1674                           if (level == 1 || level < passlevel)
1675                             break;      /* trouble */
1676                           if (level < olevel)
1677                             n = installed->start;       /* redo all */
1678                           i--;
1679                           n--;
1680                           continue;     /* retry with learnt rule */
1681                         }
1682                     }
1683                 }
1684               if (n < installed->end)
1685                 {
1686                   installedpos = i;     /* retry problem solvable next time */
1687                   break;                /* ran into trouble */
1688                 }
1689               installedpos = installed->start;  /* reset installedpos */
1690             }
1691           if (level == 0)
1692             break;              /* unsolvable */
1693           systemlevel = level + 1;
1694           if (pass < 2)
1695             continue;           /* had trouble, retry */
1696         }
1697
1698       if (level < systemlevel)
1699         systemlevel = level;
1700
1701       /*
1702        * decide
1703        */
1704       solv->decisioncnt_resolve = solv->decisionq.count;
1705       POOL_DEBUG(SOLV_DEBUG_POLICY, "deciding unresolved rules\n");
1706       for (i = 1, n = 1; n < solv->nrules; i++, n++)
1707         {
1708           if (i == solv->nrules)
1709             i = 1;
1710           r = solv->rules + i;
1711           if (r->d < 0)         /* ignore disabled rules */
1712             continue;
1713           queue_empty(&dq);
1714           if (r->d == 0)
1715             {
1716               /* binary or unary rule */
1717               /* need two positive undecided literals */
1718               if (r->p < 0 || r->w2 <= 0)
1719                 continue;
1720               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
1721                 continue;
1722               queue_push(&dq, r->p);
1723               queue_push(&dq, r->w2);
1724             }
1725           else
1726             {
1727               /* make sure that
1728                * all negative literals are installed
1729                * no positive literal is installed
1730                * i.e. the rule is not fulfilled and we
1731                * just need to decide on the positive literals
1732                */
1733               if (r->p < 0)
1734                 {
1735                   if (solv->decisionmap[-r->p] <= 0)
1736                     continue;
1737                 }
1738               else
1739                 {
1740                   if (solv->decisionmap[r->p] > 0)
1741                     continue;
1742                   if (solv->decisionmap[r->p] == 0)
1743                     queue_push(&dq, r->p);
1744                 }
1745               dp = pool->whatprovidesdata + r->d;
1746               while ((p = *dp++) != 0)
1747                 {
1748                   if (p < 0)
1749                     {
1750                       if (solv->decisionmap[-p] <= 0)
1751                         break;
1752                     }
1753                   else
1754                     {
1755                       if (solv->decisionmap[p] > 0)
1756                         break;
1757                       if (solv->decisionmap[p] == 0)
1758                         queue_push(&dq, p);
1759                     }
1760                 }
1761               if (p)
1762                 continue;
1763             }
1764           IF_POOLDEBUG (SOLV_DEBUG_PROPAGATE)
1765             {
1766               POOL_DEBUG(SOLV_DEBUG_PROPAGATE, "unfulfilled ");
1767               solver_printruleclass(solv, SOLV_DEBUG_PROPAGATE, r);
1768             }
1769           /* dq.count < 2 cannot happen as this means that
1770            * the rule is unit */
1771           assert(dq.count > 1);
1772
1773           olevel = level;
1774           level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules);
1775           if (level == 0)
1776             break;              /* unsolvable */
1777           if (level < systemlevel || level == 1)
1778             break;              /* trouble */
1779           /* something changed, so look at all rules again */
1780           n = 0;
1781         }
1782
1783       if (n != solv->nrules)    /* ran into trouble? */
1784         {
1785           if (level == 0)
1786             break;              /* unsolvable */
1787           continue;             /* start over */
1788         }
1789
1790       /* at this point we have a consistent system. now do the extras... */
1791
1792       solv->decisioncnt_weak = solv->decisionq.count;
1793       if (doweak)
1794         {
1795           int qcount;
1796
1797           POOL_DEBUG(SOLV_DEBUG_POLICY, "installing recommended packages\n");
1798           queue_empty(&dq);     /* recommended packages */
1799           queue_empty(&dqs);    /* supplemented packages */
1800           for (i = 1; i < pool->nsolvables; i++)
1801             {
1802               if (solv->decisionmap[i] < 0)
1803                 continue;
1804               if (solv->decisionmap[i] > 0)
1805                 {
1806                   /* installed, check for recommends */
1807                   Id *recp, rec, pp, p;
1808                   s = pool->solvables + i;
1809                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
1810                     continue;
1811                   /* XXX need to special case AND ? */
1812                   if (s->recommends)
1813                     {
1814                       recp = s->repo->idarraydata + s->recommends;
1815                       while ((rec = *recp++) != 0)
1816                         {
1817                           qcount = dq.count;
1818                           FOR_PROVIDES(p, pp, rec)
1819                             {
1820                               if (solv->decisionmap[p] > 0)
1821                                 {
1822                                   dq.count = qcount;
1823                                   break;
1824                                 }
1825                               else if (solv->decisionmap[p] == 0)
1826                                 {
1827                                   if (solv->dupmap_all && solv->installed && pool->solvables[p].repo == solv->installed && (solv->droporphanedmap_all || (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))))
1828                                     continue;
1829                                   queue_pushunique(&dq, p);
1830                                 }
1831                             }
1832                         }
1833                     }
1834                 }
1835               else
1836                 {
1837                   s = pool->solvables + i;
1838                   if (!s->supplements)
1839                     continue;
1840                   if (!pool_installable(pool, s))
1841                     continue;
1842                   if (!solver_is_supplementing(solv, s))
1843                     continue;
1844                   if (solv->dupmap_all && solv->installed && s->repo == solv->installed && (solv->droporphanedmap_all || (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, i - solv->installed->start))))
1845                     continue;
1846                   queue_push(&dqs, i);
1847                 }
1848             }
1849
1850           /* filter out all packages obsoleted by installed packages */
1851           /* this is no longer needed if we have reverse obsoletes */
1852           if ((dqs.count || dq.count) && solv->installed)
1853             {
1854               Map obsmap;
1855               Id obs, *obsp, po, ppo;
1856
1857               map_init(&obsmap, pool->nsolvables);
1858               for (p = solv->installed->start; p < solv->installed->end; p++)
1859                 {
1860                   s = pool->solvables + p;
1861                   if (s->repo != solv->installed || !s->obsoletes)
1862                     continue;
1863                   if (solv->decisionmap[p] <= 0)
1864                     continue;
1865                   if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
1866                     continue;
1867                   obsp = s->repo->idarraydata + s->obsoletes;
1868                   /* foreach obsoletes */
1869                   while ((obs = *obsp++) != 0)
1870                     FOR_PROVIDES(po, ppo, obs)
1871                       MAPSET(&obsmap, po);
1872                 }
1873               for (i = j = 0; i < dqs.count; i++)
1874                 if (!MAPTST(&obsmap, dqs.elements[i]))
1875                   dqs.elements[j++] = dqs.elements[i];
1876               dqs.count = j;
1877               for (i = j = 0; i < dq.count; i++)
1878                 if (!MAPTST(&obsmap, dq.elements[i]))
1879                   dq.elements[j++] = dq.elements[i];
1880               dq.count = j;
1881               map_free(&obsmap);
1882             }
1883
1884           /* filter out all already supplemented packages if requested */
1885           if (solv->ignorealreadyrecommended && dqs.count)
1886             {
1887               /* turn off all new packages */
1888               for (i = 0; i < solv->decisionq.count; i++)
1889                 {
1890                   p = solv->decisionq.elements[i];
1891                   if (p < 0)
1892                     continue;
1893                   s = pool->solvables + p;
1894                   if (s->repo && s->repo != solv->installed)
1895                     solv->decisionmap[p] = -solv->decisionmap[p];
1896                 }
1897               /* filter out old supplements */
1898               for (i = j = 0; i < dqs.count; i++)
1899                 {
1900                   p = dqs.elements[i];
1901                   s = pool->solvables + p;
1902                   if (!s->supplements)
1903                     continue;
1904                   if (!solver_is_supplementing(solv, s))
1905                     dqs.elements[j++] = p;
1906                 }
1907               dqs.count = j;
1908               /* undo turning off */
1909               for (i = 0; i < solv->decisionq.count; i++)
1910                 {
1911                   p = solv->decisionq.elements[i];
1912                   if (p < 0)
1913                     continue;
1914                   s = pool->solvables + p;
1915                   if (s->repo && s->repo != solv->installed)
1916                     solv->decisionmap[p] = -solv->decisionmap[p];
1917                 }
1918             }
1919
1920           /* multiversion doesn't mix well with supplements.
1921            * filter supplemented packages where we already decided
1922            * to install a different version (see bnc#501088) */
1923           if (dqs.count && solv->noobsoletes.size)
1924             {
1925               for (i = j = 0; i < dqs.count; i++)
1926                 {
1927                   p = dqs.elements[i];
1928                   if (MAPTST(&solv->noobsoletes, p))
1929                     {
1930                       Id p2, pp2;
1931                       s = pool->solvables + p;
1932                       FOR_PROVIDES(p2, pp2, s->name)
1933                         if (solv->decisionmap[p2] > 0 && pool->solvables[p2].name == s->name)
1934                           break;
1935                       if (p2)
1936                         continue;       /* ignore this package */
1937                     }
1938                   dqs.elements[j++] = p;
1939                 }
1940               dqs.count = j;
1941             }
1942
1943           /* make dq contain both recommended and supplemented pkgs */
1944           if (dqs.count)
1945             {
1946               for (i = 0; i < dqs.count; i++)
1947                 queue_pushunique(&dq, dqs.elements[i]);
1948             }
1949
1950           if (dq.count)
1951             {
1952               Map dqmap;
1953               int decisioncount = solv->decisionq.count;
1954
1955               if (dq.count == 1)
1956                 {
1957                   /* simple case, just one package. no need to choose to best version */
1958                   p = dq.elements[0];
1959                   if (dqs.count)
1960                     POOL_DEBUG(SOLV_DEBUG_POLICY, "installing supplemented %s\n", pool_solvid2str(pool, p));
1961                   else
1962                     POOL_DEBUG(SOLV_DEBUG_POLICY, "installing recommended %s\n", pool_solvid2str(pool, p));
1963                   level = setpropagatelearn(solv, level, p, 0, 0);
1964                   if (level == 0)
1965                     break;
1966                   continue;     /* back to main loop */
1967                 }
1968
1969               /* filter packages, this gives us the best versions */
1970               policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
1971
1972               /* create map of result */
1973               map_init(&dqmap, pool->nsolvables);
1974               for (i = 0; i < dq.count; i++)
1975                 MAPSET(&dqmap, dq.elements[i]);
1976
1977               /* install all supplemented packages */
1978               for (i = 0; i < dqs.count; i++)
1979                 {
1980                   p = dqs.elements[i];
1981                   if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
1982                     continue;
1983                   POOL_DEBUG(SOLV_DEBUG_POLICY, "installing supplemented %s\n", pool_solvid2str(pool, p));
1984                   olevel = level;
1985                   level = setpropagatelearn(solv, level, p, 0, 0);
1986                   if (level <= olevel)
1987                     break;
1988                 }
1989               if (i < dqs.count || solv->decisionq.count < decisioncount)
1990                 {
1991                   map_free(&dqmap);
1992                   if (level == 0)
1993                     break;
1994                   continue;
1995                 }
1996
1997               /* install all recommended packages */
1998               /* more work as we want to created branches if multiple
1999                * choices are valid */
2000               for (i = 0; i < decisioncount; i++)
2001                 {
2002                   Id rec, *recp, pp;
2003                   p = solv->decisionq.elements[i];
2004                   if (p < 0)
2005                     continue;
2006                   s = pool->solvables + p;
2007                   if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
2008                     continue;
2009                   if (!s->recommends)
2010                     continue;
2011                   recp = s->repo->idarraydata + s->recommends;
2012                   while ((rec = *recp++) != 0)
2013                     {
2014                       queue_empty(&dq);
2015                       FOR_PROVIDES(p, pp, rec)
2016                         {
2017                           if (solv->decisionmap[p] > 0)
2018                             {
2019                               dq.count = 0;
2020                               break;
2021                             }
2022                           else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
2023                             queue_pushunique(&dq, p);
2024                         }
2025                       if (!dq.count)
2026                         continue;
2027                       if (dq.count > 1)
2028                         {
2029                           /* multiple candidates, open a branch */
2030                           for (i = 1; i < dq.count; i++)
2031                             queue_push(&solv->branches, dq.elements[i]);
2032                           queue_push(&solv->branches, -level);
2033                         }
2034                       p = dq.elements[0];
2035                       POOL_DEBUG(SOLV_DEBUG_POLICY, "installing recommended %s\n", pool_solvid2str(pool, p));
2036                       olevel = level;
2037                       level = setpropagatelearn(solv, level, p, 0, 0);
2038                       if (level <= olevel || solv->decisionq.count < decisioncount)
2039                         break;  /* we had to revert some decisions */
2040                     }
2041                   if (rec)
2042                     break;      /* had a problem above, quit loop */
2043                 }
2044               map_free(&dqmap);
2045               if (level == 0)
2046                 break;
2047               continue;         /* back to main loop so that all deps are checked */
2048             }
2049         }
2050
2051       solv->decisioncnt_orphan = solv->decisionq.count;
2052       if (solv->dupmap_all && solv->installed)
2053         {
2054           int installedone = 0;
2055
2056           /* let's see if we can install some unsupported package */
2057           POOL_DEBUG(SOLV_DEBUG_SOLVER, "deciding orphaned packages\n");
2058           for (i = 0; i < solv->orphaned.count; i++)
2059             {
2060               p = solv->orphaned.elements[i];
2061               if (solv->decisionmap[p])
2062                 continue;       /* already decided */
2063               olevel = level;
2064               if (solv->droporphanedmap_all)
2065                 continue;
2066               if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))
2067                 continue;
2068               POOL_DEBUG(SOLV_DEBUG_SOLVER, "keeping orphaned %s\n", pool_solvid2str(pool, p));
2069               level = setpropagatelearn(solv, level, p, 0, 0);
2070               installedone = 1;
2071               if (level < olevel)
2072                 break;
2073             }
2074           if (level == 0)
2075             break;
2076           if (installedone || i < solv->orphaned.count)
2077             {
2078               if (level == 0)
2079                 break;
2080               continue;         /* back to main loop */
2081             }
2082           for (i = 0; i < solv->orphaned.count; i++)
2083             {
2084               p = solv->orphaned.elements[i];
2085               if (solv->decisionmap[p])
2086                 continue;       /* already decided */
2087               POOL_DEBUG(SOLV_DEBUG_SOLVER, "removing orphaned %s\n", pool_solvid2str(pool, p));
2088               olevel = level;
2089               level = setpropagatelearn(solv, level, -p, 0, 0);
2090               if (level < olevel)
2091                 break;
2092             }
2093           if (i < solv->orphaned.count)
2094             {
2095               if (level == 0)
2096                 break;
2097               continue;         /* back to main loop */
2098             }
2099         }
2100
2101      if (solv->solution_callback)
2102         {
2103           solv->solution_callback(solv, solv->solution_callback_data);
2104           if (solv->branches.count)
2105             {
2106               int i = solv->branches.count - 1;
2107               int l = -solv->branches.elements[i];
2108               Id why;
2109
2110               for (; i > 0; i--)
2111                 if (solv->branches.elements[i - 1] < 0)
2112                   break;
2113               p = solv->branches.elements[i];
2114               POOL_DEBUG(SOLV_DEBUG_SOLVER, "branching with %s\n", pool_solvid2str(pool, p));
2115               queue_empty(&dq);
2116               for (j = i + 1; j < solv->branches.count; j++)
2117                 queue_push(&dq, solv->branches.elements[j]);
2118               solv->branches.count = i;
2119               level = l;
2120               revert(solv, level);
2121               if (dq.count > 1)
2122                 for (j = 0; j < dq.count; j++)
2123                   queue_push(&solv->branches, dq.elements[j]);
2124               olevel = level;
2125               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2126               assert(why >= 0);
2127               level = setpropagatelearn(solv, level, p, disablerules, why);
2128               if (level == 0)
2129                 break;
2130               continue;
2131             }
2132           /* all branches done, we're finally finished */
2133           break;
2134         }
2135
2136       /* auto-minimization step */
2137      if (solv->branches.count)
2138         {
2139           int l = 0, lasti = -1, lastl = -1;
2140           Id why;
2141
2142           p = 0;
2143           for (i = solv->branches.count - 1; i >= 0; i--)
2144             {
2145               p = solv->branches.elements[i];
2146               if (p < 0)
2147                 l = -p;
2148               else if (p > 0 && solv->decisionmap[p] > l + 1)
2149                 {
2150                   lasti = i;
2151                   lastl = l;
2152                 }
2153             }
2154           if (lasti >= 0)
2155             {
2156               /* kill old solvable so that we do not loop */
2157               p = solv->branches.elements[lasti];
2158               solv->branches.elements[lasti] = 0;
2159               POOL_DEBUG(SOLV_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, pool_solvid2str(pool, p));
2160               minimizationsteps++;
2161
2162               level = lastl;
2163               revert(solv, level);
2164               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2165               assert(why >= 0);
2166               olevel = level;
2167               level = setpropagatelearn(solv, level, p, disablerules, why);
2168               if (level == 0)
2169                 break;
2170               continue;         /* back to main loop */
2171             }
2172         }
2173       /* no minimization found, we're finally finished! */
2174       break;
2175     }
2176
2177   POOL_DEBUG(SOLV_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
2178
2179   POOL_DEBUG(SOLV_DEBUG_STATS, "done solving.\n\n");
2180   queue_free(&dq);
2181   queue_free(&dqs);
2182   if (level == 0)
2183     {
2184       /* unsolvable */
2185       solv->decisioncnt_update = solv->decisionq.count;
2186       solv->decisioncnt_keep = solv->decisionq.count;
2187       solv->decisioncnt_resolve = solv->decisionq.count;
2188       solv->decisioncnt_weak = solv->decisionq.count;
2189       solv->decisioncnt_orphan = solv->decisionq.count;
2190     }
2191 #if 0
2192   solver_printdecisionq(solv, SOLV_DEBUG_RESULT);
2193 #endif
2194 }
2195
2196
2197 /*-------------------------------------------------------------------
2198  *
2199  * remove disabled conflicts
2200  *
2201  * purpose: update the decisionmap after some rules were disabled.
2202  * this is used to calculate the suggested/recommended package list.
2203  * Also returns a "removed" list to undo the discisionmap changes.
2204  */
2205
2206 static void
2207 removedisabledconflicts(Solver *solv, Queue *removed)
2208 {
2209   Pool *pool = solv->pool;
2210   int i, n;
2211   Id p, why, *dp;
2212   Id new;
2213   Rule *r;
2214   Id *decisionmap = solv->decisionmap;
2215
2216   queue_empty(removed);
2217   for (i = 0; i < solv->decisionq.count; i++)
2218     {
2219       p = solv->decisionq.elements[i];
2220       if (p > 0)
2221         continue;       /* conflicts only, please */
2222       why = solv->decisionq_why.elements[i];
2223       if (why == 0)
2224         {
2225           /* no rule involved, must be a orphan package drop */
2226           continue;
2227         }
2228       /* we never do conflicts on free decisions, so there
2229        * must have been an unit rule */
2230       assert(why > 0);
2231       r = solv->rules + why;
2232       if (r->d < 0 && decisionmap[-p])
2233         {
2234           /* rule is now disabled, remove from decisionmap */
2235           POOL_DEBUG(SOLV_DEBUG_SOLVER, "removing conflict for package %s[%d]\n", pool_solvid2str(pool, -p), -p);
2236           queue_push(removed, -p);
2237           queue_push(removed, decisionmap[-p]);
2238           decisionmap[-p] = 0;
2239         }
2240     }
2241   if (!removed->count)
2242     return;
2243   /* we removed some confliced packages. some of them might still
2244    * be in conflict, so search for unit rules and re-conflict */
2245   new = 0;
2246   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
2247     {
2248       if (i == solv->nrules)
2249         {
2250           i = 1;
2251           r = solv->rules + i;
2252         }
2253       if (r->d < 0)
2254         continue;
2255       if (!r->w2)
2256         {
2257           if (r->p < 0 && !decisionmap[-r->p])
2258             new = r->p;
2259         }
2260       else if (!r->d)
2261         {
2262           /* binary rule */
2263           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
2264             new = r->p;
2265           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
2266             new = r->w2;
2267         }
2268       else
2269         {
2270           if (r->p < 0 && decisionmap[-r->p] == 0)
2271             new = r->p;
2272           if (new || DECISIONMAP_FALSE(r->p))
2273             {
2274               dp = pool->whatprovidesdata + r->d;
2275               while ((p = *dp++) != 0)
2276                 {
2277                   if (new && p == new)
2278                     continue;
2279                   if (p < 0 && decisionmap[-p] == 0)
2280                     {
2281                       if (new)
2282                         {
2283                           new = 0;
2284                           break;
2285                         }
2286                       new = p;
2287                     }
2288                   else if (!DECISIONMAP_FALSE(p))
2289                     {
2290                       new = 0;
2291                       break;
2292                     }
2293                 }
2294             }
2295         }
2296       if (new)
2297         {
2298           POOL_DEBUG(SOLV_DEBUG_SOLVER, "re-conflicting package %s[%d]\n", pool_solvid2str(pool, -new), -new);
2299           decisionmap[-new] = -1;
2300           new = 0;
2301           n = 0;        /* redo all rules */
2302         }
2303     }
2304 }
2305
2306 static inline void
2307 undo_removedisabledconflicts(Solver *solv, Queue *removed)
2308 {
2309   int i;
2310   for (i = 0; i < removed->count; i += 2)
2311     solv->decisionmap[removed->elements[i]] = removed->elements[i + 1];
2312 }
2313
2314
2315 /*-------------------------------------------------------------------
2316  *
2317  * weaken solvable dependencies
2318  */
2319
2320 static void
2321 weaken_solvable_deps(Solver *solv, Id p)
2322 {
2323   int i;
2324   Rule *r;
2325
2326   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
2327     {
2328       if (r->p != -p)
2329         continue;
2330       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
2331         continue;       /* conflict */
2332       queue_push(&solv->weakruleq, i);
2333     }
2334 }
2335
2336
2337 /********************************************************************/
2338 /* main() */
2339
2340
2341 void
2342 solver_calculate_noobsmap(Pool *pool, Queue *job, Map *noobsmap)
2343 {
2344   int i;
2345   Id how, what, select;
2346   Id p, pp;
2347   for (i = 0; i < job->count; i += 2)
2348     {
2349       how = job->elements[i];
2350       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
2351         continue;
2352       what = job->elements[i + 1];
2353       select = how & SOLVER_SELECTMASK;
2354       if (!noobsmap->size)
2355         map_grow(noobsmap, pool->nsolvables);
2356       FOR_JOB_SELECT(p, pp, select, what)
2357         MAPSET(noobsmap, p);
2358     }
2359 }
2360
2361 /*
2362  * add a rule created by a job, record job number and weak flag
2363  */
2364 static inline void
2365 solver_addjobrule(Solver *solv, Id p, Id d, Id job, int weak)
2366 {
2367   solver_addrule(solv, p, d);
2368   queue_push(&solv->ruletojob, job);
2369   if (weak)
2370     queue_push(&solv->weakruleq, solv->nrules - 1);
2371 }
2372
2373 /*
2374  *
2375  * solve job queue
2376  *
2377  */
2378
2379 int
2380 solver_solve(Solver *solv, Queue *job)
2381 {
2382   Pool *pool = solv->pool;
2383   Repo *installed = solv->installed;
2384   int i;
2385   int oldnrules;
2386   Map addedmap;                /* '1' == have rpm-rules for solvable */
2387   Map installcandidatemap;
2388   Id how, what, select, name, weak, p, pp, d;
2389   Queue q;
2390   Solvable *s;
2391   Rule *r;
2392   int now, solve_start;
2393   int hasdupjob = 0;
2394
2395   solve_start = solv_timems(0);
2396
2397   /* log solver options */
2398   POOL_DEBUG(SOLV_DEBUG_STATS, "solver started\n");
2399   POOL_DEBUG(SOLV_DEBUG_STATS, "dosplitprovides=%d, noupdateprovide=%d noinfarchcheck=%d\n", solv->dosplitprovides, solv->noupdateprovide, solv->noinfarchcheck);
2400   POOL_DEBUG(SOLV_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
2401   POOL_DEBUG(SOLV_DEBUG_STATS, "promoteepoch=%d, allowselfconflicts=%d\n", pool->promoteepoch, pool->allowselfconflicts);
2402   POOL_DEBUG(SOLV_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d, obsoleteusescolors=%d\n", pool->obsoleteusesprovides, pool->implicitobsoleteusesprovides, pool->obsoleteusescolors);
2403   POOL_DEBUG(SOLV_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended);
2404
2405   /* create whatprovides if not already there */
2406   if (!pool->whatprovides)
2407     pool_createwhatprovides(pool);
2408
2409   /* create obsolete index */
2410   policy_create_obsolete_index(solv);
2411
2412   /* remember job */
2413   queue_free(&solv->job);
2414   queue_init_clone(&solv->job, job);
2415
2416   /*
2417    * create basic rule set of all involved packages
2418    * use addedmap bitmap to make sure we don't create rules twice
2419    */
2420
2421   /* create noobsolete map if needed */
2422   solver_calculate_noobsmap(pool, job, &solv->noobsoletes);
2423
2424   map_init(&addedmap, pool->nsolvables);
2425   MAPSET(&addedmap, SYSTEMSOLVABLE);
2426
2427   map_init(&installcandidatemap, pool->nsolvables);
2428   queue_init(&q);
2429
2430   now = solv_timems(0);
2431   /*
2432    * create rules for all package that could be involved with the solving
2433    * so called: rpm rules
2434    *
2435    */
2436   if (installed)
2437     {
2438       /* check for update/verify jobs as they need to be known early */
2439       for (i = 0; i < job->count; i += 2)
2440         {
2441           how = job->elements[i];
2442           what = job->elements[i + 1];
2443           select = how & SOLVER_SELECTMASK;
2444           switch (how & SOLVER_JOBMASK)
2445             {
2446             case SOLVER_VERIFY:
2447               if (select == SOLVER_SOLVABLE_ALL)
2448                 solv->fixmap_all = 1;
2449               FOR_JOB_SELECT(p, pp, select, what)
2450                 {
2451                   s = pool->solvables + p;
2452                   if (!solv->installed || s->repo != solv->installed)
2453                     continue;
2454                   if (!solv->fixmap.size)
2455                     map_grow(&solv->fixmap, solv->installed->end - solv->installed->start);
2456                   MAPSET(&solv->fixmap, p - solv->installed->start);
2457                 }
2458               break;
2459             case SOLVER_UPDATE:
2460               if (select == SOLVER_SOLVABLE_ALL)
2461                 solv->updatemap_all = 1;
2462               FOR_JOB_SELECT(p, pp, select, what)
2463                 {
2464                   s = pool->solvables + p;
2465                   if (!solv->installed || s->repo != solv->installed)
2466                     continue;
2467                   if (!solv->updatemap.size)
2468                     map_grow(&solv->updatemap, solv->installed->end - solv->installed->start);
2469                   MAPSET(&solv->updatemap, p - solv->installed->start);
2470                 }
2471               break;
2472             default:
2473               break;
2474             }
2475         }
2476
2477       oldnrules = solv->nrules;
2478       FOR_REPO_SOLVABLES(installed, p, s)
2479         solver_addrpmrulesforsolvable(solv, s, &addedmap);
2480       POOL_DEBUG(SOLV_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
2481       oldnrules = solv->nrules;
2482       FOR_REPO_SOLVABLES(installed, p, s)
2483         solver_addrpmrulesforupdaters(solv, s, &addedmap, 1);
2484       POOL_DEBUG(SOLV_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
2485     }
2486
2487   /*
2488    * create rules for all packages involved in the job
2489    * (to be installed or removed)
2490    */
2491
2492   oldnrules = solv->nrules;
2493   for (i = 0; i < job->count; i += 2)
2494     {
2495       how = job->elements[i];
2496       what = job->elements[i + 1];
2497       select = how & SOLVER_SELECTMASK;
2498
2499       switch (how & SOLVER_JOBMASK)
2500         {
2501         case SOLVER_INSTALL:
2502           FOR_JOB_SELECT(p, pp, select, what)
2503             {
2504               MAPSET(&installcandidatemap, p);
2505               solver_addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
2506             }
2507           break;
2508         case SOLVER_DISTUPGRADE:
2509           if (select == SOLVER_SOLVABLE_ALL)
2510             {
2511               solv->dupmap_all = 1;
2512               solv->updatemap_all = 1;
2513             }
2514           if (!solv->dupmap_all)
2515             hasdupjob = 1;
2516           break;
2517         default:
2518           break;
2519         }
2520     }
2521   POOL_DEBUG(SOLV_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
2522
2523
2524   /*
2525    * add rules for suggests, enhances
2526    */
2527   oldnrules = solv->nrules;
2528   solver_addrpmrulesforweak(solv, &addedmap);
2529   POOL_DEBUG(SOLV_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
2530
2531   /*
2532    * first pass done, we now have all the rpm rules we need.
2533    * unify existing rules before going over all job rules and
2534    * policy rules.
2535    * at this point the system is always solvable,
2536    * as an empty system (remove all packages) is a valid solution
2537    */
2538
2539   IF_POOLDEBUG (SOLV_DEBUG_STATS)
2540     {
2541       int possible = 0, installable = 0;
2542       for (i = 1; i < pool->nsolvables; i++)
2543         {
2544           if (pool_installable(pool, pool->solvables + i))
2545             installable++;
2546           if (MAPTST(&addedmap, i))
2547             possible++;
2548         }
2549       POOL_DEBUG(SOLV_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
2550     }
2551
2552   solver_unifyrules(solv);                          /* remove duplicate rpm rules */
2553   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
2554
2555   POOL_DEBUG(SOLV_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
2556   POOL_DEBUG(SOLV_DEBUG_STATS, "rpm rule creation took %d ms\n", solv_timems(now));
2557
2558   /* create dup maps if needed. We need the maps early to create our
2559    * update rules */
2560   if (hasdupjob)
2561     solver_createdupmaps(solv);
2562
2563   /*
2564    * create feature rules
2565    *
2566    * foreach installed:
2567    *   create assertion (keep installed, if no update available)
2568    *   or
2569    *   create update rule (A|update1(A)|update2(A)|...)
2570    *
2571    * those are used later on to keep a version of the installed packages in
2572    * best effort mode
2573    */
2574
2575   solv->featurerules = solv->nrules;              /* mark start of feature rules */
2576   if (installed)
2577     {
2578       /* foreach possibly installed solvable */
2579       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2580         {
2581           if (s->repo != installed)
2582             {
2583               solver_addrule(solv, 0, 0);       /* create dummy rule */
2584               continue;
2585             }
2586           solver_addupdaterule(solv, s, 1);    /* allow s to be updated */
2587         }
2588       /* make sure we accounted for all rules */
2589       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
2590     }
2591   solv->featurerules_end = solv->nrules;
2592
2593     /*
2594      * Add update rules for installed solvables
2595      *
2596      * almost identical to feature rules
2597      * except that downgrades/archchanges/vendorchanges are not allowed
2598      */
2599
2600   solv->updaterules = solv->nrules;
2601
2602   if (installed)
2603     { /* foreach installed solvables */
2604       /* we create all update rules, but disable some later on depending on the job */
2605       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2606         {
2607           Rule *sr;
2608
2609           if (s->repo != installed)
2610             {
2611               solver_addrule(solv, 0, 0);       /* create dummy rule */
2612               continue;
2613             }
2614           solver_addupdaterule(solv, s, 0);     /* allowall = 0: downgrades not allowed */
2615           /*
2616            * check for and remove duplicate
2617            */
2618           r = solv->rules + solv->nrules - 1;           /* r: update rule */
2619           sr = r - (installed->end - installed->start); /* sr: feature rule */
2620           /* it's orphaned if there is no feature rule or the feature rule
2621            * consists just of the installed package */
2622           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
2623             queue_push(&solv->orphaned, i);
2624           if (!r->p)
2625             {
2626               assert(solv->dupmap_all && !sr->p);
2627               continue;
2628             }
2629           if (!solver_samerule(solv, r, sr))
2630             {
2631               /* identical rule, kill unneeded one */
2632               if (solv->allowuninstall)
2633                 {
2634                   /* keep feature rule, make it weak */
2635                   memset(r, 0, sizeof(*r));
2636                   queue_push(&solv->weakruleq, sr - solv->rules);
2637                 }
2638               else
2639                 {
2640                   /* keep update rule */
2641                   memset(sr, 0, sizeof(*sr));
2642                 }
2643             }
2644           else if (solv->allowuninstall)
2645             {
2646               /* make both feature and update rule weak */
2647               queue_push(&solv->weakruleq, r - solv->rules);
2648               queue_push(&solv->weakruleq, sr - solv->rules);
2649             }
2650           else
2651             solver_disablerule(solv, sr);
2652         }
2653       /* consistency check: we added a rule for _every_ installed solvable */
2654       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
2655     }
2656   solv->updaterules_end = solv->nrules;
2657
2658
2659   /*
2660    * now add all job rules
2661    */
2662
2663   solv->jobrules = solv->nrules;
2664   for (i = 0; i < job->count; i += 2)
2665     {
2666       oldnrules = solv->nrules;
2667
2668       how = job->elements[i];
2669       what = job->elements[i + 1];
2670       weak = how & SOLVER_WEAK;
2671       select = how & SOLVER_SELECTMASK;
2672       switch (how & SOLVER_JOBMASK)
2673         {
2674         case SOLVER_INSTALL:
2675           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2676           if (select == SOLVER_SOLVABLE)
2677             {
2678               p = what;
2679               d = 0;
2680             }
2681           else
2682             {
2683               queue_empty(&q);
2684               FOR_JOB_SELECT(p, pp, select, what)
2685                 queue_push(&q, p);
2686               if (!q.count)
2687                 {
2688                   /* no candidate found, make this an impossible rule */
2689                   queue_push(&q, -SYSTEMSOLVABLE);
2690                 }
2691               p = queue_shift(&q);      /* get first candidate */
2692               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
2693             }
2694           solver_addjobrule(solv, p, d, i, weak);
2695           break;
2696         case SOLVER_ERASE:
2697           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %s%serase %s\n", weak ? "weak " : "", how & SOLVER_CLEANDEPS ? "clean deps " : "", solver_select2str(pool, select, what));
2698           if ((how & SOLVER_CLEANDEPS) != 0 && !solv->cleandepsmap.size && solv->installed)
2699             map_grow(&solv->cleandepsmap, solv->installed->end - solv->installed->start);
2700           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
2701             {
2702               /* special case for "erase a specific solvable": we also
2703                * erase all other solvables with that name, so that they
2704                * don't get picked up as replacement */
2705               /* XXX: look also at packages that obsolete this package? */
2706               name = pool->solvables[what].name;
2707               FOR_PROVIDES(p, pp, name)
2708                 {
2709                   if (p == what)
2710                     continue;
2711                   s = pool->solvables + p;
2712                   if (s->name != name)
2713                     continue;
2714                   /* keep other versions installed */
2715                   if (s->repo == solv->installed)
2716                     continue;
2717                   /* keep installcandidates of other jobs */
2718                   if (MAPTST(&installcandidatemap, p))
2719                     continue;
2720                   solver_addjobrule(solv, -p, 0, i, weak);      /* remove by id */
2721                 }
2722             }
2723           FOR_JOB_SELECT(p, pp, select, what)
2724             solver_addjobrule(solv, -p, 0, i, weak);
2725           break;
2726
2727         case SOLVER_UPDATE:
2728           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2729           break;
2730         case SOLVER_VERIFY:
2731           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %sverify %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2732           break;
2733         case SOLVER_WEAKENDEPS:
2734           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2735           if (select != SOLVER_SOLVABLE)
2736             break;
2737           s = pool->solvables + what;
2738           weaken_solvable_deps(solv, what);
2739           break;
2740         case SOLVER_NOOBSOLETES:
2741           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2742           break;
2743         case SOLVER_LOCK:
2744           POOL_DEBUG(SOLV_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2745           FOR_JOB_SELECT(p, pp, select, what)
2746             {
2747               s = pool->solvables + p;
2748               solver_addjobrule(solv, installed && s->repo == installed ? p : -p, 0, i, weak);
2749             }
2750           break;
2751         case SOLVER_DISTUPGRADE:
2752           POOL_DEBUG(SOLV_DEBUG_JOB, "job: distupgrade %s\n", solver_select2str(pool, select, what));
2753           break;
2754         case SOLVER_DROP_ORPHANED:
2755           POOL_DEBUG(SOLV_DEBUG_JOB, "job: drop orphaned %s\n", solver_select2str(pool, select, what));
2756           if (select == SOLVER_SOLVABLE_ALL)
2757             solv->droporphanedmap_all = 1;
2758           FOR_JOB_SELECT(p, pp, select, what)
2759             {
2760               s = pool->solvables + p;
2761               if (!installed || s->repo != installed)
2762                 continue;
2763               if (!solv->droporphanedmap.size)
2764                 map_grow(&solv->droporphanedmap, installed->end - installed->start);
2765               MAPSET(&solv->droporphanedmap, p - installed->start);
2766             }
2767           break;
2768         case SOLVER_USERINSTALLED:
2769           POOL_DEBUG(SOLV_DEBUG_JOB, "job: user installed %s\n", solver_select2str(pool, select, what));
2770           break;
2771         default:
2772           POOL_DEBUG(SOLV_DEBUG_JOB, "job: unknown job\n");
2773           break;
2774         }
2775
2776         /*
2777          * debug
2778          */
2779
2780       IF_POOLDEBUG (SOLV_DEBUG_JOB)
2781         {
2782           int j;
2783           if (solv->nrules == oldnrules)
2784             POOL_DEBUG(SOLV_DEBUG_JOB, " - no rule created\n");
2785           for (j = oldnrules; j < solv->nrules; j++)
2786             {
2787               POOL_DEBUG(SOLV_DEBUG_JOB, " - job ");
2788               solver_printrule(solv, SOLV_DEBUG_JOB, solv->rules + j);
2789             }
2790         }
2791     }
2792   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
2793   solv->jobrules_end = solv->nrules;
2794
2795   /* now create infarch and dup rules */
2796   if (!solv->noinfarchcheck)
2797     {
2798       solver_addinfarchrules(solv, &addedmap);
2799       if (pool->obsoleteusescolors)
2800         {
2801           /* currently doesn't work well with infarch rules, so make
2802            * them weak */
2803           for (i = solv->infarchrules; i < solv->infarchrules_end; i++)
2804             queue_push(&solv->weakruleq, i);
2805         }
2806     }
2807   else
2808     solv->infarchrules = solv->infarchrules_end = solv->nrules;
2809
2810   if (hasdupjob)
2811     {
2812       solver_addduprules(solv, &addedmap);
2813       solver_freedupmaps(solv); /* no longer needed */
2814     }
2815   else
2816     solv->duprules = solv->duprules_end = solv->nrules;
2817
2818   if (1)
2819     solver_addchoicerules(solv);
2820   else
2821     solv->choicerules = solv->choicerules_end = solv->nrules;
2822
2823   /* all rules created
2824    * --------------------------------------------------------------
2825    * prepare for solving
2826    */
2827
2828   /* free unneeded memory */
2829   map_free(&addedmap);
2830   map_free(&installcandidatemap);
2831   queue_free(&q);
2832
2833   POOL_DEBUG(SOLV_DEBUG_STATS, "%d rpm rules, %d job rules, %d infarch rules, %d dup rules, %d choice rules\n", solv->rpmrules_end - 1, solv->jobrules_end - solv->jobrules, solv->infarchrules_end - solv->infarchrules, solv->duprules_end - solv->duprules, solv->choicerules_end - solv->choicerules);
2834
2835   /* create weak map */
2836   map_init(&solv->weakrulemap, solv->nrules);
2837   for (i = 0; i < solv->weakruleq.count; i++)
2838     {
2839       p = solv->weakruleq.elements[i];
2840       MAPSET(&solv->weakrulemap, p);
2841     }
2842
2843   /* all new rules are learnt after this point */
2844   solv->learntrules = solv->nrules;
2845
2846   /* create watches chains */
2847   makewatches(solv);
2848
2849   /* create assertion index. it is only used to speed up
2850    * makeruledecsions() a bit */
2851   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
2852     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
2853       queue_push(&solv->ruleassertions, i);
2854
2855   /* disable update rules that conflict with our job */
2856   solver_disablepolicyrules(solv);
2857
2858   /* make initial decisions based on assertion rules */
2859   makeruledecisions(solv);
2860   POOL_DEBUG(SOLV_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count);
2861
2862   /*
2863    * ********************************************
2864    * solve!
2865    * ********************************************
2866    */
2867
2868   now = solv_timems(0);
2869   solver_run_sat(solv, 1, solv->dontinstallrecommended ? 0 : 1);
2870   POOL_DEBUG(SOLV_DEBUG_STATS, "solver took %d ms\n", solv_timems(now));
2871
2872   /*
2873    * prepare solution queue if there were problems
2874    */
2875   solver_prepare_solutions(solv);
2876
2877   POOL_DEBUG(SOLV_DEBUG_STATS, "final solver statistics: %d problems, %d learned rules, %d unsolvable\n", solv->problems.count / 2, solv->stats_learned, solv->stats_unsolvable);
2878   POOL_DEBUG(SOLV_DEBUG_STATS, "solver_solve took %d ms\n", solv_timems(solve_start));
2879
2880   /* return number of problems */
2881   return solv->problems.count ? solv->problems.count / 2 : 0;
2882 }
2883
2884 Transaction *
2885 solver_create_transaction(Solver *solv)
2886 {
2887   return transaction_create_decisionq(solv->pool, &solv->decisionq, &solv->noobsoletes);
2888 }
2889
2890 void solver_get_orphaned(Solver *solv, Queue *orphanedq)
2891 {
2892   queue_free(orphanedq);
2893   queue_init_clone(orphanedq, &solv->orphaned);
2894 }
2895
2896 void solver_get_recommendations(Solver *solv, Queue *recommendationsq, Queue *suggestionsq, int noselected)
2897 {
2898   Pool *pool = solv->pool;
2899   Queue redoq, disabledq;
2900   int goterase, i;
2901   Solvable *s;
2902   Rule *r;
2903   Map obsmap;
2904
2905   if (!recommendationsq && !suggestionsq)
2906     return;
2907
2908   map_init(&obsmap, pool->nsolvables);
2909   if (solv->installed)
2910     {
2911       Id obs, *obsp, p, po, ppo;
2912       for (p = solv->installed->start; p < solv->installed->end; p++)
2913         {
2914           s = pool->solvables + p;
2915           if (s->repo != solv->installed || !s->obsoletes)
2916             continue;
2917           if (solv->decisionmap[p] <= 0)
2918             continue;
2919           if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
2920             continue;
2921           obsp = s->repo->idarraydata + s->obsoletes;
2922           /* foreach obsoletes */
2923           while ((obs = *obsp++) != 0)
2924             FOR_PROVIDES(po, ppo, obs)
2925               MAPSET(&obsmap, po);
2926         }
2927     }
2928
2929   queue_init(&redoq);
2930   queue_init(&disabledq);
2931   goterase = 0;
2932   /* disable all erase jobs (including weak "keep uninstalled" rules) */
2933   for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2934     {
2935       if (r->d < 0)     /* disabled ? */
2936         continue;
2937       if (r->p >= 0)    /* install job? */
2938         continue;
2939       queue_push(&disabledq, i);
2940       solver_disablerule(solv, r);
2941       goterase++;
2942     }
2943
2944   if (goterase)
2945     {
2946       enabledisablelearntrules(solv);
2947       removedisabledconflicts(solv, &redoq);
2948     }
2949
2950   /*
2951    * find recommended packages
2952    */
2953   if (recommendationsq)
2954     {
2955       Id rec, *recp, p, pp;
2956
2957       queue_empty(recommendationsq);
2958       /* create map of all recommened packages */
2959       solv->recommends_index = -1;
2960       MAPZERO(&solv->recommendsmap);
2961
2962       /* put all packages the solver already chose in the map */
2963       if (solv->decisioncnt_weak)
2964         {
2965           for (i = solv->decisioncnt_weak; i < solv->decisioncnt_orphan; i++)
2966             {
2967               Id why;
2968               why = solv->decisionq_why.elements[i];
2969               if (why)
2970                 continue;       /* forced by unit rule */
2971               p = solv->decisionq.elements[i];
2972               if (p < 0)
2973                 continue;
2974               MAPSET(&solv->recommendsmap, p);
2975             }
2976         }
2977
2978       for (i = 0; i < solv->decisionq.count; i++)
2979         {
2980           p = solv->decisionq.elements[i];
2981           if (p < 0)
2982             continue;
2983           s = pool->solvables + p;
2984           if (s->recommends)
2985             {
2986               recp = s->repo->idarraydata + s->recommends;
2987               while ((rec = *recp++) != 0)
2988                 {
2989                   FOR_PROVIDES(p, pp, rec)
2990                     if (solv->decisionmap[p] > 0)
2991                       break;
2992                   if (p)
2993                     {
2994                       if (!noselected)
2995                         {
2996                           FOR_PROVIDES(p, pp, rec)
2997                             if (solv->decisionmap[p] > 0)
2998                               MAPSET(&solv->recommendsmap, p);
2999                         }
3000                       continue; /* p != 0: already fulfilled */
3001                     }
3002                   FOR_PROVIDES(p, pp, rec)
3003                     MAPSET(&solv->recommendsmap, p);
3004                 }
3005             }
3006         }
3007       for (i = 1; i < pool->nsolvables; i++)
3008         {
3009           if (solv->decisionmap[i] < 0)
3010             continue;
3011           if (solv->decisionmap[i] > 0 && noselected)
3012             continue;
3013           if (MAPTST(&obsmap, i))
3014             continue;
3015           s = pool->solvables + i;
3016           if (!MAPTST(&solv->recommendsmap, i))
3017             {
3018               if (!s->supplements)
3019                 continue;
3020               if (!pool_installable(pool, s))
3021                 continue;
3022               if (!solver_is_supplementing(solv, s))
3023                 continue;
3024             }
3025           queue_push(recommendationsq, i);
3026         }
3027       /* we use MODE_SUGGEST here so that repo prio is ignored */
3028       policy_filter_unwanted(solv, recommendationsq, POLICY_MODE_SUGGEST);
3029     }
3030
3031   /*
3032    * find suggested packages
3033    */
3034
3035   if (suggestionsq)
3036     {
3037       Id sug, *sugp, p, pp;
3038
3039       queue_empty(suggestionsq);
3040       /* create map of all suggests that are still open */
3041       solv->recommends_index = -1;
3042       MAPZERO(&solv->suggestsmap);
3043       for (i = 0; i < solv->decisionq.count; i++)
3044         {
3045           p = solv->decisionq.elements[i];
3046           if (p < 0)
3047             continue;
3048           s = pool->solvables + p;
3049           if (s->suggests)
3050             {
3051               sugp = s->repo->idarraydata + s->suggests;
3052               while ((sug = *sugp++) != 0)
3053                 {
3054                   FOR_PROVIDES(p, pp, sug)
3055                     if (solv->decisionmap[p] > 0)
3056                       break;
3057                   if (p)
3058                     {
3059                       if (!noselected)
3060                         {
3061                           FOR_PROVIDES(p, pp, sug)
3062                             if (solv->decisionmap[p] > 0)
3063                               MAPSET(&solv->suggestsmap, p);
3064                         }
3065                       continue; /* already fulfilled */
3066                     }
3067                   FOR_PROVIDES(p, pp, sug)
3068                     MAPSET(&solv->suggestsmap, p);
3069                 }
3070             }
3071         }
3072       for (i = 1; i < pool->nsolvables; i++)
3073         {
3074           if (solv->decisionmap[i] < 0)
3075             continue;
3076           if (solv->decisionmap[i] > 0 && noselected)
3077             continue;
3078           if (MAPTST(&obsmap, i))
3079             continue;
3080           s = pool->solvables + i;
3081           if (!MAPTST(&solv->suggestsmap, i))
3082             {
3083               if (!s->enhances)
3084                 continue;
3085               if (!pool_installable(pool, s))
3086                 continue;
3087               if (!solver_is_enhancing(solv, s))
3088                 continue;
3089             }
3090           queue_push(suggestionsq, i);
3091         }
3092       policy_filter_unwanted(solv, suggestionsq, POLICY_MODE_SUGGEST);
3093     }
3094
3095   /* undo removedisabledconflicts */
3096   if (redoq.count)
3097     undo_removedisabledconflicts(solv, &redoq);
3098   queue_free(&redoq);
3099
3100   /* undo job rule disabling */
3101   for (i = 0; i < disabledq.count; i++)
3102     solver_enablerule(solv, solv->rules + disabledq.elements[i]);
3103   queue_free(&disabledq);
3104   map_free(&obsmap);
3105 }
3106
3107
3108 /***********************************************************************/
3109 /* disk usage computations */
3110
3111 /*-------------------------------------------------------------------
3112  *
3113  * calculate DU changes
3114  */
3115
3116 void
3117 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
3118 {
3119   Map installedmap;
3120
3121   solver_create_state_maps(solv, &installedmap, 0);
3122   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
3123   map_free(&installedmap);
3124 }
3125
3126
3127 /*-------------------------------------------------------------------
3128  *
3129  * calculate changes in install size
3130  */
3131
3132 int
3133 solver_calc_installsizechange(Solver *solv)
3134 {
3135   Map installedmap;
3136   int change;
3137
3138   solver_create_state_maps(solv, &installedmap, 0);
3139   change = pool_calc_installsizechange(solv->pool, &installedmap);
3140   map_free(&installedmap);
3141   return change;
3142 }
3143
3144 void
3145 solver_create_state_maps(Solver *solv, Map *installedmap, Map *conflictsmap)
3146 {
3147   pool_create_state_maps(solv->pool, &solv->decisionq, installedmap, conflictsmap);
3148 }
3149
3150 void
3151 solver_trivial_installable(Solver *solv, Queue *pkgs, Queue *res)
3152 {
3153   Map installedmap;
3154   pool_create_state_maps(solv->pool,  &solv->decisionq, &installedmap, 0);
3155   pool_trivial_installable_noobsoletesmap(solv->pool, &installedmap, pkgs, res, solv->noobsoletes.size ? &solv->noobsoletes : 0);
3156   map_free(&installedmap);
3157 }
3158
3159 /*-------------------------------------------------------------------
3160  *
3161  * decision introspection
3162  */
3163
3164 int
3165 solver_get_decisionlevel(Solver *solv, Id p)
3166 {
3167   return solv->decisionmap[p];
3168 }
3169
3170 void
3171 solver_get_decisionqueue(Solver *solv, Queue *decisionq)
3172 {
3173   queue_free(decisionq);
3174   queue_init_clone(decisionq, &solv->decisionq);
3175 }
3176
3177 int
3178 solver_get_lastdecisionblocklevel(Solver *solv)
3179 {
3180   Id p;
3181   if (solv->decisionq.count == 0)
3182     return 0;
3183   p = solv->decisionq.elements[solv->decisionq.count - 1];
3184   if (p < 0)
3185     p = -p;
3186   return solv->decisionmap[p] < 0 ? -solv->decisionmap[p] : solv->decisionmap[p];
3187 }
3188
3189 void
3190 solver_get_decisionblock(Solver *solv, int level, Queue *decisionq)
3191 {
3192   Id p;
3193   int i;
3194
3195   queue_empty(decisionq);
3196   for (i = 0; i < solv->decisionq.count; i++)
3197     {
3198       p = solv->decisionq.elements[i];
3199       if (p < 0)
3200         p = -p;
3201       if (solv->decisionmap[p] == level || solv->decisionmap[p] == -level)
3202         break;
3203     }
3204   if (i == solv->decisionq.count)
3205     return;
3206   for (i = 0; i < solv->decisionq.count; i++)
3207     {
3208       p = solv->decisionq.elements[i];
3209       if (p < 0)
3210         p = -p;
3211       if (solv->decisionmap[p] == level || solv->decisionmap[p] == -level)
3212         queue_push(decisionq, p);
3213       else
3214         break;
3215     }
3216 }
3217
3218 int
3219 solver_describe_decision(Solver *solv, Id p, Id *infop)
3220 {
3221   int i;
3222   Id pp, why;
3223
3224   if (infop)
3225     *infop = 0;
3226   if (!solv->decisionmap[p])
3227     return SOLVER_REASON_UNRELATED;
3228   pp = solv->decisionmap[p] < 0 ? -p : p;
3229   for (i = 0; i < solv->decisionq.count; i++)
3230     if (solv->decisionq.elements[i] == pp)
3231       break;
3232   if (i == solv->decisionq.count)       /* just in case... */
3233     return SOLVER_REASON_UNRELATED;
3234   why = solv->decisionq_why.elements[i];
3235   if (why > 0)
3236     {
3237       if (infop)
3238         *infop = why;
3239       return SOLVER_REASON_UNIT_RULE;
3240     }
3241   why = -why;
3242   if (i < solv->decisioncnt_update)
3243     {
3244       if (i == 0)
3245         {
3246           if (infop)
3247             *infop = SYSTEMSOLVABLE;
3248           return SOLVER_REASON_KEEP_INSTALLED;
3249         }
3250       if (infop)
3251         *infop = why;
3252       return SOLVER_REASON_RESOLVE_JOB;
3253     }
3254   if (i < solv->decisioncnt_keep)
3255     {
3256       if (why == 0 && pp < 0)
3257         return SOLVER_REASON_CLEANDEPS_ERASE;
3258       if (infop)
3259         {
3260           if (why >= solv->updaterules && why < solv->updaterules_end)
3261             *infop = why - solv->updaterules;
3262           else if (why >= solv->featurerules && why < solv->featurerules_end)
3263             *infop = why - solv->featurerules;
3264         }
3265       return SOLVER_REASON_UPDATE_INSTALLED;
3266     }
3267   if (i < solv->decisioncnt_resolve)
3268     {
3269       if (why == 0 && pp < 0)
3270         return SOLVER_REASON_CLEANDEPS_ERASE;
3271       if (infop)
3272         {
3273           if (why >= solv->updaterules && why < solv->updaterules_end)
3274             *infop = why - solv->updaterules;
3275           else if (why >= solv->featurerules && why < solv->featurerules_end)
3276             *infop = why - solv->featurerules;
3277         }
3278       return SOLVER_REASON_KEEP_INSTALLED;
3279     }
3280   if (i < solv->decisioncnt_weak)
3281     {
3282       if (infop)
3283         *infop = why;
3284       return SOLVER_REASON_RESOLVE;
3285     }
3286   if (solv->decisionq.count < solv->decisioncnt_orphan)
3287     return SOLVER_REASON_WEAKDEP;
3288   return SOLVER_REASON_RESOLVE_ORPHAN;
3289 }
3290
3291
3292 void
3293 solver_describe_weakdep_decision(Solver *solv, Id p, Queue *whyq)
3294 {
3295   Pool *pool = solv->pool;
3296   int i;
3297   int level = solv->decisionmap[p];
3298   int decisionno;
3299   Solvable *s;
3300
3301   queue_empty(whyq);
3302   if (level < 0)
3303     return;     /* huh? */
3304   for (decisionno = 0; decisionno < solv->decisionq.count; decisionno++)
3305     if (solv->decisionq.elements[decisionno] == p)
3306       break;
3307   if (decisionno == solv->decisionq.count)
3308     return;     /* huh? */
3309   if (decisionno < solv->decisioncnt_weak || decisionno >= solv->decisioncnt_orphan)
3310     return;     /* huh? */
3311
3312   /* 1) list all packages that recommend us */
3313   for (i = 1; i < pool->nsolvables; i++)
3314     {
3315       Id *recp, rec, pp2, p2;
3316       if (solv->decisionmap[i] < 0 || solv->decisionmap[i] >= level)
3317         continue;
3318       s = pool->solvables + i;
3319       if (!s->recommends)
3320         continue;
3321       if (solv->ignorealreadyrecommended && s->repo == solv->installed)
3322         continue;
3323       recp = s->repo->idarraydata + s->recommends;
3324       while ((rec = *recp++) != 0)
3325         {
3326           int found = 0;
3327           FOR_PROVIDES(p2, pp2, rec)
3328             {
3329               if (p2 == p)
3330                 found = 1;
3331               else
3332                 {
3333                   /* if p2 is already installed, this recommends is ignored */
3334                   if (solv->decisionmap[p2] > 0 && solv->decisionmap[p2] < level)
3335                     break;
3336                 }
3337             }
3338           if (!p2 && found)
3339             {
3340               queue_push(whyq, SOLVER_REASON_RECOMMENDED);
3341               queue_push2(whyq, p2, rec);
3342             }
3343         }
3344     }
3345   /* 2) list all supplements */
3346   s = pool->solvables + p;
3347   if (s->supplements && level > 0)
3348     {
3349       Id *supp, sup, pp2, p2;
3350       /* this is a hack. to use solver_dep_fulfilled we temporarily clear
3351        * everything above our level in the decisionmap */
3352       for (i = decisionno; i < solv->decisionq.count; i++ )
3353         {
3354           p2 = solv->decisionq.elements[i];
3355           if (p2 > 0)
3356             solv->decisionmap[p2] = -solv->decisionmap[p2];
3357         }
3358       supp = s->repo->idarraydata + s->supplements;
3359       while ((sup = *supp++) != 0)
3360         if (solver_dep_fulfilled(solv, sup))
3361           {
3362             int found = 0;
3363             /* let's see if this is an easy supp */
3364             FOR_PROVIDES(p2, pp2, sup)
3365               {
3366                 if (solv->ignorealreadyrecommended && solv->installed)
3367                   {
3368                     if (pool->solvables[p2].repo == solv->installed)
3369                       continue;
3370                   }
3371                 if (solv->decisionmap[p2] > 0 && solv->decisionmap[p2] < level)
3372                   {
3373                     queue_push(whyq, SOLVER_REASON_SUPPLEMENTED);
3374                     queue_push2(whyq, p2, sup);
3375                     found = 1;
3376                   }
3377               }
3378             if (!found)
3379               {
3380                 /* hard case, just note dependency with no package */
3381                 queue_push(whyq, SOLVER_REASON_SUPPLEMENTED);
3382                 queue_push2(whyq, 0, sup);
3383               }
3384           }
3385       for (i = decisionno; i < solv->decisionq.count; i++)
3386         {
3387           p2 = solv->decisionq.elements[i];
3388           if (p2 > 0)
3389             solv->decisionmap[p2] = -solv->decisionmap[p2];
3390         }
3391     }
3392 }