src/solver.c

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