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