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