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 "evr.h"
  25 #include "policy.h"
  26 #include "solverdebug.h"
  27
  28 #define RULES_BLOCK 63
  29
  30 /********************************************************************
  31  *
  32  * dependency check helpers
  33  *
  34  */
  35
  36 /*-------------------------------------------------------------------
  37  * handle split provides
  38  */
  39
  40 int
  41 solver_splitprovides(Solver *solv, Id dep)
  42 {
  43   Pool *pool = solv->pool;
  44   Id p, pp;
  45   Reldep *rd;
  46   Solvable *s;
  47
  48   if (!solv->dosplitprovides || !solv->installed)
  49     return 0;
  50   if (!ISRELDEP(dep))
  51     return 0;
  52   rd = GETRELDEP(pool, dep);
  53   if (rd->flags != REL_WITH)
  54     return 0;
  55   FOR_PROVIDES(p, pp, dep)
  56     {
  57       s = pool->solvables + p;
  58       if (s->repo == solv->installed && s->name == rd->name)
  59         return 1;
  60     }
  61   return 0;
  62 }
  63
  64
  65 /*-------------------------------------------------------------------
  66  * solver_dep_installed
  67  */
  68
  69 int
  70 solver_dep_installed(Solver *solv, Id dep)
  71 {
  72 #if 0
  73   Pool *pool = solv->pool;
  74   Id p, pp;
  75
  76   if (ISRELDEP(dep))
  77     {
  78       Reldep *rd = GETRELDEP(pool, dep);
  79       if (rd->flags == REL_AND)
  80         {
  81           if (!solver_dep_installed(solv, rd->name))
  82             return 0;
  83           return solver_dep_installed(solv, rd->evr);
  84         }
  85       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
  86         return solver_dep_installed(solv, rd->evr);
  87     }
  88   FOR_PROVIDES(p, pp, dep)
  89     {
  90       if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
  91         return 1;
  92     }
  93 #endif
  94   return 0;
  95 }
  96
  97
  98 /*-------------------------------------------------------------------
  99  * Check if dependenc is possible
 100  *
 101  * this mirrors solver_dep_fulfilled
 102  * but uses map m instead of the decisionmap
 103  */
 104
 105 static inline int
 106 dep_possible(Solver *solv, Id dep, Map *m)
 107 {
 108   Pool *pool = solv->pool;
 109   Id p, pp;
 110
 111   if (ISRELDEP(dep))
 112     {
 113       Reldep *rd = GETRELDEP(pool, dep);
 114       if (rd->flags == REL_AND)
 115         {
 116           if (!dep_possible(solv, rd->name, m))
 117             return 0;
 118           return dep_possible(solv, rd->evr, m);
 119         }
 120       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_SPLITPROVIDES)
 121         return solver_splitprovides(solv, rd->evr);
 122       if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
 123         return solver_dep_installed(solv, rd->evr);
 124     }
 125   FOR_PROVIDES(p, pp, dep)
 126     {
 127       if (MAPTST(m, p))
 128         return 1;
 129     }
 130   return 0;
 131 }
 132
 133 /********************************************************************
 134  *
 135  * Rule handling
 136  *
 137  * - unify rules, remove duplicates
 138  */
 139
 140 static Pool *unifyrules_sortcmp_data;
 141
 142 /*-------------------------------------------------------------------
 143  *
 144  * compare rules for unification sort
 145  *
 146  */
 147
 148 static int
 149 unifyrules_sortcmp(const void *ap, const void *bp)
 150 {
 151   Pool *pool = unifyrules_sortcmp_data;
 152   Rule *a = (Rule *)ap;
 153   Rule *b = (Rule *)bp;
 154   Id *ad, *bd;
 155   int x;
 156
 157   x = a->p - b->p;
 158   if (x)
 159     return x;                          /* p differs */
 160
 161   /* identical p */
 162   if (a->d == 0 && b->d == 0)
 163     return a->w2 - b->w2;              /* assertion: return w2 diff */
 164
 165   if (a->d == 0)                       /* a is assertion, b not */
 166     {
 167       x = a->w2 - pool->whatprovidesdata[b->d];
 168       return x ? x : -1;
 169     }
 170
 171   if (b->d == 0)                       /* b is assertion, a not */
 172     {
 173       x = pool->whatprovidesdata[a->d] - b->w2;
 174       return x ? x : 1;
 175     }
 176
 177   /* compare whatprovidesdata */
 178   ad = pool->whatprovidesdata + a->d;
 179   bd = pool->whatprovidesdata + b->d;
 180   while (*bd)
 181     if ((x = *ad++ - *bd++) != 0)
 182       return x;
 183   return *ad;
 184 }
 185
 186
 187 /*-------------------------------------------------------------------
 188  *
 189  * unify rules
 190  * go over all rules and remove duplicates
 191  */
 192
 193 static void
 194 unifyrules(Solver *solv)
 195 {
 196   Pool *pool = solv->pool;
 197   int i, j;
 198   Rule *ir, *jr;
 199
 200   if (solv->nrules <= 1)               /* nothing to unify */
 201     return;
 202
 203   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- unifyrules -----\n");
 204
 205   /* sort rules first */
 206   unifyrules_sortcmp_data = solv->pool;
 207   qsort(solv->rules + 1, solv->nrules - 1, sizeof(Rule), unifyrules_sortcmp);
 208
 209   /* prune rules
 210    * i = unpruned
 211    * j = pruned
 212    */
 213   jr = 0;
 214   for (i = j = 1, ir = solv->rules + i; i < solv->nrules; i++, ir++)
 215     {
 216       if (jr && !unifyrules_sortcmp(ir, jr))
 217         continue;                      /* prune! */
 218       jr = solv->rules + j++;          /* keep! */
 219       if (ir != jr)
 220         *jr = *ir;
 221     }
 222
 223   /* reduced count from nrules to j rules */
 224   POOL_DEBUG(SAT_DEBUG_STATS, "pruned rules from %d to %d\n", solv->nrules, j);
 225
 226   /* adapt rule buffer */
 227   solv->nrules = j;
 228   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
 229     /*
 230      * debug: statistics
 231      */
 232   IF_POOLDEBUG (SAT_DEBUG_STATS)
 233     {
 234       int binr = 0;
 235       int lits = 0;
 236       Id *dp;
 237       Rule *r;
 238
 239       for (i = 1; i < solv->nrules; i++)
 240         {
 241           r = solv->rules + i;
 242           if (r->d == 0)
 243             binr++;
 244           else
 245             {
 246               dp = solv->pool->whatprovidesdata + r->d;
 247               while (*dp++)
 248                 lits++;
 249             }
 250         }
 251       POOL_DEBUG(SAT_DEBUG_STATS, "  binary: %d\n", binr);
 252       POOL_DEBUG(SAT_DEBUG_STATS, "  normal: %d, %d literals\n", solv->nrules - 1 - binr, lits);
 253     }
 254   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- unifyrules end -----\n");
 255 }
 256
 257 #if 0
 258
 259 /*
 260  * hash rule
 261  */
 262
 263 static Hashval
 264 hashrule(Solver *solv, Id p, Id d, int n)
 265 {
 266   unsigned int x = (unsigned int)p;
 267   int *dp;
 268
 269   if (n <= 1)
 270     return (x * 37) ^ (unsigned int)d;
 271   dp = solv->pool->whatprovidesdata + d;
 272   while (*dp)
 273     x = (x * 37) ^ (unsigned int)*dp++;
 274   return x;
 275 }
 276 #endif
 277
 278
 279 /*-------------------------------------------------------------------
 280  *
 281  */
 282
 283 /*
 284  * add rule
 285  *  p = direct literal; always < 0 for installed rpm rules
 286  *  d, if < 0 direct literal, if > 0 offset into whatprovides, if == 0 rule is assertion (look at p only)
 287  *
 288  *
 289  * A requires b, b provided by B1,B2,B3 => (-A|B1|B2|B3)
 290  *
 291  * p < 0 : pkg id of A
 292  * d > 0 : Offset in whatprovidesdata (list of providers of b)
 293  *
 294  * A conflicts b, b provided by B1,B2,B3 => (-A|-B1), (-A|-B2), (-A|-B3)
 295  * p < 0 : pkg id of A
 296  * d < 0 : Id of solvable (e.g. B1)
 297  *
 298  * d == 0: unary rule, assertion => (A) or (-A)
 299  *
 300  *   Install:    p > 0, d = 0   (A)             user requested install
 301  *   Remove:     p < 0, d = 0   (-A)            user requested remove
 302  *   Requires:   p < 0, d > 0   (-A|B1|B2|...)  d: <list of providers for requirement of p>
 303  *   Updates:    p > 0, d > 0   (A|B1|B2|...)   d: <list of updates for solvable p>
 304  *   Conflicts:  p < 0, d < 0   (-A|-B)         either p (conflict issuer) or d (conflict provider) (binary rule)
 305  *   ?           p > 0, d < 0   (A|-B)
 306  *   No-op ?:    p = 0, d = 0   (null)          (used as policy rule placeholder)
 307  *
 308  *   resulting watches:
 309  *   ------------------
 310  *   Direct assertion (no watch needed)( if d <0 ) --> d = 0, w1 = p, w2 = 0
 311  *   Binary rule: p = first literal, d = 0, w2 = second literal, w1 = p
 312  *   every other : w1 = p, w2 = whatprovidesdata[d];
 313  *   Disabled rule: w1 = 0
 314  *
 315  *   always returns a rule for non-rpm rules
 316  */
 317
 318 static Rule *
 319 addrule(Solver *solv, Id p, Id d)
 320 {
 321   Pool *pool = solv->pool;
 322   Rule *r = 0;
 323   Id *dp = 0;
 324
 325   int n = 0;                           /* number of literals in rule - 1
 326                                           0 = direct assertion (single literal)
 327                                           1 = binary rule
 328                                           >1 =
 329                                         */
 330
 331   /* it often happenes that requires lead to adding the same rpm rule
 332    * multiple times, so we prune those duplicates right away to make
 333    * the work for unifyrules a bit easier */
 334
 335   if (solv->nrules                      /* we already have rules */
 336       && !solv->rpmrules_end)           /* but are not done with rpm rules */
 337     {
 338       r = solv->rules + solv->nrules - 1;   /* get the last added rule */
 339       if (r->p == p && r->d == d && d != 0)   /* identical and not user requested */
 340         return r;
 341     }
 342
 343     /*
 344      * compute number of literals (n) in rule
 345      */
 346
 347   if (d < 0)
 348     {
 349       /* always a binary rule */
 350       if (p == d)
 351         return 0;                      /* ignore self conflict */
 352       n = 1;
 353     }
 354   else if (d > 0)
 355     {
 356       for (dp = pool->whatprovidesdata + d; *dp; dp++, n++)
 357         if (*dp == -p)
 358           return 0;                     /* rule is self-fulfilling */
 359
 360       if (n == 1)   /* have single provider */
 361         d = dp[-1];                     /* take single literal */
 362     }
 363
 364 #if 0
 365   if (n == 0 && !solv->rpmrules_end)
 366     {
 367       /* this is a rpm rule assertion, we do not have to allocate it */
 368       /* it can be identified by a level of 1 and a zero reason */
 369       /* we must not drop those rules from the decisionq when rewinding! */
 370       assert(p < 0);
 371       assert(solv->decisionmap[-p] == 0 || solv->decisionmap[-p] == -1);
 372       if (solv->decisionmap[-p])
 373         return 0;       /* already got that one */
 374       queue_push(&solv->decisionq, p);
 375       queue_push(&solv->decisionq_why, 0);
 376       solv->decisionmap[-p] = -1;
 377       return 0;
 378     }
 379 #endif
 380
 381   if (n == 1 && p > d && !solv->rpmrules_end)
 382     {
 383       /* smallest literal first so we can find dups */
 384       n = p; p = d; d = n;             /* p <-> d */
 385       n = 1;                           /* re-set n, was used as temp var */
 386     }
 387
 388     /*
 389      * check for duplicate
 390      */
 391
 392   /* check if the last added rule (r) is exactly the same as what we're looking for. */
 393   if (r && n == 1 && !r->d && r->p == p && r->w2 == d)
 394     return r;  /* binary rule */
 395
 396     /* have n-ary rule with same first literal, check other literals */
 397   if (r && n > 1 && r->d && r->p == p)
 398     {
 399       /* Rule where d is an offset in whatprovidesdata */
 400       Id *dp2;
 401       if (d == r->d)
 402         return r;
 403       dp2 = pool->whatprovidesdata + r->d;
 404       for (dp = pool->whatprovidesdata + d; *dp; dp++, dp2++)
 405         if (*dp != *dp2)
 406           break;
 407       if (*dp == *dp2)
 408         return r;
 409    }
 410
 411     /*
 412      * allocate new rule
 413      */
 414
 415   /* extend rule buffer */
 416   solv->rules = sat_extend(solv->rules, solv->nrules, 1, sizeof(Rule), RULES_BLOCK);
 417   r = solv->rules + solv->nrules++;    /* point to rule space */
 418
 419     /*
 420      * r = new rule
 421      */
 422
 423   r->p = p;
 424   if (n == 0)
 425     {
 426       /* direct assertion, no watch needed */
 427       r->d = 0;
 428       r->w1 = p;
 429       r->w2 = 0;
 430     }
 431   else if (n == 1)
 432     {
 433       /* binary rule */
 434       r->d = 0;
 435       r->w1 = p;
 436       r->w2 = d;
 437     }
 438   else
 439     {
 440       r->d = d;
 441       r->w1 = p;
 442       r->w2 = pool->whatprovidesdata[d];
 443     }
 444   r->n1 = 0;
 445   r->n2 = 0;
 446
 447   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
 448     {
 449       POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "  Add rule: ");
 450       solver_printrule(solv, SAT_DEBUG_RULE_CREATION, r);
 451     }
 452
 453   return r;
 454 }
 455
 456 /*-------------------------------------------------------------------
 457  * disable rule
 458  */
 459
 460 static inline void
 461 disablerule(Solver *solv, Rule *r)
 462 {
 463   if (r->d >= 0)
 464     r->d = -r->d - 1;
 465 }
 466
 467 /*-------------------------------------------------------------------
 468  * enable rule
 469  */
 470
 471 static inline void
 472 enablerule(Solver *solv, Rule *r)
 473 {
 474   if (r->d < 0)
 475     r->d = -r->d - 1;
 476 }
 477
 478
 479 /**********************************************************************************/
 480
 481 /* a problem is an item on the solver's problem list. It can either be >0, in that
 482  * case it is a update rule, or it can be <0, which makes it refer to a job
 483  * consisting of multiple job rules.
 484  */
 485
 486 static void
 487 disableproblem(Solver *solv, Id v)
 488 {
 489   Rule *r;
 490   int i;
 491   Id *jp;
 492
 493   if (v > 0)
 494     {
 495       disablerule(solv, solv->rules + v);
 496       return;
 497     }
 498   v = -(v + 1);
 499   jp = solv->ruletojob.elements;
 500   for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
 501     if (*jp == v)
 502       disablerule(solv, r);
 503 }
 504
 505 /*-------------------------------------------------------------------
 506  * enableproblem
 507  */
 508
 509 static void
 510 enableproblem(Solver *solv, Id v)
 511 {
 512   Rule *r;
 513   int i;
 514   Id *jp;
 515
 516   if (v > 0)
 517     {
 518       if (v >= solv->featurerules && v < solv->featurerules_end)
 519         {
 520           /* do not enable feature rule if update rule is enabled */
 521           r = solv->rules + (v - solv->featurerules + solv->updaterules);
 522           if (r->d >= 0)
 523             return;
 524         }
 525       enablerule(solv, solv->rules + v);
 526       if (v >= solv->updaterules && v < solv->updaterules_end)
 527         {
 528           /* disable feature rule when enabling update rule */
 529           r = solv->rules + (v - solv->updaterules + solv->featurerules);
 530           if (r->p)
 531             disablerule(solv, r);
 532         }
 533       return;
 534     }
 535   v = -(v + 1);
 536   jp = solv->ruletojob.elements;
 537   for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++, jp++)
 538     if (*jp == v)
 539       enablerule(solv, r);
 540 }
 541
 542
 543 /************************************************************************/
 544
 545 /*
 546  * make assertion rules into decisions
 547  *
 548  * go through update and job rules and add direct assertions
 549  * to the decisionqueue. If we find a conflict, disable rules and
 550  * add them to problem queue.
 551  */
 552
 553 static void
 554 makeruledecisions(Solver *solv)
 555 {
 556   Pool *pool = solv->pool;
 557   int i, ri, ii;
 558   Rule *r, *rr;
 559   Id v, vv;
 560   int decisionstart;
 561
 562   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
 563
 564   decisionstart = solv->decisionq.count;
 565   for (ii = 0; ii < solv->ruleassertions.count; ii++)
 566     {
 567       ri = solv->ruleassertions.elements[ii];
 568       r = solv->rules + ri;
 569
 570       if (r->d < 0 || !r->p || r->w2)   /* disabled, dummy or no assertion */
 571         continue;
 572       /* do weak rules in phase 2 */
 573       if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri))
 574         continue;
 575
 576       v = r->p;
 577       vv = v > 0 ? v : -v;
 578
 579       if (!solv->decisionmap[vv])          /* if not yet decided */
 580         {
 581             /*
 582              * decide !
 583              */
 584           queue_push(&solv->decisionq, v);
 585           queue_push(&solv->decisionq_why, r - solv->rules);
 586           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 587           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
 588             {
 589               Solvable *s = solv->pool->solvables + vv;
 590               if (v < 0)
 591                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", solvable2str(solv->pool, s));
 592               else
 593                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing  %s (assertion)\n", solvable2str(solv->pool, s));
 594             }
 595           continue;
 596         }
 597         /*
 598          * check previous decision: is it sane ?
 599          */
 600
 601       if (v > 0 && solv->decisionmap[vv] > 0)    /* ok to install */
 602         continue;
 603       if (v < 0 && solv->decisionmap[vv] < 0)    /* ok to remove */
 604         continue;
 605
 606         /*
 607          * found a conflict!
 608          *
 609          * The rule (r) we're currently processing says something
 610          * different (v = r->p) than a previous decision (decisionmap[abs(v)])
 611          * on this literal
 612          */
 613
 614       if (ri >= solv->learntrules)
 615         {
 616           /* conflict with a learnt rule */
 617           /* can happen when packages cannot be installed for
 618            * multiple reasons. */
 619           /* we disable the learnt rule in this case */
 620           disablerule(solv, r);
 621           continue;
 622         }
 623
 624         /*
 625          * find the decision which is the "opposite" of the rule
 626          */
 627
 628       for (i = 0; i < solv->decisionq.count; i++)
 629         if (solv->decisionq.elements[i] == -v)
 630           break;
 631       assert(i < solv->decisionq.count);         /* assert that we found it */
 632
 633         /*
 634          * conflict with system solvable ?
 635          */
 636
 637       if (v == -SYSTEMSOLVABLE) {
 638         /* conflict with system solvable */
 639         queue_push(&solv->problems, solv->learnt_pool.count);
 640         queue_push(&solv->learnt_pool, ri);
 641         queue_push(&solv->learnt_pool, 0);
 642         POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri);
 643         if  (ri >= solv->jobrules && ri < solv->jobrules_end)
 644           v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 645         else
 646           v = ri;
 647         queue_push(&solv->problems, v);
 648         queue_push(&solv->problems, 0);
 649         disableproblem(solv, v);
 650         continue;
 651       }
 652
 653       assert(solv->decisionq_why.elements[i]);
 654
 655         /*
 656          * conflict with an rpm rule ?
 657          */
 658
 659       if (solv->decisionq_why.elements[i] < solv->rpmrules_end)
 660         {
 661           /* conflict with rpm rule assertion */
 662           queue_push(&solv->problems, solv->learnt_pool.count);
 663           queue_push(&solv->learnt_pool, ri);
 664           queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
 665           queue_push(&solv->learnt_pool, 0);
 666           assert(v > 0 || v == -SYSTEMSOLVABLE);
 667           POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri);
 668           if (ri >= solv->jobrules && ri < solv->jobrules_end)
 669             v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
 670           else
 671             v = ri;
 672           queue_push(&solv->problems, v);
 673           queue_push(&solv->problems, 0);
 674           disableproblem(solv, v);
 675           continue;
 676         }
 677
 678         /*
 679          * conflict with another job or update/feature rule
 680          */
 681
 682       /* record proof */
 683       queue_push(&solv->problems, solv->learnt_pool.count);
 684       queue_push(&solv->learnt_pool, ri);
 685       queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
 686       queue_push(&solv->learnt_pool, 0);
 687
 688       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv);
 689
 690         /*
 691          * push all of our rules (can only be feature or job rules)
 692          * asserting this literal on the problem stack
 693          */
 694
 695       for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++)
 696         {
 697           if (rr->d < 0                          /* disabled */
 698               || rr->w2)                         /*  or no assertion */
 699             continue;
 700           if (rr->p != vv                        /* not affecting the literal */
 701               && rr->p != -vv)
 702             continue;
 703           if (MAPTST(&solv->weakrulemap, i))     /* weak: silently ignore */
 704             continue;
 705
 706           POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
 707
 708           solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + i);
 709
 710           v = i;
 711             /* is is a job rule ? */
 712           if (i >= solv->jobrules && i < solv->jobrules_end)
 713             v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
 714
 715           queue_push(&solv->problems, v);
 716           disableproblem(solv, v);
 717         }
 718       queue_push(&solv->problems, 0);
 719
 720        /*
 721         * start over
 722         * (back up from decisions)
 723         */
 724       while (solv->decisionq.count > decisionstart)
 725         {
 726           v = solv->decisionq.elements[--solv->decisionq.count];
 727           --solv->decisionq_why.count;
 728           vv = v > 0 ? v : -v;
 729           solv->decisionmap[vv] = 0;
 730         }
 731       ii = -1; /* restarts loop at 0 */
 732     }
 733
 734     /*
 735      * phase 2: now do the weak assertions
 736      */
 737   for (ii = 0; ii < solv->ruleassertions.count; ii++)
 738     {
 739       ri = solv->ruleassertions.elements[ii];
 740       r = solv->rules + ri;
 741       if (r->d < 0 || r->w2)                     /* disabled or no assertion */
 742         continue;
 743       if (!MAPTST(&solv->weakrulemap, ri))       /* skip non-weak */
 744         continue;
 745       v = r->p;
 746       vv = v > 0 ? v : -v;
 747         /*
 748          * decide !
 749          * (if not yet decided)
 750          */
 751       if (!solv->decisionmap[vv])
 752         {
 753           queue_push(&solv->decisionq, v);
 754           queue_push(&solv->decisionq_why, r - solv->rules);
 755           solv->decisionmap[vv] = v > 0 ? 1 : -1;
 756           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
 757             {
 758               Solvable *s = solv->pool->solvables + vv;
 759               if (v < 0)
 760                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", solvable2str(solv->pool, s));
 761               else
 762                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing  %s (weak assertion)\n", solvable2str(solv->pool, s));
 763             }
 764           continue;
 765         }
 766         /*
 767          * previously decided, sane ?
 768          */
 769       if (v > 0 && solv->decisionmap[vv] > 0)
 770         continue;
 771       if (v < 0 && solv->decisionmap[vv] < 0)
 772         continue;
 773
 774       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling ");
 775       solver_printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
 776       disablerule(solv, r);
 777     }
 778
 779   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);
 780 }
 781
 782
 783 /*-------------------------------------------------------------------
 784  * enable/disable learnt rules
 785  *
 786  * we have enabled or disabled some of our rules. We now reenable all
 787  * of our learnt rules but the ones that were learnt from rules that
 788  * are now disabled.
 789  */
 790 static void
 791 enabledisablelearntrules(Solver *solv)
 792 {
 793   Pool *pool = solv->pool;
 794   Rule *r;
 795   Id why, *whyp;
 796   int i;
 797
 798   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n");
 799   for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
 800     {
 801       whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
 802       while ((why = *whyp++) != 0)
 803         {
 804           assert(why > 0 && why < i);
 805           if (solv->rules[why].d < 0)
 806             break;
 807         }
 808       /* why != 0: we found a disabled rule, disable the learnt rule */
 809       if (why && r->d >= 0)
 810         {
 811           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
 812             {
 813               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "disabling ");
 814               solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
 815             }
 816           disablerule(solv, r);
 817         }
 818       else if (!why && r->d < 0)
 819         {
 820           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
 821             {
 822               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "re-enabling ");
 823               solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
 824             }
 825           enablerule(solv, r);
 826         }
 827     }
 828 }
 829
 830
 831 /*-------------------------------------------------------------------
 832  * enable weak rules
 833  *
 834  * Enable all rules, except learnt rules, which are
 835  * - disabled and weak (set in weakrulemap)
 836  *
 837  */
 838
 839 static void
 840 enableweakrules(Solver *solv)
 841 {
 842   int i;
 843   Rule *r;
 844
 845   for (i = 1, r = solv->rules + i; i < solv->learntrules; i++, r++)
 846     {
 847       if (r->d >= 0) /* skip non-direct literals */
 848         continue;
 849       if (!MAPTST(&solv->weakrulemap, i))
 850         continue;
 851       enablerule(solv, r);
 852     }
 853 }
 854
 855
 856 /* FIXME: bad code ahead, replace as soon as possible */
 857 /* FIXME: should probably look at SOLVER_INSTALL|SOLVABLE_ONE_OF */
 858
 859 /*-------------------------------------------------------------------
 860  * disable update rules
 861  */
 862
 863 static void
 864 disableupdaterules(Solver *solv, Queue *job, int jobidx)
 865 {
 866   Pool *pool = solv->pool;
 867   int i, j;
 868   Id how, select, what, p, pp;
 869   Solvable *s;
 870   Repo *installed;
 871   Rule *r;
 872   Id lastjob = -1;
 873
 874   installed = solv->installed;
 875   if (!installed)
 876     return;
 877
 878   if (jobidx != -1)
 879     {
 880       how = job->elements[jobidx];
 881       select = how & SOLVER_SELECTMASK;
 882       switch (how & SOLVER_JOBMASK)
 883         {
 884         case SOLVER_ERASE:
 885           break;
 886         case SOLVER_INSTALL:
 887           if (select != SOLVER_SOLVABLE)
 888             return;
 889           break;
 890         default:
 891           return;
 892         }
 893     }
 894   /* go through all enabled job rules */
 895   MAPZERO(&solv->noupdate);
 896   for (i = solv->jobrules; i < solv->jobrules_end; i++)
 897     {
 898       r = solv->rules + i;
 899       if (r->d < 0)     /* disabled? */
 900         continue;
 901       j = solv->ruletojob.elements[i - solv->jobrules];
 902       if (j == lastjob)
 903         continue;
 904       lastjob = j;
 905       how = job->elements[j];
 906       what = job->elements[j + 1];
 907       select = how & SOLVER_SELECTMASK;
 908       switch (how & SOLVER_JOBMASK)
 909         {
 910         case SOLVER_INSTALL:
 911           if (select != SOLVER_SOLVABLE)
 912             break;
 913           s = pool->solvables + what;
 914           if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, what))
 915             break;
 916           if (s->repo == installed)
 917             {
 918               MAPSET(&solv->noupdate, what - installed->start);
 919               break;
 920             }
 921           if (s->obsoletes)
 922             {
 923               Id obs, *obsp;
 924               obsp = s->repo->idarraydata + s->obsoletes;
 925               while ((obs = *obsp++) != 0)
 926                 FOR_PROVIDES(p, pp, obs)
 927                   {
 928                     if (pool->solvables[p].repo != installed)
 929                       continue;
 930                     if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
 931                       continue;
 932                     MAPSET(&solv->noupdate, p - installed->start);
 933                   }
 934             }
 935           FOR_PROVIDES(p, pp, s->name)
 936             {
 937               if (!solv->implicitobsoleteusesprovides && pool->solvables[p].name != s->name)
 938                 continue;
 939               if (pool->solvables[p].repo == installed)
 940                 MAPSET(&solv->noupdate, p - installed->start);
 941             }
 942           break;
 943         case SOLVER_ERASE:
 944           FOR_JOB_SELECT(p, pp, select, what)
 945             if (pool->solvables[p].repo == installed)
 946               MAPSET(&solv->noupdate, p - installed->start);
 947           break;
 948         default:
 949           break;
 950         }
 951     }
 952
 953   /* fixup update rule status */
 954   if (jobidx != -1)
 955     {
 956       /* we just disabled job #jobidx. enable all update rules
 957        * that aren't disabled by the remaining job rules */
 958       how = job->elements[jobidx];
 959       what = job->elements[jobidx + 1];
 960       select = how & SOLVER_SELECTMASK;
 961       switch (how & SOLVER_JOBMASK)
 962         {
 963         case SOLVER_INSTALL:
 964           if (select != SOLVER_SOLVABLE)
 965             break;
 966           s = pool->solvables + what;
 967           if (s->repo == installed)
 968             {
 969               r = solv->rules + solv->updaterules + (what - installed->start);
 970               if (r->d >= 0)
 971                 break;
 972               enablerule(solv, r);
 973               IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
 974                 {
 975                   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
 976                   solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
 977                 }
 978               break;
 979             }
 980           if (s->obsoletes)
 981             {
 982               Id obs, *obsp;
 983               obsp = s->repo->idarraydata + s->obsoletes;
 984               while ((obs = *obsp++) != 0)
 985                 FOR_PROVIDES(p, pp, obs)
 986                   {
 987                     if (pool->solvables[p].repo != installed)
 988                       continue;
 989                     if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
 990                       continue;
 991                     if (MAPTST(&solv->noupdate, p - installed->start))
 992                       continue;
 993                     r = solv->rules + solv->updaterules + (p - installed->start);
 994                     if (r->d >= 0)
 995                       continue;
 996                     enablerule(solv, r);
 997                     IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
 998                       {
 999                         POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
1000                         solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
1001                       }
1002                   }
1003             }
1004           FOR_PROVIDES(p, pp, s->name)
1005             {
1006               if (!solv->implicitobsoleteusesprovides && pool->solvables[p].name != s->name)
1007                 continue;
1008               if (pool->solvables[p].repo != installed)
1009                 continue;
1010               if (MAPTST(&solv->noupdate, p - installed->start))
1011                 continue;
1012               r = solv->rules + solv->updaterules + (p - installed->start);
1013               if (r->d >= 0)
1014                 continue;
1015               enablerule(solv, r);
1016               IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
1017                 {
1018                   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
1019                   solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
1020                 }
1021             }
1022           break;
1023         case SOLVER_ERASE:
1024           FOR_JOB_SELECT(p, pp, select, what)
1025             {
1026               if (pool->solvables[p].repo != installed)
1027                 continue;
1028               if (MAPTST(&solv->noupdate, p - installed->start))
1029                 continue;
1030               r = solv->rules + solv->updaterules + (p - installed->start);
1031               if (r->d >= 0)
1032                 continue;
1033               enablerule(solv, r);
1034               IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
1035                 {
1036                   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "@@@ re-enabling ");
1037                   solver_printrule(solv, SAT_DEBUG_SOLUTIONS, r);
1038                 }
1039             }
1040           break;
1041         default:
1042           break;
1043         }
1044       return;
1045     }
1046
1047   for (i = 0; i < installed->nsolvables; i++)
1048     {
1049       r = solv->rules + solv->updaterules + i;
1050       if (r->d >= 0 && MAPTST(&solv->noupdate, i))
1051         disablerule(solv, r);   /* was enabled, need to disable */
1052       r = solv->rules + solv->featurerules + i;
1053       if (r->d >= 0 && MAPTST(&solv->noupdate, i))
1054         disablerule(solv, r);   /* was enabled, need to disable */
1055     }
1056 }
1057
1058
1059 /*
1060  *  special multiversion patch conflict handling:
1061  *  a patch conflict is also satisfied, if some other
1062  *  version with the same name/arch that doesn't conflict
1063  *  get's installed. The generated rule is thus:
1064  *  -patch|-cpack|opack1|opack2|...
1065  */
1066 Id
1067 makemultiversionconflict(Solver *solv, Id n, Id con)
1068 {
1069   Pool *pool = solv->pool;
1070   Solvable *s, *sn;
1071   Queue q;
1072   Id p, pp, qbuf[64];
1073
1074   sn = pool->solvables + n;
1075   queue_init_buffer(&q, qbuf, sizeof(qbuf)/sizeof(*qbuf));
1076   queue_push(&q, -n);
1077   FOR_PROVIDES(p, pp, sn->name)
1078     {
1079       s = pool->solvables + p;
1080       if (s->name != sn->name || s->arch != sn->arch)
1081         continue;
1082       if (!MAPTST(&solv->noobsoletes, p))
1083         continue;
1084       if (pool_match_nevr(pool, pool->solvables + p, con))
1085         continue;
1086       /* here we have a multiversion solvable that doesn't conflict */
1087       /* thus we're not in conflict if it is installed */
1088       queue_push(&q, p);
1089     }
1090   if (q.count == 1)
1091     return -n;  /* no other package found, generate normal conflict */
1092   return pool_queuetowhatprovides(pool, &q);
1093 }
1094
1095
1096 /*-------------------------------------------------------------------
1097  *
1098  * add (install) rules for solvable
1099  *
1100  * s: Solvable for which to add rules
1101  * m: m[s] = 1 for solvables which have rules, prevent rule duplication
1102  *
1103  * Algorithm: 'visit all nodes of a graph'. The graph nodes are
1104  *  solvables, the edges their dependencies.
1105  *  Starting from an installed solvable, this will create all rules
1106  *  representing the graph created by the solvables dependencies.
1107  *
1108  * for unfulfilled requirements, conflicts, obsoletes,....
1109  * add a negative assertion for solvables that are not installable
1110  *
1111  * It will also create rules for all solvables referenced by 's'
1112  *  i.e. descend to all providers of requirements of 's'
1113  *
1114  */
1115
1116 static void
1117 addrpmrulesforsolvable(Solver *solv, Solvable *s, Map *m)
1118 {
1119   Pool *pool = solv->pool;
1120   Repo *installed = solv->installed;
1121
1122   /* 'work' queue. keeps Ids of solvables we still have to work on.
1123      And buffer for it. */
1124   Queue workq;
1125   Id workqbuf[64];
1126
1127   int i;
1128     /* if to add rules for broken deps ('rpm -V' functionality)
1129      * 0 = yes, 1 = no
1130      */
1131   int dontfix;
1132     /* Id var and pointer for each dependency
1133      * (not used in parallel)
1134      */
1135   Id req, *reqp;
1136   Id con, *conp;
1137   Id obs, *obsp;
1138   Id rec, *recp;
1139   Id sug, *sugp;
1140     /* var and ptr for loops */
1141   Id p, pp;
1142     /* ptr to 'whatprovides' */
1143   Id *dp;
1144     /* Id for current solvable 's' */
1145   Id n;
1146
1147   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable -----\n");
1148
1149   queue_init_buffer(&workq, workqbuf, sizeof(workqbuf)/sizeof(*workqbuf));
1150   queue_push(&workq, s - pool->solvables);      /* push solvable Id to work queue */
1151
1152   /* loop until there's no more work left */
1153   while (workq.count)
1154     {
1155       /*
1156        * n: Id of solvable
1157        * s: Pointer to solvable
1158        */
1159
1160       n = queue_shift(&workq);             /* 'pop' next solvable to work on from queue */
1161       if (MAPTST(m, n))                    /* continue if already visited */
1162         continue;
1163
1164       MAPSET(m, n);                        /* mark as visited */
1165       s = pool->solvables + n;             /* s = Solvable in question */
1166
1167       dontfix = 0;
1168       if (installed                        /* Installed system available */
1169           && !solv->fixsystem              /* NOT repair errors in rpm dependency graph */
1170           && s->repo == installed)         /* solvable is installed? */
1171       {
1172         dontfix = 1;                       /* dont care about broken rpm deps */
1173       }
1174
1175       if (!dontfix
1176           && s->arch != ARCH_SRC
1177           && s->arch != ARCH_NOSRC
1178           && !pool_installable(pool, s))
1179         {
1180           POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable\n", solvable2str(pool, s), (Id)(s - pool->solvables));
1181           addrule(solv, -n, 0);            /* uninstallable */
1182         }
1183
1184       /*-----------------------------------------
1185        * check requires of s
1186        */
1187
1188       if (s->requires)
1189         {
1190           reqp = s->repo->idarraydata + s->requires;
1191           while ((req = *reqp++) != 0)            /* go through all requires */
1192             {
1193               if (req == SOLVABLE_PREREQMARKER)   /* skip the marker */
1194                 continue;
1195
1196               /* find list of solvables providing 'req' */
1197               dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
1198
1199               if (*dp == SYSTEMSOLVABLE)          /* always installed */
1200                 continue;
1201
1202               if (dontfix)
1203                 {
1204                   /* the strategy here is to not insist on dependencies
1205                    * that are already broken. so if we find one provider
1206                    * that was already installed, we know that the
1207                    * dependency was not broken before so we enforce it */
1208
1209                   /* check if any of the providers for 'req' is installed */
1210                   for (i = 0; (p = dp[i]) != 0; i++)
1211                     {
1212                       if (pool->solvables[p].repo == installed)
1213                         break;          /* provider was installed */
1214                     }
1215                   /* didn't find an installed provider: previously broken dependency */
1216                   if (!p)
1217                     {
1218                       POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "ignoring broken requires %s of installed package %s\n", dep2str(pool, req), solvable2str(pool, s));
1219                       continue;
1220                     }
1221                 }
1222
1223               if (!*dp)
1224                 {
1225                   /* nothing provides req! */
1226                   POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "package %s [%d] is not installable (%s)\n", solvable2str(pool, s), (Id)(s - pool->solvables), dep2str(pool, req));
1227                   addrule(solv, -n, 0); /* mark requestor as uninstallable */
1228                   continue;
1229                 }
1230
1231               IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
1232                 {
1233                   POOL_DEBUG(SAT_DEBUG_RULE_CREATION,"  %s requires %s\n", solvable2str(pool, s), dep2str(pool, req));
1234                   for (i = 0; dp[i]; i++)
1235                     POOL_DEBUG(SAT_DEBUG_RULE_CREATION, "   provided by %s\n", solvable2str(pool, pool->solvables + dp[i]));
1236                 }
1237
1238               /* add 'requires' dependency */
1239               /* rule: (-requestor|provider1|provider2|...|providerN) */
1240               addrule(solv, -n, dp - pool->whatprovidesdata);
1241
1242               /* descend the dependency tree
1243                  push all non-visited providers on the work queue */
1244               for (; *dp; dp++)
1245                 {
1246                   if (!MAPTST(m, *dp))
1247                     queue_push(&workq, *dp);
1248                 }
1249
1250             } /* while, requirements of n */
1251
1252         } /* if, requirements */
1253
1254       /* that's all we check for src packages */
1255       if (s->arch == ARCH_SRC || s->arch == ARCH_NOSRC)
1256         continue;
1257
1258       /*-----------------------------------------
1259        * check conflicts of s
1260        */
1261
1262       if (s->conflicts)
1263         {
1264           int ispatch = 0;
1265
1266           /* we treat conflicts in patches a bit differen:
1267            * - nevr matching
1268            * - multiversion handling
1269            * XXX: we should really handle this different, looking
1270            * at the name is a bad hack
1271            */
1272           if (!strncmp("patch:", id2str(pool, s->name), 6))
1273             ispatch = 1;
1274           conp = s->repo->idarraydata + s->conflicts;
1275           /* foreach conflicts of 's' */
1276           while ((con = *conp++) != 0)
1277             {
1278               /* foreach providers of a conflict of 's' */
1279               FOR_PROVIDES(p, pp, con)
1280                 {
1281                   if (ispatch && !pool_match_nevr(pool, pool->solvables + p, con))
1282                     continue;
1283                   /* dontfix: dont care about conflicts with already installed packs */
1284                   if (dontfix && pool->solvables[p].repo == installed)
1285                     continue;
1286                   /* p == n: self conflict */
1287                   if (p == n && !solv->allowselfconflicts)
1288                     {
1289                       if (ISRELDEP(con))
1290                         {
1291                           Reldep *rd = GETRELDEP(pool, con);
1292                           if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_OTHERPROVIDERS)
1293                             continue;
1294                         }
1295                       p = 0;    /* make it a negative assertion, aka 'uninstallable' */
1296                     }
1297                   if (p && ispatch && solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p) && ISRELDEP(con))
1298                     {
1299                       /* our patch conflicts with a noobsoletes (aka multiversion) package */
1300                       p = -makemultiversionconflict(solv, p, con);
1301                     }
1302                  /* rule: -n|-p: either solvable _or_ provider of conflict */
1303                   addrule(solv, -n, -p);
1304                 }
1305             }
1306         }
1307
1308       /*-----------------------------------------
1309        * check obsoletes if not installed
1310        * (only installation will trigger the obsoletes in rpm)
1311        */
1312       if (!installed || pool->solvables[n].repo != installed)
1313         {                              /* not installed */
1314           int noobs = solv->noobsoletes.size && MAPTST(&solv->noobsoletes, n);
1315           if (s->obsoletes && !noobs)
1316             {
1317               obsp = s->repo->idarraydata + s->obsoletes;
1318               /* foreach obsoletes */
1319               while ((obs = *obsp++) != 0)
1320                 {
1321                   /* foreach provider of an obsoletes of 's' */
1322                   FOR_PROVIDES(p, pp, obs)
1323                     {
1324                       if (!solv->obsoleteusesprovides /* obsoletes are matched names, not provides */
1325                           && !pool_match_nevr(pool, pool->solvables + p, obs))
1326                         continue;
1327                       addrule(solv, -n, -p);
1328                     }
1329                 }
1330             }
1331           FOR_PROVIDES(p, pp, s->name)
1332             {
1333               Solvable *ps = pool->solvables + p;
1334               /* we still obsolete packages with same nevra, like rpm does */
1335               /* (actually, rpm mixes those packages. yuck...) */
1336               if (noobs && (s->name != ps->name || s->evr != ps->evr || s->arch != ps->arch))
1337                 continue;
1338               if (!solv->implicitobsoleteusesprovides && s->name != ps->name)
1339                 continue;
1340               addrule(solv, -n, -p);
1341             }
1342         }
1343
1344       /*-----------------------------------------
1345        * add recommends to the work queue
1346        */
1347       if (s->recommends)
1348         {
1349           recp = s->repo->idarraydata + s->recommends;
1350           while ((rec = *recp++) != 0)
1351             {
1352               FOR_PROVIDES(p, pp, rec)
1353                 if (!MAPTST(m, p))
1354                   queue_push(&workq, p);
1355             }
1356         }
1357       if (s->suggests)
1358         {
1359           sugp = s->repo->idarraydata + s->suggests;
1360           while ((sug = *sugp++) != 0)
1361             {
1362               FOR_PROVIDES(p, pp, sug)
1363                 if (!MAPTST(m, p))
1364                   queue_push(&workq, p);
1365             }
1366         }
1367     }
1368   queue_free(&workq);
1369   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforsolvable end -----\n");
1370 }
1371
1372
1373 /*-------------------------------------------------------------------
1374  *
1375  * Add package rules for weak rules
1376  *
1377  * m: visited solvables
1378  */
1379
1380 static void
1381 addrpmrulesforweak(Solver *solv, Map *m)
1382 {
1383   Pool *pool = solv->pool;
1384   Solvable *s;
1385   Id sup, *supp;
1386   int i, n;
1387
1388   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak -----\n");
1389     /* foreach solvable in pool */
1390   for (i = n = 1; n < pool->nsolvables; i++, n++)
1391     {
1392       if (i == pool->nsolvables)                 /* wrap i */
1393         i = 1;
1394       if (MAPTST(m, i))                          /* been there */
1395         continue;
1396
1397       s = pool->solvables + i;
1398       if (!pool_installable(pool, s))            /* only look at installable ones */
1399         continue;
1400
1401       sup = 0;
1402       if (s->supplements)
1403         {
1404           /* find possible supplements */
1405           supp = s->repo->idarraydata + s->supplements;
1406           while ((sup = *supp++) != ID_NULL)
1407             if (dep_possible(solv, sup, m))
1408               break;
1409         }
1410
1411         /* if nothing found, check for enhances */
1412       if (!sup && s->enhances)
1413         {
1414           supp = s->repo->idarraydata + s->enhances;
1415           while ((sup = *supp++) != ID_NULL)
1416             if (dep_possible(solv, sup, m))
1417               break;
1418         }
1419         /* if nothing found, goto next solvables */
1420       if (!sup)
1421         continue;
1422       addrpmrulesforsolvable(solv, s, m);
1423       n = 0;
1424     }
1425   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforweak end -----\n");
1426 }
1427
1428
1429 /*-------------------------------------------------------------------
1430  *
1431  * add package rules for possible updates
1432  *
1433  * s: solvable
1434  * m: map of already visited solvables
1435  * allow_all: 0 = dont allow downgrades, 1 = allow all candidates
1436  */
1437
1438 static void
1439 addrpmrulesforupdaters(Solver *solv, Solvable *s, Map *m, int allow_all)
1440 {
1441   Pool *pool = solv->pool;
1442   int i;
1443     /* queue and buffer for it */
1444   Queue qs;
1445   Id qsbuf[64];
1446
1447   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1448
1449   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1450     /* find update candidates for 's' */
1451   policy_findupdatepackages(solv, s, &qs, allow_all);
1452     /* add rule for 's' if not already done */
1453   if (!MAPTST(m, s - pool->solvables))
1454     addrpmrulesforsolvable(solv, s, m);
1455     /* foreach update candidate, add rule if not already done */
1456   for (i = 0; i < qs.count; i++)
1457     if (!MAPTST(m, qs.elements[i]))
1458       addrpmrulesforsolvable(solv, pool->solvables + qs.elements[i], m);
1459   queue_free(&qs);
1460
1461   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- addrpmrulesforupdaters -----\n");
1462 }
1463
1464 static Id
1465 finddistupgradepackages(Solver *solv, Solvable *s, Queue *qs, int allow_all)
1466 {
1467   Pool *pool = solv->pool;
1468   int i;
1469
1470   policy_findupdatepackages(solv, s, qs, allow_all);
1471   if (!qs->count)
1472     {
1473       if (allow_all)
1474         return 0;
1475       policy_findupdatepackages(solv, s, qs, 1);
1476       if (!qs->count)
1477         return 0;
1478       qs->count = 0;
1479       return -SYSTEMSOLVABLE;
1480     }
1481   if (allow_all)
1482     return s - pool->solvables;
1483   /* check if it is ok to keep the installed package */
1484   for (i = 0; i < qs->count; i++)
1485     {
1486       Solvable *ns = pool->solvables + qs->elements[i];
1487       if (s->evr == ns->evr && solvable_identical(pool, s, ns))
1488         return s - pool->solvables;
1489     }
1490   /* nope, it must be some other package */
1491   return queue_shift(qs);
1492 }
1493
1494 /*-------------------------------------------------------------------
1495  *
1496  * add rule for update
1497  *   (A|A1|A2|A3...)  An = update candidates for A
1498  *
1499  * s = (installed) solvable
1500  */
1501
1502 static void
1503 addupdaterule(Solver *solv, Solvable *s, int allow_all)
1504 {
1505   /* installed packages get a special upgrade allowed rule */
1506   Pool *pool = solv->pool;
1507   Id p, d;
1508   Queue qs;
1509   Id qsbuf[64];
1510
1511   POOL_DEBUG(SAT_DEBUG_SCHUBI, "-----  addupdaterule -----\n");
1512   queue_init_buffer(&qs, qsbuf, sizeof(qsbuf)/sizeof(*qsbuf));
1513   p = s - pool->solvables;
1514   /* find update candidates for 's' */
1515   if (solv->distupgrade)
1516     p = finddistupgradepackages(solv, s, &qs, allow_all);
1517   else
1518     policy_findupdatepackages(solv, s, &qs, allow_all);
1519   d = qs.count ? pool_queuetowhatprovides(pool, &qs) : 0;
1520   queue_free(&qs);
1521   addrule(solv, p, d);  /* allow update of s */
1522   POOL_DEBUG(SAT_DEBUG_SCHUBI, "-----  addupdaterule end -----\n");
1523 }
1524
1525
1526 /********************************************************************/
1527 /* watches */
1528
1529
1530 /*-------------------------------------------------------------------
1531  * makewatches
1532  *
1533  * initial setup for all watches
1534  */
1535
1536 static void
1537 makewatches(Solver *solv)
1538 {
1539   Rule *r;
1540   int i;
1541   int nsolvables = solv->pool->nsolvables;
1542
1543   sat_free(solv->watches);
1544                                        /* lower half for removals, upper half for installs */
1545   solv->watches = sat_calloc(2 * nsolvables, sizeof(Id));
1546 #if 1
1547   /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */
1548   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1549 #else
1550   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1551 #endif
1552     {
1553       if (!r->w2)               /* assertions do not need watches */
1554         continue;
1555
1556       /* see addwatches_rule(solv, r) */
1557       r->n1 = solv->watches[nsolvables + r->w1];
1558       solv->watches[nsolvables + r->w1] = r - solv->rules;
1559
1560       r->n2 = solv->watches[nsolvables + r->w2];
1561       solv->watches[nsolvables + r->w2] = r - solv->rules;
1562     }
1563 }
1564
1565
1566 /*-------------------------------------------------------------------
1567  *
1568  * add watches (for rule)
1569  * sets up watches for a single rule
1570  *
1571  * see also makewatches()
1572  */
1573
1574 static inline void
1575 addwatches_rule(Solver *solv, Rule *r)
1576 {
1577   int nsolvables = solv->pool->nsolvables;
1578
1579   r->n1 = solv->watches[nsolvables + r->w1];
1580   solv->watches[nsolvables + r->w1] = r - solv->rules;
1581
1582   r->n2 = solv->watches[nsolvables + r->w2];
1583   solv->watches[nsolvables + r->w2] = r - solv->rules;
1584 }
1585
1586
1587 /********************************************************************/
1588 /*
1589  * rule propagation
1590  */
1591
1592
1593 /* shortcuts to check if a literal (positive or negative) assignment
1594  * evaluates to 'true' or 'false'
1595  */
1596 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1597 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
1598 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0)
1599
1600 /*-------------------------------------------------------------------
1601  *
1602  * propagate
1603  *
1604  * make decision and propagate to all rules
1605  *
1606  * Evaluate each term affected by the decision (linked through watches)
1607  * If we find unit rules we make new decisions based on them
1608  *
1609  * Everything's fixed there, it's just finding rules that are
1610  * unit.
1611  *
1612  * return : 0 = everything is OK
1613  *          rule = conflict found in this rule
1614  */
1615
1616 static Rule *
1617 propagate(Solver *solv, int level)
1618 {
1619   Pool *pool = solv->pool;
1620   Id *rp, *next_rp;           /* rule pointer, next rule pointer in linked list */
1621   Rule *r;                    /* rule */
1622   Id p, pkg, other_watch;
1623   Id *dp;
1624   Id *decisionmap = solv->decisionmap;
1625
1626   Id *watches = solv->watches + pool->nsolvables;   /* place ptr in middle */
1627
1628   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
1629
1630   /* foreach non-propagated decision */
1631   while (solv->propagate_index < solv->decisionq.count)
1632     {
1633         /*
1634          * 'pkg' was just decided
1635          * negate because our watches trigger if literal goes FALSE
1636          */
1637       pkg = -solv->decisionq.elements[solv->propagate_index++];
1638
1639       IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1640         {
1641           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
1642           solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
1643         }
1644
1645       /* foreach rule where 'pkg' is now FALSE */
1646       for (rp = watches + pkg; *rp; rp = next_rp)
1647         {
1648           r = solv->rules + *rp;
1649           if (r->d < 0)
1650             {
1651               /* rule is disabled, goto next */
1652               if (pkg == r->w1)
1653                 next_rp = &r->n1;
1654               else
1655                 next_rp = &r->n2;
1656               continue;
1657             }
1658
1659           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1660             {
1661               POOL_DEBUG(SAT_DEBUG_PROPAGATE,"  watch triggered ");
1662               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1663             }
1664
1665             /* 'pkg' was just decided (was set to FALSE)
1666              *
1667              *  now find other literal watch, check clause
1668              *   and advance on linked list
1669              */
1670           if (pkg == r->w1)
1671             {
1672               other_watch = r->w2;
1673               next_rp = &r->n1;
1674             }
1675           else
1676             {
1677               other_watch = r->w1;
1678               next_rp = &r->n2;
1679             }
1680
1681             /*
1682              * This term is already true (through the other literal)
1683              * so we have nothing to do
1684              */
1685           if (DECISIONMAP_TRUE(other_watch))
1686             continue;
1687
1688             /*
1689              * The other literal is FALSE or UNDEF
1690              *
1691              */
1692
1693           if (r->d)
1694             {
1695               /* Not a binary clause, try to move our watch.
1696                *
1697                * Go over all literals and find one that is
1698                *   not other_watch
1699                *   and not FALSE
1700                *
1701                * (TRUE is also ok, in that case the rule is fulfilled)
1702                */
1703               if (r->p                                /* we have a 'p' */
1704                   && r->p != other_watch              /* which is not watched */
1705                   && !DECISIONMAP_FALSE(r->p))        /* and not FALSE */
1706                 {
1707                   p = r->p;
1708                 }
1709               else                                    /* go find a 'd' to make 'true' */
1710                 {
1711                   /* foreach p in 'd'
1712                      we just iterate sequentially, doing it in another order just changes the order of decisions, not the decisions itself
1713                    */
1714                   for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1715                     {
1716                       if (p != other_watch              /* which is not watched */
1717                           && !DECISIONMAP_FALSE(p))     /* and not FALSE */
1718                         break;
1719                     }
1720                 }
1721
1722               if (p)
1723                 {
1724                   /*
1725                    * if we found some p that is UNDEF or TRUE, move
1726                    * watch to it
1727                    */
1728                   IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1729                     {
1730                       if (p > 0)
1731                         POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1732                       else
1733                         POOL_DEBUG(SAT_DEBUG_PROPAGATE,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1734                     }
1735
1736                   *rp = *next_rp;
1737                   next_rp = rp;
1738
1739                   if (pkg == r->w1)
1740                     {
1741                       r->w1 = p;
1742                       r->n1 = watches[p];
1743                     }
1744                   else
1745                     {
1746                       r->w2 = p;
1747                       r->n2 = watches[p];
1748                     }
1749                   watches[p] = r - solv->rules;
1750                   continue;
1751                 }
1752               /* search failed, thus all unwatched literals are FALSE */
1753
1754             } /* not binary */
1755
1756             /*
1757              * unit clause found, set literal other_watch to TRUE
1758              */
1759
1760           if (DECISIONMAP_FALSE(other_watch))      /* check if literal is FALSE */
1761             return r;                              /* eek, a conflict! */
1762
1763           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1764             {
1765               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "   unit ");
1766               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1767             }
1768
1769           if (other_watch > 0)
1770             decisionmap[other_watch] = level;    /* install! */
1771           else
1772             decisionmap[-other_watch] = -level;  /* remove! */
1773
1774           queue_push(&solv->decisionq, other_watch);
1775           queue_push(&solv->decisionq_why, r - solv->rules);
1776
1777           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1778             {
1779               Solvable *s = pool->solvables + (other_watch > 0 ? other_watch : -other_watch);
1780               if (other_watch > 0)
1781                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to install %s\n", solvable2str(pool, s));
1782               else
1783                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to conflict %s\n", solvable2str(pool, s));
1784             }
1785
1786         } /* foreach rule involving 'pkg' */
1787
1788     } /* while we have non-decided decisions */
1789
1790   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
1791
1792   return 0;     /* all is well */
1793 }
1794
1795
1796 /********************************************************************/
1797 /* Analysis */
1798
1799 /*-------------------------------------------------------------------
1800  *
1801  * analyze
1802  *   and learn
1803  */
1804
1805 static int
1806 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
1807 {
1808   Pool *pool = solv->pool;
1809   Queue r;
1810   int rlevel = 1;
1811   Map seen;             /* global? */
1812   Id d, v, vv, *dp, why;
1813   int l, i, idx;
1814   int num = 0, l1num = 0;
1815   int learnt_why = solv->learnt_pool.count;
1816   Id *decisionmap = solv->decisionmap;
1817
1818   queue_init(&r);
1819
1820   POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
1821   map_init(&seen, pool->nsolvables);
1822   idx = solv->decisionq.count;
1823   for (;;)
1824     {
1825       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1826         solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1827       queue_push(&solv->learnt_pool, c - solv->rules);
1828       d = c->d < 0 ? -c->d - 1 : c->d;
1829       dp = d ? pool->whatprovidesdata + d : 0;
1830       /* go through all literals of the rule */
1831       for (i = -1; ; i++)
1832         {
1833           if (i == -1)
1834             v = c->p;
1835           else if (d == 0)
1836             v = i ? 0 : c->w2;
1837           else
1838             v = *dp++;
1839           if (v == 0)
1840             break;
1841
1842           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1843             continue;
1844           vv = v > 0 ? v : -v;
1845           if (MAPTST(&seen, vv))
1846             continue;
1847           l = solv->decisionmap[vv];
1848           if (l < 0)
1849             l = -l;
1850           MAPSET(&seen, vv);
1851           if (l == 1)
1852             l1num++;                    /* need to do this one in level1 pass */
1853           else if (l == level)
1854             num++;                      /* need to do this one as well */
1855           else
1856             {
1857               queue_push(&r, v);        /* not level1 or conflict level, add to new rule */
1858               if (l > rlevel)
1859                 rlevel = l;
1860             }
1861         }
1862 l1retry:
1863       if (!num && !--l1num)
1864         break;  /* all level 1 literals done */
1865       for (;;)
1866         {
1867           assert(idx > 0);
1868           v = solv->decisionq.elements[--idx];
1869           vv = v > 0 ? v : -v;
1870           if (MAPTST(&seen, vv))
1871             break;
1872         }
1873       MAPCLR(&seen, vv);
1874       if (num && --num == 0)
1875         {
1876           *pr = -v;     /* so that v doesn't get lost */
1877           if (!l1num)
1878             break;
1879           POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1880           for (i = 0; i < r.count; i++)
1881             {
1882               v = r.elements[i];
1883               MAPCLR(&seen, v > 0 ? v : -v);
1884             }
1885           /* only level 1 marks left */
1886           l1num++;
1887           goto l1retry;
1888         }
1889       why = solv->decisionq_why.elements[idx];
1890       if (!why)                 /* just in case, maybe for SYSTEMSOLVABLE */
1891         goto l1retry;
1892       c = solv->rules + why;
1893     }
1894   map_free(&seen);
1895
1896   if (r.count == 0)
1897     *dr = 0;
1898   else if (r.count == 1 && r.elements[0] < 0)
1899     *dr = r.elements[0];
1900   else
1901     *dr = pool_queuetowhatprovides(pool, &r);
1902   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1903     {
1904       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1905       solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1906       for (i = 0; i < r.count; i++)
1907         solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1908     }
1909   /* push end marker on learnt reasons stack */
1910   queue_push(&solv->learnt_pool, 0);
1911   if (whyp)
1912     *whyp = learnt_why;
1913   solv->stats_learned++;
1914   return rlevel;
1915 }
1916
1917
1918 /*-------------------------------------------------------------------
1919  *
1920  * reset_solver
1921  *
1922  * reset the solver decisions to right after the rpm rules.
1923  * called after rules have been enabled/disabled
1924  */
1925
1926 static void
1927 reset_solver(Solver *solv)
1928 {
1929   Pool *pool = solv->pool;
1930   int i;
1931   Id v;
1932
1933   /* rewind decisions to direct rpm rule assertions */
1934   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1935     {
1936       v = solv->decisionq.elements[i];
1937       solv->decisionmap[v > 0 ? v : -v] = 0;
1938     }
1939
1940   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1941
1942   solv->decisionq_why.count = solv->directdecisions;
1943   solv->decisionq.count = solv->directdecisions;
1944   solv->recommends_index = -1;
1945   solv->propagate_index = 0;
1946
1947   /* adapt learnt rule status to new set of enabled/disabled rules */
1948   enabledisablelearntrules(solv);
1949
1950   /* redo all job/update decisions */
1951   makeruledecisions(solv);
1952   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1953 }
1954
1955
1956 /*-------------------------------------------------------------------
1957  *
1958  * analyze_unsolvable_rule
1959  */
1960
1961 static void
1962 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1963 {
1964   Pool *pool = solv->pool;
1965   int i;
1966   Id why = r - solv->rules;
1967
1968   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1969     solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1970   if (solv->learntrules && why >= solv->learntrules)
1971     {
1972       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1973         if (solv->learnt_pool.elements[i] > 0)
1974           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
1975       return;
1976     }
1977   if (MAPTST(&solv->weakrulemap, why))
1978     if (!*lastweakp || why > *lastweakp)
1979       *lastweakp = why;
1980   /* do not add rpm rules to problem */
1981   if (why < solv->rpmrules_end)
1982     return;
1983   /* turn rule into problem */
1984   if (why >= solv->jobrules && why < solv->jobrules_end)
1985     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1986   /* return if problem already countains our rule */
1987   if (solv->problems.count)
1988     {
1989       for (i = solv->problems.count - 1; i >= 0; i--)
1990         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1991           break;
1992         else if (solv->problems.elements[i] == why)
1993           return;
1994     }
1995   queue_push(&solv->problems, why);
1996 }
1997
1998
1999 /*-------------------------------------------------------------------
2000  *
2001  * analyze_unsolvable
2002  *
2003  * return: 1 - disabled some rules, try again
2004  *         0 - hopeless
2005  */
2006
2007 static int
2008 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
2009 {
2010   Pool *pool = solv->pool;
2011   Rule *r;
2012   Map seen;             /* global to speed things up? */
2013   Id d, v, vv, *dp, why;
2014   int l, i, idx;
2015   Id *decisionmap = solv->decisionmap;
2016   int oldproblemcount;
2017   int oldlearntpoolcount;
2018   Id lastweak;
2019
2020   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
2021   solv->stats_unsolvable++;
2022   oldproblemcount = solv->problems.count;
2023   oldlearntpoolcount = solv->learnt_pool.count;
2024
2025   /* make room for proof index */
2026   /* must update it later, as analyze_unsolvable_rule would confuse
2027    * it with a rule index if we put the real value in already */
2028   queue_push(&solv->problems, 0);
2029
2030   r = cr;
2031   map_init(&seen, pool->nsolvables);
2032   queue_push(&solv->learnt_pool, r - solv->rules);
2033   lastweak = 0;
2034   analyze_unsolvable_rule(solv, r, &lastweak);
2035   d = r->d < 0 ? -r->d - 1 : r->d;
2036   dp = d ? pool->whatprovidesdata + d : 0;
2037   for (i = -1; ; i++)
2038     {
2039       if (i == -1)
2040         v = r->p;
2041       else if (d == 0)
2042         v = i ? 0 : r->w2;
2043       else
2044         v = *dp++;
2045       if (v == 0)
2046         break;
2047       if (DECISIONMAP_TRUE(v))  /* the one true literal */
2048           continue;
2049       vv = v > 0 ? v : -v;
2050       l = solv->decisionmap[vv];
2051       if (l < 0)
2052         l = -l;
2053       MAPSET(&seen, vv);
2054     }
2055   idx = solv->decisionq.count;
2056   while (idx > 0)
2057     {
2058       v = solv->decisionq.elements[--idx];
2059       vv = v > 0 ? v : -v;
2060       if (!MAPTST(&seen, vv))
2061         continue;
2062       why = solv->decisionq_why.elements[idx];
2063       queue_push(&solv->learnt_pool, why);
2064       r = solv->rules + why;
2065       analyze_unsolvable_rule(solv, r, &lastweak);
2066       d = r->d < 0 ? -r->d - 1 : r->d;
2067       dp = d ? pool->whatprovidesdata + d : 0;
2068       for (i = -1; ; i++)
2069         {
2070           if (i == -1)
2071             v = r->p;
2072           else if (d == 0)
2073             v = i ? 0 : r->w2;
2074           else
2075             v = *dp++;
2076           if (v == 0)
2077             break;
2078           if (DECISIONMAP_TRUE(v))      /* the one true literal */
2079               continue;
2080           vv = v > 0 ? v : -v;
2081           l = solv->decisionmap[vv];
2082           if (l < 0)
2083             l = -l;
2084           MAPSET(&seen, vv);
2085         }
2086     }
2087   map_free(&seen);
2088   queue_push(&solv->problems, 0);       /* mark end of this problem */
2089
2090   if (lastweak)
2091     {
2092       /* disable last weak rule */
2093       solv->problems.count = oldproblemcount;
2094       solv->learnt_pool.count = oldlearntpoolcount;
2095       r = solv->rules + lastweak;
2096       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
2097       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
2098       disablerule(solv, r);
2099       reset_solver(solv);
2100       return 1;
2101     }
2102
2103   /* finish proof */
2104   queue_push(&solv->learnt_pool, 0);
2105   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
2106
2107   if (disablerules)
2108     {
2109       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
2110         disableproblem(solv, solv->problems.elements[i]);
2111       /* XXX: might want to enable all weak rules again */
2112       reset_solver(solv);
2113       return 1;
2114     }
2115   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
2116   return 0;
2117 }
2118
2119
2120 /********************************************************************/
2121 /* Decision revert */
2122
2123 /*-------------------------------------------------------------------
2124  *
2125  * revert
2126  * revert decision at level
2127  */
2128
2129 static void
2130 revert(Solver *solv, int level)
2131 {
2132   Pool *pool = solv->pool;
2133   Id v, vv;
2134   while (solv->decisionq.count)
2135     {
2136       v = solv->decisionq.elements[solv->decisionq.count - 1];
2137       vv = v > 0 ? v : -v;
2138       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
2139         break;
2140       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
2141       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
2142         solv->recommendations.count--;
2143       solv->decisionmap[vv] = 0;
2144       solv->decisionq.count--;
2145       solv->decisionq_why.count--;
2146       solv->propagate_index = solv->decisionq.count;
2147     }
2148   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
2149     {
2150       solv->branches.count--;
2151       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
2152         solv->branches.count--;
2153     }
2154   solv->recommends_index = -1;
2155 }
2156
2157
2158 /*-------------------------------------------------------------------
2159  *
2160  * watch2onhighest - put watch2 on literal with highest level
2161  */
2162
2163 static inline void
2164 watch2onhighest(Solver *solv, Rule *r)
2165 {
2166   int l, wl = 0;
2167   Id d, v, *dp;
2168
2169   d = r->d < 0 ? -r->d - 1 : r->d;
2170   if (!d)
2171     return;     /* binary rule, both watches are set */
2172   dp = solv->pool->whatprovidesdata + d;
2173   while ((v = *dp++) != 0)
2174     {
2175       l = solv->decisionmap[v < 0 ? -v : v];
2176       if (l < 0)
2177         l = -l;
2178       if (l > wl)
2179         {
2180           r->w2 = dp[-1];
2181           wl = l;
2182         }
2183     }
2184 }
2185
2186
2187 /*-------------------------------------------------------------------
2188  *
2189  * setpropagatelearn
2190  *
2191  * add free decision (solvable to install) to decisionq
2192  * increase level and propagate decision
2193  * return if no conflict.
2194  *
2195  * in conflict case, analyze conflict rule, add resulting
2196  * rule to learnt rule set, make decision from learnt
2197  * rule (always unit) and re-propagate.
2198  *
2199  * returns the new solver level or 0 if unsolvable
2200  *
2201  */
2202
2203 static int
2204 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
2205 {
2206   Pool *pool = solv->pool;
2207   Rule *r;
2208   Id p = 0, d = 0;
2209   int l, why;
2210
2211   if (decision)
2212     {
2213       level++;
2214       if (decision > 0)
2215         solv->decisionmap[decision] = level;
2216       else
2217         solv->decisionmap[-decision] = -level;
2218       queue_push(&solv->decisionq, decision);
2219       queue_push(&solv->decisionq_why, 0);
2220     }
2221   for (;;)
2222     {
2223       r = propagate(solv, level);
2224       if (!r)
2225         break;
2226       if (level == 1)
2227         return analyze_unsolvable(solv, r, disablerules);
2228       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
2229       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
2230       assert(l > 0 && l < level);
2231       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
2232       level = l;
2233       revert(solv, level);
2234       r = addrule(solv, p, d);       /* p requires d */
2235       assert(r);
2236       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
2237       queue_push(&solv->learnt_why, why);
2238       if (d)
2239         {
2240           /* at least 2 literals, needs watches */
2241           watch2onhighest(solv, r);
2242           addwatches_rule(solv, r);
2243         }
2244       else
2245         {
2246           /* learnt rule is an assertion */
2247           queue_push(&solv->ruleassertions, r - solv->rules);
2248         }
2249       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
2250       queue_push(&solv->decisionq, p);
2251       queue_push(&solv->decisionq_why, r - solv->rules);
2252       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
2253         {
2254           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
2255           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
2256           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
2257           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
2258         }
2259     }
2260   return level;
2261 }
2262
2263
2264 /*-------------------------------------------------------------------
2265  *
2266  * select and install
2267  *
2268  * install best package from the queue. We add an extra package, inst, if
2269  * provided. See comment in weak install section.
2270  *
2271  * returns the new solver level or 0 if unsolvable
2272  *
2273  */
2274
2275 static int
2276 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
2277 {
2278   Pool *pool = solv->pool;
2279   Id p;
2280   int i;
2281
2282   /* FIXME: do we really need that inst handling? */
2283   if (solv->distupgrade && inst && dq->count)
2284     {
2285       policy_filter_unwanted(solv, dq, 0, POLICY_MODE_CHOOSE);
2286       for (i = 0; i < dq->count; i++)
2287         if (solvable_identical(pool, pool->solvables + inst, pool->solvables + dq->elements[i]))
2288           dq->elements[i] = inst;
2289     }
2290   else
2291     {
2292       if (dq->count > 1 || inst)
2293         policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
2294     }
2295
2296   i = 0;
2297   if (dq->count > 1)
2298     {
2299       /* choose the supplemented one */
2300       for (i = 0; i < dq->count; i++)
2301         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2302           break;
2303       if (i == dq->count)
2304         {
2305           for (i = 1; i < dq->count; i++)
2306             queue_push(&solv->branches, dq->elements[i]);
2307           queue_push(&solv->branches, -level);
2308           i = 0;
2309         }
2310     }
2311   p = dq->elements[i];
2312
2313   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2314
2315   return setpropagatelearn(solv, level, p, disablerules);
2316 }
2317
2318
2319 /********************************************************************/
2320 /* Main solver interface */
2321
2322
2323 /*-------------------------------------------------------------------
2324  *
2325  * solver_create
2326  * create solver structure
2327  *
2328  * pool: all available solvables
2329  * installed: installed Solvables
2330  *
2331  *
2332  * Upon solving, rules are created to flag the Solvables
2333  * of the 'installed' Repo as installed.
2334  */
2335
2336 Solver *
2337 solver_create(Pool *pool)
2338 {
2339   Solver *solv;
2340   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2341   solv->pool = pool;
2342   solv->installed = pool->installed;
2343
2344   queue_init(&solv->ruletojob);
2345   queue_init(&solv->decisionq);
2346   queue_init(&solv->decisionq_why);
2347   queue_init(&solv->problems);
2348   queue_init(&solv->suggestions);
2349   queue_init(&solv->recommendations);
2350   queue_init(&solv->orphaned);
2351   queue_init(&solv->learnt_why);
2352   queue_init(&solv->learnt_pool);
2353   queue_init(&solv->branches);
2354   queue_init(&solv->covenantq);
2355   queue_init(&solv->weakruleq);
2356   queue_init(&solv->ruleassertions);
2357
2358   map_init(&solv->recommendsmap, pool->nsolvables);
2359   map_init(&solv->suggestsmap, pool->nsolvables);
2360   map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
2361   solv->recommends_index = 0;
2362
2363   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2364   solv->nrules = 1;
2365   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2366   memset(solv->rules, 0, sizeof(Rule));
2367
2368   return solv;
2369 }
2370
2371
2372 /*-------------------------------------------------------------------
2373  *
2374  * solver_free
2375  */
2376
2377 void
2378 solver_free(Solver *solv)
2379 {
2380   queue_free(&solv->ruletojob);
2381   queue_free(&solv->decisionq);
2382   queue_free(&solv->decisionq_why);
2383   queue_free(&solv->learnt_why);
2384   queue_free(&solv->learnt_pool);
2385   queue_free(&solv->problems);
2386   queue_free(&solv->suggestions);
2387   queue_free(&solv->recommendations);
2388   queue_free(&solv->orphaned);
2389   queue_free(&solv->branches);
2390   queue_free(&solv->covenantq);
2391   queue_free(&solv->weakruleq);
2392   queue_free(&solv->ruleassertions);
2393
2394   map_free(&solv->recommendsmap);
2395   map_free(&solv->suggestsmap);
2396   map_free(&solv->noupdate);
2397   map_free(&solv->weakrulemap);
2398   map_free(&solv->noobsoletes);
2399
2400   sat_free(solv->decisionmap);
2401   sat_free(solv->rules);
2402   sat_free(solv->watches);
2403   sat_free(solv->obsoletes);
2404   sat_free(solv->obsoletes_data);
2405   sat_free(solv);
2406 }
2407
2408
2409 /*-------------------------------------------------------------------
2410  *
2411  * run_solver
2412  *
2413  * all rules have been set up, now actually run the solver
2414  *
2415  */
2416
2417 static void
2418 run_solver(Solver *solv, int disablerules, int doweak)
2419 {
2420   Queue dq;             /* local decisionqueue */
2421   Queue dqs;            /* local decisionqueue for supplements */
2422   int systemlevel;
2423   int level, olevel;
2424   Rule *r;
2425   int i, j, n;
2426   Solvable *s;
2427   Pool *pool = solv->pool;
2428   Id p, *dp;
2429
2430   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2431     {
2432       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2433       for (i = 1; i < solv->nrules; i++)
2434         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2435     }
2436
2437   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2438
2439   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2440     solver_printdecisions(solv);
2441
2442   /* start SAT algorithm */
2443   level = 1;
2444   systemlevel = level + 1;
2445   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2446
2447   queue_init(&dq);
2448   queue_init(&dqs);
2449
2450   /*
2451    * here's the main loop:
2452    * 1) propagate new decisions (only needed for level 1)
2453    * 2) try to keep installed packages
2454    * 3) fulfill all unresolved rules
2455    * 4) install recommended packages
2456    * 5) minimalize solution if we had choices
2457    * if we encounter a problem, we rewind to a safe level and restart
2458    * with step 1
2459    */
2460
2461   for (;;)
2462     {
2463       /*
2464        * propagate
2465        */
2466
2467       if (level == 1)
2468         {
2469           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2470           if ((r = propagate(solv, level)) != 0)
2471             {
2472               if (analyze_unsolvable(solv, r, disablerules))
2473                 continue;
2474               queue_free(&dq);
2475               return;
2476             }
2477         }
2478
2479      if (level < systemlevel)
2480         {
2481           POOL_DEBUG(SAT_DEBUG_STATS, "resolving job rules\n");
2482           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2483             {
2484               Id l;
2485               if (r->d < 0)             /* ignore disabled rules */
2486                 continue;
2487               queue_empty(&dq);
2488               FOR_RULELITERALS(l, dp, r)
2489                 {
2490                   if (l < 0)
2491                     {
2492                       if (solv->decisionmap[-l] <= 0)
2493                         break;
2494                     }
2495                   else
2496                     {
2497                       if (solv->decisionmap[l] > 0)
2498                         break;
2499                       if (solv->decisionmap[l] == 0)
2500                         queue_push(&dq, l);
2501                     }
2502                 }
2503               if (l || !dq.count)
2504                 continue;
2505               /* prune to installed if not updating */
2506               if (!solv->updatesystem && solv->installed && dq.count > 1)
2507                 {
2508                   int j, k;
2509                   for (j = k = 0; j < dq.count; j++)
2510                     {
2511                       Solvable *s = pool->solvables + dq.elements[j];
2512                       if (s->repo == solv->installed)
2513                         dq.elements[k++] = dq.elements[j];
2514                     }
2515                   if (k)
2516                     dq.count = k;
2517                 }
2518               olevel = level;
2519               level = selectandinstall(solv, level, &dq, 0, disablerules);
2520               if (level == 0)
2521                 {
2522                   queue_free(&dq);
2523                   return;
2524                 }
2525               if (level <= olevel)
2526                 break;
2527             }
2528           systemlevel = level + 1;
2529           if (i < solv->jobrules_end)
2530             continue;
2531         }
2532
2533
2534       /*
2535        * installed packages
2536        */
2537
2538       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2539         {
2540           if (!solv->updatesystem)
2541             {
2542               /*
2543                * Normal run (non-updating)
2544                * Keep as many packages installed as possible
2545                */
2546               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2547
2548               for (i = solv->installed->start; i < solv->installed->end; i++)
2549                 {
2550                   s = pool->solvables + i;
2551
2552                     /* skip if not installed */
2553                   if (s->repo != solv->installed)
2554                     continue;
2555
2556                     /* skip if already decided */
2557                   if (solv->decisionmap[i] != 0)
2558                     continue;
2559
2560                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2561
2562                   olevel = level;
2563                   level = setpropagatelearn(solv, level, i, disablerules);
2564
2565                   if (level == 0)                /* unsolvable */
2566                     {
2567                       queue_free(&dq);
2568                       return;
2569                     }
2570                   if (level <= olevel)
2571                     break;
2572                 }
2573               if (i < solv->installed->end)
2574                 continue;
2575             }
2576
2577           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2578
2579           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2580             {
2581               Rule *rr;
2582               Id inst;
2583               s = pool->solvables + i;
2584
2585                 /* skip if not installed (can't update) */
2586               if (s->repo != solv->installed)
2587                 continue;
2588                 /* skip if already decided */
2589               if (solv->decisionmap[i] > 0)
2590                 continue;
2591
2592                 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2593               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2594                 continue;
2595
2596               queue_empty(&dq);
2597
2598               rr = r;
2599               if (rr->d < 0)    /* disabled -> look at feature rule ? */
2600                 rr -= solv->installed->end - solv->installed->start;
2601               if (!rr->p)       /* identical to update rule? */
2602                 rr = r;
2603               if (rr->p <= 0)
2604                 continue;
2605
2606               FOR_RULELITERALS(p, dp, rr)
2607                 {
2608                   if (solv->decisionmap[p] > 0)
2609                     break;
2610                   if (solv->decisionmap[p] == 0)
2611                     queue_push(&dq, p);
2612                 }
2613               if (p || !dq.count)       /* already fulfilled or empty */
2614                 continue;
2615               if (dq.elements[0] == i)
2616                 inst = queue_shift(&dq);
2617               else
2618                 inst = 0;
2619               olevel = level;
2620               /* FIXME: it is handled a bit different because we do not want
2621                * to have it pruned just because it is not recommened.
2622                * we should not prune installed packages instead.
2623                */
2624               level = selectandinstall(solv, level, &dq, inst, disablerules);
2625               if (level == 0)
2626                 {
2627                   queue_free(&dq);
2628                   return;
2629                 }
2630               if (level <= olevel)
2631                 break;
2632             }
2633           systemlevel = level + 1;
2634           if (i < solv->installed->end)
2635             continue;
2636         }
2637
2638       if (level < systemlevel)
2639         systemlevel = level;
2640
2641       /*
2642        * decide
2643        */
2644
2645       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
2646       for (i = 1, n = 1; ; i++, n++)
2647         {
2648           if (n == solv->nrules)
2649             break;
2650           if (i == solv->nrules)
2651             i = 1;
2652           r = solv->rules + i;
2653           if (r->d < 0)         /* ignore disabled rules */
2654             continue;
2655           queue_empty(&dq);
2656           if (r->d == 0)
2657             {
2658               /* binary or unary rule */
2659               /* need two positive undecided literals */
2660               if (r->p < 0 || r->w2 <= 0)
2661                 continue;
2662               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2663                 continue;
2664               queue_push(&dq, r->p);
2665               queue_push(&dq, r->w2);
2666             }
2667           else
2668             {
2669               /* make sure that
2670                * all negative literals are installed
2671                * no positive literal is installed
2672                * i.e. the rule is not fulfilled and we
2673                * just need to decide on the positive literals
2674                */
2675               if (r->p < 0)
2676                 {
2677                   if (solv->decisionmap[-r->p] <= 0)
2678                     continue;
2679                 }
2680               else
2681                 {
2682                   if (solv->decisionmap[r->p] > 0)
2683                     continue;
2684                   if (solv->decisionmap[r->p] == 0)
2685                     queue_push(&dq, r->p);
2686                 }
2687               dp = pool->whatprovidesdata + r->d;
2688               while ((p = *dp++) != 0)
2689                 {
2690                   if (p < 0)
2691                     {
2692                       if (solv->decisionmap[-p] <= 0)
2693                         break;
2694                     }
2695                   else
2696                     {
2697                       if (solv->decisionmap[p] > 0)
2698                         break;
2699                       if (solv->decisionmap[p] == 0)
2700                         queue_push(&dq, p);
2701                     }
2702                 }
2703               if (p)
2704                 continue;
2705             }
2706           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2707             {
2708               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2709               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2710             }
2711           /* dq.count < 2 cannot happen as this means that
2712            * the rule is unit */
2713           assert(dq.count > 1);
2714
2715           olevel = level;
2716           level = selectandinstall(solv, level, &dq, 0, disablerules);
2717           if (level == 0)
2718             {
2719               queue_free(&dq);
2720               return;
2721             }
2722           if (level < systemlevel)
2723             break;
2724           n = 0;
2725         } /* for(), decide */
2726
2727       if (n != solv->nrules)    /* continue if level < systemlevel */
2728         continue;
2729
2730       if (doweak)
2731         {
2732           int qcount;
2733
2734           POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
2735           queue_empty(&dq);
2736           queue_empty(&dqs);
2737           for (i = 1; i < pool->nsolvables; i++)
2738             {
2739               if (solv->decisionmap[i] < 0)
2740                 continue;
2741               if (solv->decisionmap[i] > 0)
2742                 {
2743                   /* installed, check for recommends */
2744                   Id *recp, rec, pp, p;
2745                   s = pool->solvables + i;
2746                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
2747                     continue;
2748                   /* XXX need to special case AND ? */
2749                   if (s->recommends)
2750                     {
2751                       recp = s->repo->idarraydata + s->recommends;
2752                       while ((rec = *recp++) != 0)
2753                         {
2754                           qcount = dq.count;
2755                           FOR_PROVIDES(p, pp, rec)
2756                             {
2757                               if (solv->decisionmap[p] > 0)
2758                                 {
2759                                   dq.count = qcount;
2760                                   break;
2761                                 }
2762                               else if (solv->decisionmap[p] == 0)
2763                                 {
2764                                   queue_pushunique(&dq, p);
2765                                 }
2766                             }
2767                         }
2768                     }
2769                 }
2770               else
2771                 {
2772                   s = pool->solvables + i;
2773                   if (!s->supplements)
2774                     continue;
2775                   if (!pool_installable(pool, s))
2776                     continue;
2777                   if (!solver_is_supplementing(solv, s))
2778                     continue;
2779                   if (solv->ignorealreadyrecommended && solv->installed)
2780                     queue_pushunique(&dqs, i);  /* needs filter */
2781                   else
2782                     queue_pushunique(&dq, i);
2783                 }
2784             }
2785           if (solv->ignorealreadyrecommended && dqs.count)
2786             {
2787               /* turn off all new packages */
2788               for (i = 0; i < solv->decisionq.count; i++)
2789                 {
2790                   p = solv->decisionq.elements[i];
2791                   if (p < 0)
2792                     continue;
2793                   s = pool->solvables + p;
2794                   if (s->repo && s->repo != solv->installed)
2795                     solv->decisionmap[p] = -solv->decisionmap[p];
2796                 }
2797               /* filter out old supplements */
2798               for (i = 0; i < dqs.count; i++)
2799                 {
2800                   p = dqs.elements[i];
2801                   s = pool->solvables + p;
2802                   if (!s->supplements)
2803                     continue;
2804                   if (!solver_is_supplementing(solv, s))
2805                     queue_pushunique(&dq, p);
2806                 }
2807               /* undo turning off */
2808               for (i = 0; i < solv->decisionq.count; i++)
2809                 {
2810                   p = solv->decisionq.elements[i];
2811                   if (p < 0)
2812                     continue;
2813                   s = pool->solvables + p;
2814                   if (s->repo && s->repo != solv->installed)
2815                     solv->decisionmap[p] = -solv->decisionmap[p];
2816                 }
2817             }
2818           if (dq.count)
2819             {
2820               if (dq.count > 1)
2821                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2822               p = dq.elements[0];
2823               POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2824               queue_push(&solv->recommendations, p);
2825               level = setpropagatelearn(solv, level, p, 0);
2826               continue;
2827             }
2828         }
2829
2830      if (solv->distupgrade && solv->installed)
2831         {
2832           /* let's see if we can install some unsupported package */
2833           int ri;
2834           POOL_DEBUG(SAT_DEBUG_STATS, "deciding unsupported packages\n");
2835           for (i = solv->installed->start, ri = 0; i < solv->installed->end; i++, ri++)
2836             {
2837               s = pool->solvables + i;
2838               if (s->repo != solv->installed)
2839                 continue;
2840               if (solv->decisionmap[i])
2841                 continue;
2842               if (!solv->rules[solv->updaterules + ri].p && !solv->rules[solv->featurerules + ri].p)
2843                 break;
2844             }
2845           if (i < solv->installed->end)
2846             {
2847               if (solv->distupgrade_removeunsupported)
2848                 {
2849                   POOL_DEBUG(SAT_DEBUG_STATS, "removing unsupported %s\n", solvable2str(pool, pool->solvables + i));
2850                   level = setpropagatelearn(solv, level, -i, 0);
2851                 }
2852               else
2853                 {
2854                   POOL_DEBUG(SAT_DEBUG_STATS, "keeping unsupported %s\n", solvable2str(pool, pool->solvables + i));
2855                   level = setpropagatelearn(solv, level, i, 0);
2856                 }
2857               continue;
2858             }
2859         }
2860
2861      if (solv->solution_callback)
2862         {
2863           solv->solution_callback(solv, solv->solution_callback_data);
2864           if (solv->branches.count)
2865             {
2866               int i = solv->branches.count - 1;
2867               int l = -solv->branches.elements[i];
2868               for (; i > 0; i--)
2869                 if (solv->branches.elements[i - 1] < 0)
2870                   break;
2871               p = solv->branches.elements[i];
2872               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2873               queue_empty(&dq);
2874               for (j = i + 1; j < solv->branches.count; j++)
2875                 queue_push(&dq, solv->branches.elements[j]);
2876               solv->branches.count = i;
2877               level = l;
2878               revert(solv, level);
2879               if (dq.count > 1)
2880                 for (j = 0; j < dq.count; j++)
2881                   queue_push(&solv->branches, dq.elements[j]);
2882               olevel = level;
2883               level = setpropagatelearn(solv, level, p, disablerules);
2884               if (level == 0)
2885                 {
2886                   queue_free(&dq);
2887                   return;
2888                 }
2889               continue;
2890             }
2891           /* all branches done, we're finally finished */
2892           break;
2893         }
2894
2895       /* minimization step */
2896      if (solv->branches.count)
2897         {
2898           int l = 0, lasti = -1, lastl = -1;
2899           p = 0;
2900           for (i = solv->branches.count - 1; i >= 0; i--)
2901             {
2902               p = solv->branches.elements[i];
2903               if (p < 0)
2904                 l = -p;
2905               else if (p > 0 && solv->decisionmap[p] > l + 1)
2906                 {
2907                   lasti = i;
2908                   lastl = l;
2909                 }
2910             }
2911           if (lasti >= 0)
2912             {
2913               /* kill old solvable so that we do not loop */
2914               p = solv->branches.elements[lasti];
2915               solv->branches.elements[lasti] = 0;
2916               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2917
2918               level = lastl;
2919               revert(solv, level);
2920               olevel = level;
2921               level = setpropagatelearn(solv, level, p, disablerules);
2922               if (level == 0)
2923                 {
2924                   queue_free(&dq);
2925                   return;
2926                 }
2927               continue;
2928             }
2929         }
2930       break;
2931     }
2932   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
2933
2934   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2935   queue_free(&dq);
2936   queue_free(&dqs);
2937 }
2938
2939
2940 /*-------------------------------------------------------------------
2941  *
2942  * refine_suggestion
2943  *
2944  * at this point, all rules that led to conflicts are disabled.
2945  * we re-enable all rules of a problem set but rule "sug", then
2946  * continue to disable more rules until there as again a solution.
2947  */
2948
2949 /* FIXME: think about conflicting assertions */
2950
2951 static void
2952 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2953 {
2954   Pool *pool = solv->pool;
2955   int i, j;
2956   Id v;
2957   Queue disabled;
2958   int disabledcnt;
2959
2960   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2961     {
2962       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2963       for (i = 0; problem[i]; i++)
2964         {
2965           if (problem[i] == sug)
2966             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2967           solver_printproblem(solv, problem[i]);
2968         }
2969     }
2970   queue_init(&disabled);
2971   queue_empty(refined);
2972   queue_push(refined, sug);
2973
2974   /* re-enable all problem rules with the exception of "sug"(gestion) */
2975   revert(solv, 1);
2976   reset_solver(solv);
2977
2978   for (i = 0; problem[i]; i++)
2979     if (problem[i] != sug)
2980       enableproblem(solv, problem[i]);
2981
2982   if (sug < 0)
2983     disableupdaterules(solv, job, -(sug + 1));
2984   else if (sug >= solv->updaterules && sug < solv->updaterules_end)
2985     {
2986       /* enable feature rule */
2987       Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
2988       if (r->p)
2989         enablerule(solv, r);
2990     }
2991
2992   enableweakrules(solv);
2993
2994   for (;;)
2995     {
2996       int njob, nfeature, nupdate;
2997       queue_empty(&solv->problems);
2998       revert(solv, 1);          /* XXX no longer needed? */
2999       reset_solver(solv);
3000
3001       if (!solv->problems.count)
3002         run_solver(solv, 0, 0);
3003
3004       if (!solv->problems.count)
3005         {
3006           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
3007           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3008             solver_printdecisions(solv);
3009           break;                /* great, no more problems */
3010         }
3011       disabledcnt = disabled.count;
3012       /* start with 1 to skip over proof index */
3013       njob = nfeature = nupdate = 0;
3014       for (i = 1; i < solv->problems.count - 1; i++)
3015         {
3016           /* ignore solutions in refined */
3017           v = solv->problems.elements[i];
3018           if (v == 0)
3019             break;      /* end of problem reached */
3020           for (j = 0; problem[j]; j++)
3021             if (problem[j] != sug && problem[j] == v)
3022               break;
3023           if (problem[j])
3024             continue;
3025           if (v >= solv->featurerules && v < solv->featurerules_end)
3026             nfeature++;
3027           else if (v > 0)
3028             nupdate++;
3029           else
3030             {
3031               if ((job->elements[-v -1] & SOLVER_ESSENTIAL) != 0)
3032                 continue;       /* not that one! */
3033               njob++;
3034             }
3035           queue_push(&disabled, v);
3036         }
3037       if (disabled.count == disabledcnt)
3038         {
3039           /* no solution found, this was an invalid suggestion! */
3040           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
3041           refined->count = 0;
3042           break;
3043         }
3044       if (!njob && nupdate && nfeature)
3045         {
3046           /* got only update rules, filter out feature rules */
3047           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
3048           for (i = j = disabledcnt; i < disabled.count; i++)
3049             {
3050               v = disabled.elements[i];
3051               if (v < solv->featurerules || v >= solv->featurerules_end)
3052                 disabled.elements[j++] = v;
3053             }
3054           disabled.count = j;
3055           nfeature = 0;
3056         }
3057       if (disabled.count == disabledcnt + 1)
3058         {
3059           /* just one suggestion, add it to refined list */
3060           v = disabled.elements[disabledcnt];
3061           if (!nfeature)
3062             queue_push(refined, v);     /* do not record feature rules */
3063           disableproblem(solv, v);
3064           if (v >= solv->updaterules && v < solv->updaterules_end)
3065             {
3066               Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3067               if (r->p)
3068                 enablerule(solv, r);    /* enable corresponding feature rule */
3069             }
3070           if (v < 0)
3071             disableupdaterules(solv, job, -(v + 1));
3072         }
3073       else
3074         {
3075           /* more than one solution, disable all */
3076           /* do not push anything on refine list, as we do not know which solution to choose */
3077           /* thus, the user will get another problem if he selects this solution, where he
3078            * can choose the right one */
3079           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3080             {
3081               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
3082               for (i = disabledcnt; i < disabled.count; i++)
3083                 solver_printproblem(solv, disabled.elements[i]);
3084             }
3085           for (i = disabledcnt; i < disabled.count; i++)
3086             {
3087               v = disabled.elements[i];
3088               disableproblem(solv, v);
3089               if (v >= solv->updaterules && v < solv->updaterules_end)
3090                 {
3091                   Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3092                   if (r->p)
3093                     enablerule(solv, r);
3094                 }
3095             }
3096         }
3097     }
3098   /* all done, get us back into the same state as before */
3099   /* enable refined rules again */
3100   for (i = 0; i < disabled.count; i++)
3101     enableproblem(solv, disabled.elements[i]);
3102   /* disable problem rules again */
3103
3104   /* FIXME! */
3105   for (i = 0; problem[i]; i++)
3106     enableproblem(solv, problem[i]);
3107   disableupdaterules(solv, job, -1);
3108
3109   /* disable problem rules again */
3110   for (i = 0; problem[i]; i++)
3111     disableproblem(solv, problem[i]);
3112   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
3113 }
3114
3115
3116 /*-------------------------------------------------------------------
3117  * sorting helper for problems
3118  *
3119  * bring update rules before job rules
3120  * make essential job rules last
3121  */
3122
3123 Queue *problems_sort_data;
3124
3125 static int
3126 problems_sortcmp(const void *ap, const void *bp)
3127 {
3128   Id a = *(Id *)ap, b = *(Id *)bp;
3129   if (a < 0 && b > 0)
3130     return 1;
3131   if (a > 0 && b < 0)
3132     return -1;
3133   if (a < 0 && b < 0)
3134     {
3135       Queue *job = problems_sort_data;
3136       int af = job->elements[-a - 1] & SOLVER_ESSENTIAL;
3137       int bf = job->elements[-a - 1] & SOLVER_ESSENTIAL;
3138       int x = bf - af;
3139       if (x)
3140         return x;
3141     }
3142   return a - b;
3143 }
3144
3145
3146 /*-------------------------------------------------------------------
3147  * sort problems
3148  */
3149
3150 static void
3151 problems_sort(Solver *solv, Queue *job)
3152 {
3153   int i, j;
3154   if (!solv->problems.count)
3155     return;
3156   for (i = j = 1; i < solv->problems.count; i++)
3157     {
3158       if (!solv->problems.elements[i])
3159         {
3160           if (i > j + 1)
3161             {
3162               problems_sort_data = job;
3163               qsort(solv->problems.elements + j, i - j, sizeof(Id), problems_sortcmp);
3164             }
3165           if (++i == solv->problems.count)
3166             break;
3167           j = i + 1;
3168         }
3169     }
3170 }
3171
3172
3173 /*-------------------------------------------------------------------
3174  * convert problems to solutions
3175  */
3176
3177 static void
3178 problems_to_solutions(Solver *solv, Queue *job)
3179 {
3180   Pool *pool = solv->pool;
3181   Queue problems;
3182   Queue solution;
3183   Queue solutions;
3184   Id *problem;
3185   Id why;
3186   int i, j, nsol, probsolved;
3187   unsigned int now, refnow;
3188
3189   if (!solv->problems.count)
3190     return;
3191   now = sat_timems(0);
3192   problems_sort(solv, job);
3193   queue_clone(&problems, &solv->problems);
3194   queue_init(&solution);
3195   queue_init(&solutions);
3196   /* copy over proof index */
3197   queue_push(&solutions, problems.elements[0]);
3198   problem = problems.elements + 1;
3199   probsolved = 0;
3200   refnow = sat_timems(0);
3201   for (i = 1; i < problems.count; i++)
3202     {
3203       Id v = problems.elements[i];
3204       if (v == 0)
3205         {
3206           /* mark end of this problem */
3207           queue_push(&solutions, 0);
3208           queue_push(&solutions, 0);
3209           POOL_DEBUG(SAT_DEBUG_STATS, "refining took %d ms\n", sat_timems(refnow));
3210           if (i + 1 == problems.count)
3211             break;
3212           /* copy over proof of next problem */
3213           queue_push(&solutions, problems.elements[i + 1]);
3214           i++;
3215           problem = problems.elements + i + 1;
3216           refnow = sat_timems(0);
3217           probsolved = 0;
3218           continue;
3219         }
3220       if (v < 0 && (job->elements[-v - 1] & SOLVER_ESSENTIAL))
3221         {
3222           /* essential job, skip if we already have a solution */
3223           if (probsolved)
3224             continue;
3225         }
3226       refine_suggestion(solv, job, problem, v, &solution);
3227       if (!solution.count)
3228         continue;       /* this solution didn't work out */
3229
3230       nsol = 0;
3231       for (j = 0; j < solution.count; j++)
3232         {
3233           why = solution.elements[j];
3234           /* must be either job descriptor or update rule */
3235           assert(why < 0 || (why >= solv->updaterules && why < solv->updaterules_end));
3236 #if 0
3237           solver_printproblem(solv, why);
3238 #endif
3239           if (why < 0)
3240             {
3241               /* job descriptor */
3242               queue_push(&solutions, 0);
3243               queue_push(&solutions, -why);
3244             }
3245           else
3246             {
3247               /* update rule, find replacement package */
3248               Id p, d, *dp, rp = 0;
3249               Rule *rr;
3250               p = solv->installed->start + (why - solv->updaterules);
3251               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
3252               if (!rr->p)
3253                 rr = solv->rules + why;
3254               if (solv->distupgrade && solv->rules[why].p != p && solv->decisionmap[p] > 0)
3255                 {
3256                   /* distupgrade case, allow to keep old package */
3257                   queue_push(&solutions, p);
3258                   queue_push(&solutions, p);
3259                   nsol++;
3260                   continue;
3261                 }
3262               if (solv->decisionmap[p] > 0)
3263                 continue;       /* false alarm, turned out we can keep the package */
3264               if (rr->w2)
3265                 {
3266                   d = rr->d < 0 ? -rr->d - 1 : rr->d;
3267                   if (!d)
3268                     {
3269                       if (solv->decisionmap[rr->w2] > 0 && pool->solvables[rr->w2].repo != solv->installed)
3270                         rp = rr->w2;
3271                     }
3272                   else
3273                     {
3274                       for (dp = pool->whatprovidesdata + d; *dp; dp++)
3275                         {
3276                           if (solv->decisionmap[*dp] > 0 && pool->solvables[*dp].repo != solv->installed)
3277                             {
3278                               rp = *dp;
3279                               break;
3280                             }
3281                         }
3282                     }
3283                 }
3284               queue_push(&solutions, p);
3285               queue_push(&solutions, rp);
3286             }
3287           nsol++;
3288         }
3289       /* mark end of this solution */
3290       if (nsol)
3291         {
3292           probsolved = 1;
3293           queue_push(&solutions, 0);
3294           queue_push(&solutions, 0);
3295         }
3296       else
3297         {
3298           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "Oops, everything was fine?\n");
3299         }
3300     }
3301   queue_free(&solution);
3302   queue_free(&problems);
3303   /* copy queue over to solutions */
3304   queue_free(&solv->problems);
3305   queue_clone(&solv->problems, &solutions);
3306
3307   /* bring solver back into problem state */
3308   revert(solv, 1);              /* XXX move to reset_solver? */
3309   reset_solver(solv);
3310
3311   assert(solv->problems.count == solutions.count);
3312   queue_free(&solutions);
3313   POOL_DEBUG(SAT_DEBUG_STATS, "problems_to_solutions took %d ms\n", sat_timems(now));
3314 }
3315
3316
3317 /*-------------------------------------------------------------------
3318  *
3319  * problem iterator
3320  *
3321  * advance to next problem
3322  */
3323
3324 Id
3325 solver_next_problem(Solver *solv, Id problem)
3326 {
3327   Id *pp;
3328   if (problem == 0)
3329     return solv->problems.count ? 1 : 0;
3330   pp = solv->problems.elements + problem;
3331   while (pp[0] || pp[1])
3332     {
3333       /* solution */
3334       pp += 2;
3335       while (pp[0] || pp[1])
3336         pp += 2;
3337       pp += 2;
3338     }
3339   pp += 2;
3340   problem = pp - solv->problems.elements;
3341   if (problem >= solv->problems.count)
3342     return 0;
3343   return problem + 1;
3344 }
3345
3346
3347 /*-------------------------------------------------------------------
3348  *
3349  * solution iterator
3350  */
3351
3352 Id
3353 solver_next_solution(Solver *solv, Id problem, Id solution)
3354 {
3355   Id *pp;
3356   if (solution == 0)
3357     {
3358       solution = problem;
3359       pp = solv->problems.elements + solution;
3360       return pp[0] || pp[1] ? solution : 0;
3361     }
3362   pp = solv->problems.elements + solution;
3363   while (pp[0] || pp[1])
3364     pp += 2;
3365   pp += 2;
3366   solution = pp - solv->problems.elements;
3367   return pp[0] || pp[1] ? solution : 0;
3368 }
3369
3370
3371 /*-------------------------------------------------------------------
3372  *
3373  * solution element iterator
3374  */
3375
3376 Id
3377 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
3378 {
3379   Id *pp;
3380   element = element ? element + 2 : solution;
3381   pp = solv->problems.elements + element;
3382   if (!(pp[0] || pp[1]))
3383     return 0;
3384   *p = pp[0];
3385   *rp = pp[1];
3386   return element;
3387 }
3388
3389
3390 /*-------------------------------------------------------------------
3391  *
3392  * Retrieve information about a problematic rule
3393  *
3394  * this is basically the reverse of addrpmrulesforsolvable
3395  */
3396
3397 SolverProbleminfo
3398 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3399 {
3400   Pool *pool = solv->pool;
3401   Repo *installed = solv->installed;
3402   Rule *r;
3403   Solvable *s;
3404   int dontfix = 0;
3405   Id p, d, w2, pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3406
3407   assert(rid > 0);
3408   if (rid >= solv->jobrules && rid < solv->jobrules_end)
3409     {
3410
3411       r = solv->rules + rid;
3412       p = solv->ruletojob.elements[rid - solv->jobrules];
3413       *depp = job->elements[p + 1];
3414       *sourcep = p;
3415       *targetp = job->elements[p];
3416       d = r->d < 0 ? -r->d - 1 : r->d;
3417       if (d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && (job->elements[p] & SOLVER_SELECTMASK) != SOLVER_SOLVABLE_ONE_OF)
3418         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3419       return SOLVER_PROBLEM_JOB_RULE;
3420     }
3421   if (rid >= solv->updaterules && rid < solv->updaterules_end)
3422     {
3423       *depp = 0;
3424       *sourcep = solv->installed->start + (rid - solv->updaterules);
3425       *targetp = 0;
3426       return SOLVER_PROBLEM_UPDATE_RULE;
3427     }
3428   assert(rid < solv->rpmrules_end);
3429   r = solv->rules + rid;
3430   assert(r->p < 0);
3431   d = r->d < 0 ? -r->d - 1 : r->d;
3432   if (d == 0 && r->w2 == 0)
3433     {
3434       /* a rpm rule assertion */
3435       s = pool->solvables - r->p;
3436       if (installed && !solv->fixsystem && s->repo == installed)
3437         dontfix = 1;
3438       assert(!dontfix); /* dontfix packages never have a neg assertion */
3439       *sourcep = -r->p;
3440       *targetp = 0;
3441       /* see why the package is not installable */
3442       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3443         {
3444           *depp = 0;
3445           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3446         }
3447       /* check requires */
3448       if (s->requires)
3449         {
3450           reqp = s->repo->idarraydata + s->requires;
3451           while ((req = *reqp++) != 0)
3452             {
3453               if (req == SOLVABLE_PREREQMARKER)
3454                 continue;
3455               dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3456               if (*dp == 0)
3457                 break;
3458             }
3459           if (req)
3460             {
3461               *depp = req;
3462               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3463             }
3464         }
3465       if (!solv->allowselfconflicts && s->conflicts)
3466         {
3467           conp = s->repo->idarraydata + s->conflicts;
3468           while ((con = *conp++) != 0)
3469             FOR_PROVIDES(p, pp, con)
3470               if (p == -r->p)
3471                 {
3472                   *depp = con;
3473                   return SOLVER_PROBLEM_SELF_CONFLICT;
3474                 }
3475         }
3476       /* should never happen */
3477       *depp = 0;
3478       return SOLVER_PROBLEM_RPM_RULE;
3479     }
3480   s = pool->solvables - r->p;
3481   if (installed && !solv->fixsystem && s->repo == installed)
3482     dontfix = 1;
3483   w2 = r->w2;
3484   if (d && pool->whatprovidesdata[d] < 0)
3485     {
3486       /* rule looks like -p|-c|x|x|x..., we only create this for patches with multiversion */
3487       /* reduce it to -p|-c case */
3488       w2 = pool->whatprovidesdata[d];
3489     }
3490   if (d == 0 && w2 < 0)
3491     {
3492       /* a package conflict */
3493       Solvable *s2 = pool->solvables - w2;
3494       int dontfix2 = 0;
3495
3496       if (installed && !solv->fixsystem && s2->repo == installed)
3497         dontfix2 = 1;
3498
3499       /* if both packages have the same name and at least one of them
3500        * is not installed, they conflict */
3501       if (s->name == s2->name && !(installed && s->repo == installed && s2->repo == installed))
3502         {
3503           /* also check noobsoletes map */
3504           if ((s->evr == s2->evr && s->arch == s2->arch) || !solv->noobsoletes.size
3505                 || ((!installed || s->repo != installed) && !MAPTST(&solv->noobsoletes, -r->p))
3506                 || ((!installed || s2->repo != installed) && !MAPTST(&solv->noobsoletes, -w2)))
3507             {
3508               *depp = 0;
3509               *sourcep = -r->p;
3510               *targetp = -w2;
3511               return SOLVER_PROBLEM_SAME_NAME;
3512             }
3513         }
3514
3515       /* check conflicts in both directions */
3516       if (s->conflicts)
3517         {
3518           conp = s->repo->idarraydata + s->conflicts;
3519           while ((con = *conp++) != 0)
3520             {
3521               FOR_PROVIDES(p, pp, con)
3522                 {
3523                   if (dontfix && pool->solvables[p].repo == installed)
3524                     continue;
3525                   if (p != -w2)
3526                     continue;
3527                   *depp = con;
3528                   *sourcep = -r->p;
3529                   *targetp = p;
3530                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3531                 }
3532             }
3533         }
3534       if (s2->conflicts)
3535         {
3536           conp = s2->repo->idarraydata + s2->conflicts;
3537           while ((con = *conp++) != 0)
3538             {
3539               FOR_PROVIDES(p, pp, con)
3540                 {
3541                   if (dontfix2 && pool->solvables[p].repo == installed)
3542                     continue;
3543                   if (p != -r->p)
3544                     continue;
3545                   *depp = con;
3546                   *sourcep = -w2;
3547                   *targetp = p;
3548                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3549                 }
3550             }
3551         }
3552       /* check obsoletes in both directions */
3553       if ((!installed || s->repo != installed) && s->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3554         {
3555           obsp = s->repo->idarraydata + s->obsoletes;
3556           while ((obs = *obsp++) != 0)
3557             {
3558               FOR_PROVIDES(p, pp, obs)
3559                 {
3560                   if (p != -w2)
3561                     continue;
3562                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3563                     continue;
3564                   *depp = obs;
3565                   *sourcep = -r->p;
3566                   *targetp = p;
3567                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3568                 }
3569             }
3570         }
3571       if ((!installed || s2->repo != installed) && s2->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3572         {
3573           obsp = s2->repo->idarraydata + s2->obsoletes;
3574           while ((obs = *obsp++) != 0)
3575             {
3576               FOR_PROVIDES(p, pp, obs)
3577                 {
3578                   if (p != -r->p)
3579                     continue;
3580                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3581                     continue;
3582                   *depp = obs;
3583                   *sourcep = -w2;
3584                   *targetp = p;
3585                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3586                 }
3587             }
3588         }
3589       if (solv->implicitobsoleteusesprovides && (!installed || s->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3590         {
3591           FOR_PROVIDES(p, pp, s->name)
3592             {
3593               if (p != -w2)
3594                 continue;
3595               *depp = s->name;
3596               *sourcep = -r->p;
3597               *targetp = p;
3598               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3599             }
3600         }
3601       if (solv->implicitobsoleteusesprovides && (!installed || s2->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3602         {
3603           FOR_PROVIDES(p, pp, s2->name)
3604             {
3605               if (p != -r->p)
3606                 continue;
3607               *depp = s2->name;
3608               *sourcep = -w2;
3609               *targetp = p;
3610               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3611             }
3612         }
3613       /* all cases checked, can't happen */
3614       *depp = 0;
3615       *sourcep = -r->p;
3616       *targetp = 0;
3617       return SOLVER_PROBLEM_RPM_RULE;
3618     }
3619   /* simple requires */
3620   if (s->requires)
3621     {
3622       reqp = s->repo->idarraydata + s->requires;
3623       while ((req = *reqp++) != 0)
3624         {
3625           if (req == SOLVABLE_PREREQMARKER)
3626             continue;
3627           dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3628           if (d == 0)
3629             {
3630               if (*dp == r->w2 && dp[1] == 0)
3631                 break;
3632             }
3633           else if (dp - pool->whatprovidesdata == d)
3634             break;
3635         }
3636       if (req)
3637         {
3638           *depp = req;
3639           *sourcep = -r->p;
3640           *targetp = 0;
3641           return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3642         }
3643     }
3644   /* all cases checked, can't happen */
3645   *depp = 0;
3646   *sourcep = -r->p;
3647   *targetp = 0;
3648   return SOLVER_PROBLEM_RPM_RULE;
3649 }
3650
3651
3652 /*-------------------------------------------------------------------
3653  *
3654  * find problem rule
3655  */
3656
3657 static void
3658 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3659 {
3660   Id rid, d;
3661   Id lreqr, lconr, lsysr, ljobr;
3662   Rule *r;
3663   int reqassert = 0;
3664
3665   lreqr = lconr = lsysr = ljobr = 0;
3666   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3667     {
3668       assert(rid > 0);
3669       if (rid >= solv->learntrules)
3670         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3671       else if (rid >= solv->jobrules && rid < solv->jobrules_end)
3672         {
3673           if (!*jobrp)
3674             *jobrp = rid;
3675         }
3676       else if (rid >= solv->updaterules && rid < solv->updaterules_end)
3677         {
3678           if (!*sysrp)
3679             *sysrp = rid;
3680         }
3681       else
3682         {
3683           assert(rid < solv->rpmrules_end);
3684           r = solv->rules + rid;
3685           d = r->d < 0 ? -r->d - 1 : r->d;
3686           if (!d && r->w2 < 0)
3687             {
3688               if (!*conrp)
3689                 *conrp = rid;
3690             }
3691           else
3692             {
3693               if (!d && r->w2 == 0 && !reqassert)
3694                 {
3695                   /* prefer assertions (XXX: bad idea?) */
3696                   *reqrp = rid;
3697                   reqassert = 1;
3698                 }
3699               if (!*reqrp)
3700                 *reqrp = rid;
3701               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3702                 {
3703                   /* prefer rules of installed packages */
3704                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3705                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3706                     *reqrp = rid;
3707                 }
3708             }
3709         }
3710     }
3711   if (!*reqrp && lreqr)
3712     *reqrp = lreqr;
3713   if (!*conrp && lconr)
3714     *conrp = lconr;
3715   if (!*jobrp && ljobr)
3716     *jobrp = ljobr;
3717   if (!*sysrp && lsysr)
3718     *sysrp = lsysr;
3719 }
3720
3721
3722 /*-------------------------------------------------------------------
3723  *
3724  * find problem rule
3725  *
3726  * search for a rule that describes the problem to the
3727  * user. A pretty hopeless task, actually. We currently
3728  * prefer simple requires.
3729  */
3730
3731 Id
3732 solver_findproblemrule(Solver *solv, Id problem)
3733 {
3734   Id reqr, conr, sysr, jobr;
3735   Id idx = solv->problems.elements[problem - 1];
3736   reqr = conr = sysr = jobr = 0;
3737   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3738   if (reqr)
3739     return reqr;
3740   if (conr)
3741     return conr;
3742   if (sysr)
3743     return sysr;
3744   if (jobr)
3745     return jobr;
3746   assert(0);
3747 }
3748
3749
3750 /*-------------------------------------------------------------------
3751  *
3752  * create reverse obsoletes map for installed solvables
3753  *
3754  * for each installed solvable find which packages with *different* names
3755  * obsolete the solvable.
3756  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3757  */
3758
3759 static void
3760 create_obsolete_index(Solver *solv)
3761 {
3762   Pool *pool = solv->pool;
3763   Solvable *s;
3764   Repo *installed = solv->installed;
3765   Id p, pp, obs, *obsp, *obsoletes, *obsoletes_data;
3766   int i, n;
3767
3768   if (!installed || !installed->nsolvables)
3769     return;
3770   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3771   for (i = 1; i < pool->nsolvables; i++)
3772     {
3773       s = pool->solvables + i;
3774       if (!s->obsoletes)
3775         continue;
3776       if (!pool_installable(pool, s))
3777         continue;
3778       obsp = s->repo->idarraydata + s->obsoletes;
3779       while ((obs = *obsp++) != 0)
3780         {
3781           FOR_PROVIDES(p, pp, obs)
3782             {
3783               if (pool->solvables[p].repo != installed)
3784                 continue;
3785               if (pool->solvables[p].name == s->name)
3786                 continue;
3787               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3788                 continue;
3789               obsoletes[p - installed->start]++;
3790             }
3791         }
3792     }
3793   n = 0;
3794   for (i = 0; i < installed->nsolvables; i++)
3795     if (obsoletes[i])
3796       {
3797         n += obsoletes[i] + 1;
3798         obsoletes[i] = n;
3799       }
3800   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3801   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3802   for (i = pool->nsolvables - 1; i > 0; i--)
3803     {
3804       s = pool->solvables + i;
3805       if (!s->obsoletes)
3806         continue;
3807       if (!pool_installable(pool, s))
3808         continue;
3809       obsp = s->repo->idarraydata + s->obsoletes;
3810       while ((obs = *obsp++) != 0)
3811         {
3812           FOR_PROVIDES(p, pp, obs)
3813             {
3814               if (pool->solvables[p].repo != installed)
3815                 continue;
3816               if (pool->solvables[p].name == s->name)
3817                 continue;
3818               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3819                 continue;
3820               p -= installed->start;
3821               if (obsoletes_data[obsoletes[p]] != i)
3822                 obsoletes_data[--obsoletes[p]] = i;
3823             }
3824         }
3825     }
3826 }
3827
3828
3829 /*-------------------------------------------------------------------
3830  *
3831  * remove disabled conflicts
3832  */
3833
3834 static void
3835 removedisabledconflicts(Solver *solv, Queue *removed)
3836 {
3837   Pool *pool = solv->pool;
3838   int i, n;
3839   Id p, why, *dp;
3840   Id new;
3841   Rule *r;
3842   Id *decisionmap = solv->decisionmap;
3843
3844   POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n");
3845   queue_empty(removed);
3846   for (i = 0; i < solv->decisionq.count; i++)
3847     {
3848       p = solv->decisionq.elements[i];
3849       if (p > 0)
3850         continue;
3851       /* a conflict. we never do conflicts on free decisions, so there
3852        * must have been an unit rule */
3853       why = solv->decisionq_why.elements[i];
3854       assert(why > 0);
3855       r = solv->rules + why;
3856       if (r->d < 0 && decisionmap[-p])
3857         {
3858           /* rule is now disabled, remove from decisionmap */
3859           POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3860           queue_push(removed, -p);
3861           queue_push(removed, decisionmap[-p]);
3862           decisionmap[-p] = 0;
3863         }
3864     }
3865   if (!removed->count)
3866     return;
3867   /* we removed some confliced packages. some of them might still
3868    * be in conflict, so search for unit rules and re-conflict */
3869   new = 0;
3870   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3871     {
3872       if (i == solv->nrules)
3873         {
3874           i = 1;
3875           r = solv->rules + i;
3876         }
3877       if (r->d < 0)
3878         continue;
3879       if (!r->w2)
3880         {
3881           if (r->p < 0 && !decisionmap[-r->p])
3882             new = r->p;
3883         }
3884       else if (!r->d)
3885         {
3886           /* binary rule */
3887           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3888             new = r->p;
3889           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3890             new = r->w2;
3891         }
3892       else
3893         {
3894           if (r->p < 0 && decisionmap[-r->p] == 0)
3895             new = r->p;
3896           if (new || DECISIONMAP_FALSE(r->p))
3897             {
3898               dp = pool->whatprovidesdata + r->d;
3899               while ((p = *dp++) != 0)
3900                 {
3901                   if (new && p == new)
3902                     continue;
3903                   if (p < 0 && decisionmap[-p] == 0)
3904                     {
3905                       if (new)
3906                         {
3907                           new = 0;
3908                           break;
3909                         }
3910                       new = p;
3911                     }
3912                   else if (!DECISIONMAP_FALSE(p))
3913                     {
3914                       new = 0;
3915                       break;
3916                     }
3917                 }
3918             }
3919         }
3920       if (new)
3921         {
3922           POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
3923           decisionmap[-new] = -1;
3924           new = 0;
3925           n = 0;        /* redo all rules */
3926         }
3927     }
3928 }
3929
3930
3931 /*-------------------------------------------------------------------
3932  *
3933  * weaken solvable dependencies
3934  */
3935
3936 static void
3937 weaken_solvable_deps(Solver *solv, Id p)
3938 {
3939   int i;
3940   Rule *r;
3941
3942   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
3943     {
3944       if (r->p != -p)
3945         continue;
3946       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
3947         continue;       /* conflict */
3948       queue_push(&solv->weakruleq, i);
3949     }
3950 }
3951
3952 /********************************************************************/
3953 /* main() */
3954
3955 /*
3956  *
3957  * solve job queue
3958  *
3959  */
3960
3961 void
3962 solver_solve(Solver *solv, Queue *job)
3963 {
3964   Pool *pool = solv->pool;
3965   Repo *installed = solv->installed;
3966   int i;
3967   int oldnrules;
3968   Map addedmap;                /* '1' == have rpm-rules for solvable */
3969   Map installcandidatemap;
3970   Id how, what, select, name, weak, p, pp, d;
3971   Queue q, redoq;
3972   Solvable *s;
3973   int goterase;
3974   Rule *r;
3975   int now, solve_start;
3976
3977   solve_start = sat_timems(0);
3978   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
3979   POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide);
3980   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
3981   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
3982   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, allowvirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, solv->allowvirtualconflicts, solv->allowselfconflicts);
3983   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d\n", solv->obsoleteusesprovides, solv->implicitobsoleteusesprovides);
3984   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
3985   /* create whatprovides if not already there */
3986   if (!pool->whatprovides)
3987     pool_createwhatprovides(pool);
3988
3989   /* create obsolete index if needed */
3990   create_obsolete_index(solv);
3991
3992   /*
3993    * create basic rule set of all involved packages
3994    * use addedmap bitmap to make sure we don't create rules twice
3995    *
3996    */
3997
3998   /* create noobsolete map if needed */
3999   for (i = 0; i < job->count; i += 2)
4000     {
4001       how = job->elements[i] & ~SOLVER_WEAK;
4002       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
4003         continue;
4004       what = job->elements[i + 1];
4005       select = how & SOLVER_SELECTMASK;
4006       if (!solv->noobsoletes.size)
4007         map_init(&solv->noobsoletes, pool->nsolvables);
4008       FOR_JOB_SELECT(p, pp, select, what)
4009         MAPSET(&solv->noobsoletes, p);
4010     }
4011
4012   map_init(&addedmap, pool->nsolvables);
4013   map_init(&installcandidatemap, pool->nsolvables);
4014   queue_init(&q);
4015
4016   /*
4017    * always install our system solvable
4018    */
4019   MAPSET(&addedmap, SYSTEMSOLVABLE);
4020   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
4021   queue_push(&solv->decisionq_why, 0);
4022   solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */
4023
4024   now = sat_timems(0);
4025   /*
4026    * create rules for all package that could be involved with the solving
4027    * so called: rpm rules
4028    *
4029    */
4030   if (installed)
4031     {
4032       oldnrules = solv->nrules;
4033       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
4034       FOR_REPO_SOLVABLES(installed, p, s)
4035         addrpmrulesforsolvable(solv, s, &addedmap);
4036       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
4037       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
4038       oldnrules = solv->nrules;
4039       FOR_REPO_SOLVABLES(installed, p, s)
4040         addrpmrulesforupdaters(solv, s, &addedmap, 1);
4041       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
4042     }
4043
4044   /*
4045    * create rules for all packages involved in the job
4046    * (to be installed or removed)
4047    */
4048
4049   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
4050   oldnrules = solv->nrules;
4051   for (i = 0; i < job->count; i += 2)
4052     {
4053       how = job->elements[i];
4054       what = job->elements[i + 1];
4055       select = how & SOLVER_SELECTMASK;
4056
4057       switch (how & SOLVER_JOBMASK)
4058         {
4059         case SOLVER_INSTALL:
4060           FOR_JOB_SELECT(p, pp, select, what)
4061             {
4062               MAPSET(&installcandidatemap, p);
4063               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
4064             }
4065           break;
4066         case SOLVER_UPDATE:
4067           /* FIXME: semantics? */
4068           FOR_JOB_SELECT(p, pp, select, what)
4069             addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
4070           break;
4071         }
4072     }
4073   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
4074
4075   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
4076
4077   oldnrules = solv->nrules;
4078
4079     /*
4080      * add rules for suggests, enhances
4081      */
4082   addrpmrulesforweak(solv, &addedmap);
4083   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
4084
4085   IF_POOLDEBUG (SAT_DEBUG_STATS)
4086     {
4087       int possible = 0, installable = 0;
4088       for (i = 1; i < pool->nsolvables; i++)
4089         {
4090           if (pool_installable(pool, pool->solvables + i))
4091             installable++;
4092           if (MAPTST(&addedmap, i))
4093             possible++;
4094         }
4095       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
4096     }
4097
4098   /*
4099    * first pass done, we now have all the rpm rules we need.
4100    * unify existing rules before going over all job rules and
4101    * policy rules.
4102    * at this point the system is always solvable,
4103    * as an empty system (remove all packages) is a valid solution
4104    */
4105
4106   unifyrules(solv);                               /* remove duplicate rpm rules */
4107
4108   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
4109
4110   solv->directdecisions = solv->decisionq.count;
4111   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
4112   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
4113   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
4114
4115   /*
4116    * create feature rules
4117    *
4118    * foreach installed:
4119    *   create assertion (keep installed, if no update available)
4120    *   or
4121    *   create update rule (A|update1(A)|update2(A)|...)
4122    *
4123    * those are used later on to keep a version of the installed packages in
4124    * best effort mode
4125    */
4126
4127   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
4128   solv->featurerules = solv->nrules;              /* mark start of feature rules */
4129   if (installed)
4130     {
4131         /* foreach possibly installed solvable */
4132       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4133         {
4134           if (s->repo != installed)
4135             {
4136               addrule(solv, 0, 0);      /* create dummy rule */
4137               continue;
4138             }
4139           addupdaterule(solv, s, 1);    /* allow s to be updated */
4140         }
4141         /*
4142          * assert one rule per installed solvable,
4143          * either an assertion (A)
4144          * or a possible update (A|update1(A)|update2(A)|...)
4145          */
4146       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
4147     }
4148   solv->featurerules_end = solv->nrules;
4149
4150     /*
4151      * Add update rules for installed solvables
4152      *
4153      * almost identical to feature rules
4154      * except that downgrades/archchanges/vendorchanges are not allowed
4155      */
4156
4157   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
4158   solv->updaterules = solv->nrules;
4159
4160   if (installed)
4161     { /* foreach installed solvables */
4162       /* we create all update rules, but disable some later on depending on the job */
4163       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4164         {
4165           Rule *sr;
4166
4167           if (s->repo != installed)
4168             {
4169               addrule(solv, 0, 0);      /* create dummy rule */
4170               continue;
4171             }
4172           addupdaterule(solv, s, 0);    /* allowall = 0: downgrades not allowed */
4173             /*
4174              * check for and remove duplicate
4175              */
4176           r = solv->rules + solv->nrules - 1;           /* r: update rule */
4177           sr = r - (installed->end - installed->start); /* sr: feature rule */
4178           /* it's orphaned if there is no feature rule or the feature rule
4179            * consists just of the installed package */
4180           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
4181             queue_push(&solv->orphaned, i);
4182           if (!r->p)
4183             {
4184               assert(!sr->p);   /* can't have feature rule and no update rule */
4185               continue;
4186             }
4187           unifyrules_sortcmp_data = pool;
4188           if (!unifyrules_sortcmp(r, sr))
4189             {
4190               /* identical rule, kill unneeded rule */
4191               if (solv->allowuninstall)
4192                 {
4193                   /* keep feature rule, make it weak */
4194                   memset(r, 0, sizeof(*r));
4195                   queue_push(&solv->weakruleq, sr - solv->rules);
4196                 }
4197               else
4198                 {
4199                   /* keep update rule */
4200                   memset(sr, 0, sizeof(*sr));
4201                 }
4202             }
4203           else if (solv->allowuninstall)
4204             {
4205               /* make both feature and update rule weak */
4206               queue_push(&solv->weakruleq, r - solv->rules);
4207               queue_push(&solv->weakruleq, sr - solv->rules);
4208             }
4209           else
4210             disablerule(solv, sr);
4211         }
4212       /* consistency check: we added a rule for _every_ installed solvable */
4213       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
4214     }
4215   solv->updaterules_end = solv->nrules;
4216
4217
4218   /*
4219    * now add all job rules
4220    */
4221
4222   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
4223
4224   solv->jobrules = solv->nrules;
4225   for (i = 0; i < job->count; i += 2)
4226     {
4227       oldnrules = solv->nrules;
4228
4229       how = job->elements[i];
4230       what = job->elements[i + 1];
4231       weak = how & SOLVER_WEAK;
4232       select = how & SOLVER_SELECTMASK;
4233       switch (how & SOLVER_JOBMASK)
4234         {
4235         case SOLVER_INSTALL:
4236           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4237           if (select == SOLVER_SOLVABLE)
4238             {
4239               p = what;
4240               d = 0;
4241             }
4242           else
4243             {
4244               queue_empty(&q);
4245               FOR_JOB_SELECT(p, pp, select, what)
4246                 queue_push(&q, p);
4247               if (!q.count)
4248                 {
4249                   /* no candidate found, make this an impossible rule */
4250                   queue_push(&q, -SYSTEMSOLVABLE);
4251                 }
4252               p = queue_shift(&q);      /* get first candidate */
4253               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
4254             }
4255           addrule(solv, p, d);          /* add install rule */
4256           queue_push(&solv->ruletojob, i);
4257           if (weak)
4258             queue_push(&solv->weakruleq, solv->nrules - 1);
4259           break;
4260         case SOLVER_ERASE:
4261           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4262           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
4263             {
4264               /* special case for "erase a specific solvable": we also
4265                * erase all other solvables with that name, so that they
4266                * don't get picked up as replacement */
4267               name = pool->solvables[what].name;
4268               FOR_PROVIDES(p, pp, name)
4269                 {
4270                   if (p == what)
4271                     continue;
4272                   s = pool->solvables + p;
4273                   if (s->name != name)
4274                     continue;
4275                   /* keep other versions installed */
4276                   if (s->repo == solv->installed)
4277                     continue;
4278                   /* keep installcandidates of other jobs */
4279                   if (MAPTST(&installcandidatemap, p))
4280                     continue;
4281                   addrule(solv, -p, 0);                 /* remove by Id */
4282                   queue_push(&solv->ruletojob, i);
4283                   if (weak)
4284                     queue_push(&solv->weakruleq, solv->nrules - 1);
4285                 }
4286             }
4287           FOR_JOB_SELECT(p, pp, select, what)
4288             {
4289               addrule(solv, -p, 0);
4290               queue_push(&solv->ruletojob, i);
4291               if (weak)
4292                 queue_push(&solv->weakruleq, solv->nrules - 1);
4293             }
4294           break;
4295
4296         case SOLVER_UPDATE:
4297           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4298           if (select != SOLVER_SOLVABLE)
4299             break;
4300           s = pool->solvables + what;
4301           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
4302           addupdaterule(solv, s, 0);
4303           queue_push(&solv->ruletojob, i);
4304           if (weak)
4305             queue_push(&solv->weakruleq, solv->nrules - 1);
4306           break;
4307         case SOLVER_WEAKENDEPS:
4308           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4309           if (select != SOLVER_SOLVABLE)
4310             break;
4311           s = pool->solvables + what;
4312           weaken_solvable_deps(solv, what);
4313           break;
4314         case SOLVER_NOOBSOLETES:
4315           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4316           break;
4317         case SOLVER_LOCK:
4318           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4319           FOR_JOB_SELECT(p, pp, select, what)
4320             {
4321               s = pool->solvables + p;
4322               if (installed && s->repo == installed)
4323                 addrule(solv, p, 0);
4324               else
4325                 addrule(solv, -p, 0);
4326               queue_push(&solv->ruletojob, i);
4327               if (weak)
4328                 queue_push(&solv->weakruleq, solv->nrules - 1);
4329             }
4330           break;
4331         default:
4332           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
4333           break;
4334         }
4335
4336         /*
4337          * debug
4338          */
4339
4340       IF_POOLDEBUG (SAT_DEBUG_JOB)
4341         {
4342           int j;
4343           if (solv->nrules == oldnrules)
4344             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
4345           for (j = oldnrules; j < solv->nrules; j++)
4346             {
4347               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
4348               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
4349             }
4350         }
4351     }
4352   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
4353   solv->jobrules_end = solv->nrules;
4354
4355     /* all rules created
4356      * --------------------------------------------------------------
4357      * prepare for solving
4358      */
4359
4360   /* free unneeded memory */
4361   map_free(&addedmap);
4362   map_free(&installcandidatemap);
4363   queue_free(&q);
4364
4365   /* create weak map */
4366   map_init(&solv->weakrulemap, solv->nrules);
4367   for (i = 0; i < solv->weakruleq.count; i++)
4368     {
4369       p = solv->weakruleq.elements[i];
4370       MAPSET(&solv->weakrulemap, p);
4371     }
4372
4373   /* all new rules are learnt after this point */
4374   solv->learntrules = solv->nrules;
4375
4376   /* create assertion index. it is only used to speed up
4377    * makeruledecsions() a bit */
4378   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
4379     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
4380       queue_push(&solv->ruleassertions, i);
4381
4382   /* disable update rules that conflict with our job */
4383   disableupdaterules(solv, job, -1);
4384
4385   /* make decisions based on job/update assertions */
4386   makeruledecisions(solv);
4387
4388   /* create watches chains */
4389   makewatches(solv);
4390
4391   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4392
4393   /*
4394    * ********************************************
4395    * solve!
4396    * ********************************************
4397    */
4398
4399   now = sat_timems(0);
4400   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4401   POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
4402
4403   queue_init(&redoq);
4404   goterase = 0;
4405   /* disable all erase jobs (including weak "keep uninstalled" rules) */
4406   for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
4407     {
4408       if (r->d < 0)     /* disabled ? */
4409         continue;
4410       if (r->p > 0)     /* install job? */
4411         continue;
4412       disablerule(solv, r);
4413       goterase++;
4414     }
4415
4416   if (goterase)
4417     {
4418       enabledisablelearntrules(solv);
4419       removedisabledconflicts(solv, &redoq);
4420     }
4421
4422   /*
4423    * find recommended packages
4424    */
4425
4426   /* if redoq.count == 0 we already found all recommended in the
4427    * solver run */
4428   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
4429     {
4430       Id rec, *recp, p, pp;
4431
4432       /* create map of all recommened packages */
4433       solv->recommends_index = -1;
4434       MAPZERO(&solv->recommendsmap);
4435       for (i = 0; i < solv->decisionq.count; i++)
4436         {
4437           p = solv->decisionq.elements[i];
4438           if (p < 0)
4439             continue;
4440           s = pool->solvables + p;
4441           if (s->recommends)
4442             {
4443               recp = s->repo->idarraydata + s->recommends;
4444               while ((rec = *recp++) != 0)
4445                 {
4446                   FOR_PROVIDES(p, pp, rec)
4447                     if (solv->decisionmap[p] > 0)
4448                       break;
4449                   if (p)
4450                     {
4451                       if (!solv->dontshowinstalledrecommended)
4452                         {
4453                           FOR_PROVIDES(p, pp, rec)
4454                             if (solv->decisionmap[p] > 0)
4455                               MAPSET(&solv->recommendsmap, p);
4456                         }
4457                       continue; /* p != 0: already fulfilled */
4458                     }
4459                   FOR_PROVIDES(p, pp, rec)
4460                     MAPSET(&solv->recommendsmap, p);
4461                 }
4462             }
4463         }
4464       for (i = 1; i < pool->nsolvables; i++)
4465         {
4466           if (solv->decisionmap[i] < 0)
4467             continue;
4468           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4469             continue;
4470           s = pool->solvables + i;
4471           if (!MAPTST(&solv->recommendsmap, i))
4472             {
4473               if (!s->supplements)
4474                 continue;
4475               if (!pool_installable(pool, s))
4476                 continue;
4477               if (!solver_is_supplementing(solv, s))
4478                 continue;
4479             }
4480           if (solv->dontinstallrecommended)
4481             queue_push(&solv->recommendations, i);
4482           else
4483             queue_pushunique(&solv->recommendations, i);
4484         }
4485       /* we use MODE_SUGGEST here so that repo prio is ignored */
4486       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
4487     }
4488
4489   /*
4490    * find suggested packages
4491    */
4492
4493   if (1)
4494     {
4495       Id sug, *sugp, p, pp;
4496
4497       /* create map of all suggests that are still open */
4498       solv->recommends_index = -1;
4499       MAPZERO(&solv->suggestsmap);
4500       for (i = 0; i < solv->decisionq.count; i++)
4501         {
4502           p = solv->decisionq.elements[i];
4503           if (p < 0)
4504             continue;
4505           s = pool->solvables + p;
4506           if (s->suggests)
4507             {
4508               sugp = s->repo->idarraydata + s->suggests;
4509               while ((sug = *sugp++) != 0)
4510                 {
4511                   FOR_PROVIDES(p, pp, sug)
4512                     if (solv->decisionmap[p] > 0)
4513                       break;
4514                   if (p)
4515                     {
4516                       if (!solv->dontshowinstalledrecommended)
4517                         {
4518                           FOR_PROVIDES(p, pp, sug)
4519                             if (solv->decisionmap[p] > 0)
4520                               MAPSET(&solv->suggestsmap, p);
4521                         }
4522                       continue; /* already fulfilled */
4523                     }
4524                   FOR_PROVIDES(p, pp, sug)
4525                     MAPSET(&solv->suggestsmap, p);
4526                 }
4527             }
4528         }
4529       for (i = 1; i < pool->nsolvables; i++)
4530         {
4531           if (solv->decisionmap[i] < 0)
4532             continue;
4533           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4534             continue;
4535           s = pool->solvables + i;
4536           if (!MAPTST(&solv->suggestsmap, i))
4537             {
4538               if (!s->enhances)
4539                 continue;
4540               if (!pool_installable(pool, s))
4541                 continue;
4542               if (!solver_is_enhancing(solv, s))
4543                 continue;
4544             }
4545           queue_push(&solv->suggestions, i);
4546         }
4547       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
4548     }
4549
4550   if (redoq.count)
4551     {
4552       /* restore decisionmap */
4553       for (i = 0; i < redoq.count; i += 2)
4554         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4555     }
4556
4557     /*
4558      * if unsolvable, prepare solutions
4559      */
4560
4561   if (solv->problems.count)
4562     {
4563       int recocount = solv->recommendations.count;
4564       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
4565       queue_empty(&redoq);
4566       for (i = 0; i < solv->decisionq.count; i++)
4567         {
4568           Id p = solv->decisionq.elements[i];
4569           queue_push(&redoq, p);
4570           queue_push(&redoq, solv->decisionq_why.elements[i]);
4571           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4572         }
4573       problems_to_solutions(solv, job);
4574       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4575       queue_empty(&solv->decisionq);
4576       queue_empty(&solv->decisionq_why);
4577       for (i = 0; i < redoq.count; i += 3)
4578         {
4579           Id p = redoq.elements[i];
4580           queue_push(&solv->decisionq, p);
4581           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4582           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4583         }
4584       solv->recommendations.count = recocount;
4585     }
4586
4587   queue_free(&redoq);
4588   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
4589   POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
4590 }
4591
4592 /***********************************************************************/
4593 /* disk usage computations */
4594
4595 /*-------------------------------------------------------------------
4596  *
4597  * calculate DU changes
4598  */
4599
4600 void
4601 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4602 {
4603   Map installedmap;
4604
4605   solver_create_state_maps(solv, &installedmap, 0);
4606   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
4607   map_free(&installedmap);
4608 }
4609
4610
4611 /*-------------------------------------------------------------------
4612  *
4613  * calculate changes in install size
4614  */
4615
4616 int
4617 solver_calc_installsizechange(Solver *solv)
4618 {
4619   Map installedmap;
4620   int change;
4621
4622   solver_create_state_maps(solv, &installedmap, 0);
4623   change = pool_calc_installsizechange(solv->pool, &installedmap);
4624   map_free(&installedmap);
4625   return change;
4626 }
4627
4628 #define FIND_INVOLVED_DEBUG 0
4629 void
4630 solver_find_involved(Solver *solv, Queue *installedq, Solvable *ts, Queue *q)
4631 {
4632   Pool *pool = solv->pool;
4633   Map im;
4634   Map installedm;
4635   Solvable *s;
4636   Queue iq;
4637   Queue installedq_internal;
4638   Id tp, ip, p, pp, req, *reqp, sup, *supp;
4639   int i, count;
4640
4641   tp = ts - pool->solvables;
4642   queue_init(&iq);
4643   queue_init(&installedq_internal);
4644   map_init(&im, pool->nsolvables);
4645   map_init(&installedm, pool->nsolvables);
4646
4647   if (!installedq)
4648     {
4649       installedq = &installedq_internal;
4650       if (solv->installed)
4651         {
4652           for (ip = solv->installed->start; ip < solv->installed->end; ip++)
4653             {
4654               s = pool->solvables + ip;
4655               if (s->repo != solv->installed)
4656                 continue;
4657               queue_push(installedq, ip);
4658             }
4659         }
4660     }
4661   for (i = 0; i < installedq->count; i++)
4662     {
4663       ip = installedq->elements[i];
4664       MAPSET(&installedm, ip);
4665       MAPSET(&im, ip);
4666     }
4667
4668   queue_push(&iq, ts - pool->solvables);
4669   while (iq.count)
4670     {
4671       ip = queue_shift(&iq);
4672       if (!MAPTST(&im, ip))
4673         continue;
4674       if (!MAPTST(&installedm, ip))
4675         continue;
4676       MAPCLR(&im, ip);
4677       s = pool->solvables + ip;
4678 #if FIND_INVOLVED_DEBUG
4679       printf("hello %s\n", solvable2str(pool, s));
4680 #endif
4681       if (s->requires)
4682         {
4683           reqp = s->repo->idarraydata + s->requires;
4684           while ((req = *reqp++) != 0)
4685             {
4686               if (req == SOLVABLE_PREREQMARKER)
4687                 continue;
4688               /* count number of installed packages that match */
4689               count = 0;
4690               FOR_PROVIDES(p, pp, req)
4691                 if (MAPTST(&installedm, p))
4692                   count++;
4693               if (count > 1)
4694                 continue;
4695               FOR_PROVIDES(p, pp, req)
4696                 {
4697                   if (MAPTST(&im, p))
4698                     {
4699 #if FIND_INVOLVED_DEBUG
4700                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4701 #endif
4702                       queue_push(&iq, p);
4703                     }
4704                 }
4705             }
4706         }
4707       if (s->recommends)
4708         {
4709           reqp = s->repo->idarraydata + s->recommends;
4710           while ((req = *reqp++) != 0)
4711             {
4712               count = 0;
4713               FOR_PROVIDES(p, pp, req)
4714                 if (MAPTST(&installedm, p))
4715                   count++;
4716               if (count > 1)
4717                 continue;
4718               FOR_PROVIDES(p, pp, req)
4719                 {
4720                   if (MAPTST(&im, p))
4721                     {
4722 #if FIND_INVOLVED_DEBUG
4723                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4724 #endif
4725                       queue_push(&iq, p);
4726                     }
4727                 }
4728             }
4729         }
4730       if (!iq.count)
4731         {
4732           /* supplements pass */
4733           for (i = 0; i < installedq->count; i++)
4734             {
4735               ip = installedq->elements[i];
4736               s = pool->solvables + ip;
4737               if (!s->supplements)
4738                 continue;
4739               if (!MAPTST(&im, ip))
4740                 continue;
4741               supp = s->repo->idarraydata + s->supplements;
4742               while ((sup = *supp++) != 0)
4743                 if (!dep_possible(solv, sup, &im) && dep_possible(solv, sup, &installedm))
4744                   break;
4745               /* no longer supplemented, also erase */
4746               if (sup)
4747                 {
4748 #if FIND_INVOLVED_DEBUG
4749                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
4750 #endif
4751                   queue_push(&iq, ip);
4752                 }
4753             }
4754         }
4755     }
4756
4757   for (i = 0; i < installedq->count; i++)
4758     {
4759       ip = installedq->elements[i];
4760       if (MAPTST(&im, ip))
4761         queue_push(&iq, ip);
4762     }
4763
4764   while (iq.count)
4765     {
4766       ip = queue_shift(&iq);
4767       if (!MAPTST(&installedm, ip))
4768         continue;
4769       s = pool->solvables + ip;
4770 #if FIND_INVOLVED_DEBUG
4771       printf("bye %s\n", solvable2str(pool, s));
4772 #endif
4773       if (s->requires)
4774         {
4775           reqp = s->repo->idarraydata + s->requires;
4776           while ((req = *reqp++) != 0)
4777             {
4778               FOR_PROVIDES(p, pp, req)
4779                 {
4780                   if (!MAPTST(&im, p))
4781                     {
4782                       if (p == tp)
4783                         continue;
4784 #if FIND_INVOLVED_DEBUG
4785                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4786 #endif
4787                       MAPSET(&im, p);
4788                       queue_push(&iq, p);
4789                     }
4790                 }
4791             }
4792         }
4793       if (s->recommends)
4794         {
4795           reqp = s->repo->idarraydata + s->recommends;
4796           while ((req = *reqp++) != 0)
4797             {
4798               FOR_PROVIDES(p, pp, req)
4799                 {
4800                   if (!MAPTST(&im, p))
4801                     {
4802                       if (p == tp)
4803                         continue;
4804 #if FIND_INVOLVED_DEBUG
4805                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4806 #endif
4807                       MAPSET(&im, p);
4808                       queue_push(&iq, p);
4809                     }
4810                 }
4811             }
4812         }
4813       if (!iq.count)
4814         {
4815           /* supplements pass */
4816           for (i = 0; i < installedq->count; i++)
4817             {
4818               ip = installedq->elements[i];
4819               if (ip == tp)
4820                 continue;
4821               s = pool->solvables + ip;
4822               if (!s->supplements)
4823                 continue;
4824               if (MAPTST(&im, ip))
4825                 continue;
4826               supp = s->repo->idarraydata + s->supplements;
4827               while ((sup = *supp++) != 0)
4828                 if (dep_possible(solv, sup, &im))
4829                   break;
4830               if (sup)
4831                 {
4832 #if FIND_INVOLVED_DEBUG
4833                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
4834 #endif
4835                   MAPSET(&im, ip);
4836                   queue_push(&iq, ip);
4837                 }
4838             }
4839         }
4840     }
4841
4842   queue_free(&iq);
4843
4844   /* convert map into result */
4845   for (i = 0; i < installedq->count; i++)
4846     {
4847       ip = installedq->elements[i];
4848       if (MAPTST(&im, ip))
4849         continue;
4850       if (ip == ts - pool->solvables)
4851         continue;
4852       queue_push(q, ip);
4853     }
4854   map_free(&im);
4855   map_free(&installedm);
4856   queue_free(&installedq_internal);
4857 }
4858
4859 /* EOF */