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