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   if (solv->learntrules && why >= solv->learntrules)
 866     {
 867       if (MAPTST(rseen, why - solv->learntrules))
 868         return;
 869       MAPSET(rseen, why - solv->learntrules);
 870       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
 871         if (solv->learnt_pool.elements[i] > 0)
 872           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp, rseen);
 873       return;
 874     }
 875   if (MAPTST(&solv->weakrulemap, why))
 876     if (!*lastweakp || why > *lastweakp)
 877       *lastweakp = why;
 878   /* do not add rpm rules to problem */
 879   if (why < solv->rpmrules_end)
 880     return;
 881   /* turn rule into problem */
 882   if (why >= solv->jobrules && why < solv->jobrules_end)
 883     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
 884   /* normalize dup/infarch rules */
 885   if (why > solv->infarchrules && why < solv->infarchrules_end)
 886     {
 887       Id name = pool->solvables[-solv->rules[why].p].name;
 888       while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name)
 889         why--;
 890     }
 891   if (why > solv->duprules && why < solv->duprules_end)
 892     {
 893       Id name = pool->solvables[-solv->rules[why].p].name;
 894       while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name)
 895         why--;
 896     }
 897
 898   /* return if problem already countains our rule */
 899   if (solv->problems.count)
 900     {
 901       for (i = solv->problems.count - 1; i >= 0; i--)
 902         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
 903           break;
 904         else if (solv->problems.elements[i] == why)
 905           return;
 906     }
 907   queue_push(&solv->problems, why);
 908 }
 909
 910
 911 /*-------------------------------------------------------------------
 912  *
 913  * analyze_unsolvable
 914  *
 915  * return: 1 - disabled some rules, try again
 916  *         0 - hopeless
 917  */
 918
 919 static int
 920 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
 921 {
 922   Pool *pool = solv->pool;
 923   Rule *r;
 924   Map seen;             /* global to speed things up? */
 925   Map rseen;
 926   Id d, v, vv, *dp, why;
 927   int l, i, idx;
 928   Id *decisionmap = solv->decisionmap;
 929   int oldproblemcount;
 930   int oldlearntpoolcount;
 931   Id lastweak;
 932   int record_proof = 1;
 933
 934   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
 935   solv->stats_unsolvable++;
 936   oldproblemcount = solv->problems.count;
 937   oldlearntpoolcount = solv->learnt_pool.count;
 938
 939   /* make room for proof index */
 940   /* must update it later, as analyze_unsolvable_rule would confuse
 941    * it with a rule index if we put the real value in already */
 942   queue_push(&solv->problems, 0);
 943
 944   r = cr;
 945   map_init(&seen, pool->nsolvables);
 946   map_init(&rseen, solv->learntrules ? solv->nrules - solv->learntrules : 0);
 947   if (record_proof)
 948     queue_push(&solv->learnt_pool, r - solv->rules);
 949   lastweak = 0;
 950   analyze_unsolvable_rule(solv, r, &lastweak, &rseen);
 951   d = r->d < 0 ? -r->d - 1 : r->d;
 952   dp = d ? pool->whatprovidesdata + d : 0;
 953   for (i = -1; ; i++)
 954     {
 955       if (i == -1)
 956         v = r->p;
 957       else if (d == 0)
 958         v = i ? 0 : r->w2;
 959       else
 960         v = *dp++;
 961       if (v == 0)
 962         break;
 963       if (DECISIONMAP_TRUE(v))  /* the one true literal */
 964           continue;
 965       vv = v > 0 ? v : -v;
 966       l = solv->decisionmap[vv];
 967       if (l < 0)
 968         l = -l;
 969       MAPSET(&seen, vv);
 970     }
 971   idx = solv->decisionq.count;
 972   while (idx > 0)
 973     {
 974       v = solv->decisionq.elements[--idx];
 975       vv = v > 0 ? v : -v;
 976       if (!MAPTST(&seen, vv))
 977         continue;
 978       why = solv->decisionq_why.elements[idx];
 979       assert(why > 0);
 980       if (record_proof)
 981         queue_push(&solv->learnt_pool, why);
 982       r = solv->rules + why;
 983       analyze_unsolvable_rule(solv, r, &lastweak, &rseen);
 984       d = r->d < 0 ? -r->d - 1 : r->d;
 985       dp = d ? pool->whatprovidesdata + d : 0;
 986       for (i = -1; ; i++)
 987         {
 988           if (i == -1)
 989             v = r->p;
 990           else if (d == 0)
 991             v = i ? 0 : r->w2;
 992           else
 993             v = *dp++;
 994           if (v == 0)
 995             break;
 996           if (DECISIONMAP_TRUE(v))      /* the one true literal */
 997               continue;
 998           vv = v > 0 ? v : -v;
 999           l = solv->decisionmap[vv];
1000           if (l < 0)
1001             l = -l;
1002           MAPSET(&seen, vv);
1003         }
1004     }
1005   map_free(&seen);
1006   map_free(&rseen);
1007   queue_push(&solv->problems, 0);       /* mark end of this problem */
1008
1009   if (lastweak)
1010     {
1011       Id v;
1012       /* disable last weak rule */
1013       solv->problems.count = oldproblemcount;
1014       solv->learnt_pool.count = oldlearntpoolcount;
1015       if (lastweak >= solv->jobrules && lastweak < solv->jobrules_end)
1016         v = -(solv->ruletojob.elements[lastweak - solv->jobrules] + 1);
1017       else
1018         v = lastweak;
1019       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
1020       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + lastweak);
1021       if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end)
1022         solver_disablechoicerules(solv, solv->rules + lastweak);
1023       solver_disableproblem(solv, v);
1024       if (v < 0)
1025         solver_reenablepolicyrules(solv, -(v + 1));
1026       solver_reset(solv);
1027       return 1;
1028     }
1029
1030   /* finish proof */
1031   if (record_proof)
1032     {
1033       queue_push(&solv->learnt_pool, 0);
1034       solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1035     }
1036
1037   if (disablerules)
1038     {
1039       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1040         solver_disableproblem(solv, solv->problems.elements[i]);
1041       /* XXX: might want to enable all weak rules again */
1042       solver_reset(solv);
1043       return 1;
1044     }
1045   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1046   return 0;
1047 }
1048
1049
1050 /********************************************************************/
1051 /* Decision revert */
1052
1053 /*-------------------------------------------------------------------
1054  *
1055  * revert
1056  * revert decisionq to a level
1057  */
1058
1059 static void
1060 revert(Solver *solv, int level)
1061 {
1062   Pool *pool = solv->pool;
1063   Id v, vv;
1064   while (solv->decisionq.count)
1065     {
1066       v = solv->decisionq.elements[solv->decisionq.count - 1];
1067       vv = v > 0 ? v : -v;
1068       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1069         break;
1070       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1071       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
1072         solv->recommendations.count--;
1073       solv->decisionmap[vv] = 0;
1074       solv->decisionq.count--;
1075       solv->decisionq_why.count--;
1076       solv->propagate_index = solv->decisionq.count;
1077     }
1078   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1079     {
1080       solv->branches.count--;
1081       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1082         solv->branches.count--;
1083     }
1084   solv->recommends_index = -1;
1085 }
1086
1087
1088 /*-------------------------------------------------------------------
1089  *
1090  * watch2onhighest - put watch2 on literal with highest level
1091  */
1092
1093 static inline void
1094 watch2onhighest(Solver *solv, Rule *r)
1095 {
1096   int l, wl = 0;
1097   Id d, v, *dp;
1098
1099   d = r->d < 0 ? -r->d - 1 : r->d;
1100   if (!d)
1101     return;     /* binary rule, both watches are set */
1102   dp = solv->pool->whatprovidesdata + d;
1103   while ((v = *dp++) != 0)
1104     {
1105       l = solv->decisionmap[v < 0 ? -v : v];
1106       if (l < 0)
1107         l = -l;
1108       if (l > wl)
1109         {
1110           r->w2 = dp[-1];
1111           wl = l;
1112         }
1113     }
1114 }
1115
1116
1117 /*-------------------------------------------------------------------
1118  *
1119  * setpropagatelearn
1120  *
1121  * add free decision (solvable to install) to decisionq
1122  * increase level and propagate decision
1123  * return if no conflict.
1124  *
1125  * in conflict case, analyze conflict rule, add resulting
1126  * rule to learnt rule set, make decision from learnt
1127  * rule (always unit) and re-propagate.
1128  *
1129  * returns the new solver level or 0 if unsolvable
1130  *
1131  */
1132
1133 static int
1134 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules, Id ruleid)
1135 {
1136   Pool *pool = solv->pool;
1137   Rule *r;
1138   Id p = 0, d = 0;
1139   int l, why;
1140
1141   assert(ruleid >= 0);
1142   if (decision)
1143     {
1144       level++;
1145       if (decision > 0)
1146         solv->decisionmap[decision] = level;
1147       else
1148         solv->decisionmap[-decision] = -level;
1149       queue_push(&solv->decisionq, decision);
1150       queue_push(&solv->decisionq_why, -ruleid);        /* <= 0 -> free decision */
1151     }
1152   for (;;)
1153     {
1154       r = propagate(solv, level);
1155       if (!r)
1156         break;
1157       if (level == 1)
1158         return analyze_unsolvable(solv, r, disablerules);
1159       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
1160       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1161       assert(l > 0 && l < level);
1162       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
1163       level = l;
1164       revert(solv, level);
1165       r = solver_addrule(solv, p, d);
1166       assert(r);
1167       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
1168       queue_push(&solv->learnt_why, why);
1169       if (d)
1170         {
1171           /* at least 2 literals, needs watches */
1172           watch2onhighest(solv, r);
1173           addwatches_rule(solv, r);
1174         }
1175       else
1176         {
1177           /* learnt rule is an assertion */
1178           queue_push(&solv->ruleassertions, r - solv->rules);
1179         }
1180       /* the new rule is unit by design */
1181       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1182       queue_push(&solv->decisionq, p);
1183       queue_push(&solv->decisionq_why, r - solv->rules);
1184       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1185         {
1186           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
1187           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
1188           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
1189           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
1190         }
1191     }
1192   return level;
1193 }
1194
1195
1196 /*-------------------------------------------------------------------
1197  *
1198  * select and install
1199  *
1200  * install best package from the queue. We add an extra package, inst, if
1201  * provided. See comment in weak install section.
1202  *
1203  * returns the new solver level or 0 if unsolvable
1204  *
1205  */
1206
1207 static int
1208 selectandinstall(Solver *solv, int level, Queue *dq, int disablerules, Id ruleid)
1209 {
1210   Pool *pool = solv->pool;
1211   Id p;
1212   int i;
1213
1214   if (dq->count > 1)
1215     policy_filter_unwanted(solv, dq, POLICY_MODE_CHOOSE);
1216   if (dq->count > 1)
1217     {
1218       /* XXX: didn't we already do that? */
1219       /* XXX: shouldn't we prefer installed packages? */
1220       /* XXX: move to policy.c? */
1221       /* choose the supplemented one */
1222       for (i = 0; i < dq->count; i++)
1223         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1224           {
1225             dq->elements[0] = dq->elements[i];
1226             dq->count = 1;
1227             break;
1228           }
1229     }
1230   if (dq->count > 1)
1231     {
1232       /* multiple candidates, open a branch */
1233       for (i = 1; i < dq->count; i++)
1234         queue_push(&solv->branches, dq->elements[i]);
1235       queue_push(&solv->branches, -level);
1236     }
1237   p = dq->elements[0];
1238
1239   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvid2str(pool, p));
1240
1241   return setpropagatelearn(solv, level, p, disablerules, ruleid);
1242 }
1243
1244
1245 /********************************************************************/
1246 /* Main solver interface */
1247
1248
1249 /*-------------------------------------------------------------------
1250  *
1251  * solver_create
1252  * create solver structure
1253  *
1254  * pool: all available solvables
1255  * installed: installed Solvables
1256  *
1257  *
1258  * Upon solving, rules are created to flag the Solvables
1259  * of the 'installed' Repo as installed.
1260  */
1261
1262 Solver *
1263 solver_create(Pool *pool)
1264 {
1265   Solver *solv;
1266   solv = (Solver *)sat_calloc(1, sizeof(Solver));
1267   solv->pool = pool;
1268   solv->installed = pool->installed;
1269
1270   transaction_init(&solv->trans, pool);
1271   queue_init(&solv->ruletojob);
1272   queue_init(&solv->decisionq);
1273   queue_init(&solv->decisionq_why);
1274   queue_init(&solv->problems);
1275   queue_init(&solv->suggestions);
1276   queue_init(&solv->recommendations);
1277   queue_init(&solv->orphaned);
1278   queue_init(&solv->learnt_why);
1279   queue_init(&solv->learnt_pool);
1280   queue_init(&solv->branches);
1281   queue_init(&solv->covenantq);
1282   queue_init(&solv->weakruleq);
1283   queue_init(&solv->ruleassertions);
1284
1285   queue_push(&solv->learnt_pool, 0);    /* so that 0 does not describe a proof */
1286
1287   map_init(&solv->recommendsmap, pool->nsolvables);
1288   map_init(&solv->suggestsmap, pool->nsolvables);
1289   map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
1290   solv->recommends_index = 0;
1291
1292   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
1293   solv->nrules = 1;
1294   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
1295   memset(solv->rules, 0, sizeof(Rule));
1296
1297   return solv;
1298 }
1299
1300
1301 /*-------------------------------------------------------------------
1302  *
1303  * solver_free
1304  */
1305
1306 void
1307 solver_free(Solver *solv)
1308 {
1309   transaction_free(&solv->trans);
1310   queue_free(&solv->job);
1311   queue_free(&solv->ruletojob);
1312   queue_free(&solv->decisionq);
1313   queue_free(&solv->decisionq_why);
1314   queue_free(&solv->learnt_why);
1315   queue_free(&solv->learnt_pool);
1316   queue_free(&solv->problems);
1317   queue_free(&solv->solutions);
1318   queue_free(&solv->suggestions);
1319   queue_free(&solv->recommendations);
1320   queue_free(&solv->orphaned);
1321   queue_free(&solv->branches);
1322   queue_free(&solv->covenantq);
1323   queue_free(&solv->weakruleq);
1324   queue_free(&solv->ruleassertions);
1325
1326   map_free(&solv->recommendsmap);
1327   map_free(&solv->suggestsmap);
1328   map_free(&solv->noupdate);
1329   map_free(&solv->weakrulemap);
1330   map_free(&solv->noobsoletes);
1331
1332   map_free(&solv->updatemap);
1333   map_free(&solv->fixmap);
1334   map_free(&solv->dupmap);
1335   map_free(&solv->dupinvolvedmap);
1336   map_free(&solv->droporphanedmap);
1337   map_free(&solv->cleandepsmap);
1338
1339   sat_free(solv->decisionmap);
1340   sat_free(solv->rules);
1341   sat_free(solv->watches);
1342   sat_free(solv->obsoletes);
1343   sat_free(solv->obsoletes_data);
1344   sat_free(solv->multiversionupdaters);
1345   sat_free(solv->choicerules_ref);
1346   sat_free(solv);
1347 }
1348
1349
1350 /*-------------------------------------------------------------------
1351  *
1352  * solver_run_sat
1353  *
1354  * all rules have been set up, now actually run the solver
1355  *
1356  */
1357
1358 void
1359 solver_run_sat(Solver *solv, int disablerules, int doweak)
1360 {
1361   Queue dq;             /* local decisionqueue */
1362   Queue dqs;            /* local decisionqueue for supplements */
1363   int systemlevel;
1364   int level, olevel;
1365   Rule *r;
1366   int i, j, n;
1367   Solvable *s;
1368   Pool *pool = solv->pool;
1369   Id p, *dp;
1370   int minimizationsteps;
1371   int installedpos = solv->installed ? solv->installed->start : 0;
1372
1373   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
1374     {
1375       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
1376       for (i = 1; i < solv->nrules; i++)
1377         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
1378     }
1379
1380   POOL_DEBUG(SAT_DEBUG_SOLVER, "initial decisions: %d\n", solv->decisionq.count);
1381
1382   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
1383     solver_printdecisions(solv);
1384
1385   /* start SAT algorithm */
1386   level = 1;
1387   systemlevel = level + 1;
1388   POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n");
1389
1390   queue_init(&dq);
1391   queue_init(&dqs);
1392
1393   /*
1394    * here's the main loop:
1395    * 1) propagate new decisions (only needed once)
1396    * 2) fulfill jobs
1397    * 3) try to keep installed packages
1398    * 4) fulfill all unresolved rules
1399    * 5) install recommended packages
1400    * 6) minimalize solution if we had choices
1401    * if we encounter a problem, we rewind to a safe level and restart
1402    * with step 1
1403    */
1404
1405   minimizationsteps = 0;
1406   for (;;)
1407     {
1408       /*
1409        * initial propagation of the assertions
1410        */
1411       if (level == 1)
1412         {
1413           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
1414           if ((r = propagate(solv, level)) != 0)
1415             {
1416               if (analyze_unsolvable(solv, r, disablerules))
1417                 continue;
1418               queue_free(&dq);
1419               queue_free(&dqs);
1420               return;
1421             }
1422         }
1423
1424       /*
1425        * resolve jobs first
1426        */
1427      if (level < systemlevel)
1428         {
1429           POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving job rules\n");
1430           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
1431             {
1432               Id l;
1433               if (r->d < 0)             /* ignore disabled rules */
1434                 continue;
1435               queue_empty(&dq);
1436               FOR_RULELITERALS(l, dp, r)
1437                 {
1438                   if (l < 0)
1439                     {
1440                       if (solv->decisionmap[-l] <= 0)
1441                         break;
1442                     }
1443                   else
1444                     {
1445                       if (solv->decisionmap[l] > 0)
1446                         break;
1447                       if (solv->decisionmap[l] == 0)
1448                         queue_push(&dq, l);
1449                     }
1450                 }
1451               if (l || !dq.count)
1452                 continue;
1453               /* prune to installed if not updating */
1454               if (dq.count > 1 && solv->installed && !solv->updatemap_all)
1455                 {
1456                   int j, k;
1457                   for (j = k = 0; j < dq.count; j++)
1458                     {
1459                       Solvable *s = pool->solvables + dq.elements[j];
1460                       if (s->repo == solv->installed)
1461                         {
1462                           dq.elements[k++] = dq.elements[j];
1463                           if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start))
1464                             {
1465                               k = 0;    /* package wants to be updated, do not prune */
1466                               break;
1467                             }
1468                         }
1469                     }
1470                   if (k)
1471                     dq.count = k;
1472                 }
1473               olevel = level;
1474               level = selectandinstall(solv, level, &dq, disablerules, i);
1475               if (level == 0)
1476                 {
1477                   queue_free(&dq);
1478                   queue_free(&dqs);
1479                   return;
1480                 }
1481               if (level <= olevel)
1482                 break;
1483             }
1484           systemlevel = level + 1;
1485           if (i < solv->jobrules_end)
1486             continue;
1487         }
1488
1489
1490       /*
1491        * installed packages
1492        */
1493       if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled)
1494         {
1495           Repo *installed = solv->installed;
1496           int pass;
1497
1498           POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n");
1499           /* we use two passes if we need to update packages
1500            * to create a better user experience */
1501           for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
1502             {
1503               int passlevel = level;
1504               /* start with installedpos, the position that gave us problems last time */
1505               for (i = installedpos, n = installed->start; n < installed->end; i++, n++)
1506                 {
1507                   Rule *rr;
1508                   Id d;
1509
1510                   if (i == installed->end)
1511                     i = installed->start;
1512                   s = pool->solvables + i;
1513                   if (s->repo != installed)
1514                     continue;
1515
1516                   if (solv->decisionmap[i] > 0)
1517                     continue;
1518                   if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start))
1519                     continue;           /* updates first */
1520                   r = solv->rules + solv->updaterules + (i - installed->start);
1521                   rr = r;
1522                   if (!rr->p || rr->d < 0)      /* disabled -> look at feature rule */
1523                     rr -= solv->installed->end - solv->installed->start;
1524                   if (!rr->p)           /* identical to update rule? */
1525                     rr = r;
1526                   if (!rr->p)
1527                     continue;           /* orpaned package */
1528
1529                   /* XXX: noupdate check is probably no longer needed, as all jobs should
1530                    * already be satisfied */
1531                   /* Actually we currently still need it because of erase jobs */
1532                   /* if noupdate is set we do not look at update candidates */
1533                   queue_empty(&dq);
1534                   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))
1535                     {
1536                       if (solv->noobsoletes.size && solv->multiversionupdaters
1537                              && (d = solv->multiversionupdaters[i - installed->start]) != 0)
1538                         {
1539                           /* special multiversion handling, make sure best version is chosen */
1540                           queue_push(&dq, i);
1541                           while ((p = pool->whatprovidesdata[d++]) != 0)
1542                             if (solv->decisionmap[p] >= 0)
1543                               queue_push(&dq, p);
1544                           policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE);
1545                           p = dq.elements[0];
1546                           if (p != i && solv->decisionmap[p] == 0)
1547                             {
1548                               rr = solv->rules + solv->featurerules + (i - solv->installed->start);
1549                               if (!rr->p)               /* update rule == feature rule? */
1550                                 rr = rr - solv->featurerules + solv->updaterules;
1551                               dq.count = 1;
1552                             }
1553                           else
1554                             dq.count = 0;
1555                         }
1556                       else
1557                         {
1558                           /* update to best package */
1559                           FOR_RULELITERALS(p, dp, rr)
1560                             {
1561                               if (solv->decisionmap[p] > 0)
1562                                 {
1563                                   dq.count = 0;         /* already fulfilled */
1564                                   break;
1565                                 }
1566                               if (!solv->decisionmap[p])
1567                                 queue_push(&dq, p);
1568                             }
1569                         }
1570                     }
1571                   /* install best version */
1572                   if (dq.count)
1573                     {
1574                       olevel = level;
1575                       level = selectandinstall(solv, level, &dq, disablerules, rr - solv->rules);
1576                       if (level == 0)
1577                         {
1578                           queue_free(&dq);
1579                           queue_free(&dqs);
1580                           return;
1581                         }
1582                       if (level <= olevel)
1583                         {
1584                           if (level == 1 || level < passlevel)
1585                             break;      /* trouble */
1586                           if (level < olevel)
1587                             n = installed->start;       /* redo all */
1588                           i--;
1589                           n--;
1590                           continue;
1591                         }
1592                     }
1593                   /* if still undecided keep package */
1594                   if (solv->decisionmap[i] == 0)
1595                     {
1596                       olevel = level;
1597                       if (solv->cleandepsmap.size && MAPTST(&solv->cleandepsmap, i - installed->start))
1598                         {
1599                           POOL_DEBUG(SAT_DEBUG_POLICY, "cleandeps erasing %s\n", solvid2str(pool, i));
1600                           level = setpropagatelearn(solv, level, -i, disablerules, 0);
1601                         }
1602                       else
1603                         {
1604                           POOL_DEBUG(SAT_DEBUG_POLICY, "keeping %s\n", solvid2str(pool, i));
1605                           level = setpropagatelearn(solv, level, i, disablerules, r - solv->rules);
1606                         }
1607                       if (level == 0)
1608                         {
1609                           queue_free(&dq);
1610                           queue_free(&dqs);
1611                           return;
1612                         }
1613                       if (level <= olevel)
1614                         {
1615                           if (level == 1 || level < passlevel)
1616                             break;      /* trouble */
1617                           if (level < olevel)
1618                             n = installed->start;       /* redo all */
1619                           i--;
1620                           n--;
1621                           continue; /* retry with learnt rule */
1622                         }
1623                     }
1624                 }
1625               if (n < installed->end)
1626                 {
1627                   installedpos = i;     /* retry problem solvable next time */
1628                   break;                /* ran into trouble */
1629                 }
1630               installedpos = installed->start;  /* reset installedpos */
1631             }
1632           systemlevel = level + 1;
1633           if (pass < 2)
1634             continue;           /* had trouble, retry */
1635         }
1636
1637       if (level < systemlevel)
1638         systemlevel = level;
1639
1640       /*
1641        * decide
1642        */
1643       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
1644       for (i = 1, n = 1; n < solv->nrules; i++, n++)
1645         {
1646           if (i == solv->nrules)
1647             i = 1;
1648           r = solv->rules + i;
1649           if (r->d < 0)         /* ignore disabled rules */
1650             continue;
1651           queue_empty(&dq);
1652           if (r->d == 0)
1653             {
1654               /* binary or unary rule */
1655               /* need two positive undecided literals */
1656               if (r->p < 0 || r->w2 <= 0)
1657                 continue;
1658               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
1659                 continue;
1660               queue_push(&dq, r->p);
1661               queue_push(&dq, r->w2);
1662             }
1663           else
1664             {
1665               /* make sure that
1666                * all negative literals are installed
1667                * no positive literal is installed
1668                * i.e. the rule is not fulfilled and we
1669                * just need to decide on the positive literals
1670                */
1671               if (r->p < 0)
1672                 {
1673                   if (solv->decisionmap[-r->p] <= 0)
1674                     continue;
1675                 }
1676               else
1677                 {
1678                   if (solv->decisionmap[r->p] > 0)
1679                     continue;
1680                   if (solv->decisionmap[r->p] == 0)
1681                     queue_push(&dq, r->p);
1682                 }
1683               dp = pool->whatprovidesdata + r->d;
1684               while ((p = *dp++) != 0)
1685                 {
1686                   if (p < 0)
1687                     {
1688                       if (solv->decisionmap[-p] <= 0)
1689                         break;
1690                     }
1691                   else
1692                     {
1693                       if (solv->decisionmap[p] > 0)
1694                         break;
1695                       if (solv->decisionmap[p] == 0)
1696                         queue_push(&dq, p);
1697                     }
1698                 }
1699               if (p)
1700                 continue;
1701             }
1702           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1703             {
1704               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
1705               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
1706             }
1707           /* dq.count < 2 cannot happen as this means that
1708            * the rule is unit */
1709           assert(dq.count > 1);
1710
1711           olevel = level;
1712           level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules);
1713           if (level == 0)
1714             {
1715               queue_free(&dq);
1716               queue_free(&dqs);
1717               return;
1718             }
1719           if (level < systemlevel || level == 1)
1720             break;              /* trouble */
1721           /* something changed, so look at all rules again */
1722           n = 0;
1723         }
1724
1725       if (n != solv->nrules)    /* ran into trouble, restart */
1726         continue;
1727
1728       /* at this point we have a consistent system. now do the extras... */
1729
1730       if (doweak)
1731         {
1732           int qcount;
1733
1734           POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
1735           queue_empty(&dq);     /* recommended packages */
1736           queue_empty(&dqs);    /* supplemented packages */
1737           for (i = 1; i < pool->nsolvables; i++)
1738             {
1739               if (solv->decisionmap[i] < 0)
1740                 continue;
1741               if (solv->decisionmap[i] > 0)
1742                 {
1743                   /* installed, check for recommends */
1744                   Id *recp, rec, pp, p;
1745                   s = pool->solvables + i;
1746                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
1747                     continue;
1748                   /* XXX need to special case AND ? */
1749                   if (s->recommends)
1750                     {
1751                       recp = s->repo->idarraydata + s->recommends;
1752                       while ((rec = *recp++) != 0)
1753                         {
1754                           qcount = dq.count;
1755                           FOR_PROVIDES(p, pp, rec)
1756                             {
1757                               if (solv->decisionmap[p] > 0)
1758                                 {
1759                                   dq.count = qcount;
1760                                   break;
1761                                 }
1762                               else if (solv->decisionmap[p] == 0)
1763                                 {
1764                                   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))))
1765                                     continue;
1766                                   queue_pushunique(&dq, p);
1767                                 }
1768                             }
1769                         }
1770                     }
1771                 }
1772               else
1773                 {
1774                   s = pool->solvables + i;
1775                   if (!s->supplements)
1776                     continue;
1777                   if (!pool_installable(pool, s))
1778                     continue;
1779                   if (!solver_is_supplementing(solv, s))
1780                     continue;
1781                   if (solv->dupmap_all && solv->installed && s->repo == solv->installed && (solv->droporphanedmap_all || (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, i - solv->installed->start))))
1782                     continue;
1783                   queue_push(&dqs, i);
1784                 }
1785             }
1786
1787           /* filter out all packages obsoleted by installed packages */
1788           /* this is no longer needed if we have reverse obsoletes */
1789           if ((dqs.count || dq.count) && solv->installed)
1790             {
1791               Map obsmap;
1792               Id obs, *obsp, po, ppo;
1793
1794               map_init(&obsmap, pool->nsolvables);
1795               for (p = solv->installed->start; p < solv->installed->end; p++)
1796                 {
1797                   s = pool->solvables + p;
1798                   if (s->repo != solv->installed || !s->obsoletes)
1799                     continue;
1800                   if (solv->decisionmap[p] <= 0)
1801                     continue;
1802                   if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
1803                     continue;
1804                   obsp = s->repo->idarraydata + s->obsoletes;
1805                   /* foreach obsoletes */
1806                   while ((obs = *obsp++) != 0)
1807                     FOR_PROVIDES(po, ppo, obs)
1808                       MAPSET(&obsmap, po);
1809                 }
1810               for (i = j = 0; i < dqs.count; i++)
1811                 if (!MAPTST(&obsmap, dqs.elements[i]))
1812                   dqs.elements[j++] = dqs.elements[i];
1813               dqs.count = j;
1814               for (i = j = 0; i < dq.count; i++)
1815                 if (!MAPTST(&obsmap, dq.elements[i]))
1816                   dq.elements[j++] = dq.elements[i];
1817               dq.count = j;
1818               map_free(&obsmap);
1819             }
1820
1821           /* filter out all already supplemented packages if requested */
1822           if (solv->ignorealreadyrecommended && dqs.count)
1823             {
1824               /* turn off all new packages */
1825               for (i = 0; i < solv->decisionq.count; i++)
1826                 {
1827                   p = solv->decisionq.elements[i];
1828                   if (p < 0)
1829                     continue;
1830                   s = pool->solvables + p;
1831                   if (s->repo && s->repo != solv->installed)
1832                     solv->decisionmap[p] = -solv->decisionmap[p];
1833                 }
1834               /* filter out old supplements */
1835               for (i = j = 0; i < dqs.count; i++)
1836                 {
1837                   p = dqs.elements[i];
1838                   s = pool->solvables + p;
1839                   if (!s->supplements)
1840                     continue;
1841                   if (!solver_is_supplementing(solv, s))
1842                     dqs.elements[j++] = p;
1843                 }
1844               dqs.count = j;
1845               /* undo turning off */
1846               for (i = 0; i < solv->decisionq.count; i++)
1847                 {
1848                   p = solv->decisionq.elements[i];
1849                   if (p < 0)
1850                     continue;
1851                   s = pool->solvables + p;
1852                   if (s->repo && s->repo != solv->installed)
1853                     solv->decisionmap[p] = -solv->decisionmap[p];
1854                 }
1855             }
1856
1857           /* multiversion doesn't mix well with supplements.
1858            * filter supplemented packages where we already decided
1859            * to install a different version (see bnc#501088) */
1860           if (dqs.count && solv->noobsoletes.size)
1861             {
1862               for (i = j = 0; i < dqs.count; i++)
1863                 {
1864                   p = dqs.elements[i];
1865                   if (MAPTST(&solv->noobsoletes, p))
1866                     {
1867                       Id p2, pp2;
1868                       s = pool->solvables + p;
1869                       FOR_PROVIDES(p2, pp2, s->name)
1870                         if (solv->decisionmap[p2] > 0 && pool->solvables[p2].name == s->name)
1871                           break;
1872                       if (p2)
1873                         continue;       /* ignore this package */
1874                     }
1875                   dqs.elements[j++] = p;
1876                 }
1877               dqs.count = j;
1878             }
1879
1880           /* make dq contain both recommended and supplemented pkgs */
1881           if (dqs.count)
1882             {
1883               for (i = 0; i < dqs.count; i++)
1884                 queue_pushunique(&dq, dqs.elements[i]);
1885             }
1886
1887           if (dq.count)
1888             {
1889               Map dqmap;
1890               int decisioncount = solv->decisionq.count;
1891
1892               if (dq.count == 1)
1893                 {
1894                   /* simple case, just one package. no need to choose  */
1895                   p = dq.elements[0];
1896                   if (dqs.count)
1897                     POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
1898                   else
1899                     POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
1900                   queue_push(&solv->recommendations, p);
1901                   level = setpropagatelearn(solv, level, p, 0, 0);
1902                   continue;     /* back to main loop */
1903                 }
1904
1905               /* filter packages, this gives us the best versions */
1906               policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
1907
1908               /* create map of result */
1909               map_init(&dqmap, pool->nsolvables);
1910               for (i = 0; i < dq.count; i++)
1911                 MAPSET(&dqmap, dq.elements[i]);
1912
1913               /* install all supplemented packages */
1914               for (i = 0; i < dqs.count; i++)
1915                 {
1916                   p = dqs.elements[i];
1917                   if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
1918                     continue;
1919                   POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
1920                   queue_push(&solv->recommendations, p);
1921                   olevel = level;
1922                   level = setpropagatelearn(solv, level, p, 0, 0);
1923                   if (level <= olevel)
1924                     break;
1925                 }
1926               if (i < dqs.count || solv->decisionq.count < decisioncount)
1927                 {
1928                   map_free(&dqmap);
1929                   continue;
1930                 }
1931
1932               /* install all recommended packages */
1933               /* more work as we want to created branches if multiple
1934                * choices are valid */
1935               for (i = 0; i < decisioncount; i++)
1936                 {
1937                   Id rec, *recp, pp;
1938                   p = solv->decisionq.elements[i];
1939                   if (p < 0)
1940                     continue;
1941                   s = pool->solvables + p;
1942                   if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
1943                     continue;
1944                   if (!s->recommends)
1945                     continue;
1946                   recp = s->repo->idarraydata + s->recommends;
1947                   while ((rec = *recp++) != 0)
1948                     {
1949                       queue_empty(&dq);
1950                       FOR_PROVIDES(p, pp, rec)
1951                         {
1952                           if (solv->decisionmap[p] > 0)
1953                             {
1954                               dq.count = 0;
1955                               break;
1956                             }
1957                           else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
1958                             queue_pushunique(&dq, p);
1959                         }
1960                       if (!dq.count)
1961                         continue;
1962                       if (dq.count > 1)
1963                         {
1964                           /* multiple candidates, open a branch */
1965                           for (i = 1; i < dq.count; i++)
1966                             queue_push(&solv->branches, dq.elements[i]);
1967                           queue_push(&solv->branches, -level);
1968                         }
1969                       p = dq.elements[0];
1970                       POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
1971                       queue_push(&solv->recommendations, p);
1972                       olevel = level;
1973                       level = setpropagatelearn(solv, level, p, 0, 0);
1974                       if (level <= olevel || solv->decisionq.count < decisioncount)
1975                         break;  /* we had to revert some decisions */
1976                     }
1977                   if (rec)
1978                     break;      /* had a problem above, quit loop */
1979                 }
1980               map_free(&dqmap);
1981
1982               continue;         /* back to main loop so that all deps are checked */
1983             }
1984         }
1985
1986      if (solv->dupmap_all && solv->installed)
1987         {
1988           int installedone = 0;
1989
1990           /* let's see if we can install some unsupported package */
1991           POOL_DEBUG(SAT_DEBUG_SOLVER, "deciding orphaned packages\n");
1992           for (i = 0; i < solv->orphaned.count; i++)
1993             {
1994               p = solv->orphaned.elements[i];
1995               if (solv->decisionmap[p])
1996                 continue;       /* already decided */
1997               olevel = level;
1998               if (solv->droporphanedmap_all)
1999                 continue;
2000               if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))
2001                 continue;
2002               POOL_DEBUG(SAT_DEBUG_SOLVER, "keeping orphaned %s\n", solvid2str(pool, p));
2003               level = setpropagatelearn(solv, level, p, 0, 0);
2004               installedone = 1;
2005               if (level < olevel)
2006                 break;
2007             }
2008           if (installedone || i < solv->orphaned.count)
2009             continue;           /* back to main loop */
2010           for (i = 0; i < solv->orphaned.count; i++)
2011             {
2012               p = solv->orphaned.elements[i];
2013               if (solv->decisionmap[p])
2014                 continue;       /* already decided */
2015               POOL_DEBUG(SAT_DEBUG_SOLVER, "removing orphaned %s\n", solvid2str(pool, p));
2016               olevel = level;
2017               level = setpropagatelearn(solv, level, -p, 0, 0);
2018               if (level < olevel)
2019                 break;
2020             }
2021           if (i < solv->orphaned.count)
2022             continue;           /* back to main loop */
2023         }
2024
2025      if (solv->solution_callback)
2026         {
2027           solv->solution_callback(solv, solv->solution_callback_data);
2028           if (solv->branches.count)
2029             {
2030               int i = solv->branches.count - 1;
2031               int l = -solv->branches.elements[i];
2032               Id why;
2033
2034               for (; i > 0; i--)
2035                 if (solv->branches.elements[i - 1] < 0)
2036                   break;
2037               p = solv->branches.elements[i];
2038               POOL_DEBUG(SAT_DEBUG_SOLVER, "branching with %s\n", solvid2str(pool, p));
2039               queue_empty(&dq);
2040               for (j = i + 1; j < solv->branches.count; j++)
2041                 queue_push(&dq, solv->branches.elements[j]);
2042               solv->branches.count = i;
2043               level = l;
2044               revert(solv, level);
2045               if (dq.count > 1)
2046                 for (j = 0; j < dq.count; j++)
2047                   queue_push(&solv->branches, dq.elements[j]);
2048               olevel = level;
2049               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2050               assert(why >= 0);
2051               level = setpropagatelearn(solv, level, p, disablerules, why);
2052               if (level == 0)
2053                 {
2054                   queue_free(&dq);
2055                   queue_free(&dqs);
2056                   return;
2057                 }
2058               continue;
2059             }
2060           /* all branches done, we're finally finished */
2061           break;
2062         }
2063
2064       /* minimization step */
2065      if (solv->branches.count)
2066         {
2067           int l = 0, lasti = -1, lastl = -1;
2068           Id why;
2069
2070           p = 0;
2071           for (i = solv->branches.count - 1; i >= 0; i--)
2072             {
2073               p = solv->branches.elements[i];
2074               if (p < 0)
2075                 l = -p;
2076               else if (p > 0 && solv->decisionmap[p] > l + 1)
2077                 {
2078                   lasti = i;
2079                   lastl = l;
2080                 }
2081             }
2082           if (lasti >= 0)
2083             {
2084               /* kill old solvable so that we do not loop */
2085               p = solv->branches.elements[lasti];
2086               solv->branches.elements[lasti] = 0;
2087               POOL_DEBUG(SAT_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, solvid2str(pool, p));
2088               minimizationsteps++;
2089
2090               level = lastl;
2091               revert(solv, level);
2092               why = -solv->decisionq_why.elements[solv->decisionq_why.count];
2093               assert(why >= 0);
2094               olevel = level;
2095               level = setpropagatelearn(solv, level, p, disablerules, why);
2096               if (level == 0)
2097                 {
2098                   queue_free(&dq);
2099                   queue_free(&dqs);
2100                   return;
2101                 }
2102               continue;         /* back to main loop */
2103             }
2104         }
2105       /* no minimization found, we're finally finished! */
2106       break;
2107     }
2108
2109   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
2110
2111   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2112   queue_free(&dq);
2113   queue_free(&dqs);
2114 #if 0
2115   solver_printdecisionq(solv, SAT_DEBUG_RESULT);
2116 #endif
2117 }
2118
2119
2120 /*-------------------------------------------------------------------
2121  *
2122  * remove disabled conflicts
2123  *
2124  * purpose: update the decisionmap after some rules were disabled.
2125  * this is used to calculate the suggested/recommended package list.
2126  * Also returns a "removed" list to undo the discisionmap changes.
2127  */
2128
2129 static void
2130 removedisabledconflicts(Solver *solv, Queue *removed)
2131 {
2132   Pool *pool = solv->pool;
2133   int i, n;
2134   Id p, why, *dp;
2135   Id new;
2136   Rule *r;
2137   Id *decisionmap = solv->decisionmap;
2138
2139   POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n");
2140   queue_empty(removed);
2141   for (i = 0; i < solv->decisionq.count; i++)
2142     {
2143       p = solv->decisionq.elements[i];
2144       if (p > 0)
2145         continue;       /* conflicts only, please */
2146       why = solv->decisionq_why.elements[i];
2147       if (why == 0)
2148         {
2149           /* no rule involved, must be a orphan package drop */
2150           continue;
2151         }
2152       /* we never do conflicts on free decisions, so there
2153        * must have been an unit rule */
2154       assert(why > 0);
2155       r = solv->rules + why;
2156       if (r->d < 0 && decisionmap[-p])
2157         {
2158           /* rule is now disabled, remove from decisionmap */
2159           POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvid2str(pool, -p), -p);
2160           queue_push(removed, -p);
2161           queue_push(removed, decisionmap[-p]);
2162           decisionmap[-p] = 0;
2163         }
2164     }
2165   if (!removed->count)
2166     return;
2167   /* we removed some confliced packages. some of them might still
2168    * be in conflict, so search for unit rules and re-conflict */
2169   new = 0;
2170   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
2171     {
2172       if (i == solv->nrules)
2173         {
2174           i = 1;
2175           r = solv->rules + i;
2176         }
2177       if (r->d < 0)
2178         continue;
2179       if (!r->w2)
2180         {
2181           if (r->p < 0 && !decisionmap[-r->p])
2182             new = r->p;
2183         }
2184       else if (!r->d)
2185         {
2186           /* binary rule */
2187           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
2188             new = r->p;
2189           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
2190             new = r->w2;
2191         }
2192       else
2193         {
2194           if (r->p < 0 && decisionmap[-r->p] == 0)
2195             new = r->p;
2196           if (new || DECISIONMAP_FALSE(r->p))
2197             {
2198               dp = pool->whatprovidesdata + r->d;
2199               while ((p = *dp++) != 0)
2200                 {
2201                   if (new && p == new)
2202                     continue;
2203                   if (p < 0 && decisionmap[-p] == 0)
2204                     {
2205                       if (new)
2206                         {
2207                           new = 0;
2208                           break;
2209                         }
2210                       new = p;
2211                     }
2212                   else if (!DECISIONMAP_FALSE(p))
2213                     {
2214                       new = 0;
2215                       break;
2216                     }
2217                 }
2218             }
2219         }
2220       if (new)
2221         {
2222           POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvid2str(pool, -new), -new);
2223           decisionmap[-new] = -1;
2224           new = 0;
2225           n = 0;        /* redo all rules */
2226         }
2227     }
2228 }
2229
2230 static inline void
2231 undo_removedisabledconflicts(Solver *solv, Queue *removed)
2232 {
2233   int i;
2234   for (i = 0; i < removed->count; i += 2)
2235     solv->decisionmap[removed->elements[i]] = removed->elements[i + 1];
2236 }
2237
2238
2239 /*-------------------------------------------------------------------
2240  *
2241  * weaken solvable dependencies
2242  */
2243
2244 static void
2245 weaken_solvable_deps(Solver *solv, Id p)
2246 {
2247   int i;
2248   Rule *r;
2249
2250   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
2251     {
2252       if (r->p != -p)
2253         continue;
2254       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
2255         continue;       /* conflict */
2256       queue_push(&solv->weakruleq, i);
2257     }
2258 }
2259
2260
2261 /********************************************************************/
2262 /* main() */
2263
2264
2265 static void
2266 findrecommendedsuggested(Solver *solv)
2267 {
2268   Pool *pool = solv->pool;
2269   Queue redoq, disabledq;
2270   int goterase, i;
2271   Solvable *s;
2272   Rule *r;
2273   Map obsmap;
2274
2275   map_init(&obsmap, pool->nsolvables);
2276   if (solv->installed)
2277     {
2278       Id obs, *obsp, p, po, ppo;
2279       for (p = solv->installed->start; p < solv->installed->end; p++)
2280         {
2281           s = pool->solvables + p;
2282           if (s->repo != solv->installed || !s->obsoletes)
2283             continue;
2284           if (solv->decisionmap[p] <= 0)
2285             continue;
2286           if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
2287             continue;
2288           obsp = s->repo->idarraydata + s->obsoletes;
2289           /* foreach obsoletes */
2290           while ((obs = *obsp++) != 0)
2291             FOR_PROVIDES(po, ppo, obs)
2292               MAPSET(&obsmap, po);
2293         }
2294     }
2295
2296   queue_init(&redoq);
2297   queue_init(&disabledq);
2298   goterase = 0;
2299   /* disable all erase jobs (including weak "keep uninstalled" rules) */
2300   for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2301     {
2302       if (r->d < 0)     /* disabled ? */
2303         continue;
2304       if (r->p >= 0)    /* install job? */
2305         continue;
2306       queue_push(&disabledq, i);
2307       solver_disablerule(solv, r);
2308       goterase++;
2309     }
2310
2311   if (goterase)
2312     {
2313       enabledisablelearntrules(solv);
2314       removedisabledconflicts(solv, &redoq);
2315     }
2316
2317   /*
2318    * find recommended packages
2319    */
2320
2321   /* if redoq.count == 0 we already found all recommended in the
2322    * solver run */
2323   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
2324     {
2325       Id rec, *recp, p, pp;
2326
2327       /* create map of all recommened packages */
2328       solv->recommends_index = -1;
2329       MAPZERO(&solv->recommendsmap);
2330       for (i = 0; i < solv->decisionq.count; i++)
2331         {
2332           p = solv->decisionq.elements[i];
2333           if (p < 0)
2334             continue;
2335           s = pool->solvables + p;
2336           if (s->recommends)
2337             {
2338               recp = s->repo->idarraydata + s->recommends;
2339               while ((rec = *recp++) != 0)
2340                 {
2341                   FOR_PROVIDES(p, pp, rec)
2342                     if (solv->decisionmap[p] > 0)
2343                       break;
2344                   if (p)
2345                     {
2346                       if (!solv->dontshowinstalledrecommended)
2347                         {
2348                           FOR_PROVIDES(p, pp, rec)
2349                             if (solv->decisionmap[p] > 0)
2350                               MAPSET(&solv->recommendsmap, p);
2351                         }
2352                       continue; /* p != 0: already fulfilled */
2353                     }
2354                   FOR_PROVIDES(p, pp, rec)
2355                     MAPSET(&solv->recommendsmap, p);
2356                 }
2357             }
2358         }
2359       for (i = 1; i < pool->nsolvables; i++)
2360         {
2361           if (solv->decisionmap[i] < 0)
2362             continue;
2363           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
2364             continue;
2365           if (MAPTST(&obsmap, i))
2366             continue;
2367           s = pool->solvables + i;
2368           if (!MAPTST(&solv->recommendsmap, i))
2369             {
2370               if (!s->supplements)
2371                 continue;
2372               if (!pool_installable(pool, s))
2373                 continue;
2374               if (!solver_is_supplementing(solv, s))
2375                 continue;
2376             }
2377           if (solv->dontinstallrecommended)
2378             queue_push(&solv->recommendations, i);
2379           else
2380             queue_pushunique(&solv->recommendations, i);
2381         }
2382       /* we use MODE_SUGGEST here so that repo prio is ignored */
2383       policy_filter_unwanted(solv, &solv->recommendations, POLICY_MODE_SUGGEST);
2384     }
2385
2386   /*
2387    * find suggested packages
2388    */
2389
2390   if (1)
2391     {
2392       Id sug, *sugp, p, pp;
2393
2394       /* create map of all suggests that are still open */
2395       solv->recommends_index = -1;
2396       MAPZERO(&solv->suggestsmap);
2397       for (i = 0; i < solv->decisionq.count; i++)
2398         {
2399           p = solv->decisionq.elements[i];
2400           if (p < 0)
2401             continue;
2402           s = pool->solvables + p;
2403           if (s->suggests)
2404             {
2405               sugp = s->repo->idarraydata + s->suggests;
2406               while ((sug = *sugp++) != 0)
2407                 {
2408                   FOR_PROVIDES(p, pp, sug)
2409                     if (solv->decisionmap[p] > 0)
2410                       break;
2411                   if (p)
2412                     {
2413                       if (!solv->dontshowinstalledrecommended)
2414                         {
2415                           FOR_PROVIDES(p, pp, sug)
2416                             if (solv->decisionmap[p] > 0)
2417                               MAPSET(&solv->suggestsmap, p);
2418                         }
2419                       continue; /* already fulfilled */
2420                     }
2421                   FOR_PROVIDES(p, pp, sug)
2422                     MAPSET(&solv->suggestsmap, p);
2423                 }
2424             }
2425         }
2426       for (i = 1; i < pool->nsolvables; i++)
2427         {
2428           if (solv->decisionmap[i] < 0)
2429             continue;
2430           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
2431             continue;
2432           if (MAPTST(&obsmap, i))
2433             continue;
2434           s = pool->solvables + i;
2435           if (!MAPTST(&solv->suggestsmap, i))
2436             {
2437               if (!s->enhances)
2438                 continue;
2439               if (!pool_installable(pool, s))
2440                 continue;
2441               if (!solver_is_enhancing(solv, s))
2442                 continue;
2443             }
2444           queue_push(&solv->suggestions, i);
2445         }
2446       policy_filter_unwanted(solv, &solv->suggestions, POLICY_MODE_SUGGEST);
2447     }
2448
2449   /* undo removedisabledconflicts */
2450   if (redoq.count)
2451     undo_removedisabledconflicts(solv, &redoq);
2452   queue_free(&redoq);
2453
2454   /* undo job rule disabling */
2455   for (i = 0; i < disabledq.count; i++)
2456     solver_enablerule(solv, solv->rules + disabledq.elements[i]);
2457   queue_free(&disabledq);
2458   map_free(&obsmap);
2459 }
2460
2461 void
2462 solver_calculate_noobsmap(Pool *pool, Queue *job, Map *noobsmap)
2463 {
2464   int i;
2465   Id how, what, select;
2466   Id p, pp;
2467   for (i = 0; i < job->count; i += 2)
2468     {
2469       how = job->elements[i];
2470       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
2471         continue;
2472       what = job->elements[i + 1];
2473       select = how & SOLVER_SELECTMASK;
2474       if (!noobsmap->size)
2475         map_grow(noobsmap, pool->nsolvables);
2476       FOR_JOB_SELECT(p, pp, select, what)
2477         MAPSET(noobsmap, p);
2478     }
2479 }
2480
2481 /*
2482  * add a rule created by a job, record job number and weak flag
2483  */
2484 static inline void
2485 solver_addjobrule(Solver *solv, Id p, Id d, Id job, int weak)
2486 {
2487   solver_addrule(solv, p, d);
2488   queue_push(&solv->ruletojob, job);
2489   if (weak)
2490     queue_push(&solv->weakruleq, solv->nrules - 1);
2491 }
2492
2493 /*
2494  *
2495  * solve job queue
2496  *
2497  */
2498
2499 void
2500 solver_solve(Solver *solv, Queue *job)
2501 {
2502   Pool *pool = solv->pool;
2503   Repo *installed = solv->installed;
2504   int i;
2505   int oldnrules;
2506   Map addedmap;                /* '1' == have rpm-rules for solvable */
2507   Map installcandidatemap;
2508   Id how, what, select, name, weak, p, pp, d;
2509   Queue q;
2510   Solvable *s;
2511   Rule *r;
2512   int now, solve_start;
2513   int hasdupjob = 0;
2514
2515   solve_start = sat_timems(0);
2516
2517   /* log solver options */
2518   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
2519   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);
2520   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
2521   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
2522   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, novirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, pool->novirtualconflicts, pool->allowselfconflicts);
2523   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d, obsoleteusescolors=%d\n", pool->obsoleteusesprovides, pool->implicitobsoleteusesprovides, pool->obsoleteusescolors);
2524   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
2525
2526   /* create whatprovides if not already there */
2527   if (!pool->whatprovides)
2528     pool_createwhatprovides(pool);
2529
2530   /* create obsolete index */
2531   policy_create_obsolete_index(solv);
2532
2533   /* remember job */
2534   queue_free(&solv->job);
2535   queue_init_clone(&solv->job, job);
2536
2537   /* initialize with legacy values */
2538   solv->fixmap_all = solv->fixsystem;
2539   solv->updatemap_all = solv->updatesystem;
2540   solv->droporphanedmap_all = solv->distupgrade_removeunsupported;
2541   solv->dupmap_all = solv->distupgrade;
2542
2543   /*
2544    * create basic rule set of all involved packages
2545    * use addedmap bitmap to make sure we don't create rules twice
2546    */
2547
2548   /* create noobsolete map if needed */
2549   solver_calculate_noobsmap(pool, job, &solv->noobsoletes);
2550
2551   map_init(&addedmap, pool->nsolvables);
2552   MAPSET(&addedmap, SYSTEMSOLVABLE);
2553
2554   map_init(&installcandidatemap, pool->nsolvables);
2555   queue_init(&q);
2556
2557   now = sat_timems(0);
2558   /*
2559    * create rules for all package that could be involved with the solving
2560    * so called: rpm rules
2561    *
2562    */
2563   if (installed)
2564     {
2565       /* check for update/verify jobs as they need to be known early */
2566       for (i = 0; i < job->count; i += 2)
2567         {
2568           how = job->elements[i];
2569           what = job->elements[i + 1];
2570           select = how & SOLVER_SELECTMASK;
2571           switch (how & SOLVER_JOBMASK)
2572             {
2573             case SOLVER_VERIFY:
2574               if (select == SOLVER_SOLVABLE_ALL)
2575                 solv->fixmap_all = 1;
2576               FOR_JOB_SELECT(p, pp, select, what)
2577                 {
2578                   s = pool->solvables + p;
2579                   if (!solv->installed || s->repo != solv->installed)
2580                     continue;
2581                   if (!solv->fixmap.size)
2582                     map_grow(&solv->fixmap, solv->installed->end - solv->installed->start);
2583                   MAPSET(&solv->fixmap, p - solv->installed->start);
2584                 }
2585               break;
2586             case SOLVER_UPDATE:
2587               if (select == SOLVER_SOLVABLE_ALL)
2588                 solv->updatemap_all = 1;
2589               FOR_JOB_SELECT(p, pp, select, what)
2590                 {
2591                   s = pool->solvables + p;
2592                   if (!solv->installed || s->repo != solv->installed)
2593                     continue;
2594                   if (!solv->updatemap.size)
2595                     map_grow(&solv->updatemap, solv->installed->end - solv->installed->start);
2596                   MAPSET(&solv->updatemap, p - solv->installed->start);
2597                 }
2598               break;
2599             default:
2600               break;
2601             }
2602         }
2603
2604       oldnrules = solv->nrules;
2605       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
2606       FOR_REPO_SOLVABLES(installed, p, s)
2607         solver_addrpmrulesforsolvable(solv, s, &addedmap);
2608       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
2609       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
2610       oldnrules = solv->nrules;
2611       FOR_REPO_SOLVABLES(installed, p, s)
2612         solver_addrpmrulesforupdaters(solv, s, &addedmap, 1);
2613       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
2614     }
2615
2616   /*
2617    * create rules for all packages involved in the job
2618    * (to be installed or removed)
2619    */
2620
2621   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
2622   oldnrules = solv->nrules;
2623   for (i = 0; i < job->count; i += 2)
2624     {
2625       how = job->elements[i];
2626       what = job->elements[i + 1];
2627       select = how & SOLVER_SELECTMASK;
2628
2629       switch (how & SOLVER_JOBMASK)
2630         {
2631         case SOLVER_INSTALL:
2632           FOR_JOB_SELECT(p, pp, select, what)
2633             {
2634               MAPSET(&installcandidatemap, p);
2635               solver_addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
2636             }
2637           break;
2638         case SOLVER_DISTUPGRADE:
2639           if (select == SOLVER_SOLVABLE_ALL)
2640             {
2641               solv->dupmap_all = 1;
2642               solv->updatemap_all = 1;
2643             }
2644           if (!solv->dupmap_all)
2645             hasdupjob = 1;
2646           break;
2647         default:
2648           break;
2649         }
2650     }
2651   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
2652
2653
2654   /*
2655    * add rules for suggests, enhances
2656    */
2657   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for suggested/enhanced packages ***\n");
2658   oldnrules = solv->nrules;
2659   solver_addrpmrulesforweak(solv, &addedmap);
2660   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
2661
2662   /*
2663    * first pass done, we now have all the rpm rules we need.
2664    * unify existing rules before going over all job rules and
2665    * policy rules.
2666    * at this point the system is always solvable,
2667    * as an empty system (remove all packages) is a valid solution
2668    */
2669
2670   IF_POOLDEBUG (SAT_DEBUG_STATS)
2671     {
2672       int possible = 0, installable = 0;
2673       for (i = 1; i < pool->nsolvables; i++)
2674         {
2675           if (pool_installable(pool, pool->solvables + i))
2676             installable++;
2677           if (MAPTST(&addedmap, i))
2678             possible++;
2679         }
2680       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
2681     }
2682
2683   solver_unifyrules(solv);                          /* remove duplicate rpm rules */
2684   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
2685
2686   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
2687   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
2688
2689   /* create dup maps if needed. We need the maps early to create our
2690    * update rules */
2691   if (hasdupjob)
2692     solver_createdupmaps(solv);
2693
2694   /*
2695    * create feature rules
2696    *
2697    * foreach installed:
2698    *   create assertion (keep installed, if no update available)
2699    *   or
2700    *   create update rule (A|update1(A)|update2(A)|...)
2701    *
2702    * those are used later on to keep a version of the installed packages in
2703    * best effort mode
2704    */
2705
2706   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
2707   solv->featurerules = solv->nrules;              /* mark start of feature rules */
2708   if (installed)
2709     {
2710       /* foreach possibly installed solvable */
2711       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2712         {
2713           if (s->repo != installed)
2714             {
2715               solver_addrule(solv, 0, 0);       /* create dummy rule */
2716               continue;
2717             }
2718           solver_addupdaterule(solv, s, 1);    /* allow s to be updated */
2719         }
2720       /* make sure we accounted for all rules */
2721       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
2722     }
2723   solv->featurerules_end = solv->nrules;
2724
2725     /*
2726      * Add update rules for installed solvables
2727      *
2728      * almost identical to feature rules
2729      * except that downgrades/archchanges/vendorchanges are not allowed
2730      */
2731
2732   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
2733   solv->updaterules = solv->nrules;
2734
2735   if (installed)
2736     { /* foreach installed solvables */
2737       /* we create all update rules, but disable some later on depending on the job */
2738       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
2739         {
2740           Rule *sr;
2741
2742           if (s->repo != installed)
2743             {
2744               solver_addrule(solv, 0, 0);       /* create dummy rule */
2745               continue;
2746             }
2747           solver_addupdaterule(solv, s, 0);     /* allowall = 0: downgrades not allowed */
2748           /*
2749            * check for and remove duplicate
2750            */
2751           r = solv->rules + solv->nrules - 1;           /* r: update rule */
2752           sr = r - (installed->end - installed->start); /* sr: feature rule */
2753           /* it's orphaned if there is no feature rule or the feature rule
2754            * consists just of the installed package */
2755           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
2756             queue_push(&solv->orphaned, i);
2757           if (!r->p)
2758             {
2759               assert(solv->dupmap_all && !sr->p);
2760               continue;
2761             }
2762           if (!solver_samerule(solv, r, sr))
2763             {
2764               /* identical rule, kill unneeded one */
2765               if (solv->allowuninstall)
2766                 {
2767                   /* keep feature rule, make it weak */
2768                   memset(r, 0, sizeof(*r));
2769                   queue_push(&solv->weakruleq, sr - solv->rules);
2770                 }
2771               else
2772                 {
2773                   /* keep update rule */
2774                   memset(sr, 0, sizeof(*sr));
2775                 }
2776             }
2777           else if (solv->allowuninstall)
2778             {
2779               /* make both feature and update rule weak */
2780               queue_push(&solv->weakruleq, r - solv->rules);
2781               queue_push(&solv->weakruleq, sr - solv->rules);
2782             }
2783           else
2784             solver_disablerule(solv, sr);
2785         }
2786       /* consistency check: we added a rule for _every_ installed solvable */
2787       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
2788     }
2789   solv->updaterules_end = solv->nrules;
2790
2791
2792   /*
2793    * now add all job rules
2794    */
2795
2796   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
2797
2798   solv->jobrules = solv->nrules;
2799   for (i = 0; i < job->count; i += 2)
2800     {
2801       oldnrules = solv->nrules;
2802
2803       how = job->elements[i];
2804       what = job->elements[i + 1];
2805       weak = how & SOLVER_WEAK;
2806       select = how & SOLVER_SELECTMASK;
2807       switch (how & SOLVER_JOBMASK)
2808         {
2809         case SOLVER_INSTALL:
2810           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2811           if (select == SOLVER_SOLVABLE)
2812             {
2813               p = what;
2814               d = 0;
2815             }
2816           else
2817             {
2818               queue_empty(&q);
2819               FOR_JOB_SELECT(p, pp, select, what)
2820                 queue_push(&q, p);
2821               if (!q.count)
2822                 {
2823                   /* no candidate found, make this an impossible rule */
2824                   queue_push(&q, -SYSTEMSOLVABLE);
2825                 }
2826               p = queue_shift(&q);      /* get first candidate */
2827               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
2828             }
2829           solver_addjobrule(solv, p, d, i, weak);
2830           break;
2831         case SOLVER_ERASE:
2832           POOL_DEBUG(SAT_DEBUG_JOB, "job: %s%serase %s\n", weak ? "weak " : "", how & SOLVER_CLEANDEPS ? "clean deps " : "", solver_select2str(pool, select, what));
2833           if ((how & SOLVER_CLEANDEPS) != 0 && !solv->cleandepsmap.size && solv->installed)
2834             map_grow(&solv->cleandepsmap, solv->installed->end - solv->installed->start);
2835           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
2836             {
2837               /* special case for "erase a specific solvable": we also
2838                * erase all other solvables with that name, so that they
2839                * don't get picked up as replacement */
2840               /* XXX: look also at packages that obsolete this package? */
2841               name = pool->solvables[what].name;
2842               FOR_PROVIDES(p, pp, name)
2843                 {
2844                   if (p == what)
2845                     continue;
2846                   s = pool->solvables + p;
2847                   if (s->name != name)
2848                     continue;
2849                   /* keep other versions installed */
2850                   if (s->repo == solv->installed)
2851                     continue;
2852                   /* keep installcandidates of other jobs */
2853                   if (MAPTST(&installcandidatemap, p))
2854                     continue;
2855                   solver_addjobrule(solv, -p, 0, i, weak);      /* remove by id */
2856                 }
2857             }
2858           FOR_JOB_SELECT(p, pp, select, what)
2859             solver_addjobrule(solv, -p, 0, i, weak);
2860           break;
2861
2862         case SOLVER_UPDATE:
2863           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2864           break;
2865         case SOLVER_VERIFY:
2866           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sverify %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2867           break;
2868         case SOLVER_WEAKENDEPS:
2869           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2870           if (select != SOLVER_SOLVABLE)
2871             break;
2872           s = pool->solvables + what;
2873           weaken_solvable_deps(solv, what);
2874           break;
2875         case SOLVER_NOOBSOLETES:
2876           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2877           break;
2878         case SOLVER_LOCK:
2879           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
2880           FOR_JOB_SELECT(p, pp, select, what)
2881             {
2882               s = pool->solvables + p;
2883               solver_addjobrule(solv, installed && s->repo == installed ? p : -p, 0, i, weak);
2884             }
2885           break;
2886         case SOLVER_DISTUPGRADE:
2887           POOL_DEBUG(SAT_DEBUG_JOB, "job: distupgrade %s\n", solver_select2str(pool, select, what));
2888           break;
2889         case SOLVER_DROP_ORPHANED:
2890           POOL_DEBUG(SAT_DEBUG_JOB, "job: drop orphaned %s\n", solver_select2str(pool, select, what));
2891           if (select == SOLVER_SOLVABLE_ALL)
2892             solv->droporphanedmap_all = 1;
2893           FOR_JOB_SELECT(p, pp, select, what)
2894             {
2895               s = pool->solvables + p;
2896               if (!installed || s->repo != installed)
2897                 continue;
2898               if (!solv->droporphanedmap.size)
2899                 map_grow(&solv->droporphanedmap, installed->end - installed->start);
2900               MAPSET(&solv->droporphanedmap, p - installed->start);
2901             }
2902           break;
2903         case SOLVER_USERINSTALLED:
2904           POOL_DEBUG(SAT_DEBUG_JOB, "job: user installed %s\n", solver_select2str(pool, select, what));
2905           break;
2906         default:
2907           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
2908           break;
2909         }
2910
2911         /*
2912          * debug
2913          */
2914
2915       IF_POOLDEBUG (SAT_DEBUG_JOB)
2916         {
2917           int j;
2918           if (solv->nrules == oldnrules)
2919             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
2920           for (j = oldnrules; j < solv->nrules; j++)
2921             {
2922               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
2923               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
2924             }
2925         }
2926     }
2927   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
2928   solv->jobrules_end = solv->nrules;
2929
2930   /* now create infarch and dup rules */
2931   if (!solv->noinfarchcheck)
2932     {
2933       solver_addinfarchrules(solv, &addedmap);
2934       if (pool->obsoleteusescolors)
2935         {
2936           /* currently doesn't work well with infarch rules, so make
2937            * them weak */
2938           for (i = solv->infarchrules; i < solv->infarchrules_end; i++)
2939             queue_push(&solv->weakruleq, i);
2940         }
2941     }
2942   else
2943     solv->infarchrules = solv->infarchrules_end = solv->nrules;
2944
2945   if (hasdupjob)
2946     {
2947       solver_addduprules(solv, &addedmap);
2948       solver_freedupmaps(solv); /* no longer needed */
2949     }
2950   else
2951     solv->duprules = solv->duprules_end = solv->nrules;
2952
2953   if (1)
2954     solver_addchoicerules(solv);
2955   else
2956     solv->choicerules = solv->choicerules_end = solv->nrules;
2957
2958   /* all rules created
2959    * --------------------------------------------------------------
2960    * prepare for solving
2961    */
2962
2963   /* free unneeded memory */
2964   map_free(&addedmap);
2965   map_free(&installcandidatemap);
2966   queue_free(&q);
2967
2968   POOL_DEBUG(SAT_DEBUG_STATS, "%d rpm rules, %d job rules, %d infarch rules, %d dup rules, %d choice rules\n", solv->rpmrules_end - 1, solv->jobrules_end - solv->jobrules, solv->infarchrules_end - solv->infarchrules, solv->duprules_end - solv->duprules, solv->choicerules_end - solv->choicerules);
2969
2970   /* create weak map */
2971   map_init(&solv->weakrulemap, solv->nrules);
2972   for (i = 0; i < solv->weakruleq.count; i++)
2973     {
2974       p = solv->weakruleq.elements[i];
2975       MAPSET(&solv->weakrulemap, p);
2976     }
2977
2978   /* all new rules are learnt after this point */
2979   solv->learntrules = solv->nrules;
2980
2981   /* create watches chains */
2982   makewatches(solv);
2983
2984   /* create assertion index. it is only used to speed up
2985    * makeruledecsions() a bit */
2986   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
2987     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
2988       queue_push(&solv->ruleassertions, i);
2989
2990   /* disable update rules that conflict with our job */
2991   solver_disablepolicyrules(solv);
2992
2993   /* make initial decisions based on assertion rules */
2994   makeruledecisions(solv);
2995   POOL_DEBUG(SAT_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count);
2996
2997   /*
2998    * ********************************************
2999    * solve!
3000    * ********************************************
3001    */
3002
3003   now = sat_timems(0);
3004   solver_run_sat(solv, 1, solv->dontinstallrecommended ? 0 : 1);
3005   POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
3006
3007   /*
3008    * calculate recommended/suggested packages
3009    */
3010   findrecommendedsuggested(solv);
3011
3012   /*
3013    * prepare solution queue if there were problems
3014    */
3015   solver_prepare_solutions(solv);
3016
3017   /*
3018    * finally prepare transaction info
3019    */
3020   transaction_calculate(&solv->trans, &solv->decisionq, &solv->noobsoletes);
3021
3022   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d problems, %d learned rules, %d unsolvable\n", solv->problems.count / 2, solv->stats_learned, solv->stats_unsolvable);
3023   POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
3024 }
3025
3026 /***********************************************************************/
3027 /* disk usage computations */
3028
3029 /*-------------------------------------------------------------------
3030  *
3031  * calculate DU changes
3032  */
3033
3034 void
3035 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
3036 {
3037   Map installedmap;
3038
3039   solver_create_state_maps(solv, &installedmap, 0);
3040   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
3041   map_free(&installedmap);
3042 }
3043
3044
3045 /*-------------------------------------------------------------------
3046  *
3047  * calculate changes in install size
3048  */
3049
3050 int
3051 solver_calc_installsizechange(Solver *solv)
3052 {
3053   Map installedmap;
3054   int change;
3055
3056   solver_create_state_maps(solv, &installedmap, 0);
3057   change = pool_calc_installsizechange(solv->pool, &installedmap);
3058   map_free(&installedmap);
3059   return change;
3060 }
3061
3062 void
3063 solver_trivial_installable(Solver *solv, Queue *pkgs, Queue *res)
3064 {
3065   Map installedmap;
3066   solver_create_state_maps(solv, &installedmap, 0);
3067   pool_trivial_installable_noobsoletesmap(solv->pool, &installedmap, pkgs, res, solv->noobsoletes.size ? &solv->noobsoletes : 0);
3068   map_free(&installedmap);
3069 }
3070