src/solver.c

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