src/solver.c

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