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           IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1586             printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1587           for (i = -1; ; i++)
1588             {
1589               if (i == -1)
1590                 v = c->p;
1591               else if (c->d == 0)
1592                 v = i ? 0 : c->w2;
1593               else
1594                 v = *dp++;
1595               if (v == 0)
1596                 break;
1597               if (DECISIONMAP_TRUE(v))  /* the one true literal */
1598                 continue;
1599               vv = v > 0 ? v : -v;
1600               l = solv->decisionmap[vv];
1601               if (l != 1 && l != -1)
1602                 continue;
1603               MAPSET(&seen, vv);
1604             }
1605         }
1606     }
1607   map_free(&seen);
1608
1609   if (r.count == 0)
1610     *dr = 0;
1611   else if (r.count == 1 && r.elements[0] < 0)
1612     *dr = r.elements[0];
1613   else
1614     *dr = pool_queuetowhatprovides(pool, &r);
1615   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1616     {
1617       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1618       printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1619       for (i = 0; i < r.count; i++)
1620         printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1621     }
1622   /* push end marker on learnt reasons stack */
1623   queue_push(&solv->learnt_pool, 0);
1624   if (whyp)
1625     *whyp = learnt_why;
1626   return rlevel;
1627 }
1628
1629
1630 /*
1631  * reset_solver
1632  * reset the solver decisions to right after the rpm rules.
1633  * called after rules have been enabled/disabled
1634  */
1635
1636 static void
1637 reset_solver(Solver *solv)
1638 {
1639   Pool *pool = solv->pool;
1640   int i;
1641   Id v;
1642
1643   /* rewind decisions to direct rpm rule assertions */
1644   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1645     {
1646       v = solv->decisionq.elements[i];
1647       solv->decisionmap[v > 0 ? v : -v] = 0;
1648     }
1649
1650   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1651
1652   solv->decisionq_why.count = solv->directdecisions;
1653   solv->decisionq.count = solv->directdecisions;
1654   solv->recommends_index = -1;
1655   solv->propagate_index = 0;
1656
1657   /* adapt learnt rule status to new set of enabled/disabled rules */
1658   enabledisablelearntrules(solv);
1659
1660   /* redo all job/system decisions */
1661   makeruledecisions(solv);
1662   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1663
1664   /* recreate watch chains */
1665   makewatches(solv);
1666 }
1667
1668
1669 /*
1670  * analyze_unsolvable_rule
1671  */
1672
1673 static void
1674 analyze_unsolvable_rule(Solver *solv, Rule *r)
1675 {
1676   Pool *pool = solv->pool;
1677   int i;
1678   Id why = r - solv->rules;
1679   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1680     printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1681   if (solv->learntrules && why >= solv->learntrules)
1682     {
1683       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1684         if (solv->learnt_pool.elements[i] > 0)
1685           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i]);
1686       return;
1687     }
1688   /* do not add rpm rules to problem */
1689   if (why < solv->jobrules)
1690     return;
1691   /* turn rule into problem */
1692   if (why >= solv->jobrules && why < solv->systemrules)
1693     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1694   /* return if problem already countains our rule */
1695   if (solv->problems.count)
1696     {
1697       for (i = solv->problems.count - 1; i >= 0; i--)
1698         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1699           break;
1700         else if (solv->problems.elements[i] == why)
1701           return;
1702     }
1703   queue_push(&solv->problems, why);
1704 }
1705
1706
1707 /*
1708  * analyze_unsolvable
1709  *
1710  * return: 1 - disabled some rules, try again
1711  *         0 - hopeless
1712  */
1713
1714 static int
1715 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1716 {
1717   Pool *pool = solv->pool;
1718   Rule *r;
1719   Map seen;             /* global to speed things up? */
1720   Id v, vv, *dp, why;
1721   int l, i, idx;
1722   Id *decisionmap = solv->decisionmap;
1723   int oldproblemcount;
1724   int oldlearntpoolcount;
1725   int lastweak;
1726
1727   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1728   oldproblemcount = solv->problems.count;
1729   oldlearntpoolcount = solv->learnt_pool.count;
1730
1731   /* make room for proof index */
1732   /* must update it later, as analyze_unsolvable_rule would confuse
1733    * it with a rule index if we put the real value in already */
1734   queue_push(&solv->problems, 0);
1735
1736   r = cr;
1737   map_init(&seen, pool->nsolvables);
1738   queue_push(&solv->learnt_pool, r - solv->rules);
1739   analyze_unsolvable_rule(solv, r);
1740   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1741   for (i = -1; ; i++)
1742     {
1743       if (i == -1)
1744         v = r->p;
1745       else if (r->d == 0)
1746         v = i ? 0 : r->w2;
1747       else
1748         v = *dp++;
1749       if (v == 0)
1750         break;
1751       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1752           continue;
1753       vv = v > 0 ? v : -v;
1754       l = solv->decisionmap[vv];
1755       if (l < 0)
1756         l = -l;
1757       MAPSET(&seen, vv);
1758     }
1759   idx = solv->decisionq.count;
1760   while (idx > 0)
1761     {
1762       v = solv->decisionq.elements[--idx];
1763       vv = v > 0 ? v : -v;
1764       if (!MAPTST(&seen, vv))
1765         continue;
1766       why = solv->decisionq_why.elements[idx];
1767       if (!why)
1768         {
1769           /* level 1 and no why, must be an rpm assertion */
1770           IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1771             {
1772               POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "RPM ");
1773               printruleelement(solv, SAT_DEBUG_UNSOLVABLE, 0, v);
1774             }
1775           /* this is the only positive rpm assertion */
1776           if (v == SYSTEMSOLVABLE)
1777             v = -v;
1778           assert(v < 0);
1779           queue_push(&solv->learnt_pool, v);
1780           continue;
1781         }
1782       queue_push(&solv->learnt_pool, why);
1783       r = solv->rules + why;
1784       analyze_unsolvable_rule(solv, r);
1785       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1786       for (i = -1; ; i++)
1787         {
1788           if (i == -1)
1789             v = r->p;
1790           else if (r->d == 0)
1791             v = i ? 0 : r->w2;
1792           else
1793             v = *dp++;
1794           if (v == 0)
1795             break;
1796           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1797               continue;
1798           vv = v > 0 ? v : -v;
1799           l = solv->decisionmap[vv];
1800           if (l < 0)
1801             l = -l;
1802           MAPSET(&seen, vv);
1803         }
1804     }
1805   map_free(&seen);
1806   queue_push(&solv->problems, 0);       /* mark end of this problem */
1807
1808   lastweak = 0;
1809   if (solv->weakrules != solv->learntrules)
1810     {
1811       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1812         {
1813           why = solv->problems.elements[i];
1814           if (why < solv->weakrules || why >= solv->learntrules)
1815             continue;
1816           if (!lastweak || lastweak < why)
1817             lastweak = why;
1818         }
1819     }
1820   if (lastweak)
1821     {
1822       /* disable last weak rule */
1823       solv->problems.count = oldproblemcount;
1824       solv->learnt_pool.count = oldlearntpoolcount;
1825       r = solv->rules + lastweak;
1826       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling weak ");
1827       printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
1828       disablerule(solv, r);
1829       reset_solver(solv);
1830       return 1;
1831     }
1832
1833   /* finish proof */
1834   queue_push(&solv->learnt_pool, 0);
1835   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1836
1837   if (disablerules)
1838     {
1839       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1840         disableproblem(solv, solv->problems.elements[i]);
1841       reset_solver(solv);
1842       return 1;
1843     }
1844   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1845   return 0;
1846 }
1847
1848
1849 /*-----------------------------------------------------------------*/
1850 /* Decision revert */
1851
1852 /*
1853  * revert
1854  * revert decision at level
1855  */
1856
1857 static void
1858 revert(Solver *solv, int level)
1859 {
1860   Pool *pool = solv->pool;
1861   Id v, vv;
1862   while (solv->decisionq.count)
1863     {
1864       v = solv->decisionq.elements[solv->decisionq.count - 1];
1865       vv = v > 0 ? v : -v;
1866       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1867         break;
1868       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1869       solv->decisionmap[vv] = 0;
1870       solv->decisionq.count--;
1871       solv->decisionq_why.count--;
1872       solv->propagate_index = solv->decisionq.count;
1873     }
1874   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1875     {
1876       solv->branches.count--;
1877       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1878         solv->branches.count--;
1879     }
1880   solv->recommends_index = -1;
1881 }
1882
1883
1884 /*
1885  * watch2onhighest - put watch2 on literal with highest level
1886  */
1887
1888 static inline void
1889 watch2onhighest(Solver *solv, Rule *r)
1890 {
1891   int l, wl = 0;
1892   Id v, *dp;
1893
1894   if (!r->d)
1895     return;     /* binary rule, both watches are set */
1896   dp = solv->pool->whatprovidesdata + r->d;
1897   while ((v = *dp++) != 0)
1898     {
1899       l = solv->decisionmap[v < 0 ? -v : v];
1900       if (l < 0)
1901         l = -l;
1902       if (l > wl)
1903         {
1904           r->w2 = dp[-1];
1905           wl = l;
1906         }
1907     }
1908 }
1909
1910
1911 /*
1912  * setpropagatelearn
1913  *
1914  * add free decision to decisionq, increase level and
1915  * propagate decision, return if no conflict.
1916  * in conflict case, analyze conflict rule, add resulting
1917  * rule to learnt rule set, make decision from learnt
1918  * rule (always unit) and re-propagate.
1919  *
1920  * returns the new solver level or 0 if unsolvable
1921  *
1922  */
1923
1924 static int
1925 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1926 {
1927   Pool *pool = solv->pool;
1928   Rule *r;
1929   Id p, d;
1930   int l, why;
1931
1932   if (decision)
1933     {
1934       level++;
1935       if (decision > 0)
1936         solv->decisionmap[decision] = level;
1937       else
1938         solv->decisionmap[-decision] = -level;
1939       queue_push(&solv->decisionq, decision);
1940       queue_push(&solv->decisionq_why, 0);
1941     }
1942   for (;;)
1943     {
1944       r = propagate(solv, level);
1945       if (!r)
1946         break;
1947       if (level == 1)
1948         return analyze_unsolvable(solv, r, disablerules);
1949       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
1950       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1951       assert(l > 0 && l < level);
1952       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
1953       level = l;
1954       revert(solv, level);
1955       r = addrule(solv, p, d);       /* p requires d */
1956       assert(r);
1957       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
1958       queue_push(&solv->learnt_why, why);
1959       if (d)
1960         {
1961           /* at least 2 literals, needs watches */
1962           watch2onhighest(solv, r);
1963           addwatches(solv, r);
1964         }
1965       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1966       queue_push(&solv->decisionq, p);
1967       queue_push(&solv->decisionq_why, r - solv->rules);
1968       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1969         {
1970           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
1971           printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
1972           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
1973           printrule(solv, SAT_DEBUG_ANALYZE, r);
1974         }
1975     }
1976   return level;
1977 }
1978
1979
1980 /*
1981  * install best package from the queue. We add an extra package, inst, if
1982  * provided. See comment in weak install section.
1983  *
1984  * returns the new solver level or 0 if unsolvable
1985  *
1986  */
1987 static int
1988 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1989 {
1990   Pool *pool = solv->pool;
1991   Id p;
1992   int i;
1993
1994   if (dq->count > 1 || inst)
1995     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1996
1997   i = 0;
1998   if (dq->count > 1)
1999     {
2000       /* choose the supplemented one */
2001       for (i = 0; i < dq->count; i++)
2002         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2003           break;
2004       if (i == dq->count)
2005         {
2006           for (i = 1; i < dq->count; i++)
2007             queue_push(&solv->branches, dq->elements[i]);
2008           queue_push(&solv->branches, -level);
2009           i = 0;
2010         }
2011     }
2012   p = dq->elements[i];
2013
2014   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2015
2016   return setpropagatelearn(solv, level, p, disablerules);
2017 }
2018
2019
2020 /*-----------------------------------------------------------------*/
2021 /* Main solver interface */
2022
2023
2024 /*
2025  * solver_create
2026  * create solver structure
2027  *
2028  * pool: all available solvables
2029  * installed: installed Solvables
2030  *
2031  *
2032  * Upon solving, rules are created to flag the Solvables
2033  * of the 'installed' Repo as installed.
2034  */
2035
2036 Solver *
2037 solver_create(Pool *pool, Repo *installed)
2038 {
2039   Solver *solv;
2040   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2041   solv->pool = pool;
2042   solv->installed = installed;
2043
2044   queue_init(&solv->ruletojob);
2045   queue_init(&solv->decisionq);
2046   queue_init(&solv->decisionq_why);
2047   queue_init(&solv->problems);
2048   queue_init(&solv->suggestions);
2049   queue_init(&solv->learnt_why);
2050   queue_init(&solv->learnt_pool);
2051   queue_init(&solv->branches);
2052   queue_init(&solv->covenantq);
2053
2054   map_init(&solv->recommendsmap, pool->nsolvables);
2055   map_init(&solv->suggestsmap, pool->nsolvables);
2056   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
2057   solv->recommends_index = 0;
2058
2059   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2060   solv->nrules = 1;
2061   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2062   memset(solv->rules, 0, sizeof(Rule));
2063
2064   return solv;
2065 }
2066
2067
2068 /*
2069  * solver_free
2070  */
2071
2072 void
2073 solver_free(Solver *solv)
2074 {
2075   queue_free(&solv->ruletojob);
2076   queue_free(&solv->decisionq);
2077   queue_free(&solv->decisionq_why);
2078   queue_free(&solv->learnt_why);
2079   queue_free(&solv->learnt_pool);
2080   queue_free(&solv->problems);
2081   queue_free(&solv->suggestions);
2082   queue_free(&solv->branches);
2083   queue_free(&solv->covenantq);
2084
2085   map_free(&solv->recommendsmap);
2086   map_free(&solv->suggestsmap);
2087   map_free(&solv->noupdate);
2088
2089   sat_free(solv->decisionmap);
2090   sat_free(solv->rules);
2091   sat_free(solv->watches);
2092   sat_free(solv->weaksystemrules);
2093   sat_free(solv->obsoletes);
2094   sat_free(solv->obsoletes_data);
2095   sat_free(solv);
2096 }
2097
2098
2099 /*-------------------------------------------------------*/
2100
2101 /*
2102  * run_solver
2103  *
2104  * all rules have been set up, now actually run the solver
2105  *
2106  */
2107
2108 static void
2109 run_solver(Solver *solv, int disablerules, int doweak)
2110 {
2111   Queue dq;
2112   int systemlevel;
2113   int level, olevel;
2114   Rule *r;
2115   int i, j, n;
2116   Solvable *s;
2117   Pool *pool = solv->pool;
2118   Id p, *dp;
2119
2120   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2121     {
2122       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2123       for (i = 0; i < solv->nrules; i++)
2124         printrule(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2125     }
2126
2127   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2128
2129   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2130     printdecisions(solv);
2131
2132   /* start SAT algorithm */
2133   level = 1;
2134   systemlevel = level + 1;
2135   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2136
2137   queue_init(&dq);
2138   for (;;)
2139     {
2140       /*
2141        * propagate
2142        */
2143
2144       if (level == 1)
2145         {
2146           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2147           if ((r = propagate(solv, level)) != 0)
2148             {
2149               if (analyze_unsolvable(solv, r, disablerules))
2150                 continue;
2151               queue_free(&dq);
2152               return;
2153             }
2154         }
2155
2156       /*
2157        * installed packages
2158        */
2159
2160       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2161         {
2162           if (!solv->updatesystem)
2163             {
2164               /* try to keep as many packages as possible */
2165               POOL_DEBUG(SAT_DEBUG_STATS, "installing system packages\n");
2166               for (i = solv->installed->start, n = 0; ; i++)
2167                 {
2168                   if (n == solv->installed->nsolvables)
2169                     break;
2170                   if (i == solv->installed->end)
2171                     i = solv->installed->start;
2172                   s = pool->solvables + i;
2173                   if (s->repo != solv->installed)
2174                     continue;
2175                   n++;
2176                   if (solv->decisionmap[i] != 0)
2177                     continue;
2178                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2179                   olevel = level;
2180                   level = setpropagatelearn(solv, level, i, disablerules);
2181                   if (level == 0)
2182                     {
2183                       queue_free(&dq);
2184                       return;
2185                     }
2186                   if (level <= olevel)
2187                     n = 0;
2188                 }
2189             }
2190           if (solv->weaksystemrules)
2191             {
2192               POOL_DEBUG(SAT_DEBUG_STATS, "installing weak system packages\n");
2193               for (i = solv->installed->start; i < solv->installed->end; i++)
2194                 {
2195                   if (pool->solvables[i].repo != solv->installed)
2196                     continue;
2197                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
2198                     continue;
2199                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2200                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2201                     continue;
2202                   queue_empty(&dq);
2203                   if (solv->weaksystemrules[i - solv->installed->start])
2204                     {
2205                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
2206                       while ((p = *dp++) != 0)
2207                         {
2208                           if (solv->decisionmap[p] > 0)
2209                             break;
2210                           if (solv->decisionmap[p] == 0)
2211                             queue_push(&dq, p);
2212                         }
2213                       if (p)
2214                         continue;       /* update package already installed */
2215                     }
2216                   if (!dq.count && solv->decisionmap[i] != 0)
2217                     continue;
2218                   olevel = level;
2219                   /* FIXME: i is handled a bit different because we do not want
2220                    * to have it pruned just because it is not recommened.
2221                    * we should not prune installed packages instead */
2222                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2223                   if (level == 0)
2224                     {
2225                       queue_free(&dq);
2226                       return;
2227                     }
2228                   if (level <= olevel)
2229                     break;
2230                 }
2231               if (i < solv->installed->end)
2232                 continue;
2233             }
2234           systemlevel = level;
2235         }
2236
2237       /*
2238        * decide
2239        */
2240
2241       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2242       for (i = 1, n = 1; ; i++, n++)
2243         {
2244           if (n == solv->nrules)
2245             break;
2246           if (i == solv->nrules)
2247             i = 1;
2248           r = solv->rules + i;
2249           if (!r->w1)   /* ignore disabled rules */
2250             continue;
2251           queue_empty(&dq);
2252           if (r->d == 0)
2253             {
2254               /* binary or unary rule */
2255               /* need two positive undecided literals */
2256               if (r->p < 0 || r->w2 <= 0)
2257                 continue;
2258               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2259                 continue;
2260               queue_push(&dq, r->p);
2261               queue_push(&dq, r->w2);
2262             }
2263           else
2264             {
2265               /* make sure that
2266                * all negative literals are installed
2267                * no positive literal is installed
2268                * i.e. the rule is not fulfilled and we
2269                * just need to decide on the positive literals
2270                */
2271               if (r->p < 0)
2272                 {
2273                   if (solv->decisionmap[-r->p] <= 0)
2274                     continue;
2275                 }
2276               else
2277                 {
2278                   if (solv->decisionmap[r->p] > 0)
2279                     continue;
2280                   if (solv->decisionmap[r->p] == 0)
2281                     queue_push(&dq, r->p);
2282                 }
2283               dp = pool->whatprovidesdata + r->d;
2284               while ((p = *dp++) != 0)
2285                 {
2286                   if (p < 0)
2287                     {
2288                       if (solv->decisionmap[-p] <= 0)
2289                         break;
2290                     }
2291                   else
2292                     {
2293                       if (solv->decisionmap[p] > 0)
2294                         break;
2295                       if (solv->decisionmap[p] == 0)
2296                         queue_push(&dq, p);
2297                     }
2298                 }
2299               if (p)
2300                 continue;
2301             }
2302           /* dq.count < 2 cannot happen as this means that
2303            * the rule is unit */
2304           assert(dq.count > 1);
2305           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2306             {
2307               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2308               printrule(solv, SAT_DEBUG_PROPAGATE, r);
2309             }
2310
2311           olevel = level;
2312           level = selectandinstall(solv, level, &dq, 0, disablerules);
2313           if (level == 0)
2314             {
2315               queue_free(&dq);
2316               return;
2317             }
2318           if (level < systemlevel)
2319             break;
2320           n = 0;
2321         } /* for(), decide */
2322
2323       if (n != solv->nrules)    /* continue if level < systemlevel */
2324         continue;
2325
2326       if (doweak && !solv->problems.count)
2327         {
2328           int qcount;
2329
2330           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2331           if (!REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2332             {
2333               for (i = 0; i < solv->decisionq.count; i++)
2334                 {
2335                   p = solv->decisionq.elements[i];
2336                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2337                     solv->decisionmap[p] = -solv->decisionmap[p];
2338                 }
2339             }
2340           queue_empty(&dq);
2341           for (i = 1; i < pool->nsolvables; i++)
2342             {
2343               if (solv->decisionmap[i] < 0)
2344                 continue;
2345               if (solv->decisionmap[i] > 0)
2346                 {
2347                   Id *recp, rec, *pp, p;
2348                   s = pool->solvables + i;
2349                   /* installed, check for recommends */
2350                   /* XXX need to special case AND ? */
2351                   if (s->recommends)
2352                     {
2353                       recp = s->repo->idarraydata + s->recommends;
2354                       while ((rec = *recp++) != 0)
2355                         {
2356                           qcount = dq.count;
2357                           FOR_PROVIDES(p, pp, rec)
2358                             {
2359                               if (solv->decisionmap[p] > 0)
2360                                 {
2361                                   dq.count = qcount;
2362                                   break;
2363                                 }
2364                               else if (solv->decisionmap[p] == 0)
2365                                 {
2366                                   queue_pushunique(&dq, p);
2367                                 }
2368                             }
2369                         }
2370                     }
2371                 }
2372               else
2373                 {
2374                   s = pool->solvables + i;
2375                   if (!s->supplements && !s->freshens)
2376                     continue;
2377                   if (!pool_installable(pool, s))
2378                     continue;
2379                   if (solver_is_supplementing(solv, s))
2380                     queue_pushunique(&dq, i);
2381                 }
2382             }
2383           if (!REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2384             {
2385               for (i = 0; i < solv->decisionq.count; i++)
2386                 {
2387                   p = solv->decisionq.elements[i];
2388                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2389                     solv->decisionmap[p] = -solv->decisionmap[p];
2390                 }
2391             }
2392           if (dq.count)
2393             {
2394               if (dq.count > 1)
2395                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2396               p = dq.elements[0];
2397               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2398               level = setpropagatelearn(solv, level, p, 0);
2399               continue;
2400             }
2401         }
2402
2403      if (solv->solution_callback)
2404         {
2405           solv->solution_callback(solv, solv->solution_callback_data);
2406           if (solv->branches.count)
2407             {
2408               int i = solv->branches.count - 1;
2409               int l = -solv->branches.elements[i];
2410               for (; i > 0; i--)
2411                 if (solv->branches.elements[i - 1] < 0)
2412                   break;
2413               p = solv->branches.elements[i];
2414               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2415               queue_empty(&dq);
2416               for (j = i + 1; j < solv->branches.count; j++)
2417                 queue_push(&dq, solv->branches.elements[j]);
2418               solv->branches.count = i;
2419               level = l;
2420               revert(solv, level);
2421               if (dq.count > 1)
2422                 for (j = 0; j < dq.count; j++)
2423                   queue_push(&solv->branches, dq.elements[j]);
2424               olevel = level;
2425               level = setpropagatelearn(solv, level, p, disablerules);
2426               if (level == 0)
2427                 {
2428                   queue_free(&dq);
2429                   return;
2430                 }
2431               continue;
2432             }
2433           /* all branches done, we're finally finished */
2434           break;
2435         }
2436
2437       /* minimization step */
2438      if (solv->branches.count)
2439         {
2440           int l = 0, lasti = -1, lastl = -1;
2441           p = 0;
2442           for (i = solv->branches.count - 1; i >= 0; i--)
2443             {
2444               p = solv->branches.elements[i];
2445               if (p < 0)
2446                 l = -p;
2447               else if (p > 0 && solv->decisionmap[p] > l + 1)
2448                 {
2449                   lasti = i;
2450                   lastl = l;
2451                 }
2452             }
2453           if (lasti >= 0)
2454             {
2455               /* kill old solvable so that we do not loop */
2456               p = solv->branches.elements[lasti];
2457               solv->branches.elements[lasti] = 0;
2458               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2459
2460               level = lastl;
2461               revert(solv, level);
2462               olevel = level;
2463               level = setpropagatelearn(solv, level, p, disablerules);
2464               if (level == 0)
2465                 {
2466                   queue_free(&dq);
2467                   return;
2468                 }
2469               continue;
2470             }
2471         }
2472       break;
2473     }
2474   queue_free(&dq);
2475 }
2476
2477
2478 /*
2479  * refine_suggestion
2480  * at this point, all rules that led to conflicts are disabled.
2481  * we re-enable all rules of a problem set but rule "sug", then
2482  * continue to disable more rules until there as again a solution.
2483  */
2484
2485 /* FIXME: think about conflicting assertions */
2486
2487 static void
2488 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2489 {
2490   Pool *pool = solv->pool;
2491   Rule *r;
2492   int i, j;
2493   Id v;
2494   Queue disabled;
2495   int disabledcnt;
2496
2497   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2498     {
2499       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2500       for (i = 0; problem[i]; i++)
2501         {
2502           if (problem[i] == sug)
2503             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2504           printproblem(solv, problem[i]);
2505         }
2506     }
2507   queue_init(&disabled);
2508   queue_empty(refined);
2509   queue_push(refined, sug);
2510
2511   /* re-enable all problem rules with the exception of "sug" */
2512   revert(solv, 1);
2513   reset_solver(solv);
2514
2515   for (i = 0; problem[i]; i++)
2516     if (problem[i] != sug)
2517       enableproblem(solv, problem[i]);
2518
2519   if (sug < 0)
2520     disableupdaterules(solv, job, -(sug + 1));
2521
2522   for (;;)
2523     {
2524       /* re-enable as many weak rules as possible */
2525       for (i = solv->weakrules; i < solv->learntrules; i++)
2526         {
2527           r = solv->rules + i;
2528           if (!r->w1)
2529             enablerule(solv, r);
2530         }
2531
2532       queue_empty(&solv->problems);
2533       revert(solv, 1);          /* XXX move to reset_solver? */
2534       reset_solver(solv);
2535
2536       if (!solv->problems.count)
2537         run_solver(solv, 0, 0);
2538
2539       if (!solv->problems.count)
2540         {
2541           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2542           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2543             printdecisions(solv);
2544           break;                /* great, no more problems */
2545         }
2546       disabledcnt = disabled.count;
2547       /* start with 1 to skip over proof index */
2548       for (i = 1; i < solv->problems.count - 1; i++)
2549         {
2550           /* ignore solutions in refined */
2551           v = solv->problems.elements[i];
2552           if (v == 0)
2553             break;      /* end of problem reached */
2554           for (j = 0; problem[j]; j++)
2555             if (problem[j] != sug && problem[j] == v)
2556               break;
2557           if (problem[j])
2558             continue;
2559           queue_push(&disabled, v);
2560         }
2561       if (disabled.count == disabledcnt)
2562         {
2563           /* no solution found, this was an invalid suggestion! */
2564           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2565           refined->count = 0;
2566           break;
2567         }
2568       if (disabled.count == disabledcnt + 1)
2569         {
2570           /* just one suggestion, add it to refined list */
2571           v = disabled.elements[disabledcnt];
2572           queue_push(refined, v);
2573           disableproblem(solv, v);
2574           if (v < 0)
2575             disableupdaterules(solv, job, -(v + 1));
2576         }
2577       else
2578         {
2579           /* more than one solution, disable all */
2580           /* do not push anything on refine list */
2581           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2582             {
2583               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2584               for (i = disabledcnt; i < disabled.count; i++)
2585                 printproblem(solv, disabled.elements[i]);
2586             }
2587           for (i = disabledcnt; i < disabled.count; i++)
2588             disableproblem(solv, disabled.elements[i]);
2589         }
2590     }
2591   /* all done, get us back into the same state as before */
2592   /* enable refined rules again */
2593   for (i = 0; i < disabled.count; i++)
2594     enableproblem(solv, disabled.elements[i]);
2595   /* disable problem rules again */
2596   for (i = 0; problem[i]; i++)
2597     disableproblem(solv, problem[i]);
2598   disableupdaterules(solv, job, -1);
2599   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2600 }
2601
2602 static void
2603 problems_to_solutions(Solver *solv, Queue *job)
2604 {
2605   Pool *pool = solv->pool;
2606   Queue problems;
2607   Queue solution;
2608   Queue solutions;
2609   Id *problem;
2610   Id why;
2611   int i, j;
2612
2613   if (!solv->problems.count)
2614     return;
2615   queue_clone(&problems, &solv->problems);
2616   queue_init(&solution);
2617   queue_init(&solutions);
2618   /* copy over proof index */
2619   queue_push(&solutions, problems.elements[0]);
2620   problem = problems.elements + 1;
2621   for (i = 1; i < problems.count; i++)
2622     {
2623       Id v = problems.elements[i];
2624       if (v == 0)
2625         {
2626           /* mark end of this problem */
2627           queue_push(&solutions, 0);
2628           queue_push(&solutions, 0);
2629           if (i + 1 == problems.count)
2630             break;
2631           /* copy over proof of next problem */
2632           queue_push(&solutions, problems.elements[i + 1]);
2633           i++;
2634           problem = problems.elements + i + 1;
2635           continue;
2636         }
2637       refine_suggestion(solv, job, problem, v, &solution);
2638       if (!solution.count)
2639         continue;       /* this solution didn't work out */
2640
2641       for (j = 0; j < solution.count; j++)
2642         {
2643           why = solution.elements[j];
2644           /* must be either job descriptor or system rule */
2645           assert(why < 0 || (why >= solv->systemrules && why < solv->weakrules));
2646 #if 0
2647           printproblem(solv, why);
2648 #endif
2649           if (why < 0)
2650             {
2651               /* job descriptor */
2652               queue_push(&solutions, 0);
2653               queue_push(&solutions, -why);
2654             }
2655           else
2656             {
2657               /* system rule, find replacement package */
2658               Id p, rp = 0;
2659               p = solv->installed->start + (why - solv->systemrules);
2660               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2661                 {
2662                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2663                   for (; *dp; dp++)
2664                     {
2665                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2666                         continue;
2667                       if (solv->decisionmap[*dp] > 0)
2668                         {
2669                           rp = *dp;
2670                           break;
2671                         }
2672                     }
2673                 }
2674               queue_push(&solutions, p);
2675               queue_push(&solutions, rp);
2676             }
2677         }
2678       /* mark end of this solution */
2679       queue_push(&solutions, 0);
2680       queue_push(&solutions, 0);
2681     }
2682   queue_free(&solution);
2683   queue_free(&problems);
2684   /* copy queue over to solutions */
2685   queue_free(&solv->problems);
2686   queue_clone(&solv->problems, &solutions);
2687
2688   /* bring solver back into problem state */
2689   revert(solv, 1);              /* XXX move to reset_solver? */
2690   reset_solver(solv);
2691
2692   assert(solv->problems.count == solutions.count);
2693   queue_free(&solutions);
2694 }
2695
2696 Id
2697 solver_next_problem(Solver *solv, Id problem)
2698 {
2699   Id *pp;
2700   if (problem == 0)
2701     return solv->problems.count ? 1 : 0;
2702   pp = solv->problems.elements + problem;
2703   while (pp[0] || pp[1])
2704     {
2705       /* solution */
2706       pp += 2;
2707       while (pp[0] || pp[1])
2708         pp += 2;
2709       pp += 2;
2710     }
2711   pp += 2;
2712   problem = pp - solv->problems.elements;
2713   if (problem >= solv->problems.count)
2714     return 0;
2715   return problem + 1;
2716 }
2717
2718 Id
2719 solver_next_solution(Solver *solv, Id problem, Id solution)
2720 {
2721   Id *pp;
2722   if (solution == 0)
2723     {
2724       solution = problem;
2725       pp = solv->problems.elements + solution;
2726       return pp[0] || pp[1] ? solution : 0;
2727     }
2728   pp = solv->problems.elements + solution;
2729   while (pp[0] || pp[1])
2730     pp += 2;
2731   pp += 2;
2732   solution = pp - solv->problems.elements;
2733   return pp[0] || pp[1] ? solution : 0;
2734 }
2735
2736 Id
2737 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2738 {
2739   Id *pp;
2740   element = element ? element + 2 : solution;
2741   pp = solv->problems.elements + element;
2742   if (!(pp[0] || pp[1]))
2743     return 0;
2744   *p = pp[0];
2745   *rp = pp[1];
2746   return element;
2747 }
2748
2749
2750 /*
2751  * create obsoletesmap from solver decisions
2752  * required for decision handling
2753  */
2754
2755 Id *
2756 create_decisions_obsoletesmap(Solver *solv)
2757 {
2758   Pool *pool = solv->pool;
2759   Repo *installed = solv->installed;
2760   Id p, *obsoletesmap = NULL;
2761   int i;
2762   Solvable *s;
2763
2764   obsoletesmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2765   if (installed)
2766     {
2767       for (i = 0; i < solv->decisionq.count; i++)
2768         {
2769           Id *pp, n;
2770
2771           n = solv->decisionq.elements[i];
2772           if (n < 0)
2773             continue;
2774           if (n == SYSTEMSOLVABLE)
2775             continue;
2776           s = pool->solvables + n;
2777           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2778             continue;
2779           FOR_PROVIDES(p, pp, s->name)
2780             if (s->name == pool->solvables[p].name)
2781               {
2782                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2783                   {
2784                     obsoletesmap[p] = n;
2785                     obsoletesmap[n]++;
2786                   }
2787               }
2788         }
2789       for (i = 0; i < solv->decisionq.count; i++)
2790         {
2791           Id obs, *obsp;
2792           Id *pp, n;
2793
2794           n = solv->decisionq.elements[i];
2795           if (n < 0)
2796             continue;
2797           if (n == SYSTEMSOLVABLE)
2798             continue;
2799           s = pool->solvables + n;
2800           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2801             continue;
2802           if (!s->obsoletes)
2803             continue;
2804           obsp = s->repo->idarraydata + s->obsoletes;
2805           while ((obs = *obsp++) != 0)
2806             FOR_PROVIDES(p, pp, obs)
2807               {
2808                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2809                   {
2810                     obsoletesmap[p] = n;
2811                     obsoletesmap[n]++;
2812                   }
2813               }
2814         }
2815     }
2816   return obsoletesmap;
2817 }
2818
2819 /*
2820  * printdecisions
2821  */
2822
2823
2824 void
2825 printdecisions(Solver *solv)
2826 {
2827   Pool *pool = solv->pool;
2828   Repo *installed = solv->installed;
2829   Id p, *obsoletesmap = create_decisions_obsoletesmap( solv );
2830   int i;
2831   Solvable *s;
2832
2833   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions -----\n");
2834
2835   /* print solvables to be erased */
2836
2837   if (installed)
2838     {
2839       FOR_REPO_SOLVABLES(installed, p, s)
2840         {
2841           if (solv->decisionmap[p] >= 0)
2842             continue;
2843           if (obsoletesmap[p])
2844             continue;
2845           POOL_DEBUG(SAT_DEBUG_RESULT, "erase   %s\n", solvable2str(pool, s));
2846         }
2847     }
2848
2849   /* print solvables to be installed */
2850
2851   for (i = 0; i < solv->decisionq.count; i++)
2852     {
2853       int j;
2854       p = solv->decisionq.elements[i];
2855       if (p < 0)
2856         {
2857             IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2858             {
2859               p = -p;
2860               s = pool->solvables + p;
2861               POOL_DEBUG(SAT_DEBUG_SCHUBI, "level of %s is %d\n", solvable2str(pool, s), p);
2862             }
2863             continue;
2864         }
2865       if (p == SYSTEMSOLVABLE)
2866         {
2867             POOL_DEBUG(SAT_DEBUG_SCHUBI, "SYSTEMSOLVABLE\n");
2868             continue;
2869         }
2870       s = pool->solvables + p;
2871       if (installed && s->repo == installed)
2872         continue;
2873
2874       if (!obsoletesmap[p])
2875         {
2876           POOL_DEBUG(SAT_DEBUG_RESULT, "install %s", solvable2str(pool, s));
2877         }
2878       else
2879         {
2880           POOL_DEBUG(SAT_DEBUG_RESULT, "update  %s", solvable2str(pool, s));
2881           POOL_DEBUG(SAT_DEBUG_RESULT, "  (obsoletes");
2882           for (j = installed->start; j < installed->end; j++)
2883             if (obsoletesmap[j] == p)
2884               POOL_DEBUG(SAT_DEBUG_RESULT, " %s", solvable2str(pool, pool->solvables + j));
2885           POOL_DEBUG(SAT_DEBUG_RESULT, ")");
2886         }
2887       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
2888     }
2889
2890   sat_free(obsoletesmap);
2891
2892   if (solv->suggestions.count)
2893     {
2894       POOL_DEBUG(SAT_DEBUG_RESULT, "\nsuggested packages:\n");
2895       for (i = 0; i < solv->suggestions.count; i++)
2896         {
2897           s = pool->solvables + solv->suggestions.elements[i];
2898           POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
2899         }
2900     }
2901   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions end -----\n");
2902 }
2903
2904 /* this is basically the reverse of addrpmrulesforsolvable */
2905 SolverProbleminfo
2906 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
2907 {
2908   Pool *pool = solv->pool;
2909   Repo *installed = solv->installed;
2910   Rule *r;
2911   Solvable *s;
2912   int dontfix = 0;
2913   Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
2914
2915   assert(rid < solv->weakrules);
2916   if (rid >= solv->systemrules)
2917     {
2918       *depp = 0;
2919       *sourcep = solv->installed->start + (rid - solv->systemrules);
2920       *targetp = 0;
2921       return SOLVER_PROBLEM_UPDATE_RULE;
2922     }
2923   if (rid >= solv->jobrules)
2924     {
2925
2926       r = solv->rules + rid;
2927       p = solv->ruletojob.elements[rid - solv->jobrules];
2928       *depp = job->elements[p + 1];
2929       *sourcep = p;
2930       *targetp = job->elements[p];
2931       if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE)
2932         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
2933       return SOLVER_PROBLEM_JOB_RULE;
2934     }
2935   if (rid < 0)
2936     {
2937       /* a rpm rule assertion */
2938       assert(rid != -SYSTEMSOLVABLE);
2939       s = pool->solvables - rid;
2940       if (installed && !solv->fixsystem && s->repo == installed)
2941         dontfix = 1;
2942       assert(!dontfix); /* dontfix packages never have a neg assertion */
2943       /* see why the package is not installable */
2944       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
2945         return SOLVER_PROBLEM_NOT_INSTALLABLE;
2946       /* check requires */
2947       assert(s->requires);
2948       reqp = s->repo->idarraydata + s->requires;
2949       while ((req = *reqp++) != 0)
2950         {
2951           if (req == SOLVABLE_PREREQMARKER)
2952             continue;
2953           dp = pool_whatprovides(pool, req);
2954           if (*dp == 0)
2955             break;
2956         }
2957       assert(req);
2958       *depp = req;
2959       *sourcep = -rid;
2960       *targetp = 0;
2961       return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
2962     }
2963   r = solv->rules + rid;
2964   assert(r->p < 0);
2965   if (r->d == 0 && r->w2 == 0)
2966     {
2967       /* an assertion. we don't store them as rpm rules, so
2968        * can't happen */
2969       assert(0);
2970     }
2971   s = pool->solvables - r->p;
2972   if (installed && !solv->fixsystem && s->repo == installed)
2973     dontfix = 1;
2974   if (r->d == 0 && r->w2 < 0)
2975     {
2976       /* a package conflict */
2977       Solvable *s2 = pool->solvables - r->w2;
2978       int dontfix2 = 0;
2979
2980       if (installed && !solv->fixsystem && s2->repo == installed)
2981         dontfix2 = 1;
2982
2983       /* if both packages have the same name and at least one of them
2984        * is not installed, they conflict */
2985       if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
2986         {
2987           *depp = 0;
2988           *sourcep = -r->p;
2989           *targetp = -r->w2;
2990           return SOLVER_PROBLEM_SAME_NAME;
2991         }
2992
2993       /* check conflicts in both directions */
2994       if (s->conflicts)
2995         {
2996           conp = s->repo->idarraydata + s->conflicts;
2997           while ((con = *conp++) != 0)
2998             {
2999               FOR_PROVIDES(p, pp, con)
3000                 {
3001                   if (dontfix && pool->solvables[p].repo == installed)
3002                     continue;
3003                   if (p != -r->w2)
3004                     continue;
3005                   *depp = con;
3006                   *sourcep = -r->p;
3007                   *targetp = p;
3008                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3009                 }
3010             }
3011         }
3012       if (s2->conflicts)
3013         {
3014           conp = s2->repo->idarraydata + s2->conflicts;
3015           while ((con = *conp++) != 0)
3016             {
3017               FOR_PROVIDES(p, pp, con)
3018                 {
3019                   if (dontfix2 && pool->solvables[p].repo == installed)
3020                     continue;
3021                   if (p != -r->p)
3022                     continue;
3023                   *depp = con;
3024                   *sourcep = -r->w2;
3025                   *targetp = p;
3026                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3027                 }
3028             }
3029         }
3030       /* check obsoletes in both directions */
3031       if ((!installed || s->repo != installed) && s->obsoletes)
3032         {
3033           obsp = s->repo->idarraydata + s->obsoletes;
3034           while ((obs = *obsp++) != 0)
3035             {
3036               FOR_PROVIDES(p, pp, obs)
3037                 {
3038                   if (p != -r->w2)
3039                     continue;
3040                   *depp = obs;
3041                   *sourcep = -r->p;
3042                   *targetp = p;
3043                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3044                 }
3045             }
3046         }
3047       if ((!installed || s2->repo != installed) && s2->obsoletes)
3048         {
3049           obsp = s2->repo->idarraydata + s2->obsoletes;
3050           while ((obs = *obsp++) != 0)
3051             {
3052               FOR_PROVIDES(p, pp, obs)
3053                 {
3054                   if (p != -r->p)
3055                     continue;
3056                   *depp = obs;
3057                   *sourcep = -r->w2;
3058                   *targetp = p;
3059                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3060                 }
3061             }
3062         }
3063       /* all cases checked, can't happen */
3064       assert(0);
3065     }
3066   /* simple requires */
3067   assert(s->requires);
3068   reqp = s->repo->idarraydata + s->requires;
3069   while ((req = *reqp++) != 0)
3070     {
3071       if (req == SOLVABLE_PREREQMARKER)
3072         continue;
3073       dp = pool_whatprovides(pool, req);
3074       if (r->d == 0)
3075         {
3076           if (*dp == r->w2 && dp[1] == 0)
3077             break;
3078         }
3079       else if (dp - pool->whatprovidesdata == r->d)
3080         break;
3081     }
3082   assert(req);
3083   *depp = req;
3084   *sourcep = -r->p;
3085   *targetp = 0;
3086   return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3087 }
3088
3089 static void
3090 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3091 {
3092   Id rid;
3093   Id lreqr, lconr, lsysr, ljobr;
3094   Rule *r;
3095   int reqassert = 0;
3096
3097   lreqr = lconr = lsysr = ljobr = 0;
3098   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3099     {
3100       if (rid >= solv->learntrules)
3101         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3102       else if (rid >= solv->systemrules)
3103         {
3104           if (!*sysrp)
3105             *sysrp = rid;
3106         }
3107       else if (rid >= solv->jobrules)
3108         {
3109           if (!*jobrp)
3110             *jobrp = rid;
3111         }
3112       else if (rid >= 0)
3113         {
3114           r = solv->rules + rid;
3115           if (!r->d && r->w2 < 0)
3116             {
3117               if (!*conrp)
3118                 *conrp = rid;
3119             }
3120           else
3121             {
3122               if (!*reqrp)
3123                 *reqrp = rid;
3124             }
3125         }
3126       else
3127         {
3128           /* assertion, counts as require rule */
3129           /* ignore system solvable as we need useful info */
3130           if (rid == -SYSTEMSOLVABLE)
3131             continue;
3132           if (!*reqrp || !reqassert)
3133             {
3134               *reqrp = rid;
3135               reqassert = 1;
3136             }
3137         }
3138     }
3139   if (!*reqrp && lreqr)
3140     *reqrp = lreqr;
3141   if (!*conrp && lconr)
3142     *conrp = lconr;
3143   if (!*jobrp && ljobr)
3144     *jobrp = ljobr;
3145   if (!*sysrp && lsysr)
3146     *sysrp = lsysr;
3147 }
3148
3149 Id
3150 solver_findproblemrule(Solver *solv, Id problem)
3151 {
3152   Id reqr, conr, sysr, jobr;
3153   Id idx = solv->problems.elements[problem - 1];
3154   reqr = conr = sysr = jobr = 0;
3155   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3156   if (reqr)
3157     return reqr;
3158   if (conr)
3159     return conr;
3160   if (sysr)
3161     return sysr;
3162   if (jobr)
3163     return jobr;
3164   assert(0);
3165 }
3166
3167 void
3168 printprobleminfo(Solver *solv, Queue *job, Id problem)
3169 {
3170   Pool *pool = solv->pool;
3171   Id probr;
3172   Id dep, source, target;
3173   Solvable *s, *s2;
3174
3175   probr = solver_findproblemrule(solv, problem);
3176   switch (solver_problemruleinfo(solv, job, probr, &dep, &source, &target))
3177     {
3178     case SOLVER_PROBLEM_UPDATE_RULE:
3179       s = pool_id2solvable(pool, source);
3180       POOL_DEBUG(SAT_DEBUG_RESULT, "problem with installed package %s\n", solvable2str(pool, s));
3181       return;
3182     case SOLVER_PROBLEM_JOB_RULE:
3183       POOL_DEBUG(SAT_DEBUG_RESULT, "conflicting requests\n");
3184       return;
3185     case SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP:
3186       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides requested %s\n", dep2str(pool, dep));
3187       return;
3188     case SOLVER_PROBLEM_NOT_INSTALLABLE:
3189       s = pool_id2solvable(pool, source);
3190       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s is not installable\n", solvable2str(pool, s));
3191       return;
3192     case SOLVER_PROBLEM_NOTHING_PROVIDES_DEP:
3193       s = pool_id2solvable(pool, source);
3194       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides %s needed by %s\n", dep2str(pool, dep), solvable2str(pool, s));
3195       return;
3196     case SOLVER_PROBLEM_SAME_NAME:
3197       s = pool_id2solvable(pool, source);
3198       s2 = pool_id2solvable(pool, target);
3199       POOL_DEBUG(SAT_DEBUG_RESULT, "cannot install both %s and %s\n", solvable2str(pool, s), solvable2str(pool, s2));
3200       return;
3201     case SOLVER_PROBLEM_PACKAGE_CONFLICT:
3202       s = pool_id2solvable(pool, source);
3203       s2 = pool_id2solvable(pool, target);
3204       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3205       return;
3206     case SOLVER_PROBLEM_PACKAGE_OBSOLETES:
3207       s = pool_id2solvable(pool, source);
3208       s2 = pool_id2solvable(pool, target);
3209       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s obsoletes %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3210       return;
3211     case SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE:
3212       s = pool_id2solvable(pool, source);
3213       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s requires %s, but none of the providers can be installed\n", solvable2str(pool, s), dep2str(pool, dep));
3214       return;
3215     }
3216 }
3217
3218 void
3219 printsolutions(Solver *solv, Queue *job)
3220 {
3221   Pool *pool = solv->pool;
3222   int pcnt;
3223   Id p, rp, what;
3224   Id problem, solution, element;
3225   Solvable *s, *sd;
3226
3227   POOL_DEBUG(SAT_DEBUG_RESULT, "Encountered problems! Here are the solutions:\n\n");
3228   pcnt = 1;
3229   problem = 0;
3230   while ((problem = solver_next_problem(solv, problem)) != 0)
3231     {
3232       POOL_DEBUG(SAT_DEBUG_RESULT, "Problem %d:\n", pcnt++);
3233       POOL_DEBUG(SAT_DEBUG_RESULT, "====================================\n");
3234       printprobleminfo(solv, job, problem);
3235       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3236       solution = 0;
3237       while ((solution = solver_next_solution(solv, problem, solution)) != 0)
3238         {
3239           element = 0;
3240           while ((element = solver_next_solutionelement(solv, problem, solution, element, &p, &rp)) != 0)
3241             {
3242               if (p == 0)
3243                 {
3244                   /* job, rp is index into job queue */
3245                   what = job->elements[rp];
3246                   switch (job->elements[rp - 1])
3247                     {
3248                     case SOLVER_INSTALL_SOLVABLE:
3249                       s = pool->solvables + what;
3250                       if (solv->installed && s->repo == solv->installed)
3251                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not keep %s installed\n", solvable2str(pool, s));
3252                       else
3253                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", solvable2str(pool, s));
3254                       break;
3255                     case SOLVER_ERASE_SOLVABLE:
3256                       s = pool->solvables + what;
3257                       if (solv->installed && s->repo == solv->installed)
3258                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", solvable2str(pool, s));
3259                       else
3260                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not forbid installation of %s\n", solvable2str(pool, s));
3261                       break;
3262                     case SOLVER_INSTALL_SOLVABLE_NAME:
3263                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", id2str(pool, what));
3264                       break;
3265                     case SOLVER_ERASE_SOLVABLE_NAME:
3266                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", id2str(pool, what));
3267                       break;
3268                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3269                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install a solvable providing %s\n", dep2str(pool, what));
3270                       break;
3271                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
3272                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall all solvables providing %s\n", dep2str(pool, what));
3273                       break;
3274                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
3275                       s = pool->solvables + what;
3276                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install most recent version of %s\n", solvable2str(pool, s));
3277                       break;
3278                     default:
3279                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do something different\n");
3280                       break;
3281                     }
3282                 }
3283               else
3284                 {
3285                   /* policy, replace p with rp */
3286                   s = pool->solvables + p;
3287                   sd = rp ? pool->solvables + rp : 0;
3288                   if (sd)
3289                     {
3290                       int gotone = 0;
3291                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr, EVRCMP_MATCH_RELEASE) > 0)
3292                         {
3293                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow downgrade of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3294                           gotone = 1;
3295                         }
3296                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(solv, pool, s, sd))
3297                         {
3298                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow architecture change of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3299                           gotone = 1;
3300                         }
3301                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(solv,pool, s, sd))
3302                         {
3303                           if (sd->vendor)
3304                             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));
3305                           else
3306                             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));
3307                           gotone = 1;
3308                         }
3309                       if (!gotone)
3310                         POOL_DEBUG(SAT_DEBUG_RESULT, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3311                     }
3312                   else
3313                     {
3314                       POOL_DEBUG(SAT_DEBUG_RESULT, "- allow deinstallation of %s\n", solvable2str(pool, s));
3315                     }
3316
3317                 }
3318             }
3319           POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3320         }
3321     }
3322 }
3323
3324
3325 /* create reverse obsoletes map for installed solvables
3326  *
3327  * for each installed solvable find which packages with *different* names
3328  * obsolete the solvable.
3329  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3330  */
3331
3332 static void
3333 create_obsolete_index(Solver *solv)
3334 {
3335   Pool *pool = solv->pool;
3336   Solvable *s;
3337   Repo *installed = solv->installed;
3338   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3339   int i, n;
3340
3341   if (!installed || !installed->nsolvables)
3342     return;
3343   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3344   for (i = 1; i < pool->nsolvables; i++)
3345     {
3346       s = pool->solvables + i;
3347       if (s->repo == installed)
3348         continue;
3349       if (!s->obsoletes)
3350         continue;
3351       if (!pool_installable(pool, s))
3352         continue;
3353       obsp = s->repo->idarraydata + s->obsoletes;
3354       while ((obs = *obsp++) != 0)
3355         FOR_PROVIDES(p, pp, obs)
3356           {
3357             if (pool->solvables[p].repo != installed)
3358               continue;
3359             if (pool->solvables[p].name == s->name)
3360               continue;
3361             obsoletes[p - installed->start]++;
3362           }
3363     }
3364   n = 0;
3365   for (i = 0; i < installed->nsolvables; i++)
3366     if (obsoletes[i])
3367       {
3368         n += obsoletes[i] + 1;
3369         obsoletes[i] = n;
3370       }
3371   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3372   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3373   for (i = pool->nsolvables - 1; i > 0; i--)
3374     {
3375       s = pool->solvables + i;
3376       if (s->repo == installed)
3377         continue;
3378       if (!s->obsoletes)
3379         continue;
3380       if (!pool_installable(pool, s))
3381         continue;
3382       obsp = s->repo->idarraydata + s->obsoletes;
3383       while ((obs = *obsp++) != 0)
3384         FOR_PROVIDES(p, pp, obs)
3385           {
3386             if (pool->solvables[p].repo != installed)
3387               continue;
3388             if (pool->solvables[p].name == s->name)
3389               continue;
3390             p -= installed->start;
3391             if (obsoletes_data[obsoletes[p]] != i)
3392               obsoletes_data[--obsoletes[p]] = i;
3393           }
3394     }
3395 }
3396
3397
3398 /*-----------------------------------------------------------------*/
3399 /* main() */
3400
3401 /*
3402  *
3403  * solve job queue
3404  *
3405  */
3406
3407 void
3408 solver_solve(Solver *solv, Queue *job)
3409 {
3410   Pool *pool = solv->pool;
3411   Repo *installed = solv->installed;
3412   int i;
3413   int oldnrules;
3414   Map addedmap;                /* '1' == have rpm-rules for solvable */
3415   Id how, what, p, *pp, d;
3416   Queue q;
3417   Solvable *s;
3418
3419   /* create whatprovides if not already there */
3420   if (!pool->whatprovides)
3421     pool_createwhatprovides(pool);
3422
3423   /* create obsolete index if needed */
3424   if (solv->noupdateprovide)
3425     create_obsolete_index(solv);
3426
3427   /*
3428    * create basic rule set of all involved packages
3429    * use addedmap bitmap to make sure we don't create rules twice
3430    *
3431    */
3432
3433   map_init(&addedmap, pool->nsolvables);
3434   queue_init(&q);
3435
3436   /*
3437    * always install our system solvable
3438    */
3439   MAPSET(&addedmap, SYSTEMSOLVABLE);
3440   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3441   queue_push(&solv->decisionq_why, 0);
3442   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3443
3444   /*
3445    * create rules for all package that could be involved with the solving
3446    * so called: rpm rules
3447    *
3448    */
3449   if (installed)
3450     {
3451       oldnrules = solv->nrules;
3452       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3453       FOR_REPO_SOLVABLES(installed, p, s)
3454         addrpmrulesforsolvable(solv, s, &addedmap);
3455       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3456       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3457       oldnrules = solv->nrules;
3458       FOR_REPO_SOLVABLES(installed, p, s)
3459         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3460       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3461     }
3462
3463   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3464   oldnrules = solv->nrules;
3465   for (i = 0; i < job->count; i += 2)
3466     {
3467       how = job->elements[i];
3468       what = job->elements[i + 1];
3469
3470       switch(how)
3471         {
3472         case SOLVER_INSTALL_SOLVABLE:
3473           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3474           break;
3475         case SOLVER_INSTALL_SOLVABLE_NAME:
3476         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3477           FOR_PROVIDES(p, pp, what)
3478             {
3479               /* if by name, ensure that the name matches */
3480               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3481                 continue;
3482               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3483             }
3484           break;
3485         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3486           /* dont allow downgrade */
3487           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3488           break;
3489         }
3490     }
3491   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3492
3493   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3494
3495   oldnrules = solv->nrules;
3496   addrpmrulesforweak(solv, &addedmap);
3497   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3498
3499   IF_POOLDEBUG (SAT_DEBUG_STATS)
3500     {
3501       int possible = 0, installable = 0;
3502       for (i = 1; i < pool->nsolvables; i++)
3503         {
3504           if (pool_installable(pool, pool->solvables + i))
3505             installable++;
3506           if (MAPTST(&addedmap, i))
3507             possible++;
3508         }
3509       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving (rules has been generated for)\n", possible, installable);
3510     }
3511
3512   /*
3513    * first pass done, we now have all the rpm rules we need.
3514    * unify existing rules before going over all job rules and
3515    * policy rules.
3516    * at this point the system is always solvable,
3517    * as an empty system (remove all packages) is a valid solution
3518    */
3519
3520   unifyrules(solv);     /* remove duplicate rpm rules */
3521   solv->directdecisions = solv->decisionq.count;
3522
3523   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3524   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3525     printdecisions (solv);
3526
3527   /*
3528    * now add all job rules
3529    */
3530
3531   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3532
3533   solv->jobrules = solv->nrules;
3534
3535   for (i = 0; i < job->count; i += 2)
3536     {
3537       oldnrules = solv->nrules;
3538
3539       how = job->elements[i];
3540       what = job->elements[i + 1];
3541       switch(how)
3542         {
3543         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3544           s = pool->solvables + what;
3545           POOL_DEBUG(SAT_DEBUG_JOB, "job: install solvable %s\n", solvable2str(pool, s));
3546           addrule(solv, what, 0);                       /* install by Id */
3547           queue_push(&solv->ruletojob, i);
3548           break;
3549         case SOLVER_ERASE_SOLVABLE:
3550           s = pool->solvables + what;
3551           POOL_DEBUG(SAT_DEBUG_JOB, "job: erase solvable %s\n", solvable2str(pool, s));
3552           addrule(solv, -what, 0);                      /* remove by Id */
3553           queue_push(&solv->ruletojob, i);
3554           break;
3555         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3556         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3557           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3558             POOL_DEBUG(SAT_DEBUG_JOB, "job: install name %s\n", id2str(pool, what));
3559           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3560             POOL_DEBUG(SAT_DEBUG_JOB, "job: install provides %s\n", dep2str(pool, what));
3561           queue_empty(&q);
3562           FOR_PROVIDES(p, pp, what)
3563             {
3564               /* if by name, ensure that the name matches */
3565               if (how == SOLVER_INSTALL_SOLVABLE_NAME && pool->solvables[p].name != what)
3566                 continue;
3567               queue_push(&q, p);
3568             }
3569           if (!q.count)
3570             {
3571               /* no provider, make this an impossible rule */
3572               queue_push(&q, -SYSTEMSOLVABLE);
3573             }
3574
3575           p = queue_shift(&q);         /* get first provider */
3576           if (!q.count)
3577             d = 0;                     /* single provider ? -> make assertion */
3578           else
3579             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3580           addrule(solv, p, d);         /* add 'requires' rule */
3581           queue_push(&solv->ruletojob, i);
3582           break;
3583         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3584         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3585           if (how == SOLVER_ERASE_SOLVABLE_NAME)
3586             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase name %s\n", id2str(pool, what));
3587           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3588             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase provides %s\n", dep2str(pool, what));
3589           FOR_PROVIDES(p, pp, what)
3590             {
3591               /* if by name, ensure that the name matches */
3592               if (how == SOLVER_ERASE_SOLVABLE_NAME && pool->solvables[p].name != what)
3593                 continue;
3594               addrule(solv, -p, 0);  /* add 'remove' rule */
3595               queue_push(&solv->ruletojob, i);
3596             }
3597           break;
3598         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3599           s = pool->solvables + what;
3600           POOL_DEBUG(SAT_DEBUG_JOB, "job: update %s\n", solvable2str(pool, s));
3601           addupdaterule(solv, s, 0);
3602           queue_push(&solv->ruletojob, i);
3603           break;
3604         }
3605       IF_POOLDEBUG (SAT_DEBUG_JOB)
3606         {
3607           int j;
3608           if (solv->nrules == oldnrules)
3609             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created");
3610           for (j = oldnrules; j < solv->nrules; j++)
3611             {
3612               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3613               printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3614             }
3615         }
3616     }
3617   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
3618
3619   /*
3620    * now add system rules
3621    *
3622    */
3623
3624   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add system rules ***\n");
3625
3626
3627   solv->systemrules = solv->nrules;
3628
3629   /*
3630    * create rules for updating installed solvables
3631    *
3632    */
3633
3634   if (installed && !solv->allowuninstall)
3635     {                                  /* loop over all installed solvables */
3636       /* we create all update rules, but disable some later on depending on the job */
3637       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3638         {
3639           /* no system rules for patch atoms */
3640           if (s->freshens && !s->supplements)
3641             {
3642               const char *name = id2str(pool, s->name);
3643               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3644                 {
3645                   addrule(solv, 0, 0);
3646                   continue;
3647                 }
3648             }
3649           if (s->repo == installed)
3650             addupdaterule(solv, s, 0);  /* allowall = 0 */
3651           else
3652             addrule(solv, 0, 0);        /* create dummy rule */
3653         }
3654       /* consistency check: we added a rule for _every_ system solvable */
3655       assert(solv->nrules - solv->systemrules == installed->end - installed->start);
3656     }
3657
3658   /* create special weak system rules */
3659   /* those are used later on to keep a version of the installed packages in
3660      best effort mode */
3661   if (installed && installed->nsolvables)
3662     {
3663       solv->weaksystemrules = sat_calloc(installed->end - installed->start, sizeof(Id));
3664       FOR_REPO_SOLVABLES(installed, p, s)
3665         {
3666           policy_findupdatepackages(solv, s, &q, 1);
3667           if (q.count)
3668             solv->weaksystemrules[p - installed->start] = pool_queuetowhatprovides(pool, &q);
3669         }
3670     }
3671
3672   /* free unneeded memory */
3673   map_free(&addedmap);
3674   queue_free(&q);
3675
3676   solv->weakrules = solv->nrules;
3677
3678   /* try real hard to keep packages installed */
3679   if (0)
3680     {
3681       FOR_REPO_SOLVABLES(installed, p, s)
3682         {
3683           /* FIXME: can't work with refine_suggestion! */
3684           /* need to always add the rule but disable it */
3685           if (MAPTST(&solv->noupdate, p - installed->start))
3686             continue;
3687           d = solv->weaksystemrules[p - installed->start];
3688           addrule(solv, p, d);
3689         }
3690     }
3691
3692   /* all new rules are learnt after this point */
3693   solv->learntrules = solv->nrules;
3694
3695   /* disable system rules that conflict with our job */
3696   disableupdaterules(solv, job, -1);
3697
3698   /* make decisions based on job/system assertions */
3699   makeruledecisions(solv);
3700
3701   /* create watches chains */
3702   makewatches(solv);
3703
3704   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
3705
3706   /* solve! */
3707   run_solver(solv, 1, 1);
3708
3709   /* find suggested packages */
3710   if (!solv->problems.count)
3711     {
3712       Id sug, *sugp, p, *pp;
3713
3714       /* create map of all suggests that are still open */
3715       solv->recommends_index = -1;
3716       MAPZERO(&solv->suggestsmap);
3717       for (i = 0; i < solv->decisionq.count; i++)
3718         {
3719           p = solv->decisionq.elements[i];
3720           if (p < 0)
3721             continue;
3722           s = pool->solvables + p;
3723           if (s->suggests)
3724             {
3725               sugp = s->repo->idarraydata + s->suggests;
3726               while ((sug = *sugp++) != 0)
3727                 {
3728                   FOR_PROVIDES(p, pp, sug)
3729                     if (solv->decisionmap[p] > 0)
3730                       break;
3731                   if (p)
3732                     continue;   /* already fulfilled */
3733                   FOR_PROVIDES(p, pp, sug)
3734                     MAPSET(&solv->suggestsmap, p);
3735                 }
3736             }
3737         }
3738       for (i = 1; i < pool->nsolvables; i++)
3739         {
3740           if (solv->decisionmap[i] != 0)
3741             continue;
3742           s = pool->solvables + i;
3743           if (!MAPTST(&solv->suggestsmap, i))
3744             {
3745               if (!s->enhances)
3746                 continue;
3747               if (!pool_installable(pool, s))
3748                 continue;
3749               if (!solver_is_enhancing(solv, s))
3750                 continue;
3751             }
3752           queue_push(&solv->suggestions, i);
3753         }
3754       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3755     }
3756
3757   if (solv->problems.count)
3758     problems_to_solutions(solv, job);
3759 }
3760