src/solver.c

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