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