src/solver.c

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