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