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