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