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