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