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