src/solver.c

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