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