src/solver.c

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