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