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