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