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             MAPCLR(&seen, r.elements[i]);
1535           /* only level 1 marks left */
1536           l1num++;
1537           goto l1retry;
1538         }
1539       why = solv->decisionq_why.elements[idx];
1540       if (!why)                 /* just in case, maye for SYSTEMSOLVABLE */
1541         goto l1retry;
1542       c = solv->rules + why;
1543     }
1544   map_free(&seen);
1545
1546   if (r.count == 0)
1547     *dr = 0;
1548   else if (r.count == 1 && r.elements[0] < 0)
1549     *dr = r.elements[0];
1550   else
1551     *dr = pool_queuetowhatprovides(pool, &r);
1552   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1553     {
1554       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1555       solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1556       for (i = 0; i < r.count; i++)
1557         solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1558     }
1559   /* push end marker on learnt reasons stack */
1560   queue_push(&solv->learnt_pool, 0);
1561   if (whyp)
1562     *whyp = learnt_why;
1563   return rlevel;
1564 }
1565
1566
1567 /*
1568  * reset_solver
1569  * reset the solver decisions to right after the rpm rules.
1570  * called after rules have been enabled/disabled
1571  */
1572
1573 static void
1574 reset_solver(Solver *solv)
1575 {
1576   Pool *pool = solv->pool;
1577   int i;
1578   Id v;
1579
1580   /* rewind decisions to direct rpm rule assertions */
1581   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1582     {
1583       v = solv->decisionq.elements[i];
1584       solv->decisionmap[v > 0 ? v : -v] = 0;
1585     }
1586
1587   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1588
1589   solv->decisionq_why.count = solv->directdecisions;
1590   solv->decisionq.count = solv->directdecisions;
1591   solv->recommends_index = -1;
1592   solv->propagate_index = 0;
1593
1594   /* adapt learnt rule status to new set of enabled/disabled rules */
1595   enabledisablelearntrules(solv);
1596
1597   /* redo all job/update decisions */
1598   makeruledecisions(solv);
1599   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1600
1601   /* recreate watch chains */
1602   makewatches(solv);
1603 }
1604
1605
1606 /*
1607  * analyze_unsolvable_rule
1608  */
1609
1610 static void
1611 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1612 {
1613   Pool *pool = solv->pool;
1614   int i;
1615   Id why = r - solv->rules;
1616
1617   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1618     solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1619   if (solv->learntrules && why >= solv->learntrules)
1620     {
1621       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1622         if (solv->learnt_pool.elements[i] > 0)
1623           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
1624       return;
1625     }
1626   if (MAPTST(&solv->weakrulemap, why))
1627     if (!*lastweakp || why > *lastweakp)
1628       *lastweakp = why;
1629   /* do not add rpm rules to problem */
1630   if (why < solv->jobrules)
1631     return;
1632   /* turn rule into problem */
1633   if (why >= solv->jobrules && why < solv->updaterules)
1634     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1635   /* return if problem already countains our rule */
1636   if (solv->problems.count)
1637     {
1638       for (i = solv->problems.count - 1; i >= 0; i--)
1639         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1640           break;
1641         else if (solv->problems.elements[i] == why)
1642           return;
1643     }
1644   queue_push(&solv->problems, why);
1645 }
1646
1647
1648 /*
1649  * analyze_unsolvable
1650  *
1651  * return: 1 - disabled some rules, try again
1652  *         0 - hopeless
1653  */
1654
1655 static int
1656 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1657 {
1658   Pool *pool = solv->pool;
1659   Rule *r;
1660   Map seen;             /* global to speed things up? */
1661   Id v, vv, *dp, why;
1662   int l, i, idx;
1663   Id *decisionmap = solv->decisionmap;
1664   int oldproblemcount;
1665   int oldlearntpoolcount;
1666   Id lastweak;
1667
1668   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1669   oldproblemcount = solv->problems.count;
1670   oldlearntpoolcount = solv->learnt_pool.count;
1671
1672   /* make room for proof index */
1673   /* must update it later, as analyze_unsolvable_rule would confuse
1674    * it with a rule index if we put the real value in already */
1675   queue_push(&solv->problems, 0);
1676
1677   r = cr;
1678   map_init(&seen, pool->nsolvables);
1679   queue_push(&solv->learnt_pool, r - solv->rules);
1680   lastweak = 0;
1681   analyze_unsolvable_rule(solv, r, &lastweak);
1682   dp = r->d ? pool->whatprovidesdata + r->d : 0;
1683   for (i = -1; ; i++)
1684     {
1685       if (i == -1)
1686         v = r->p;
1687       else if (r->d == 0)
1688         v = i ? 0 : r->w2;
1689       else
1690         v = *dp++;
1691       if (v == 0)
1692         break;
1693       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1694           continue;
1695       vv = v > 0 ? v : -v;
1696       l = solv->decisionmap[vv];
1697       if (l < 0)
1698         l = -l;
1699       MAPSET(&seen, vv);
1700     }
1701   idx = solv->decisionq.count;
1702   while (idx > 0)
1703     {
1704       v = solv->decisionq.elements[--idx];
1705       vv = v > 0 ? v : -v;
1706       if (!MAPTST(&seen, vv))
1707         continue;
1708       why = solv->decisionq_why.elements[idx];
1709       queue_push(&solv->learnt_pool, why);
1710       r = solv->rules + why;
1711       analyze_unsolvable_rule(solv, r, &lastweak);
1712       dp = r->d ? pool->whatprovidesdata + r->d : 0;
1713       for (i = -1; ; i++)
1714         {
1715           if (i == -1)
1716             v = r->p;
1717           else if (r->d == 0)
1718             v = i ? 0 : r->w2;
1719           else
1720             v = *dp++;
1721           if (v == 0)
1722             break;
1723           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1724               continue;
1725           vv = v > 0 ? v : -v;
1726           l = solv->decisionmap[vv];
1727           if (l < 0)
1728             l = -l;
1729           MAPSET(&seen, vv);
1730         }
1731     }
1732   map_free(&seen);
1733   queue_push(&solv->problems, 0);       /* mark end of this problem */
1734
1735   if (lastweak)
1736     {
1737       /* disable last weak rule */
1738       solv->problems.count = oldproblemcount;
1739       solv->learnt_pool.count = oldlearntpoolcount;
1740       r = solv->rules + lastweak;
1741       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
1742       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1743       disablerule(solv, r);
1744       reset_solver(solv);
1745       return 1;
1746     }
1747
1748   /* finish proof */
1749   queue_push(&solv->learnt_pool, 0);
1750   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
1751
1752   if (disablerules)
1753     {
1754       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
1755         disableproblem(solv, solv->problems.elements[i]);
1756       /* XXX: might want to enable all weak rules again */
1757       reset_solver(solv);
1758       return 1;
1759     }
1760   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
1761   return 0;
1762 }
1763
1764
1765 /*-----------------------------------------------------------------*/
1766 /* Decision revert */
1767
1768 /*
1769  * revert
1770  * revert decision at level
1771  */
1772
1773 static void
1774 revert(Solver *solv, int level)
1775 {
1776   Pool *pool = solv->pool;
1777   Id v, vv;
1778   while (solv->decisionq.count)
1779     {
1780       v = solv->decisionq.elements[solv->decisionq.count - 1];
1781       vv = v > 0 ? v : -v;
1782       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
1783         break;
1784       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
1785       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
1786         solv->recommendations.count--;
1787       solv->decisionmap[vv] = 0;
1788       solv->decisionq.count--;
1789       solv->decisionq_why.count--;
1790       solv->propagate_index = solv->decisionq.count;
1791     }
1792   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
1793     {
1794       solv->branches.count--;
1795       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
1796         solv->branches.count--;
1797     }
1798   solv->recommends_index = -1;
1799 }
1800
1801
1802 /*
1803  * watch2onhighest - put watch2 on literal with highest level
1804  */
1805
1806 static inline void
1807 watch2onhighest(Solver *solv, Rule *r)
1808 {
1809   int l, wl = 0;
1810   Id v, *dp;
1811
1812   if (!r->d)
1813     return;     /* binary rule, both watches are set */
1814   dp = solv->pool->whatprovidesdata + r->d;
1815   while ((v = *dp++) != 0)
1816     {
1817       l = solv->decisionmap[v < 0 ? -v : v];
1818       if (l < 0)
1819         l = -l;
1820       if (l > wl)
1821         {
1822           r->w2 = dp[-1];
1823           wl = l;
1824         }
1825     }
1826 }
1827
1828
1829 /*
1830  * setpropagatelearn
1831  *
1832  * add free decision to decisionq, increase level and
1833  * propagate decision, return if no conflict.
1834  * in conflict case, analyze conflict rule, add resulting
1835  * rule to learnt rule set, make decision from learnt
1836  * rule (always unit) and re-propagate.
1837  *
1838  * returns the new solver level or 0 if unsolvable
1839  *
1840  */
1841
1842 static int
1843 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
1844 {
1845   Pool *pool = solv->pool;
1846   Rule *r;
1847   Id p = 0, d = 0;
1848   int l, why;
1849
1850   if (decision)
1851     {
1852       level++;
1853       if (decision > 0)
1854         solv->decisionmap[decision] = level;
1855       else
1856         solv->decisionmap[-decision] = -level;
1857       queue_push(&solv->decisionq, decision);
1858       queue_push(&solv->decisionq_why, 0);
1859     }
1860   for (;;)
1861     {
1862       r = propagate(solv, level);
1863       if (!r)
1864         break;
1865       if (level == 1)
1866         return analyze_unsolvable(solv, r, disablerules);
1867       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
1868       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
1869       assert(l > 0 && l < level);
1870       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
1871       level = l;
1872       revert(solv, level);
1873       r = addrule(solv, p, d);       /* p requires d */
1874       assert(r);
1875       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
1876       queue_push(&solv->learnt_why, why);
1877       if (d)
1878         {
1879           /* at least 2 literals, needs watches */
1880           watch2onhighest(solv, r);
1881           addwatches(solv, r);
1882         }
1883       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
1884       queue_push(&solv->decisionq, p);
1885       queue_push(&solv->decisionq_why, r - solv->rules);
1886       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1887         {
1888           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
1889           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
1890           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
1891           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
1892         }
1893     }
1894   return level;
1895 }
1896
1897
1898 /*
1899  * install best package from the queue. We add an extra package, inst, if
1900  * provided. See comment in weak install section.
1901  *
1902  * returns the new solver level or 0 if unsolvable
1903  *
1904  */
1905 static int
1906 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
1907 {
1908   Pool *pool = solv->pool;
1909   Id p;
1910   int i;
1911
1912   if (dq->count > 1 || inst)
1913     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
1914
1915   i = 0;
1916   if (dq->count > 1)
1917     {
1918       /* choose the supplemented one */
1919       for (i = 0; i < dq->count; i++)
1920         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
1921           break;
1922       if (i == dq->count)
1923         {
1924           for (i = 1; i < dq->count; i++)
1925             queue_push(&solv->branches, dq->elements[i]);
1926           queue_push(&solv->branches, -level);
1927           i = 0;
1928         }
1929     }
1930   p = dq->elements[i];
1931
1932   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
1933
1934   return setpropagatelearn(solv, level, p, disablerules);
1935 }
1936
1937
1938 /*-----------------------------------------------------------------*/
1939 /* Main solver interface */
1940
1941
1942 /*
1943  * solver_create
1944  * create solver structure
1945  *
1946  * pool: all available solvables
1947  * installed: installed Solvables
1948  *
1949  *
1950  * Upon solving, rules are created to flag the Solvables
1951  * of the 'installed' Repo as installed.
1952  */
1953
1954 Solver *
1955 solver_create(Pool *pool, Repo *installed)
1956 {
1957   Solver *solv;
1958   solv = (Solver *)sat_calloc(1, sizeof(Solver));
1959   solv->pool = pool;
1960   solv->installed = installed;
1961
1962   queue_init(&solv->ruletojob);
1963   queue_init(&solv->decisionq);
1964   queue_init(&solv->decisionq_why);
1965   queue_init(&solv->problems);
1966   queue_init(&solv->suggestions);
1967   queue_init(&solv->recommendations);
1968   queue_init(&solv->learnt_why);
1969   queue_init(&solv->learnt_pool);
1970   queue_init(&solv->branches);
1971   queue_init(&solv->covenantq);
1972   queue_init(&solv->weakruleq);
1973
1974   map_init(&solv->recommendsmap, pool->nsolvables);
1975   map_init(&solv->suggestsmap, pool->nsolvables);
1976   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
1977   solv->recommends_index = 0;
1978
1979   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
1980   solv->nrules = 1;
1981   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
1982   memset(solv->rules, 0, sizeof(Rule));
1983
1984   return solv;
1985 }
1986
1987
1988 /*
1989  * solver_free
1990  */
1991
1992 void
1993 solver_free(Solver *solv)
1994 {
1995   queue_free(&solv->ruletojob);
1996   queue_free(&solv->decisionq);
1997   queue_free(&solv->decisionq_why);
1998   queue_free(&solv->learnt_why);
1999   queue_free(&solv->learnt_pool);
2000   queue_free(&solv->problems);
2001   queue_free(&solv->suggestions);
2002   queue_free(&solv->recommendations);
2003   queue_free(&solv->branches);
2004   queue_free(&solv->covenantq);
2005   queue_free(&solv->weakruleq);
2006
2007   map_free(&solv->recommendsmap);
2008   map_free(&solv->suggestsmap);
2009   map_free(&solv->noupdate);
2010   map_free(&solv->weakrulemap);
2011
2012   sat_free(solv->decisionmap);
2013   sat_free(solv->rules);
2014   sat_free(solv->watches);
2015   sat_free(solv->obsoletes);
2016   sat_free(solv->obsoletes_data);
2017   sat_free(solv);
2018 }
2019
2020
2021 /*-------------------------------------------------------*/
2022
2023 /*
2024  * run_solver
2025  *
2026  * all rules have been set up, now actually run the solver
2027  *
2028  */
2029
2030 static void
2031 run_solver(Solver *solv, int disablerules, int doweak)
2032 {
2033   Queue dq;
2034   int systemlevel;
2035   int level, olevel;
2036   Rule *r;
2037   int i, j, n;
2038   Solvable *s;
2039   Pool *pool = solv->pool;
2040   Id p, *dp;
2041
2042   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2043     {
2044       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2045       for (i = 1; i < solv->nrules; i++)
2046         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2047     }
2048
2049   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2050
2051   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2052     solver_printdecisions(solv);
2053
2054   /* start SAT algorithm */
2055   level = 1;
2056   systemlevel = level + 1;
2057   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2058
2059   queue_init(&dq);
2060
2061   /*
2062    * here's the main loop:
2063    * 1) propagate new decisions (only needed for level 1)
2064    * 2) try to keep installed packages
2065    * 3) fulfill all unresolved rules
2066    * 4) install recommended packages
2067    * 5) minimalize solution if we had choices
2068    * if we encounter a problem, we rewind to a safe level and restart
2069    * with step 1
2070    */
2071
2072   for (;;)
2073     {
2074       /*
2075        * propagate
2076        */
2077
2078       if (level == 1)
2079         {
2080           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2081           if ((r = propagate(solv, level)) != 0)
2082             {
2083               if (analyze_unsolvable(solv, r, disablerules))
2084                 continue;
2085               queue_free(&dq);
2086               return;
2087             }
2088         }
2089
2090       /*
2091        * installed packages
2092        */
2093
2094       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2095         {
2096           if (!solv->updatesystem)
2097             {
2098               /* try to keep as many packages as possible */
2099               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2100               for (i = solv->installed->start; i < solv->installed->end; i++)
2101                 {
2102                   s = pool->solvables + i;
2103                   if (s->repo != solv->installed)
2104                     continue;
2105                   if (solv->decisionmap[i] != 0)
2106                     continue;
2107                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2108                   olevel = level;
2109                   level = setpropagatelearn(solv, level, i, disablerules);
2110                   if (level == 0)
2111                     {
2112                       queue_free(&dq);
2113                       return;
2114                     }
2115                   if (level <= olevel)
2116                     break;
2117                 }
2118               if (i < solv->installed->end)
2119                 continue;
2120             }
2121           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2122           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2123             {
2124               Rule *rr;
2125               s = pool->solvables + i;
2126               if (s->repo != solv->installed)
2127                 continue;
2128               if (solv->decisionmap[i] > 0)
2129                 continue;
2130               /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2131               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2132                 continue;
2133               queue_empty(&dq);
2134               if (!solv->allowuninstall)
2135                 {
2136                   rr = r;
2137                   if (!rr->w1)
2138                     rr += solv->installed->end - solv->installed->start;
2139                 }
2140               else
2141                 rr = solv->rules + solv->featurerules + (i - solv->installed->start);
2142               if (rr->d == 0)
2143                 {
2144                   if (!rr->w2 || solv->decisionmap[rr->w2] > 0)
2145                     continue;
2146                   if (solv->decisionmap[rr->w2] == 0)
2147                     queue_push(&dq, rr->w2);
2148                 }
2149               else
2150                 {
2151                   dp = pool->whatprovidesdata + rr->d;
2152                   while ((p = *dp++) != 0)
2153                     {
2154                       if (solv->decisionmap[p] > 0)
2155                         break;
2156                       if (solv->decisionmap[p] == 0)
2157                         queue_push(&dq, p);
2158                     }
2159                   if (p)
2160                     continue;
2161                 }
2162               if (!dq.count && solv->decisionmap[i] != 0)
2163                 continue;
2164               olevel = level;
2165               /* FIXME: i is handled a bit different because we do not want
2166                * to have it pruned just because it is not recommened.
2167                * we should not prune installed packages instead */
2168               level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2169               if (level == 0)
2170                 {
2171                   queue_free(&dq);
2172                   return;
2173                 }
2174               if (level <= olevel)
2175                 break;
2176             }
2177           if (i < solv->installed->end)
2178             continue;
2179           systemlevel = level;
2180         }
2181
2182       /*
2183        * decide
2184        */
2185
2186       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2187       for (i = 1, n = 1; ; i++, n++)
2188         {
2189           if (n == solv->nrules)
2190             break;
2191           if (i == solv->nrules)
2192             i = 1;
2193           r = solv->rules + i;
2194           if (!r->w1)   /* ignore disabled rules */
2195             continue;
2196           queue_empty(&dq);
2197           if (r->d == 0)
2198             {
2199               /* binary or unary rule */
2200               /* need two positive undecided literals */
2201               if (r->p < 0 || r->w2 <= 0)
2202                 continue;
2203               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2204                 continue;
2205               queue_push(&dq, r->p);
2206               queue_push(&dq, r->w2);
2207             }
2208           else
2209             {
2210               /* make sure that
2211                * all negative literals are installed
2212                * no positive literal is installed
2213                * i.e. the rule is not fulfilled and we
2214                * just need to decide on the positive literals
2215                */
2216               if (r->p < 0)
2217                 {
2218                   if (solv->decisionmap[-r->p] <= 0)
2219                     continue;
2220                 }
2221               else
2222                 {
2223                   if (solv->decisionmap[r->p] > 0)
2224                     continue;
2225                   if (solv->decisionmap[r->p] == 0)
2226                     queue_push(&dq, r->p);
2227                 }
2228               dp = pool->whatprovidesdata + r->d;
2229               while ((p = *dp++) != 0)
2230                 {
2231                   if (p < 0)
2232                     {
2233                       if (solv->decisionmap[-p] <= 0)
2234                         break;
2235                     }
2236                   else
2237                     {
2238                       if (solv->decisionmap[p] > 0)
2239                         break;
2240                       if (solv->decisionmap[p] == 0)
2241                         queue_push(&dq, p);
2242                     }
2243                 }
2244               if (p)
2245                 continue;
2246             }
2247           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2248             {
2249               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2250               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2251             }
2252           /* dq.count < 2 cannot happen as this means that
2253            * the rule is unit */
2254           assert(dq.count > 1);
2255
2256           olevel = level;
2257           level = selectandinstall(solv, level, &dq, 0, disablerules);
2258           if (level == 0)
2259             {
2260               queue_free(&dq);
2261               return;
2262             }
2263           if (level < systemlevel)
2264             break;
2265           n = 0;
2266         } /* for(), decide */
2267
2268       if (n != solv->nrules)    /* continue if level < systemlevel */
2269         continue;
2270
2271       if (doweak)
2272         {
2273           int qcount;
2274
2275           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2276           queue_empty(&dq);
2277           for (i = 1; i < pool->nsolvables; i++)
2278             {
2279               if (solv->decisionmap[i] < 0)
2280                 continue;
2281               if (solv->decisionmap[i] > 0)
2282                 {
2283                   Id *recp, rec, *pp, p;
2284                   s = pool->solvables + i;
2285                   /* installed, check for recommends */
2286                   /* XXX need to special case AND ? */
2287                   if (s->recommends)
2288                     {
2289                       recp = s->repo->idarraydata + s->recommends;
2290                       while ((rec = *recp++) != 0)
2291                         {
2292                           qcount = dq.count;
2293                           FOR_PROVIDES(p, pp, rec)
2294                             {
2295                               if (solv->decisionmap[p] > 0)
2296                                 {
2297                                   dq.count = qcount;
2298                                   break;
2299                                 }
2300                               else if (solv->decisionmap[p] == 0)
2301                                 {
2302                                   queue_pushunique(&dq, p);
2303                                 }
2304                             }
2305                         }
2306                     }
2307                 }
2308               else
2309                 {
2310                   s = pool->solvables + i;
2311                   if (!s->supplements && !s->freshens)
2312                     continue;
2313                   if (!pool_installable(pool, s))
2314                     continue;
2315                   if (solver_is_supplementing(solv, s))
2316                     queue_pushunique(&dq, i);
2317                 }
2318             }
2319           if (dq.count)
2320             {
2321               if (dq.count > 1)
2322                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2323               p = dq.elements[0];
2324               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2325               queue_push(&solv->recommendations, p);
2326               level = setpropagatelearn(solv, level, p, 0);
2327               continue;
2328             }
2329         }
2330
2331      if (solv->solution_callback)
2332         {
2333           solv->solution_callback(solv, solv->solution_callback_data);
2334           if (solv->branches.count)
2335             {
2336               int i = solv->branches.count - 1;
2337               int l = -solv->branches.elements[i];
2338               for (; i > 0; i--)
2339                 if (solv->branches.elements[i - 1] < 0)
2340                   break;
2341               p = solv->branches.elements[i];
2342               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2343               queue_empty(&dq);
2344               for (j = i + 1; j < solv->branches.count; j++)
2345                 queue_push(&dq, solv->branches.elements[j]);
2346               solv->branches.count = i;
2347               level = l;
2348               revert(solv, level);
2349               if (dq.count > 1)
2350                 for (j = 0; j < dq.count; j++)
2351                   queue_push(&solv->branches, dq.elements[j]);
2352               olevel = level;
2353               level = setpropagatelearn(solv, level, p, disablerules);
2354               if (level == 0)
2355                 {
2356                   queue_free(&dq);
2357                   return;
2358                 }
2359               continue;
2360             }
2361           /* all branches done, we're finally finished */
2362           break;
2363         }
2364
2365       /* minimization step */
2366      if (solv->branches.count)
2367         {
2368           int l = 0, lasti = -1, lastl = -1;
2369           p = 0;
2370           for (i = solv->branches.count - 1; i >= 0; i--)
2371             {
2372               p = solv->branches.elements[i];
2373               if (p < 0)
2374                 l = -p;
2375               else if (p > 0 && solv->decisionmap[p] > l + 1)
2376                 {
2377                   lasti = i;
2378                   lastl = l;
2379                 }
2380             }
2381           if (lasti >= 0)
2382             {
2383               /* kill old solvable so that we do not loop */
2384               p = solv->branches.elements[lasti];
2385               solv->branches.elements[lasti] = 0;
2386               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2387
2388               level = lastl;
2389               revert(solv, level);
2390               olevel = level;
2391               level = setpropagatelearn(solv, level, p, disablerules);
2392               if (level == 0)
2393                 {
2394                   queue_free(&dq);
2395                   return;
2396                 }
2397               continue;
2398             }
2399         }
2400       break;
2401     }
2402   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2403   queue_free(&dq);
2404 }
2405
2406
2407 /*
2408  * refine_suggestion
2409  * at this point, all rules that led to conflicts are disabled.
2410  * we re-enable all rules of a problem set but rule "sug", then
2411  * continue to disable more rules until there as again a solution.
2412  */
2413
2414 /* FIXME: think about conflicting assertions */
2415
2416 static void
2417 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2418 {
2419   Pool *pool = solv->pool;
2420   int i, j;
2421   Id v;
2422   Queue disabled;
2423   int disabledcnt;
2424
2425   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2426     {
2427       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2428       for (i = 0; problem[i]; i++)
2429         {
2430           if (problem[i] == sug)
2431             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2432           solver_printproblem(solv, problem[i]);
2433         }
2434     }
2435   queue_init(&disabled);
2436   queue_empty(refined);
2437   queue_push(refined, sug);
2438
2439   /* re-enable all problem rules with the exception of "sug"(gestion) */
2440   revert(solv, 1);
2441   reset_solver(solv);
2442
2443   for (i = 0; problem[i]; i++)
2444     if (problem[i] != sug)
2445       enableproblem(solv, problem[i]);
2446
2447   if (sug < 0)
2448     disableupdaterules(solv, job, -(sug + 1));
2449
2450   for (;;)
2451     {
2452       int njob, nfeature, nupdate;
2453       queue_empty(&solv->problems);
2454       enableweakrules(solv);
2455       revert(solv, 1);          /* XXX no longer needed? */
2456       reset_solver(solv);
2457
2458       if (!solv->problems.count)
2459         run_solver(solv, 0, 0);
2460
2461       if (!solv->problems.count)
2462         {
2463           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2464           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2465             solver_printdecisions(solv);
2466           break;                /* great, no more problems */
2467         }
2468       disabledcnt = disabled.count;
2469       /* start with 1 to skip over proof index */
2470       njob = nfeature = nupdate = 0;
2471       for (i = 1; i < solv->problems.count - 1; i++)
2472         {
2473           /* ignore solutions in refined */
2474           v = solv->problems.elements[i];
2475           if (v == 0)
2476             break;      /* end of problem reached */
2477           for (j = 0; problem[j]; j++)
2478             if (problem[j] != sug && problem[j] == v)
2479               break;
2480           if (problem[j])
2481             continue;
2482           if (v >= solv->featurerules && v < solv->learntrules)
2483             nfeature++;
2484           else if (v > 0)
2485             nupdate++;
2486           else
2487             njob++;
2488           queue_push(&disabled, v);
2489         }
2490       if (disabled.count == disabledcnt)
2491         {
2492           /* no solution found, this was an invalid suggestion! */
2493           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2494           refined->count = 0;
2495           break;
2496         }
2497       if (!njob && nupdate && nfeature)
2498         {
2499           /* got only update rules, filter out feature rules */
2500           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
2501           for (i = j = disabledcnt; i < disabled.count; i++)
2502             {
2503               v = disabled.elements[i];
2504               if (v < solv->featurerules || v >= solv->learntrules)
2505                 disabled.elements[j++] = v;
2506             }
2507           disabled.count = j;
2508           nfeature = 0;
2509         }
2510       if (disabled.count == disabledcnt + 1)
2511         {
2512           /* just one suggestion, add it to refined list */
2513           v = disabled.elements[disabledcnt];
2514           if (!nfeature)
2515             queue_push(refined, v);     /* do not record feature rules */
2516           disableproblem(solv, v);
2517           if (v >= solv->updaterules && v < solv->featurerules)
2518             {
2519               Rule *r = solv->rules + v + (solv->installed->end - solv->installed->start);
2520               if (r->p)
2521                 enablerule(solv, r);    /* enable corresponding feature rule */
2522             }
2523           if (v < 0)
2524             disableupdaterules(solv, job, -(v + 1));
2525         }
2526       else
2527         {
2528           /* more than one solution, disable all */
2529           /* do not push anything on refine list, as we do not know which solution to choose */
2530           /* thus, the user will get another problem if he selects this solution, where he
2531            * can choose the right one */
2532           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2533             {
2534               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2535               for (i = disabledcnt; i < disabled.count; i++)
2536                 solver_printproblem(solv, disabled.elements[i]);
2537             }
2538           for (i = disabledcnt; i < disabled.count; i++)
2539             {
2540               v = disabled.elements[i];
2541               disableproblem(solv, v);
2542               if (v >= solv->updaterules && v < solv->featurerules)
2543                 {
2544                   Rule *r = solv->rules + v + (solv->installed->end - solv->installed->start);
2545                   if (r->p)
2546                     enablerule(solv, r);
2547                 }
2548             }
2549         }
2550     }
2551   /* all done, get us back into the same state as before */
2552   /* enable refined rules again */
2553   for (i = 0; i < disabled.count; i++)
2554     enableproblem(solv, disabled.elements[i]);
2555   /* disable problem rules again */
2556   for (i = 0; problem[i]; i++)
2557     disableproblem(solv, problem[i]);
2558   disableupdaterules(solv, job, -1);
2559   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2560 }
2561
2562 static void
2563 problems_to_solutions(Solver *solv, Queue *job)
2564 {
2565   Pool *pool = solv->pool;
2566   Queue problems;
2567   Queue solution;
2568   Queue solutions;
2569   Id *problem;
2570   Id why;
2571   int i, j;
2572
2573   if (!solv->problems.count)
2574     return;
2575   queue_clone(&problems, &solv->problems);
2576   queue_init(&solution);
2577   queue_init(&solutions);
2578   /* copy over proof index */
2579   queue_push(&solutions, problems.elements[0]);
2580   problem = problems.elements + 1;
2581   for (i = 1; i < problems.count; i++)
2582     {
2583       Id v = problems.elements[i];
2584       if (v == 0)
2585         {
2586           /* mark end of this problem */
2587           queue_push(&solutions, 0);
2588           queue_push(&solutions, 0);
2589           if (i + 1 == problems.count)
2590             break;
2591           /* copy over proof of next problem */
2592           queue_push(&solutions, problems.elements[i + 1]);
2593           i++;
2594           problem = problems.elements + i + 1;
2595           continue;
2596         }
2597       refine_suggestion(solv, job, problem, v, &solution);
2598       if (!solution.count)
2599         continue;       /* this solution didn't work out */
2600
2601       for (j = 0; j < solution.count; j++)
2602         {
2603           why = solution.elements[j];
2604           /* must be either job descriptor or update rule */
2605           assert(why < 0 || (why >= solv->updaterules && why < solv->featurerules));
2606 #if 0
2607           solver_printproblem(solv, why);
2608 #endif
2609           if (why < 0)
2610             {
2611               /* job descriptor */
2612               queue_push(&solutions, 0);
2613               queue_push(&solutions, -why);
2614             }
2615           else
2616             {
2617               /* update rule, find replacement package */
2618               Id p, rp = 0;
2619               Rule *rr;
2620               p = solv->installed->start + (why - solv->updaterules);
2621               if (solv->decisionmap[p] > 0)
2622                 continue;       /* false alarm, turned out we can keep the package */
2623               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
2624               if (!rr->p)
2625                 rr = solv->rules + why;
2626               if (rr->w2)
2627                 {
2628                   if (!rr->d)
2629                     {
2630                       if (solv->decisionmap[rr->w2] > 0 && pool->solvables[rr->w2].repo != solv->installed)
2631                         rp = rr->w2;
2632                     }
2633                   else
2634                     {
2635                       Id *dp = pool->whatprovidesdata + rr->d;
2636                       for (; *dp; dp++)
2637                         {
2638                           if (solv->decisionmap[*dp] > 0 && pool->solvables[*dp].repo != solv->installed)
2639                             {
2640                               rp = *dp;
2641                               break;
2642                             }
2643                         }
2644                     }
2645                 }
2646               queue_push(&solutions, p);
2647               queue_push(&solutions, rp);
2648             }
2649         }
2650       /* mark end of this solution */
2651       queue_push(&solutions, 0);
2652       queue_push(&solutions, 0);
2653     }
2654   queue_free(&solution);
2655   queue_free(&problems);
2656   /* copy queue over to solutions */
2657   queue_free(&solv->problems);
2658   queue_clone(&solv->problems, &solutions);
2659
2660   /* bring solver back into problem state */
2661   revert(solv, 1);              /* XXX move to reset_solver? */
2662   reset_solver(solv);
2663
2664   assert(solv->problems.count == solutions.count);
2665   queue_free(&solutions);
2666 }
2667
2668 Id
2669 solver_next_problem(Solver *solv, Id problem)
2670 {
2671   Id *pp;
2672   if (problem == 0)
2673     return solv->problems.count ? 1 : 0;
2674   pp = solv->problems.elements + problem;
2675   while (pp[0] || pp[1])
2676     {
2677       /* solution */
2678       pp += 2;
2679       while (pp[0] || pp[1])
2680         pp += 2;
2681       pp += 2;
2682     }
2683   pp += 2;
2684   problem = pp - solv->problems.elements;
2685   if (problem >= solv->problems.count)
2686     return 0;
2687   return problem + 1;
2688 }
2689
2690 Id
2691 solver_next_solution(Solver *solv, Id problem, Id solution)
2692 {
2693   Id *pp;
2694   if (solution == 0)
2695     {
2696       solution = problem;
2697       pp = solv->problems.elements + solution;
2698       return pp[0] || pp[1] ? solution : 0;
2699     }
2700   pp = solv->problems.elements + solution;
2701   while (pp[0] || pp[1])
2702     pp += 2;
2703   pp += 2;
2704   solution = pp - solv->problems.elements;
2705   return pp[0] || pp[1] ? solution : 0;
2706 }
2707
2708 Id
2709 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
2710 {
2711   Id *pp;
2712   element = element ? element + 2 : solution;
2713   pp = solv->problems.elements + element;
2714   if (!(pp[0] || pp[1]))
2715     return 0;
2716   *p = pp[0];
2717   *rp = pp[1];
2718   return element;
2719 }
2720
2721
2722 /* this is basically the reverse of addrpmrulesforsolvable */
2723 SolverProbleminfo
2724 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
2725 {
2726   Pool *pool = solv->pool;
2727   Repo *installed = solv->installed;
2728   Rule *r;
2729   Solvable *s;
2730   int dontfix = 0;
2731   Id p, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
2732
2733   assert(rid > 0);
2734   if (rid >= solv->updaterules)
2735     {
2736       *depp = 0;
2737       *sourcep = solv->installed->start + (rid - solv->updaterules);
2738       *targetp = 0;
2739       return SOLVER_PROBLEM_UPDATE_RULE;
2740     }
2741   if (rid >= solv->jobrules)
2742     {
2743
2744       r = solv->rules + rid;
2745       p = solv->ruletojob.elements[rid - solv->jobrules];
2746       *depp = job->elements[p + 1];
2747       *sourcep = p;
2748       *targetp = job->elements[p];
2749       if (r->d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && job->elements[p] != SOLVER_INSTALL_SOLVABLE_ONE_OF)
2750         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
2751       return SOLVER_PROBLEM_JOB_RULE;
2752     }
2753   r = solv->rules + rid;
2754   assert(r->p < 0);
2755   if (r->d == 0 && r->w2 == 0)
2756     {
2757       /* a rpm rule assertion */
2758       s = pool->solvables - r->p;
2759       if (installed && !solv->fixsystem && s->repo == installed)
2760         dontfix = 1;
2761       assert(!dontfix); /* dontfix packages never have a neg assertion */
2762       *sourcep = -r->p;
2763       *targetp = 0;
2764       /* see why the package is not installable */
2765       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
2766         {
2767           *depp = 0;
2768           return SOLVER_PROBLEM_NOT_INSTALLABLE;
2769         }
2770       /* check requires */
2771       if (s->requires)
2772         {
2773           reqp = s->repo->idarraydata + s->requires;
2774           while ((req = *reqp++) != 0)
2775             {
2776               if (req == SOLVABLE_PREREQMARKER)
2777                 continue;
2778               dp = pool_whatprovides(pool, req);
2779               if (*dp == 0)
2780                 break;
2781             }
2782           if (req)
2783             {
2784               *depp = req;
2785               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
2786             }
2787         }
2788       assert(!solv->allowselfconflicts);
2789       assert(s->conflicts);
2790       conp = s->repo->idarraydata + s->conflicts;
2791       while ((con = *conp++) != 0)
2792         FOR_PROVIDES(p, pp, con)
2793           if (p == -r->p)
2794             {
2795               *depp = con;
2796               return SOLVER_PROBLEM_SELF_CONFLICT;
2797             }
2798       assert(0);
2799     }
2800   s = pool->solvables - r->p;
2801   if (installed && !solv->fixsystem && s->repo == installed)
2802     dontfix = 1;
2803   if (r->d == 0 && r->w2 < 0)
2804     {
2805       /* a package conflict */
2806       Solvable *s2 = pool->solvables - r->w2;
2807       int dontfix2 = 0;
2808
2809       if (installed && !solv->fixsystem && s2->repo == installed)
2810         dontfix2 = 1;
2811
2812       /* if both packages have the same name and at least one of them
2813        * is not installed, they conflict */
2814       if (s->name == s2->name && (!installed || (s->repo != installed || s2->repo != installed)))
2815         {
2816           *depp = 0;
2817           *sourcep = -r->p;
2818           *targetp = -r->w2;
2819           return SOLVER_PROBLEM_SAME_NAME;
2820         }
2821
2822       /* check conflicts in both directions */
2823       if (s->conflicts)
2824         {
2825           conp = s->repo->idarraydata + s->conflicts;
2826           while ((con = *conp++) != 0)
2827             {
2828               FOR_PROVIDES(p, pp, con)
2829                 {
2830                   if (dontfix && pool->solvables[p].repo == installed)
2831                     continue;
2832                   if (p != -r->w2)
2833                     continue;
2834                   *depp = con;
2835                   *sourcep = -r->p;
2836                   *targetp = p;
2837                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
2838                 }
2839             }
2840         }
2841       if (s2->conflicts)
2842         {
2843           conp = s2->repo->idarraydata + s2->conflicts;
2844           while ((con = *conp++) != 0)
2845             {
2846               FOR_PROVIDES(p, pp, con)
2847                 {
2848                   if (dontfix2 && pool->solvables[p].repo == installed)
2849                     continue;
2850                   if (p != -r->p)
2851                     continue;
2852                   *depp = con;
2853                   *sourcep = -r->w2;
2854                   *targetp = p;
2855                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
2856                 }
2857             }
2858         }
2859       /* check obsoletes in both directions */
2860       if ((!installed || s->repo != installed) && s->obsoletes)
2861         {
2862           obsp = s->repo->idarraydata + s->obsoletes;
2863           while ((obs = *obsp++) != 0)
2864             {
2865               FOR_PROVIDES(p, pp, obs)
2866                 {
2867                   if (p != -r->w2)
2868                     continue;
2869                   *depp = obs;
2870                   *sourcep = -r->p;
2871                   *targetp = p;
2872                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
2873                 }
2874             }
2875         }
2876       if ((!installed || s2->repo != installed) && s2->obsoletes)
2877         {
2878           obsp = s2->repo->idarraydata + s2->obsoletes;
2879           while ((obs = *obsp++) != 0)
2880             {
2881               FOR_PROVIDES(p, pp, obs)
2882                 {
2883                   if (p != -r->p)
2884                     continue;
2885                   *depp = obs;
2886                   *sourcep = -r->w2;
2887                   *targetp = p;
2888                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
2889                 }
2890             }
2891         }
2892       /* all cases checked, can't happen */
2893       assert(0);
2894     }
2895   /* simple requires */
2896   assert(s->requires);
2897   reqp = s->repo->idarraydata + s->requires;
2898   while ((req = *reqp++) != 0)
2899     {
2900       if (req == SOLVABLE_PREREQMARKER)
2901         continue;
2902       dp = pool_whatprovides(pool, req);
2903       if (r->d == 0)
2904         {
2905           if (*dp == r->w2 && dp[1] == 0)
2906             break;
2907         }
2908       else if (dp - pool->whatprovidesdata == r->d)
2909         break;
2910     }
2911   assert(req);
2912   *depp = req;
2913   *sourcep = -r->p;
2914   *targetp = 0;
2915   return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
2916 }
2917
2918 static void
2919 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
2920 {
2921   Id rid;
2922   Id lreqr, lconr, lsysr, ljobr;
2923   Rule *r;
2924   int reqassert = 0;
2925
2926   lreqr = lconr = lsysr = ljobr = 0;
2927   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
2928     {
2929       assert(rid > 0);
2930       if (rid >= solv->learntrules)
2931         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
2932       else if (rid >= solv->updaterules)
2933         {
2934           if (!*sysrp)
2935             *sysrp = rid;
2936         }
2937       else if (rid >= solv->jobrules)
2938         {
2939           if (!*jobrp)
2940             *jobrp = rid;
2941         }
2942       else
2943         {
2944           r = solv->rules + rid;
2945           if (!r->d && r->w2 < 0)
2946             {
2947               if (!*conrp)
2948                 *conrp = rid;
2949             }
2950           else
2951             {
2952               if (r->d == 0 && r->w2 == 0 && !reqassert)
2953                 {
2954                   /* prefer assertions (XXX: bad idea?) */
2955                   *reqrp = rid;
2956                   reqassert = 1;
2957                 }
2958               if (!*reqrp)
2959                 *reqrp = rid;
2960               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
2961                 {
2962                   /* prefer rules of installed packages */
2963                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
2964                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
2965                     *reqrp = rid;
2966                 }
2967             }
2968         }
2969     }
2970   if (!*reqrp && lreqr)
2971     *reqrp = lreqr;
2972   if (!*conrp && lconr)
2973     *conrp = lconr;
2974   if (!*jobrp && ljobr)
2975     *jobrp = ljobr;
2976   if (!*sysrp && lsysr)
2977     *sysrp = lsysr;
2978 }
2979
2980 /*
2981  * search for a rule that describes the problem to the
2982  * user. A pretty hopeless task, actually. We currently
2983  * prefer simple requires.
2984  */
2985 Id
2986 solver_findproblemrule(Solver *solv, Id problem)
2987 {
2988   Id reqr, conr, sysr, jobr;
2989   Id idx = solv->problems.elements[problem - 1];
2990   reqr = conr = sysr = jobr = 0;
2991   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
2992   if (reqr)
2993     return reqr;
2994   if (conr)
2995     return conr;
2996   if (sysr)
2997     return sysr;
2998   if (jobr)
2999     return jobr;
3000   assert(0);
3001 }
3002
3003
3004 /* create reverse obsoletes map for installed solvables
3005  *
3006  * for each installed solvable find which packages with *different* names
3007  * obsolete the solvable.
3008  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3009  */
3010
3011 static void
3012 create_obsolete_index(Solver *solv)
3013 {
3014   Pool *pool = solv->pool;
3015   Solvable *s;
3016   Repo *installed = solv->installed;
3017   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3018   int i, n;
3019
3020   if (!installed || !installed->nsolvables)
3021     return;
3022   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3023   for (i = 1; i < pool->nsolvables; i++)
3024     {
3025       s = pool->solvables + i;
3026       if (s->repo == installed)
3027         continue;
3028       if (!s->obsoletes)
3029         continue;
3030       if (!pool_installable(pool, s))
3031         continue;
3032       obsp = s->repo->idarraydata + s->obsoletes;
3033       while ((obs = *obsp++) != 0)
3034         FOR_PROVIDES(p, pp, obs)
3035           {
3036             if (pool->solvables[p].repo != installed)
3037               continue;
3038             if (pool->solvables[p].name == s->name)
3039               continue;
3040             obsoletes[p - installed->start]++;
3041           }
3042     }
3043   n = 0;
3044   for (i = 0; i < installed->nsolvables; i++)
3045     if (obsoletes[i])
3046       {
3047         n += obsoletes[i] + 1;
3048         obsoletes[i] = n;
3049       }
3050   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3051   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3052   for (i = pool->nsolvables - 1; i > 0; i--)
3053     {
3054       s = pool->solvables + i;
3055       if (s->repo == installed)
3056         continue;
3057       if (!s->obsoletes)
3058         continue;
3059       if (!pool_installable(pool, s))
3060         continue;
3061       obsp = s->repo->idarraydata + s->obsoletes;
3062       while ((obs = *obsp++) != 0)
3063         FOR_PROVIDES(p, pp, obs)
3064           {
3065             if (pool->solvables[p].repo != installed)
3066               continue;
3067             if (pool->solvables[p].name == s->name)
3068               continue;
3069             p -= installed->start;
3070             if (obsoletes_data[obsoletes[p]] != i)
3071               obsoletes_data[--obsoletes[p]] = i;
3072           }
3073     }
3074 }
3075
3076 static void
3077 removedisabledconflicts(Solver *solv, Queue *removed)
3078 {
3079   Pool *pool = solv->pool;
3080   int i, n;
3081   Id p, why, *dp;
3082   Id new;
3083   Rule *r;
3084   Id *decisionmap = solv->decisionmap;
3085
3086   POOL_DEBUG(SAT_DEBUG_STATS, "removedisabledconflicts\n");
3087   queue_empty(removed);
3088   for (i = 0; i < solv->decisionq.count; i++)
3089     {
3090       p = solv->decisionq.elements[i];
3091       if (p > 0)
3092         continue;
3093       /* a conflict. we never do conflicts on free decisions, so there
3094        * must have been an unit rule */
3095       why = solv->decisionq_why.elements[i];
3096       assert(why > 0);
3097       r = solv->rules + why;
3098       if (!r->w1 && decisionmap[-p])
3099         {
3100           /* rule is now disabled, remove from decisionmap */
3101           POOL_DEBUG(SAT_DEBUG_STATS, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3102           queue_push(removed, -p);
3103           queue_push(removed, decisionmap[-p]);
3104           decisionmap[-p] = 0;
3105         }
3106     }
3107   if (!removed->count)
3108     return;
3109   /* we removed some confliced packages. some of them might still
3110    * be in conflict, so search for unit rules and re-conflict */
3111   new = 0;
3112   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3113     {
3114       if (i == solv->nrules)
3115         {
3116           i = 1;
3117           r = solv->rules + i;
3118         }
3119       if (!r->w1)
3120         continue;
3121       if (!r->w2)
3122         {
3123           if (r->p < 0 && !decisionmap[-r->p])
3124             new = r->p;
3125         }
3126       else if (!r->d)
3127         {
3128           /* binary rule */
3129           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3130             new = r->p;
3131           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3132             new = r->w2;
3133         }
3134       else
3135         {
3136           if (r->p < 0 && decisionmap[-r->p] == 0)
3137             new = r->p;
3138           if (new || DECISIONMAP_FALSE(r->p))
3139             {
3140               dp = pool->whatprovidesdata + r->d;
3141               while ((p = *dp++) != 0)
3142                 {
3143                   if (new && p == new)
3144                     continue;
3145                   if (p < 0 && decisionmap[-p] == 0)
3146                     {
3147                       if (new)
3148                         {
3149                           new = 0;
3150                           break;
3151                         }
3152                       new = p;
3153                     }
3154                   else if (!DECISIONMAP_FALSE(p))
3155                     {
3156                       new = 0;
3157                       break;
3158                     }
3159                 }
3160             }
3161         }
3162       if (new)
3163         {
3164           POOL_DEBUG(SAT_DEBUG_STATS, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
3165           decisionmap[-new] = -1;
3166           new = 0;
3167           n = 0;        /* redo all rules */
3168         }
3169     }
3170 }
3171
3172 static void
3173 weaken_solvable_deps(Solver *solv, Id p)
3174 {
3175   int i;
3176   Rule *r;
3177
3178   for (i = 1, r = solv->rules + i; i < solv->jobrules; i++, r++)
3179     {
3180       if (r->p != -p)
3181         continue;
3182       if (r->d == 0 && r->w2 < 0)
3183         continue;       /* conflict */
3184       queue_push(&solv->weakruleq, i);
3185     }
3186 }
3187
3188 /*-----------------------------------------------------------------*/
3189 /* main() */
3190
3191 /*
3192  *
3193  * solve job queue
3194  *
3195  */
3196
3197 void
3198 solver_solve(Solver *solv, Queue *job)
3199 {
3200   Pool *pool = solv->pool;
3201   Repo *installed = solv->installed;
3202   int i;
3203   int oldnrules;
3204   Map addedmap;                /* '1' == have rpm-rules for solvable */
3205   Id how, what, weak, name, p, *pp, d;
3206   Queue q, redoq;
3207   Solvable *s;
3208   int goterase;
3209   Rule *r;
3210
3211   /* create whatprovides if not already there */
3212   if (!pool->whatprovides)
3213     pool_createwhatprovides(pool);
3214
3215   /* create obsolete index if needed */
3216   if (solv->noupdateprovide)
3217     create_obsolete_index(solv);
3218
3219   /*
3220    * create basic rule set of all involved packages
3221    * use addedmap bitmap to make sure we don't create rules twice
3222    *
3223    */
3224
3225   map_init(&addedmap, pool->nsolvables);
3226   queue_init(&q);
3227
3228   /*
3229    * always install our system solvable
3230    */
3231   MAPSET(&addedmap, SYSTEMSOLVABLE);
3232   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3233   queue_push(&solv->decisionq_why, 0);
3234   solv->decisionmap[SYSTEMSOLVABLE] = 1;
3235
3236   /*
3237    * create rules for all package that could be involved with the solving
3238    * so called: rpm rules
3239    *
3240    */
3241   if (installed)
3242     {
3243       oldnrules = solv->nrules;
3244       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3245       FOR_REPO_SOLVABLES(installed, p, s)
3246         addrpmrulesforsolvable(solv, s, &addedmap);
3247       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3248       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3249       oldnrules = solv->nrules;
3250       FOR_REPO_SOLVABLES(installed, p, s)
3251         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3252       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3253     }
3254
3255   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3256   oldnrules = solv->nrules;
3257   for (i = 0; i < job->count; i += 2)
3258     {
3259       how = job->elements[i] & ~SOLVER_WEAK;
3260       what = job->elements[i + 1];
3261
3262       switch(how)
3263         {
3264         case SOLVER_INSTALL_SOLVABLE:
3265           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3266           break;
3267         case SOLVER_INSTALL_SOLVABLE_NAME:
3268         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3269           name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3270           while (ISRELDEP(name))
3271             {
3272               Reldep *rd = GETRELDEP(pool, name);
3273               name = rd->name;
3274             }
3275           FOR_PROVIDES(p, pp, what)
3276             {
3277               /* if by name, ensure that the name matches */
3278               if (name && pool->solvables[p].name != name)
3279                 continue;
3280               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3281             }
3282           break;
3283         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3284           /* dont allow downgrade */
3285           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3286           break;
3287         case SOLVER_INSTALL_SOLVABLE_ONE_OF:
3288           pp = pool->whatprovidesdata + what;
3289           while ((p = *pp++) != 0)
3290             addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3291           break;
3292         }
3293     }
3294   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3295
3296   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3297
3298   oldnrules = solv->nrules;
3299   addrpmrulesforweak(solv, &addedmap);
3300   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3301
3302   IF_POOLDEBUG (SAT_DEBUG_STATS)
3303     {
3304       int possible = 0, installable = 0;
3305       for (i = 1; i < pool->nsolvables; i++)
3306         {
3307           if (pool_installable(pool, pool->solvables + i))
3308             installable++;
3309           if (MAPTST(&addedmap, i))
3310             possible++;
3311         }
3312       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
3313     }
3314
3315   /*
3316    * first pass done, we now have all the rpm rules we need.
3317    * unify existing rules before going over all job rules and
3318    * policy rules.
3319    * at this point the system is always solvable,
3320    * as an empty system (remove all packages) is a valid solution
3321    */
3322
3323   unifyrules(solv);     /* remove duplicate rpm rules */
3324   solv->directdecisions = solv->decisionq.count;
3325
3326   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3327   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
3328     solver_printdecisions (solv);
3329
3330   /*
3331    * now add all job rules
3332    */
3333
3334   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
3335
3336   solv->jobrules = solv->nrules;
3337
3338   for (i = 0; i < job->count; i += 2)
3339     {
3340       oldnrules = solv->nrules;
3341
3342       how = job->elements[i] & ~SOLVER_WEAK;
3343       weak = job->elements[i] & SOLVER_WEAK;
3344       what = job->elements[i + 1];
3345       switch(how)
3346         {
3347         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
3348           s = pool->solvables + what;
3349           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
3350           addrule(solv, what, 0);                       /* install by Id */
3351           queue_push(&solv->ruletojob, i);
3352           if (weak)
3353             queue_push(&solv->weakruleq, solv->nrules - 1);
3354           break;
3355         case SOLVER_ERASE_SOLVABLE:
3356           s = pool->solvables + what;
3357           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
3358           addrule(solv, -what, 0);                      /* remove by Id */
3359           queue_push(&solv->ruletojob, i);
3360           if (weak)
3361             queue_push(&solv->weakruleq, solv->nrules - 1);
3362           break;
3363         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
3364         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3365           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
3366             POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall name %s\n", weak ? "weak " : "", dep2str(pool, what));
3367           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
3368             POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall provides %s\n", weak ? "weak " : "", dep2str(pool, what));
3369           queue_empty(&q);
3370           name = (how == SOLVER_INSTALL_SOLVABLE_NAME) ? what : 0;
3371           while (ISRELDEP(name))
3372             {
3373               Reldep *rd = GETRELDEP(pool, name);
3374               name = rd->name;
3375             }
3376           FOR_PROVIDES(p, pp, what)
3377             {
3378               /* if by name, ensure that the name matches */
3379               if (name && pool->solvables[p].name != name)
3380                 continue;
3381               queue_push(&q, p);
3382             }
3383           if (!q.count)
3384             {
3385               /* no provider, make this an impossible rule */
3386               queue_push(&q, -SYSTEMSOLVABLE);
3387             }
3388
3389           p = queue_shift(&q);         /* get first provider */
3390           if (!q.count)
3391             d = 0;                     /* single provider ? -> make assertion */
3392           else
3393             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
3394           addrule(solv, p, d);         /* add 'requires' rule */
3395           queue_push(&solv->ruletojob, i);
3396           if (weak)
3397             queue_push(&solv->weakruleq, solv->nrules - 1);
3398           break;
3399         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
3400         case SOLVER_ERASE_SOLVABLE_PROVIDES:
3401           if (how == SOLVER_ERASE_SOLVABLE_NAME)
3402             POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase name %s\n", weak ? "weak " : "", dep2str(pool, what));
3403           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
3404             POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase provides %s\n", weak ? "weak " : "", dep2str(pool, what));
3405           name = (how == SOLVER_ERASE_SOLVABLE_NAME) ? what : 0;
3406           while (ISRELDEP(name))
3407             {
3408               Reldep *rd = GETRELDEP(pool, name);
3409               name = rd->name;
3410             }
3411           FOR_PROVIDES(p, pp, what)
3412             {
3413               /* if by name, ensure that the name matches */
3414               if (name && pool->solvables[p].name != name)
3415                 continue;
3416               addrule(solv, -p, 0);  /* add 'remove' rule */
3417               queue_push(&solv->ruletojob, i);
3418               if (weak)
3419                 queue_push(&solv->weakruleq, solv->nrules - 1);
3420             }
3421           break;
3422         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
3423           s = pool->solvables + what;
3424           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
3425           addupdaterule(solv, s, 0);
3426           queue_push(&solv->ruletojob, i);
3427           if (weak)
3428             queue_push(&solv->weakruleq, solv->nrules - 1);
3429           break;
3430         case SOLVER_INSTALL_SOLVABLE_ONE_OF:
3431           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sone of\n", weak ? "weak " : "");
3432           for (pp = pool->whatprovidesdata + what; *pp; pp++)
3433             POOL_DEBUG(SAT_DEBUG_JOB, "  %s\n", solvable2str(pool, pool->solvables + *pp));
3434           addrule(solv, -SYSTEMSOLVABLE, what);
3435           queue_push(&solv->ruletojob, i);
3436           if (weak)
3437             queue_push(&solv->weakruleq, solv->nrules - 1);
3438           break;
3439         case SOLVER_WEAKEN_SOLVABLE_DEPS:
3440           s = pool->solvables + what;
3441           POOL_DEBUG(SAT_DEBUG_JOB, "job: weaken deps %s\n", solvable2str(pool, s));
3442           weaken_solvable_deps(solv, what);
3443           break;
3444         }
3445       IF_POOLDEBUG (SAT_DEBUG_JOB)
3446         {
3447           int j;
3448           if (solv->nrules == oldnrules)
3449             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
3450           for (j = oldnrules; j < solv->nrules; j++)
3451             {
3452               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
3453               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
3454             }
3455         }
3456     }
3457   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
3458
3459   /*
3460    * now add update rules
3461    *
3462    */
3463
3464   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
3465
3466
3467
3468   /*
3469    * create rules for updating installed solvables
3470    *
3471    */
3472
3473   solv->updaterules = solv->nrules;
3474   if (installed && !solv->allowuninstall)
3475     { /* loop over all installed solvables */
3476       /* we create all update rules, but disable some later on depending on the job */
3477       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3478         {
3479           /* no update rules for patch atoms */
3480           if (s->freshens && !s->supplements)
3481             {
3482               const char *name = id2str(pool, s->name);
3483               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3484                 {
3485                   addrule(solv, 0, 0);
3486                   continue;
3487                 }
3488             }
3489           if (s->repo == installed)
3490             addupdaterule(solv, s, 0);  /* allowall = 0 */
3491           else
3492             addrule(solv, 0, 0);        /* create dummy rule */
3493         }
3494       /* consistency check: we added a rule for _every_ installed solvable */
3495       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
3496     }
3497
3498   /* create feature rules */
3499   /* those are used later on to keep a version of the installed packages in
3500      best effort mode */
3501   solv->featurerules = solv->nrules;
3502   if (installed)
3503     {
3504       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3505         {
3506           if (s->freshens && !s->supplements)
3507             {
3508               const char *name = id2str(pool, s->name);
3509               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3510                 {
3511                   addrule(solv, 0, 0);
3512                   continue;
3513                 }
3514             }
3515           if (s->repo == installed)
3516             {
3517               Rule *sr;
3518               addupdaterule(solv, s, 1);        /* allowall = 0 */
3519               if (solv->allowuninstall)
3520                 {
3521                   queue_push(&solv->weakruleq, solv->nrules - 1);
3522                   continue;
3523                 }
3524               r = solv->rules + solv->nrules - 1;
3525               sr = r - (installed->end - installed->start);
3526               if (sr->p)
3527                 disablerule(solv, r);
3528               if (sr->p && !unifyrules_sortcmp(r, sr))
3529                 {
3530                   /* identical rule, kill feature rule */
3531                   memset(r, 0, sizeof(*r));
3532                 }
3533             }
3534           else
3535             addrule(solv, 0, 0);        /* create dummy rule */
3536         }
3537       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
3538     }
3539
3540   /* free unneeded memory */
3541   map_free(&addedmap);
3542   queue_free(&q);
3543
3544   /* create weak map */
3545   map_init(&solv->weakrulemap, solv->nrules);
3546   for (i = 0; i < solv->weakruleq.count; i++)
3547     {
3548       p = solv->weakruleq.elements[i];
3549       MAPSET(&solv->weakrulemap, p);
3550     }
3551
3552   /* all new rules are learnt after this point */
3553   solv->learntrules = solv->nrules;
3554
3555   /* disable update rules that conflict with our job */
3556   disableupdaterules(solv, job, -1);
3557
3558
3559   /* make decisions based on job/update assertions */
3560   makeruledecisions(solv);
3561
3562   /* create watches chains */
3563   makewatches(solv);
3564
3565   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
3566
3567   /* solve! */
3568   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
3569
3570   queue_init(&redoq);
3571   goterase = 0;
3572   /* disable all erase jobs (continuing weak "keep uninstalled" rules) */
3573   for (i = solv->jobrules, r = solv->rules + i; i < solv->updaterules; i++, r++)
3574     {
3575       if (!r->w1)
3576         continue;
3577       if (r->p > 0)     /* install job? */
3578         continue;
3579       disablerule(solv, r);
3580       goterase++;
3581     }
3582
3583   if (goterase)
3584     {
3585       enabledisablelearntrules(solv);
3586       removedisabledconflicts(solv, &redoq);
3587     }
3588
3589   /* find recommended packages */
3590   /* if redoq.count == 0 we already found all recommended in the
3591    * solver run */
3592   if (redoq.count || solv->dontinstallrecommended)
3593     {
3594       Id rec, *recp, p, *pp;
3595
3596       /* create map of all suggests that are still open */
3597       solv->recommends_index = -1;
3598       MAPZERO(&solv->recommendsmap);
3599       for (i = 0; i < solv->decisionq.count; i++)
3600         {
3601           p = solv->decisionq.elements[i];
3602           if (p < 0)
3603             continue;
3604           s = pool->solvables + p;
3605           if (s->recommends)
3606             {
3607               recp = s->repo->idarraydata + s->recommends;
3608               while ((rec = *recp++) != 0)
3609                 {
3610                   FOR_PROVIDES(p, pp, rec)
3611                     if (solv->decisionmap[p] > 0)
3612                       break;
3613                   if (p)
3614                     continue;   /* p != 0: already fulfilled */
3615                   FOR_PROVIDES(p, pp, rec)
3616                     MAPSET(&solv->recommendsmap, p);
3617                 }
3618             }
3619         }
3620       for (i = 1; i < pool->nsolvables; i++)
3621         {
3622           if (solv->decisionmap[i] != 0)
3623             continue;
3624           s = pool->solvables + i;
3625           if (!MAPTST(&solv->recommendsmap, i))
3626             {
3627               if (!s->supplements)
3628                 continue;
3629               if (!pool_installable(pool, s))
3630                 continue;
3631               if (!solver_is_supplementing(solv, s))
3632                 continue;
3633             }
3634           if (solv->dontinstallrecommended)
3635             queue_push(&solv->recommendations, i);
3636           else
3637             queue_pushunique(&solv->recommendations, i);
3638         }
3639       /* we use MODE_SUGGEST here so that repo prio is ignored */
3640       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
3641     }
3642
3643   /* find suggested packages */
3644   if (1)
3645     {
3646       Id sug, *sugp, p, *pp;
3647
3648       /* create map of all suggests that are still open */
3649       solv->recommends_index = -1;
3650       MAPZERO(&solv->suggestsmap);
3651       for (i = 0; i < solv->decisionq.count; i++)
3652         {
3653           p = solv->decisionq.elements[i];
3654           if (p < 0)
3655             continue;
3656           s = pool->solvables + p;
3657           if (s->suggests)
3658             {
3659               sugp = s->repo->idarraydata + s->suggests;
3660               while ((sug = *sugp++) != 0)
3661                 {
3662                   FOR_PROVIDES(p, pp, sug)
3663                     if (solv->decisionmap[p] > 0)
3664                       break;
3665                   if (p)
3666                     continue;   /* already fulfilled */
3667                   FOR_PROVIDES(p, pp, sug)
3668                     MAPSET(&solv->suggestsmap, p);
3669                 }
3670             }
3671         }
3672       for (i = 1; i < pool->nsolvables; i++)
3673         {
3674           if (solv->decisionmap[i] != 0)
3675             continue;
3676           s = pool->solvables + i;
3677           if (!MAPTST(&solv->suggestsmap, i))
3678             {
3679               if (!s->enhances)
3680                 continue;
3681               if (!pool_installable(pool, s))
3682                 continue;
3683               if (!solver_is_enhancing(solv, s))
3684                 continue;
3685             }
3686           queue_push(&solv->suggestions, i);
3687         }
3688       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
3689     }
3690
3691   if (redoq.count)
3692     {
3693       /* restore decisionmap */
3694       for (i = 0; i < redoq.count; i += 2)
3695         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
3696     }
3697
3698
3699   if (solv->problems.count)
3700     {
3701       int recocount = solv->recommendations.count;
3702       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
3703       queue_empty(&redoq);
3704       for (i = 0; i < solv->decisionq.count; i++)
3705         {
3706           Id p = solv->decisionq.elements[i];
3707           queue_push(&redoq, p);
3708           queue_push(&redoq, solv->decisionq_why.elements[i]);
3709           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
3710         }
3711       problems_to_solutions(solv, job);
3712       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
3713       queue_empty(&solv->decisionq);
3714       queue_empty(&solv->decisionq_why);
3715       for (i = 0; i < redoq.count; i += 3)
3716         {
3717           Id p = redoq.elements[i];
3718           queue_push(&solv->decisionq, p);
3719           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
3720           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
3721         }
3722       solv->recommendations.count = recocount;
3723     }
3724   queue_free(&redoq);
3725 }
3726
3727 /***********************************************************************/
3728
3729 void
3730 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
3731 {
3732   Map installedmap;
3733
3734   solver_create_state_maps(solv, &installedmap, 0);
3735   pool_calc_duchanges(solv->pool, solv->installed, &installedmap, mps, nmps);
3736   map_free(&installedmap);
3737 }
3738
3739 int
3740 solver_calc_installsizechange(Solver *solv)
3741 {
3742   Map installedmap;
3743   int change;
3744
3745   solver_create_state_maps(solv, &installedmap, 0);
3746   change = pool_calc_installsizechange(solv->pool, solv->installed, &installedmap);
3747   map_free(&installedmap);
3748   return change;
3749 }
3750