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;       /* orphaned */
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 -SYSTEMSOLVABLE;
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   if (!allow_all && qs.count && solv->noobsoletes.size)
1520     {
1521       int i, j;
1522
1523       d = pool_queuetowhatprovides(pool, &qs);
1524       /* filter out all noobsoletes packages as they don't update */
1525       for (i = j = 0; i < qs.count; i++)
1526         {
1527           if (MAPTST(&solv->noobsoletes, qs.elements[i]))
1528             {
1529               /* it's ok if they have same nevra */
1530               Solvable *ps = pool->solvables + qs.elements[i];
1531               if (ps->name != s->name || ps->evr != s->evr || ps->arch != s->arch)
1532                 continue;
1533             }
1534           qs.elements[j++] = qs.elements[i];
1535         }
1536       if (j == 0 && p == -SYSTEMSOLVABLE && solv->distupgrade)
1537         {
1538           queue_push(&solv->orphaned, s - pool->solvables);     /* treat as orphaned */
1539           j = qs.count;
1540         }
1541       if (j < qs.count)
1542         {
1543           if (d && solv->updatesystem && solv->installed && s->repo == solv->installed)
1544             {
1545               if (!solv->multiversionupdaters)
1546                 solv->multiversionupdaters = sat_calloc(solv->installed->end - solv->installed->start, sizeof(Id));
1547               solv->multiversionupdaters[s - pool->solvables - solv->installed->start] = d;
1548             }
1549           qs.count = j;
1550         }
1551     }
1552   if (qs.count && p == -SYSTEMSOLVABLE)
1553     p = queue_shift(&qs);
1554   d = qs.count ? pool_queuetowhatprovides(pool, &qs) : 0;
1555   queue_free(&qs);
1556   addrule(solv, p, d);  /* allow update of s */
1557   POOL_DEBUG(SAT_DEBUG_SCHUBI, "-----  addupdaterule end -----\n");
1558 }
1559
1560
1561 /********************************************************************/
1562 /* watches */
1563
1564
1565 /*-------------------------------------------------------------------
1566  * makewatches
1567  *
1568  * initial setup for all watches
1569  */
1570
1571 static void
1572 makewatches(Solver *solv)
1573 {
1574   Rule *r;
1575   int i;
1576   int nsolvables = solv->pool->nsolvables;
1577
1578   sat_free(solv->watches);
1579                                        /* lower half for removals, upper half for installs */
1580   solv->watches = sat_calloc(2 * nsolvables, sizeof(Id));
1581 #if 1
1582   /* do it reverse so rpm rules get triggered first (XXX: obsolete?) */
1583   for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
1584 #else
1585   for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
1586 #endif
1587     {
1588       if (!r->w2)               /* assertions do not need watches */
1589         continue;
1590
1591       /* see addwatches_rule(solv, r) */
1592       r->n1 = solv->watches[nsolvables + r->w1];
1593       solv->watches[nsolvables + r->w1] = r - solv->rules;
1594
1595       r->n2 = solv->watches[nsolvables + r->w2];
1596       solv->watches[nsolvables + r->w2] = r - solv->rules;
1597     }
1598 }
1599
1600
1601 /*-------------------------------------------------------------------
1602  *
1603  * add watches (for rule)
1604  * sets up watches for a single rule
1605  *
1606  * see also makewatches()
1607  */
1608
1609 static inline void
1610 addwatches_rule(Solver *solv, Rule *r)
1611 {
1612   int nsolvables = solv->pool->nsolvables;
1613
1614   r->n1 = solv->watches[nsolvables + r->w1];
1615   solv->watches[nsolvables + r->w1] = r - solv->rules;
1616
1617   r->n2 = solv->watches[nsolvables + r->w2];
1618   solv->watches[nsolvables + r->w2] = r - solv->rules;
1619 }
1620
1621
1622 /********************************************************************/
1623 /*
1624  * rule propagation
1625  */
1626
1627
1628 /* shortcuts to check if a literal (positive or negative) assignment
1629  * evaluates to 'true' or 'false'
1630  */
1631 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
1632 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
1633 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0)
1634
1635 /*-------------------------------------------------------------------
1636  *
1637  * propagate
1638  *
1639  * make decision and propagate to all rules
1640  *
1641  * Evaluate each term affected by the decision (linked through watches)
1642  * If we find unit rules we make new decisions based on them
1643  *
1644  * Everything's fixed there, it's just finding rules that are
1645  * unit.
1646  *
1647  * return : 0 = everything is OK
1648  *          rule = conflict found in this rule
1649  */
1650
1651 static Rule *
1652 propagate(Solver *solv, int level)
1653 {
1654   Pool *pool = solv->pool;
1655   Id *rp, *next_rp;           /* rule pointer, next rule pointer in linked list */
1656   Rule *r;                    /* rule */
1657   Id p, pkg, other_watch;
1658   Id *dp;
1659   Id *decisionmap = solv->decisionmap;
1660
1661   Id *watches = solv->watches + pool->nsolvables;   /* place ptr in middle */
1662
1663   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
1664
1665   /* foreach non-propagated decision */
1666   while (solv->propagate_index < solv->decisionq.count)
1667     {
1668         /*
1669          * 'pkg' was just decided
1670          * negate because our watches trigger if literal goes FALSE
1671          */
1672       pkg = -solv->decisionq.elements[solv->propagate_index++];
1673
1674       IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1675         {
1676           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
1677           solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
1678         }
1679
1680       /* foreach rule where 'pkg' is now FALSE */
1681       for (rp = watches + pkg; *rp; rp = next_rp)
1682         {
1683           r = solv->rules + *rp;
1684           if (r->d < 0)
1685             {
1686               /* rule is disabled, goto next */
1687               if (pkg == r->w1)
1688                 next_rp = &r->n1;
1689               else
1690                 next_rp = &r->n2;
1691               continue;
1692             }
1693
1694           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1695             {
1696               POOL_DEBUG(SAT_DEBUG_PROPAGATE,"  watch triggered ");
1697               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1698             }
1699
1700             /* 'pkg' was just decided (was set to FALSE)
1701              *
1702              *  now find other literal watch, check clause
1703              *   and advance on linked list
1704              */
1705           if (pkg == r->w1)
1706             {
1707               other_watch = r->w2;
1708               next_rp = &r->n1;
1709             }
1710           else
1711             {
1712               other_watch = r->w1;
1713               next_rp = &r->n2;
1714             }
1715
1716             /*
1717              * This term is already true (through the other literal)
1718              * so we have nothing to do
1719              */
1720           if (DECISIONMAP_TRUE(other_watch))
1721             continue;
1722
1723             /*
1724              * The other literal is FALSE or UNDEF
1725              *
1726              */
1727
1728           if (r->d)
1729             {
1730               /* Not a binary clause, try to move our watch.
1731                *
1732                * Go over all literals and find one that is
1733                *   not other_watch
1734                *   and not FALSE
1735                *
1736                * (TRUE is also ok, in that case the rule is fulfilled)
1737                */
1738               if (r->p                                /* we have a 'p' */
1739                   && r->p != other_watch              /* which is not watched */
1740                   && !DECISIONMAP_FALSE(r->p))        /* and not FALSE */
1741                 {
1742                   p = r->p;
1743                 }
1744               else                                    /* go find a 'd' to make 'true' */
1745                 {
1746                   /* foreach p in 'd'
1747                      we just iterate sequentially, doing it in another order just changes the order of decisions, not the decisions itself
1748                    */
1749                   for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1750                     {
1751                       if (p != other_watch              /* which is not watched */
1752                           && !DECISIONMAP_FALSE(p))     /* and not FALSE */
1753                         break;
1754                     }
1755                 }
1756
1757               if (p)
1758                 {
1759                   /*
1760                    * if we found some p that is UNDEF or TRUE, move
1761                    * watch to it
1762                    */
1763                   IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1764                     {
1765                       if (p > 0)
1766                         POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1767                       else
1768                         POOL_DEBUG(SAT_DEBUG_PROPAGATE,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1769                     }
1770
1771                   *rp = *next_rp;
1772                   next_rp = rp;
1773
1774                   if (pkg == r->w1)
1775                     {
1776                       r->w1 = p;
1777                       r->n1 = watches[p];
1778                     }
1779                   else
1780                     {
1781                       r->w2 = p;
1782                       r->n2 = watches[p];
1783                     }
1784                   watches[p] = r - solv->rules;
1785                   continue;
1786                 }
1787               /* search failed, thus all unwatched literals are FALSE */
1788
1789             } /* not binary */
1790
1791             /*
1792              * unit clause found, set literal other_watch to TRUE
1793              */
1794
1795           if (DECISIONMAP_FALSE(other_watch))      /* check if literal is FALSE */
1796             return r;                              /* eek, a conflict! */
1797
1798           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1799             {
1800               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "   unit ");
1801               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1802             }
1803
1804           if (other_watch > 0)
1805             decisionmap[other_watch] = level;    /* install! */
1806           else
1807             decisionmap[-other_watch] = -level;  /* remove! */
1808
1809           queue_push(&solv->decisionq, other_watch);
1810           queue_push(&solv->decisionq_why, r - solv->rules);
1811
1812           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1813             {
1814               Solvable *s = pool->solvables + (other_watch > 0 ? other_watch : -other_watch);
1815               if (other_watch > 0)
1816                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to install %s\n", solvable2str(pool, s));
1817               else
1818                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to conflict %s\n", solvable2str(pool, s));
1819             }
1820
1821         } /* foreach rule involving 'pkg' */
1822
1823     } /* while we have non-decided decisions */
1824
1825   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
1826
1827   return 0;     /* all is well */
1828 }
1829
1830
1831 /********************************************************************/
1832 /* Analysis */
1833
1834 /*-------------------------------------------------------------------
1835  *
1836  * analyze
1837  *   and learn
1838  */
1839
1840 static int
1841 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
1842 {
1843   Pool *pool = solv->pool;
1844   Queue r;
1845   int rlevel = 1;
1846   Map seen;             /* global? */
1847   Id d, v, vv, *dp, why;
1848   int l, i, idx;
1849   int num = 0, l1num = 0;
1850   int learnt_why = solv->learnt_pool.count;
1851   Id *decisionmap = solv->decisionmap;
1852
1853   queue_init(&r);
1854
1855   POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
1856   map_init(&seen, pool->nsolvables);
1857   idx = solv->decisionq.count;
1858   for (;;)
1859     {
1860       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1861         solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1862       queue_push(&solv->learnt_pool, c - solv->rules);
1863       d = c->d < 0 ? -c->d - 1 : c->d;
1864       dp = d ? pool->whatprovidesdata + d : 0;
1865       /* go through all literals of the rule */
1866       for (i = -1; ; i++)
1867         {
1868           if (i == -1)
1869             v = c->p;
1870           else if (d == 0)
1871             v = i ? 0 : c->w2;
1872           else
1873             v = *dp++;
1874           if (v == 0)
1875             break;
1876
1877           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1878             continue;
1879           vv = v > 0 ? v : -v;
1880           if (MAPTST(&seen, vv))
1881             continue;
1882           l = solv->decisionmap[vv];
1883           if (l < 0)
1884             l = -l;
1885           MAPSET(&seen, vv);
1886           if (l == 1)
1887             l1num++;                    /* need to do this one in level1 pass */
1888           else if (l == level)
1889             num++;                      /* need to do this one as well */
1890           else
1891             {
1892               queue_push(&r, v);        /* not level1 or conflict level, add to new rule */
1893               if (l > rlevel)
1894                 rlevel = l;
1895             }
1896         }
1897 l1retry:
1898       if (!num && !--l1num)
1899         break;  /* all level 1 literals done */
1900       for (;;)
1901         {
1902           assert(idx > 0);
1903           v = solv->decisionq.elements[--idx];
1904           vv = v > 0 ? v : -v;
1905           if (MAPTST(&seen, vv))
1906             break;
1907         }
1908       MAPCLR(&seen, vv);
1909       if (num && --num == 0)
1910         {
1911           *pr = -v;     /* so that v doesn't get lost */
1912           if (!l1num)
1913             break;
1914           POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1915           for (i = 0; i < r.count; i++)
1916             {
1917               v = r.elements[i];
1918               MAPCLR(&seen, v > 0 ? v : -v);
1919             }
1920           /* only level 1 marks left */
1921           l1num++;
1922           goto l1retry;
1923         }
1924       why = solv->decisionq_why.elements[idx];
1925       if (!why)                 /* just in case, maybe for SYSTEMSOLVABLE */
1926         goto l1retry;
1927       c = solv->rules + why;
1928     }
1929   map_free(&seen);
1930
1931   if (r.count == 0)
1932     *dr = 0;
1933   else if (r.count == 1 && r.elements[0] < 0)
1934     *dr = r.elements[0];
1935   else
1936     *dr = pool_queuetowhatprovides(pool, &r);
1937   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1938     {
1939       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1940       solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1941       for (i = 0; i < r.count; i++)
1942         solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1943     }
1944   /* push end marker on learnt reasons stack */
1945   queue_push(&solv->learnt_pool, 0);
1946   if (whyp)
1947     *whyp = learnt_why;
1948   solv->stats_learned++;
1949   return rlevel;
1950 }
1951
1952
1953 /*-------------------------------------------------------------------
1954  *
1955  * reset_solver
1956  *
1957  * reset the solver decisions to right after the rpm rules.
1958  * called after rules have been enabled/disabled
1959  */
1960
1961 static void
1962 reset_solver(Solver *solv)
1963 {
1964   Pool *pool = solv->pool;
1965   int i;
1966   Id v;
1967
1968   /* rewind decisions to direct rpm rule assertions */
1969   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1970     {
1971       v = solv->decisionq.elements[i];
1972       solv->decisionmap[v > 0 ? v : -v] = 0;
1973     }
1974
1975   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1976
1977   solv->decisionq_why.count = solv->directdecisions;
1978   solv->decisionq.count = solv->directdecisions;
1979   solv->recommends_index = -1;
1980   solv->propagate_index = 0;
1981
1982   /* adapt learnt rule status to new set of enabled/disabled rules */
1983   enabledisablelearntrules(solv);
1984
1985   /* redo all job/update decisions */
1986   makeruledecisions(solv);
1987   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1988 }
1989
1990
1991 /*-------------------------------------------------------------------
1992  *
1993  * analyze_unsolvable_rule
1994  */
1995
1996 static void
1997 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1998 {
1999   Pool *pool = solv->pool;
2000   int i;
2001   Id why = r - solv->rules;
2002
2003   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
2004     solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
2005   if (solv->learntrules && why >= solv->learntrules)
2006     {
2007       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
2008         if (solv->learnt_pool.elements[i] > 0)
2009           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
2010       return;
2011     }
2012   if (MAPTST(&solv->weakrulemap, why))
2013     if (!*lastweakp || why > *lastweakp)
2014       *lastweakp = why;
2015   /* do not add rpm rules to problem */
2016   if (why < solv->rpmrules_end)
2017     return;
2018   /* turn rule into problem */
2019   if (why >= solv->jobrules && why < solv->jobrules_end)
2020     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
2021   /* return if problem already countains our rule */
2022   if (solv->problems.count)
2023     {
2024       for (i = solv->problems.count - 1; i >= 0; i--)
2025         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
2026           break;
2027         else if (solv->problems.elements[i] == why)
2028           return;
2029     }
2030   queue_push(&solv->problems, why);
2031 }
2032
2033
2034 /*-------------------------------------------------------------------
2035  *
2036  * analyze_unsolvable
2037  *
2038  * return: 1 - disabled some rules, try again
2039  *         0 - hopeless
2040  */
2041
2042 static int
2043 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
2044 {
2045   Pool *pool = solv->pool;
2046   Rule *r;
2047   Map seen;             /* global to speed things up? */
2048   Id d, v, vv, *dp, why;
2049   int l, i, idx;
2050   Id *decisionmap = solv->decisionmap;
2051   int oldproblemcount;
2052   int oldlearntpoolcount;
2053   Id lastweak;
2054
2055   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
2056   solv->stats_unsolvable++;
2057   oldproblemcount = solv->problems.count;
2058   oldlearntpoolcount = solv->learnt_pool.count;
2059
2060   /* make room for proof index */
2061   /* must update it later, as analyze_unsolvable_rule would confuse
2062    * it with a rule index if we put the real value in already */
2063   queue_push(&solv->problems, 0);
2064
2065   r = cr;
2066   map_init(&seen, pool->nsolvables);
2067   queue_push(&solv->learnt_pool, r - solv->rules);
2068   lastweak = 0;
2069   analyze_unsolvable_rule(solv, r, &lastweak);
2070   d = r->d < 0 ? -r->d - 1 : r->d;
2071   dp = d ? pool->whatprovidesdata + d : 0;
2072   for (i = -1; ; i++)
2073     {
2074       if (i == -1)
2075         v = r->p;
2076       else if (d == 0)
2077         v = i ? 0 : r->w2;
2078       else
2079         v = *dp++;
2080       if (v == 0)
2081         break;
2082       if (DECISIONMAP_TRUE(v))  /* the one true literal */
2083           continue;
2084       vv = v > 0 ? v : -v;
2085       l = solv->decisionmap[vv];
2086       if (l < 0)
2087         l = -l;
2088       MAPSET(&seen, vv);
2089     }
2090   idx = solv->decisionq.count;
2091   while (idx > 0)
2092     {
2093       v = solv->decisionq.elements[--idx];
2094       vv = v > 0 ? v : -v;
2095       if (!MAPTST(&seen, vv))
2096         continue;
2097       why = solv->decisionq_why.elements[idx];
2098       queue_push(&solv->learnt_pool, why);
2099       r = solv->rules + why;
2100       analyze_unsolvable_rule(solv, r, &lastweak);
2101       d = r->d < 0 ? -r->d - 1 : r->d;
2102       dp = d ? pool->whatprovidesdata + d : 0;
2103       for (i = -1; ; i++)
2104         {
2105           if (i == -1)
2106             v = r->p;
2107           else if (d == 0)
2108             v = i ? 0 : r->w2;
2109           else
2110             v = *dp++;
2111           if (v == 0)
2112             break;
2113           if (DECISIONMAP_TRUE(v))      /* the one true literal */
2114               continue;
2115           vv = v > 0 ? v : -v;
2116           l = solv->decisionmap[vv];
2117           if (l < 0)
2118             l = -l;
2119           MAPSET(&seen, vv);
2120         }
2121     }
2122   map_free(&seen);
2123   queue_push(&solv->problems, 0);       /* mark end of this problem */
2124
2125   if (lastweak)
2126     {
2127       /* disable last weak rule */
2128       solv->problems.count = oldproblemcount;
2129       solv->learnt_pool.count = oldlearntpoolcount;
2130       r = solv->rules + lastweak;
2131       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
2132       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
2133       disablerule(solv, r);
2134       reset_solver(solv);
2135       return 1;
2136     }
2137
2138   /* finish proof */
2139   queue_push(&solv->learnt_pool, 0);
2140   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
2141
2142   if (disablerules)
2143     {
2144       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
2145         disableproblem(solv, solv->problems.elements[i]);
2146       /* XXX: might want to enable all weak rules again */
2147       reset_solver(solv);
2148       return 1;
2149     }
2150   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
2151   return 0;
2152 }
2153
2154
2155 /********************************************************************/
2156 /* Decision revert */
2157
2158 /*-------------------------------------------------------------------
2159  *
2160  * revert
2161  * revert decision at level
2162  */
2163
2164 static void
2165 revert(Solver *solv, int level)
2166 {
2167   Pool *pool = solv->pool;
2168   Id v, vv;
2169   while (solv->decisionq.count)
2170     {
2171       v = solv->decisionq.elements[solv->decisionq.count - 1];
2172       vv = v > 0 ? v : -v;
2173       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
2174         break;
2175       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
2176       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
2177         solv->recommendations.count--;
2178       solv->decisionmap[vv] = 0;
2179       solv->decisionq.count--;
2180       solv->decisionq_why.count--;
2181       solv->propagate_index = solv->decisionq.count;
2182     }
2183   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
2184     {
2185       solv->branches.count--;
2186       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
2187         solv->branches.count--;
2188     }
2189   solv->recommends_index = -1;
2190 }
2191
2192
2193 /*-------------------------------------------------------------------
2194  *
2195  * watch2onhighest - put watch2 on literal with highest level
2196  */
2197
2198 static inline void
2199 watch2onhighest(Solver *solv, Rule *r)
2200 {
2201   int l, wl = 0;
2202   Id d, v, *dp;
2203
2204   d = r->d < 0 ? -r->d - 1 : r->d;
2205   if (!d)
2206     return;     /* binary rule, both watches are set */
2207   dp = solv->pool->whatprovidesdata + d;
2208   while ((v = *dp++) != 0)
2209     {
2210       l = solv->decisionmap[v < 0 ? -v : v];
2211       if (l < 0)
2212         l = -l;
2213       if (l > wl)
2214         {
2215           r->w2 = dp[-1];
2216           wl = l;
2217         }
2218     }
2219 }
2220
2221
2222 /*-------------------------------------------------------------------
2223  *
2224  * setpropagatelearn
2225  *
2226  * add free decision (solvable to install) to decisionq
2227  * increase level and propagate decision
2228  * return if no conflict.
2229  *
2230  * in conflict case, analyze conflict rule, add resulting
2231  * rule to learnt rule set, make decision from learnt
2232  * rule (always unit) and re-propagate.
2233  *
2234  * returns the new solver level or 0 if unsolvable
2235  *
2236  */
2237
2238 static int
2239 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
2240 {
2241   Pool *pool = solv->pool;
2242   Rule *r;
2243   Id p = 0, d = 0;
2244   int l, why;
2245
2246   if (decision)
2247     {
2248       level++;
2249       if (decision > 0)
2250         solv->decisionmap[decision] = level;
2251       else
2252         solv->decisionmap[-decision] = -level;
2253       queue_push(&solv->decisionq, decision);
2254       queue_push(&solv->decisionq_why, 0);
2255     }
2256   for (;;)
2257     {
2258       r = propagate(solv, level);
2259       if (!r)
2260         break;
2261       if (level == 1)
2262         return analyze_unsolvable(solv, r, disablerules);
2263       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
2264       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
2265       assert(l > 0 && l < level);
2266       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
2267       level = l;
2268       revert(solv, level);
2269       r = addrule(solv, p, d);       /* p requires d */
2270       assert(r);
2271       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
2272       queue_push(&solv->learnt_why, why);
2273       if (d)
2274         {
2275           /* at least 2 literals, needs watches */
2276           watch2onhighest(solv, r);
2277           addwatches_rule(solv, r);
2278         }
2279       else
2280         {
2281           /* learnt rule is an assertion */
2282           queue_push(&solv->ruleassertions, r - solv->rules);
2283         }
2284       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
2285       queue_push(&solv->decisionq, p);
2286       queue_push(&solv->decisionq_why, r - solv->rules);
2287       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
2288         {
2289           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
2290           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
2291           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
2292           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
2293         }
2294     }
2295   return level;
2296 }
2297
2298
2299 /*-------------------------------------------------------------------
2300  *
2301  * select and install
2302  *
2303  * install best package from the queue. We add an extra package, inst, if
2304  * provided. See comment in weak install section.
2305  *
2306  * returns the new solver level or 0 if unsolvable
2307  *
2308  */
2309
2310 static int
2311 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
2312 {
2313   Pool *pool = solv->pool;
2314   Id p;
2315   int i;
2316
2317   /* FIXME: do we really need that inst handling? */
2318   if (solv->distupgrade && inst && dq->count)
2319     {
2320       policy_filter_unwanted(solv, dq, 0, POLICY_MODE_CHOOSE);
2321       for (i = 0; i < dq->count; i++)
2322         if (solvable_identical(pool, pool->solvables + inst, pool->solvables + dq->elements[i]))
2323           dq->elements[i] = inst;
2324     }
2325   else
2326     {
2327       if (dq->count > 1 || inst)
2328         policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
2329     }
2330
2331   i = 0;
2332   if (dq->count > 1)
2333     {
2334       /* choose the supplemented one */
2335       for (i = 0; i < dq->count; i++)
2336         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2337           break;
2338       if (i == dq->count)
2339         {
2340           for (i = 1; i < dq->count; i++)
2341             queue_push(&solv->branches, dq->elements[i]);
2342           queue_push(&solv->branches, -level);
2343           i = 0;
2344         }
2345     }
2346   p = dq->elements[i];
2347
2348   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2349
2350   return setpropagatelearn(solv, level, p, disablerules);
2351 }
2352
2353
2354 /********************************************************************/
2355 /* Main solver interface */
2356
2357
2358 /*-------------------------------------------------------------------
2359  *
2360  * solver_create
2361  * create solver structure
2362  *
2363  * pool: all available solvables
2364  * installed: installed Solvables
2365  *
2366  *
2367  * Upon solving, rules are created to flag the Solvables
2368  * of the 'installed' Repo as installed.
2369  */
2370
2371 Solver *
2372 solver_create(Pool *pool)
2373 {
2374   Solver *solv;
2375   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2376   solv->pool = pool;
2377   solv->installed = pool->installed;
2378
2379   queue_init(&solv->ruletojob);
2380   queue_init(&solv->decisionq);
2381   queue_init(&solv->decisionq_why);
2382   queue_init(&solv->problems);
2383   queue_init(&solv->suggestions);
2384   queue_init(&solv->recommendations);
2385   queue_init(&solv->orphaned);
2386   queue_init(&solv->learnt_why);
2387   queue_init(&solv->learnt_pool);
2388   queue_init(&solv->branches);
2389   queue_init(&solv->covenantq);
2390   queue_init(&solv->weakruleq);
2391   queue_init(&solv->ruleassertions);
2392
2393   map_init(&solv->recommendsmap, pool->nsolvables);
2394   map_init(&solv->suggestsmap, pool->nsolvables);
2395   map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
2396   solv->recommends_index = 0;
2397
2398   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2399   solv->nrules = 1;
2400   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2401   memset(solv->rules, 0, sizeof(Rule));
2402
2403   return solv;
2404 }
2405
2406
2407 /*-------------------------------------------------------------------
2408  *
2409  * solver_free
2410  */
2411
2412 void
2413 solver_free(Solver *solv)
2414 {
2415   queue_free(&solv->ruletojob);
2416   queue_free(&solv->decisionq);
2417   queue_free(&solv->decisionq_why);
2418   queue_free(&solv->learnt_why);
2419   queue_free(&solv->learnt_pool);
2420   queue_free(&solv->problems);
2421   queue_free(&solv->suggestions);
2422   queue_free(&solv->recommendations);
2423   queue_free(&solv->orphaned);
2424   queue_free(&solv->branches);
2425   queue_free(&solv->covenantq);
2426   queue_free(&solv->weakruleq);
2427   queue_free(&solv->ruleassertions);
2428
2429   map_free(&solv->recommendsmap);
2430   map_free(&solv->suggestsmap);
2431   map_free(&solv->noupdate);
2432   map_free(&solv->weakrulemap);
2433   map_free(&solv->noobsoletes);
2434
2435   sat_free(solv->decisionmap);
2436   sat_free(solv->rules);
2437   sat_free(solv->watches);
2438   sat_free(solv->obsoletes);
2439   sat_free(solv->obsoletes_data);
2440   sat_free(solv->multiversionupdaters);
2441   sat_free(solv);
2442 }
2443
2444
2445 /*-------------------------------------------------------------------
2446  *
2447  * run_solver
2448  *
2449  * all rules have been set up, now actually run the solver
2450  *
2451  */
2452
2453 static void
2454 run_solver(Solver *solv, int disablerules, int doweak)
2455 {
2456   Queue dq;             /* local decisionqueue */
2457   Queue dqs;            /* local decisionqueue for supplements */
2458   int systemlevel;
2459   int level, olevel;
2460   Rule *r;
2461   int i, j, n;
2462   Solvable *s;
2463   Pool *pool = solv->pool;
2464   Id p, *dp;
2465
2466   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2467     {
2468       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2469       for (i = 1; i < solv->nrules; i++)
2470         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2471     }
2472
2473   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2474
2475   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2476     solver_printdecisions(solv);
2477
2478   /* start SAT algorithm */
2479   level = 1;
2480   systemlevel = level + 1;
2481   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2482
2483   queue_init(&dq);
2484   queue_init(&dqs);
2485
2486   /*
2487    * here's the main loop:
2488    * 1) propagate new decisions (only needed for level 1)
2489    * 2) try to keep installed packages
2490    * 3) fulfill all unresolved rules
2491    * 4) install recommended packages
2492    * 5) minimalize solution if we had choices
2493    * if we encounter a problem, we rewind to a safe level and restart
2494    * with step 1
2495    */
2496
2497   for (;;)
2498     {
2499       /*
2500        * propagate
2501        */
2502
2503       if (level == 1)
2504         {
2505           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2506           if ((r = propagate(solv, level)) != 0)
2507             {
2508               if (analyze_unsolvable(solv, r, disablerules))
2509                 continue;
2510               queue_free(&dq);
2511               queue_free(&dqs);
2512               return;
2513             }
2514         }
2515
2516      if (level < systemlevel)
2517         {
2518           POOL_DEBUG(SAT_DEBUG_STATS, "resolving job rules\n");
2519           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2520             {
2521               Id l;
2522               if (r->d < 0)             /* ignore disabled rules */
2523                 continue;
2524               queue_empty(&dq);
2525               FOR_RULELITERALS(l, dp, r)
2526                 {
2527                   if (l < 0)
2528                     {
2529                       if (solv->decisionmap[-l] <= 0)
2530                         break;
2531                     }
2532                   else
2533                     {
2534                       if (solv->decisionmap[l] > 0)
2535                         break;
2536                       if (solv->decisionmap[l] == 0)
2537                         queue_push(&dq, l);
2538                     }
2539                 }
2540               if (l || !dq.count)
2541                 continue;
2542               /* prune to installed if not updating */
2543               if (!solv->updatesystem && solv->installed && dq.count > 1)
2544                 {
2545                   int j, k;
2546                   for (j = k = 0; j < dq.count; j++)
2547                     {
2548                       Solvable *s = pool->solvables + dq.elements[j];
2549                       if (s->repo == solv->installed)
2550                         dq.elements[k++] = dq.elements[j];
2551                     }
2552                   if (k)
2553                     dq.count = k;
2554                 }
2555               olevel = level;
2556               level = selectandinstall(solv, level, &dq, 0, disablerules);
2557               if (level == 0)
2558                 {
2559                   queue_free(&dq);
2560                   queue_free(&dqs);
2561                   return;
2562                 }
2563               if (level <= olevel)
2564                 break;
2565             }
2566           systemlevel = level + 1;
2567           if (i < solv->jobrules_end)
2568             continue;
2569         }
2570
2571
2572       /*
2573        * installed packages
2574        */
2575
2576       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2577         {
2578           if (!solv->updatesystem)
2579             {
2580               /*
2581                * Normal run (non-updating)
2582                * Keep as many packages installed as possible
2583                */
2584               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2585
2586               for (i = solv->installed->start; i < solv->installed->end; i++)
2587                 {
2588                   s = pool->solvables + i;
2589
2590                     /* skip if not installed */
2591                   if (s->repo != solv->installed)
2592                     continue;
2593
2594                     /* skip if already decided */
2595                   if (solv->decisionmap[i] != 0)
2596                     continue;
2597
2598                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2599
2600                   olevel = level;
2601                   level = setpropagatelearn(solv, level, i, disablerules);
2602
2603                   if (level == 0)                /* unsolvable */
2604                     {
2605                       queue_free(&dq);
2606                       queue_free(&dqs);
2607                       return;
2608                     }
2609                   if (level <= olevel)
2610                     break;
2611                 }
2612               systemlevel = level + 1;
2613               if (i < solv->installed->end)
2614                 continue;
2615             }
2616           else if (solv->noobsoletes.size && solv->multiversionupdaters)
2617             {
2618               /* see if we can multi-version install the newest package */
2619               for (i = solv->installed->start; i < solv->installed->end; i++)
2620                 {
2621                   Id d;
2622                   s = pool->solvables + i;
2623                   if (s->repo != solv->installed)
2624                     continue;
2625                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2626                     continue;
2627                   d = solv->multiversionupdaters[i - solv->installed->start];
2628                   if (!d)
2629                     continue;
2630                   queue_empty(&dq);
2631                   while ((p = pool->whatprovidesdata[d++]) != 0)
2632                     if (solv->decisionmap[p] >= 0)
2633                       queue_push(&dq, p);
2634                   policy_filter_unwanted(solv, &dq, i, POLICY_MODE_CHOOSE);
2635                   p = dq.elements[0];
2636                   if (p != i && solv->decisionmap[p] == 0)
2637                     {
2638                       olevel = level;
2639                       POOL_DEBUG(SAT_DEBUG_POLICY, "installing (multi-version) %s\n", solvable2str(pool, pool->solvables + p));
2640                       level = setpropagatelearn(solv, level, p, disablerules);
2641                       if (level == 0)
2642                         {
2643                           queue_free(&dq);
2644                           queue_free(&dqs);
2645                           return;
2646                         }
2647                       if (level <= olevel)
2648                         break;
2649                     }
2650                   p = i;
2651                   /* now that the best version is installed, try to
2652                    * keep the original one */
2653                   if (solv->decisionmap[p])     /* already decided? */
2654                    continue;
2655                   r = solv->rules + solv->updaterules + (i - solv->installed->start);
2656                   if (!r->p)            /* update rule == feature rule? */
2657                     r = r - solv->updaterules + solv->featurerules;
2658                   if (r->p == p)        /* allowed to keep package? */
2659                     {
2660                       olevel = level;
2661                       POOL_DEBUG(SAT_DEBUG_POLICY, "keeping (multi-version) %s\n", solvable2str(pool, pool->solvables + p));
2662                       level = setpropagatelearn(solv, level, p, disablerules);
2663                       if (level == 0)
2664                         {
2665                           queue_free(&dq);
2666                           queue_free(&dqs);
2667                           return;
2668                         }
2669                       if (level <= olevel)
2670                         break;
2671                     }
2672                 }
2673               systemlevel = level + 1;
2674               if (i < solv->installed->end)
2675                 continue;
2676             }
2677
2678           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2679
2680           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2681             {
2682               Rule *rr;
2683               Id inst;
2684               s = pool->solvables + i;
2685
2686                 /* skip if not installed (can't update) */
2687               if (s->repo != solv->installed)
2688                 continue;
2689                 /* skip if already decided */
2690               if (solv->decisionmap[i] > 0)
2691                 continue;
2692
2693                 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2694               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2695                 continue;
2696
2697               queue_empty(&dq);
2698
2699               rr = r;
2700               if (rr->d < 0)    /* disabled -> look at feature rule ? */
2701                 rr -= solv->installed->end - solv->installed->start;
2702               if (!rr->p)       /* identical to update rule? */
2703                 rr = r;
2704               if (rr->p <= 0)
2705                 continue;       /* no such rule or disabled */
2706
2707               FOR_RULELITERALS(p, dp, rr)
2708                 {
2709                   if (solv->decisionmap[p] > 0)
2710                     break;
2711                   if (solv->decisionmap[p] == 0)
2712                     queue_push(&dq, p);
2713                 }
2714               if (p || !dq.count)       /* already fulfilled or empty */
2715                 continue;
2716               if (dq.elements[0] == i)
2717                 inst = queue_shift(&dq);
2718               else
2719                 inst = 0;
2720               olevel = level;
2721               /* FIXME: it is handled a bit different because we do not want
2722                * to have it pruned just because it is not recommened.
2723                * we should not prune installed packages instead.
2724                */
2725               level = selectandinstall(solv, level, &dq, inst, disablerules);
2726               if (level == 0)
2727                 {
2728                   queue_free(&dq);
2729                   queue_free(&dqs);
2730                   return;
2731                 }
2732               if (level <= olevel)
2733                 break;
2734             }
2735           systemlevel = level + 1;
2736           if (i < solv->installed->end)
2737             continue;
2738         }
2739
2740       if (level < systemlevel)
2741         systemlevel = level;
2742
2743       /*
2744        * decide
2745        */
2746
2747       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
2748       for (i = 1, n = 1; ; i++, n++)
2749         {
2750           if (n == solv->nrules)
2751             break;
2752           if (i == solv->nrules)
2753             i = 1;
2754           r = solv->rules + i;
2755           if (r->d < 0)         /* ignore disabled rules */
2756             continue;
2757           queue_empty(&dq);
2758           if (r->d == 0)
2759             {
2760               /* binary or unary rule */
2761               /* need two positive undecided literals */
2762               if (r->p < 0 || r->w2 <= 0)
2763                 continue;
2764               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2765                 continue;
2766               queue_push(&dq, r->p);
2767               queue_push(&dq, r->w2);
2768             }
2769           else
2770             {
2771               /* make sure that
2772                * all negative literals are installed
2773                * no positive literal is installed
2774                * i.e. the rule is not fulfilled and we
2775                * just need to decide on the positive literals
2776                */
2777               if (r->p < 0)
2778                 {
2779                   if (solv->decisionmap[-r->p] <= 0)
2780                     continue;
2781                 }
2782               else
2783                 {
2784                   if (solv->decisionmap[r->p] > 0)
2785                     continue;
2786                   if (solv->decisionmap[r->p] == 0)
2787                     queue_push(&dq, r->p);
2788                 }
2789               dp = pool->whatprovidesdata + r->d;
2790               while ((p = *dp++) != 0)
2791                 {
2792                   if (p < 0)
2793                     {
2794                       if (solv->decisionmap[-p] <= 0)
2795                         break;
2796                     }
2797                   else
2798                     {
2799                       if (solv->decisionmap[p] > 0)
2800                         break;
2801                       if (solv->decisionmap[p] == 0)
2802                         queue_push(&dq, p);
2803                     }
2804                 }
2805               if (p)
2806                 continue;
2807             }
2808           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2809             {
2810               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2811               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2812             }
2813           /* dq.count < 2 cannot happen as this means that
2814            * the rule is unit */
2815           assert(dq.count > 1);
2816
2817           olevel = level;
2818           level = selectandinstall(solv, level, &dq, 0, disablerules);
2819           if (level == 0)
2820             {
2821               queue_free(&dq);
2822               queue_free(&dqs);
2823               return;
2824             }
2825           if (level < systemlevel)
2826             break;
2827           n = 0;
2828         } /* for(), decide */
2829
2830       if (n != solv->nrules)    /* continue if level < systemlevel */
2831         continue;
2832
2833       if (doweak)
2834         {
2835           int qcount;
2836
2837           POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
2838           queue_empty(&dq);
2839           queue_empty(&dqs);
2840           for (i = 1; i < pool->nsolvables; i++)
2841             {
2842               if (solv->decisionmap[i] < 0)
2843                 continue;
2844               if (solv->decisionmap[i] > 0)
2845                 {
2846                   /* installed, check for recommends */
2847                   Id *recp, rec, pp, p;
2848                   s = pool->solvables + i;
2849                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
2850                     continue;
2851                   /* XXX need to special case AND ? */
2852                   if (s->recommends)
2853                     {
2854                       recp = s->repo->idarraydata + s->recommends;
2855                       while ((rec = *recp++) != 0)
2856                         {
2857                           qcount = dq.count;
2858                           FOR_PROVIDES(p, pp, rec)
2859                             {
2860                               if (solv->decisionmap[p] > 0)
2861                                 {
2862                                   dq.count = qcount;
2863                                   break;
2864                                 }
2865                               else if (solv->decisionmap[p] == 0)
2866                                 {
2867                                   queue_pushunique(&dq, p);
2868                                 }
2869                             }
2870                         }
2871                     }
2872                 }
2873               else
2874                 {
2875                   s = pool->solvables + i;
2876                   if (!s->supplements)
2877                     continue;
2878                   if (!pool_installable(pool, s))
2879                     continue;
2880                   if (!solver_is_supplementing(solv, s))
2881                     continue;
2882                   if (solv->ignorealreadyrecommended && solv->installed)
2883                     queue_pushunique(&dqs, i);  /* needs filter */
2884                   else
2885                     queue_pushunique(&dq, i);
2886                 }
2887             }
2888           if (solv->ignorealreadyrecommended && dqs.count)
2889             {
2890               /* turn off all new packages */
2891               for (i = 0; i < solv->decisionq.count; i++)
2892                 {
2893                   p = solv->decisionq.elements[i];
2894                   if (p < 0)
2895                     continue;
2896                   s = pool->solvables + p;
2897                   if (s->repo && s->repo != solv->installed)
2898                     solv->decisionmap[p] = -solv->decisionmap[p];
2899                 }
2900               /* filter out old supplements */
2901               for (i = 0; i < dqs.count; i++)
2902                 {
2903                   p = dqs.elements[i];
2904                   s = pool->solvables + p;
2905                   if (!s->supplements)
2906                     continue;
2907                   if (!solver_is_supplementing(solv, s))
2908                     queue_pushunique(&dq, p);
2909                 }
2910               /* undo turning off */
2911               for (i = 0; i < solv->decisionq.count; i++)
2912                 {
2913                   p = solv->decisionq.elements[i];
2914                   if (p < 0)
2915                     continue;
2916                   s = pool->solvables + p;
2917                   if (s->repo && s->repo != solv->installed)
2918                     solv->decisionmap[p] = -solv->decisionmap[p];
2919                 }
2920             }
2921           if (dq.count)
2922             {
2923               if (dq.count > 1)
2924                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2925               p = dq.elements[0];
2926               POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2927               queue_push(&solv->recommendations, p);
2928               level = setpropagatelearn(solv, level, p, 0);
2929               continue;
2930             }
2931         }
2932
2933      if (solv->distupgrade && solv->installed)
2934         {
2935           /* let's see if we can install some unsupported package */
2936           POOL_DEBUG(SAT_DEBUG_STATS, "deciding unsupported packages\n");
2937           for (i = 0; i < solv->orphaned.count; i++)
2938             {
2939               p = solv->orphaned.elements[i];
2940               if (!solv->decisionmap[p])
2941                 break;
2942             }
2943           if (i < solv->orphaned.count)
2944             {
2945               p = solv->orphaned.elements[i];
2946               if (solv->distupgrade_removeunsupported)
2947                 {
2948                   POOL_DEBUG(SAT_DEBUG_STATS, "removing unsupported %s\n", solvable2str(pool, pool->solvables + p));
2949                   level = setpropagatelearn(solv, level, -p, 0);
2950                 }
2951               else
2952                 {
2953                   POOL_DEBUG(SAT_DEBUG_STATS, "keeping unsupported %s\n", solvable2str(pool, pool->solvables + p));
2954                   level = setpropagatelearn(solv, level, p, 0);
2955                 }
2956               continue;
2957             }
2958         }
2959
2960      if (solv->solution_callback)
2961         {
2962           solv->solution_callback(solv, solv->solution_callback_data);
2963           if (solv->branches.count)
2964             {
2965               int i = solv->branches.count - 1;
2966               int l = -solv->branches.elements[i];
2967               for (; i > 0; i--)
2968                 if (solv->branches.elements[i - 1] < 0)
2969                   break;
2970               p = solv->branches.elements[i];
2971               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2972               queue_empty(&dq);
2973               for (j = i + 1; j < solv->branches.count; j++)
2974                 queue_push(&dq, solv->branches.elements[j]);
2975               solv->branches.count = i;
2976               level = l;
2977               revert(solv, level);
2978               if (dq.count > 1)
2979                 for (j = 0; j < dq.count; j++)
2980                   queue_push(&solv->branches, dq.elements[j]);
2981               olevel = level;
2982               level = setpropagatelearn(solv, level, p, disablerules);
2983               if (level == 0)
2984                 {
2985                   queue_free(&dq);
2986                   queue_free(&dqs);
2987                   return;
2988                 }
2989               continue;
2990             }
2991           /* all branches done, we're finally finished */
2992           break;
2993         }
2994
2995       /* minimization step */
2996      if (solv->branches.count)
2997         {
2998           int l = 0, lasti = -1, lastl = -1;
2999           p = 0;
3000           for (i = solv->branches.count - 1; i >= 0; i--)
3001             {
3002               p = solv->branches.elements[i];
3003               if (p < 0)
3004                 l = -p;
3005               else if (p > 0 && solv->decisionmap[p] > l + 1)
3006                 {
3007                   lasti = i;
3008                   lastl = l;
3009                 }
3010             }
3011           if (lasti >= 0)
3012             {
3013               /* kill old solvable so that we do not loop */
3014               p = solv->branches.elements[lasti];
3015               solv->branches.elements[lasti] = 0;
3016               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
3017
3018               level = lastl;
3019               revert(solv, level);
3020               olevel = level;
3021               level = setpropagatelearn(solv, level, p, disablerules);
3022               if (level == 0)
3023                 {
3024                   queue_free(&dq);
3025                   queue_free(&dqs);
3026                   return;
3027                 }
3028               continue;
3029             }
3030         }
3031       break;
3032     }
3033   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
3034
3035   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
3036   queue_free(&dq);
3037   queue_free(&dqs);
3038 }
3039
3040
3041 /*-------------------------------------------------------------------
3042  *
3043  * refine_suggestion
3044  *
3045  * at this point, all rules that led to conflicts are disabled.
3046  * we re-enable all rules of a problem set but rule "sug", then
3047  * continue to disable more rules until there as again a solution.
3048  */
3049
3050 /* FIXME: think about conflicting assertions */
3051
3052 static void
3053 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
3054 {
3055   Pool *pool = solv->pool;
3056   int i, j;
3057   Id v;
3058   Queue disabled;
3059   int disabledcnt;
3060
3061   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3062     {
3063       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
3064       for (i = 0; problem[i]; i++)
3065         {
3066           if (problem[i] == sug)
3067             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
3068           solver_printproblem(solv, problem[i]);
3069         }
3070     }
3071   queue_init(&disabled);
3072   queue_empty(refined);
3073   queue_push(refined, sug);
3074
3075   /* re-enable all problem rules with the exception of "sug"(gestion) */
3076   revert(solv, 1);
3077   reset_solver(solv);
3078
3079   for (i = 0; problem[i]; i++)
3080     if (problem[i] != sug)
3081       enableproblem(solv, problem[i]);
3082
3083   if (sug < 0)
3084     disableupdaterules(solv, job, -(sug + 1));
3085   else if (sug >= solv->updaterules && sug < solv->updaterules_end)
3086     {
3087       /* enable feature rule */
3088       Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
3089       if (r->p)
3090         enablerule(solv, r);
3091     }
3092
3093   enableweakrules(solv);
3094
3095   for (;;)
3096     {
3097       int njob, nfeature, nupdate;
3098       queue_empty(&solv->problems);
3099       revert(solv, 1);          /* XXX no longer needed? */
3100       reset_solver(solv);
3101
3102       if (!solv->problems.count)
3103         run_solver(solv, 0, 0);
3104
3105       if (!solv->problems.count)
3106         {
3107           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
3108           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3109             solver_printdecisions(solv);
3110           break;                /* great, no more problems */
3111         }
3112       disabledcnt = disabled.count;
3113       /* start with 1 to skip over proof index */
3114       njob = nfeature = nupdate = 0;
3115       for (i = 1; i < solv->problems.count - 1; i++)
3116         {
3117           /* ignore solutions in refined */
3118           v = solv->problems.elements[i];
3119           if (v == 0)
3120             break;      /* end of problem reached */
3121           for (j = 0; problem[j]; j++)
3122             if (problem[j] != sug && problem[j] == v)
3123               break;
3124           if (problem[j])
3125             continue;
3126           if (v >= solv->featurerules && v < solv->featurerules_end)
3127             nfeature++;
3128           else if (v > 0)
3129             nupdate++;
3130           else
3131             {
3132               if ((job->elements[-v -1] & SOLVER_ESSENTIAL) != 0)
3133                 continue;       /* not that one! */
3134               njob++;
3135             }
3136           queue_push(&disabled, v);
3137         }
3138       if (disabled.count == disabledcnt)
3139         {
3140           /* no solution found, this was an invalid suggestion! */
3141           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
3142           refined->count = 0;
3143           break;
3144         }
3145       if (!njob && nupdate && nfeature)
3146         {
3147           /* got only update rules, filter out feature rules */
3148           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
3149           for (i = j = disabledcnt; i < disabled.count; i++)
3150             {
3151               v = disabled.elements[i];
3152               if (v < solv->featurerules || v >= solv->featurerules_end)
3153                 disabled.elements[j++] = v;
3154             }
3155           disabled.count = j;
3156           nfeature = 0;
3157         }
3158       if (disabled.count == disabledcnt + 1)
3159         {
3160           /* just one suggestion, add it to refined list */
3161           v = disabled.elements[disabledcnt];
3162           if (!nfeature)
3163             queue_push(refined, v);     /* do not record feature rules */
3164           disableproblem(solv, v);
3165           if (v >= solv->updaterules && v < solv->updaterules_end)
3166             {
3167               Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3168               if (r->p)
3169                 enablerule(solv, r);    /* enable corresponding feature rule */
3170             }
3171           if (v < 0)
3172             disableupdaterules(solv, job, -(v + 1));
3173         }
3174       else
3175         {
3176           /* more than one solution, disable all */
3177           /* do not push anything on refine list, as we do not know which solution to choose */
3178           /* thus, the user will get another problem if he selects this solution, where he
3179            * can choose the right one */
3180           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3181             {
3182               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
3183               for (i = disabledcnt; i < disabled.count; i++)
3184                 solver_printproblem(solv, disabled.elements[i]);
3185             }
3186           for (i = disabledcnt; i < disabled.count; i++)
3187             {
3188               v = disabled.elements[i];
3189               disableproblem(solv, v);
3190               if (v >= solv->updaterules && v < solv->updaterules_end)
3191                 {
3192                   Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3193                   if (r->p)
3194                     enablerule(solv, r);
3195                 }
3196             }
3197         }
3198     }
3199   /* all done, get us back into the same state as before */
3200   /* enable refined rules again */
3201   for (i = 0; i < disabled.count; i++)
3202     enableproblem(solv, disabled.elements[i]);
3203   /* disable problem rules again */
3204
3205   /* FIXME! */
3206   for (i = 0; problem[i]; i++)
3207     enableproblem(solv, problem[i]);
3208   disableupdaterules(solv, job, -1);
3209
3210   /* disable problem rules again */
3211   for (i = 0; problem[i]; i++)
3212     disableproblem(solv, problem[i]);
3213   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
3214 }
3215
3216
3217 /*-------------------------------------------------------------------
3218  * sorting helper for problems
3219  *
3220  * bring update rules before job rules
3221  * make essential job rules last
3222  */
3223
3224 Queue *problems_sort_data;
3225
3226 static int
3227 problems_sortcmp(const void *ap, const void *bp)
3228 {
3229   Id a = *(Id *)ap, b = *(Id *)bp;
3230   if (a < 0 && b > 0)
3231     return 1;
3232   if (a > 0 && b < 0)
3233     return -1;
3234   if (a < 0 && b < 0)
3235     {
3236       Queue *job = problems_sort_data;
3237       int af = job->elements[-a - 1] & SOLVER_ESSENTIAL;
3238       int bf = job->elements[-a - 1] & SOLVER_ESSENTIAL;
3239       int x = bf - af;
3240       if (x)
3241         return x;
3242     }
3243   return a - b;
3244 }
3245
3246
3247 /*-------------------------------------------------------------------
3248  * sort problems
3249  */
3250
3251 static void
3252 problems_sort(Solver *solv, Queue *job)
3253 {
3254   int i, j;
3255   if (!solv->problems.count)
3256     return;
3257   for (i = j = 1; i < solv->problems.count; i++)
3258     {
3259       if (!solv->problems.elements[i])
3260         {
3261           if (i > j + 1)
3262             {
3263               problems_sort_data = job;
3264               qsort(solv->problems.elements + j, i - j, sizeof(Id), problems_sortcmp);
3265             }
3266           if (++i == solv->problems.count)
3267             break;
3268           j = i + 1;
3269         }
3270     }
3271 }
3272
3273
3274 /*-------------------------------------------------------------------
3275  * convert problems to solutions
3276  */
3277
3278 static void
3279 problems_to_solutions(Solver *solv, Queue *job)
3280 {
3281   Pool *pool = solv->pool;
3282   Queue problems;
3283   Queue solution;
3284   Queue solutions;
3285   Id *problem;
3286   Id why;
3287   int i, j, nsol, probsolved;
3288   unsigned int now, refnow;
3289
3290   if (!solv->problems.count)
3291     return;
3292   now = sat_timems(0);
3293   problems_sort(solv, job);
3294   queue_clone(&problems, &solv->problems);
3295   queue_init(&solution);
3296   queue_init(&solutions);
3297   /* copy over proof index */
3298   queue_push(&solutions, problems.elements[0]);
3299   problem = problems.elements + 1;
3300   probsolved = 0;
3301   refnow = sat_timems(0);
3302   for (i = 1; i < problems.count; i++)
3303     {
3304       Id v = problems.elements[i];
3305       if (v == 0)
3306         {
3307           /* mark end of this problem */
3308           queue_push(&solutions, 0);
3309           queue_push(&solutions, 0);
3310           POOL_DEBUG(SAT_DEBUG_STATS, "refining took %d ms\n", sat_timems(refnow));
3311           if (i + 1 == problems.count)
3312             break;
3313           /* copy over proof of next problem */
3314           queue_push(&solutions, problems.elements[i + 1]);
3315           i++;
3316           problem = problems.elements + i + 1;
3317           refnow = sat_timems(0);
3318           probsolved = 0;
3319           continue;
3320         }
3321       if (v < 0 && (job->elements[-v - 1] & SOLVER_ESSENTIAL))
3322         {
3323           /* essential job, skip if we already have a non-essential
3324              solution */
3325           if (probsolved > 0)
3326             continue;
3327           probsolved = -1;      /* show all solutions */
3328         }
3329       refine_suggestion(solv, job, problem, v, &solution);
3330       if (!solution.count)
3331         continue;       /* this solution didn't work out */
3332
3333       nsol = 0;
3334       for (j = 0; j < solution.count; j++)
3335         {
3336           why = solution.elements[j];
3337           /* must be either job descriptor or update rule */
3338           assert(why < 0 || (why >= solv->updaterules && why < solv->updaterules_end));
3339 #if 0
3340           solver_printproblem(solv, why);
3341 #endif
3342           if (why < 0)
3343             {
3344               /* job descriptor */
3345               queue_push(&solutions, 0);
3346               queue_push(&solutions, -why);
3347             }
3348           else
3349             {
3350               /* update rule, find replacement package */
3351               Id p, *dp, rp = 0;
3352               Rule *rr;
3353               p = solv->installed->start + (why - solv->updaterules);
3354               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
3355               if (!rr->p)
3356                 rr = solv->rules + why;
3357               if (solv->distupgrade && solv->rules[why].p != p && solv->decisionmap[p] > 0)
3358                 {
3359                   /* distupgrade case, allow to keep old package */
3360                   queue_push(&solutions, p);
3361                   queue_push(&solutions, p);
3362                   nsol++;
3363                   continue;
3364                 }
3365               if (solv->decisionmap[p] > 0)
3366                 continue;       /* false alarm, turned out we can keep the package */
3367               if (rr->w2)
3368                 {
3369                   int mvrp = 0;         /* multi-version replacement */
3370                   FOR_RULELITERALS(rp, dp, rr)
3371                     {
3372                       if (rp > 0 && solv->decisionmap[rp] > 0 && pool->solvables[rp].repo != solv->installed)
3373                         {
3374                           mvrp = rp;
3375                           if (!(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, rp)))
3376                             break;
3377                         }
3378                     }
3379                   if (!rp && mvrp)
3380                     {
3381                       /* found only multi-version replacements */
3382                       /* have to split solution into two parts */
3383                       queue_push(&solutions, p);
3384                       queue_push(&solutions, mvrp);
3385                       nsol++;
3386                     }
3387                 }
3388               queue_push(&solutions, p);
3389               queue_push(&solutions, rp);
3390             }
3391           nsol++;
3392         }
3393       /* mark end of this solution */
3394       if (nsol)
3395         {
3396           if (!probsolved)
3397             probsolved = 1;
3398           queue_push(&solutions, 0);
3399           queue_push(&solutions, 0);
3400         }
3401       else
3402         {
3403           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "Oops, everything was fine?\n");
3404         }
3405     }
3406   queue_free(&solution);
3407   queue_free(&problems);
3408   /* copy queue over to solutions */
3409   queue_free(&solv->problems);
3410   queue_clone(&solv->problems, &solutions);
3411
3412   /* bring solver back into problem state */
3413   revert(solv, 1);              /* XXX move to reset_solver? */
3414   reset_solver(solv);
3415
3416   assert(solv->problems.count == solutions.count);
3417   queue_free(&solutions);
3418   POOL_DEBUG(SAT_DEBUG_STATS, "problems_to_solutions took %d ms\n", sat_timems(now));
3419 }
3420
3421
3422 /*-------------------------------------------------------------------
3423  *
3424  * problem iterator
3425  *
3426  * advance to next problem
3427  */
3428
3429 Id
3430 solver_next_problem(Solver *solv, Id problem)
3431 {
3432   Id *pp;
3433   if (problem == 0)
3434     return solv->problems.count ? 1 : 0;
3435   pp = solv->problems.elements + problem;
3436   while (pp[0] || pp[1])
3437     {
3438       /* solution */
3439       pp += 2;
3440       while (pp[0] || pp[1])
3441         pp += 2;
3442       pp += 2;
3443     }
3444   pp += 2;
3445   problem = pp - solv->problems.elements;
3446   if (problem >= solv->problems.count)
3447     return 0;
3448   return problem + 1;
3449 }
3450
3451
3452 /*-------------------------------------------------------------------
3453  *
3454  * solution iterator
3455  */
3456
3457 Id
3458 solver_next_solution(Solver *solv, Id problem, Id solution)
3459 {
3460   Id *pp;
3461   if (solution == 0)
3462     {
3463       solution = problem;
3464       pp = solv->problems.elements + solution;
3465       return pp[0] || pp[1] ? solution : 0;
3466     }
3467   pp = solv->problems.elements + solution;
3468   while (pp[0] || pp[1])
3469     pp += 2;
3470   pp += 2;
3471   solution = pp - solv->problems.elements;
3472   return pp[0] || pp[1] ? solution : 0;
3473 }
3474
3475
3476 /*-------------------------------------------------------------------
3477  *
3478  * solution element iterator
3479  */
3480
3481 Id
3482 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
3483 {
3484   Id *pp;
3485   element = element ? element + 2 : solution;
3486   pp = solv->problems.elements + element;
3487   if (!(pp[0] || pp[1]))
3488     return 0;
3489   *p = pp[0];
3490   *rp = pp[1];
3491   return element;
3492 }
3493
3494
3495 /*-------------------------------------------------------------------
3496  *
3497  * Retrieve information about a problematic rule
3498  *
3499  * this is basically the reverse of addrpmrulesforsolvable
3500  */
3501
3502 SolverProbleminfo
3503 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3504 {
3505   Pool *pool = solv->pool;
3506   Repo *installed = solv->installed;
3507   Rule *r;
3508   Solvable *s;
3509   int dontfix = 0;
3510   Id p, d, w2, pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3511
3512   assert(rid > 0);
3513   if (rid >= solv->jobrules && rid < solv->jobrules_end)
3514     {
3515
3516       r = solv->rules + rid;
3517       p = solv->ruletojob.elements[rid - solv->jobrules];
3518       *depp = job->elements[p + 1];
3519       *sourcep = p;
3520       *targetp = job->elements[p];
3521       d = r->d < 0 ? -r->d - 1 : r->d;
3522       if (d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && (job->elements[p] & SOLVER_SELECTMASK) != SOLVER_SOLVABLE_ONE_OF)
3523         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3524       return SOLVER_PROBLEM_JOB_RULE;
3525     }
3526   if (rid >= solv->updaterules && rid < solv->updaterules_end)
3527     {
3528       *depp = 0;
3529       *sourcep = solv->installed->start + (rid - solv->updaterules);
3530       *targetp = 0;
3531       return SOLVER_PROBLEM_UPDATE_RULE;
3532     }
3533   assert(rid < solv->rpmrules_end);
3534   r = solv->rules + rid;
3535   assert(r->p < 0);
3536   d = r->d < 0 ? -r->d - 1 : r->d;
3537   if (d == 0 && r->w2 == 0)
3538     {
3539       /* a rpm rule assertion */
3540       s = pool->solvables - r->p;
3541       if (installed && !solv->fixsystem && s->repo == installed)
3542         dontfix = 1;
3543       assert(!dontfix); /* dontfix packages never have a neg assertion */
3544       *sourcep = -r->p;
3545       *targetp = 0;
3546       /* see why the package is not installable */
3547       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3548         {
3549           *depp = 0;
3550           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3551         }
3552       /* check requires */
3553       if (s->requires)
3554         {
3555           reqp = s->repo->idarraydata + s->requires;
3556           while ((req = *reqp++) != 0)
3557             {
3558               if (req == SOLVABLE_PREREQMARKER)
3559                 continue;
3560               dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3561               if (*dp == 0)
3562                 break;
3563             }
3564           if (req)
3565             {
3566               *depp = req;
3567               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3568             }
3569         }
3570       if (!solv->allowselfconflicts && s->conflicts)
3571         {
3572           conp = s->repo->idarraydata + s->conflicts;
3573           while ((con = *conp++) != 0)
3574             FOR_PROVIDES(p, pp, con)
3575               if (p == -r->p)
3576                 {
3577                   *depp = con;
3578                   return SOLVER_PROBLEM_SELF_CONFLICT;
3579                 }
3580         }
3581       /* should never happen */
3582       *depp = 0;
3583       return SOLVER_PROBLEM_RPM_RULE;
3584     }
3585   s = pool->solvables - r->p;
3586   if (installed && !solv->fixsystem && s->repo == installed)
3587     dontfix = 1;
3588   w2 = r->w2;
3589   if (d && pool->whatprovidesdata[d] < 0)
3590     {
3591       /* rule looks like -p|-c|x|x|x..., we only create this for patches with multiversion */
3592       /* reduce it to -p|-c case */
3593       w2 = pool->whatprovidesdata[d];
3594     }
3595   if (d == 0 && w2 < 0)
3596     {
3597       /* a package conflict */
3598       Solvable *s2 = pool->solvables - w2;
3599       int dontfix2 = 0;
3600
3601       if (installed && !solv->fixsystem && s2->repo == installed)
3602         dontfix2 = 1;
3603
3604       /* if both packages have the same name and at least one of them
3605        * is not installed, they conflict */
3606       if (s->name == s2->name && !(installed && s->repo == installed && s2->repo == installed))
3607         {
3608           /* also check noobsoletes map */
3609           if ((s->evr == s2->evr && s->arch == s2->arch) || !solv->noobsoletes.size
3610                 || ((!installed || s->repo != installed) && !MAPTST(&solv->noobsoletes, -r->p))
3611                 || ((!installed || s2->repo != installed) && !MAPTST(&solv->noobsoletes, -w2)))
3612             {
3613               *depp = 0;
3614               *sourcep = -r->p;
3615               *targetp = -w2;
3616               return SOLVER_PROBLEM_SAME_NAME;
3617             }
3618         }
3619
3620       /* check conflicts in both directions */
3621       if (s->conflicts)
3622         {
3623           conp = s->repo->idarraydata + s->conflicts;
3624           while ((con = *conp++) != 0)
3625             {
3626               FOR_PROVIDES(p, pp, con)
3627                 {
3628                   if (dontfix && pool->solvables[p].repo == installed)
3629                     continue;
3630                   if (p != -w2)
3631                     continue;
3632                   *depp = con;
3633                   *sourcep = -r->p;
3634                   *targetp = p;
3635                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3636                 }
3637             }
3638         }
3639       if (s2->conflicts)
3640         {
3641           conp = s2->repo->idarraydata + s2->conflicts;
3642           while ((con = *conp++) != 0)
3643             {
3644               FOR_PROVIDES(p, pp, con)
3645                 {
3646                   if (dontfix2 && pool->solvables[p].repo == installed)
3647                     continue;
3648                   if (p != -r->p)
3649                     continue;
3650                   *depp = con;
3651                   *sourcep = -w2;
3652                   *targetp = p;
3653                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3654                 }
3655             }
3656         }
3657       /* check obsoletes in both directions */
3658       if ((!installed || s->repo != installed) && s->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3659         {
3660           obsp = s->repo->idarraydata + s->obsoletes;
3661           while ((obs = *obsp++) != 0)
3662             {
3663               FOR_PROVIDES(p, pp, obs)
3664                 {
3665                   if (p != -w2)
3666                     continue;
3667                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3668                     continue;
3669                   *depp = obs;
3670                   *sourcep = -r->p;
3671                   *targetp = p;
3672                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3673                 }
3674             }
3675         }
3676       if ((!installed || s2->repo != installed) && s2->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3677         {
3678           obsp = s2->repo->idarraydata + s2->obsoletes;
3679           while ((obs = *obsp++) != 0)
3680             {
3681               FOR_PROVIDES(p, pp, obs)
3682                 {
3683                   if (p != -r->p)
3684                     continue;
3685                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3686                     continue;
3687                   *depp = obs;
3688                   *sourcep = -w2;
3689                   *targetp = p;
3690                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3691                 }
3692             }
3693         }
3694       if (solv->implicitobsoleteusesprovides && (!installed || s->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3695         {
3696           FOR_PROVIDES(p, pp, s->name)
3697             {
3698               if (p != -w2)
3699                 continue;
3700               *depp = s->name;
3701               *sourcep = -r->p;
3702               *targetp = p;
3703               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3704             }
3705         }
3706       if (solv->implicitobsoleteusesprovides && (!installed || s2->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3707         {
3708           FOR_PROVIDES(p, pp, s2->name)
3709             {
3710               if (p != -r->p)
3711                 continue;
3712               *depp = s2->name;
3713               *sourcep = -w2;
3714               *targetp = p;
3715               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3716             }
3717         }
3718       /* all cases checked, can't happen */
3719       *depp = 0;
3720       *sourcep = -r->p;
3721       *targetp = 0;
3722       return SOLVER_PROBLEM_RPM_RULE;
3723     }
3724   /* simple requires */
3725   if (s->requires)
3726     {
3727       reqp = s->repo->idarraydata + s->requires;
3728       while ((req = *reqp++) != 0)
3729         {
3730           if (req == SOLVABLE_PREREQMARKER)
3731             continue;
3732           dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3733           if (d == 0)
3734             {
3735               if (*dp == r->w2 && dp[1] == 0)
3736                 break;
3737             }
3738           else if (dp - pool->whatprovidesdata == d)
3739             break;
3740         }
3741       if (req)
3742         {
3743           *depp = req;
3744           *sourcep = -r->p;
3745           *targetp = 0;
3746           return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3747         }
3748     }
3749   /* all cases checked, can't happen */
3750   *depp = 0;
3751   *sourcep = -r->p;
3752   *targetp = 0;
3753   return SOLVER_PROBLEM_RPM_RULE;
3754 }
3755
3756
3757 /*-------------------------------------------------------------------
3758  *
3759  * find problem rule
3760  */
3761
3762 static void
3763 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3764 {
3765   Id rid, d;
3766   Id lreqr, lconr, lsysr, ljobr;
3767   Rule *r;
3768   int reqassert = 0;
3769
3770   lreqr = lconr = lsysr = ljobr = 0;
3771   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3772     {
3773       assert(rid > 0);
3774       if (rid >= solv->learntrules)
3775         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3776       else if (rid >= solv->jobrules && rid < solv->jobrules_end)
3777         {
3778           if (!*jobrp)
3779             *jobrp = rid;
3780         }
3781       else if (rid >= solv->updaterules && rid < solv->updaterules_end)
3782         {
3783           if (!*sysrp)
3784             *sysrp = rid;
3785         }
3786       else
3787         {
3788           assert(rid < solv->rpmrules_end);
3789           r = solv->rules + rid;
3790           d = r->d < 0 ? -r->d - 1 : r->d;
3791           if (!d && r->w2 < 0)
3792             {
3793               if (!*conrp)
3794                 *conrp = rid;
3795             }
3796           else
3797             {
3798               if (!d && r->w2 == 0 && !reqassert)
3799                 {
3800                   /* prefer assertions (XXX: bad idea?) */
3801                   *reqrp = rid;
3802                   reqassert = 1;
3803                 }
3804               if (!*reqrp)
3805                 *reqrp = rid;
3806               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3807                 {
3808                   /* prefer rules of installed packages */
3809                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3810                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3811                     *reqrp = rid;
3812                 }
3813             }
3814         }
3815     }
3816   if (!*reqrp && lreqr)
3817     *reqrp = lreqr;
3818   if (!*conrp && lconr)
3819     *conrp = lconr;
3820   if (!*jobrp && ljobr)
3821     *jobrp = ljobr;
3822   if (!*sysrp && lsysr)
3823     *sysrp = lsysr;
3824 }
3825
3826
3827 /*-------------------------------------------------------------------
3828  *
3829  * find problem rule
3830  *
3831  * search for a rule that describes the problem to the
3832  * user. A pretty hopeless task, actually. We currently
3833  * prefer simple requires.
3834  */
3835
3836 Id
3837 solver_findproblemrule(Solver *solv, Id problem)
3838 {
3839   Id reqr, conr, sysr, jobr;
3840   Id idx = solv->problems.elements[problem - 1];
3841   reqr = conr = sysr = jobr = 0;
3842   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3843   if (reqr)
3844     return reqr;
3845   if (conr)
3846     return conr;
3847   if (sysr)
3848     return sysr;
3849   if (jobr)
3850     return jobr;
3851   assert(0);
3852 }
3853
3854
3855 /*-------------------------------------------------------------------
3856  *
3857  * create reverse obsoletes map for installed solvables
3858  *
3859  * for each installed solvable find which packages with *different* names
3860  * obsolete the solvable.
3861  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3862  */
3863
3864 static void
3865 create_obsolete_index(Solver *solv)
3866 {
3867   Pool *pool = solv->pool;
3868   Solvable *s;
3869   Repo *installed = solv->installed;
3870   Id p, pp, obs, *obsp, *obsoletes, *obsoletes_data;
3871   int i, n;
3872
3873   if (!installed || !installed->nsolvables)
3874     return;
3875   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3876   for (i = 1; i < pool->nsolvables; i++)
3877     {
3878       s = pool->solvables + i;
3879       if (!s->obsoletes)
3880         continue;
3881       if (!pool_installable(pool, s))
3882         continue;
3883       obsp = s->repo->idarraydata + s->obsoletes;
3884       while ((obs = *obsp++) != 0)
3885         {
3886           FOR_PROVIDES(p, pp, obs)
3887             {
3888               if (pool->solvables[p].repo != installed)
3889                 continue;
3890               if (pool->solvables[p].name == s->name)
3891                 continue;
3892               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3893                 continue;
3894               obsoletes[p - installed->start]++;
3895             }
3896         }
3897     }
3898   n = 0;
3899   for (i = 0; i < installed->nsolvables; i++)
3900     if (obsoletes[i])
3901       {
3902         n += obsoletes[i] + 1;
3903         obsoletes[i] = n;
3904       }
3905   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3906   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3907   for (i = pool->nsolvables - 1; i > 0; i--)
3908     {
3909       s = pool->solvables + i;
3910       if (!s->obsoletes)
3911         continue;
3912       if (!pool_installable(pool, s))
3913         continue;
3914       obsp = s->repo->idarraydata + s->obsoletes;
3915       while ((obs = *obsp++) != 0)
3916         {
3917           FOR_PROVIDES(p, pp, obs)
3918             {
3919               if (pool->solvables[p].repo != installed)
3920                 continue;
3921               if (pool->solvables[p].name == s->name)
3922                 continue;
3923               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3924                 continue;
3925               p -= installed->start;
3926               if (obsoletes_data[obsoletes[p]] != i)
3927                 obsoletes_data[--obsoletes[p]] = i;
3928             }
3929         }
3930     }
3931 }
3932
3933
3934 /*-------------------------------------------------------------------
3935  *
3936  * remove disabled conflicts
3937  */
3938
3939 static void
3940 removedisabledconflicts(Solver *solv, Queue *removed)
3941 {
3942   Pool *pool = solv->pool;
3943   int i, n;
3944   Id p, why, *dp;
3945   Id new;
3946   Rule *r;
3947   Id *decisionmap = solv->decisionmap;
3948
3949   POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n");
3950   queue_empty(removed);
3951   for (i = 0; i < solv->decisionq.count; i++)
3952     {
3953       p = solv->decisionq.elements[i];
3954       if (p > 0)
3955         continue;
3956       /* a conflict. we never do conflicts on free decisions, so there
3957        * must have been an unit rule */
3958       why = solv->decisionq_why.elements[i];
3959       assert(why > 0);
3960       r = solv->rules + why;
3961       if (r->d < 0 && decisionmap[-p])
3962         {
3963           /* rule is now disabled, remove from decisionmap */
3964           POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3965           queue_push(removed, -p);
3966           queue_push(removed, decisionmap[-p]);
3967           decisionmap[-p] = 0;
3968         }
3969     }
3970   if (!removed->count)
3971     return;
3972   /* we removed some confliced packages. some of them might still
3973    * be in conflict, so search for unit rules and re-conflict */
3974   new = 0;
3975   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3976     {
3977       if (i == solv->nrules)
3978         {
3979           i = 1;
3980           r = solv->rules + i;
3981         }
3982       if (r->d < 0)
3983         continue;
3984       if (!r->w2)
3985         {
3986           if (r->p < 0 && !decisionmap[-r->p])
3987             new = r->p;
3988         }
3989       else if (!r->d)
3990         {
3991           /* binary rule */
3992           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3993             new = r->p;
3994           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3995             new = r->w2;
3996         }
3997       else
3998         {
3999           if (r->p < 0 && decisionmap[-r->p] == 0)
4000             new = r->p;
4001           if (new || DECISIONMAP_FALSE(r->p))
4002             {
4003               dp = pool->whatprovidesdata + r->d;
4004               while ((p = *dp++) != 0)
4005                 {
4006                   if (new && p == new)
4007                     continue;
4008                   if (p < 0 && decisionmap[-p] == 0)
4009                     {
4010                       if (new)
4011                         {
4012                           new = 0;
4013                           break;
4014                         }
4015                       new = p;
4016                     }
4017                   else if (!DECISIONMAP_FALSE(p))
4018                     {
4019                       new = 0;
4020                       break;
4021                     }
4022                 }
4023             }
4024         }
4025       if (new)
4026         {
4027           POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
4028           decisionmap[-new] = -1;
4029           new = 0;
4030           n = 0;        /* redo all rules */
4031         }
4032     }
4033 }
4034
4035
4036 /*-------------------------------------------------------------------
4037  *
4038  * weaken solvable dependencies
4039  */
4040
4041 static void
4042 weaken_solvable_deps(Solver *solv, Id p)
4043 {
4044   int i;
4045   Rule *r;
4046
4047   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
4048     {
4049       if (r->p != -p)
4050         continue;
4051       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
4052         continue;       /* conflict */
4053       queue_push(&solv->weakruleq, i);
4054     }
4055 }
4056
4057 /********************************************************************/
4058 /* main() */
4059
4060 /*
4061  *
4062  * solve job queue
4063  *
4064  */
4065
4066 void
4067 solver_solve(Solver *solv, Queue *job)
4068 {
4069   Pool *pool = solv->pool;
4070   Repo *installed = solv->installed;
4071   int i;
4072   int oldnrules;
4073   Map addedmap;                /* '1' == have rpm-rules for solvable */
4074   Map installcandidatemap;
4075   Id how, what, select, name, weak, p, pp, d;
4076   Queue q, redoq;
4077   Solvable *s;
4078   int goterase;
4079   Rule *r;
4080   int now, solve_start;
4081
4082   solve_start = sat_timems(0);
4083   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
4084   POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide);
4085   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
4086   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
4087   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, allowvirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, solv->allowvirtualconflicts, solv->allowselfconflicts);
4088   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d\n", solv->obsoleteusesprovides, solv->implicitobsoleteusesprovides);
4089   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
4090   /* create whatprovides if not already there */
4091   if (!pool->whatprovides)
4092     pool_createwhatprovides(pool);
4093
4094   /* create obsolete index if needed */
4095   create_obsolete_index(solv);
4096
4097   /*
4098    * create basic rule set of all involved packages
4099    * use addedmap bitmap to make sure we don't create rules twice
4100    *
4101    */
4102
4103   /* create noobsolete map if needed */
4104   for (i = 0; i < job->count; i += 2)
4105     {
4106       how = job->elements[i] & ~SOLVER_WEAK;
4107       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
4108         continue;
4109       what = job->elements[i + 1];
4110       select = how & SOLVER_SELECTMASK;
4111       if (!solv->noobsoletes.size)
4112         map_init(&solv->noobsoletes, pool->nsolvables);
4113       FOR_JOB_SELECT(p, pp, select, what)
4114         MAPSET(&solv->noobsoletes, p);
4115     }
4116
4117   map_init(&addedmap, pool->nsolvables);
4118   map_init(&installcandidatemap, pool->nsolvables);
4119   queue_init(&q);
4120
4121   /*
4122    * always install our system solvable
4123    */
4124   MAPSET(&addedmap, SYSTEMSOLVABLE);
4125   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
4126   queue_push(&solv->decisionq_why, 0);
4127   solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */
4128
4129   now = sat_timems(0);
4130   /*
4131    * create rules for all package that could be involved with the solving
4132    * so called: rpm rules
4133    *
4134    */
4135   if (installed)
4136     {
4137       oldnrules = solv->nrules;
4138       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
4139       FOR_REPO_SOLVABLES(installed, p, s)
4140         addrpmrulesforsolvable(solv, s, &addedmap);
4141       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
4142       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
4143       oldnrules = solv->nrules;
4144       FOR_REPO_SOLVABLES(installed, p, s)
4145         addrpmrulesforupdaters(solv, s, &addedmap, 1);
4146       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
4147     }
4148
4149   /*
4150    * create rules for all packages involved in the job
4151    * (to be installed or removed)
4152    */
4153
4154   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
4155   oldnrules = solv->nrules;
4156   for (i = 0; i < job->count; i += 2)
4157     {
4158       how = job->elements[i];
4159       what = job->elements[i + 1];
4160       select = how & SOLVER_SELECTMASK;
4161
4162       switch (how & SOLVER_JOBMASK)
4163         {
4164         case SOLVER_INSTALL:
4165           FOR_JOB_SELECT(p, pp, select, what)
4166             {
4167               MAPSET(&installcandidatemap, p);
4168               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
4169             }
4170           break;
4171         case SOLVER_UPDATE:
4172           /* FIXME: semantics? */
4173           FOR_JOB_SELECT(p, pp, select, what)
4174             addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
4175           break;
4176         }
4177     }
4178   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
4179
4180   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
4181
4182   oldnrules = solv->nrules;
4183
4184     /*
4185      * add rules for suggests, enhances
4186      */
4187   addrpmrulesforweak(solv, &addedmap);
4188   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
4189
4190   IF_POOLDEBUG (SAT_DEBUG_STATS)
4191     {
4192       int possible = 0, installable = 0;
4193       for (i = 1; i < pool->nsolvables; i++)
4194         {
4195           if (pool_installable(pool, pool->solvables + i))
4196             installable++;
4197           if (MAPTST(&addedmap, i))
4198             possible++;
4199         }
4200       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
4201     }
4202
4203   /*
4204    * first pass done, we now have all the rpm rules we need.
4205    * unify existing rules before going over all job rules and
4206    * policy rules.
4207    * at this point the system is always solvable,
4208    * as an empty system (remove all packages) is a valid solution
4209    */
4210
4211   unifyrules(solv);                               /* remove duplicate rpm rules */
4212
4213   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
4214
4215   solv->directdecisions = solv->decisionq.count;
4216   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
4217   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
4218   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
4219
4220   /*
4221    * create feature rules
4222    *
4223    * foreach installed:
4224    *   create assertion (keep installed, if no update available)
4225    *   or
4226    *   create update rule (A|update1(A)|update2(A)|...)
4227    *
4228    * those are used later on to keep a version of the installed packages in
4229    * best effort mode
4230    */
4231
4232   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
4233   solv->featurerules = solv->nrules;              /* mark start of feature rules */
4234   if (installed)
4235     {
4236         /* foreach possibly installed solvable */
4237       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4238         {
4239           if (s->repo != installed)
4240             {
4241               addrule(solv, 0, 0);      /* create dummy rule */
4242               continue;
4243             }
4244           addupdaterule(solv, s, 1);    /* allow s to be updated */
4245         }
4246         /*
4247          * assert one rule per installed solvable,
4248          * either an assertion (A)
4249          * or a possible update (A|update1(A)|update2(A)|...)
4250          */
4251       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
4252     }
4253   solv->featurerules_end = solv->nrules;
4254
4255     /*
4256      * Add update rules for installed solvables
4257      *
4258      * almost identical to feature rules
4259      * except that downgrades/archchanges/vendorchanges are not allowed
4260      */
4261
4262   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
4263   solv->updaterules = solv->nrules;
4264
4265   if (installed)
4266     { /* foreach installed solvables */
4267       /* we create all update rules, but disable some later on depending on the job */
4268       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4269         {
4270           Rule *sr;
4271
4272           if (s->repo != installed)
4273             {
4274               addrule(solv, 0, 0);      /* create dummy rule */
4275               continue;
4276             }
4277           addupdaterule(solv, s, 0);    /* allowall = 0: downgrades not allowed */
4278             /*
4279              * check for and remove duplicate
4280              */
4281           r = solv->rules + solv->nrules - 1;           /* r: update rule */
4282           sr = r - (installed->end - installed->start); /* sr: feature rule */
4283           /* it's orphaned if there is no feature rule or the feature rule
4284            * consists just of the installed package */
4285           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
4286             queue_push(&solv->orphaned, i);
4287           if (!r->p)
4288             {
4289               assert(solv->distupgrade && !sr->p);
4290               continue;
4291             }
4292           unifyrules_sortcmp_data = pool;
4293           if (!unifyrules_sortcmp(r, sr))
4294             {
4295               /* identical rule, kill unneeded rule */
4296               if (solv->allowuninstall)
4297                 {
4298                   /* keep feature rule, make it weak */
4299                   memset(r, 0, sizeof(*r));
4300                   queue_push(&solv->weakruleq, sr - solv->rules);
4301                 }
4302               else
4303                 {
4304                   /* keep update rule */
4305                   memset(sr, 0, sizeof(*sr));
4306                 }
4307             }
4308           else if (solv->allowuninstall)
4309             {
4310               /* make both feature and update rule weak */
4311               queue_push(&solv->weakruleq, r - solv->rules);
4312               queue_push(&solv->weakruleq, sr - solv->rules);
4313             }
4314           else
4315             disablerule(solv, sr);
4316         }
4317       /* consistency check: we added a rule for _every_ installed solvable */
4318       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
4319     }
4320   solv->updaterules_end = solv->nrules;
4321
4322
4323   /*
4324    * now add all job rules
4325    */
4326
4327   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
4328
4329   solv->jobrules = solv->nrules;
4330   for (i = 0; i < job->count; i += 2)
4331     {
4332       oldnrules = solv->nrules;
4333
4334       how = job->elements[i];
4335       what = job->elements[i + 1];
4336       weak = how & SOLVER_WEAK;
4337       select = how & SOLVER_SELECTMASK;
4338       switch (how & SOLVER_JOBMASK)
4339         {
4340         case SOLVER_INSTALL:
4341           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4342           if (select == SOLVER_SOLVABLE)
4343             {
4344               p = what;
4345               d = 0;
4346             }
4347           else
4348             {
4349               queue_empty(&q);
4350               FOR_JOB_SELECT(p, pp, select, what)
4351                 queue_push(&q, p);
4352               if (!q.count)
4353                 {
4354                   /* no candidate found, make this an impossible rule */
4355                   queue_push(&q, -SYSTEMSOLVABLE);
4356                 }
4357               p = queue_shift(&q);      /* get first candidate */
4358               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
4359             }
4360           addrule(solv, p, d);          /* add install rule */
4361           queue_push(&solv->ruletojob, i);
4362           if (weak)
4363             queue_push(&solv->weakruleq, solv->nrules - 1);
4364           break;
4365         case SOLVER_ERASE:
4366           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4367           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
4368             {
4369               /* special case for "erase a specific solvable": we also
4370                * erase all other solvables with that name, so that they
4371                * don't get picked up as replacement */
4372               name = pool->solvables[what].name;
4373               FOR_PROVIDES(p, pp, name)
4374                 {
4375                   if (p == what)
4376                     continue;
4377                   s = pool->solvables + p;
4378                   if (s->name != name)
4379                     continue;
4380                   /* keep other versions installed */
4381                   if (s->repo == solv->installed)
4382                     continue;
4383                   /* keep installcandidates of other jobs */
4384                   if (MAPTST(&installcandidatemap, p))
4385                     continue;
4386                   addrule(solv, -p, 0);                 /* remove by Id */
4387                   queue_push(&solv->ruletojob, i);
4388                   if (weak)
4389                     queue_push(&solv->weakruleq, solv->nrules - 1);
4390                 }
4391             }
4392           FOR_JOB_SELECT(p, pp, select, what)
4393             {
4394               addrule(solv, -p, 0);
4395               queue_push(&solv->ruletojob, i);
4396               if (weak)
4397                 queue_push(&solv->weakruleq, solv->nrules - 1);
4398             }
4399           break;
4400
4401         case SOLVER_UPDATE:
4402           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4403           if (select != SOLVER_SOLVABLE)
4404             break;
4405           s = pool->solvables + what;
4406           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
4407           addupdaterule(solv, s, 0);
4408           queue_push(&solv->ruletojob, i);
4409           if (weak)
4410             queue_push(&solv->weakruleq, solv->nrules - 1);
4411           break;
4412         case SOLVER_WEAKENDEPS:
4413           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4414           if (select != SOLVER_SOLVABLE)
4415             break;
4416           s = pool->solvables + what;
4417           weaken_solvable_deps(solv, what);
4418           break;
4419         case SOLVER_NOOBSOLETES:
4420           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4421           break;
4422         case SOLVER_LOCK:
4423           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4424           FOR_JOB_SELECT(p, pp, select, what)
4425             {
4426               s = pool->solvables + p;
4427               if (installed && s->repo == installed)
4428                 addrule(solv, p, 0);
4429               else
4430                 addrule(solv, -p, 0);
4431               queue_push(&solv->ruletojob, i);
4432               if (weak)
4433                 queue_push(&solv->weakruleq, solv->nrules - 1);
4434             }
4435           break;
4436         default:
4437           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
4438           break;
4439         }
4440
4441         /*
4442          * debug
4443          */
4444
4445       IF_POOLDEBUG (SAT_DEBUG_JOB)
4446         {
4447           int j;
4448           if (solv->nrules == oldnrules)
4449             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
4450           for (j = oldnrules; j < solv->nrules; j++)
4451             {
4452               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
4453               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
4454             }
4455         }
4456     }
4457   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
4458   solv->jobrules_end = solv->nrules;
4459
4460     /* all rules created
4461      * --------------------------------------------------------------
4462      * prepare for solving
4463      */
4464
4465   /* free unneeded memory */
4466   map_free(&addedmap);
4467   map_free(&installcandidatemap);
4468   queue_free(&q);
4469
4470   /* create weak map */
4471   map_init(&solv->weakrulemap, solv->nrules);
4472   for (i = 0; i < solv->weakruleq.count; i++)
4473     {
4474       p = solv->weakruleq.elements[i];
4475       MAPSET(&solv->weakrulemap, p);
4476     }
4477
4478   /* all new rules are learnt after this point */
4479   solv->learntrules = solv->nrules;
4480
4481   /* create assertion index. it is only used to speed up
4482    * makeruledecsions() a bit */
4483   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
4484     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
4485       queue_push(&solv->ruleassertions, i);
4486
4487   /* disable update rules that conflict with our job */
4488   disableupdaterules(solv, job, -1);
4489
4490   /* make decisions based on job/update assertions */
4491   makeruledecisions(solv);
4492
4493   /* create watches chains */
4494   makewatches(solv);
4495
4496   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4497
4498   /*
4499    * ********************************************
4500    * solve!
4501    * ********************************************
4502    */
4503
4504   now = sat_timems(0);
4505   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4506   POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
4507
4508   queue_init(&redoq);
4509   goterase = 0;
4510   /* disable all erase jobs (including weak "keep uninstalled" rules) */
4511   for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
4512     {
4513       if (r->d < 0)     /* disabled ? */
4514         continue;
4515       if (r->p > 0)     /* install job? */
4516         continue;
4517       disablerule(solv, r);
4518       goterase++;
4519     }
4520
4521   if (goterase)
4522     {
4523       enabledisablelearntrules(solv);
4524       removedisabledconflicts(solv, &redoq);
4525     }
4526
4527   /*
4528    * find recommended packages
4529    */
4530
4531   /* if redoq.count == 0 we already found all recommended in the
4532    * solver run */
4533   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
4534     {
4535       Id rec, *recp, p, pp;
4536
4537       /* create map of all recommened packages */
4538       solv->recommends_index = -1;
4539       MAPZERO(&solv->recommendsmap);
4540       for (i = 0; i < solv->decisionq.count; i++)
4541         {
4542           p = solv->decisionq.elements[i];
4543           if (p < 0)
4544             continue;
4545           s = pool->solvables + p;
4546           if (s->recommends)
4547             {
4548               recp = s->repo->idarraydata + s->recommends;
4549               while ((rec = *recp++) != 0)
4550                 {
4551                   FOR_PROVIDES(p, pp, rec)
4552                     if (solv->decisionmap[p] > 0)
4553                       break;
4554                   if (p)
4555                     {
4556                       if (!solv->dontshowinstalledrecommended)
4557                         {
4558                           FOR_PROVIDES(p, pp, rec)
4559                             if (solv->decisionmap[p] > 0)
4560                               MAPSET(&solv->recommendsmap, p);
4561                         }
4562                       continue; /* p != 0: already fulfilled */
4563                     }
4564                   FOR_PROVIDES(p, pp, rec)
4565                     MAPSET(&solv->recommendsmap, p);
4566                 }
4567             }
4568         }
4569       for (i = 1; i < pool->nsolvables; i++)
4570         {
4571           if (solv->decisionmap[i] < 0)
4572             continue;
4573           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4574             continue;
4575           s = pool->solvables + i;
4576           if (!MAPTST(&solv->recommendsmap, i))
4577             {
4578               if (!s->supplements)
4579                 continue;
4580               if (!pool_installable(pool, s))
4581                 continue;
4582               if (!solver_is_supplementing(solv, s))
4583                 continue;
4584             }
4585           if (solv->dontinstallrecommended)
4586             queue_push(&solv->recommendations, i);
4587           else
4588             queue_pushunique(&solv->recommendations, i);
4589         }
4590       /* we use MODE_SUGGEST here so that repo prio is ignored */
4591       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
4592     }
4593
4594   /*
4595    * find suggested packages
4596    */
4597
4598   if (1)
4599     {
4600       Id sug, *sugp, p, pp;
4601
4602       /* create map of all suggests that are still open */
4603       solv->recommends_index = -1;
4604       MAPZERO(&solv->suggestsmap);
4605       for (i = 0; i < solv->decisionq.count; i++)
4606         {
4607           p = solv->decisionq.elements[i];
4608           if (p < 0)
4609             continue;
4610           s = pool->solvables + p;
4611           if (s->suggests)
4612             {
4613               sugp = s->repo->idarraydata + s->suggests;
4614               while ((sug = *sugp++) != 0)
4615                 {
4616                   FOR_PROVIDES(p, pp, sug)
4617                     if (solv->decisionmap[p] > 0)
4618                       break;
4619                   if (p)
4620                     {
4621                       if (!solv->dontshowinstalledrecommended)
4622                         {
4623                           FOR_PROVIDES(p, pp, sug)
4624                             if (solv->decisionmap[p] > 0)
4625                               MAPSET(&solv->suggestsmap, p);
4626                         }
4627                       continue; /* already fulfilled */
4628                     }
4629                   FOR_PROVIDES(p, pp, sug)
4630                     MAPSET(&solv->suggestsmap, p);
4631                 }
4632             }
4633         }
4634       for (i = 1; i < pool->nsolvables; i++)
4635         {
4636           if (solv->decisionmap[i] < 0)
4637             continue;
4638           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4639             continue;
4640           s = pool->solvables + i;
4641           if (!MAPTST(&solv->suggestsmap, i))
4642             {
4643               if (!s->enhances)
4644                 continue;
4645               if (!pool_installable(pool, s))
4646                 continue;
4647               if (!solver_is_enhancing(solv, s))
4648                 continue;
4649             }
4650           queue_push(&solv->suggestions, i);
4651         }
4652       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
4653     }
4654
4655   if (redoq.count)
4656     {
4657       /* restore decisionmap */
4658       for (i = 0; i < redoq.count; i += 2)
4659         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4660     }
4661
4662     /*
4663      * if unsolvable, prepare solutions
4664      */
4665
4666   if (solv->problems.count)
4667     {
4668       int recocount = solv->recommendations.count;
4669       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
4670       queue_empty(&redoq);
4671       for (i = 0; i < solv->decisionq.count; i++)
4672         {
4673           Id p = solv->decisionq.elements[i];
4674           queue_push(&redoq, p);
4675           queue_push(&redoq, solv->decisionq_why.elements[i]);
4676           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4677         }
4678       problems_to_solutions(solv, job);
4679       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4680       queue_empty(&solv->decisionq);
4681       queue_empty(&solv->decisionq_why);
4682       for (i = 0; i < redoq.count; i += 3)
4683         {
4684           Id p = redoq.elements[i];
4685           queue_push(&solv->decisionq, p);
4686           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4687           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4688         }
4689       solv->recommendations.count = recocount;
4690     }
4691
4692   queue_free(&redoq);
4693   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
4694   POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
4695 }
4696
4697 /***********************************************************************/
4698 /* disk usage computations */
4699
4700 /*-------------------------------------------------------------------
4701  *
4702  * calculate DU changes
4703  */
4704
4705 void
4706 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4707 {
4708   Map installedmap;
4709
4710   solver_create_state_maps(solv, &installedmap, 0);
4711   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
4712   map_free(&installedmap);
4713 }
4714
4715
4716 /*-------------------------------------------------------------------
4717  *
4718  * calculate changes in install size
4719  */
4720
4721 int
4722 solver_calc_installsizechange(Solver *solv)
4723 {
4724   Map installedmap;
4725   int change;
4726
4727   solver_create_state_maps(solv, &installedmap, 0);
4728   change = pool_calc_installsizechange(solv->pool, &installedmap);
4729   map_free(&installedmap);
4730   return change;
4731 }
4732
4733 #define FIND_INVOLVED_DEBUG 0
4734 void
4735 solver_find_involved(Solver *solv, Queue *installedq, Solvable *ts, Queue *q)
4736 {
4737   Pool *pool = solv->pool;
4738   Map im;
4739   Map installedm;
4740   Solvable *s;
4741   Queue iq;
4742   Queue installedq_internal;
4743   Id tp, ip, p, pp, req, *reqp, sup, *supp;
4744   int i, count;
4745
4746   tp = ts - pool->solvables;
4747   queue_init(&iq);
4748   queue_init(&installedq_internal);
4749   map_init(&im, pool->nsolvables);
4750   map_init(&installedm, pool->nsolvables);
4751
4752   if (!installedq)
4753     {
4754       installedq = &installedq_internal;
4755       if (solv->installed)
4756         {
4757           for (ip = solv->installed->start; ip < solv->installed->end; ip++)
4758             {
4759               s = pool->solvables + ip;
4760               if (s->repo != solv->installed)
4761                 continue;
4762               queue_push(installedq, ip);
4763             }
4764         }
4765     }
4766   for (i = 0; i < installedq->count; i++)
4767     {
4768       ip = installedq->elements[i];
4769       MAPSET(&installedm, ip);
4770       MAPSET(&im, ip);
4771     }
4772
4773   queue_push(&iq, ts - pool->solvables);
4774   while (iq.count)
4775     {
4776       ip = queue_shift(&iq);
4777       if (!MAPTST(&im, ip))
4778         continue;
4779       if (!MAPTST(&installedm, ip))
4780         continue;
4781       MAPCLR(&im, ip);
4782       s = pool->solvables + ip;
4783 #if FIND_INVOLVED_DEBUG
4784       printf("hello %s\n", solvable2str(pool, s));
4785 #endif
4786       if (s->requires)
4787         {
4788           reqp = s->repo->idarraydata + s->requires;
4789           while ((req = *reqp++) != 0)
4790             {
4791               if (req == SOLVABLE_PREREQMARKER)
4792                 continue;
4793               /* count number of installed packages that match */
4794               count = 0;
4795               FOR_PROVIDES(p, pp, req)
4796                 if (MAPTST(&installedm, p))
4797                   count++;
4798               if (count > 1)
4799                 continue;
4800               FOR_PROVIDES(p, pp, req)
4801                 {
4802                   if (MAPTST(&im, p))
4803                     {
4804 #if FIND_INVOLVED_DEBUG
4805                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4806 #endif
4807                       queue_push(&iq, p);
4808                     }
4809                 }
4810             }
4811         }
4812       if (s->recommends)
4813         {
4814           reqp = s->repo->idarraydata + s->recommends;
4815           while ((req = *reqp++) != 0)
4816             {
4817               count = 0;
4818               FOR_PROVIDES(p, pp, req)
4819                 if (MAPTST(&installedm, p))
4820                   count++;
4821               if (count > 1)
4822                 continue;
4823               FOR_PROVIDES(p, pp, req)
4824                 {
4825                   if (MAPTST(&im, p))
4826                     {
4827 #if FIND_INVOLVED_DEBUG
4828                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4829 #endif
4830                       queue_push(&iq, p);
4831                     }
4832                 }
4833             }
4834         }
4835       if (!iq.count)
4836         {
4837           /* supplements pass */
4838           for (i = 0; i < installedq->count; i++)
4839             {
4840               ip = installedq->elements[i];
4841               s = pool->solvables + ip;
4842               if (!s->supplements)
4843                 continue;
4844               if (!MAPTST(&im, ip))
4845                 continue;
4846               supp = s->repo->idarraydata + s->supplements;
4847               while ((sup = *supp++) != 0)
4848                 if (!dep_possible(solv, sup, &im) && dep_possible(solv, sup, &installedm))
4849                   break;
4850               /* no longer supplemented, also erase */
4851               if (sup)
4852                 {
4853 #if FIND_INVOLVED_DEBUG
4854                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
4855 #endif
4856                   queue_push(&iq, ip);
4857                 }
4858             }
4859         }
4860     }
4861
4862   for (i = 0; i < installedq->count; i++)
4863     {
4864       ip = installedq->elements[i];
4865       if (MAPTST(&im, ip))
4866         queue_push(&iq, ip);
4867     }
4868
4869   while (iq.count)
4870     {
4871       ip = queue_shift(&iq);
4872       if (!MAPTST(&installedm, ip))
4873         continue;
4874       s = pool->solvables + ip;
4875 #if FIND_INVOLVED_DEBUG
4876       printf("bye %s\n", solvable2str(pool, s));
4877 #endif
4878       if (s->requires)
4879         {
4880           reqp = s->repo->idarraydata + s->requires;
4881           while ((req = *reqp++) != 0)
4882             {
4883               FOR_PROVIDES(p, pp, req)
4884                 {
4885                   if (!MAPTST(&im, p))
4886                     {
4887                       if (p == tp)
4888                         continue;
4889 #if FIND_INVOLVED_DEBUG
4890                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4891 #endif
4892                       MAPSET(&im, p);
4893                       queue_push(&iq, p);
4894                     }
4895                 }
4896             }
4897         }
4898       if (s->recommends)
4899         {
4900           reqp = s->repo->idarraydata + s->recommends;
4901           while ((req = *reqp++) != 0)
4902             {
4903               FOR_PROVIDES(p, pp, req)
4904                 {
4905                   if (!MAPTST(&im, p))
4906                     {
4907                       if (p == tp)
4908                         continue;
4909 #if FIND_INVOLVED_DEBUG
4910                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4911 #endif
4912                       MAPSET(&im, p);
4913                       queue_push(&iq, p);
4914                     }
4915                 }
4916             }
4917         }
4918       if (!iq.count)
4919         {
4920           /* supplements pass */
4921           for (i = 0; i < installedq->count; i++)
4922             {
4923               ip = installedq->elements[i];
4924               if (ip == tp)
4925                 continue;
4926               s = pool->solvables + ip;
4927               if (!s->supplements)
4928                 continue;
4929               if (MAPTST(&im, ip))
4930                 continue;
4931               supp = s->repo->idarraydata + s->supplements;
4932               while ((sup = *supp++) != 0)
4933                 if (dep_possible(solv, sup, &im))
4934                   break;
4935               if (sup)
4936                 {
4937 #if FIND_INVOLVED_DEBUG
4938                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
4939 #endif
4940                   MAPSET(&im, ip);
4941                   queue_push(&iq, ip);
4942                 }
4943             }
4944         }
4945     }
4946
4947   queue_free(&iq);
4948
4949   /* convert map into result */
4950   for (i = 0; i < installedq->count; i++)
4951     {
4952       ip = installedq->elements[i];
4953       if (MAPTST(&im, ip))
4954         continue;
4955       if (ip == ts - pool->solvables)
4956         continue;
4957       queue_push(q, ip);
4958     }
4959   map_free(&im);
4960   map_free(&installedm);
4961   queue_free(&installedq_internal);
4962 }
4963
4964 /* EOF */