src/solver.c

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