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