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