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