src/solver.c

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