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  * return : 0 = everything is OK
1561  *          rule = conflict found in this rule
1562  */
1563
1564 static Rule *
1565 propagate(Solver *solv, int level)
1566 {
1567   Pool *pool = solv->pool;
1568   Id *rp, *next_rp;           /* rule pointer, next rule pointer in linked list */
1569   Rule *r;                    /* rule */
1570   Id p, pkg, other_watch;
1571   Id *dp;
1572   Id *decisionmap = solv->decisionmap;
1573
1574   Id *watches = solv->watches + pool->nsolvables;   /* place ptr in middle */
1575
1576   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
1577
1578   /* foreach non-propagated decision */
1579   while (solv->propagate_index < solv->decisionq.count)
1580     {
1581         /*
1582          * 'pkg' was just decided
1583          * negate because our watches trigger if literal goes FALSE
1584          */
1585       pkg = -solv->decisionq.elements[solv->propagate_index++];
1586
1587       IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1588         {
1589           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
1590           solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
1591         }
1592
1593       /* foreach rule where 'pkg' is now FALSE */
1594       for (rp = watches + pkg; *rp; rp = next_rp)
1595         {
1596           r = solv->rules + *rp;
1597           if (r->d < 0)
1598             {
1599               /* rule is disabled, goto next */
1600               if (pkg == r->w1)
1601                 next_rp = &r->n1;
1602               else
1603                 next_rp = &r->n2;
1604               continue;
1605             }
1606
1607           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1608             {
1609               POOL_DEBUG(SAT_DEBUG_PROPAGATE,"  watch triggered ");
1610               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1611             }
1612
1613             /* 'pkg' was just decided
1614              *   now find other literal watch, check clause
1615              *  and advance on linked list
1616              */
1617           if (pkg == r->w1)
1618             {
1619               other_watch = r->w2;
1620               next_rp = &r->n1;
1621             }
1622           else
1623             {
1624               other_watch = r->w1;
1625               next_rp = &r->n2;
1626             }
1627
1628             /*
1629              * This term is already true (through the other literal)
1630              * so we have nothing to do
1631              */
1632           if (DECISIONMAP_TRUE(other_watch))
1633             continue;
1634
1635             /*
1636              * The other literal is FALSE or UNDEF
1637              */
1638
1639           if (r->d)
1640             {
1641               /* not a binary clause, try to move our watch.
1642                * search for a literal that is not other_watch and not FALSE
1643                * (TRUE is also ok, in that case the rule is fulfilled)
1644                */
1645               if (r->p                                /* we have a 'p' */
1646                   && r->p != other_watch              /* which is watched */
1647                   && !DECISIONMAP_FALSE(r->p))        /* and not FALSE */
1648                 {
1649                   p = r->p;
1650                 }
1651               else                                    /* go find a 'd' to make 'true' */
1652                 {
1653                   /* foreach 'd' */
1654                   for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
1655                     if (p != other_watch              /* which is not watched */
1656                         && !DECISIONMAP_FALSE(p))     /* and not FALSE */
1657                       break;
1658                 }
1659
1660               if (p)
1661                 {
1662                   /*
1663                    * if we found some p that is UNDEF or TRUE, move
1664                    * watch to it
1665                    */
1666                   IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1667                     {
1668                       if (p > 0)
1669                         POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables + p));
1670                       else
1671                         POOL_DEBUG(SAT_DEBUG_PROPAGATE,"    -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvable2str(pool, pool->solvables - p));
1672                     }
1673
1674                   *rp = *next_rp;
1675                   next_rp = rp;
1676
1677                   if (pkg == r->w1)
1678                     {
1679                       r->w1 = p;
1680                       r->n1 = watches[p];
1681                     }
1682                   else
1683                     {
1684                       r->w2 = p;
1685                       r->n2 = watches[p];
1686                     }
1687                   watches[p] = r - solv->rules;
1688                   continue;
1689                 }
1690               /* search failed, thus all unwatched literals are FALSE */
1691
1692             } /* not binary */
1693
1694             /*
1695              * unit clause found, set literal other_watch to TRUE
1696              */
1697
1698           if (DECISIONMAP_FALSE(other_watch))      /* check if literal is FALSE */
1699             return r;                              /* eek, a conflict! */
1700
1701           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1702             {
1703               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "   unit ");
1704               solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
1705             }
1706
1707           if (other_watch > 0)
1708             decisionmap[other_watch] = level;    /* install! */
1709           else
1710             decisionmap[-other_watch] = -level;  /* remove! */
1711
1712           queue_push(&solv->decisionq, other_watch);
1713           queue_push(&solv->decisionq_why, r - solv->rules);
1714
1715           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
1716             {
1717               Solvable *s = pool->solvables + (other_watch > 0 ? other_watch : -other_watch);
1718               if (other_watch > 0)
1719                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to install %s\n", solvable2str(pool, s));
1720               else
1721                 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "    -> decided to conflict %s\n", solvable2str(pool, s));
1722             }
1723
1724         } /* foreach rule involving 'pkg' */
1725
1726     } /* while we have non-decided decisions */
1727
1728   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
1729
1730   return 0;     /* all is well */
1731 }
1732
1733
1734 /********************************************************************/
1735 /* Analysis */
1736
1737 /*-------------------------------------------------------------------
1738  *
1739  * analyze
1740  *   and learn
1741  */
1742
1743 static int
1744 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
1745 {
1746   Pool *pool = solv->pool;
1747   Queue r;
1748   int rlevel = 1;
1749   Map seen;             /* global? */
1750   Id d, v, vv, *dp, why;
1751   int l, i, idx;
1752   int num = 0, l1num = 0;
1753   int learnt_why = solv->learnt_pool.count;
1754   Id *decisionmap = solv->decisionmap;
1755
1756   queue_init(&r);
1757
1758   POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
1759   map_init(&seen, pool->nsolvables);
1760   idx = solv->decisionq.count;
1761   for (;;)
1762     {
1763       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1764         solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c);
1765       queue_push(&solv->learnt_pool, c - solv->rules);
1766       d = c->d < 0 ? -c->d - 1 : c->d;
1767       dp = d ? pool->whatprovidesdata + d : 0;
1768       /* go through all literals of the rule */
1769       for (i = -1; ; i++)
1770         {
1771           if (i == -1)
1772             v = c->p;
1773           else if (d == 0)
1774             v = i ? 0 : c->w2;
1775           else
1776             v = *dp++;
1777           if (v == 0)
1778             break;
1779
1780           if (DECISIONMAP_TRUE(v))      /* the one true literal */
1781             continue;
1782           vv = v > 0 ? v : -v;
1783           if (MAPTST(&seen, vv))
1784             continue;
1785           l = solv->decisionmap[vv];
1786           if (l < 0)
1787             l = -l;
1788           MAPSET(&seen, vv);
1789           if (l == 1)
1790             l1num++;                    /* need to do this one in level1 pass */
1791           else if (l == level)
1792             num++;                      /* need to do this one as well */
1793           else
1794             {
1795               queue_push(&r, v);        /* not level1 or conflict level, add to new rule */
1796               if (l > rlevel)
1797                 rlevel = l;
1798             }
1799         }
1800 l1retry:
1801       if (!num && !--l1num)
1802         break;  /* all level 1 literals done */
1803       for (;;)
1804         {
1805           assert(idx > 0);
1806           v = solv->decisionq.elements[--idx];
1807           vv = v > 0 ? v : -v;
1808           if (MAPTST(&seen, vv))
1809             break;
1810         }
1811       MAPCLR(&seen, vv);
1812       if (num && --num == 0)
1813         {
1814           *pr = -v;     /* so that v doesn't get lost */
1815           if (!l1num)
1816             break;
1817           POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
1818           for (i = 0; i < r.count; i++)
1819             {
1820               v = r.elements[i];
1821               MAPCLR(&seen, v > 0 ? v : -v);
1822             }
1823           /* only level 1 marks left */
1824           l1num++;
1825           goto l1retry;
1826         }
1827       why = solv->decisionq_why.elements[idx];
1828       if (!why)                 /* just in case, maye for SYSTEMSOLVABLE */
1829         goto l1retry;
1830       c = solv->rules + why;
1831     }
1832   map_free(&seen);
1833
1834   if (r.count == 0)
1835     *dr = 0;
1836   else if (r.count == 1 && r.elements[0] < 0)
1837     *dr = r.elements[0];
1838   else
1839     *dr = pool_queuetowhatprovides(pool, &r);
1840   IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
1841     {
1842       POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
1843       solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
1844       for (i = 0; i < r.count; i++)
1845         solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
1846     }
1847   /* push end marker on learnt reasons stack */
1848   queue_push(&solv->learnt_pool, 0);
1849   if (whyp)
1850     *whyp = learnt_why;
1851   solv->stats_learned++;
1852   return rlevel;
1853 }
1854
1855
1856 /*-------------------------------------------------------------------
1857  *
1858  * reset_solver
1859  *
1860  * reset the solver decisions to right after the rpm rules.
1861  * called after rules have been enabled/disabled
1862  */
1863
1864 static void
1865 reset_solver(Solver *solv)
1866 {
1867   Pool *pool = solv->pool;
1868   int i;
1869   Id v;
1870
1871   /* rewind decisions to direct rpm rule assertions */
1872   for (i = solv->decisionq.count - 1; i >= solv->directdecisions; i--)
1873     {
1874       v = solv->decisionq.elements[i];
1875       solv->decisionmap[v > 0 ? v : -v] = 0;
1876     }
1877
1878   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions done reduced from %d to %d\n", solv->decisionq.count, solv->directdecisions);
1879
1880   solv->decisionq_why.count = solv->directdecisions;
1881   solv->decisionq.count = solv->directdecisions;
1882   solv->recommends_index = -1;
1883   solv->propagate_index = 0;
1884
1885   /* adapt learnt rule status to new set of enabled/disabled rules */
1886   enabledisablelearntrules(solv);
1887
1888   /* redo all job/update decisions */
1889   makeruledecisions(solv);
1890   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
1891 }
1892
1893
1894 /*-------------------------------------------------------------------
1895  *
1896  * analyze_unsolvable_rule
1897  */
1898
1899 static void
1900 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
1901 {
1902   Pool *pool = solv->pool;
1903   int i;
1904   Id why = r - solv->rules;
1905
1906   IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
1907     solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
1908   if (solv->learntrules && why >= solv->learntrules)
1909     {
1910       for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
1911         if (solv->learnt_pool.elements[i] > 0)
1912           analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
1913       return;
1914     }
1915   if (MAPTST(&solv->weakrulemap, why))
1916     if (!*lastweakp || why > *lastweakp)
1917       *lastweakp = why;
1918   /* do not add rpm rules to problem */
1919   if (why < solv->rpmrules_end)
1920     return;
1921   /* turn rule into problem */
1922   if (why >= solv->jobrules && why < solv->jobrules_end)
1923     why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
1924   /* return if problem already countains our rule */
1925   if (solv->problems.count)
1926     {
1927       for (i = solv->problems.count - 1; i >= 0; i--)
1928         if (solv->problems.elements[i] == 0)    /* end of last problem reached? */
1929           break;
1930         else if (solv->problems.elements[i] == why)
1931           return;
1932     }
1933   queue_push(&solv->problems, why);
1934 }
1935
1936
1937 /*-------------------------------------------------------------------
1938  *
1939  * analyze_unsolvable
1940  *
1941  * return: 1 - disabled some rules, try again
1942  *         0 - hopeless
1943  */
1944
1945 static int
1946 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
1947 {
1948   Pool *pool = solv->pool;
1949   Rule *r;
1950   Map seen;             /* global to speed things up? */
1951   Id d, v, vv, *dp, why;
1952   int l, i, idx;
1953   Id *decisionmap = solv->decisionmap;
1954   int oldproblemcount;
1955   int oldlearntpoolcount;
1956   Id lastweak;
1957
1958   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
1959   solv->stats_unsolvable++;
1960   oldproblemcount = solv->problems.count;
1961   oldlearntpoolcount = solv->learnt_pool.count;
1962
1963   /* make room for proof index */
1964   /* must update it later, as analyze_unsolvable_rule would confuse
1965    * it with a rule index if we put the real value in already */
1966   queue_push(&solv->problems, 0);
1967
1968   r = cr;
1969   map_init(&seen, pool->nsolvables);
1970   queue_push(&solv->learnt_pool, r - solv->rules);
1971   lastweak = 0;
1972   analyze_unsolvable_rule(solv, r, &lastweak);
1973   d = r->d < 0 ? -r->d - 1 : r->d;
1974   dp = d ? pool->whatprovidesdata + d : 0;
1975   for (i = -1; ; i++)
1976     {
1977       if (i == -1)
1978         v = r->p;
1979       else if (d == 0)
1980         v = i ? 0 : r->w2;
1981       else
1982         v = *dp++;
1983       if (v == 0)
1984         break;
1985       if (DECISIONMAP_TRUE(v))  /* the one true literal */
1986           continue;
1987       vv = v > 0 ? v : -v;
1988       l = solv->decisionmap[vv];
1989       if (l < 0)
1990         l = -l;
1991       MAPSET(&seen, vv);
1992     }
1993   idx = solv->decisionq.count;
1994   while (idx > 0)
1995     {
1996       v = solv->decisionq.elements[--idx];
1997       vv = v > 0 ? v : -v;
1998       if (!MAPTST(&seen, vv))
1999         continue;
2000       why = solv->decisionq_why.elements[idx];
2001       queue_push(&solv->learnt_pool, why);
2002       r = solv->rules + why;
2003       analyze_unsolvable_rule(solv, r, &lastweak);
2004       d = r->d < 0 ? -r->d - 1 : r->d;
2005       dp = d ? pool->whatprovidesdata + d : 0;
2006       for (i = -1; ; i++)
2007         {
2008           if (i == -1)
2009             v = r->p;
2010           else if (d == 0)
2011             v = i ? 0 : r->w2;
2012           else
2013             v = *dp++;
2014           if (v == 0)
2015             break;
2016           if (DECISIONMAP_TRUE(v))      /* the one true literal */
2017               continue;
2018           vv = v > 0 ? v : -v;
2019           l = solv->decisionmap[vv];
2020           if (l < 0)
2021             l = -l;
2022           MAPSET(&seen, vv);
2023         }
2024     }
2025   map_free(&seen);
2026   queue_push(&solv->problems, 0);       /* mark end of this problem */
2027
2028   if (lastweak)
2029     {
2030       /* disable last weak rule */
2031       solv->problems.count = oldproblemcount;
2032       solv->learnt_pool.count = oldlearntpoolcount;
2033       r = solv->rules + lastweak;
2034       POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
2035       solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
2036       disablerule(solv, r);
2037       reset_solver(solv);
2038       return 1;
2039     }
2040
2041   /* finish proof */
2042   queue_push(&solv->learnt_pool, 0);
2043   solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
2044
2045   if (disablerules)
2046     {
2047       for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
2048         disableproblem(solv, solv->problems.elements[i]);
2049       /* XXX: might want to enable all weak rules again */
2050       reset_solver(solv);
2051       return 1;
2052     }
2053   POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
2054   return 0;
2055 }
2056
2057
2058 /********************************************************************/
2059 /* Decision revert */
2060
2061 /*-------------------------------------------------------------------
2062  *
2063  * revert
2064  * revert decision at level
2065  */
2066
2067 static void
2068 revert(Solver *solv, int level)
2069 {
2070   Pool *pool = solv->pool;
2071   Id v, vv;
2072   while (solv->decisionq.count)
2073     {
2074       v = solv->decisionq.elements[solv->decisionq.count - 1];
2075       vv = v > 0 ? v : -v;
2076       if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
2077         break;
2078       POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
2079       if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
2080         solv->recommendations.count--;
2081       solv->decisionmap[vv] = 0;
2082       solv->decisionq.count--;
2083       solv->decisionq_why.count--;
2084       solv->propagate_index = solv->decisionq.count;
2085     }
2086   while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
2087     {
2088       solv->branches.count--;
2089       while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
2090         solv->branches.count--;
2091     }
2092   solv->recommends_index = -1;
2093 }
2094
2095
2096 /*-------------------------------------------------------------------
2097  *
2098  * watch2onhighest - put watch2 on literal with highest level
2099  */
2100
2101 static inline void
2102 watch2onhighest(Solver *solv, Rule *r)
2103 {
2104   int l, wl = 0;
2105   Id d, v, *dp;
2106
2107   d = r->d < 0 ? -r->d - 1 : r->d;
2108   if (!d)
2109     return;     /* binary rule, both watches are set */
2110   dp = solv->pool->whatprovidesdata + d;
2111   while ((v = *dp++) != 0)
2112     {
2113       l = solv->decisionmap[v < 0 ? -v : v];
2114       if (l < 0)
2115         l = -l;
2116       if (l > wl)
2117         {
2118           r->w2 = dp[-1];
2119           wl = l;
2120         }
2121     }
2122 }
2123
2124
2125 /*-------------------------------------------------------------------
2126  *
2127  * setpropagatelearn
2128  *
2129  * add free decision (solvable to install) to decisionq
2130  * increase level and propagate decision
2131  * return if no conflict.
2132  *
2133  * in conflict case, analyze conflict rule, add resulting
2134  * rule to learnt rule set, make decision from learnt
2135  * rule (always unit) and re-propagate.
2136  *
2137  * returns the new solver level or 0 if unsolvable
2138  *
2139  */
2140
2141 static int
2142 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules)
2143 {
2144   Pool *pool = solv->pool;
2145   Rule *r;
2146   Id p = 0, d = 0;
2147   int l, why;
2148
2149   if (decision)
2150     {
2151       level++;
2152       if (decision > 0)
2153         solv->decisionmap[decision] = level;
2154       else
2155         solv->decisionmap[-decision] = -level;
2156       queue_push(&solv->decisionq, decision);
2157       queue_push(&solv->decisionq_why, 0);
2158     }
2159   for (;;)
2160     {
2161       r = propagate(solv, level);
2162       if (!r)
2163         break;
2164       if (level == 1)
2165         return analyze_unsolvable(solv, r, disablerules);
2166       POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
2167       l = analyze(solv, level, r, &p, &d, &why);        /* learnt rule in p and d */
2168       assert(l > 0 && l < level);
2169       POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
2170       level = l;
2171       revert(solv, level);
2172       r = addrule(solv, p, d);       /* p requires d */
2173       assert(r);
2174       assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
2175       queue_push(&solv->learnt_why, why);
2176       if (d)
2177         {
2178           /* at least 2 literals, needs watches */
2179           watch2onhighest(solv, r);
2180           addwatches_rule(solv, r);
2181         }
2182       else
2183         {
2184           /* learnt rule is an assertion */
2185           queue_push(&solv->ruleassertions, r - solv->rules);
2186         }
2187       solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
2188       queue_push(&solv->decisionq, p);
2189       queue_push(&solv->decisionq_why, r - solv->rules);
2190       IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
2191         {
2192           POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
2193           solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
2194           POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
2195           solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
2196         }
2197     }
2198   return level;
2199 }
2200
2201
2202 /*-------------------------------------------------------------------
2203  *
2204  * select and install
2205  *
2206  * install best package from the queue. We add an extra package, inst, if
2207  * provided. See comment in weak install section.
2208  *
2209  * returns the new solver level or 0 if unsolvable
2210  *
2211  */
2212
2213 static int
2214 selectandinstall(Solver *solv, int level, Queue *dq, Id inst, int disablerules)
2215 {
2216   Pool *pool = solv->pool;
2217   Id p;
2218   int i;
2219
2220   if (dq->count > 1 || inst)
2221     policy_filter_unwanted(solv, dq, inst, POLICY_MODE_CHOOSE);
2222
2223   i = 0;
2224   if (dq->count > 1)
2225     {
2226       /* choose the supplemented one */
2227       for (i = 0; i < dq->count; i++)
2228         if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
2229           break;
2230       if (i == dq->count)
2231         {
2232           for (i = 1; i < dq->count; i++)
2233             queue_push(&solv->branches, dq->elements[i]);
2234           queue_push(&solv->branches, -level);
2235           i = 0;
2236         }
2237     }
2238   p = dq->elements[i];
2239
2240   POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvable2str(pool, pool->solvables + p));
2241
2242   return setpropagatelearn(solv, level, p, disablerules);
2243 }
2244
2245
2246 /********************************************************************/
2247 /* Main solver interface */
2248
2249
2250 /*-------------------------------------------------------------------
2251  *
2252  * solver_create
2253  * create solver structure
2254  *
2255  * pool: all available solvables
2256  * installed: installed Solvables
2257  *
2258  *
2259  * Upon solving, rules are created to flag the Solvables
2260  * of the 'installed' Repo as installed.
2261  */
2262
2263 Solver *
2264 solver_create(Pool *pool, Repo *installed)
2265 {
2266   Solver *solv;
2267   solv = (Solver *)sat_calloc(1, sizeof(Solver));
2268   solv->pool = pool;
2269   solv->installed = installed;
2270
2271   queue_init(&solv->ruletojob);
2272   queue_init(&solv->decisionq);
2273   queue_init(&solv->decisionq_why);
2274   queue_init(&solv->problems);
2275   queue_init(&solv->suggestions);
2276   queue_init(&solv->recommendations);
2277   queue_init(&solv->learnt_why);
2278   queue_init(&solv->learnt_pool);
2279   queue_init(&solv->branches);
2280   queue_init(&solv->covenantq);
2281   queue_init(&solv->weakruleq);
2282   queue_init(&solv->ruleassertions);
2283
2284   map_init(&solv->recommendsmap, pool->nsolvables);
2285   map_init(&solv->suggestsmap, pool->nsolvables);
2286   map_init(&solv->noupdate, installed ? installed->end - installed->start : 0);
2287   solv->recommends_index = 0;
2288
2289   solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
2290   solv->nrules = 1;
2291   solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
2292   memset(solv->rules, 0, sizeof(Rule));
2293
2294   return solv;
2295 }
2296
2297
2298 /*-------------------------------------------------------------------
2299  *
2300  * solver_free
2301  */
2302
2303 void
2304 solver_free(Solver *solv)
2305 {
2306   queue_free(&solv->ruletojob);
2307   queue_free(&solv->decisionq);
2308   queue_free(&solv->decisionq_why);
2309   queue_free(&solv->learnt_why);
2310   queue_free(&solv->learnt_pool);
2311   queue_free(&solv->problems);
2312   queue_free(&solv->suggestions);
2313   queue_free(&solv->recommendations);
2314   queue_free(&solv->branches);
2315   queue_free(&solv->covenantq);
2316   queue_free(&solv->weakruleq);
2317   queue_free(&solv->ruleassertions);
2318
2319   map_free(&solv->recommendsmap);
2320   map_free(&solv->suggestsmap);
2321   map_free(&solv->noupdate);
2322   map_free(&solv->weakrulemap);
2323   map_free(&solv->noobsoletes);
2324
2325   sat_free(solv->decisionmap);
2326   sat_free(solv->rules);
2327   sat_free(solv->watches);
2328   sat_free(solv->obsoletes);
2329   sat_free(solv->obsoletes_data);
2330   sat_free(solv);
2331 }
2332
2333
2334 /*-------------------------------------------------------------------
2335  *
2336  * run_solver
2337  *
2338  * all rules have been set up, now actually run the solver
2339  *
2340  */
2341
2342 static void
2343 run_solver(Solver *solv, int disablerules, int doweak)
2344 {
2345   Queue dq;         /* local decisionqueue */
2346   int systemlevel;
2347   int level, olevel;
2348   Rule *r;
2349   int i, j, n;
2350   Solvable *s;
2351   Pool *pool = solv->pool;
2352   Id p, *dp;
2353
2354   IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
2355     {
2356       POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
2357       for (i = 1; i < solv->nrules; i++)
2358         solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
2359     }
2360
2361   POOL_DEBUG(SAT_DEBUG_STATS, "initial decisions: %d\n", solv->decisionq.count);
2362
2363   IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2364     solver_printdecisions(solv);
2365
2366   /* start SAT algorithm */
2367   level = 1;
2368   systemlevel = level + 1;
2369   POOL_DEBUG(SAT_DEBUG_STATS, "solving...\n");
2370
2371   queue_init(&dq);
2372
2373   /*
2374    * here's the main loop:
2375    * 1) propagate new decisions (only needed for level 1)
2376    * 2) try to keep installed packages
2377    * 3) fulfill all unresolved rules
2378    * 4) install recommended packages
2379    * 5) minimalize solution if we had choices
2380    * if we encounter a problem, we rewind to a safe level and restart
2381    * with step 1
2382    */
2383
2384   for (;;)
2385     {
2386       /*
2387        * propagate
2388        */
2389
2390       if (level == 1)
2391         {
2392           POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d;  size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
2393           if ((r = propagate(solv, level)) != 0)
2394             {
2395               if (analyze_unsolvable(solv, r, disablerules))
2396                 continue;
2397               queue_free(&dq);
2398               return;
2399             }
2400         }
2401
2402       /*
2403        * installed packages
2404        */
2405
2406       if (level < systemlevel && solv->installed && solv->installed->nsolvables)
2407         {
2408           if (!solv->updatesystem)
2409             {
2410               /*
2411                * Normal run (non-updating)
2412                * Keep as many packages installed as possible
2413                */
2414               POOL_DEBUG(SAT_DEBUG_STATS, "installing old packages\n");
2415
2416               for (i = solv->installed->start; i < solv->installed->end; i++)
2417                 {
2418                   s = pool->solvables + i;
2419
2420                     /* skip if not installed */
2421                   if (s->repo != solv->installed)
2422                     continue;
2423
2424                     /* skip if already decided */
2425                   if (solv->decisionmap[i] != 0)
2426                     continue;
2427
2428                   POOL_DEBUG(SAT_DEBUG_PROPAGATE, "keeping %s\n", solvable2str(pool, s));
2429
2430                   olevel = level;
2431                   level = setpropagatelearn(solv, level, i, disablerules);
2432
2433                   if (level == 0)                /* unsolvable */
2434                     {
2435                       queue_free(&dq);
2436                       return;
2437                     }
2438                   if (level <= olevel)
2439                     break;
2440                 }
2441               if (i < solv->installed->end)
2442                 continue;
2443             }
2444
2445           POOL_DEBUG(SAT_DEBUG_STATS, "resolving update/feature rules\n");
2446
2447           for (i = solv->installed->start, r = solv->rules + solv->updaterules; i < solv->installed->end; i++, r++)
2448             {
2449               Rule *rr;
2450               Id d;
2451               s = pool->solvables + i;
2452
2453                 /* skip if not installed (can't update) */
2454               if (s->repo != solv->installed)
2455                 continue;
2456                 /* skip if already decided */
2457               if (solv->decisionmap[i] > 0)
2458                 continue;
2459
2460                 /* noupdate is set if a job is erasing the installed solvable or installing a specific version */
2461               if (MAPTST(&solv->noupdate, i - solv->installed->start))
2462                 continue;
2463
2464               queue_empty(&dq);
2465               rr = r;
2466               if (rr->d < 0)    /* disabled -> look at feature rule ? */
2467                 rr -= solv->installed->end - solv->installed->start;
2468               if (!rr->p)       /* identical to update rule? */
2469                 rr = r;
2470               d = (rr->d < 0) ? -rr->d - 1 : rr->d;
2471               if (d == 0)
2472                 {
2473                   if (!rr->w2 || solv->decisionmap[rr->w2] > 0)
2474                     continue;
2475                     /* decide w2 if yet undecided */
2476                   if (solv->decisionmap[rr->w2] == 0)
2477                     queue_push(&dq, rr->w2);
2478                 }
2479               else
2480                 {
2481                   dp = pool->whatprovidesdata + d;
2482                   while ((p = *dp++) != 0)
2483                     {
2484                       if (solv->decisionmap[p] > 0)
2485                         break;
2486                         /* decide p if yet undecided */
2487                       if (solv->decisionmap[p] == 0)
2488                         queue_push(&dq, p);
2489                     }
2490                   if (p)
2491                     continue;
2492                 }
2493               if (!dq.count && solv->decisionmap[i] != 0)
2494                 continue;
2495               olevel = level;
2496               /* FIXME: it is handled a bit different because we do not want
2497                * to have it pruned just because it is not recommened.
2498                * we should not prune installed packages instead
2499                */
2500               level = selectandinstall(solv, level, &dq, (solv->decisionmap[i] ? 0 : i), disablerules);
2501               if (level == 0)
2502                 {
2503                   queue_free(&dq);
2504                   return;
2505                 }
2506               if (level <= olevel)
2507                 break;
2508             }
2509           if (i < solv->installed->end)
2510             continue;
2511           systemlevel = level;
2512         }
2513
2514       /*
2515        * decide
2516        */
2517
2518       POOL_DEBUG(SAT_DEBUG_STATS, "deciding unresolved rules\n");
2519       for (i = 1, n = 1; ; i++, n++)
2520         {
2521           if (n == solv->nrules)
2522             break;
2523           if (i == solv->nrules)
2524             i = 1;
2525           r = solv->rules + i;
2526           if (r->d < 0)         /* ignore disabled rules */
2527             continue;
2528           queue_empty(&dq);
2529           if (r->d == 0)
2530             {
2531               /* binary or unary rule */
2532               /* need two positive undecided literals */
2533               if (r->p < 0 || r->w2 <= 0)
2534                 continue;
2535               if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
2536                 continue;
2537               queue_push(&dq, r->p);
2538               queue_push(&dq, r->w2);
2539             }
2540           else
2541             {
2542               /* make sure that
2543                * all negative literals are installed
2544                * no positive literal is installed
2545                * i.e. the rule is not fulfilled and we
2546                * just need to decide on the positive literals
2547                */
2548               if (r->p < 0)
2549                 {
2550                   if (solv->decisionmap[-r->p] <= 0)
2551                     continue;
2552                 }
2553               else
2554                 {
2555                   if (solv->decisionmap[r->p] > 0)
2556                     continue;
2557                   if (solv->decisionmap[r->p] == 0)
2558                     queue_push(&dq, r->p);
2559                 }
2560               dp = pool->whatprovidesdata + r->d;
2561               while ((p = *dp++) != 0)
2562                 {
2563                   if (p < 0)
2564                     {
2565                       if (solv->decisionmap[-p] <= 0)
2566                         break;
2567                     }
2568                   else
2569                     {
2570                       if (solv->decisionmap[p] > 0)
2571                         break;
2572                       if (solv->decisionmap[p] == 0)
2573                         queue_push(&dq, p);
2574                     }
2575                 }
2576               if (p)
2577                 continue;
2578             }
2579           IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
2580             {
2581               POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
2582               solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
2583             }
2584           /* dq.count < 2 cannot happen as this means that
2585            * the rule is unit */
2586           assert(dq.count > 1);
2587
2588           olevel = level;
2589           level = selectandinstall(solv, level, &dq, 0, disablerules);
2590           if (level == 0)
2591             {
2592               queue_free(&dq);
2593               return;
2594             }
2595           if (level < systemlevel)
2596             break;
2597           n = 0;
2598         } /* for(), decide */
2599
2600       if (n != solv->nrules)    /* continue if level < systemlevel */
2601         continue;
2602
2603       if (doweak)
2604         {
2605           int qcount;
2606
2607           POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended packages\n");
2608           queue_empty(&dq);
2609           for (i = 1; i < pool->nsolvables; i++)
2610             {
2611               if (solv->decisionmap[i] < 0)
2612                 continue;
2613               if (solv->decisionmap[i] > 0)
2614                 {
2615                   Id *recp, rec, *pp, p;
2616                   s = pool->solvables + i;
2617                   /* installed, check for recommends */
2618                   /* XXX need to special case AND ? */
2619                   if (s->recommends)
2620                     {
2621                       recp = s->repo->idarraydata + s->recommends;
2622                       while ((rec = *recp++) != 0)
2623                         {
2624                           qcount = dq.count;
2625                           FOR_PROVIDES(p, pp, rec)
2626                             {
2627                               if (solv->decisionmap[p] > 0)
2628                                 {
2629                                   dq.count = qcount;
2630                                   break;
2631                                 }
2632                               else if (solv->decisionmap[p] == 0)
2633                                 {
2634                                   queue_pushunique(&dq, p);
2635                                 }
2636                             }
2637                         }
2638                     }
2639                 }
2640               else
2641                 {
2642                   s = pool->solvables + i;
2643                   if (!s->supplements && !s->freshens)
2644                     continue;
2645                   if (!pool_installable(pool, s))
2646                     continue;
2647                   if (solver_is_supplementing(solv, s))
2648                     queue_pushunique(&dq, i);
2649                 }
2650             }
2651           if (dq.count)
2652             {
2653               if (dq.count > 1)
2654                 policy_filter_unwanted(solv, &dq, 0, POLICY_MODE_RECOMMEND);
2655               p = dq.elements[0];
2656               POOL_DEBUG(SAT_DEBUG_STATS, "installing recommended %s\n", solvable2str(pool, pool->solvables + p));
2657               queue_push(&solv->recommendations, p);
2658               level = setpropagatelearn(solv, level, p, 0);
2659               continue;
2660             }
2661         }
2662
2663      if (solv->solution_callback)
2664         {
2665           solv->solution_callback(solv, solv->solution_callback_data);
2666           if (solv->branches.count)
2667             {
2668               int i = solv->branches.count - 1;
2669               int l = -solv->branches.elements[i];
2670               for (; i > 0; i--)
2671                 if (solv->branches.elements[i - 1] < 0)
2672                   break;
2673               p = solv->branches.elements[i];
2674               POOL_DEBUG(SAT_DEBUG_STATS, "branching with %s\n", solvable2str(pool, pool->solvables + p));
2675               queue_empty(&dq);
2676               for (j = i + 1; j < solv->branches.count; j++)
2677                 queue_push(&dq, solv->branches.elements[j]);
2678               solv->branches.count = i;
2679               level = l;
2680               revert(solv, level);
2681               if (dq.count > 1)
2682                 for (j = 0; j < dq.count; j++)
2683                   queue_push(&solv->branches, dq.elements[j]);
2684               olevel = level;
2685               level = setpropagatelearn(solv, level, p, disablerules);
2686               if (level == 0)
2687                 {
2688                   queue_free(&dq);
2689                   return;
2690                 }
2691               continue;
2692             }
2693           /* all branches done, we're finally finished */
2694           break;
2695         }
2696
2697       /* minimization step */
2698      if (solv->branches.count)
2699         {
2700           int l = 0, lasti = -1, lastl = -1;
2701           p = 0;
2702           for (i = solv->branches.count - 1; i >= 0; i--)
2703             {
2704               p = solv->branches.elements[i];
2705               if (p < 0)
2706                 l = -p;
2707               else if (p > 0 && solv->decisionmap[p] > l + 1)
2708                 {
2709                   lasti = i;
2710                   lastl = l;
2711                 }
2712             }
2713           if (lasti >= 0)
2714             {
2715               /* kill old solvable so that we do not loop */
2716               p = solv->branches.elements[lasti];
2717               solv->branches.elements[lasti] = 0;
2718               POOL_DEBUG(SAT_DEBUG_STATS, "minimizing %d -> %d with %s\n", solv->decisionmap[p], l, solvable2str(pool, pool->solvables + p));
2719
2720               level = lastl;
2721               revert(solv, level);
2722               olevel = level;
2723               level = setpropagatelearn(solv, level, p, disablerules);
2724               if (level == 0)
2725                 {
2726                   queue_free(&dq);
2727                   return;
2728                 }
2729               continue;
2730             }
2731         }
2732       break;
2733     }
2734   POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
2735
2736   POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
2737   queue_free(&dq);
2738 }
2739
2740
2741 /*-------------------------------------------------------------------
2742  *
2743  * refine_suggestion
2744  *
2745  * at this point, all rules that led to conflicts are disabled.
2746  * we re-enable all rules of a problem set but rule "sug", then
2747  * continue to disable more rules until there as again a solution.
2748  */
2749
2750 /* FIXME: think about conflicting assertions */
2751
2752 static void
2753 refine_suggestion(Solver *solv, Queue *job, Id *problem, Id sug, Queue *refined)
2754 {
2755   Pool *pool = solv->pool;
2756   int i, j;
2757   Id v;
2758   Queue disabled;
2759   int disabledcnt;
2760
2761   IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2762     {
2763       POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion start\n");
2764       for (i = 0; problem[i]; i++)
2765         {
2766           if (problem[i] == sug)
2767             POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "=> ");
2768           solver_printproblem(solv, problem[i]);
2769         }
2770     }
2771   queue_init(&disabled);
2772   queue_empty(refined);
2773   queue_push(refined, sug);
2774
2775   /* re-enable all problem rules with the exception of "sug"(gestion) */
2776   revert(solv, 1);
2777   reset_solver(solv);
2778
2779   for (i = 0; problem[i]; i++)
2780     if (problem[i] != sug)
2781       enableproblem(solv, problem[i]);
2782
2783   if (sug < 0)
2784     disableupdaterules(solv, job, -(sug + 1));
2785   else if (sug >= solv->updaterules && sug < solv->updaterules_end)
2786     {
2787       /* enable feature rule */
2788       Rule *r = solv->rules + solv->featurerules + (sug - solv->updaterules);
2789       if (r->p)
2790         enablerule(solv, r);
2791     }
2792
2793   enableweakrules(solv);
2794
2795   for (;;)
2796     {
2797       int njob, nfeature, nupdate;
2798       queue_empty(&solv->problems);
2799       revert(solv, 1);          /* XXX no longer needed? */
2800       reset_solver(solv);
2801
2802       if (!solv->problems.count)
2803         run_solver(solv, 0, 0);
2804
2805       if (!solv->problems.count)
2806         {
2807           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no more problems!\n");
2808           IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
2809             solver_printdecisions(solv);
2810           break;                /* great, no more problems */
2811         }
2812       disabledcnt = disabled.count;
2813       /* start with 1 to skip over proof index */
2814       njob = nfeature = nupdate = 0;
2815       for (i = 1; i < solv->problems.count - 1; i++)
2816         {
2817           /* ignore solutions in refined */
2818           v = solv->problems.elements[i];
2819           if (v == 0)
2820             break;      /* end of problem reached */
2821           for (j = 0; problem[j]; j++)
2822             if (problem[j] != sug && problem[j] == v)
2823               break;
2824           if (problem[j])
2825             continue;
2826           if (v >= solv->featurerules && v < solv->featurerules_end)
2827             nfeature++;
2828           else if (v > 0)
2829             nupdate++;
2830           else
2831             njob++;
2832           queue_push(&disabled, v);
2833         }
2834       if (disabled.count == disabledcnt)
2835         {
2836           /* no solution found, this was an invalid suggestion! */
2837           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "no solution found!\n");
2838           refined->count = 0;
2839           break;
2840         }
2841       if (!njob && nupdate && nfeature)
2842         {
2843           /* got only update rules, filter out feature rules */
2844           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "throwing away feature rules\n");
2845           for (i = j = disabledcnt; i < disabled.count; i++)
2846             {
2847               v = disabled.elements[i];
2848               if (v < solv->featurerules || v >= solv->featurerules_end)
2849                 disabled.elements[j++] = v;
2850             }
2851           disabled.count = j;
2852           nfeature = 0;
2853         }
2854       if (disabled.count == disabledcnt + 1)
2855         {
2856           /* just one suggestion, add it to refined list */
2857           v = disabled.elements[disabledcnt];
2858           if (!nfeature)
2859             queue_push(refined, v);     /* do not record feature rules */
2860           disableproblem(solv, v);
2861           if (v >= solv->updaterules && v < solv->updaterules_end)
2862             {
2863               Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
2864               if (r->p)
2865                 enablerule(solv, r);    /* enable corresponding feature rule */
2866             }
2867           if (v < 0)
2868             disableupdaterules(solv, job, -(v + 1));
2869         }
2870       else
2871         {
2872           /* more than one solution, disable all */
2873           /* do not push anything on refine list, as we do not know which solution to choose */
2874           /* thus, the user will get another problem if he selects this solution, where he
2875            * can choose the right one */
2876           IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
2877             {
2878               POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "more than one solution found:\n");
2879               for (i = disabledcnt; i < disabled.count; i++)
2880                 solver_printproblem(solv, disabled.elements[i]);
2881             }
2882           for (i = disabledcnt; i < disabled.count; i++)
2883             {
2884               v = disabled.elements[i];
2885               disableproblem(solv, v);
2886               if (v >= solv->updaterules && v < solv->updaterules_end)
2887                 {
2888                   Rule *r = solv->rules + (v - solv->updaterules + solv->featurerules);
2889                   if (r->p)
2890                     enablerule(solv, r);
2891                 }
2892             }
2893         }
2894     }
2895   /* all done, get us back into the same state as before */
2896   /* enable refined rules again */
2897   for (i = 0; i < disabled.count; i++)
2898     enableproblem(solv, disabled.elements[i]);
2899   /* disable problem rules again */
2900
2901   /* FIXME! */
2902   for (i = 0; problem[i]; i++)
2903     enableproblem(solv, problem[i]);
2904   disableupdaterules(solv, job, -1);
2905
2906   /* disable problem rules again */
2907   for (i = 0; problem[i]; i++)
2908     disableproblem(solv, problem[i]);
2909   POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "refine_suggestion end\n");
2910 }
2911
2912
2913 /*-------------------------------------------------------------------
2914  * sorting helper for problems
2915  */
2916
2917 static int
2918 problems_sortcmp(const void *ap, const void *bp)
2919 {
2920   Id a = *(Id *)ap, b = *(Id *)bp;
2921   if (a < 0 && b > 0)
2922     return 1;
2923   if (a > 0 && b < 0)
2924     return -1;
2925   return a - b;
2926 }
2927
2928
2929 /*-------------------------------------------------------------------
2930  * sort problems
2931  */
2932
2933 static void
2934 problems_sort(Solver *solv)
2935 {
2936   int i, j;
2937   if (!solv->problems.count)
2938     return;
2939   for (i = j = 1; i < solv->problems.count; i++)
2940     {
2941       if (!solv->problems.elements[i])
2942         {
2943           if (i > j + 1)
2944             qsort(solv->problems.elements + j, i - j, sizeof(Id), problems_sortcmp);
2945           if (++i == solv->problems.count)
2946             break;
2947           j = i + 1;
2948         }
2949     }
2950 }
2951
2952
2953 /*-------------------------------------------------------------------
2954  * convert problems to solutions
2955  */
2956
2957 static void
2958 problems_to_solutions(Solver *solv, Queue *job)
2959 {
2960   Pool *pool = solv->pool;
2961   Queue problems;
2962   Queue solution;
2963   Queue solutions;
2964   Id *problem;
2965   Id why;
2966   int i, j, nsol;
2967
2968   if (!solv->problems.count)
2969     return;
2970   problems_sort(solv);
2971   queue_clone(&problems, &solv->problems);
2972   queue_init(&solution);
2973   queue_init(&solutions);
2974   /* copy over proof index */
2975   queue_push(&solutions, problems.elements[0]);
2976   problem = problems.elements + 1;
2977   for (i = 1; i < problems.count; i++)
2978     {
2979       Id v = problems.elements[i];
2980       if (v == 0)
2981         {
2982           /* mark end of this problem */
2983           queue_push(&solutions, 0);
2984           queue_push(&solutions, 0);
2985           if (i + 1 == problems.count)
2986             break;
2987           /* copy over proof of next problem */
2988           queue_push(&solutions, problems.elements[i + 1]);
2989           i++;
2990           problem = problems.elements + i + 1;
2991           continue;
2992         }
2993       refine_suggestion(solv, job, problem, v, &solution);
2994       if (!solution.count)
2995         continue;       /* this solution didn't work out */
2996
2997       nsol = 0;
2998       for (j = 0; j < solution.count; j++)
2999         {
3000           why = solution.elements[j];
3001           /* must be either job descriptor or update rule */
3002           assert(why < 0 || (why >= solv->updaterules && why < solv->updaterules_end));
3003 #if 0
3004           solver_printproblem(solv, why);
3005 #endif
3006           if (why < 0)
3007             {
3008               /* job descriptor */
3009               queue_push(&solutions, 0);
3010               queue_push(&solutions, -why);
3011             }
3012           else
3013             {
3014               /* update rule, find replacement package */
3015               Id p, d, *dp, rp = 0;
3016               Rule *rr;
3017               p = solv->installed->start + (why - solv->updaterules);
3018               if (solv->decisionmap[p] > 0)
3019                 continue;       /* false alarm, turned out we can keep the package */
3020               rr = solv->rules + solv->featurerules + (why - solv->updaterules);
3021               if (!rr->p)
3022                 rr = solv->rules + why;
3023               if (rr->w2)
3024                 {
3025                   d = rr->d < 0 ? -rr->d - 1 : rr->d;
3026                   if (!d)
3027                     {
3028                       if (solv->decisionmap[rr->w2] > 0 && pool->solvables[rr->w2].repo != solv->installed)
3029                         rp = rr->w2;
3030                     }
3031                   else
3032                     {
3033                       for (dp = pool->whatprovidesdata + d; *dp; dp++)
3034                         {
3035                           if (solv->decisionmap[*dp] > 0 && pool->solvables[*dp].repo != solv->installed)
3036                             {
3037                               rp = *dp;
3038                               break;
3039                             }
3040                         }
3041                     }
3042                 }
3043               queue_push(&solutions, p);
3044               queue_push(&solutions, rp);
3045             }
3046           nsol++;
3047         }
3048       /* mark end of this solution */
3049       if (nsol)
3050         {
3051           queue_push(&solutions, 0);
3052           queue_push(&solutions, 0);
3053         }
3054       else
3055         {
3056           POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "Oops, everything was fine?\n");
3057         }
3058     }
3059   queue_free(&solution);
3060   queue_free(&problems);
3061   /* copy queue over to solutions */
3062   queue_free(&solv->problems);
3063   queue_clone(&solv->problems, &solutions);
3064
3065   /* bring solver back into problem state */
3066   revert(solv, 1);              /* XXX move to reset_solver? */
3067   reset_solver(solv);
3068
3069   assert(solv->problems.count == solutions.count);
3070   queue_free(&solutions);
3071 }
3072
3073
3074 /*-------------------------------------------------------------------
3075  *
3076  * problem iterator
3077  *
3078  * advance to next problem
3079  */
3080
3081 Id
3082 solver_next_problem(Solver *solv, Id problem)
3083 {
3084   Id *pp;
3085   if (problem == 0)
3086     return solv->problems.count ? 1 : 0;
3087   pp = solv->problems.elements + problem;
3088   while (pp[0] || pp[1])
3089     {
3090       /* solution */
3091       pp += 2;
3092       while (pp[0] || pp[1])
3093         pp += 2;
3094       pp += 2;
3095     }
3096   pp += 2;
3097   problem = pp - solv->problems.elements;
3098   if (problem >= solv->problems.count)
3099     return 0;
3100   return problem + 1;
3101 }
3102
3103
3104 /*-------------------------------------------------------------------
3105  *
3106  * solution iterator
3107  */
3108
3109 Id
3110 solver_next_solution(Solver *solv, Id problem, Id solution)
3111 {
3112   Id *pp;
3113   if (solution == 0)
3114     {
3115       solution = problem;
3116       pp = solv->problems.elements + solution;
3117       return pp[0] || pp[1] ? solution : 0;
3118     }
3119   pp = solv->problems.elements + solution;
3120   while (pp[0] || pp[1])
3121     pp += 2;
3122   pp += 2;
3123   solution = pp - solv->problems.elements;
3124   return pp[0] || pp[1] ? solution : 0;
3125 }
3126
3127
3128 /*-------------------------------------------------------------------
3129  *
3130  * solution element iterator
3131  */
3132
3133 Id
3134 solver_next_solutionelement(Solver *solv, Id problem, Id solution, Id element, Id *p, Id *rp)
3135 {
3136   Id *pp;
3137   element = element ? element + 2 : solution;
3138   pp = solv->problems.elements + element;
3139   if (!(pp[0] || pp[1]))
3140     return 0;
3141   *p = pp[0];
3142   *rp = pp[1];
3143   return element;
3144 }
3145
3146
3147 /*-------------------------------------------------------------------
3148  *
3149  * Retrieve information about a problematic rule
3150  *
3151  * this is basically the reverse of addrpmrulesforsolvable
3152  */
3153
3154 SolverProbleminfo
3155 solver_problemruleinfo(Solver *solv, Queue *job, Id rid, Id *depp, Id *sourcep, Id *targetp)
3156 {
3157   Pool *pool = solv->pool;
3158   Repo *installed = solv->installed;
3159   Rule *r;
3160   Solvable *s;
3161   int dontfix = 0;
3162   Id p, d, *pp, req, *reqp, con, *conp, obs, *obsp, *dp;
3163
3164   assert(rid > 0);
3165   if (rid >= solv->jobrules && rid < solv->jobrules_end)
3166     {
3167
3168       r = solv->rules + rid;
3169       p = solv->ruletojob.elements[rid - solv->jobrules];
3170       *depp = job->elements[p + 1];
3171       *sourcep = p;
3172       *targetp = job->elements[p];
3173       d = r->d < 0 ? -r->d - 1 : r->d;
3174       if (d == 0 && r->w2 == 0 && r->p == -SYSTEMSOLVABLE && job->elements[p] != SOLVER_INSTALL_SOLVABLE_ONE_OF)
3175         return SOLVER_PROBLEM_JOB_NOTHING_PROVIDES_DEP;
3176       return SOLVER_PROBLEM_JOB_RULE;
3177     }
3178   if (rid >= solv->updaterules && rid < solv->updaterules_end)
3179     {
3180       *depp = 0;
3181       *sourcep = solv->installed->start + (rid - solv->updaterules);
3182       *targetp = 0;
3183       return SOLVER_PROBLEM_UPDATE_RULE;
3184     }
3185   assert(rid < solv->rpmrules_end);
3186   r = solv->rules + rid;
3187   assert(r->p < 0);
3188   d = r->d < 0 ? -r->d - 1 : r->d;
3189   if (d == 0 && r->w2 == 0)
3190     {
3191       /* a rpm rule assertion */
3192       s = pool->solvables - r->p;
3193       if (installed && !solv->fixsystem && s->repo == installed)
3194         dontfix = 1;
3195       assert(!dontfix); /* dontfix packages never have a neg assertion */
3196       *sourcep = -r->p;
3197       *targetp = 0;
3198       /* see why the package is not installable */
3199       if (s->arch != ARCH_SRC && s->arch != ARCH_NOSRC && !pool_installable(pool, s))
3200         {
3201           *depp = 0;
3202           return SOLVER_PROBLEM_NOT_INSTALLABLE;
3203         }
3204       /* check requires */
3205       if (s->requires)
3206         {
3207           reqp = s->repo->idarraydata + s->requires;
3208           while ((req = *reqp++) != 0)
3209             {
3210               if (req == SOLVABLE_PREREQMARKER)
3211                 continue;
3212               dp = pool_whatprovides(pool, req);
3213               if (*dp == 0)
3214                 break;
3215             }
3216           if (req)
3217             {
3218               *depp = req;
3219               return SOLVER_PROBLEM_NOTHING_PROVIDES_DEP;
3220             }
3221         }
3222       if (!solv->allowselfconflicts && s->conflicts)
3223         {
3224           conp = s->repo->idarraydata + s->conflicts;
3225           while ((con = *conp++) != 0)
3226             FOR_PROVIDES(p, pp, con)
3227               if (p == -r->p)
3228                 {
3229                   *depp = con;
3230                   return SOLVER_PROBLEM_SELF_CONFLICT;
3231                 }
3232         }
3233       /* should never happen */
3234       *depp = 0;
3235       return SOLVER_PROBLEM_RPM_RULE;
3236     }
3237   s = pool->solvables - r->p;
3238   if (installed && !solv->fixsystem && s->repo == installed)
3239     dontfix = 1;
3240   if (d == 0 && r->w2 < 0)
3241     {
3242       /* a package conflict */
3243       Solvable *s2 = pool->solvables - r->w2;
3244       int dontfix2 = 0;
3245
3246       if (installed && !solv->fixsystem && s2->repo == installed)
3247         dontfix2 = 1;
3248
3249       /* if both packages have the same name and at least one of them
3250        * is not installed, they conflict */
3251       if (s->name == s2->name && !(installed && s->repo == installed && s2->repo == installed))
3252         {
3253           /* also check noobsoletes map */
3254           if ((s->evr == s2->evr && s->arch == s2->arch) || !solv->noobsoletes.size
3255                 || ((!installed || s->repo != installed) && !MAPTST(&solv->noobsoletes, -r->p))
3256                 || ((!installed || s2->repo != installed) && !MAPTST(&solv->noobsoletes, -r->w2)))
3257             {
3258               *depp = 0;
3259               *sourcep = -r->p;
3260               *targetp = -r->w2;
3261               return SOLVER_PROBLEM_SAME_NAME;
3262             }
3263         }
3264
3265       /* check conflicts in both directions */
3266       if (s->conflicts)
3267         {
3268           conp = s->repo->idarraydata + s->conflicts;
3269           while ((con = *conp++) != 0)
3270             {
3271               FOR_PROVIDES(p, pp, con)
3272                 {
3273                   if (dontfix && pool->solvables[p].repo == installed)
3274                     continue;
3275                   if (p != -r->w2)
3276                     continue;
3277                   *depp = con;
3278                   *sourcep = -r->p;
3279                   *targetp = p;
3280                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3281                 }
3282             }
3283         }
3284       if (s2->conflicts)
3285         {
3286           conp = s2->repo->idarraydata + s2->conflicts;
3287           while ((con = *conp++) != 0)
3288             {
3289               FOR_PROVIDES(p, pp, con)
3290                 {
3291                   if (dontfix2 && pool->solvables[p].repo == installed)
3292                     continue;
3293                   if (p != -r->p)
3294                     continue;
3295                   *depp = con;
3296                   *sourcep = -r->w2;
3297                   *targetp = p;
3298                   return SOLVER_PROBLEM_PACKAGE_CONFLICT;
3299                 }
3300             }
3301         }
3302       /* check obsoletes in both directions */
3303       if ((!installed || s->repo != installed) && s->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3304         {
3305           obsp = s->repo->idarraydata + s->obsoletes;
3306           while ((obs = *obsp++) != 0)
3307             {
3308               FOR_PROVIDES(p, pp, obs)
3309                 {
3310                   if (p != -r->w2)
3311                     continue;
3312                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3313                     continue;
3314                   *depp = obs;
3315                   *sourcep = -r->p;
3316                   *targetp = p;
3317                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3318                 }
3319             }
3320         }
3321       if ((!installed || s2->repo != installed) && s2->obsoletes && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->w2)))
3322         {
3323           obsp = s2->repo->idarraydata + s2->obsoletes;
3324           while ((obs = *obsp++) != 0)
3325             {
3326               FOR_PROVIDES(p, pp, obs)
3327                 {
3328                   if (p != -r->p)
3329                     continue;
3330                   if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3331                     continue;
3332                   *depp = obs;
3333                   *sourcep = -r->w2;
3334                   *targetp = p;
3335                   return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3336                 }
3337             }
3338         }
3339       if (solv->implicitobsoleteusesprovides && (!installed || s->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->p)))
3340         {
3341           FOR_PROVIDES(p, pp, s->name)
3342             {
3343               if (p != -r->w2)
3344                 continue;
3345               *depp = s->name;
3346               *sourcep = -r->p;
3347               *targetp = p;
3348               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3349             }
3350         }
3351       if (solv->implicitobsoleteusesprovides && (!installed || s2->repo != installed) && !(solv->noobsoletes.size && MAPTST(&solv->noobsoletes, -r->w2)))
3352         {
3353           FOR_PROVIDES(p, pp, s2->name)
3354             {
3355               if (p != -r->p)
3356                 continue;
3357               *depp = s2->name;
3358               *sourcep = -r->w2;
3359               *targetp = p;
3360               return SOLVER_PROBLEM_PACKAGE_OBSOLETES;
3361             }
3362         }
3363       /* all cases checked, can't happen */
3364       *depp = 0;
3365       *sourcep = -r->p;
3366       *targetp = 0;
3367       return SOLVER_PROBLEM_RPM_RULE;
3368     }
3369   /* simple requires */
3370   if (s->requires)
3371     {
3372       reqp = s->repo->idarraydata + s->requires;
3373       while ((req = *reqp++) != 0)
3374         {
3375           if (req == SOLVABLE_PREREQMARKER)
3376             continue;
3377           dp = pool_whatprovides(pool, req);
3378           if (d == 0)
3379             {
3380               if (*dp == r->w2 && dp[1] == 0)
3381                 break;
3382             }
3383           else if (dp - pool->whatprovidesdata == d)
3384             break;
3385         }
3386       if (req)
3387         {
3388           *depp = req;
3389           *sourcep = -r->p;
3390           *targetp = 0;
3391           return SOLVER_PROBLEM_DEP_PROVIDERS_NOT_INSTALLABLE;
3392         }
3393     }
3394   /* all cases checked, can't happen */
3395   *depp = 0;
3396   *sourcep = -r->p;
3397   *targetp = 0;
3398   return SOLVER_PROBLEM_RPM_RULE;
3399 }
3400
3401
3402 /*-------------------------------------------------------------------
3403  *
3404  * find problem rule
3405  */
3406
3407 static void
3408 findproblemrule_internal(Solver *solv, Id idx, Id *reqrp, Id *conrp, Id *sysrp, Id *jobrp)
3409 {
3410   Id rid, d;
3411   Id lreqr, lconr, lsysr, ljobr;
3412   Rule *r;
3413   int reqassert = 0;
3414
3415   lreqr = lconr = lsysr = ljobr = 0;
3416   while ((rid = solv->learnt_pool.elements[idx++]) != 0)
3417     {
3418       assert(rid > 0);
3419       if (rid >= solv->learntrules)
3420         findproblemrule_internal(solv, solv->learnt_why.elements[rid - solv->learntrules], &lreqr, &lconr, &lsysr, &ljobr);
3421       else if (rid >= solv->jobrules && rid < solv->jobrules_end)
3422         {
3423           if (!*jobrp)
3424             *jobrp = rid;
3425         }
3426       else if (rid >= solv->updaterules && rid < solv->updaterules_end)
3427         {
3428           if (!*sysrp)
3429             *sysrp = rid;
3430         }
3431       else
3432         {
3433           assert(rid < solv->rpmrules_end);
3434           r = solv->rules + rid;
3435           d = r->d < 0 ? -r->d - 1 : r->d;
3436           if (!d && r->w2 < 0)
3437             {
3438               if (!*conrp)
3439                 *conrp = rid;
3440             }
3441           else
3442             {
3443               if (!d && r->w2 == 0 && !reqassert)
3444                 {
3445                   /* prefer assertions (XXX: bad idea?) */
3446                   *reqrp = rid;
3447                   reqassert = 1;
3448                 }
3449               if (!*reqrp)
3450                 *reqrp = rid;
3451               else if (solv->installed && r->p < 0 && solv->pool->solvables[-r->p].repo == solv->installed)
3452                 {
3453                   /* prefer rules of installed packages */
3454                   Id op = *reqrp >= 0 ? solv->rules[*reqrp].p : -*reqrp;
3455                   if (op <= 0 || solv->pool->solvables[op].repo != solv->installed)
3456                     *reqrp = rid;
3457                 }
3458             }
3459         }
3460     }
3461   if (!*reqrp && lreqr)
3462     *reqrp = lreqr;
3463   if (!*conrp && lconr)
3464     *conrp = lconr;
3465   if (!*jobrp && ljobr)
3466     *jobrp = ljobr;
3467   if (!*sysrp && lsysr)
3468     *sysrp = lsysr;
3469 }
3470
3471
3472 /*-------------------------------------------------------------------
3473  *
3474  * find problem rule
3475  *
3476  * search for a rule that describes the problem to the
3477  * user. A pretty hopeless task, actually. We currently
3478  * prefer simple requires.
3479  */
3480
3481 Id
3482 solver_findproblemrule(Solver *solv, Id problem)
3483 {
3484   Id reqr, conr, sysr, jobr;
3485   Id idx = solv->problems.elements[problem - 1];
3486   reqr = conr = sysr = jobr = 0;
3487   findproblemrule_internal(solv, idx, &reqr, &conr, &sysr, &jobr);
3488   if (reqr)
3489     return reqr;
3490   if (conr)
3491     return conr;
3492   if (sysr)
3493     return sysr;
3494   if (jobr)
3495     return jobr;
3496   assert(0);
3497 }
3498
3499
3500 /*-------------------------------------------------------------------
3501  *
3502  * create reverse obsoletes map for installed solvables
3503  *
3504  * for each installed solvable find which packages with *different* names
3505  * obsolete the solvable.
3506  * this index is used in policy_findupdatepackages if noupdateprovide is set.
3507  */
3508
3509 static void
3510 create_obsolete_index(Solver *solv)
3511 {
3512   Pool *pool = solv->pool;
3513   Solvable *s;
3514   Repo *installed = solv->installed;
3515   Id p, *pp, obs, *obsp, *obsoletes, *obsoletes_data;
3516   int i, n;
3517
3518   if (!installed || !installed->nsolvables)
3519     return;
3520   solv->obsoletes = obsoletes = sat_calloc(installed->end - installed->start, sizeof(Id));
3521   for (i = 1; i < pool->nsolvables; i++)
3522     {
3523       s = pool->solvables + i;
3524       if (!s->obsoletes)
3525         continue;
3526       if (!pool_installable(pool, s))
3527         continue;
3528       obsp = s->repo->idarraydata + s->obsoletes;
3529       while ((obs = *obsp++) != 0)
3530         {
3531           FOR_PROVIDES(p, pp, obs)
3532             {
3533               if (pool->solvables[p].repo != installed)
3534                 continue;
3535               if (pool->solvables[p].name == s->name)
3536                 continue;
3537               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3538                 continue;
3539               obsoletes[p - installed->start]++;
3540             }
3541         }
3542     }
3543   n = 0;
3544   for (i = 0; i < installed->nsolvables; i++)
3545     if (obsoletes[i])
3546       {
3547         n += obsoletes[i] + 1;
3548         obsoletes[i] = n;
3549       }
3550   solv->obsoletes_data = obsoletes_data = sat_calloc(n + 1, sizeof(Id));
3551   POOL_DEBUG(SAT_DEBUG_STATS, "obsoletes data: %d entries\n", n + 1);
3552   for (i = pool->nsolvables - 1; i > 0; i--)
3553     {
3554       s = pool->solvables + i;
3555       if (!s->obsoletes)
3556         continue;
3557       if (!pool_installable(pool, s))
3558         continue;
3559       obsp = s->repo->idarraydata + s->obsoletes;
3560       while ((obs = *obsp++) != 0)
3561         {
3562           FOR_PROVIDES(p, pp, obs)
3563             {
3564               if (pool->solvables[p].repo != installed)
3565                 continue;
3566               if (pool->solvables[p].name == s->name)
3567                 continue;
3568               if (!solv->obsoleteusesprovides && !pool_match_nevr(pool, pool->solvables + p, obs))
3569                 continue;
3570               p -= installed->start;
3571               if (obsoletes_data[obsoletes[p]] != i)
3572                 obsoletes_data[--obsoletes[p]] = i;
3573             }
3574         }
3575     }
3576 }
3577
3578
3579 /*-------------------------------------------------------------------
3580  *
3581  * remove disabled conflicts
3582  */
3583
3584 static void
3585 removedisabledconflicts(Solver *solv, Queue *removed)
3586 {
3587   Pool *pool = solv->pool;
3588   int i, n;
3589   Id p, why, *dp;
3590   Id new;
3591   Rule *r;
3592   Id *decisionmap = solv->decisionmap;
3593
3594   POOL_DEBUG(SAT_DEBUG_STATS, "removedisabledconflicts\n");
3595   queue_empty(removed);
3596   for (i = 0; i < solv->decisionq.count; i++)
3597     {
3598       p = solv->decisionq.elements[i];
3599       if (p > 0)
3600         continue;
3601       /* a conflict. we never do conflicts on free decisions, so there
3602        * must have been an unit rule */
3603       why = solv->decisionq_why.elements[i];
3604       assert(why > 0);
3605       r = solv->rules + why;
3606       if (r->d < 0 && decisionmap[-p])
3607         {
3608           /* rule is now disabled, remove from decisionmap */
3609           POOL_DEBUG(SAT_DEBUG_STATS, "removing conflict for package %s[%d]\n", solvable2str(pool, pool->solvables - p), -p);
3610           queue_push(removed, -p);
3611           queue_push(removed, decisionmap[-p]);
3612           decisionmap[-p] = 0;
3613         }
3614     }
3615   if (!removed->count)
3616     return;
3617   /* we removed some confliced packages. some of them might still
3618    * be in conflict, so search for unit rules and re-conflict */
3619   new = 0;
3620   for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
3621     {
3622       if (i == solv->nrules)
3623         {
3624           i = 1;
3625           r = solv->rules + i;
3626         }
3627       if (r->d < 0)
3628         continue;
3629       if (!r->w2)
3630         {
3631           if (r->p < 0 && !decisionmap[-r->p])
3632             new = r->p;
3633         }
3634       else if (!r->d)
3635         {
3636           /* binary rule */
3637           if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
3638             new = r->p;
3639           else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
3640             new = r->w2;
3641         }
3642       else
3643         {
3644           if (r->p < 0 && decisionmap[-r->p] == 0)
3645             new = r->p;
3646           if (new || DECISIONMAP_FALSE(r->p))
3647             {
3648               dp = pool->whatprovidesdata + r->d;
3649               while ((p = *dp++) != 0)
3650                 {
3651                   if (new && p == new)
3652                     continue;
3653                   if (p < 0 && decisionmap[-p] == 0)
3654                     {
3655                       if (new)
3656                         {
3657                           new = 0;
3658                           break;
3659                         }
3660                       new = p;
3661                     }
3662                   else if (!DECISIONMAP_FALSE(p))
3663                     {
3664                       new = 0;
3665                       break;
3666                     }
3667                 }
3668             }
3669         }
3670       if (new)
3671         {
3672           POOL_DEBUG(SAT_DEBUG_STATS, "re-conflicting package %s[%d]\n", solvable2str(pool, pool->solvables - new), -new);
3673           decisionmap[-new] = -1;
3674           new = 0;
3675           n = 0;        /* redo all rules */
3676         }
3677     }
3678 }
3679
3680
3681 /*-------------------------------------------------------------------
3682  *
3683  * weaken solvable dependencies
3684  */
3685
3686 static void
3687 weaken_solvable_deps(Solver *solv, Id p)
3688 {
3689   int i;
3690   Rule *r;
3691
3692   for (i = 1, r = solv->rules + i; i < solv->featurerules; i++, r++)
3693     {
3694       if (r->p != -p)
3695         continue;
3696       if ((r->d == 0 || r->d == -1) && r->w2 < 0)
3697         continue;       /* conflict */
3698       queue_push(&solv->weakruleq, i);
3699     }
3700 }
3701
3702 /********************************************************************/
3703 /* main() */
3704
3705 /*
3706  *
3707  * solve job queue
3708  *
3709  */
3710
3711 void
3712 solver_solve(Solver *solv, Queue *job)
3713 {
3714   Pool *pool = solv->pool;
3715   Repo *installed = solv->installed;
3716   int i;
3717   int oldnrules;
3718   Map addedmap;                /* '1' == have rpm-rules for solvable */
3719   Id how, what, weak, p, *pp, d;
3720   Queue q, redoq;
3721   Solvable *s;
3722   int goterase;
3723   Rule *r;
3724
3725   /* create whatprovides if not already there */
3726   if (!pool->whatprovides)
3727     pool_createwhatprovides(pool);
3728
3729   /* create obsolete index if needed */
3730   if (solv->noupdateprovide)
3731     create_obsolete_index(solv);
3732
3733   /*
3734    * create basic rule set of all involved packages
3735    * use addedmap bitmap to make sure we don't create rules twice
3736    *
3737    */
3738
3739   /* create noobsolete map if needed */
3740   for (i = 0; i < job->count; i += 2)
3741     {
3742       how = job->elements[i] & ~SOLVER_WEAK;
3743       what = job->elements[i + 1];
3744       switch(how)
3745         {
3746         case SOLVER_NOOBSOLETES_SOLVABLE:
3747         case SOLVER_NOOBSOLETES_SOLVABLE_NAME:
3748         case SOLVER_NOOBSOLETES_SOLVABLE_PROVIDES:
3749           if (!solv->noobsoletes.size)
3750             map_init(&solv->noobsoletes, pool->nsolvables);
3751           if (how == SOLVER_NOOBSOLETES_SOLVABLE)
3752             {
3753               MAPSET(&solv->noobsoletes, what);
3754               break;
3755             }
3756           FOR_PROVIDES(p, pp, what)
3757             {
3758               if (how == SOLVER_NOOBSOLETES_SOLVABLE_NAME && !pool_match_nevr(pool, pool->solvables + p, what))
3759                 continue;
3760               MAPSET(&solv->noobsoletes, p);
3761             }
3762           break;
3763         default:
3764           break;
3765         }
3766     }
3767
3768   map_init(&addedmap, pool->nsolvables);
3769   queue_init(&q);
3770
3771   /*
3772    * always install our system solvable
3773    */
3774   MAPSET(&addedmap, SYSTEMSOLVABLE);
3775   queue_push(&solv->decisionq, SYSTEMSOLVABLE);
3776   queue_push(&solv->decisionq_why, 0);
3777   solv->decisionmap[SYSTEMSOLVABLE] = 1; /* installed at level '1' */
3778
3779   /*
3780    * create rules for all package that could be involved with the solving
3781    * so called: rpm rules
3782    *
3783    */
3784   if (installed)
3785     {
3786       oldnrules = solv->nrules;
3787       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
3788       FOR_REPO_SOLVABLES(installed, p, s)
3789         addrpmrulesforsolvable(solv, s, &addedmap);
3790       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
3791       POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
3792       oldnrules = solv->nrules;
3793       FOR_REPO_SOLVABLES(installed, p, s)
3794         addrpmrulesforupdaters(solv, s, &addedmap, 1);
3795       POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
3796     }
3797
3798   /*
3799    * create rules for all packages involved in the job
3800    * (to be installed or removed)
3801    */
3802
3803   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
3804   oldnrules = solv->nrules;
3805   for (i = 0; i < job->count; i += 2)
3806     {
3807       how = job->elements[i] & ~SOLVER_WEAK;
3808       what = job->elements[i + 1];
3809
3810       switch(how)
3811         {
3812         case SOLVER_INSTALL_SOLVABLE:
3813           addrpmrulesforsolvable(solv, pool->solvables + what, &addedmap);
3814           break;
3815         case SOLVER_INSTALL_SOLVABLE_NAME:
3816         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
3817           FOR_PROVIDES(p, pp, what)
3818             {
3819               /* if by name, ensure that the name matches */
3820               if (how == SOLVER_INSTALL_SOLVABLE_NAME && !pool_match_nevr(pool, pool->solvables + p, what))
3821                 continue;
3822               addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3823             }
3824           break;
3825         case SOLVER_INSTALL_SOLVABLE_UPDATE:
3826           /* dont allow downgrade */
3827           addrpmrulesforupdaters(solv, pool->solvables + what, &addedmap, 0);
3828           break;
3829         case SOLVER_INSTALL_SOLVABLE_ONE_OF:
3830           pp = pool->whatprovidesdata + what;
3831           while ((p = *pp++) != 0)
3832             addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
3833           break;
3834         }
3835     }
3836   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
3837
3838   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for recommended/suggested packages ***\n");
3839
3840   oldnrules = solv->nrules;
3841
3842     /*
3843      * add rules for suggests, [freshens,] enhances
3844      */
3845   addrpmrulesforweak(solv, &addedmap);
3846   POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
3847
3848   IF_POOLDEBUG (SAT_DEBUG_STATS)
3849     {
3850       int possible = 0, installable = 0;
3851       for (i = 1; i < pool->nsolvables; i++)
3852         {
3853           if (pool_installable(pool, pool->solvables + i))
3854             installable++;
3855           if (MAPTST(&addedmap, i))
3856             possible++;
3857         }
3858       POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
3859     }
3860
3861   /*
3862    * first pass done, we now have all the rpm rules we need.
3863    * unify existing rules before going over all job rules and
3864    * policy rules.
3865    * at this point the system is always solvable,
3866    * as an empty system (remove all packages) is a valid solution
3867    */
3868
3869   unifyrules(solv);                               /* remove duplicate rpm rules */
3870
3871   solv->rpmrules_end = solv->nrules;              /* mark end of rpm rules */
3872
3873   solv->directdecisions = solv->decisionq.count;
3874   POOL_DEBUG(SAT_DEBUG_STATS, "decisions so far: %d\n", solv->decisionq.count);
3875
3876   /*
3877    * create feature rules
3878    *
3879    * foreach installed:
3880    *   create assertion (keep installed, if no update available)
3881    *   or
3882    *   create update rule (A|update1(A)|update2(A)|...)
3883    *
3884    * those are used later on to keep a version of the installed packages in
3885    * best effort mode
3886    */
3887
3888   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
3889   solv->featurerules = solv->nrules;              /* mark start of feature rules */
3890   if (installed)
3891     {
3892         /* foreach installed solvable */
3893       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3894         {
3895             /*
3896              * patterns use this
3897              */
3898
3899           if (s->freshens && !s->supplements)
3900             {
3901               const char *name = id2str(pool, s->name);
3902               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3903                 {
3904                   addrule(solv, 0, 0);
3905                   continue;
3906                 }
3907             }
3908
3909           if (s->repo != installed)
3910             {
3911               addrule(solv, 0, 0);      /* create dummy rule */
3912               continue;
3913             }
3914           addupdaterule(solv, s, 1);    /* allow s to be updated */
3915         }
3916         /*
3917          * assert one rule per installed solvable,
3918          * either an assertion (A)
3919          * or a possible update (A|update1(A)|update2(A)|...)
3920          */
3921       assert(solv->nrules - solv->featurerules == installed->end - installed->start);
3922     }
3923   solv->featurerules_end = solv->nrules;
3924
3925     /*
3926      * Add update rules for installed solvables
3927      *
3928      * almost identical to feature rules
3929      * except that downgrades are allowed
3930      */
3931
3932   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
3933   solv->updaterules = solv->nrules;
3934   if (installed)
3935     { /* foreach installed solvables */
3936       /* we create all update rules, but disable some later on depending on the job */
3937       for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
3938         {
3939           Rule *sr;
3940
3941 #if CODE10
3942           /* no update rules for patch atoms */
3943           if (s->freshens && !s->supplements)
3944             {
3945               const char *name = id2str(pool, s->name);
3946               if (name[0] == 'a' && !strncmp(name, "atom:", 5))
3947                 {
3948                   addrule(solv, 0, 0);
3949                   continue;
3950                 }
3951             }
3952 #endif
3953           if (s->repo != installed)
3954             {
3955               addrule(solv, 0, 0);      /* create dummy rule */
3956               continue;
3957             }
3958           addupdaterule(solv, s, 0);    /* allowall = 0: downgrades allowed */
3959
3960             /*
3961              * check for and remove duplicate
3962              */
3963
3964           r = solv->rules + solv->nrules - 1;           /* r: update rule */
3965           sr = r - (installed->end - installed->start); /* sr: feature rule */
3966           unifyrules_sortcmp_data = pool;
3967           if (!unifyrules_sortcmp(r, sr))
3968             {
3969               /* identical rule, kill unneeded rule */
3970               if (solv->allowuninstall)
3971                 {
3972                   /* keep feature rule */
3973                   memset(r, 0, sizeof(*r));
3974                   queue_push(&solv->weakruleq, sr - solv->rules);
3975                 }
3976               else
3977                 {
3978                   /* keep update rule */
3979                   memset(sr, 0, sizeof(*sr));
3980                 }
3981             }
3982           else if (solv->allowuninstall)
3983             {
3984               /* make both feature and update rule weak */
3985               queue_push(&solv->weakruleq, r - solv->rules);
3986               queue_push(&solv->weakruleq, sr - solv->rules);
3987             }
3988           else
3989             disablerule(solv, sr);
3990         }
3991       /* consistency check: we added a rule for _every_ installed solvable */
3992       assert(solv->nrules - solv->updaterules == installed->end - installed->start);
3993     }
3994   solv->updaterules_end = solv->nrules;
3995
3996
3997   /*
3998    * now add all job rules
3999    */
4000
4001   POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
4002
4003   solv->jobrules = solv->nrules;
4004   for (i = 0; i < job->count; i += 2)
4005     {
4006       oldnrules = solv->nrules;
4007
4008       how = job->elements[i] & ~SOLVER_WEAK;
4009       weak = job->elements[i] & SOLVER_WEAK;
4010       what = job->elements[i + 1];
4011       switch(how)
4012         {
4013         case SOLVER_INSTALL_SOLVABLE:                   /* install specific solvable */
4014           s = pool->solvables + what;
4015           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
4016           addrule(solv, what, 0);                       /* install by Id */
4017           queue_push(&solv->ruletojob, i);
4018           if (weak)
4019             queue_push(&solv->weakruleq, solv->nrules - 1);
4020           break;
4021         case SOLVER_ERASE_SOLVABLE:
4022           s = pool->solvables + what;
4023           POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase solvable %s\n", weak ? "weak " : "", solvable2str(pool, s));
4024           addrule(solv, -what, 0);                      /* remove by Id */
4025           queue_push(&solv->ruletojob, i);
4026           if (weak)
4027             queue_push(&solv->weakruleq, solv->nrules - 1);
4028           break;
4029         case SOLVER_INSTALL_SOLVABLE_NAME:              /* install by capability */
4030         case SOLVER_INSTALL_SOLVABLE_PROVIDES:
4031           if (how == SOLVER_INSTALL_SOLVABLE_NAME)
4032             POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall name %s\n", weak ? "weak " : "", dep2str(pool, what));
4033           if (how == SOLVER_INSTALL_SOLVABLE_PROVIDES)
4034             POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall provides %s\n", weak ? "weak " : "", dep2str(pool, what));
4035           queue_empty(&q);
4036           FOR_PROVIDES(p, pp, what)
4037             {
4038               /* if by name, ensure that the name matches */
4039               if (how == SOLVER_INSTALL_SOLVABLE_NAME && !pool_match_nevr(pool, pool->solvables + p, what))
4040                 continue;
4041               queue_push(&q, p);
4042             }
4043           if (!q.count)
4044             {
4045               /* no provider, make this an impossible rule */
4046               queue_push(&q, -SYSTEMSOLVABLE);
4047             }
4048
4049           p = queue_shift(&q);         /* get first provider */
4050           if (!q.count)
4051             d = 0;                     /* single provider ? -> make assertion */
4052           else
4053             d = pool_queuetowhatprovides(pool, &q);   /* get all providers */
4054           addrule(solv, p, d);         /* add 'requires' rule */
4055           queue_push(&solv->ruletojob, i);
4056           if (weak)
4057             queue_push(&solv->weakruleq, solv->nrules - 1);
4058           break;
4059         case SOLVER_ERASE_SOLVABLE_NAME:                  /* remove by capability */
4060         case SOLVER_ERASE_SOLVABLE_PROVIDES:
4061           if (how == SOLVER_ERASE_SOLVABLE_NAME)
4062             POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase name %s\n", weak ? "weak " : "", dep2str(pool, what));
4063           if (how == SOLVER_ERASE_SOLVABLE_PROVIDES)
4064             POOL_DEBUG(SAT_DEBUG_JOB, "job: %serase provides %s\n", weak ? "weak " : "", dep2str(pool, what));
4065           FOR_PROVIDES(p, pp, what)
4066             {
4067               /* if by name, ensure that the name matches */
4068               if (how == SOLVER_ERASE_SOLVABLE_NAME && !pool_match_nevr(pool, pool->solvables + p, what))
4069                 continue;
4070               addrule(solv, -p, 0);  /* add 'remove' rule */
4071               queue_push(&solv->ruletojob, i);
4072               if (weak)
4073                 queue_push(&solv->weakruleq, solv->nrules - 1);
4074             }
4075           break;
4076         case SOLVER_INSTALL_SOLVABLE_UPDATE:              /* find update for solvable */
4077           s = pool->solvables + what;
4078           POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solvable2str(pool, s));
4079           addupdaterule(solv, s, 0);
4080           queue_push(&solv->ruletojob, i);
4081           if (weak)
4082             queue_push(&solv->weakruleq, solv->nrules - 1);
4083           break;
4084         case SOLVER_INSTALL_SOLVABLE_ONE_OF:
4085           POOL_DEBUG(SAT_DEBUG_JOB, "job: %sone of\n", weak ? "weak " : "");
4086           for (pp = pool->whatprovidesdata + what; *pp; pp++)
4087             POOL_DEBUG(SAT_DEBUG_JOB, "  %s\n", solvable2str(pool, pool->solvables + *pp));
4088           addrule(solv, -SYSTEMSOLVABLE, what);
4089           queue_push(&solv->ruletojob, i);
4090           if (weak)
4091             queue_push(&solv->weakruleq, solv->nrules - 1);
4092           break;
4093         case SOLVER_WEAKEN_SOLVABLE_DEPS:
4094           s = pool->solvables + what;
4095           POOL_DEBUG(SAT_DEBUG_JOB, "job: weaken deps %s\n", solvable2str(pool, s));
4096           weaken_solvable_deps(solv, what);
4097           break;
4098         case SOLVER_NOOBSOLETES_SOLVABLE:
4099           POOL_DEBUG(SAT_DEBUG_JOB, "job: no obsolete %s\n", solvable2str(pool, pool->solvables + what));
4100           break;
4101         case SOLVER_NOOBSOLETES_SOLVABLE_NAME:
4102           POOL_DEBUG(SAT_DEBUG_JOB, "job: no obsolete name %s\n", dep2str(pool, what));
4103           break;
4104         case SOLVER_NOOBSOLETES_SOLVABLE_PROVIDES:
4105           POOL_DEBUG(SAT_DEBUG_JOB, "job: no obsolete provides %s\n", dep2str(pool, what));
4106           break;
4107         }
4108
4109         /*
4110          * debug
4111          */
4112
4113       IF_POOLDEBUG (SAT_DEBUG_JOB)
4114         {
4115           int j;
4116           if (solv->nrules == oldnrules)
4117             POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
4118           for (j = oldnrules; j < solv->nrules; j++)
4119             {
4120               POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
4121               solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
4122             }
4123         }
4124     }
4125   assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
4126   solv->jobrules_end = solv->nrules;
4127
4128     /* all rules created
4129      * --------------------------------------------------------------
4130      * prepare for solving
4131      */
4132
4133   /* free unneeded memory */
4134   map_free(&addedmap);
4135   queue_free(&q);
4136
4137   /* create weak map */
4138   map_init(&solv->weakrulemap, solv->nrules);
4139   for (i = 0; i < solv->weakruleq.count; i++)
4140     {
4141       p = solv->weakruleq.elements[i];
4142       MAPSET(&solv->weakrulemap, p);
4143     }
4144
4145   /* all new rules are learnt after this point */
4146   solv->learntrules = solv->nrules;
4147
4148   /* create assertion index. it is only used to speed up
4149    * makeruledecsions() a bit */
4150   for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
4151     if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
4152       queue_push(&solv->ruleassertions, i);
4153
4154   /* disable update rules that conflict with our job */
4155   disableupdaterules(solv, job, -1);
4156
4157   /* make decisions based on job/update assertions */
4158   makeruledecisions(solv);
4159
4160   /* create watches chains */
4161   makewatches(solv);
4162
4163   POOL_DEBUG(SAT_DEBUG_STATS, "problems so far: %d\n", solv->problems.count);
4164
4165   /*
4166    * ********************************************
4167    * solve!
4168    * ********************************************
4169    */
4170
4171   run_solver(solv, 1, solv->dontinstallrecommended ? 0 : 1);
4172
4173   queue_init(&redoq);
4174   goterase = 0;
4175   /* disable all erase jobs (including weak "keep uninstalled" rules) */
4176   for (i = solv->jobrules, r = solv->rules + i; i < solv->learntrules; i++, r++)
4177     {
4178       if (r->d < 0)     /* disabled ? */
4179         continue;
4180       if (r->p > 0)     /* install job? */
4181         continue;
4182       disablerule(solv, r);
4183       goterase++;
4184     }
4185
4186   if (goterase)
4187     {
4188       enabledisablelearntrules(solv);
4189       removedisabledconflicts(solv, &redoq);
4190     }
4191
4192   /*
4193    * find recommended packages
4194    */
4195
4196   /* if redoq.count == 0 we already found all recommended in the
4197    * solver run */
4198   if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended)
4199     {
4200       Id rec, *recp, p, *pp;
4201
4202       /* create map of all recommened packages */
4203       solv->recommends_index = -1;
4204       MAPZERO(&solv->recommendsmap);
4205       for (i = 0; i < solv->decisionq.count; i++)
4206         {
4207           p = solv->decisionq.elements[i];
4208           if (p < 0)
4209             continue;
4210           s = pool->solvables + p;
4211           if (s->recommends)
4212             {
4213               recp = s->repo->idarraydata + s->recommends;
4214               while ((rec = *recp++) != 0)
4215                 {
4216                   FOR_PROVIDES(p, pp, rec)
4217                     if (solv->decisionmap[p] > 0)
4218                       break;
4219                   if (p)
4220                     {
4221                       if (!solv->dontshowinstalledrecommended)
4222                         {
4223                           FOR_PROVIDES(p, pp, rec)
4224                             if (solv->decisionmap[p] > 0)
4225                               MAPSET(&solv->recommendsmap, p);
4226                         }
4227                       continue; /* p != 0: already fulfilled */
4228                     }
4229                   FOR_PROVIDES(p, pp, rec)
4230                     MAPSET(&solv->recommendsmap, p);
4231                 }
4232             }
4233         }
4234       for (i = 1; i < pool->nsolvables; i++)
4235         {
4236           if (solv->decisionmap[i] < 0)
4237             continue;
4238           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4239             continue;
4240           s = pool->solvables + i;
4241           if (!MAPTST(&solv->recommendsmap, i))
4242             {
4243               if (!s->supplements)
4244                 continue;
4245               if (!pool_installable(pool, s))
4246                 continue;
4247               if (!solver_is_supplementing(solv, s))
4248                 continue;
4249             }
4250           if (solv->dontinstallrecommended)
4251             queue_push(&solv->recommendations, i);
4252           else
4253             queue_pushunique(&solv->recommendations, i);
4254         }
4255       /* we use MODE_SUGGEST here so that repo prio is ignored */
4256       policy_filter_unwanted(solv, &solv->recommendations, 0, POLICY_MODE_SUGGEST);
4257     }
4258
4259   /*
4260    * find suggested packages
4261    */
4262
4263   if (1)
4264     {
4265       Id sug, *sugp, p, *pp;
4266
4267       /* create map of all suggests that are still open */
4268       solv->recommends_index = -1;
4269       MAPZERO(&solv->suggestsmap);
4270       for (i = 0; i < solv->decisionq.count; i++)
4271         {
4272           p = solv->decisionq.elements[i];
4273           if (p < 0)
4274             continue;
4275           s = pool->solvables + p;
4276           if (s->suggests)
4277             {
4278               sugp = s->repo->idarraydata + s->suggests;
4279               while ((sug = *sugp++) != 0)
4280                 {
4281                   FOR_PROVIDES(p, pp, sug)
4282                     if (solv->decisionmap[p] > 0)
4283                       break;
4284                   if (p)
4285                     {
4286                       if (!solv->dontshowinstalledrecommended)
4287                         {
4288                           FOR_PROVIDES(p, pp, sug)
4289                             if (solv->decisionmap[p] > 0)
4290                               MAPSET(&solv->suggestsmap, p);
4291                         }
4292                       continue; /* already fulfilled */
4293                     }
4294                   FOR_PROVIDES(p, pp, sug)
4295                     MAPSET(&solv->suggestsmap, p);
4296                 }
4297             }
4298         }
4299       for (i = 1; i < pool->nsolvables; i++)
4300         {
4301           if (solv->decisionmap[i] < 0)
4302             continue;
4303           if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
4304             continue;
4305           s = pool->solvables + i;
4306           if (!MAPTST(&solv->suggestsmap, i))
4307             {
4308               if (!s->enhances)
4309                 continue;
4310               if (!pool_installable(pool, s))
4311                 continue;
4312               if (!solver_is_enhancing(solv, s))
4313                 continue;
4314             }
4315           queue_push(&solv->suggestions, i);
4316         }
4317       policy_filter_unwanted(solv, &solv->suggestions, 0, POLICY_MODE_SUGGEST);
4318     }
4319
4320   if (redoq.count)
4321     {
4322       /* restore decisionmap */
4323       for (i = 0; i < redoq.count; i += 2)
4324         solv->decisionmap[redoq.elements[i]] = redoq.elements[i + 1];
4325     }
4326
4327     /*
4328      * if unsolvable, prepare solutions
4329      */
4330
4331   if (solv->problems.count)
4332     {
4333       int recocount = solv->recommendations.count;
4334       solv->recommendations.count = 0;  /* so that revert() doesn't mess with it */
4335       queue_empty(&redoq);
4336       for (i = 0; i < solv->decisionq.count; i++)
4337         {
4338           Id p = solv->decisionq.elements[i];
4339           queue_push(&redoq, p);
4340           queue_push(&redoq, solv->decisionq_why.elements[i]);
4341           queue_push(&redoq, solv->decisionmap[p > 0 ? p : -p]);
4342         }
4343       problems_to_solutions(solv, job);
4344       memset(solv->decisionmap, 0, pool->nsolvables * sizeof(Id));
4345       queue_empty(&solv->decisionq);
4346       queue_empty(&solv->decisionq_why);
4347       for (i = 0; i < redoq.count; i += 3)
4348         {
4349           Id p = redoq.elements[i];
4350           queue_push(&solv->decisionq, p);
4351           queue_push(&solv->decisionq_why, redoq.elements[i + 1]);
4352           solv->decisionmap[p > 0 ? p : -p] = redoq.elements[i + 2];
4353         }
4354       solv->recommendations.count = recocount;
4355     }
4356
4357   POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d learned rules, %d unsolvable\n", solv->stats_learned, solv->stats_unsolvable);
4358   queue_free(&redoq);
4359 }
4360
4361 /***********************************************************************/
4362 /* disk usage computations */
4363
4364 /*-------------------------------------------------------------------
4365  *
4366  * calculate DU changes
4367  */
4368
4369 void
4370 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
4371 {
4372   Map installedmap;
4373
4374   solver_create_state_maps(solv, &installedmap, 0);
4375   pool_calc_duchanges(solv->pool, solv->installed, &installedmap, mps, nmps);
4376   map_free(&installedmap);
4377 }
4378
4379
4380 /*-------------------------------------------------------------------
4381  *
4382  * calculate changes in install size
4383  */
4384
4385 int
4386 solver_calc_installsizechange(Solver *solv)
4387 {
4388   Map installedmap;
4389   int change;
4390
4391   solver_create_state_maps(solv, &installedmap, 0);
4392   change = pool_calc_installsizechange(solv->pool, solv->installed, &installedmap);
4393   map_free(&installedmap);
4394   return change;
4395 }
4396
4397 /* EOF */