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, "propagate 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; i < solv->installed->end; i++)
2193                 {
2194                   s = pool->solvables + i;
2195                   if (s->repo != solv->installed)
2196                     continue;
2197                   if (solv->decisionmap[i] != 0)
2198                     continue;
2199                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2200                   olevel = level;
2201                   level = setpropagatelearn(solv, level, i, disablerules);
2202                   if (level == 0)
2203                     {
2204                       queue_free(&dq);
2205                       return;
2206                     }
2207                   if (level <= olevel)
2208                     break;
2209                 }
2210               if (i < solv->installed->end)
2211                 continue;
2212             }
2213           if (solv->weaksystemrules)
2214             {
2215               POOL_DEBUG(SAT_DEBUG_STATS, "installing weak system packages\n");
2216               for (i = solv->installed->start; i < solv->installed->end; i++)
2217                 {
2218                   s = pool->solvables + i;
2219                   if (s->repo != solv->installed)
2220                     continue;
2221                   if (solv->decisionmap[i] > 0 || (solv->decisionmap[i] < 0 && solv->weaksystemrules[i - solv->installed->start] == 0))
2222                     continue;
2223                   /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2224                   if (MAPTST(&solv->noupdate, i - solv->installed->start))
2225                     continue;
2226                   queue_empty(&dq);
2227                   if (solv->weaksystemrules[i - solv->installed->start])
2228                     {
2229                       dp = pool->whatprovidesdata + solv->weaksystemrules[i - solv->installed->start];
2230                       while ((p = *dp++) != 0)
2231                         {
2232                           if (solv->decisionmap[p] > 0)
2233                             break;
2234                           if (solv->decisionmap[p] == 0)
2235                             queue_push(&dq, p);
2236                         }
2237                       if (p)
2238                         continue;       /* update package already installed */
2239                     }
2240                   if (!dq.count && solv->decisionmap[i] != 0)
2241                     continue;
2242                   olevel = level;
2243                   /* FIXME: i is handled a bit different because we do not want
2244                    * to have it pruned just because it is not recommened.
2245                    * we should not prune installed packages instead */
2246                   level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2247                   if (level == 0)
2248                     {
2249                       queue_free(&dq);
2250                       return;
2251                     }
2252                   if (level <= olevel)
2253                     break;
2254                 }
2255               if (i < solv->installed->end)
2256                 continue;
2257             }
2258           systemlevel = level;
2259         }
2260
2261       /*
2262        * decide
2263        */
2264
2265       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2266       for (i = 1, n = 1; ; i++, n++)
2267         {
2268           if (n == solv->nrules)
2269             break;
2270           if (i == solv->nrules)
2271             i = 1;
2272           r = solv->rules + i;
2273           if (!r->w1)   /* ignore disabled rules */
2274             continue;
2275           queue_empty(&dq);
2276           if (r->d == 0)
2277             {
2278               /* binary or unary rule */
2279               /* need two positive undecided literals */
2280               if (r->p < 0 || r->w2 <= 0)
2281                 continue;
2282               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2283                 continue;
2284               queue_push(&dq, r->p);
2285               queue_push(&dq, r->w2);
2286             }
2287           else
2288             {
2289               /* make sure that
2290                * all negative literals are installed
2291                * no positive literal is installed
2292                * i.e. the rule is not fulfilled and we
2293                * just need to decide on the positive literals
2294                */
2295               if (r->p < 0)
2296                 {
2297                   if (solv->decisionmap[-r->p] <= 0)
2298                     continue;
2299                 }
2300               else
2301                 {
2302                   if (solv->decisionmap[r->p] > 0)
2303                     continue;
2304                   if (solv->decisionmap[r->p] == 0)
2305                     queue_push(&dq, r->p);
2306                 }
2307               dp = pool->whatprovidesdata + r->d;
2308               while ((p = *dp++) != 0)
2309                 {
2310                   if (p < 0)
2311                     {
2312                       if (solv->decisionmap[-p] <= 0)
2313                         break;
2314                     }
2315                   else
2316                     {
2317                       if (solv->decisionmap[p] > 0)
2318                         break;
2319                       if (solv->decisionmap[p] == 0)
2320                         queue_push(&dq, p);
2321                     }
2322                 }
2323               if (p)
2324                 continue;
2325             }
2326           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2327             {
2328               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2329               printrule(solv, SAT_DEBUG_PROPAGATE, r);
2330             }
2331           /* dq.count < 2 cannot happen as this means that
2332            * the rule is unit */
2333           assert(dq.count > 1);
2334
2335           olevel = level;
2336           level = selectandinstall(solv, level, &dq, 0, disablerules);
2337           if (level == 0)
2338             {
2339               queue_free(&dq);
2340               return;
2341             }
2342           if (level < systemlevel)
2343             break;
2344           n = 0;
2345         } /* for(), decide */
2346
2347       if (n != solv->nrules)    /* continue if level < systemlevel */
2348         continue;
2349
2350       if (doweak && !solv->problems.count)
2351         {
2352           int qcount;
2353
2354           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2355           if (!solv->dosplitprovides && !REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2356             {
2357               for (i = 1; i < solv->decisionq.count; i++)
2358                 {
2359                   p = solv->decisionq.elements[i];
2360                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2361                     solv->decisionmap[p] = -solv->decisionmap[p];
2362                 }
2363             }
2364           queue_empty(&dq);
2365           for (i = 1; i < pool->nsolvables; i++)
2366             {
2367               if (solv->decisionmap[i] < 0)
2368                 continue;
2369               if (solv->decisionmap[i] > 0)
2370                 {
2371                   Id *recp, rec, *pp, p;
2372                   s = pool->solvables + i;
2373                   /* installed, check for recommends */
2374                   /* XXX need to special case AND ? */
2375                   if (s->recommends)
2376                     {
2377                       recp = s->repo->idarraydata + s->recommends;
2378                       while ((rec = *recp++) != 0)
2379                         {
2380                           qcount = dq.count;
2381                           FOR_PROVIDES(p, pp, rec)
2382                             {
2383                               if (solv->decisionmap[p] > 0)
2384                                 {
2385                                   dq.count = qcount;
2386                                   break;
2387                                 }
2388                               else if (solv->decisionmap[p] == 0)
2389                                 {
2390                                   queue_pushunique(&dq, p);
2391                                 }
2392                             }
2393                         }
2394                     }
2395                 }
2396               else
2397                 {
2398                   s = pool->solvables + i;
2399                   if (!s->supplements && !s->freshens)
2400                     continue;
2401                   if (!pool_installable(pool, s))
2402                     continue;
2403                   if (solver_is_supplementing(solv, s))
2404                     queue_pushunique(&dq, i);
2405                 }
2406             }
2407           if (!solv->dosplitprovides && !REGARD_RECOMMENDS_OF_INSTALLED_ITEMS)
2408             {
2409               for (i = 1; i < solv->decisionq.count; i++)
2410                 {
2411                   p = solv->decisionq.elements[i];
2412                   if (p > 0 && pool->solvables[p].repo == solv->installed)
2413                     solv->decisionmap[p] = -solv->decisionmap[p];
2414                 }
2415             }
2416           if (dq.count)
2417             {
2418               if (dq.count > 1)
2419                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2420               p = dq.elements[0];
2421               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2422               queue_push(&solv->recommendations, p);
2423               level = setpropagatelearn(solv, level, p, 0);
2424               continue;
2425             }
2426         }
2427
2428      if (solv->solution_callback)
2429         {
2430           solv->solution_callback(solv, solv->solution_callback_data);
2431           if (solv->branches.count)
2432             {
2433               int i = solv->branches.count - 1;
2434               int l = -solv->branches.elements[i];
2435               for (; i > 0; i--)
2436                 if (solv->branches.elements[i - 1] < 0)
2437                   break;
2438               p = solv->branches.elements[i];
2439               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2440               queue_empty(&dq);
2441               for (j = i + 1; j < solv->branches.count; j++)
2442                 queue_push(&dq, solv->branches.elements[j]);
2443               solv->branches.count = i;
2444               level = l;
2445               revert(solv, level);
2446               if (dq.count > 1)
2447                 for (j = 0; j < dq.count; j++)
2448                   queue_push(&solv->branches, dq.elements[j]);
2449               olevel = level;
2450               level = setpropagatelearn(solv, level, p, disablerules);
2451               if (level == 0)
2452                 {
2453                   queue_free(&dq);
2454                   return;
2455                 }
2456               continue;
2457             }
2458           /* all branches done, we're finally finished */
2459           break;
2460         }
2461
2462       /* minimization step */
2463      if (solv->branches.count)
2464         {
2465           int l = 0, lasti = -1, lastl = -1;
2466           p = 0;
2467           for (i = solv->branches.count - 1; i >= 0; i--)
2468             {
2469               p = solv->branches.elements[i];
2470               if (p < 0)
2471                 l = -p;
2472               else if (p > 0 && solv->decisionmap[p] > l + 1)
2473                 {
2474                   lasti = i;
2475                   lastl = l;
2476                 }
2477             }
2478           if (lasti >= 0)
2479             {
2480               /* kill old solvable so that we do not loop */
2481               p = solv->branches.elements[lasti];
2482               solv->branches.elements[lasti] = 0;
2483               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2484
2485               level = lastl;
2486               revert(solv, level);
2487               olevel = level;
2488               level = setpropagatelearn(solv, level, p, disablerules);
2489               if (level == 0)
2490                 {
2491                   queue_free(&dq);
2492                   return;
2493                 }
2494               continue;
2495             }
2496         }
2497       break;
2498     }
2499   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2500   queue_free(&dq);
2501 }
2502
2503
2504 /*
2505  * refine_suggestion
2506  * at this point, all rules that led to conflicts are disabled.
2507  * we re-enable all rules of a problem set but rule "sug", then
2508  * continue to disable more rules until there as again a solution.
2509  */
2510
2511 /* FIXME: think about conflicting assertions */
2512
2513 static void
2514 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2515 {
2516   Pool *pool = solv->pool;
2517   Rule *r;
2518   int i, j;
2519   Id v;
2520   Queue disabled;
2521   int disabledcnt;
2522
2523   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2524     {
2525       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2526       for (i = 0; problem[i]; i++)
2527         {
2528           if (problem[i] == sug)
2529             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2530           printproblem(solv, problem[i]);
2531         }
2532     }
2533   queue_init(&disabled);
2534   queue_empty(refined);
2535   queue_push(refined, sug);
2536
2537   /* re-enable all problem rules with the exception of "sug"(gests) */
2538   revert(solv, 1);
2539   reset_solver(solv);
2540
2541   for (i = 0; problem[i]; i++)
2542     if (problem[i] != sug)
2543       enableproblem(solv, problem[i]);
2544
2545   if (sug < 0)
2546     disableupdaterules(solv, job, -(sug + 1));
2547
2548   for (;;)
2549     {
2550       /* re-enable as many weak rules as possible */
2551       for (i = solv->weakrules; i < solv->learntrules; i++)
2552         {
2553           r = solv->rules + i;
2554           if (!r->w1)
2555             enablerule(solv, r);
2556         }
2557
2558       queue_empty(&solv->problems);
2559       revert(solv, 1);          /* XXX move to reset_solver? */
2560       reset_solver(solv);
2561
2562       if (!solv->problems.count)
2563         run_solver(solv, 0, 0);
2564
2565       if (!solv->problems.count)
2566         {
2567           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2568           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2569             printdecisions(solv);
2570           break;                /* great, no more problems */
2571         }
2572       disabledcnt = disabled.count;
2573       /* start with 1 to skip over proof index */
2574       for (i = 1; i < solv->problems.count - 1; i++)
2575         {
2576           /* ignore solutions in refined */
2577           v = solv->problems.elements[i];
2578           if (v == 0)
2579             break;      /* end of problem reached */
2580           for (j = 0; problem[j]; j++)
2581             if (problem[j] != sug && problem[j] == v)
2582               break;
2583           if (problem[j])
2584             continue;
2585           queue_push(&disabled, v);
2586         }
2587       if (disabled.count == disabledcnt)
2588         {
2589           /* no solution found, this was an invalid suggestion! */
2590           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2591           refined->count = 0;
2592           break;
2593         }
2594       if (disabled.count == disabledcnt + 1)
2595         {
2596           /* just one suggestion, add it to refined list */
2597           v = disabled.elements[disabledcnt];
2598           queue_push(refined, v);
2599           disableproblem(solv, v);
2600           if (v < 0)
2601             disableupdaterules(solv, job, -(v + 1));
2602         }
2603       else
2604         {
2605           /* more than one solution, disable all */
2606           /* do not push anything on refine list */
2607           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2608             {
2609               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2610               for (i = disabledcnt; i < disabled.count; i++)
2611                 printproblem(solv, disabled.elements[i]);
2612             }
2613           for (i = disabledcnt; i < disabled.count; i++)
2614             disableproblem(solv, disabled.elements[i]);
2615         }
2616     }
2617   /* all done, get us back into the same state as before */
2618   /* enable refined rules again */
2619   for (i = 0; i < disabled.count; i++)
2620     enableproblem(solv, disabled.elements[i]);
2621   /* disable problem rules again */
2622   for (i = 0; problem[i]; i++)
2623     disableproblem(solv, problem[i]);
2624   disableupdaterules(solv, job, -1);
2625   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2626 }
2627
2628 static void
2629 problems_to_solutions(Solver *solv, Queue *job)
2630 {
2631   Pool *pool = solv->pool;
2632   Queue problems;
2633   Queue solution;
2634   Queue solutions;
2635   Id *problem;
2636   Id why;
2637   int i, j;
2638
2639   if (!solv->problems.count)
2640     return;
2641   queue_clone(&problems, &solv->problems);
2642   queue_init(&solution);
2643   queue_init(&solutions);
2644   /* copy over proof index */
2645   queue_push(&solutions, problems.elements[0]);
2646   problem = problems.elements + 1;
2647   for (i = 1; i < problems.count; i++)
2648     {
2649       Id v = problems.elements[i];
2650       if (v == 0)
2651         {
2652           /* mark end of this problem */
2653           queue_push(&solutions, 0);
2654           queue_push(&solutions, 0);
2655           if (i + 1 == problems.count)
2656             break;
2657           /* copy over proof of next problem */
2658           queue_push(&solutions, problems.elements[i + 1]);
2659           i++;
2660           problem = problems.elements + i + 1;
2661           continue;
2662         }
2663       refine_suggestion(solv, job, problem, v, &solution);
2664       if (!solution.count)
2665         continue;       /* this solution didn't work out */
2666
2667       for (j = 0; j < solution.count; j++)
2668         {
2669           why = solution.elements[j];
2670           /* must be either job descriptor or system rule */
2671           assert(why < 0 || (why >= solv->systemrules && why < solv->weakrules));
2672 #if 0
2673           printproblem(solv, why);
2674 #endif
2675           if (why < 0)
2676             {
2677               /* job descriptor */
2678               queue_push(&solutions, 0);
2679               queue_push(&solutions, -why);
2680             }
2681           else
2682             {
2683               /* system rule, find replacement package */
2684               Id p, rp = 0;
2685               p = solv->installed->start + (why - solv->systemrules);
2686               if (solv->weaksystemrules && solv->weaksystemrules[why - solv->systemrules])
2687                 {
2688                   Id *dp = pool->whatprovidesdata + solv->weaksystemrules[why - solv->systemrules];
2689                   for (; *dp; dp++)
2690                     {
2691                       if (*dp >= solv->installed->start && *dp < solv->installed->start + solv->installed->nsolvables)
2692                         continue;
2693                       if (solv->decisionmap[*dp] > 0)
2694                         {
2695                           rp = *dp;
2696                           break;
2697                         }
2698                     }
2699                 }
2700               queue_push(&solutions, p);
2701               queue_push(&solutions, rp);
2702             }
2703         }
2704       /* mark end of this solution */
2705       queue_push(&solutions, 0);
2706       queue_push(&solutions, 0);
2707     }
2708   queue_free(&solution);
2709   queue_free(&problems);
2710   /* copy queue over to solutions */
2711   queue_free(&solv->problems);
2712   queue_clone(&solv->problems, &solutions);
2713
2714   /* bring solver back into problem state */
2715   revert(solv, 1);              /* XXX move to reset_solver? */
2716   reset_solver(solv);
2717
2718   assert(solv->problems.count == solutions.count);
2719   queue_free(&solutions);
2720 }
2721
2722 Id
2723 solver_next_problem(Solver *solv, Id problem)
2724 {
2725   Id *pp;
2726   if (problem == 0)
2727     return solv->problems.count ? 1 : 0;
2728   pp = solv->problems.elements + problem;
2729   while (pp[0] || pp[1])
2730     {
2731       /* solution */
2732       pp += 2;
2733       while (pp[0] || pp[1])
2734         pp += 2;
2735       pp += 2;
2736     }
2737   pp += 2;
2738   problem = pp - solv->problems.elements;
2739   if (problem >= solv->problems.count)
2740     return 0;
2741   return problem + 1;
2742 }
2743
2744 Id
2745 solver_next_solution(Solver *solv, Id problem, Id solution)
2746 {
2747   Id *pp;
2748   if (solution == 0)
2749     {
2750       solution = problem;
2751       pp = solv->problems.elements + solution;
2752       return pp[0] || pp[1] ? solution : 0;
2753     }
2754   pp = solv->problems.elements + solution;
2755   while (pp[0] || pp[1])
2756     pp += 2;
2757   pp += 2;
2758   solution = pp - solv->problems.elements;
2759   return pp[0] || pp[1] ? solution : 0;
2760 }
2761
2762 Id
2763 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2764 {
2765   Id *pp;
2766   element = element ? element + 2 : solution;
2767   pp = solv->problems.elements + element;
2768   if (!(pp[0] || pp[1]))
2769     return 0;
2770   *p = pp[0];
2771   *rp = pp[1];
2772   return element;
2773 }
2774
2775
2776 /*
2777  * create obsoletesmap from solver decisions
2778  * required for decision handling
2779  */
2780
2781 Id *
2782 create_decisions_obsoletesmap(Solver *solv)
2783 {
2784   Pool *pool = solv->pool;
2785   Repo *installed = solv->installed;
2786   Id p, *obsoletesmap = NULL;
2787   int i;
2788   Solvable *s;
2789
2790   obsoletesmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2791   if (installed)
2792     {
2793       for (i = 0; i < solv->decisionq.count; i++)
2794         {
2795           Id *pp, n;
2796
2797           n = solv->decisionq.elements[i];
2798           if (n < 0)
2799             continue;
2800           if (n == SYSTEMSOLVABLE)
2801             continue;
2802           s = pool->solvables + n;
2803           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2804             continue;
2805           FOR_PROVIDES(p, pp, s->name)
2806             if (s->name == pool->solvables[p].name)
2807               {
2808                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2809                   {
2810                     obsoletesmap[p] = n;
2811                     obsoletesmap[n]++;
2812                   }
2813               }
2814         }
2815       for (i = 0; i < solv->decisionq.count; i++)
2816         {
2817           Id obs, *obsp;
2818           Id *pp, n;
2819
2820           n = solv->decisionq.elements[i];
2821           if (n < 0)
2822             continue;
2823           if (n == SYSTEMSOLVABLE)
2824             continue;
2825           s = pool->solvables + n;
2826           if (s->repo == installed)             /* obsoletes don't count for already installed packages */
2827             continue;
2828           if (!s->obsoletes)
2829             continue;
2830           obsp = s->repo->idarraydata + s->obsoletes;
2831           while ((obs = *obsp++) != 0)
2832             FOR_PROVIDES(p, pp, obs)
2833               {
2834                 if (pool->solvables[p].repo == installed && !obsoletesmap[p])
2835                   {
2836                     obsoletesmap[p] = n;
2837                     obsoletesmap[n]++;
2838                   }
2839               }
2840         }
2841     }
2842   return obsoletesmap;
2843 }
2844
2845 /*
2846  * printdecisions
2847  */
2848
2849
2850 void
2851 printdecisions(Solver *solv)
2852 {
2853   Pool *pool = solv->pool;
2854   Repo *installed = solv->installed;
2855   Id p, *obsoletesmap = create_decisions_obsoletesmap( solv );
2856   int i;
2857   Solvable *s;
2858
2859   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions -----\n");
2860
2861   /* print solvables to be erased */
2862
2863   if (installed)
2864     {
2865       FOR_REPO_SOLVABLES(installed, p, s)
2866         {
2867           if (solv->decisionmap[p] >= 0)
2868             continue;
2869           if (obsoletesmap[p])
2870             continue;
2871           POOL_DEBUG(SAT_DEBUG_RESULT, "erase   %s\n", solvable2str(pool, s));
2872         }
2873     }
2874
2875   /* print solvables to be installed */
2876
2877   for (i = 0; i < solv->decisionq.count; i++)
2878     {
2879       int j;
2880       p = solv->decisionq.elements[i];
2881       if (p < 0)
2882         {
2883             IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2884             {
2885               p = -p;
2886               s = pool->solvables + p;
2887               POOL_DEBUG(SAT_DEBUG_SCHUBI, "level of %s is %d\n", solvable2str(pool, s), p);
2888             }
2889             continue;
2890         }
2891       if (p == SYSTEMSOLVABLE)
2892         {
2893             POOL_DEBUG(SAT_DEBUG_SCHUBI, "SYSTEMSOLVABLE\n");
2894             continue;
2895         }
2896       s = pool->solvables + p;
2897       if (installed && s->repo == installed)
2898         continue;
2899
2900       if (!obsoletesmap[p])
2901         {
2902           POOL_DEBUG(SAT_DEBUG_RESULT, "install %s", solvable2str(pool, s));
2903         }
2904       else
2905         {
2906           POOL_DEBUG(SAT_DEBUG_RESULT, "update  %s", solvable2str(pool, s));
2907           POOL_DEBUG(SAT_DEBUG_RESULT, "  (obsoletes");
2908           for (j = installed->start; j < installed->end; j++)
2909             if (obsoletesmap[j] == p)
2910               POOL_DEBUG(SAT_DEBUG_RESULT, " %s", solvable2str(pool, pool->solvables + j));
2911           POOL_DEBUG(SAT_DEBUG_RESULT, ")");
2912         }
2913       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
2914     }
2915
2916   sat_free(obsoletesmap);
2917
2918   if (solv->recommendations.count)
2919     {
2920       POOL_DEBUG(SAT_DEBUG_RESULT, "\nrecommended packages:\n");
2921       for (i = 0; i < solv->recommendations.count; i++)
2922         {
2923           s = pool->solvables + solv->recommendations.elements[i];
2924           POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
2925         }
2926     }
2927
2928   if (solv->suggestions.count)
2929     {
2930       POOL_DEBUG(SAT_DEBUG_RESULT, "\nsuggested packages:\n");
2931       for (i = 0; i < solv->suggestions.count; i++)
2932         {
2933           s = pool->solvables + solv->suggestions.elements[i];
2934           POOL_DEBUG(SAT_DEBUG_RESULT, "- %s\n", solvable2str(pool, s));
2935         }
2936     }
2937   POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- Decisions end -----\n");
2938 }
2939
2940 /* this is basically the reverse of addrpmrulesforsolvable */
2941 SolverProbleminfo
2942 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
2943 {
2944   Pool *pool = solv->pool;
2945   Repo *installed = solv->installed;
2946   Rule *r;
2947   Solvable *s;
2948   int dontfix = 0;
2949   Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
2950
2951   assert(rid < solv->weakrules);
2952   if (rid >= solv->systemrules)
2953     {
2954       *depp = 0;
2955       *sourcep = solv->installed->start + (rid - solv->systemrules);
2956       *targetp = 0;
2957       return SOLVER_PROBLEM_UPDATE_RULE;
2958     }
2959   if (rid >= solv->jobrules)
2960     {
2961
2962       r = solv->rules + rid;
2963       p = solv->ruletojob.elements[rid - solv->jobrules];
2964       *depp = job->elements[p + 1];
2965       *sourcep = p;
2966       *targetp = job->elements[p];
2967       if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE)
2968         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
2969       return SOLVER_PROBLEM_JOB_RULE;
2970     }
2971   if (rid < 0)
2972     {
2973       /* a rpm rule assertion */
2974       assert(rid != -SYSTEMSOLVABLE);
2975       s = pool->solvables - rid;
2976       if (installed && !solv->fixsystem && s->repo == installed)
2977         dontfix = 1;
2978       assert(!dontfix); /* dontfix packages never have a neg assertion */
2979       /* see why the package is not installable */
2980       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
2981         {
2982           *depp = 0;
2983           *sourcep = -rid;
2984           *targetp = 0;
2985           return SOLVER_PROBLEM_NOT_INSTALLABLE;
2986         }
2987       /* check requires */
2988       assert(s->requires);
2989       reqp = s->repo->idarraydata + s->requires;
2990       while ((req = *reqp++) != 0)
2991         {
2992           if (req == SOLVABLE_PREREQMARKER)
2993             continue;
2994           dp = pool_whatprovides(pool, req);
2995           if (*dp == 0)
2996             break;
2997         }
2998       assert(req);
2999       *depp = req;
3000       *sourcep = -rid;
3001       *targetp = 0;
3002       return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3003     }
3004   r = solv->rules + rid;
3005   assert(r->p < 0);
3006   if (r->d == 0 && r->w2 == 0)
3007     {
3008       /* an assertion. we don't store them as rpm rules, so
3009        * can't happen */
3010       assert(0);
3011     }
3012   s = pool->solvables - r->p;
3013   if (installed && !solv->fixsystem && s->repo == installed)
3014     dontfix = 1;
3015   if (r->d == 0 && r->w2 < 0)
3016     {
3017       /* a package conflict */
3018       Solvable *s2 = pool->solvables - r->w2;
3019       int dontfix2 = 0;
3020
3021       if (installed && !solv->fixsystem && s2->repo == installed)
3022         dontfix2 = 1;
3023
3024       /* if both packages have the same name and at least one of them
3025        * is not installed, they conflict */
3026       if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
3027         {
3028           *depp = 0;
3029           *sourcep = -r->p;
3030           *targetp = -r->w2;
3031           return SOLVER_PROBLEM_SAME_NAME;
3032         }
3033
3034       /* check conflicts in both directions */
3035       if (s->conflicts)
3036         {
3037           conp = s->repo->idarraydata + s->conflicts;
3038           while ((con = *conp++) != 0)
3039             {
3040               FOR_PROVIDES(p, pp, con)
3041                 {
3042                   if (dontfix && pool->solvables[p].repo == installed)
3043                     continue;
3044                   if (p != -r->w2)
3045                     continue;
3046                   *depp = con;
3047                   *sourcep = -r->p;
3048                   *targetp = p;
3049                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3050                 }
3051             }
3052         }
3053       if (s2->conflicts)
3054         {
3055           conp = s2->repo->idarraydata + s2->conflicts;
3056           while ((con = *conp++) != 0)
3057             {
3058               FOR_PROVIDES(p, pp, con)
3059                 {
3060                   if (dontfix2 && pool->solvables[p].repo == installed)
3061                     continue;
3062                   if (p != -r->p)
3063                     continue;
3064                   *depp = con;
3065                   *sourcep = -r->w2;
3066                   *targetp = p;
3067                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3068                 }
3069             }
3070         }
3071       /* check obsoletes in both directions */
3072       if ((!installed || s->repo != installed) && s->obsoletes)
3073         {
3074           obsp = s->repo->idarraydata + s->obsoletes;
3075           while ((obs = *obsp++) != 0)
3076             {
3077               FOR_PROVIDES(p, pp, obs)
3078                 {
3079                   if (p != -r->w2)
3080                     continue;
3081                   *depp = obs;
3082                   *sourcep = -r->p;
3083                   *targetp = p;
3084                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3085                 }
3086             }
3087         }
3088       if ((!installed || s2->repo != installed) && s2->obsoletes)
3089         {
3090           obsp = s2->repo->idarraydata + s2->obsoletes;
3091           while ((obs = *obsp++) != 0)
3092             {
3093               FOR_PROVIDES(p, pp, obs)
3094                 {
3095                   if (p != -r->p)
3096                     continue;
3097                   *depp = obs;
3098                   *sourcep = -r->w2;
3099                   *targetp = p;
3100                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3101                 }
3102             }
3103         }
3104       /* all cases checked, can't happen */
3105       assert(0);
3106     }
3107   /* simple requires */
3108   assert(s->requires);
3109   reqp = s->repo->idarraydata + s->requires;
3110   while ((req = *reqp++) != 0)
3111     {
3112       if (req == SOLVABLE_PREREQMARKER)
3113         continue;
3114       dp = pool_whatprovides(pool, req);
3115       if (r->d == 0)
3116         {
3117           if (*dp == r->w2 && dp[1] == 0)
3118             break;
3119         }
3120       else if (dp - pool->whatprovidesdata == r->d)
3121         break;
3122     }
3123   assert(req);
3124   *depp = req;
3125   *sourcep = -r->p;
3126   *targetp = 0;
3127   return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3128 }
3129
3130 static void
3131 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3132 {
3133   Id rid;
3134   Id lreqr, lconr, lsysr, ljobr;
3135   Rule *r;
3136   int reqassert = 0;
3137
3138   lreqr = lconr = lsysr = ljobr = 0;
3139   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3140     {
3141       if (rid >= solv->learntrules)
3142         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3143       else if (rid >= solv->systemrules)
3144         {
3145           if (!*sysrp)
3146             *sysrp = rid;
3147         }
3148       else if (rid >= solv->jobrules)
3149         {
3150           if (!*jobrp)
3151             *jobrp = rid;
3152         }
3153       else if (rid >= 0)
3154         {
3155           r = solv->rules + rid;
3156           if (!r->d && r->w2 < 0)
3157             {
3158               if (!*conrp)
3159                 *conrp = rid;
3160             }
3161           else
3162             {
3163               if (!*reqrp)
3164                 *reqrp = rid;
3165               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3166                 {
3167                   /* prefer rules of installed packages */
3168                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3169                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3170                     *reqrp = rid;
3171                 }
3172             }
3173         }
3174       else
3175         {
3176           /* assertion, counts as require rule */
3177           /* ignore system solvable as we need useful info */
3178           if (rid == -SYSTEMSOLVABLE)
3179             continue;
3180           if (!*reqrp || !reqassert)
3181             {
3182               *reqrp = rid;
3183               reqassert = 1;
3184             }
3185           else if (solv->installed && solv->pool->solvables[-rid].repo == solv->installed)
3186             {
3187               /* prefer rules of installed packages */
3188               Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3189               if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3190                 *reqrp = rid;
3191             }
3192         }
3193     }
3194   if (!*reqrp && lreqr)
3195     *reqrp = lreqr;
3196   if (!*conrp && lconr)
3197     *conrp = lconr;
3198   if (!*jobrp && ljobr)
3199     *jobrp = ljobr;
3200   if (!*sysrp && lsysr)
3201     *sysrp = lsysr;
3202 }
3203
3204 Id
3205 solver_findproblemrule(Solver *solv, Id problem)
3206 {
3207   Id reqr, conr, sysr, jobr;
3208   Id idx = solv->problems.elements[problem - 1];
3209   reqr = conr = sysr = jobr = 0;
3210   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3211   if (reqr)
3212     return reqr;
3213   if (conr)
3214     return conr;
3215   if (sysr)
3216     return sysr;
3217   if (jobr)
3218     return jobr;
3219   assert(0);
3220 }
3221
3222 void
3223 printprobleminfo(Solver *solv, Queue *job, Id problem)
3224 {
3225   Pool *pool = solv->pool;
3226   Id probr;
3227   Id dep, source, target;
3228   Solvable *s, *s2;
3229
3230   probr = solver_findproblemrule(solv, problem);
3231   switch (solver_problemruleinfo(solv, job, probr, &dep, &source, &target))
3232     {
3233     case SOLVER_PROBLEM_UPDATE_RULE:
3234       s = pool_id2solvable(pool, source);
3235       POOL_DEBUG(SAT_DEBUG_RESULT, "problem with installed package %s\n", solvable2str(pool, s));
3236       return;
3237     case SOLVER_PROBLEM_JOB_RULE:
3238       POOL_DEBUG(SAT_DEBUG_RESULT, "conflicting requests\n");
3239       return;
3240     case SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP:
3241       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides requested %s\n", dep2str(pool, dep));
3242       return;
3243     case SOLVER_PROBLEM_NOT_INSTALLABLE:
3244       s = pool_id2solvable(pool, source);
3245       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s is not installable\n", solvable2str(pool, s));
3246       return;
3247     case SOLVER_PROBLEM_NOTHING_PROVIDES_DEP:
3248       s = pool_id2solvable(pool, source);
3249       POOL_DEBUG(SAT_DEBUG_RESULT, "nothing provides %s needed by %s\n", dep2str(pool, dep), solvable2str(pool, s));
3250       return;
3251     case SOLVER_PROBLEM_SAME_NAME:
3252       s = pool_id2solvable(pool, source);
3253       s2 = pool_id2solvable(pool, target);
3254       POOL_DEBUG(SAT_DEBUG_RESULT, "cannot install both %s and %s\n", solvable2str(pool, s), solvable2str(pool, s2));
3255       return;
3256     case SOLVER_PROBLEM_PACKAGE_CONFLICT:
3257       s = pool_id2solvable(pool, source);
3258       s2 = pool_id2solvable(pool, target);
3259       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s conflicts with %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3260       return;
3261     case SOLVER_PROBLEM_PACKAGE_OBSOLETES:
3262       s = pool_id2solvable(pool, source);
3263       s2 = pool_id2solvable(pool, target);
3264       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s obsoletes %s provided by %s\n", solvable2str(pool, s), dep2str(pool, dep), solvable2str(pool, s2));
3265       return;
3266     case SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE:
3267       s = pool_id2solvable(pool, source);
3268       POOL_DEBUG(SAT_DEBUG_RESULT, "package %s requires %s, but none of the providers can be installed\n", solvable2str(pool, s), dep2str(pool, dep));
3269       return;
3270     }
3271 }
3272
3273 void
3274 printsolutions(Solver *solv, Queue *job)
3275 {
3276   Pool *pool = solv->pool;
3277   int pcnt;
3278   Id p, rp, what;
3279   Id problem, solution, element;
3280   Solvable *s, *sd;
3281
3282   POOL_DEBUG(SAT_DEBUG_RESULT, "Encountered problems! Here are the solutions:\n\n");
3283   pcnt = 1;
3284   problem = 0;
3285   while ((problem = solver_next_problem(solv, problem)) != 0)
3286     {
3287       POOL_DEBUG(SAT_DEBUG_RESULT, "Problem %d:\n", pcnt++);
3288       POOL_DEBUG(SAT_DEBUG_RESULT, "====================================\n");
3289       printprobleminfo(solv, job, problem);
3290       POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3291       solution = 0;
3292       while ((solution = solver_next_solution(solv, problem, solution)) != 0)
3293         {
3294           element = 0;
3295           while ((element = solver_next_solutionelement(solv, problem, solution, element, &p, &rp)) != 0)
3296             {
3297               if (p == 0)
3298                 {
3299                   /* job, rp is index into job queue */
3300                   what = job->elements[rp];
3301                   switch (job->elements[rp - 1])
3302                     {
3303                     case SOLVER_INSTALL_SOLVABLE:
3304                       s = pool->solvables + what;
3305                       if (solv->installed && s->repo == solv->installed)
3306                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not keep %s installed\n", solvable2str(pool, s));
3307                       else
3308                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", solvable2str(pool, s));
3309                       break;
3310                     case SOLVER_ERASE_SOLVABLE:
3311                       s = pool->solvables + what;
3312                       if (solv->installed && s->repo == solv->installed)
3313                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", solvable2str(pool, s));
3314                       else
3315                         POOL_DEBUG(SAT_DEBUG_RESULT, "- do not forbid installation of %s\n", solvable2str(pool, s));
3316                       break;
3317                     case SOLVER_INSTALL_SOLVABLE_NAME:
3318                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install %s\n", dep2str(pool, what));
3319                       break;
3320                     case SOLVER_ERASE_SOLVABLE_NAME:
3321                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall %s\n", dep2str(pool, what));
3322                       break;
3323                     case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3324                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install a solvable providing %s\n", dep2str(pool, what));
3325                       break;
3326                     case SOLVER_ERASE_SOLVABLE_PROVIDES:
3327                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not deinstall all solvables providing %s\n", dep2str(pool, what));
3328                       break;
3329                     case SOLVER_INSTALL_SOLVABLE_UPDATE:
3330                       s = pool->solvables + what;
3331                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do not install most recent version of %s\n", solvable2str(pool, s));
3332                       break;
3333                     default:
3334                       POOL_DEBUG(SAT_DEBUG_RESULT, "- do something different\n");
3335                       break;
3336                     }
3337                 }
3338               else
3339                 {
3340                   /* policy, replace p with rp */
3341                   s = pool->solvables + p;
3342                   sd = rp ? pool->solvables + rp : 0;
3343                   if (sd)
3344                     {
3345                       int gotone = 0;
3346                       if (!solv->allowdowngrade && evrcmp(pool, s->evr, sd->evr, EVRCMP_MATCH_RELEASE) > 0)
3347                         {
3348                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow downgrade of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3349                           gotone = 1;
3350                         }
3351                       if (!solv->allowarchchange && s->name == sd->name && s->arch != sd->arch && policy_illegal_archchange(solv, s, sd))
3352                         {
3353                           POOL_DEBUG(SAT_DEBUG_RESULT, "- allow architecture change of %s to %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3354                           gotone = 1;
3355                         }
3356                       if (!solv->allowvendorchange && s->name == sd->name && s->vendor != sd->vendor && policy_illegal_vendorchange(solv, s, sd))
3357                         {
3358                           if (sd->vendor)
3359                             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));
3360                           else
3361                             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));
3362                           gotone = 1;
3363                         }
3364                       if (!gotone)
3365                         POOL_DEBUG(SAT_DEBUG_RESULT, "- allow replacement of %s with %s\n", solvable2str(pool, s), solvable2str(pool, sd));
3366                     }
3367                   else
3368                     {
3369                       POOL_DEBUG(SAT_DEBUG_RESULT, "- allow deinstallation of %s\n", solvable2str(pool, s));
3370                     }
3371
3372                 }
3373             }
3374           POOL_DEBUG(SAT_DEBUG_RESULT, "\n");
3375         }
3376     }
3377 }
3378
3379
3380 /* create reverse obsoletes map for installed solvables
3381  *
3382  * for each installed solvable find which packages with *different* names
3383  * obsolete the solvable.
3384  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3385  */
3386
3387 static void
3388 create_obsolete_index(Solver *solv)
3389 {
3390   Pool *pool = solv->pool;
3391   Solvable *s;
3392   Repo *installed = solv->installed;
3393   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3394   int i, n;
3395
3396   if (!installed || !installed->nsolvables)
3397     return;
3398   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3399   for (i = 1; i < pool->nsolvables; i++)
3400     {
3401       s = pool->solvables + i;
3402       if (s->repo == installed)
3403         continue;
3404       if (!s->obsoletes)
3405         continue;
3406       if (!pool_installable(pool, s))
3407         continue;
3408       obsp = s->repo->idarraydata + s->obsoletes;
3409       while ((obs = *obsp++) != 0)
3410         FOR_PROVIDES(p, pp, obs)
3411           {
3412             if (pool->solvables[p].repo != installed)
3413               continue;
3414             if (pool->solvables[p].name == s->name)
3415               continue;
3416             obsoletes[p - installed->start]++;
3417           }
3418     }
3419   n = 0;
3420   for (i = 0; i < installed->nsolvables; i++)
3421     if (obsoletes[i])
3422       {
3423         n += obsoletes[i] + 1;
3424         obsoletes[i] = n;
3425       }
3426   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3427   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3428   for (i = pool->nsolvables - 1; i > 0; i--)
3429     {
3430       s = pool->solvables + i;
3431       if (s->repo == installed)
3432         continue;
3433       if (!s->obsoletes)
3434         continue;
3435       if (!pool_installable(pool, s))
3436         continue;
3437       obsp = s->repo->idarraydata + s->obsoletes;
3438       while ((obs = *obsp++) != 0)
3439         FOR_PROVIDES(p, pp, obs)
3440           {
3441             if (pool->solvables[p].repo != installed)
3442               continue;
3443             if (pool->solvables[p].name == s->name)
3444               continue;
3445             p -= installed->start;
3446             if (obsoletes_data[obsoletes[p]] != i)
3447               obsoletes_data[--obsoletes[p]] = i;
3448           }
3449     }
3450 }
3451
3452
3453 /*-----------------------------------------------------------------*/
3454 /* main() */
3455
3456 /*
3457  *
3458  * solve job queue
3459  *
3460  */
3461
3462 void
3463 solver_solve(Solver *solv, Queue *job)
3464 {
3465   Pool *pool = solv->pool;
3466   Repo *installed = solv->installed;
3467   int i;
3468   int oldnrules;
3469   Map addedmap;                /* '1' == have rpm-rules for solvable */
3470   Id how, what, name, p, *pp, d;
3471   Queue q;
3472   Solvable *s;
3473
3474   /* create whatprovides if not already there */
3475   if (!pool->whatprovides)
3476     pool_createwhatprovides(pool);
3477
3478   /* create obsolete index if needed */
3479   if (solv->noupdateprovide)
3480     create_obsolete_index(solv);
3481
3482   /*
3483    * create basic rule set of all involved packages
3484    * use addedmap bitmap to make sure we don't create rules twice
3485    *
3486    */
3487
3488   map_init(&addedmap, pool->nsolvables);
3489   queue_init(&q);
3490
3491   /*
3492    * always install our system solvable
3493    */
3494   MAPSET(&addedmap, SYSTEMSOLVABLE);
3495   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3496   queue_push(&solv->decisionq_why, 0);
3497   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3498
3499   /*
3500    * create rules for all package that could be involved with the solving
3501    * so called: rpm rules
3502    *
3503    */
3504   if (installed)
3505     {
3506       oldnrules = solv->nrules;
3507       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3508       FOR_REPO_SOLVABLES(installed, p, s)
3509         addrpmrulesforsolvable(solv, s, &addedmap);
3510       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3511       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3512       oldnrules = solv->nrules;
3513       FOR_REPO_SOLVABLES(installed, p, s)
3514         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3515       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3516     }
3517
3518   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3519   oldnrules = solv->nrules;
3520   for (i = 0; i < job->count; i += 2)
3521     {
3522       how = job->elements[i];
3523       what = job->elements[i + 1];
3524
3525       switch(how)
3526         {
3527         case SOLVER_INSTALL_SOLVABLE:
3528           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3529           break;
3530         case SOLVER_INSTALL_SOLVABLE_NAME:
3531         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3532           name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3533           while (ISRELDEP(name))
3534             {
3535               Reldep *rd = GETRELDEP(pool, name);
3536               name = rd->name;
3537             }
3538           FOR_PROVIDES(p, pp, what)
3539             {
3540               /* if by name, ensure that the name matches */
3541               if (name && pool->solvables[p].name != name)
3542                 continue;
3543               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3544             }
3545           break;
3546         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3547           /* dont allow downgrade */
3548           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3549           break;
3550         }
3551     }
3552   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3553
3554   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3555
3556   oldnrules = solv->nrules;
3557   addrpmrulesforweak(solv, &addedmap);
3558   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3559
3560   IF_POOLDEBUG (SAT_DEBUG_STATS)
3561     {
3562       int possible = 0, installable = 0;
3563       for (i = 1; i < pool->nsolvables; i++)
3564         {
3565           if (pool_installable(pool, pool->solvables + i))
3566             installable++;
3567           if (MAPTST(&addedmap, i))
3568             possible++;
3569         }
3570       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
3571     }
3572
3573   /*
3574    * first pass done, we now have all the rpm rules we need.
3575    * unify existing rules before going over all job rules and
3576    * policy rules.
3577    * at this point the system is always solvable,
3578    * as an empty system (remove all packages) is a valid solution
3579    */
3580
3581   unifyrules(solv);     /* remove duplicate rpm rules */
3582   solv->directdecisions = solv->decisionq.count;
3583
3584   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3585   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3586     printdecisions (solv);
3587
3588   /*
3589    * now add all job rules
3590    */
3591
3592   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3593
3594   solv->jobrules = solv->nrules;
3595
3596   for (i = 0; i < job->count; i += 2)
3597     {
3598       oldnrules = solv->nrules;
3599
3600       how = job->elements[i];
3601       what = job->elements[i + 1];
3602       switch(how)
3603         {
3604         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3605           s = pool->solvables + what;
3606           POOL_DEBUG(SAT_DEBUG_JOB, "job: install solvable %s\n", solvable2str(pool, s));
3607           addrule(solv, what, 0);                       /* install by Id */
3608           queue_push(&solv->ruletojob, i);
3609           break;
3610         case SOLVER_ERASE_SOLVABLE:
3611           s = pool->solvables + what;
3612           POOL_DEBUG(SAT_DEBUG_JOB, "job: erase solvable %s\n", solvable2str(pool, s));
3613           addrule(solv, -what, 0);                      /* remove by Id */
3614           queue_push(&solv->ruletojob, i);
3615           break;
3616         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3617         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3618           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3619             POOL_DEBUG(SAT_DEBUG_JOB, "job: install name %s\n", dep2str(pool, what));
3620           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3621             POOL_DEBUG(SAT_DEBUG_JOB, "job: install provides %s\n", dep2str(pool, what));
3622           queue_empty(&q);
3623           name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3624           while (ISRELDEP(name))
3625             {
3626               Reldep *rd = GETRELDEP(pool, name);
3627               name = rd->name;
3628             }
3629           FOR_PROVIDES(p, pp, what)
3630             {
3631               /* if by name, ensure that the name matches */
3632               if (name && pool->solvables[p].name != name)
3633                 continue;
3634               queue_push(&q, p);
3635             }
3636           if (!q.count)
3637             {
3638               /* no provider, make this an impossible rule */
3639               queue_push(&q, -SYSTEMSOLVABLE);
3640             }
3641
3642           p = queue_shift(&q);         /* get first provider */
3643           if (!q.count)
3644             d = 0;                     /* single provider ? -> make assertion */
3645           else
3646             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3647           addrule(solv, p, d);         /* add 'requires' rule */
3648           queue_push(&solv->ruletojob, i);
3649           break;
3650         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3651         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3652           if (how == SOLVER_ERASE_SOLVABLE_NAME)
3653             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase name %s\n", dep2str(pool, what));
3654           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3655             POOL_DEBUG(SAT_DEBUG_JOB, "job: erase provides %s\n", dep2str(pool, what));
3656           name = (how == SOLVER_ERASE_SOLVABLE_NAME) ? what : 0;
3657           while (ISRELDEP(name))
3658             {
3659               Reldep *rd = GETRELDEP(pool, name);
3660               name = rd->name;
3661             }
3662           FOR_PROVIDES(p, pp, what)
3663             {
3664               /* if by name, ensure that the name matches */
3665               if (name && pool->solvables[p].name != name)
3666                 continue;
3667               addrule(solv, -p, 0);  /* add 'remove' rule */
3668               queue_push(&solv->ruletojob, i);
3669             }
3670           break;
3671         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3672           s = pool->solvables + what;
3673           POOL_DEBUG(SAT_DEBUG_JOB, "job: update %s\n", solvable2str(pool, s));
3674           addupdaterule(solv, s, 0);
3675           queue_push(&solv->ruletojob, i);
3676           break;
3677         }
3678       IF_POOLDEBUG (SAT_DEBUG_JOB)
3679         {
3680           int j;
3681           if (solv->nrules == oldnrules)
3682             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
3683           for (j = oldnrules; j < solv->nrules; j++)
3684             {
3685               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3686               printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3687             }
3688         }
3689     }
3690   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
3691
3692   /*
3693    * now add system rules
3694    *
3695    */
3696
3697   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add system rules ***\n");
3698
3699
3700   solv->systemrules = solv->nrules;
3701
3702   /*
3703    * create rules for updating installed solvables
3704    *
3705    */
3706
3707   if (installed && !solv->allowuninstall)
3708     {                                  /* loop over all installed solvables */
3709       /* we create all update rules, but disable some later on depending on the job */
3710       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3711         {
3712           /* no system rules for patch atoms */
3713           if (s->freshens && !s->supplements)
3714             {
3715               const char *name = id2str(pool, s->name);
3716               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3717                 {
3718                   addrule(solv, 0, 0);
3719                   continue;
3720                 }
3721             }
3722           if (s->repo == installed)
3723             addupdaterule(solv, s, 0);  /* allowall = 0 */
3724           else
3725             addrule(solv, 0, 0);        /* create dummy rule */
3726         }
3727       /* consistency check: we added a rule for _every_ system solvable */
3728       assert(solv->nrules - solv->systemrules == installed->end - installed->start);
3729     }
3730
3731   /* create special weak system rules */
3732   /* those are used later on to keep a version of the installed packages in
3733      best effort mode */
3734   if (installed && installed->nsolvables)
3735     {
3736       solv->weaksystemrules = sat_calloc(installed->end - installed->start, sizeof(Id));
3737       FOR_REPO_SOLVABLES(installed, p, s)
3738         {
3739           policy_findupdatepackages(solv, s, &q, 1);
3740           if (q.count)
3741             solv->weaksystemrules[p - installed->start] = pool_queuetowhatprovides(pool, &q);
3742         }
3743     }
3744
3745   /* free unneeded memory */
3746   map_free(&addedmap);
3747   queue_free(&q);
3748
3749   solv->weakrules = solv->nrules;
3750
3751   /* try real hard to keep packages installed */
3752   if (0)
3753     {
3754       FOR_REPO_SOLVABLES(installed, p, s)
3755         {
3756           /* FIXME: can't work with refine_suggestion! */
3757           /* need to always add the rule but disable it */
3758           if (MAPTST(&solv->noupdate, p - installed->start))
3759             continue;
3760           d = solv->weaksystemrules[p - installed->start];
3761           addrule(solv, p, d);
3762         }
3763     }
3764
3765   /* all new rules are learnt after this point */
3766   solv->learntrules = solv->nrules;
3767
3768   /* disable system rules that conflict with our job */
3769   disableupdaterules(solv, job, -1);
3770
3771   /* make decisions based on job/system assertions */
3772   makeruledecisions(solv);
3773
3774   /* create watches chains */
3775   makewatches(solv);
3776
3777   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
3778
3779   /* solve! */
3780   run_solver(solv, solv->dontinstallrecommended ? 0 : 1, 1);
3781
3782   /* find recommended packages */
3783   if (!solv->problems.count && solv->dontinstallrecommended)
3784     {
3785       Id rec, *recp, p, *pp;
3786
3787       /* create map of all suggests that are still open */
3788       solv->recommends_index = -1;
3789       MAPZERO(&solv->recommendsmap);
3790       for (i = 0; i < solv->decisionq.count; i++)
3791         {
3792           p = solv->decisionq.elements[i];
3793           if (p < 0)
3794             continue;
3795           s = pool->solvables + p;
3796           if (s->recommends)
3797             {
3798               recp = s->repo->idarraydata + s->recommends;
3799               while ((rec = *recp++) != 0)
3800                 {
3801                   FOR_PROVIDES(p, pp, rec)
3802                     if (solv->decisionmap[p] > 0)
3803                       break;
3804                   if (p)
3805                     continue;   /* already fulfilled */
3806                   FOR_PROVIDES(p, pp, rec)
3807                     MAPSET(&solv->recommendsmap, p);
3808                 }
3809             }
3810         }
3811       for (i = 1; i < pool->nsolvables; i++)
3812         {
3813           if (solv->decisionmap[i] != 0)
3814             continue;
3815           s = pool->solvables + i;
3816           if (!MAPTST(&solv->recommendsmap, i))
3817             {
3818               if (!s->supplements)
3819                 continue;
3820               if (!pool_installable(pool, s))
3821                 continue;
3822               if (!solver_is_supplementing(solv, s))
3823                 continue;
3824             }
3825           queue_push(&solv->recommendations, i);
3826         }
3827       /* we use MODE_SUGGEST here so that repo prio is ignored */
3828       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
3829     }
3830
3831   /* find suggested packages */
3832   if (!solv->problems.count)
3833     {
3834       Id sug, *sugp, p, *pp;
3835
3836       /* create map of all suggests that are still open */
3837       solv->recommends_index = -1;
3838       MAPZERO(&solv->suggestsmap);
3839       for (i = 0; i < solv->decisionq.count; i++)
3840         {
3841           p = solv->decisionq.elements[i];
3842           if (p < 0)
3843             continue;
3844           s = pool->solvables + p;
3845           if (s->suggests)
3846             {
3847               sugp = s->repo->idarraydata + s->suggests;
3848               while ((sug = *sugp++) != 0)
3849                 {
3850                   FOR_PROVIDES(p, pp, sug)
3851                     if (solv->decisionmap[p] > 0)
3852                       break;
3853                   if (p)
3854                     continue;   /* already fulfilled */
3855                   FOR_PROVIDES(p, pp, sug)
3856                     MAPSET(&solv->suggestsmap, p);
3857                 }
3858             }
3859         }
3860       for (i = 1; i < pool->nsolvables; i++)
3861         {
3862           if (solv->decisionmap[i] != 0)
3863             continue;
3864           s = pool->solvables + i;
3865           if (!MAPTST(&solv->suggestsmap, i))
3866             {
3867               if (!s->enhances)
3868                 continue;
3869               if (!pool_installable(pool, s))
3870                 continue;
3871               if (!solver_is_enhancing(solv, s))
3872                 continue;
3873             }
3874           queue_push(&solv->suggestions, i);
3875         }
3876       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3877     }
3878
3879   if (solv->problems.count)
3880     problems_to_solutions(solv, job);
3881 }
3882
3883 /***********************************************************************/
3884
3885 void
3886 solver_calc_changed_pkgs(Solver *solv, Queue *pkgs)
3887 {
3888   Pool *pool = solv->pool;
3889   Map installmap;
3890   Solvable *s;
3891   int i;
3892   Id p;
3893
3894   /* create list of solvables that have to be installed */
3895   /* (this is actually just a simple sort) */
3896   map_init(&installmap, pool->nsolvables);
3897   for (i = 1; i < solv->decisionq.count; i++)
3898     {
3899       Id p = solv->decisionq.elements[i];
3900       if (p < 0)
3901         continue;
3902       s = pool->solvables + p;
3903       if (!s->repo)
3904         continue;
3905       if (solv->installed && s->repo == solv->installed)
3906         continue;
3907       MAPSET(&installmap, p);
3908     }
3909   for (p = 1; p < pool->nsolvables; p++)
3910     if (MAPTST(&installmap, p))
3911       queue_push(pkgs, p);
3912   map_free(&installmap);
3913   /* run through erase solvable dudata */
3914   if (solv->installed)
3915     {
3916       FOR_REPO_SOLVABLES(solv->installed, p, s)
3917         {
3918           if (solv->decisionmap[p] < 0)
3919             queue_push(pkgs, -p);
3920         }
3921     }
3922 }
3923
3924 void
3925 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
3926 {
3927   Queue pkgs;
3928   queue_init(&pkgs);
3929   solver_calc_changed_pkgs(solv, &pkgs);
3930   pool_calc_duchanges(solv->pool, &pkgs, mps, nmps);
3931   queue_free(&pkgs);
3932 }
3933
3934 int
3935 solver_calc_installsizechange(Solver *solv)
3936 {
3937   int change;
3938   Queue pkgs;
3939   queue_init(&pkgs);
3940   solver_calc_changed_pkgs(solv, &pkgs);
3941   change = pool_calc_installsizechange(solv->pool, &pkgs);
3942   queue_free(&pkgs);
3943   return change;
3944 }
3945