src/solver.c

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