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