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(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, int disablerules)
2312 {
2313   Pool *pool = solv->pool;
2314   Id p;
2315   int i;
2316
2317   if (dq->count > 1)
2318     policy_filter_unwanted(solv, dq, POLICY_MODE_CHOOSE);
2319   if (dq->count > 1)
2320     {
2321       /* XXX: didn't we already do that? */
2322       /* XXX: shouldn't we prefer installed packages? */
2323       /* XXX: move to policy.c? */
2324       /* choose the supplemented one */
2325       for (i = 0; i < dq->count; i++)
2326         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2327           {
2328             dq->elements[0] = dq->elements[i];
2329             dq->count = 1;
2330             break;
2331           }
2332     }
2333   if (dq->count > 1)
2334     {
2335       /* multiple candidates, open a branch */
2336       for (i = 1; i < dq->count; i++)
2337         queue_push(&solv->branches, dq->elements[i]);
2338       queue_push(&solv->branches, -level);
2339     }
2340   p = dq->elements[0];
2341
2342   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2343
2344   return setpropagatelearn(solv, level, p, disablerules);
2345 }
2346
2347
2348 /********************************************************************/
2349 /* Main solver interface */
2350
2351
2352 /*-------------------------------------------------------------------
2353  *
2354  * solver_create
2355  * create solver structure
2356  *
2357  * pool: all available solvables
2358  * installed: installed Solvables
2359  *
2360  *
2361  * Upon solving, rules are created to flag the Solvables
2362  * of the 'installed' Repo as installed.
2363  */
2364
2365 Solver *
2366 solver_create(Pool *pool)
2367 {
2368   Solver *solv;
2369   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2370   solv->pool = pool;
2371   solv->installed = pool->installed;
2372
2373   queue_init(&solv->ruletojob);
2374   queue_init(&solv->decisionq);
2375   queue_init(&solv->decisionq_why);
2376   queue_init(&solv->problems);
2377   queue_init(&solv->suggestions);
2378   queue_init(&solv->recommendations);
2379   queue_init(&solv->orphaned);
2380   queue_init(&solv->learnt_why);
2381   queue_init(&solv->learnt_pool);
2382   queue_init(&solv->branches);
2383   queue_init(&solv->covenantq);
2384   queue_init(&solv->weakruleq);
2385   queue_init(&solv->ruleassertions);
2386
2387   map_init(&solv->recommendsmap, pool->nsolvables);
2388   map_init(&solv->suggestsmap, pool->nsolvables);
2389   map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
2390   solv->recommends_index = 0;
2391
2392   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2393   solv->nrules = 1;
2394   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2395   memset(solv->rules, 0, sizeof(Rule));
2396
2397   return solv;
2398 }
2399
2400
2401 /*-------------------------------------------------------------------
2402  *
2403  * solver_free
2404  */
2405
2406 void
2407 solver_free(Solver *solv)
2408 {
2409   queue_free(&solv->ruletojob);
2410   queue_free(&solv->decisionq);
2411   queue_free(&solv->decisionq_why);
2412   queue_free(&solv->learnt_why);
2413   queue_free(&solv->learnt_pool);
2414   queue_free(&solv->problems);
2415   queue_free(&solv->suggestions);
2416   queue_free(&solv->recommendations);
2417   queue_free(&solv->orphaned);
2418   queue_free(&solv->branches);
2419   queue_free(&solv->covenantq);
2420   queue_free(&solv->weakruleq);
2421   queue_free(&solv->ruleassertions);
2422
2423   map_free(&solv->recommendsmap);
2424   map_free(&solv->suggestsmap);
2425   map_free(&solv->noupdate);
2426   map_free(&solv->weakrulemap);
2427   map_free(&solv->noobsoletes);
2428
2429   sat_free(solv->decisionmap);
2430   sat_free(solv->rules);
2431   sat_free(solv->watches);
2432   sat_free(solv->obsoletes);
2433   sat_free(solv->obsoletes_data);
2434   sat_free(solv->multiversionupdaters);
2435   sat_free(solv);
2436 }
2437
2438
2439 /*-------------------------------------------------------------------
2440  *
2441  * run_solver
2442  *
2443  * all rules have been set up, now actually run the solver
2444  *
2445  */
2446
2447 static void
2448 run_solver(Solver *solv, int disablerules, int doweak)
2449 {
2450   Queue dq;             /* local decisionqueue */
2451   Queue dqs;            /* local decisionqueue for supplements */
2452   int systemlevel;
2453   int level, olevel;
2454   Rule *r;
2455   int i, j, n;
2456   Solvable *s;
2457   Pool *pool = solv->pool;
2458   Id p, *dp;
2459   int minimizationsteps;
2460
2461   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2462     {
2463       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2464       for (i = 1; i < solv->nrules; i++)
2465         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2466     }
2467
2468   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2469
2470   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2471     solver_printdecisions(solv);
2472
2473   /* start SAT algorithm */
2474   level = 1;
2475   systemlevel = level + 1;
2476   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2477
2478   queue_init(&dq);
2479   queue_init(&dqs);
2480
2481   /*
2482    * here's the main loop:
2483    * 1) propagate new decisions (only needed for level 1)
2484    * 2) try to keep installed packages
2485    * 3) fulfill all unresolved rules
2486    * 4) install recommended packages
2487    * 5) minimalize solution if we had choices
2488    * if we encounter a problem, we rewind to a safe level and restart
2489    * with step 1
2490    */
2491
2492   minimizationsteps = 0;
2493   for (;;)
2494     {
2495       /*
2496        * propagate
2497        */
2498
2499       if (level == 1)
2500         {
2501           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2502           if ((r = propagate(solv, level)) != 0)
2503             {
2504               if (analyze_unsolvable(solv, r, disablerules))
2505                 continue;
2506               queue_free(&dq);
2507               queue_free(&dqs);
2508               return;
2509             }
2510         }
2511
2512      if (level < systemlevel)
2513         {
2514           POOL_DEBUG(SAT_DEBUG_STATS, "resolving job rules\n");
2515           for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
2516             {
2517               Id l;
2518               if (r->d < 0)             /* ignore disabled rules */
2519                 continue;
2520               queue_empty(&dq);
2521               FOR_RULELITERALS(l, dp, r)
2522                 {
2523                   if (l < 0)
2524                     {
2525                       if (solv->decisionmap[-l] <= 0)
2526                         break;
2527                     }
2528                   else
2529                     {
2530                       if (solv->decisionmap[l] > 0)
2531                         break;
2532                       if (solv->decisionmap[l] == 0)
2533                         queue_push(&dq, l);
2534                     }
2535                 }
2536               if (l || !dq.count)
2537                 continue;
2538               /* prune to installed if not updating */
2539               if (!solv->updatesystem && solv->installed && dq.count > 1)
2540                 {
2541                   int j, k;
2542                   for (j = k = 0; j < dq.count; j++)
2543                     {
2544                       Solvable *s = pool->solvables + dq.elements[j];
2545                       if (s->repo == solv->installed)
2546                         dq.elements[k++] = dq.elements[j];
2547                     }
2548                   if (k)
2549                     dq.count = k;
2550                 }
2551               olevel = level;
2552               level = selectandinstall(solv, level, &dq, disablerules);
2553               if (level == 0)
2554                 {
2555                   queue_free(&dq);
2556                   queue_free(&dqs);
2557                   return;
2558                 }
2559               if (level <= olevel)
2560                 break;
2561             }
2562           systemlevel = level + 1;
2563           if (i < solv->jobrules_end)
2564             continue;
2565         }
2566
2567
2568       /*
2569        * installed packages
2570        */
2571
2572       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2573         {
2574           if (!solv->updatesystem)
2575             {
2576               /*
2577                * Normal run (non-updating)
2578                * Keep as many packages installed as possible
2579                */
2580               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2581
2582               for (i = solv->installed->start; i < solv->installed->end; i++)
2583                 {
2584                   s = pool->solvables + i;
2585
2586                     /* skip if not installed */
2587                   if (s->repo != solv->installed)
2588                     continue;
2589
2590                     /* skip if already decided */
2591                   if (solv->decisionmap[i] != 0)
2592                     continue;
2593
2594                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2595
2596                   olevel = level;
2597                   level = setpropagatelearn(solv, level, i, disablerules);
2598
2599                   if (level == 0)                /* unsolvable */
2600                     {
2601                       queue_free(&dq);
2602                       queue_free(&dqs);
2603                       return;
2604                     }
2605                   if (level <= olevel)
2606                     break;
2607                 }
2608               systemlevel = level + 1;
2609               if (i < solv->installed->end)
2610                 continue;
2611             }
2612           else if (solv->noobsoletes.size && solv->multiversionupdaters)
2613             {
2614               /* see if we can multi-version install the newest package */
2615               for (i = solv->installed->start; i < solv->installed->end; i++)
2616                 {
2617                   Id d;
2618                   s = pool->solvables + i;
2619                   if (s->repo != solv->installed)
2620                     continue;
2621                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2622                     continue;
2623                   d = solv->multiversionupdaters[i - solv->installed->start];
2624                   if (!d)
2625                     continue;
2626                   queue_empty(&dq);
2627                   queue_push(&dq, i);
2628                   while ((p = pool->whatprovidesdata[d++]) != 0)
2629                     if (solv->decisionmap[p] >= 0)
2630                       queue_push(&dq, p);
2631                   policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE);
2632                   p = dq.elements[0];
2633                   if (p != i && solv->decisionmap[p] == 0)
2634                     {
2635                       olevel = level;
2636                       POOL_DEBUG(SAT_DEBUG_POLICY, "installing (multi-version) %s\n", solvable2str(pool, pool->solvables + p));
2637                       level = setpropagatelearn(solv, level, p, disablerules);
2638                       if (level == 0)
2639                         {
2640                           queue_free(&dq);
2641                           queue_free(&dqs);
2642                           return;
2643                         }
2644                       if (level <= olevel)
2645                         break;
2646                     }
2647                   p = i;
2648                   /* now that the best version is installed, try to
2649                    * keep the original one */
2650                   if (solv->decisionmap[p])     /* already decided? */
2651                    continue;
2652                   r = solv->rules + solv->updaterules + (i - solv->installed->start);
2653                   if (!r->p)            /* update rule == feature rule? */
2654                     r = r - solv->updaterules + solv->featurerules;
2655                   if (r->p == p)        /* allowed to keep package? */
2656                     {
2657                       olevel = level;
2658                       POOL_DEBUG(SAT_DEBUG_POLICY, "keeping (multi-version) %s\n", solvable2str(pool, pool->solvables + p));
2659                       level = setpropagatelearn(solv, level, p, disablerules);
2660                       if (level == 0)
2661                         {
2662                           queue_free(&dq);
2663                           queue_free(&dqs);
2664                           return;
2665                         }
2666                       if (level <= olevel)
2667                         break;
2668                     }
2669                 }
2670               systemlevel = level + 1;
2671               if (i < solv->installed->end)
2672                 continue;
2673             }
2674
2675           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2676
2677           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2678             {
2679               Rule *rr;
2680               s = pool->solvables + i;
2681
2682                 /* skip if not installed (can't update) */
2683               if (s->repo != solv->installed)
2684                 continue;
2685                 /* skip if already decided */
2686               if (solv->decisionmap[i] > 0)
2687                 continue;
2688
2689                 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2690               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2691                 continue;
2692
2693               queue_empty(&dq);
2694
2695               rr = r;
2696               if (rr->d < 0)    /* disabled -> look at feature rule ? */
2697                 rr -= solv->installed->end - solv->installed->start;
2698               if (!rr->p)       /* identical to update rule? */
2699                 rr = r;
2700               if (rr->p <= 0)
2701                 continue;       /* no such rule or disabled */
2702
2703               FOR_RULELITERALS(p, dp, rr)
2704                 {
2705                   if (solv->decisionmap[p] > 0)
2706                     break;
2707                   if (solv->decisionmap[p] == 0)
2708                     queue_push(&dq, p);
2709                 }
2710               if (p || !dq.count)       /* already fulfilled or empty */
2711                 continue;
2712               olevel = level;
2713               level = selectandinstall(solv, level, &dq, disablerules);
2714               if (level == 0)
2715                 {
2716                   queue_free(&dq);
2717                   queue_free(&dqs);
2718                   return;
2719                 }
2720               if (level <= olevel)
2721                 break;
2722             }
2723           systemlevel = level + 1;
2724           if (i < solv->installed->end)
2725             continue;
2726         }
2727
2728       if (level < systemlevel)
2729         systemlevel = level;
2730
2731       /*
2732        * decide
2733        */
2734
2735       POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
2736       for (i = 1, n = 1; ; i++, n++)
2737         {
2738           if (n == solv->nrules)
2739             break;
2740           if (i == solv->nrules)
2741             i = 1;
2742           r = solv->rules + i;
2743           if (r->d < 0)         /* ignore disabled rules */
2744             continue;
2745           queue_empty(&dq);
2746           if (r->d == 0)
2747             {
2748               /* binary or unary rule */
2749               /* need two positive undecided literals */
2750               if (r->p < 0 || r->w2 <= 0)
2751                 continue;
2752               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2753                 continue;
2754               queue_push(&dq, r->p);
2755               queue_push(&dq, r->w2);
2756             }
2757           else
2758             {
2759               /* make sure that
2760                * all negative literals are installed
2761                * no positive literal is installed
2762                * i.e. the rule is not fulfilled and we
2763                * just need to decide on the positive literals
2764                */
2765               if (r->p < 0)
2766                 {
2767                   if (solv->decisionmap[-r->p] <= 0)
2768                     continue;
2769                 }
2770               else
2771                 {
2772                   if (solv->decisionmap[r->p] > 0)
2773                     continue;
2774                   if (solv->decisionmap[r->p] == 0)
2775                     queue_push(&dq, r->p);
2776                 }
2777               dp = pool->whatprovidesdata + r->d;
2778               while ((p = *dp++) != 0)
2779                 {
2780                   if (p < 0)
2781                     {
2782                       if (solv->decisionmap[-p] <= 0)
2783                         break;
2784                     }
2785                   else
2786                     {
2787                       if (solv->decisionmap[p] > 0)
2788                         break;
2789                       if (solv->decisionmap[p] == 0)
2790                         queue_push(&dq, p);
2791                     }
2792                 }
2793               if (p)
2794                 continue;
2795             }
2796           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2797             {
2798               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2799               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2800             }
2801           /* dq.count < 2 cannot happen as this means that
2802            * the rule is unit */
2803           assert(dq.count > 1);
2804
2805           olevel = level;
2806           level = selectandinstall(solv, level, &dq, disablerules);
2807           if (level == 0)
2808             {
2809               queue_free(&dq);
2810               queue_free(&dqs);
2811               return;
2812             }
2813           if (level < systemlevel)
2814             break;
2815           n = 0;
2816         } /* for(), decide */
2817
2818       if (n != solv->nrules)    /* continue if level < systemlevel */
2819         continue;
2820
2821       if (doweak)
2822         {
2823           int qcount;
2824
2825           POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
2826           queue_empty(&dq);     /* recommended packages */
2827           queue_empty(&dqs);    /* supplemented packages */
2828           for (i = 1; i < pool->nsolvables; i++)
2829             {
2830               if (solv->decisionmap[i] < 0)
2831                 continue;
2832               if (solv->decisionmap[i] > 0)
2833                 {
2834                   /* installed, check for recommends */
2835                   Id *recp, rec, pp, p;
2836                   s = pool->solvables + i;
2837                   if (solv->ignorealreadyrecommended && s->repo == solv->installed)
2838                     continue;
2839                   /* XXX need to special case AND ? */
2840                   if (s->recommends)
2841                     {
2842                       recp = s->repo->idarraydata + s->recommends;
2843                       while ((rec = *recp++) != 0)
2844                         {
2845                           qcount = dq.count;
2846                           FOR_PROVIDES(p, pp, rec)
2847                             {
2848                               if (solv->decisionmap[p] > 0)
2849                                 {
2850                                   dq.count = qcount;
2851                                   break;
2852                                 }
2853                               else if (solv->decisionmap[p] == 0)
2854                                 {
2855                                   queue_pushunique(&dq, p);
2856                                 }
2857                             }
2858                         }
2859                     }
2860                 }
2861               else
2862                 {
2863                   s = pool->solvables + i;
2864                   if (!s->supplements)
2865                     continue;
2866                   if (!pool_installable(pool, s))
2867                     continue;
2868                   if (!solver_is_supplementing(solv, s))
2869                     continue;
2870                   queue_push(&dqs, i);
2871                 }
2872             }
2873
2874           /* filter out all already supplemented packages if requested */
2875           if (solv->ignorealreadyrecommended && dqs.count)
2876             {
2877               /* turn off all new packages */
2878               for (i = 0; i < solv->decisionq.count; i++)
2879                 {
2880                   p = solv->decisionq.elements[i];
2881                   if (p < 0)
2882                     continue;
2883                   s = pool->solvables + p;
2884                   if (s->repo && s->repo != solv->installed)
2885                     solv->decisionmap[p] = -solv->decisionmap[p];
2886                 }
2887               /* filter out old supplements */
2888               for (i = j = 0; i < dqs.count; i++)
2889                 {
2890                   p = dqs.elements[i];
2891                   s = pool->solvables + p;
2892                   if (!s->supplements)
2893                     continue;
2894                   if (!solver_is_supplementing(solv, s))
2895                     dqs.elements[j++] = p;
2896                 }
2897               dqs.count = j;
2898               /* undo turning off */
2899               for (i = 0; i < solv->decisionq.count; i++)
2900                 {
2901                   p = solv->decisionq.elements[i];
2902                   if (p < 0)
2903                     continue;
2904                   s = pool->solvables + p;
2905                   if (s->repo && s->repo != solv->installed)
2906                     solv->decisionmap[p] = -solv->decisionmap[p];
2907                 }
2908             }
2909
2910           /* make dq contain both recommended and supplemented pkgs */
2911           if (dqs.count)
2912             {
2913               for (i = 0; i < dqs.count; i++)
2914                 queue_pushunique(&dq, dqs.elements[i]);
2915             }
2916
2917 #if 1
2918           if (dq.count)
2919             {
2920               Map dqmap;
2921               int decisioncount = solv->decisionq.count;
2922
2923               if (dq.count == 1)
2924                 {
2925                   /* simple case, just one package. no need to choose  */
2926                   p = dq.elements[0];
2927                   if (dqs.count)
2928                     POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvable2str(pool, pool->solvables + p));
2929                   else
2930                     POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2931                   queue_push(&solv->recommendations, p);
2932                   level = setpropagatelearn(solv, level, p, 0);
2933                   continue;
2934                 }
2935
2936               /* filter and create a map of result */
2937               policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
2938               map_init(&dqmap, pool->nsolvables);
2939               for (i = 0; i < dq.count; i++)
2940                 MAPSET(&dqmap, dq.elements[i]);
2941
2942               /* install all supplemented packages */
2943               for (i = 0; i < dqs.count; i++)
2944                 {
2945                   p = dqs.elements[i];
2946                   if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
2947                     continue;
2948                   POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvable2str(pool, pool->solvables + p));
2949                   queue_push(&solv->recommendations, p);
2950                   olevel = level;
2951                   level = setpropagatelearn(solv, level, p, 0);
2952                   if (level <= olevel)
2953                     break;
2954                 }
2955               if (i < dqs.count || solv->decisionq.count < decisioncount)
2956                 {
2957                   map_free(&dqmap);
2958                   continue;
2959                 }
2960
2961               /* install all recommended packages */
2962               /* more work as we want to created branches if multiple
2963                * choices are valid */
2964               for (i = 0; i < decisioncount; i++)
2965                 {
2966                   Id rec, *recp, pp;
2967                   p = solv->decisionq.elements[i];
2968                   if (p < 0)
2969                     continue;
2970                   s = pool->solvables + p;
2971                   if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
2972                     continue;
2973                   if (!s->recommends)
2974                     continue;
2975                   recp = s->repo->idarraydata + s->recommends;
2976                   while ((rec = *recp++) != 0)
2977                     {
2978                       queue_empty(&dq);
2979                       FOR_PROVIDES(p, pp, rec)
2980                         {
2981                           if (solv->decisionmap[p] > 0)
2982                             {
2983                               dq.count = 0;
2984                               break;
2985                             }
2986                           else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
2987                             queue_pushunique(&dq, p);
2988                         }
2989                       if (!dq.count)
2990                         continue;
2991                       if (dq.count > 1)
2992                         {
2993                           /* multiple candidates, open a branch */
2994                           for (i = 1; i < dq.count; i++)
2995                             queue_push(&solv->branches, dq.elements[i]);
2996                           queue_push(&solv->branches, -level);
2997                         }
2998                       p = dq.elements[0];
2999                       POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
3000                       queue_push(&solv->recommendations, p);
3001                       olevel = level;
3002                       level = setpropagatelearn(solv, level, p, 0);
3003                       if (level <= olevel || solv->decisionq.count < decisioncount)
3004                         break;
3005                     }
3006                   if (rec)
3007                     break;      /* had a problem above, quit loop */
3008                 }
3009               map_free(&dqmap);
3010               continue;
3011             }
3012 #else
3013           if (dq.count)
3014             {
3015               if (dq.count > 1)
3016                 policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
3017               p = dq.elements[0];
3018               /* prefer recommended patterns (bnc#450226) */
3019               /* real fix is to minimize recommended packages as well */
3020               for (i = 0; i < dq.count; i++)
3021                 if (!strncmp(id2str(pool, pool->solvables[dq.elements[i]].name), "pattern:", 8))
3022                   {
3023                     p = dq.elements[i];
3024                     break;
3025                   }
3026               POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
3027               queue_push(&solv->recommendations, p);
3028               level = setpropagatelearn(solv, level, p, 0);
3029               continue;
3030             }
3031 #endif
3032         }
3033
3034      if (solv->distupgrade && solv->installed)
3035         {
3036           /* let's see if we can install some unsupported package */
3037           POOL_DEBUG(SAT_DEBUG_STATS, "deciding unsupported packages\n");
3038           for (i = 0; i < solv->orphaned.count; i++)
3039             {
3040               p = solv->orphaned.elements[i];
3041               if (!solv->decisionmap[p])
3042                 break;
3043             }
3044           if (i < solv->orphaned.count)
3045             {
3046               p = solv->orphaned.elements[i];
3047               if (solv->distupgrade_removeunsupported)
3048                 {
3049                   POOL_DEBUG(SAT_DEBUG_STATS, "removing unsupported %s\n", solvable2str(pool, pool->solvables + p));
3050                   level = setpropagatelearn(solv, level, -p, 0);
3051                 }
3052               else
3053                 {
3054                   POOL_DEBUG(SAT_DEBUG_STATS, "keeping unsupported %s\n", solvable2str(pool, pool->solvables + p));
3055                   level = setpropagatelearn(solv, level, p, 0);
3056                 }
3057               continue;
3058             }
3059         }
3060
3061      if (solv->solution_callback)
3062         {
3063           solv->solution_callback(solv, solv->solution_callback_data);
3064           if (solv->branches.count)
3065             {
3066               int i = solv->branches.count - 1;
3067               int l = -solv->branches.elements[i];
3068               for (; i > 0; i--)
3069                 if (solv->branches.elements[i - 1] < 0)
3070                   break;
3071               p = solv->branches.elements[i];
3072               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
3073               queue_empty(&dq);
3074               for (j = i + 1; j < solv->branches.count; j++)
3075                 queue_push(&dq, solv->branches.elements[j]);
3076               solv->branches.count = i;
3077               level = l;
3078               revert(solv, level);
3079               if (dq.count > 1)
3080                 for (j = 0; j < dq.count; j++)
3081                   queue_push(&solv->branches, dq.elements[j]);
3082               olevel = level;
3083               level = setpropagatelearn(solv, level, p, disablerules);
3084               if (level == 0)
3085                 {
3086                   queue_free(&dq);
3087                   queue_free(&dqs);
3088                   return;
3089                 }
3090               continue;
3091             }
3092           /* all branches done, we're finally finished */
3093           break;
3094         }
3095
3096       /* minimization step */
3097      if (solv->branches.count)
3098         {
3099           int l = 0, lasti = -1, lastl = -1;
3100           p = 0;
3101           for (i = solv->branches.count - 1; i >= 0; i--)
3102             {
3103               p = solv->branches.elements[i];
3104               if (p < 0)
3105                 l = -p;
3106               else if (p > 0 && solv->decisionmap[p] > l + 1)
3107                 {
3108                   lasti = i;
3109                   lastl = l;
3110                 }
3111             }
3112           if (lasti >= 0)
3113             {
3114               /* kill old solvable so that we do not loop */
3115               p = solv->branches.elements[lasti];
3116               solv->branches.elements[lasti] = 0;
3117               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, solvable2str(pool, pool->solvables + p));
3118               minimizationsteps++;
3119
3120               level = lastl;
3121               revert(solv, level);
3122               olevel = level;
3123               level = setpropagatelearn(solv, level, p, disablerules);
3124               if (level == 0)
3125                 {
3126                   queue_free(&dq);
3127                   queue_free(&dqs);
3128                   return;
3129                 }
3130               continue;
3131             }
3132         }
3133       break;
3134     }
3135   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
3136
3137   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
3138   queue_free(&dq);
3139   queue_free(&dqs);
3140 }
3141
3142
3143 /*-------------------------------------------------------------------
3144  *
3145  * refine_suggestion
3146  *
3147  * at this point, all rules that led to conflicts are disabled.
3148  * we re-enable all rules of a problem set but rule "sug", then
3149  * continue to disable more rules until there as again a solution.
3150  */
3151
3152 /* FIXME: think about conflicting assertions */
3153
3154 static void
3155 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
3156 {
3157   Pool *pool = solv->pool;
3158   int i, j;
3159   Id v;
3160   Queue disabled;
3161   int disabledcnt;
3162
3163   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3164     {
3165       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
3166       for (i = 0; problem[i]; i++)
3167         {
3168           if (problem[i] == sug)
3169             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
3170           solver_printproblem(solv, problem[i]);
3171         }
3172     }
3173   queue_init(&disabled);
3174   queue_empty(refined);
3175   queue_push(refined, sug);
3176
3177   /* re-enable all problem rules with the exception of "sug"(gestion) */
3178   revert(solv, 1);
3179   reset_solver(solv);
3180
3181   for (i = 0; problem[i]; i++)
3182     if (problem[i] != sug)
3183       enableproblem(solv, problem[i]);
3184
3185   if (sug < 0)
3186     disableupdaterules(solv, job, -(sug + 1));
3187   else if (sug >= solv->updaterules && sug < solv->updaterules_end)
3188     {
3189       /* enable feature rule */
3190       Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
3191       if (r->p)
3192         enablerule(solv, r);
3193     }
3194
3195   enableweakrules(solv);
3196
3197   for (;;)
3198     {
3199       int njob, nfeature, nupdate;
3200       queue_empty(&solv->problems);
3201       revert(solv, 1);          /* XXX no longer needed? */
3202       reset_solver(solv);
3203
3204       if (!solv->problems.count)
3205         run_solver(solv, 0, 0);
3206
3207       if (!solv->problems.count)
3208         {
3209           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
3210           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3211             solver_printdecisions(solv);
3212           break;                /* great, no more problems */
3213         }
3214       disabledcnt = disabled.count;
3215       /* start with 1 to skip over proof index */
3216       njob = nfeature = nupdate = 0;
3217       for (i = 1; i < solv->problems.count - 1; i++)
3218         {
3219           /* ignore solutions in refined */
3220           v = solv->problems.elements[i];
3221           if (v == 0)
3222             break;      /* end of problem reached */
3223           for (j = 0; problem[j]; j++)
3224             if (problem[j] != sug && problem[j] == v)
3225               break;
3226           if (problem[j])
3227             continue;
3228           if (v >= solv->featurerules && v < solv->featurerules_end)
3229             nfeature++;
3230           else if (v > 0)
3231             nupdate++;
3232           else
3233             {
3234               if ((job->elements[-v -1] & SOLVER_ESSENTIAL) != 0)
3235                 continue;       /* not that one! */
3236               njob++;
3237             }
3238           queue_push(&disabled, v);
3239         }
3240       if (disabled.count == disabledcnt)
3241         {
3242           /* no solution found, this was an invalid suggestion! */
3243           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
3244           refined->count = 0;
3245           break;
3246         }
3247       if (!njob && nupdate && nfeature)
3248         {
3249           /* got only update rules, filter out feature rules */
3250           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
3251           for (i = j = disabledcnt; i < disabled.count; i++)
3252             {
3253               v = disabled.elements[i];
3254               if (v < solv->featurerules || v >= solv->featurerules_end)
3255                 disabled.elements[j++] = v;
3256             }
3257           disabled.count = j;
3258           nfeature = 0;
3259         }
3260       if (disabled.count == disabledcnt + 1)
3261         {
3262           /* just one suggestion, add it to refined list */
3263           v = disabled.elements[disabledcnt];
3264           if (!nfeature)
3265             queue_push(refined, v);     /* do not record feature rules */
3266           disableproblem(solv, v);
3267           if (v >= solv->updaterules && v < solv->updaterules_end)
3268             {
3269               Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3270               if (r->p)
3271                 enablerule(solv, r);    /* enable corresponding feature rule */
3272             }
3273           if (v < 0)
3274             disableupdaterules(solv, job, -(v + 1));
3275         }
3276       else
3277         {
3278           /* more than one solution, disable all */
3279           /* do not push anything on refine list, as we do not know which solution to choose */
3280           /* thus, the user will get another problem if he selects this solution, where he
3281            * can choose the right one */
3282           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
3283             {
3284               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
3285               for (i = disabledcnt; i < disabled.count; i++)
3286                 solver_printproblem(solv, disabled.elements[i]);
3287             }
3288           for (i = disabledcnt; i < disabled.count; i++)
3289             {
3290               v = disabled.elements[i];
3291               disableproblem(solv, v);
3292               if (v >= solv->updaterules && v < solv->updaterules_end)
3293                 {
3294                   Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
3295                   if (r->p)
3296                     enablerule(solv, r);
3297                 }
3298             }
3299         }
3300     }
3301   /* all done, get us back into the same state as before */
3302   /* enable refined rules again */
3303   for (i = 0; i < disabled.count; i++)
3304     enableproblem(solv, disabled.elements[i]);
3305   /* disable problem rules again */
3306
3307   /* FIXME! */
3308   for (i = 0; problem[i]; i++)
3309     enableproblem(solv, problem[i]);
3310   disableupdaterules(solv, job, -1);
3311
3312   /* disable problem rules again */
3313   for (i = 0; problem[i]; i++)
3314     disableproblem(solv, problem[i]);
3315   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
3316 }
3317
3318
3319 /*-------------------------------------------------------------------
3320  * sorting helper for problems
3321  *
3322  * bring update rules before job rules
3323  * make essential job rules last
3324  */
3325
3326 Queue *problems_sort_data;
3327
3328 static int
3329 problems_sortcmp(const void *ap, const void *bp)
3330 {
3331   Id a = *(Id *)ap, b = *(Id *)bp;
3332   if (a < 0 && b > 0)
3333     return 1;
3334   if (a > 0 && b < 0)
3335     return -1;
3336   if (a < 0 && b < 0)
3337     {
3338       Queue *job = problems_sort_data;
3339       int af = job->elements[-a - 1] & SOLVER_ESSENTIAL;
3340       int bf = job->elements[-b - 1] & SOLVER_ESSENTIAL;
3341       int x = af - bf;
3342       if (x)
3343         return x;
3344     }
3345   return a - b;
3346 }
3347
3348
3349 /*-------------------------------------------------------------------
3350  * sort problems
3351  */
3352
3353 static void
3354 problems_sort(Solver *solv, Queue *job)
3355 {
3356   int i, j;
3357   if (!solv->problems.count)
3358     return;
3359   for (i = j = 1; i < solv->problems.count; i++)
3360     {
3361       if (!solv->problems.elements[i])
3362         {
3363           if (i > j + 1)
3364             {
3365               problems_sort_data = job;
3366               qsort(solv->problems.elements + j, i - j, sizeof(Id), problems_sortcmp);
3367             }
3368           if (++i == solv->problems.count)
3369             break;
3370           j = i + 1;
3371         }
3372     }
3373 }
3374
3375
3376 /*-------------------------------------------------------------------
3377  * convert problems to solutions
3378  */
3379
3380 static void
3381 problems_to_solutions(Solver *solv, Queue *job)
3382 {
3383   Pool *pool = solv->pool;
3384   Queue problems;
3385   Queue solution;
3386   Queue solutions;
3387   Id *problem;
3388   Id why;
3389   int i, j, nsol, probsolved;
3390   unsigned int now, refnow;
3391
3392   if (!solv->problems.count)
3393     return;
3394   now = sat_timems(0);
3395   problems_sort(solv, job);
3396   queue_clone(&problems, &solv->problems);
3397   queue_init(&solution);
3398   queue_init(&solutions);
3399   /* copy over proof index */
3400   queue_push(&solutions, problems.elements[0]);
3401   problem = problems.elements + 1;
3402   probsolved = 0;
3403   refnow = sat_timems(0);
3404   for (i = 1; i < problems.count; i++)
3405     {
3406       Id v = problems.elements[i];
3407       if (v == 0)
3408         {
3409           /* mark end of this problem */
3410           queue_push(&solutions, 0);
3411           queue_push(&solutions, 0);
3412           POOL_DEBUG(SAT_DEBUG_STATS, "refining took %d ms\n", sat_timems(refnow));
3413           if (i + 1 == problems.count)
3414             break;
3415           /* copy over proof of next problem */
3416           queue_push(&solutions, problems.elements[i + 1]);
3417           i++;
3418           problem = problems.elements + i + 1;
3419           refnow = sat_timems(0);
3420           probsolved = 0;
3421           continue;
3422         }
3423       if (v < 0 && (job->elements[-v - 1] & SOLVER_ESSENTIAL))
3424         {
3425           /* essential job, skip if we already have a non-essential
3426              solution */
3427           if (probsolved > 0)
3428             continue;
3429           probsolved = -1;      /* show all solutions */
3430         }
3431       refine_suggestion(solv, job, problem, v, &solution);
3432       if (!solution.count)
3433         continue;       /* this solution didn't work out */
3434
3435       nsol = 0;
3436       for (j = 0; j < solution.count; j++)
3437         {
3438           why = solution.elements[j];
3439           /* must be either job descriptor or update rule */
3440           assert(why < 0 || (why >= solv->updaterules && why < solv->updaterules_end));
3441 #if 0
3442           solver_printproblem(solv, why);
3443 #endif
3444           if (why < 0)
3445             {
3446               /* job descriptor */
3447               queue_push(&solutions, 0);
3448               queue_push(&solutions, -why);
3449             }
3450           else
3451             {
3452               /* update rule, find replacement package */
3453               Id p, *dp, rp = 0;
3454               Rule *rr;
3455               p = solv->installed->start + (why - solv->updaterules);
3456               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
3457               if (!rr->p)
3458                 rr = solv->rules + why;
3459               if (solv->distupgrade && solv->rules[why].p != p && solv->decisionmap[p] > 0)
3460                 {
3461                   /* distupgrade case, allow to keep old package */
3462                   queue_push(&solutions, p);
3463                   queue_push(&solutions, p);
3464                   nsol++;
3465                   continue;
3466                 }
3467               if (solv->decisionmap[p] > 0)
3468                 continue;       /* false alarm, turned out we can keep the package */
3469               if (rr->w2)
3470                 {
3471                   int mvrp = 0;         /* multi-version replacement */
3472                   FOR_RULELITERALS(rp, dp, rr)
3473                     {
3474                       if (rp > 0 && solv->decisionmap[rp] > 0 && pool->solvables[rp].repo != solv->installed)
3475                         {
3476                           mvrp = rp;
3477                           if (!(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, rp)))
3478                             break;
3479                         }
3480                     }
3481                   if (!rp && mvrp)
3482                     {
3483                       /* found only multi-version replacements */
3484                       /* have to split solution into two parts */
3485                       queue_push(&solutions, p);
3486                       queue_push(&solutions, mvrp);
3487                       nsol++;
3488                     }
3489                 }
3490               queue_push(&solutions, p);
3491               queue_push(&solutions, rp);
3492             }
3493           nsol++;
3494         }
3495       /* mark end of this solution */
3496       if (nsol)
3497         {
3498           if (!probsolved)
3499             probsolved = 1;
3500           queue_push(&solutions, 0);
3501           queue_push(&solutions, 0);
3502         }
3503       else
3504         {
3505           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "Oops, everything was fine?\n");
3506         }
3507     }
3508   queue_free(&solution);
3509   queue_free(&problems);
3510   /* copy queue over to solutions */
3511   queue_free(&solv->problems);
3512   queue_clone(&solv->problems, &solutions);
3513
3514   /* bring solver back into problem state */
3515   revert(solv, 1);              /* XXX move to reset_solver? */
3516   reset_solver(solv);
3517
3518   assert(solv->problems.count == solutions.count);
3519   queue_free(&solutions);
3520   POOL_DEBUG(SAT_DEBUG_STATS, "problems_to_solutions took %d ms\n", sat_timems(now));
3521 }
3522
3523
3524 /*-------------------------------------------------------------------
3525  *
3526  * problem iterator
3527  *
3528  * advance to next problem
3529  */
3530
3531 Id
3532 solver_next_problem(Solver *solv, Id problem)
3533 {
3534   Id *pp;
3535   if (problem == 0)
3536     return solv->problems.count ? 1 : 0;
3537   pp = solv->problems.elements + problem;
3538   while (pp[0] || pp[1])
3539     {
3540       /* solution */
3541       pp += 2;
3542       while (pp[0] || pp[1])
3543         pp += 2;
3544       pp += 2;
3545     }
3546   pp += 2;
3547   problem = pp - solv->problems.elements;
3548   if (problem >= solv->problems.count)
3549     return 0;
3550   return problem + 1;
3551 }
3552
3553
3554 /*-------------------------------------------------------------------
3555  *
3556  * solution iterator
3557  */
3558
3559 Id
3560 solver_next_solution(Solver *solv, Id problem, Id solution)
3561 {
3562   Id *pp;
3563   if (solution == 0)
3564     {
3565       solution = problem;
3566       pp = solv->problems.elements + solution;
3567       return pp[0] || pp[1] ? solution : 0;
3568     }
3569   pp = solv->problems.elements + solution;
3570   while (pp[0] || pp[1])
3571     pp += 2;
3572   pp += 2;
3573   solution = pp - solv->problems.elements;
3574   return pp[0] || pp[1] ? solution : 0;
3575 }
3576
3577
3578 /*-------------------------------------------------------------------
3579  *
3580  * solution element iterator
3581  */
3582
3583 Id
3584 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
3585 {
3586   Id *pp;
3587   element = element ? element + 2 : solution;
3588   pp = solv->problems.elements + element;
3589   if (!(pp[0] || pp[1]))
3590     return 0;
3591   *p = pp[0];
3592   *rp = pp[1];
3593   return element;
3594 }
3595
3596
3597 /*-------------------------------------------------------------------
3598  *
3599  * Retrieve information about a problematic rule
3600  *
3601  * this is basically the reverse of addrpmrulesforsolvable
3602  */
3603
3604 SolverProbleminfo
3605 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3606 {
3607   Pool *pool = solv->pool;
3608   Repo *installed = solv->installed;
3609   Rule *r;
3610   Solvable *s;
3611   int dontfix = 0;
3612   Id p, d, w2, pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3613
3614   assert(rid > 0);
3615   if (rid >= solv->jobrules && rid < solv->jobrules_end)
3616     {
3617
3618       r = solv->rules + rid;
3619       p = solv->ruletojob.elements[rid - solv->jobrules];
3620       *depp = job->elements[p + 1];
3621       *sourcep = p;
3622       *targetp = job->elements[p];
3623       d = r->d < 0 ? -r->d - 1 : r->d;
3624       if (d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && (job->elements[p] & SOLVER_SELECTMASK) != SOLVER_SOLVABLE_ONE_OF)
3625         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3626       return SOLVER_PROBLEM_JOB_RULE;
3627     }
3628   if (rid >= solv->updaterules && rid < solv->updaterules_end)
3629     {
3630       *depp = 0;
3631       *sourcep = solv->installed->start + (rid - solv->updaterules);
3632       *targetp = 0;
3633       return SOLVER_PROBLEM_UPDATE_RULE;
3634     }
3635   assert(rid < solv->rpmrules_end);
3636   r = solv->rules + rid;
3637   assert(r->p < 0);
3638   d = r->d < 0 ? -r->d - 1 : r->d;
3639   if (d == 0 && r->w2 == 0)
3640     {
3641       /* a rpm rule assertion */
3642       s = pool->solvables - r->p;
3643       if (installed && !solv->fixsystem && s->repo == installed)
3644         dontfix = 1;
3645       assert(!dontfix); /* dontfix packages never have a neg assertion */
3646       *sourcep = -r->p;
3647       *targetp = 0;
3648       /* see why the package is not installable */
3649       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3650         {
3651           *depp = 0;
3652           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3653         }
3654       /* check requires */
3655       if (s->requires)
3656         {
3657           reqp = s->repo->idarraydata + s->requires;
3658           while ((req = *reqp++) != 0)
3659             {
3660               if (req == SOLVABLE_PREREQMARKER)
3661                 continue;
3662               dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3663               if (*dp == 0)
3664                 break;
3665             }
3666           if (req)
3667             {
3668               *depp = req;
3669               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3670             }
3671         }
3672       if (!solv->allowselfconflicts && s->conflicts)
3673         {
3674           conp = s->repo->idarraydata + s->conflicts;
3675           while ((con = *conp++) != 0)
3676             FOR_PROVIDES(p, pp, con)
3677               if (p == -r->p)
3678                 {
3679                   *depp = con;
3680                   return SOLVER_PROBLEM_SELF_CONFLICT;
3681                 }
3682         }
3683       /* should never happen */
3684       *depp = 0;
3685       return SOLVER_PROBLEM_RPM_RULE;
3686     }
3687   s = pool->solvables - r->p;
3688   if (installed && !solv->fixsystem && s->repo == installed)
3689     dontfix = 1;
3690   w2 = r->w2;
3691   if (d && pool->whatprovidesdata[d] < 0)
3692     {
3693       /* rule looks like -p|-c|x|x|x..., we only create this for patches with multiversion */
3694       /* reduce it to -p|-c case */
3695       w2 = pool->whatprovidesdata[d];
3696     }
3697   if (d == 0 && w2 < 0)
3698     {
3699       /* a package conflict */
3700       Solvable *s2 = pool->solvables - w2;
3701       int dontfix2 = 0;
3702
3703       if (installed && !solv->fixsystem && s2->repo == installed)
3704         dontfix2 = 1;
3705
3706       /* if both packages have the same name and at least one of them
3707        * is not installed, they conflict */
3708       if (s->name == s2->name && !(installed && s->repo == installed && s2->repo == installed))
3709         {
3710           /* also check noobsoletes map */
3711           if ((s->evr == s2->evr && s->arch == s2->arch) || !solv->noobsoletes.size
3712                 || ((!installed || s->repo != installed) && !MAPTST(&solv->noobsoletes, -r->p))
3713                 || ((!installed || s2->repo != installed) && !MAPTST(&solv->noobsoletes, -w2)))
3714             {
3715               *depp = 0;
3716               *sourcep = -r->p;
3717               *targetp = -w2;
3718               return SOLVER_PROBLEM_SAME_NAME;
3719             }
3720         }
3721
3722       /* check conflicts in both directions */
3723       if (s->conflicts)
3724         {
3725           conp = s->repo->idarraydata + s->conflicts;
3726           while ((con = *conp++) != 0)
3727             {
3728               FOR_PROVIDES(p, pp, con)
3729                 {
3730                   if (dontfix && pool->solvables[p].repo == installed)
3731                     continue;
3732                   if (p != -w2)
3733                     continue;
3734                   *depp = con;
3735                   *sourcep = -r->p;
3736                   *targetp = p;
3737                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3738                 }
3739             }
3740         }
3741       if (s2->conflicts)
3742         {
3743           conp = s2->repo->idarraydata + s2->conflicts;
3744           while ((con = *conp++) != 0)
3745             {
3746               FOR_PROVIDES(p, pp, con)
3747                 {
3748                   if (dontfix2 && pool->solvables[p].repo == installed)
3749                     continue;
3750                   if (p != -r->p)
3751                     continue;
3752                   *depp = con;
3753                   *sourcep = -w2;
3754                   *targetp = p;
3755                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3756                 }
3757             }
3758         }
3759       /* check obsoletes in both directions */
3760       if ((!installed || s->repo != installed) && s->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3761         {
3762           obsp = s->repo->idarraydata + s->obsoletes;
3763           while ((obs = *obsp++) != 0)
3764             {
3765               FOR_PROVIDES(p, pp, obs)
3766                 {
3767                   if (p != -w2)
3768                     continue;
3769                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3770                     continue;
3771                   *depp = obs;
3772                   *sourcep = -r->p;
3773                   *targetp = p;
3774                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3775                 }
3776             }
3777         }
3778       if ((!installed || s2->repo != installed) && s2->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3779         {
3780           obsp = s2->repo->idarraydata + s2->obsoletes;
3781           while ((obs = *obsp++) != 0)
3782             {
3783               FOR_PROVIDES(p, pp, obs)
3784                 {
3785                   if (p != -r->p)
3786                     continue;
3787                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3788                     continue;
3789                   *depp = obs;
3790                   *sourcep = -w2;
3791                   *targetp = p;
3792                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3793                 }
3794             }
3795         }
3796       if (solv->implicitobsoleteusesprovides && (!installed || s->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3797         {
3798           FOR_PROVIDES(p, pp, s->name)
3799             {
3800               if (p != -w2)
3801                 continue;
3802               *depp = s->name;
3803               *sourcep = -r->p;
3804               *targetp = p;
3805               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3806             }
3807         }
3808       if (solv->implicitobsoleteusesprovides && (!installed || s2->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -w2)))
3809         {
3810           FOR_PROVIDES(p, pp, s2->name)
3811             {
3812               if (p != -r->p)
3813                 continue;
3814               *depp = s2->name;
3815               *sourcep = -w2;
3816               *targetp = p;
3817               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3818             }
3819         }
3820       /* all cases checked, can't happen */
3821       *depp = 0;
3822       *sourcep = -r->p;
3823       *targetp = 0;
3824       return SOLVER_PROBLEM_RPM_RULE;
3825     }
3826   /* simple requires */
3827   if (s->requires)
3828     {
3829       reqp = s->repo->idarraydata + s->requires;
3830       while ((req = *reqp++) != 0)
3831         {
3832           if (req == SOLVABLE_PREREQMARKER)
3833             continue;
3834           dp = pool->whatprovidesdata + pool_whatprovides(pool, req);
3835           if (d == 0)
3836             {
3837               if (*dp == r->w2 && dp[1] == 0)
3838                 break;
3839             }
3840           else if (dp - pool->whatprovidesdata == d)
3841             break;
3842         }
3843       if (req)
3844         {
3845           *depp = req;
3846           *sourcep = -r->p;
3847           *targetp = 0;
3848           return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3849         }
3850     }
3851   /* all cases checked, can't happen */
3852   *depp = 0;
3853   *sourcep = -r->p;
3854   *targetp = 0;
3855   return SOLVER_PROBLEM_RPM_RULE;
3856 }
3857
3858
3859 /*-------------------------------------------------------------------
3860  *
3861  * find problem rule
3862  */
3863
3864 static void
3865 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3866 {
3867   Id rid, d;
3868   Id lreqr, lconr, lsysr, ljobr;
3869   Rule *r;
3870   int reqassert = 0;
3871
3872   lreqr = lconr = lsysr = ljobr = 0;
3873   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3874     {
3875       assert(rid > 0);
3876       if (rid >= solv->learntrules)
3877         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3878       else if (rid >= solv->jobrules && rid < solv->jobrules_end)
3879         {
3880           if (!*jobrp)
3881             *jobrp = rid;
3882         }
3883       else if (rid >= solv->updaterules && rid < solv->updaterules_end)
3884         {
3885           if (!*sysrp)
3886             *sysrp = rid;
3887         }
3888       else
3889         {
3890           assert(rid < solv->rpmrules_end);
3891           r = solv->rules + rid;
3892           d = r->d < 0 ? -r->d - 1 : r->d;
3893           if (!d && r->w2 < 0)
3894             {
3895               if (!*conrp)
3896                 *conrp = rid;
3897             }
3898           else
3899             {
3900               if (!d && r->w2 == 0 && !reqassert)
3901                 {
3902                   if (*reqrp > 0 && r->p < -1)
3903                     {
3904                       Id op = -solv->rules[*reqrp].p;
3905                       if (op > 1 && solv->pool->solvables[op].arch != solv->pool->solvables[-r->p].arch)
3906                         continue;       /* different arch, skip */
3907                     }
3908                   /* prefer assertions */
3909                   *reqrp = rid;
3910                   reqassert = 1;
3911                 }
3912               if (!*reqrp)
3913                 *reqrp = rid;
3914               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed && !reqassert)
3915                 {
3916                   /* prefer rules of installed packages */
3917                   *reqrp = rid;
3918                 }
3919             }
3920         }
3921     }
3922   if (!*reqrp && lreqr)
3923     *reqrp = lreqr;
3924   if (!*conrp && lconr)
3925     *conrp = lconr;
3926   if (!*jobrp && ljobr)
3927     *jobrp = ljobr;
3928   if (!*sysrp && lsysr)
3929     *sysrp = lsysr;
3930 }
3931
3932
3933 /*-------------------------------------------------------------------
3934  *
3935  * find problem rule
3936  *
3937  * search for a rule that describes the problem to the
3938  * user. A pretty hopeless task, actually. We currently
3939  * prefer simple requires.
3940  */
3941
3942 Id
3943 solver_findproblemrule(Solver *solv, Id problem)
3944 {
3945   Id reqr, conr, sysr, jobr;
3946   Id idx = solv->problems.elements[problem - 1];
3947   reqr = conr = sysr = jobr = 0;
3948   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3949   if (reqr)
3950     return reqr;
3951   if (conr)
3952     return conr;
3953   if (sysr)
3954     return sysr;
3955   if (jobr)
3956     return jobr;
3957   assert(0);
3958 }
3959
3960
3961 /*-------------------------------------------------------------------
3962  *
3963  * create reverse obsoletes map for installed solvables
3964  *
3965  * for each installed solvable find which packages with *different* names
3966  * obsolete the solvable.
3967  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3968  */
3969
3970 static void
3971 create_obsolete_index(Solver *solv)
3972 {
3973   Pool *pool = solv->pool;
3974   Solvable *s;
3975   Repo *installed = solv->installed;
3976   Id p, pp, obs, *obsp, *obsoletes, *obsoletes_data;
3977   int i, n;
3978
3979   if (!installed || !installed->nsolvables)
3980     return;
3981   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3982   for (i = 1; i < pool->nsolvables; i++)
3983     {
3984       s = pool->solvables + i;
3985       if (!s->obsoletes)
3986         continue;
3987       if (!pool_installable(pool, s))
3988         continue;
3989       obsp = s->repo->idarraydata + s->obsoletes;
3990       while ((obs = *obsp++) != 0)
3991         {
3992           FOR_PROVIDES(p, pp, obs)
3993             {
3994               if (pool->solvables[p].repo != installed)
3995                 continue;
3996               if (pool->solvables[p].name == s->name)
3997                 continue;
3998               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3999                 continue;
4000               obsoletes[p - installed->start]++;
4001             }
4002         }
4003     }
4004   n = 0;
4005   for (i = 0; i < installed->nsolvables; i++)
4006     if (obsoletes[i])
4007       {
4008         n += obsoletes[i] + 1;
4009         obsoletes[i] = n;
4010       }
4011   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
4012   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
4013   for (i = pool->nsolvables - 1; i > 0; i--)
4014     {
4015       s = pool->solvables + i;
4016       if (!s->obsoletes)
4017         continue;
4018       if (!pool_installable(pool, s))
4019         continue;
4020       obsp = s->repo->idarraydata + s->obsoletes;
4021       while ((obs = *obsp++) != 0)
4022         {
4023           FOR_PROVIDES(p, pp, obs)
4024             {
4025               if (pool->solvables[p].repo != installed)
4026                 continue;
4027               if (pool->solvables[p].name == s->name)
4028                 continue;
4029               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
4030                 continue;
4031               p -= installed->start;
4032               if (obsoletes_data[obsoletes[p]] != i)
4033                 obsoletes_data[--obsoletes[p]] = i;
4034             }
4035         }
4036     }
4037 }
4038
4039
4040 /*-------------------------------------------------------------------
4041  *
4042  * remove disabled conflicts
4043  */
4044
4045 static void
4046 removedisabledconflicts(Solver *solv, Queue *removed)
4047 {
4048   Pool *pool = solv->pool;
4049   int i, n;
4050   Id p, why, *dp;
4051   Id new;
4052   Rule *r;
4053   Id *decisionmap = solv->decisionmap;
4054
4055   POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n");
4056   queue_empty(removed);
4057   for (i = 0; i < solv->decisionq.count; i++)
4058     {
4059       p = solv->decisionq.elements[i];
4060       if (p > 0)
4061         continue;
4062       /* a conflict. we never do conflicts on free decisions, so there
4063        * must have been an unit rule */
4064       why = solv->decisionq_why.elements[i];
4065       assert(why > 0);
4066       r = solv->rules + why;
4067       if (r->d < 0 && decisionmap[-p])
4068         {
4069           /* rule is now disabled, remove from decisionmap */
4070           POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
4071           queue_push(removed, -p);
4072           queue_push(removed, decisionmap[-p]);
4073           decisionmap[-p] = 0;
4074         }
4075     }
4076   if (!removed->count)
4077     return;
4078   /* we removed some confliced packages. some of them might still
4079    * be in conflict, so search for unit rules and re-conflict */
4080   new = 0;
4081   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
4082     {
4083       if (i == solv->nrules)
4084         {
4085           i = 1;
4086           r = solv->rules + i;
4087         }
4088       if (r->d < 0)
4089         continue;
4090       if (!r->w2)
4091         {
4092           if (r->p < 0 && !decisionmap[-r->p])
4093             new = r->p;
4094         }
4095       else if (!r->d)
4096         {
4097           /* binary rule */
4098           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
4099             new = r->p;
4100           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
4101             new = r->w2;
4102         }
4103       else
4104         {
4105           if (r->p < 0 && decisionmap[-r->p] == 0)
4106             new = r->p;
4107           if (new || DECISIONMAP_FALSE(r->p))
4108             {
4109               dp = pool->whatprovidesdata + r->d;
4110               while ((p = *dp++) != 0)
4111                 {
4112                   if (new && p == new)
4113                     continue;
4114                   if (p < 0 && decisionmap[-p] == 0)
4115                     {
4116                       if (new)
4117                         {
4118                           new = 0;
4119                           break;
4120                         }
4121                       new = p;
4122                     }
4123                   else if (!DECISIONMAP_FALSE(p))
4124                     {
4125                       new = 0;
4126                       break;
4127                     }
4128                 }
4129             }
4130         }
4131       if (new)
4132         {
4133           POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
4134           decisionmap[-new] = -1;
4135           new = 0;
4136           n = 0;        /* redo all rules */
4137         }
4138     }
4139 }
4140
4141
4142 /*-------------------------------------------------------------------
4143  *
4144  * weaken solvable dependencies
4145  */
4146
4147 static void
4148 weaken_solvable_deps(Solver *solv, Id p)
4149 {
4150   int i;
4151   Rule *r;
4152
4153   for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
4154     {
4155       if (r->p != -p)
4156         continue;
4157       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
4158         continue;       /* conflict */
4159       queue_push(&solv->weakruleq, i);
4160     }
4161 }
4162
4163 /********************************************************************/
4164 /* main() */
4165
4166 /*
4167  *
4168  * solve job queue
4169  *
4170  */
4171
4172 void
4173 solver_solve(Solver *solv, Queue *job)
4174 {
4175   Pool *pool = solv->pool;
4176   Repo *installed = solv->installed;
4177   int i;
4178   int oldnrules;
4179   Map addedmap;                /* '1' == have rpm-rules for solvable */
4180   Map installcandidatemap;
4181   Id how, what, select, name, weak, p, pp, d;
4182   Queue q, redoq;
4183   Solvable *s;
4184   int goterase;
4185   Rule *r;
4186   int now, solve_start;
4187
4188   solve_start = sat_timems(0);
4189   POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
4190   POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide);
4191   POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
4192   POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
4193   POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, allowvirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, solv->allowvirtualconflicts, solv->allowselfconflicts);
4194   POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d\n", solv->obsoleteusesprovides, solv->implicitobsoleteusesprovides);
4195   POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
4196   /* create whatprovides if not already there */
4197   if (!pool->whatprovides)
4198     pool_createwhatprovides(pool);
4199
4200   /* create obsolete index if needed */
4201   create_obsolete_index(solv);
4202
4203   /*
4204    * create basic rule set of all involved packages
4205    * use addedmap bitmap to make sure we don't create rules twice
4206    *
4207    */
4208
4209   /* create noobsolete map if needed */
4210   for (i = 0; i < job->count; i += 2)
4211     {
4212       how = job->elements[i] & ~SOLVER_WEAK;
4213       if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
4214         continue;
4215       what = job->elements[i + 1];
4216       select = how & SOLVER_SELECTMASK;
4217       if (!solv->noobsoletes.size)
4218         map_init(&solv->noobsoletes, pool->nsolvables);
4219       FOR_JOB_SELECT(p, pp, select, what)
4220         MAPSET(&solv->noobsoletes, p);
4221     }
4222
4223   map_init(&addedmap, pool->nsolvables);
4224   map_init(&installcandidatemap, pool->nsolvables);
4225   queue_init(&q);
4226
4227   /*
4228    * always install our system solvable
4229    */
4230   MAPSET(&addedmap, SYSTEMSOLVABLE);
4231   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
4232   queue_push(&solv->decisionq_why, 0);
4233   solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */
4234
4235   now = sat_timems(0);
4236   /*
4237    * create rules for all package that could be involved with the solving
4238    * so called: rpm rules
4239    *
4240    */
4241   if (installed)
4242     {
4243       oldnrules = solv->nrules;
4244       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
4245       FOR_REPO_SOLVABLES(installed, p, s)
4246         addrpmrulesforsolvable(solv, s, &addedmap);
4247       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
4248       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
4249       oldnrules = solv->nrules;
4250       FOR_REPO_SOLVABLES(installed, p, s)
4251         addrpmrulesforupdaters(solv, s, &addedmap, 1);
4252       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
4253     }
4254
4255   /*
4256    * create rules for all packages involved in the job
4257    * (to be installed or removed)
4258    */
4259
4260   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
4261   oldnrules = solv->nrules;
4262   for (i = 0; i < job->count; i += 2)
4263     {
4264       how = job->elements[i];
4265       what = job->elements[i + 1];
4266       select = how & SOLVER_SELECTMASK;
4267
4268       switch (how & SOLVER_JOBMASK)
4269         {
4270         case SOLVER_INSTALL:
4271           FOR_JOB_SELECT(p, pp, select, what)
4272             {
4273               MAPSET(&installcandidatemap, p);
4274               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
4275             }
4276           break;
4277         case SOLVER_UPDATE:
4278           /* FIXME: semantics? */
4279           FOR_JOB_SELECT(p, pp, select, what)
4280             addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
4281           break;
4282         }
4283     }
4284   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
4285
4286   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
4287
4288   oldnrules = solv->nrules;
4289
4290     /*
4291      * add rules for suggests, enhances
4292      */
4293   addrpmrulesforweak(solv, &addedmap);
4294   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
4295
4296   IF_POOLDEBUG (SAT_DEBUG_STATS)
4297     {
4298       int possible = 0, installable = 0;
4299       for (i = 1; i < pool->nsolvables; i++)
4300         {
4301           if (pool_installable(pool, pool->solvables + i))
4302             installable++;
4303           if (MAPTST(&addedmap, i))
4304             possible++;
4305         }
4306       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
4307     }
4308
4309   /*
4310    * first pass done, we now have all the rpm rules we need.
4311    * unify existing rules before going over all job rules and
4312    * policy rules.
4313    * at this point the system is always solvable,
4314    * as an empty system (remove all packages) is a valid solution
4315    */
4316
4317   unifyrules(solv);                               /* remove duplicate rpm rules */
4318
4319   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
4320
4321   solv->directdecisions = solv->decisionq.count;
4322   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
4323   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
4324   POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
4325
4326   /*
4327    * create feature rules
4328    *
4329    * foreach installed:
4330    *   create assertion (keep installed, if no update available)
4331    *   or
4332    *   create update rule (A|update1(A)|update2(A)|...)
4333    *
4334    * those are used later on to keep a version of the installed packages in
4335    * best effort mode
4336    */
4337
4338   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
4339   solv->featurerules = solv->nrules;              /* mark start of feature rules */
4340   if (installed)
4341     {
4342         /* foreach possibly installed solvable */
4343       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4344         {
4345           if (s->repo != installed)
4346             {
4347               addrule(solv, 0, 0);      /* create dummy rule */
4348               continue;
4349             }
4350           addupdaterule(solv, s, 1);    /* allow s to be updated */
4351         }
4352         /*
4353          * assert one rule per installed solvable,
4354          * either an assertion (A)
4355          * or a possible update (A|update1(A)|update2(A)|...)
4356          */
4357       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
4358     }
4359   solv->featurerules_end = solv->nrules;
4360
4361     /*
4362      * Add update rules for installed solvables
4363      *
4364      * almost identical to feature rules
4365      * except that downgrades/archchanges/vendorchanges are not allowed
4366      */
4367
4368   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
4369   solv->updaterules = solv->nrules;
4370
4371   if (installed)
4372     { /* foreach installed solvables */
4373       /* we create all update rules, but disable some later on depending on the job */
4374       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
4375         {
4376           Rule *sr;
4377
4378           if (s->repo != installed)
4379             {
4380               addrule(solv, 0, 0);      /* create dummy rule */
4381               continue;
4382             }
4383           addupdaterule(solv, s, 0);    /* allowall = 0: downgrades not allowed */
4384             /*
4385              * check for and remove duplicate
4386              */
4387           r = solv->rules + solv->nrules - 1;           /* r: update rule */
4388           sr = r - (installed->end - installed->start); /* sr: feature rule */
4389           /* it's orphaned if there is no feature rule or the feature rule
4390            * consists just of the installed package */
4391           if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
4392             queue_push(&solv->orphaned, i);
4393           if (!r->p)
4394             {
4395               assert(solv->distupgrade && !sr->p);
4396               continue;
4397             }
4398           unifyrules_sortcmp_data = pool;
4399           if (!unifyrules_sortcmp(r, sr))
4400             {
4401               /* identical rule, kill unneeded rule */
4402               if (solv->allowuninstall)
4403                 {
4404                   /* keep feature rule, make it weak */
4405                   memset(r, 0, sizeof(*r));
4406                   queue_push(&solv->weakruleq, sr - solv->rules);
4407                 }
4408               else
4409                 {
4410                   /* keep update rule */
4411                   memset(sr, 0, sizeof(*sr));
4412                 }
4413             }
4414           else if (solv->allowuninstall)
4415             {
4416               /* make both feature and update rule weak */
4417               queue_push(&solv->weakruleq, r - solv->rules);
4418               queue_push(&solv->weakruleq, sr - solv->rules);
4419             }
4420           else
4421             disablerule(solv, sr);
4422         }
4423       /* consistency check: we added a rule for _every_ installed solvable */
4424       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
4425     }
4426   solv->updaterules_end = solv->nrules;
4427
4428
4429   /*
4430    * now add all job rules
4431    */
4432
4433   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
4434
4435   solv->jobrules = solv->nrules;
4436   for (i = 0; i < job->count; i += 2)
4437     {
4438       oldnrules = solv->nrules;
4439
4440       how = job->elements[i];
4441       what = job->elements[i + 1];
4442       weak = how & SOLVER_WEAK;
4443       select = how & SOLVER_SELECTMASK;
4444       switch (how & SOLVER_JOBMASK)
4445         {
4446         case SOLVER_INSTALL:
4447           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4448           if (select == SOLVER_SOLVABLE)
4449             {
4450               p = what;
4451               d = 0;
4452             }
4453           else
4454             {
4455               queue_empty(&q);
4456               FOR_JOB_SELECT(p, pp, select, what)
4457                 queue_push(&q, p);
4458               if (!q.count)
4459                 {
4460                   /* no candidate found, make this an impossible rule */
4461                   queue_push(&q, -SYSTEMSOLVABLE);
4462                 }
4463               p = queue_shift(&q);      /* get first candidate */
4464               d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);    /* internalize */
4465             }
4466           addrule(solv, p, d);          /* add install rule */
4467           queue_push(&solv->ruletojob, i);
4468           if (weak)
4469             queue_push(&solv->weakruleq, solv->nrules - 1);
4470           break;
4471         case SOLVER_ERASE:
4472           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4473           if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
4474             {
4475               /* special case for "erase a specific solvable": we also
4476                * erase all other solvables with that name, so that they
4477                * don't get picked up as replacement */
4478               name = pool->solvables[what].name;
4479               FOR_PROVIDES(p, pp, name)
4480                 {
4481                   if (p == what)
4482                     continue;
4483                   s = pool->solvables + p;
4484                   if (s->name != name)
4485                     continue;
4486                   /* keep other versions installed */
4487                   if (s->repo == solv->installed)
4488                     continue;
4489                   /* keep installcandidates of other jobs */
4490                   if (MAPTST(&installcandidatemap, p))
4491                     continue;
4492                   addrule(solv, -p, 0);                 /* remove by Id */
4493                   queue_push(&solv->ruletojob, i);
4494                   if (weak)
4495                     queue_push(&solv->weakruleq, solv->nrules - 1);
4496                 }
4497             }
4498           FOR_JOB_SELECT(p, pp, select, what)
4499             {
4500               addrule(solv, -p, 0);
4501               queue_push(&solv->ruletojob, i);
4502               if (weak)
4503                 queue_push(&solv->weakruleq, solv->nrules - 1);
4504             }
4505           break;
4506
4507         case SOLVER_UPDATE:
4508           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4509           if (select != SOLVER_SOLVABLE)
4510             break;
4511           s = pool->solvables + what;
4512           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
4513           addupdaterule(solv, s, 0);
4514           queue_push(&solv->ruletojob, i);
4515           if (weak)
4516             queue_push(&solv->weakruleq, solv->nrules - 1);
4517           break;
4518         case SOLVER_WEAKENDEPS:
4519           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4520           if (select != SOLVER_SOLVABLE)
4521             break;
4522           s = pool->solvables + what;
4523           weaken_solvable_deps(solv, what);
4524           break;
4525         case SOLVER_NOOBSOLETES:
4526           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4527           break;
4528         case SOLVER_LOCK:
4529           POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(solv, select, what));
4530           FOR_JOB_SELECT(p, pp, select, what)
4531             {
4532               s = pool->solvables + p;
4533               if (installed && s->repo == installed)
4534                 addrule(solv, p, 0);
4535               else
4536                 addrule(solv, -p, 0);
4537               queue_push(&solv->ruletojob, i);
4538               if (weak)
4539                 queue_push(&solv->weakruleq, solv->nrules - 1);
4540             }
4541           break;
4542         default:
4543           POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
4544           break;
4545         }
4546
4547         /*
4548          * debug
4549          */
4550
4551       IF_POOLDEBUG (SAT_DEBUG_JOB)
4552         {
4553           int j;
4554           if (solv->nrules == oldnrules)
4555             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
4556           for (j = oldnrules; j < solv->nrules; j++)
4557             {
4558               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
4559               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
4560             }
4561         }
4562     }
4563   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
4564   solv->jobrules_end = solv->nrules;
4565
4566     /* all rules created
4567      * --------------------------------------------------------------
4568      * prepare for solving
4569      */
4570
4571   /* free unneeded memory */
4572   map_free(&addedmap);
4573   map_free(&installcandidatemap);
4574   queue_free(&q);
4575
4576   /* create weak map */
4577   map_init(&solv->weakrulemap, solv->nrules);
4578   for (i = 0; i < solv->weakruleq.count; i++)
4579     {
4580       p = solv->weakruleq.elements[i];
4581       MAPSET(&solv->weakrulemap, p);
4582     }
4583
4584   /* all new rules are learnt after this point */
4585   solv->learntrules = solv->nrules;
4586
4587   /* create assertion index. it is only used to speed up
4588    * makeruledecsions() a bit */
4589   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
4590     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
4591       queue_push(&solv->ruleassertions, i);
4592
4593   /* disable update rules that conflict with our job */
4594   disableupdaterules(solv, job, -1);
4595
4596   /* make decisions based on job/update assertions */
4597   makeruledecisions(solv);
4598
4599   /* create watches chains */
4600   makewatches(solv);
4601
4602   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4603
4604   /*
4605    * ********************************************
4606    * solve!
4607    * ********************************************
4608    */
4609
4610   now = sat_timems(0);
4611   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4612   POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
4613
4614   queue_init(&redoq);
4615   goterase = 0;
4616   /* disable all erase jobs (including weak "keep uninstalled" rules) */
4617   for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
4618     {
4619       if (r->d < 0)     /* disabled ? */
4620         continue;
4621       if (r->p > 0)     /* install job? */
4622         continue;
4623       disablerule(solv, r);
4624       goterase++;
4625     }
4626
4627   if (goterase)
4628     {
4629       enabledisablelearntrules(solv);
4630       removedisabledconflicts(solv, &redoq);
4631     }
4632
4633   /*
4634    * find recommended packages
4635    */
4636
4637   /* if redoq.count == 0 we already found all recommended in the
4638    * solver run */
4639   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
4640     {
4641       Id rec, *recp, p, pp;
4642
4643       /* create map of all recommened packages */
4644       solv->recommends_index = -1;
4645       MAPZERO(&solv->recommendsmap);
4646       for (i = 0; i < solv->decisionq.count; i++)
4647         {
4648           p = solv->decisionq.elements[i];
4649           if (p < 0)
4650             continue;
4651           s = pool->solvables + p;
4652           if (s->recommends)
4653             {
4654               recp = s->repo->idarraydata + s->recommends;
4655               while ((rec = *recp++) != 0)
4656                 {
4657                   FOR_PROVIDES(p, pp, rec)
4658                     if (solv->decisionmap[p] > 0)
4659                       break;
4660                   if (p)
4661                     {
4662                       if (!solv->dontshowinstalledrecommended)
4663                         {
4664                           FOR_PROVIDES(p, pp, rec)
4665                             if (solv->decisionmap[p] > 0)
4666                               MAPSET(&solv->recommendsmap, p);
4667                         }
4668                       continue; /* p != 0: already fulfilled */
4669                     }
4670                   FOR_PROVIDES(p, pp, rec)
4671                     MAPSET(&solv->recommendsmap, p);
4672                 }
4673             }
4674         }
4675       for (i = 1; i < pool->nsolvables; i++)
4676         {
4677           if (solv->decisionmap[i] < 0)
4678             continue;
4679           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4680             continue;
4681           s = pool->solvables + i;
4682           if (!MAPTST(&solv->recommendsmap, i))
4683             {
4684               if (!s->supplements)
4685                 continue;
4686               if (!pool_installable(pool, s))
4687                 continue;
4688               if (!solver_is_supplementing(solv, s))
4689                 continue;
4690             }
4691           if (solv->dontinstallrecommended)
4692             queue_push(&solv->recommendations, i);
4693           else
4694             queue_pushunique(&solv->recommendations, i);
4695         }
4696       /* we use MODE_SUGGEST here so that repo prio is ignored */
4697       policy_filter_unwanted(solv, &solv->recommendations, POLICY_MODE_SUGGEST);
4698     }
4699
4700   /*
4701    * find suggested packages
4702    */
4703
4704   if (1)
4705     {
4706       Id sug, *sugp, p, pp;
4707
4708       /* create map of all suggests that are still open */
4709       solv->recommends_index = -1;
4710       MAPZERO(&solv->suggestsmap);
4711       for (i = 0; i < solv->decisionq.count; i++)
4712         {
4713           p = solv->decisionq.elements[i];
4714           if (p < 0)
4715             continue;
4716           s = pool->solvables + p;
4717           if (s->suggests)
4718             {
4719               sugp = s->repo->idarraydata + s->suggests;
4720               while ((sug = *sugp++) != 0)
4721                 {
4722                   FOR_PROVIDES(p, pp, sug)
4723                     if (solv->decisionmap[p] > 0)
4724                       break;
4725                   if (p)
4726                     {
4727                       if (!solv->dontshowinstalledrecommended)
4728                         {
4729                           FOR_PROVIDES(p, pp, sug)
4730                             if (solv->decisionmap[p] > 0)
4731                               MAPSET(&solv->suggestsmap, p);
4732                         }
4733                       continue; /* already fulfilled */
4734                     }
4735                   FOR_PROVIDES(p, pp, sug)
4736                     MAPSET(&solv->suggestsmap, p);
4737                 }
4738             }
4739         }
4740       for (i = 1; i < pool->nsolvables; i++)
4741         {
4742           if (solv->decisionmap[i] < 0)
4743             continue;
4744           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4745             continue;
4746           s = pool->solvables + i;
4747           if (!MAPTST(&solv->suggestsmap, i))
4748             {
4749               if (!s->enhances)
4750                 continue;
4751               if (!pool_installable(pool, s))
4752                 continue;
4753               if (!solver_is_enhancing(solv, s))
4754                 continue;
4755             }
4756           queue_push(&solv->suggestions, i);
4757         }
4758       policy_filter_unwanted(solv, &solv->suggestions, POLICY_MODE_SUGGEST);
4759     }
4760
4761   if (redoq.count)
4762     {
4763       /* restore decisionmap */
4764       for (i = 0; i < redoq.count; i += 2)
4765         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4766     }
4767
4768     /*
4769      * if unsolvable, prepare solutions
4770      */
4771
4772   if (solv->problems.count)
4773     {
4774       int recocount = solv->recommendations.count;
4775       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
4776       queue_empty(&redoq);
4777       for (i = 0; i < solv->decisionq.count; i++)
4778         {
4779           Id p = solv->decisionq.elements[i];
4780           queue_push(&redoq, p);
4781           queue_push(&redoq, solv->decisionq_why.elements[i]);
4782           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4783         }
4784       problems_to_solutions(solv, job);
4785       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4786       queue_empty(&solv->decisionq);
4787       queue_empty(&solv->decisionq_why);
4788       for (i = 0; i < redoq.count; i += 3)
4789         {
4790           Id p = redoq.elements[i];
4791           queue_push(&solv->decisionq, p);
4792           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4793           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4794         }
4795       solv->recommendations.count = recocount;
4796     }
4797
4798   queue_free(&redoq);
4799   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
4800   POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
4801 }
4802
4803 /***********************************************************************/
4804 /* disk usage computations */
4805
4806 /*-------------------------------------------------------------------
4807  *
4808  * calculate DU changes
4809  */
4810
4811 void
4812 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4813 {
4814   Map installedmap;
4815
4816   solver_create_state_maps(solv, &installedmap, 0);
4817   pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
4818   map_free(&installedmap);
4819 }
4820
4821
4822 /*-------------------------------------------------------------------
4823  *
4824  * calculate changes in install size
4825  */
4826
4827 int
4828 solver_calc_installsizechange(Solver *solv)
4829 {
4830   Map installedmap;
4831   int change;
4832
4833   solver_create_state_maps(solv, &installedmap, 0);
4834   change = pool_calc_installsizechange(solv->pool, &installedmap);
4835   map_free(&installedmap);
4836   return change;
4837 }
4838
4839 #define FIND_INVOLVED_DEBUG 0
4840 void
4841 solver_find_involved(Solver *solv, Queue *installedq, Solvable *ts, Queue *q)
4842 {
4843   Pool *pool = solv->pool;
4844   Map im;
4845   Map installedm;
4846   Solvable *s;
4847   Queue iq;
4848   Queue installedq_internal;
4849   Id tp, ip, p, pp, req, *reqp, sup, *supp;
4850   int i, count;
4851
4852   tp = ts - pool->solvables;
4853   queue_init(&iq);
4854   queue_init(&installedq_internal);
4855   map_init(&im, pool->nsolvables);
4856   map_init(&installedm, pool->nsolvables);
4857
4858   if (!installedq)
4859     {
4860       installedq = &installedq_internal;
4861       if (solv->installed)
4862         {
4863           for (ip = solv->installed->start; ip < solv->installed->end; ip++)
4864             {
4865               s = pool->solvables + ip;
4866               if (s->repo != solv->installed)
4867                 continue;
4868               queue_push(installedq, ip);
4869             }
4870         }
4871     }
4872   for (i = 0; i < installedq->count; i++)
4873     {
4874       ip = installedq->elements[i];
4875       MAPSET(&installedm, ip);
4876       MAPSET(&im, ip);
4877     }
4878
4879   queue_push(&iq, ts - pool->solvables);
4880   while (iq.count)
4881     {
4882       ip = queue_shift(&iq);
4883       if (!MAPTST(&im, ip))
4884         continue;
4885       if (!MAPTST(&installedm, ip))
4886         continue;
4887       MAPCLR(&im, ip);
4888       s = pool->solvables + ip;
4889 #if FIND_INVOLVED_DEBUG
4890       printf("hello %s\n", solvable2str(pool, s));
4891 #endif
4892       if (s->requires)
4893         {
4894           reqp = s->repo->idarraydata + s->requires;
4895           while ((req = *reqp++) != 0)
4896             {
4897               if (req == SOLVABLE_PREREQMARKER)
4898                 continue;
4899               /* count number of installed packages that match */
4900               count = 0;
4901               FOR_PROVIDES(p, pp, req)
4902                 if (MAPTST(&installedm, p))
4903                   count++;
4904               if (count > 1)
4905                 continue;
4906               FOR_PROVIDES(p, pp, req)
4907                 {
4908                   if (MAPTST(&im, p))
4909                     {
4910 #if FIND_INVOLVED_DEBUG
4911                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4912 #endif
4913                       queue_push(&iq, p);
4914                     }
4915                 }
4916             }
4917         }
4918       if (s->recommends)
4919         {
4920           reqp = s->repo->idarraydata + s->recommends;
4921           while ((req = *reqp++) != 0)
4922             {
4923               count = 0;
4924               FOR_PROVIDES(p, pp, req)
4925                 if (MAPTST(&installedm, p))
4926                   count++;
4927               if (count > 1)
4928                 continue;
4929               FOR_PROVIDES(p, pp, req)
4930                 {
4931                   if (MAPTST(&im, p))
4932                     {
4933 #if FIND_INVOLVED_DEBUG
4934                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4935 #endif
4936                       queue_push(&iq, p);
4937                     }
4938                 }
4939             }
4940         }
4941       if (!iq.count)
4942         {
4943           /* supplements pass */
4944           for (i = 0; i < installedq->count; i++)
4945             {
4946               ip = installedq->elements[i];
4947               s = pool->solvables + ip;
4948               if (!s->supplements)
4949                 continue;
4950               if (!MAPTST(&im, ip))
4951                 continue;
4952               supp = s->repo->idarraydata + s->supplements;
4953               while ((sup = *supp++) != 0)
4954                 if (!dep_possible(solv, sup, &im) && dep_possible(solv, sup, &installedm))
4955                   break;
4956               /* no longer supplemented, also erase */
4957               if (sup)
4958                 {
4959 #if FIND_INVOLVED_DEBUG
4960                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
4961 #endif
4962                   queue_push(&iq, ip);
4963                 }
4964             }
4965         }
4966     }
4967
4968   for (i = 0; i < installedq->count; i++)
4969     {
4970       ip = installedq->elements[i];
4971       if (MAPTST(&im, ip))
4972         queue_push(&iq, ip);
4973     }
4974
4975   while (iq.count)
4976     {
4977       ip = queue_shift(&iq);
4978       if (!MAPTST(&installedm, ip))
4979         continue;
4980       s = pool->solvables + ip;
4981 #if FIND_INVOLVED_DEBUG
4982       printf("bye %s\n", solvable2str(pool, s));
4983 #endif
4984       if (s->requires)
4985         {
4986           reqp = s->repo->idarraydata + s->requires;
4987           while ((req = *reqp++) != 0)
4988             {
4989               FOR_PROVIDES(p, pp, req)
4990                 {
4991                   if (!MAPTST(&im, p))
4992                     {
4993                       if (p == tp)
4994                         continue;
4995 #if FIND_INVOLVED_DEBUG
4996                       printf("%s requires %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
4997 #endif
4998                       MAPSET(&im, p);
4999                       queue_push(&iq, p);
5000                     }
5001                 }
5002             }
5003         }
5004       if (s->recommends)
5005         {
5006           reqp = s->repo->idarraydata + s->recommends;
5007           while ((req = *reqp++) != 0)
5008             {
5009               FOR_PROVIDES(p, pp, req)
5010                 {
5011                   if (!MAPTST(&im, p))
5012                     {
5013                       if (p == tp)
5014                         continue;
5015 #if FIND_INVOLVED_DEBUG
5016                       printf("%s recommends %s\n", solvable2str(pool, pool->solvables + ip), solvable2str(pool, pool->solvables + p));
5017 #endif
5018                       MAPSET(&im, p);
5019                       queue_push(&iq, p);
5020                     }
5021                 }
5022             }
5023         }
5024       if (!iq.count)
5025         {
5026           /* supplements pass */
5027           for (i = 0; i < installedq->count; i++)
5028             {
5029               ip = installedq->elements[i];
5030               if (ip == tp)
5031                 continue;
5032               s = pool->solvables + ip;
5033               if (!s->supplements)
5034                 continue;
5035               if (MAPTST(&im, ip))
5036                 continue;
5037               supp = s->repo->idarraydata + s->supplements;
5038               while ((sup = *supp++) != 0)
5039                 if (dep_possible(solv, sup, &im))
5040                   break;
5041               if (sup)
5042                 {
5043 #if FIND_INVOLVED_DEBUG
5044                   printf("%s supplemented\n", solvable2str(pool, pool->solvables + ip));
5045 #endif
5046                   MAPSET(&im, ip);
5047                   queue_push(&iq, ip);
5048                 }
5049             }
5050         }
5051     }
5052
5053   queue_free(&iq);
5054
5055   /* convert map into result */
5056   for (i = 0; i < installedq->count; i++)
5057     {
5058       ip = installedq->elements[i];
5059       if (MAPTST(&im, ip))
5060         continue;
5061       if (ip == ts - pool->solvables)
5062         continue;
5063       queue_push(q, ip);
5064     }
5065   map_free(&im);
5066   map_free(&installedm);
5067   queue_free(&installedq_internal);
5068 }
5069
5070 /* EOF */