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