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