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