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 + 1));
 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 + 1));
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               queue_free(&dq);
1411               queue_free(&dqs);
1412               return;
1413             }
1414         }
1415
1416       /*
1417        * resolve jobs first
1418        */
1419      if (level < systemlevel)
1420         {
1421           POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving job rules\n");
1422           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
1423             {
1424               Id l;
1425               if (r->d < 0)             /* ignore disabled rules */
1426                 continue;
1427               queue_empty(&dq);
1428               FOR_RULELITERALS(l, dp, r)
1429                 {
1430                   if (l < 0)
1431                     {
1432                       if (solv->decisionmap[-l] <= 0)
1433                         break;
1434                     }
1435                   else
1436                     {
1437                       if (solv->decisionmap[l] > 0)
1438                         break;
1439                       if (solv->decisionmap[l] == 0)
1440                         queue_push(&dq, l);
1441                     }
1442                 }
1443               if (l || !dq.count)
1444                 continue;
1445               /* prune to installed if not updating */
1446               if (dq.count > 1 && solv->installed && !solv->updatemap_all)
1447                 {
1448                   int j, k;
1449                   for (j = k = 0; j < dq.count; j++)
1450                     {
1451                       Solvable *s = pool->solvables + dq.elements[j];
1452                       if (s->repo == solv->installed)
1453                         {
1454                           dq.elements[k++] = dq.elements[j];
1455                           if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start))
1456                             {
1457                               k = 0;    /* package wants to be updated, do not prune */
1458                               break;
1459                             }
1460                         }
1461                     }
1462                   if (k)
1463                     dq.count = k;
1464                 }
1465               olevel = level;
1466               level = selectandinstall(solv, level, &dq, disablerules, i);
1467               if (level == 0)
1468                 {
1469                   queue_free(&dq);
1470                   queue_free(&dqs);
1471                   return;
1472                 }
1473               if (level <= olevel)
1474                 break;
1475             }
1476           systemlevel = level + 1;
1477           if (i < solv->jobrules_end)
1478             continue;
1479         }
1480
1481
1482       /*
1483        * installed packages
1484        */
1485       if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled)
1486         {
1487           Repo *installed = solv->installed;
1488           int pass;
1489
1490           POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n");
1491           /* we use two passes if we need to update packages
1492            * to create a better user experience */
1493           for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
1494             {
1495               int passlevel = level;
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                         {
1601                           queue_free(&dq);
1602                           queue_free(&dqs);
1603                           return;
1604                         }
1605                       if (level <= olevel)
1606                         {
1607                           if (level == 1 || level < passlevel)
1608                             break;      /* trouble */
1609                           if (level < olevel)
1610                             n = installed->start;       /* redo all */
1611                           i--;
1612                           n--;
1613                           continue; /* retry with learnt rule */
1614                         }
1615                     }
1616                 }
1617               if (n < installed->end)
1618                 {
1619                   installedpos = i;     /* retry problem solvable next time */
1620                   break;                /* ran into trouble */
1621                 }
1622               installedpos = installed->start;  /* reset installedpos */
1623             }
1624           systemlevel = level + 1;
1625           if (pass < 2)
1626             continue;           /* had trouble, retry */
1627         }
1628
1629       if (level < systemlevel)
1630         systemlevel = level;
1631
1632       /*
1633        * decide
1634        */
1635       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
1636       for (i = 1, n = 1; n < solv->nrules; i++, n++)
1637         {
1638           if (i == solv->nrules)
1639             i = 1;
1640           r = solv->rules + i;
1641           if (r->d < 0)         /* ignore disabled rules */
1642             continue;
1643           queue_empty(&dq);
1644           if (r->d == 0)
1645             {
1646               /* binary or unary rule */
1647               /* need two positive undecided literals */
1648               if (r->p < 0 || r->w2 <= 0)
1649                 continue;
1650               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
1651                 continue;
1652               queue_push(&dq, r->p);
1653               queue_push(&dq, r->w2);
1654             }
1655           else
1656             {
1657               /* make sure that
1658                * all negative literals are installed
1659                * no positive literal is installed
1660                * i.e. the rule is not fulfilled and we
1661                * just need to decide on the positive literals
1662                */
1663               if (r->p < 0)
1664                 {
1665                   if (solv->decisionmap[-r->p] <= 0)
1666                     continue;
1667                 }
1668               else
1669                 {
1670                   if (solv->decisionmap[r->p] > 0)
1671                     continue;
1672                   if (solv->decisionmap[r->p] == 0)
1673                     queue_push(&dq, r->p);
1674                 }
1675               dp = pool->whatprovidesdata + r->d;
1676               while ((p = *dp++) != 0)
1677                 {
1678                   if (p < 0)
1679                     {
1680                       if (solv->decisionmap[-p] <= 0)
1681                         break;
1682                     }
1683                   else
1684                     {
1685                       if (solv->decisionmap[p] > 0)
1686                         break;
1687                       if (solv->decisionmap[p] == 0)
1688                         queue_push(&dq, p);
1689                     }
1690                 }
1691               if (p)
1692                 continue;
1693             }
1694           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1695             {
1696               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
1697               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
1698             }
1699           /* dq.count < 2 cannot happen as this means that
1700            * the rule is unit */
1701           assert(dq.count > 1);
1702
1703           olevel = level;
1704           level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules);
1705           if (level == 0)
1706             {
1707               queue_free(&dq);
1708               queue_free(&dqs);
1709               return;
1710             }
1711           if (level < systemlevel || level == 1)
1712             break;              /* trouble */
1713           /* something changed, so look at all rules again */
1714           n = 0;
1715         }
1716
1717       if (n != solv->nrules)    /* ran into trouble, restart */
1718         continue;
1719
1720       /* at this point we have a consistent system. now do the extras... */
1721
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                   continue;     /* back to main loop */
1895                 }
1896
1897               /* filter packages, this gives us the best versions */
1898               policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
1899
1900               /* create map of result */
1901               map_init(&dqmap, pool->nsolvables);
1902               for (i = 0; i < dq.count; i++)
1903                 MAPSET(&dqmap, dq.elements[i]);
1904
1905               /* install all supplemented packages */
1906               for (i = 0; i < dqs.count; i++)
1907                 {
1908                   p = dqs.elements[i];
1909                   if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
1910                     continue;
1911                   POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", pool_solvid2str(pool, p));
1912                   queue_push(&solv->recommendations, p);
1913                   olevel = level;
1914                   level = setpropagatelearn(solv, level, p, 0, 0);
1915                   if (level <= olevel)
1916                     break;
1917                 }
1918               if (i < dqs.count || solv->decisionq.count < decisioncount)
1919                 {
1920                   map_free(&dqmap);
1921                   continue;
1922                 }
1923
1924               /* install all recommended packages */
1925               /* more work as we want to created branches if multiple
1926                * choices are valid */
1927               for (i = 0; i < decisioncount; i++)
1928                 {
1929                   Id rec, *recp, pp;
1930                   p = solv->decisionq.elements[i];
1931                   if (p < 0)
1932                     continue;
1933                   s = pool->solvables + p;
1934                   if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
1935                     continue;
1936                   if (!s->recommends)
1937                     continue;
1938                   recp = s->repo->idarraydata + s->recommends;
1939                   while ((rec = *recp++) != 0)
1940                     {
1941                       queue_empty(&dq);
1942                       FOR_PROVIDES(p, pp, rec)
1943                         {
1944                           if (solv->decisionmap[p] > 0)
1945                             {
1946                               dq.count = 0;
1947                               break;
1948                             }
1949                           else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
1950                             queue_pushunique(&dq, p);
1951                         }
1952                       if (!dq.count)
1953                         continue;
1954                       if (dq.count > 1)
1955                         {
1956                           /* multiple candidates, open a branch */
1957                           for (i = 1; i < dq.count; i++)
1958                             queue_push(&solv->branches, dq.elements[i]);
1959                           queue_push(&solv->branches, -level);
1960                         }
1961                       p = dq.elements[0];
1962                       POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", pool_solvid2str(pool, p));
1963                       queue_push(&solv->recommendations, p);
1964                       olevel = level;
1965                       level = setpropagatelearn(solv, level, p, 0, 0);
1966                       if (level <= olevel || solv->decisionq.count < decisioncount)
1967                         break;  /* we had to revert some decisions */
1968                     }
1969                   if (rec)
1970                     break;      /* had a problem above, quit loop */
1971                 }
1972               map_free(&dqmap);
1973
1974               continue;         /* back to main loop so that all deps are checked */
1975             }
1976         }
1977
1978      if (solv->dupmap_all && solv->installed)
1979         {
1980           int installedone = 0;
1981
1982           /* let's see if we can install some unsupported package */
1983           POOL_DEBUG(SAT_DEBUG_SOLVER, "deciding orphaned packages\n");
1984           for (i = 0; i < solv->orphaned.count; i++)
1985             {
1986               p = solv->orphaned.elements[i];
1987               if (solv->decisionmap[p])
1988                 continue;       /* already decided */
1989               olevel = level;
1990               if (solv->droporphanedmap_all)
1991                 continue;
1992               if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))
1993                 continue;
1994               POOL_DEBUG(SAT_DEBUG_SOLVER, "keeping orphaned %s\n", pool_solvid2str(pool, p));
1995               level = setpropagatelearn(solv, level, p, 0, 0);
1996               installedone = 1;
1997               if (level < olevel)
1998                 break;
1999             }
2000           if (installedone || i < solv->orphaned.count)
2001             continue;           /* back to main loop */
2002           for (i = 0; i < solv->orphaned.count; i++)
2003             {
2004               p = solv->orphaned.elements[i];
2005               if (solv->decisionmap[p])
2006                 continue;       /* already decided */
2007               POOL_DEBUG(SAT_DEBUG_SOLVER, "removing orphaned %s\n", pool_solvid2str(pool, p));
2008               olevel = level;
2009               level = setpropagatelearn(solv, level, -p, 0, 0);
2010               if (level < olevel)
2011                 break;
2012             }
2013           if (i < solv->orphaned.count)
2014             continue;           /* back to main loop */
2015         }
2016
2017      if (solv->solution_callback)
2018         {
2019           solv->solution_callback(solv, solv->solution_callback_data);
2020           if (solv->branches.count)
2021             {
2022               int i = solv->branches.count - 1;
2023               int l = -solv->branches.elements[i];
2024               Id why;
2025
2026               for (; i > 0; i--)
2027                 if (solv->branches.elements[i - 1] < 0)
2028                   break;
2029               p = solv->branches.elements[i];
2030               POOL_DEBUG(SAT_DEBUG_SOLVER, "branching with %s\n", pool_solvid2str(pool, p));
2031               queue_empty(&dq);
2032               for (j = i + 1; j < solv->branches.count; j++)
2033                 queue_push(&dq, solv->branches.elements[j]);
2034               solv->branches.count = i;
2035               level = l;
2036               revert(solv, level);
2037               if (dq.count > 1)
2038                 for (j = 0; j < dq.count; j++)
2039                   queue_push(&solv->branches, dq.elements[j]);
2040               olevel = level;
2041               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2042               assert(why >= 0);
2043               level = setpropagatelearn(solv, level, p, disablerules, why);
2044               if (level == 0)
2045                 {
2046                   queue_free(&dq);
2047                   queue_free(&dqs);
2048                   return;
2049                 }
2050               continue;
2051             }
2052           /* all branches done, we're finally finished */
2053           break;
2054         }
2055
2056       /* minimization step */
2057      if (solv->branches.count)
2058         {
2059           int l = 0, lasti = -1, lastl = -1;
2060           Id why;
2061
2062           p = 0;
2063           for (i = solv->branches.count - 1; i >= 0; i--)
2064             {
2065               p = solv->branches.elements[i];
2066               if (p < 0)
2067                 l = -p;
2068               else if (p > 0 && solv->decisionmap[p] > l + 1)
2069                 {
2070                   lasti = i;
2071                   lastl = l;
2072                 }
2073             }
2074           if (lasti >= 0)
2075             {
2076               /* kill old solvable so that we do not loop */
2077               p = solv->branches.elements[lasti];
2078               solv->branches.elements[lasti] = 0;
2079               POOL_DEBUG(SAT_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, pool_solvid2str(pool, p));
2080               minimizationsteps++;
2081
2082               level = lastl;
2083               revert(solv, level);
2084               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2085               assert(why >= 0);
2086               olevel = level;
2087               level = setpropagatelearn(solv, level, p, disablerules, why);
2088               if (level == 0)
2089                 {
2090                   queue_free(&dq);
2091                   queue_free(&dqs);
2092                   return;
2093                 }
2094               continue;         /* back to main loop */
2095             }
2096         }
2097       /* no minimization found, we're finally finished! */
2098       break;
2099     }
2100
2101   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
2102
2103   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2104   queue_free(&dq);
2105   queue_free(&dqs);
2106 #if 0
2107   solver_printdecisionq(solv, SAT_DEBUG_RESULT);
2108 #endif
2109 }
2110
2111
2112 /*-------------------------------------------------------------------
2113  *
2114  * remove disabled conflicts
2115  *
2116  * purpose: update the decisionmap after some rules were disabled.
2117  * this is used to calculate the suggested/recommended package list.
2118  * Also returns a "removed" list to undo the discisionmap changes.
2119  */
2120
2121 static void
2122 removedisabledconflicts(Solver *solv, Queue *removed)
2123 {
2124   Pool *pool = solv->pool;
2125   int i, n;
2126   Id p, why, *dp;
2127   Id new;
2128   Rule *r;
2129   Id *decisionmap = solv->decisionmap;
2130
2131   queue_empty(removed);
2132   for (i = 0; i < solv->decisionq.count; i++)
2133     {
2134       p = solv->decisionq.elements[i];
2135       if (p > 0)
2136         continue;       /* conflicts only, please */
2137       why = solv->decisionq_why.elements[i];
2138       if (why == 0)
2139         {
2140           /* no rule involved, must be a orphan package drop */
2141           continue;
2142         }
2143       /* we never do conflicts on free decisions, so there
2144        * must have been an unit rule */
2145       assert(why > 0);
2146       r = solv->rules + why;
2147       if (r->d < 0 && decisionmap[-p])
2148         {
2149           /* rule is now disabled, remove from decisionmap */
2150           POOL_DEBUG(SAT_DEBUG_SOLVER, "removing conflict for package %s[%d]\n", pool_solvid2str(pool, -p), -p);
2151           queue_push(removed, -p);
2152           queue_push(removed, decisionmap[-p]);
2153           decisionmap[-p] = 0;
2154         }
2155     }
2156   if (!removed->count)
2157     return;
2158   /* we removed some confliced packages. some of them might still
2159    * be in conflict, so search for unit rules and re-conflict */
2160   new = 0;
2161   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
2162     {
2163       if (i == solv->nrules)
2164         {
2165           i = 1;
2166           r = solv->rules + i;
2167         }
2168       if (r->d < 0)
2169         continue;
2170       if (!r->w2)
2171         {
2172           if (r->p < 0 && !decisionmap[-r->p])
2173             new = r->p;
2174         }
2175       else if (!r->d)
2176         {
2177           /* binary rule */
2178           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
2179             new = r->p;
2180           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
2181             new = r->w2;
2182         }
2183       else
2184         {
2185           if (r->p < 0 && decisionmap[-r->p] == 0)
2186             new = r->p;
2187           if (new || DECISIONMAP_FALSE(r->p))
2188             {
2189               dp = pool->whatprovidesdata + r->d;
2190               while ((p = *dp++) != 0)
2191                 {
2192                   if (new && p == new)
2193                     continue;
2194                   if (p < 0 && decisionmap[-p] == 0)
2195                     {
2196                       if (new)
2197                         {
2198                           new = 0;
2199                           break;
2200                         }
2201                       new = p;
2202                     }
2203                   else if (!DECISIONMAP_FALSE(p))
2204                     {
2205                       new = 0;
2206                       break;
2207                     }
2208                 }
2209             }
2210         }
2211       if (new)
2212         {
2213           POOL_DEBUG(SAT_DEBUG_SOLVER, "re-conflicting package %s[%d]\n", pool_solvid2str(pool, -new), -new);
2214           decisionmap[-new] = -1;
2215           new = 0;
2216           n = 0;        /* redo all rules */
2217         }
2218     }
2219 }
2220
2221 static inline void
2222 undo_removedisabledconflicts(Solver *solv, Queue *removed)
2223 {
2224   int i;
2225   for (i = 0; i < removed->count; i += 2)
2226     solv->decisionmap[removed->elements[i]] = removed->elements[i + 1];
2227 }
2228
2229
2230 /*-------------------------------------------------------------------
2231  *
2232  * weaken solvable dependencies
2233  */
2234
2235 static void
2236 weaken_solvable_deps(Solver *solv, Id p)
2237 {
2238   int i;
2239   Rule *r;
2240
2241   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
2242     {
2243       if (r->p != -p)
2244         continue;
2245       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
2246         continue;       /* conflict */
2247       queue_push(&solv->weakruleq, i);
2248     }
2249 }
2250
2251
2252 /********************************************************************/
2253 /* main() */
2254
2255
2256 static void
2257 findrecommendedsuggested(Solver *solv)
2258 {
2259   Pool *pool = solv->pool;
2260   Queue redoq, disabledq;
2261   int goterase, i;
2262   Solvable *s;
2263   Rule *r;
2264   Map obsmap;
2265
2266   map_init(&obsmap, pool->nsolvables);
2267   if (solv->installed)
2268     {
2269       Id obs, *obsp, p, po, ppo;
2270       for (p = solv->installed->start; p < solv->installed->end; p++)
2271         {
2272           s = pool->solvables + p;
2273           if (s->repo != solv->installed || !s->obsoletes)
2274             continue;
2275           if (solv->decisionmap[p] <= 0)
2276             continue;
2277           if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
2278             continue;
2279           obsp = s->repo->idarraydata + s->obsoletes;
2280           /* foreach obsoletes */
2281           while ((obs = *obsp++) != 0)
2282             FOR_PROVIDES(po, ppo, obs)
2283               MAPSET(&obsmap, po);
2284         }
2285     }
2286
2287   queue_init(&redoq);
2288   queue_init(&disabledq);
2289   goterase = 0;
2290   /* disable all erase jobs (including weak "keep uninstalled" rules) */
2291   for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2292     {
2293       if (r->d < 0)     /* disabled ? */
2294         continue;
2295       if (r->p >= 0)    /* install job? */
2296         continue;
2297       queue_push(&disabledq, i);
2298       solver_disablerule(solv, r);
2299       goterase++;
2300     }
2301
2302   if (goterase)
2303     {
2304       enabledisablelearntrules(solv);
2305       removedisabledconflicts(solv, &redoq);
2306     }
2307
2308   /*
2309    * find recommended packages
2310    */
2311
2312   /* if redoq.count == 0 we already found all recommended in the
2313    * solver run */
2314   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
2315     {
2316       Id rec, *recp, p, pp;
2317
2318       /* create map of all recommened packages */
2319       solv->recommends_index = -1;
2320       MAPZERO(&solv->recommendsmap);
2321       for (i = 0; i < solv->decisionq.count; i++)
2322         {
2323           p = solv->decisionq.elements[i];
2324           if (p < 0)
2325             continue;
2326           s = pool->solvables + p;
2327           if (s->recommends)
2328             {
2329               recp = s->repo->idarraydata + s->recommends;
2330               while ((rec = *recp++) != 0)
2331                 {
2332                   FOR_PROVIDES(p, pp, rec)
2333                     if (solv->decisionmap[p] > 0)
2334                       break;
2335                   if (p)
2336                     {
2337                       if (!solv->dontshowinstalledrecommended)
2338                         {
2339                           FOR_PROVIDES(p, pp, rec)
2340                             if (solv->decisionmap[p] > 0)
2341                               MAPSET(&solv->recommendsmap, p);
2342                         }
2343                       continue; /* p != 0: already fulfilled */
2344                     }
2345                   FOR_PROVIDES(p, pp, rec)
2346                     MAPSET(&solv->recommendsmap, p);
2347                 }
2348             }
2349         }
2350       for (i = 1; i < pool->nsolvables; i++)
2351         {
2352           if (solv->decisionmap[i] < 0)
2353             continue;
2354           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
2355             continue;
2356           if (MAPTST(&obsmap, i))
2357             continue;
2358           s = pool->solvables + i;
2359           if (!MAPTST(&solv->recommendsmap, i))
2360             {
2361               if (!s->supplements)
2362                 continue;
2363               if (!pool_installable(pool, s))
2364                 continue;
2365               if (!solver_is_supplementing(solv, s))
2366                 continue;
2367             }
2368           if (solv->dontinstallrecommended)
2369             queue_push(&solv->recommendations, i);
2370           else
2371             queue_pushunique(&solv->recommendations, i);
2372         }
2373       /* we use MODE_SUGGEST here so that repo prio is ignored */
2374       policy_filter_unwanted(solv, &solv->recommendations, POLICY_MODE_SUGGEST);
2375     }
2376
2377   /*
2378    * find suggested packages
2379    */
2380
2381   if (1)
2382     {
2383       Id sug, *sugp, p, pp;
2384
2385       /* create map of all suggests that are still open */
2386       solv->recommends_index = -1;
2387       MAPZERO(&solv->suggestsmap);
2388       for (i = 0; i < solv->decisionq.count; i++)
2389         {
2390           p = solv->decisionq.elements[i];
2391           if (p < 0)
2392             continue;
2393           s = pool->solvables + p;
2394           if (s->suggests)
2395             {
2396               sugp = s->repo->idarraydata + s->suggests;
2397               while ((sug = *sugp++) != 0)
2398                 {
2399                   FOR_PROVIDES(p, pp, sug)
2400                     if (solv->decisionmap[p] > 0)
2401                       break;
2402                   if (p)
2403                     {
2404                       if (!solv->dontshowinstalledrecommended)
2405                         {
2406                           FOR_PROVIDES(p, pp, sug)
2407                             if (solv->decisionmap[p] > 0)
2408                               MAPSET(&solv->suggestsmap, p);
2409                         }
2410                       continue; /* already fulfilled */
2411                     }
2412                   FOR_PROVIDES(p, pp, sug)
2413                     MAPSET(&solv->suggestsmap, p);
2414                 }
2415             }
2416         }
2417       for (i = 1; i < pool->nsolvables; i++)
2418         {
2419           if (solv->decisionmap[i] < 0)
2420             continue;
2421           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
2422             continue;
2423           if (MAPTST(&obsmap, i))
2424             continue;
2425           s = pool->solvables + i;
2426           if (!MAPTST(&solv->suggestsmap, i))
2427             {
2428               if (!s->enhances)
2429                 continue;
2430               if (!pool_installable(pool, s))
2431                 continue;
2432               if (!solver_is_enhancing(solv, s))
2433                 continue;
2434             }
2435           queue_push(&solv->suggestions, i);
2436         }
2437       policy_filter_unwanted(solv, &solv->suggestions, POLICY_MODE_SUGGEST);
2438     }
2439
2440   /* undo removedisabledconflicts */
2441   if (redoq.count)
2442     undo_removedisabledconflicts(solv, &redoq);
2443   queue_free(&redoq);
2444
2445   /* undo job rule disabling */
2446   for (i = 0; i < disabledq.count; i++)
2447     solver_enablerule(solv, solv->rules + disabledq.elements[i]);
2448   queue_free(&disabledq);
2449   map_free(&obsmap);
2450 }
2451
2452 void
2453 solver_calculate_noobsmap(Pool *pool, Queue *job, Map *noobsmap)
2454 {
2455   int i;
2456   Id how, what, select;
2457   Id p, pp;
2458   for (i = 0; i < job->count; i += 2)
2459     {
2460       how = job->elements[i];
2461       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
2462         continue;
2463       what = job->elements[i + 1];
2464       select = how & SOLVER_SELECTMASK;
2465       if (!noobsmap->size)
2466         map_grow(noobsmap, pool->nsolvables);
2467       FOR_JOB_SELECT(p, pp, select, what)
2468         MAPSET(noobsmap, p);
2469     }
2470 }
2471
2472 /*
2473  * add a rule created by a job, record job number and weak flag
2474  */
2475 static inline void
2476 solver_addjobrule(Solver *solv, Id p, Id d, Id job, int weak)
2477 {
2478   solver_addrule(solv, p, d);
2479   queue_push(&solv->ruletojob, job);
2480   if (weak)
2481     queue_push(&solv->weakruleq, solv->nrules - 1);
2482 }
2483
2484 /*
2485  *
2486  * solve job queue
2487  *
2488  */
2489
2490 int
2491 solver_solve(Solver *solv, Queue *job)
2492 {
2493   Pool *pool = solv->pool;
2494   Repo *installed = solv->installed;
2495   int i;
2496   int oldnrules;
2497   Map addedmap;                /* '1' == have rpm-rules for solvable */
2498   Map installcandidatemap;
2499   Id how, what, select, name, weak, p, pp, d;
2500   Queue q;
2501   Solvable *s;
2502   Rule *r;
2503   int now, solve_start;
2504   int hasdupjob = 0;
2505
2506   solve_start = sat_timems(0);
2507
2508   /* log solver options */
2509   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
2510   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);
2511   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
2512   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
2513   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, allowselfconflicts=%d\n", pool->promoteepoch, pool->allowselfconflicts);
2514   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d, obsoleteusescolors=%d\n", pool->obsoleteusesprovides, pool->implicitobsoleteusesprovides, pool->obsoleteusescolors);
2515   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
2516
2517   /* create whatprovides if not already there */
2518   if (!pool->whatprovides)
2519     pool_createwhatprovides(pool);
2520
2521   /* create obsolete index */
2522   policy_create_obsolete_index(solv);
2523
2524   /* remember job */
2525   queue_free(&solv->job);
2526   queue_init_clone(&solv->job, job);
2527
2528   /* initialize with legacy values */
2529   solv->fixmap_all = solv->fixsystem;
2530   solv->updatemap_all = solv->updatesystem;
2531   solv->droporphanedmap_all = solv->distupgrade_removeunsupported;
2532   solv->dupmap_all = solv->distupgrade;
2533
2534   /*
2535    * create basic rule set of all involved packages
2536    * use addedmap bitmap to make sure we don't create rules twice
2537    */
2538
2539   /* create noobsolete map if needed */
2540   solver_calculate_noobsmap(pool, job, &solv->noobsoletes);
2541
2542   map_init(&addedmap, pool->nsolvables);
2543   MAPSET(&addedmap, SYSTEMSOLVABLE);
2544
2545   map_init(&installcandidatemap, pool->nsolvables);
2546   queue_init(&q);
2547
2548   now = sat_timems(0);
2549   /*
2550    * create rules for all package that could be involved with the solving
2551    * so called: rpm rules
2552    *
2553    */
2554   if (installed)
2555     {
2556       /* check for update/verify jobs as they need to be known early */
2557       for (i = 0; i < job->count; i += 2)
2558         {
2559           how = job->elements[i];
2560           what = job->elements[i + 1];
2561           select = how & SOLVER_SELECTMASK;
2562           switch (how & SOLVER_JOBMASK)
2563             {
2564             case SOLVER_VERIFY:
2565               if (select == SOLVER_SOLVABLE_ALL)
2566                 solv->fixmap_all = 1;
2567               FOR_JOB_SELECT(p, pp, select, what)
2568                 {
2569                   s = pool->solvables + p;
2570                   if (!solv->installed || s->repo != solv->installed)
2571                     continue;
2572                   if (!solv->fixmap.size)
2573                     map_grow(&solv->fixmap, solv->installed->end - solv->installed->start);
2574                   MAPSET(&solv->fixmap, p - solv->installed->start);
2575                 }
2576               break;
2577             case SOLVER_UPDATE:
2578               if (select == SOLVER_SOLVABLE_ALL)
2579                 solv->updatemap_all = 1;
2580               FOR_JOB_SELECT(p, pp, select, what)
2581                 {
2582                   s = pool->solvables + p;
2583                   if (!solv->installed || s->repo != solv->installed)
2584                     continue;
2585                   if (!solv->updatemap.size)
2586                     map_grow(&solv->updatemap, solv->installed->end - solv->installed->start);
2587                   MAPSET(&solv->updatemap, p - solv->installed->start);
2588                 }
2589               break;
2590             default:
2591               break;
2592             }
2593         }
2594
2595       oldnrules = solv->nrules;
2596       FOR_REPO_SOLVABLES(installed, p, s)
2597         solver_addrpmrulesforsolvable(solv, s, &addedmap);
2598       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
2599       oldnrules = solv->nrules;
2600       FOR_REPO_SOLVABLES(installed, p, s)
2601         solver_addrpmrulesforupdaters(solv, s, &addedmap, 1);
2602       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
2603     }
2604
2605   /*
2606    * create rules for all packages involved in the job
2607    * (to be installed or removed)
2608    */
2609
2610   oldnrules = solv->nrules;
2611   for (i = 0; i < job->count; i += 2)
2612     {
2613       how = job->elements[i];
2614       what = job->elements[i + 1];
2615       select = how & SOLVER_SELECTMASK;
2616
2617       switch (how & SOLVER_JOBMASK)
2618         {
2619         case SOLVER_INSTALL:
2620           FOR_JOB_SELECT(p, pp, select, what)
2621             {
2622               MAPSET(&installcandidatemap, p);
2623               solver_addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
2624             }
2625           break;
2626         case SOLVER_DISTUPGRADE:
2627           if (select == SOLVER_SOLVABLE_ALL)
2628             {
2629               solv->dupmap_all = 1;
2630               solv->updatemap_all = 1;
2631             }
2632           if (!solv->dupmap_all)
2633             hasdupjob = 1;
2634           break;
2635         default:
2636           break;
2637         }
2638     }
2639   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
2640
2641
2642   /*
2643    * add rules for suggests, enhances
2644    */
2645   oldnrules = solv->nrules;
2646   solver_addrpmrulesforweak(solv, &addedmap);
2647   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
2648
2649   /*
2650    * first pass done, we now have all the rpm rules we need.
2651    * unify existing rules before going over all job rules and
2652    * policy rules.
2653    * at this point the system is always solvable,
2654    * as an empty system (remove all packages) is a valid solution
2655    */
2656
2657   IF_POOLDEBUG (SAT_DEBUG_STATS)
2658     {
2659       int possible = 0, installable = 0;
2660       for (i = 1; i < pool->nsolvables; i++)
2661         {
2662           if (pool_installable(pool, pool->solvables + i))
2663             installable++;
2664           if (MAPTST(&addedmap, i))
2665             possible++;
2666         }
2667       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
2668     }
2669
2670   solver_unifyrules(solv);                          /* remove duplicate rpm rules */
2671   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
2672
2673   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
2674   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
2675
2676   /* create dup maps if needed. We need the maps early to create our
2677    * update rules */
2678   if (hasdupjob)
2679     solver_createdupmaps(solv);
2680
2681   /*
2682    * create feature rules
2683    *
2684    * foreach installed:
2685    *   create assertion (keep installed, if no update available)
2686    *   or
2687    *   create update rule (A|update1(A)|update2(A)|...)
2688    *
2689    * those are used later on to keep a version of the installed packages in
2690    * best effort mode
2691    */
2692
2693   solv->featurerules = solv->nrules;              /* mark start of feature rules */
2694   if (installed)
2695     {
2696       /* foreach possibly installed solvable */
2697       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2698         {
2699           if (s->repo != installed)
2700             {
2701               solver_addrule(solv, 0, 0);       /* create dummy rule */
2702               continue;
2703             }
2704           solver_addupdaterule(solv, s, 1);    /* allow s to be updated */
2705         }
2706       /* make sure we accounted for all rules */
2707       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
2708     }
2709   solv->featurerules_end = solv->nrules;
2710
2711     /*
2712      * Add update rules for installed solvables
2713      *
2714      * almost identical to feature rules
2715      * except that downgrades/archchanges/vendorchanges are not allowed
2716      */
2717
2718   solv->updaterules = solv->nrules;
2719
2720   if (installed)
2721     { /* foreach installed solvables */
2722       /* we create all update rules, but disable some later on depending on the job */
2723       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2724         {
2725           Rule *sr;
2726
2727           if (s->repo != installed)
2728             {
2729               solver_addrule(solv, 0, 0);       /* create dummy rule */
2730               continue;
2731             }
2732           solver_addupdaterule(solv, s, 0);     /* allowall = 0: downgrades not allowed */
2733           /*
2734            * check for and remove duplicate
2735            */
2736           r = solv->rules + solv->nrules - 1;           /* r: update rule */
2737           sr = r - (installed->end - installed->start); /* sr: feature rule */
2738           /* it's orphaned if there is no feature rule or the feature rule
2739            * consists just of the installed package */
2740           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
2741             queue_push(&solv->orphaned, i);
2742           if (!r->p)
2743             {
2744               assert(solv->dupmap_all && !sr->p);
2745               continue;
2746             }
2747           if (!solver_samerule(solv, r, sr))
2748             {
2749               /* identical rule, kill unneeded one */
2750               if (solv->allowuninstall)
2751                 {
2752                   /* keep feature rule, make it weak */
2753                   memset(r, 0, sizeof(*r));
2754                   queue_push(&solv->weakruleq, sr - solv->rules);
2755                 }
2756               else
2757                 {
2758                   /* keep update rule */
2759                   memset(sr, 0, sizeof(*sr));
2760                 }
2761             }
2762           else if (solv->allowuninstall)
2763             {
2764               /* make both feature and update rule weak */
2765               queue_push(&solv->weakruleq, r - solv->rules);
2766               queue_push(&solv->weakruleq, sr - solv->rules);
2767             }
2768           else
2769             solver_disablerule(solv, sr);
2770         }
2771       /* consistency check: we added a rule for _every_ installed solvable */
2772       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
2773     }
2774   solv->updaterules_end = solv->nrules;
2775
2776
2777   /*
2778    * now add all job rules
2779    */
2780
2781   solv->jobrules = solv->nrules;
2782   for (i = 0; i < job->count; i += 2)
2783     {
2784       oldnrules = solv->nrules;
2785
2786       how = job->elements[i];
2787       what = job->elements[i + 1];
2788       weak = how & SOLVER_WEAK;
2789       select = how & SOLVER_SELECTMASK;
2790       switch (how & SOLVER_JOBMASK)
2791         {
2792         case SOLVER_INSTALL:
2793           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2794           if (select == SOLVER_SOLVABLE)
2795             {
2796               p = what;
2797               d = 0;
2798             }
2799           else
2800             {
2801               queue_empty(&q);
2802               FOR_JOB_SELECT(p, pp, select, what)
2803                 queue_push(&q, p);
2804               if (!q.count)
2805                 {
2806                   /* no candidate found, make this an impossible rule */
2807                   queue_push(&q, -SYSTEMSOLVABLE);
2808                 }
2809               p = queue_shift(&q);      /* get first candidate */
2810               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
2811             }
2812           solver_addjobrule(solv, p, d, i, weak);
2813           break;
2814         case SOLVER_ERASE:
2815           POOL_DEBUG(SAT_DEBUG_JOB, "job: %s%serase %s\n", weak ? "weak " : "", how & SOLVER_CLEANDEPS ? "clean deps " : "", solver_select2str(pool, select, what));
2816           if ((how & SOLVER_CLEANDEPS) != 0 && !solv->cleandepsmap.size && solv->installed)
2817             map_grow(&solv->cleandepsmap, solv->installed->end - solv->installed->start);
2818           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
2819             {
2820               /* special case for "erase a specific solvable": we also
2821                * erase all other solvables with that name, so that they
2822                * don't get picked up as replacement */
2823               /* XXX: look also at packages that obsolete this package? */
2824               name = pool->solvables[what].name;
2825               FOR_PROVIDES(p, pp, name)
2826                 {
2827                   if (p == what)
2828                     continue;
2829                   s = pool->solvables + p;
2830                   if (s->name != name)
2831                     continue;
2832                   /* keep other versions installed */
2833                   if (s->repo == solv->installed)
2834                     continue;
2835                   /* keep installcandidates of other jobs */
2836                   if (MAPTST(&installcandidatemap, p))
2837                     continue;
2838                   solver_addjobrule(solv, -p, 0, i, weak);      /* remove by id */
2839                 }
2840             }
2841           FOR_JOB_SELECT(p, pp, select, what)
2842             solver_addjobrule(solv, -p, 0, i, weak);
2843           break;
2844
2845         case SOLVER_UPDATE:
2846           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2847           break;
2848         case SOLVER_VERIFY:
2849           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sverify %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2850           break;
2851         case SOLVER_WEAKENDEPS:
2852           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2853           if (select != SOLVER_SOLVABLE)
2854             break;
2855           s = pool->solvables + what;
2856           weaken_solvable_deps(solv, what);
2857           break;
2858         case SOLVER_NOOBSOLETES:
2859           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2860           break;
2861         case SOLVER_LOCK:
2862           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2863           FOR_JOB_SELECT(p, pp, select, what)
2864             {
2865               s = pool->solvables + p;
2866               solver_addjobrule(solv, installed && s->repo == installed ? p : -p, 0, i, weak);
2867             }
2868           break;
2869         case SOLVER_DISTUPGRADE:
2870           POOL_DEBUG(SAT_DEBUG_JOB, "job: distupgrade %s\n", solver_select2str(pool, select, what));
2871           break;
2872         case SOLVER_DROP_ORPHANED:
2873           POOL_DEBUG(SAT_DEBUG_JOB, "job: drop orphaned %s\n", solver_select2str(pool, select, what));
2874           if (select == SOLVER_SOLVABLE_ALL)
2875             solv->droporphanedmap_all = 1;
2876           FOR_JOB_SELECT(p, pp, select, what)
2877             {
2878               s = pool->solvables + p;
2879               if (!installed || s->repo != installed)
2880                 continue;
2881               if (!solv->droporphanedmap.size)
2882                 map_grow(&solv->droporphanedmap, installed->end - installed->start);
2883               MAPSET(&solv->droporphanedmap, p - installed->start);
2884             }
2885           break;
2886         case SOLVER_USERINSTALLED:
2887           POOL_DEBUG(SAT_DEBUG_JOB, "job: user installed %s\n", solver_select2str(pool, select, what));
2888           break;
2889         default:
2890           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
2891           break;
2892         }
2893
2894         /*
2895          * debug
2896          */
2897
2898       IF_POOLDEBUG (SAT_DEBUG_JOB)
2899         {
2900           int j;
2901           if (solv->nrules == oldnrules)
2902             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
2903           for (j = oldnrules; j < solv->nrules; j++)
2904             {
2905               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
2906               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
2907             }
2908         }
2909     }
2910   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
2911   solv->jobrules_end = solv->nrules;
2912
2913   /* now create infarch and dup rules */
2914   if (!solv->noinfarchcheck)
2915     {
2916       solver_addinfarchrules(solv, &addedmap);
2917       if (pool->obsoleteusescolors)
2918         {
2919           /* currently doesn't work well with infarch rules, so make
2920            * them weak */
2921           for (i = solv->infarchrules; i < solv->infarchrules_end; i++)
2922             queue_push(&solv->weakruleq, i);
2923         }
2924     }
2925   else
2926     solv->infarchrules = solv->infarchrules_end = solv->nrules;
2927
2928   if (hasdupjob)
2929     {
2930       solver_addduprules(solv, &addedmap);
2931       solver_freedupmaps(solv); /* no longer needed */
2932     }
2933   else
2934     solv->duprules = solv->duprules_end = solv->nrules;
2935
2936   if (1)
2937     solver_addchoicerules(solv);
2938   else
2939     solv->choicerules = solv->choicerules_end = solv->nrules;
2940
2941   /* all rules created
2942    * --------------------------------------------------------------
2943    * prepare for solving
2944    */
2945
2946   /* free unneeded memory */
2947   map_free(&addedmap);
2948   map_free(&installcandidatemap);
2949   queue_free(&q);
2950
2951   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);
2952
2953   /* create weak map */
2954   map_init(&solv->weakrulemap, solv->nrules);
2955   for (i = 0; i < solv->weakruleq.count; i++)
2956     {
2957       p = solv->weakruleq.elements[i];
2958       MAPSET(&solv->weakrulemap, p);
2959     }
2960
2961   /* all new rules are learnt after this point */
2962   solv->learntrules = solv->nrules;
2963
2964   /* create watches chains */
2965   makewatches(solv);
2966
2967   /* create assertion index. it is only used to speed up
2968    * makeruledecsions() a bit */
2969   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
2970     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
2971       queue_push(&solv->ruleassertions, i);
2972
2973   /* disable update rules that conflict with our job */
2974   solver_disablepolicyrules(solv);
2975
2976   /* make initial decisions based on assertion rules */
2977   makeruledecisions(solv);
2978   POOL_DEBUG(SAT_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count);
2979
2980   /*
2981    * ********************************************
2982    * solve!
2983    * ********************************************
2984    */
2985
2986   now = sat_timems(0);
2987   solver_run_sat(solv, 1, solv->dontinstallrecommended ? 0 : 1);
2988   POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
2989
2990   /*
2991    * calculate recommended/suggested packages
2992    */
2993   findrecommendedsuggested(solv);
2994
2995   /*
2996    * prepare solution queue if there were problems
2997    */
2998   solver_prepare_solutions(solv);
2999
3000   /*
3001    * finally prepare transaction info
3002    */
3003   transaction_calculate(&solv->trans, &solv->decisionq, &solv->noobsoletes);
3004
3005   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);
3006   POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
3007   return solv->problems.count ? solv->problems.count / 2 : 0;
3008 }
3009
3010 /***********************************************************************/
3011 /* disk usage computations */
3012
3013 /*-------------------------------------------------------------------
3014  *
3015  * calculate DU changes
3016  */
3017
3018 void
3019 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
3020 {
3021   Map installedmap;
3022
3023   solver_create_state_maps(solv, &installedmap, 0);
3024   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
3025   map_free(&installedmap);
3026 }
3027
3028
3029 /*-------------------------------------------------------------------
3030  *
3031  * calculate changes in install size
3032  */
3033
3034 int
3035 solver_calc_installsizechange(Solver *solv)
3036 {
3037   Map installedmap;
3038   int change;
3039
3040   solver_create_state_maps(solv, &installedmap, 0);
3041   change = pool_calc_installsizechange(solv->pool, &installedmap);
3042   map_free(&installedmap);
3043   return change;
3044 }
3045
3046 void
3047 solver_create_state_maps(Solver *solv, Map *installedmap, Map *conflictsmap)
3048 {
3049   pool_create_state_maps(solv->pool, &solv->decisionq, installedmap, conflictsmap);
3050 }
3051
3052 void
3053 solver_trivial_installable(Solver *solv, Queue *pkgs, Queue *res)
3054 {
3055   Map installedmap;
3056   pool_create_state_maps(solv->pool,  &solv->decisionq, &installedmap, 0);
3057   pool_trivial_installable_noobsoletesmap(solv->pool, &installedmap, pkgs, res, solv->noobsoletes.size ? &solv->noobsoletes : 0);
3058   map_free(&installedmap);
3059 }
3060