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