00001
00002
00003
00004
00005
00006
00007
00008
00009
00010
00011
00012
00013
00014 #include <stdio.h>
00015 #include <stdlib.h>
00016 #include <unistd.h>
00017 #include <string.h>
00018 #include <assert.h>
00019
00020 #include "solver.h"
00021 #include "bitmap.h"
00022 #include "pool.h"
00023 #include "util.h"
00024 #include "policy.h"
00025 #include "solverdebug.h"
00026
00027 #define RULES_BLOCK 63
00028
00029
00030
00031
00032
00033
00034
00035
00036
00037
00038
00039 int
00040 solver_splitprovides(Solver *solv, Id dep)
00041 {
00042 Pool *pool = solv->pool;
00043 Id p, pp;
00044 Reldep *rd;
00045 Solvable *s;
00046
00047 if (!solv->dosplitprovides || !solv->installed)
00048 return 0;
00049 if (!ISRELDEP(dep))
00050 return 0;
00051 rd = GETRELDEP(pool, dep);
00052 if (rd->flags != REL_WITH)
00053 return 0;
00054 FOR_PROVIDES(p, pp, dep)
00055 {
00056 s = pool->solvables + p;
00057 if (s->repo == solv->installed && s->name == rd->name)
00058 return 1;
00059 }
00060 return 0;
00061 }
00062
00063
00064
00065
00066
00067
00068 int
00069 solver_dep_installed(Solver *solv, Id dep)
00070 {
00071 #if 0
00072 Pool *pool = solv->pool;
00073 Id p, pp;
00074
00075 if (ISRELDEP(dep))
00076 {
00077 Reldep *rd = GETRELDEP(pool, dep);
00078 if (rd->flags == REL_AND)
00079 {
00080 if (!solver_dep_installed(solv, rd->name))
00081 return 0;
00082 return solver_dep_installed(solv, rd->evr);
00083 }
00084 if (rd->flags == REL_NAMESPACE && rd->name == NAMESPACE_INSTALLED)
00085 return solver_dep_installed(solv, rd->evr);
00086 }
00087 FOR_PROVIDES(p, pp, dep)
00088 {
00089 if (p == SYSTEMSOLVABLE || (solv->installed && pool->solvables[p].repo == solv->installed))
00090 return 1;
00091 }
00092 #endif
00093 return 0;
00094 }
00095
00096
00097
00098
00099
00100
00101
00102
00103
00104
00105
00106
00107 static void
00108 makeruledecisions(Solver *solv)
00109 {
00110 Pool *pool = solv->pool;
00111 int i, ri, ii;
00112 Rule *r, *rr;
00113 Id v, vv;
00114 int decisionstart;
00115
00116 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions ; size decisionq: %d -----\n",solv->decisionq.count);
00117
00118
00119 assert(solv->decisionq.count == 0);
00120 queue_push(&solv->decisionq, SYSTEMSOLVABLE);
00121 queue_push(&solv->decisionq_why, 0);
00122 solv->decisionmap[SYSTEMSOLVABLE] = 1;
00123
00124 decisionstart = solv->decisionq.count;
00125 for (ii = 0; ii < solv->ruleassertions.count; ii++)
00126 {
00127 ri = solv->ruleassertions.elements[ii];
00128 r = solv->rules + ri;
00129
00130 if (r->d < 0 || !r->p || r->w2)
00131 continue;
00132
00133 if (ri < solv->learntrules && MAPTST(&solv->weakrulemap, ri))
00134 continue;
00135
00136 v = r->p;
00137 vv = v > 0 ? v : -v;
00138
00139 if (!solv->decisionmap[vv])
00140 {
00141
00142
00143
00144 queue_push(&solv->decisionq, v);
00145 queue_push(&solv->decisionq_why, r - solv->rules);
00146 solv->decisionmap[vv] = v > 0 ? 1 : -1;
00147 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00148 {
00149 Solvable *s = solv->pool->solvables + vv;
00150 if (v < 0)
00151 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (assertion)\n", solvable2str(solv->pool, s));
00152 else
00153 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (assertion)\n", solvable2str(solv->pool, s));
00154 }
00155 continue;
00156 }
00157
00158
00159
00160
00161 if (v > 0 && solv->decisionmap[vv] > 0)
00162 continue;
00163 if (v < 0 && solv->decisionmap[vv] < 0)
00164 continue;
00165
00166
00167
00168
00169
00170
00171
00172
00173
00174 if (ri >= solv->learntrules)
00175 {
00176
00177
00178
00179
00180 solver_disablerule(solv, r);
00181 continue;
00182 }
00183
00184
00185
00186
00187
00188 for (i = 0; i < solv->decisionq.count; i++)
00189 if (solv->decisionq.elements[i] == -v)
00190 break;
00191 assert(i < solv->decisionq.count);
00192
00193
00194
00195
00196
00197 if (v == -SYSTEMSOLVABLE) {
00198
00199 queue_push(&solv->problems, solv->learnt_pool.count);
00200 queue_push(&solv->learnt_pool, ri);
00201 queue_push(&solv->learnt_pool, 0);
00202 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with system solvable, disabling rule #%d\n", ri);
00203 if (ri >= solv->jobrules && ri < solv->jobrules_end)
00204 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
00205 else
00206 v = ri;
00207 queue_push(&solv->problems, v);
00208 queue_push(&solv->problems, 0);
00209 solver_disableproblem(solv, v);
00210 continue;
00211 }
00212
00213 assert(solv->decisionq_why.elements[i] > 0);
00214
00215
00216
00217
00218
00219 if (solv->decisionq_why.elements[i] < solv->rpmrules_end)
00220 {
00221
00222 queue_push(&solv->problems, solv->learnt_pool.count);
00223 queue_push(&solv->learnt_pool, ri);
00224 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
00225 queue_push(&solv->learnt_pool, 0);
00226 assert(v > 0 || v == -SYSTEMSOLVABLE);
00227 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflict with rpm rule, disabling rule #%d\n", ri);
00228 if (ri >= solv->jobrules && ri < solv->jobrules_end)
00229 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
00230 else
00231 v = ri;
00232 queue_push(&solv->problems, v);
00233 queue_push(&solv->problems, 0);
00234 solver_disableproblem(solv, v);
00235 continue;
00236 }
00237
00238
00239
00240
00241
00242
00243 queue_push(&solv->problems, solv->learnt_pool.count);
00244 queue_push(&solv->learnt_pool, ri);
00245 queue_push(&solv->learnt_pool, solv->decisionq_why.elements[i]);
00246 queue_push(&solv->learnt_pool, 0);
00247
00248 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "conflicting update/job assertions over literal %d\n", vv);
00249
00250
00251
00252
00253
00254
00255 for (i = solv->featurerules, rr = solv->rules + i; i < solv->learntrules; i++, rr++)
00256 {
00257 if (rr->d < 0
00258 || rr->w2)
00259 continue;
00260 if (rr->p != vv
00261 && rr->p != -vv)
00262 continue;
00263 if (MAPTST(&solv->weakrulemap, i))
00264 continue;
00265
00266 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, " - disabling rule #%d\n", i);
00267
00268 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + i);
00269
00270 v = i;
00271
00272 if (i >= solv->jobrules && i < solv->jobrules_end)
00273 v = -(solv->ruletojob.elements[i - solv->jobrules] + 1);
00274
00275 queue_push(&solv->problems, v);
00276 solver_disableproblem(solv, v);
00277 }
00278 queue_push(&solv->problems, 0);
00279
00280
00281
00282
00283
00284 while (solv->decisionq.count > decisionstart)
00285 {
00286 v = solv->decisionq.elements[--solv->decisionq.count];
00287 --solv->decisionq_why.count;
00288 vv = v > 0 ? v : -v;
00289 solv->decisionmap[vv] = 0;
00290 }
00291 ii = -1;
00292 }
00293
00294
00295
00296
00297 for (ii = 0; ii < solv->ruleassertions.count; ii++)
00298 {
00299 ri = solv->ruleassertions.elements[ii];
00300 r = solv->rules + ri;
00301 if (r->d < 0 || r->w2)
00302 continue;
00303 if (ri >= solv->learntrules || !MAPTST(&solv->weakrulemap, ri))
00304 continue;
00305 v = r->p;
00306 vv = v > 0 ? v : -v;
00307
00308
00309
00310
00311 if (!solv->decisionmap[vv])
00312 {
00313 queue_push(&solv->decisionq, v);
00314 queue_push(&solv->decisionq_why, r - solv->rules);
00315 solv->decisionmap[vv] = v > 0 ? 1 : -1;
00316 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00317 {
00318 Solvable *s = solv->pool->solvables + vv;
00319 if (v < 0)
00320 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "conflicting %s (weak assertion)\n", solvable2str(solv->pool, s));
00321 else
00322 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "installing %s (weak assertion)\n", solvable2str(solv->pool, s));
00323 }
00324 continue;
00325 }
00326
00327
00328
00329 if (v > 0 && solv->decisionmap[vv] > 0)
00330 continue;
00331 if (v < 0 && solv->decisionmap[vv] < 0)
00332 continue;
00333
00334 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "assertion conflict, but I am weak, disabling ");
00335 solver_printrule(solv, SAT_DEBUG_UNSOLVABLE, r);
00336
00337 if (ri >= solv->jobrules && ri < solv->jobrules_end)
00338 v = -(solv->ruletojob.elements[ri - solv->jobrules] + 1);
00339 else
00340 v = ri;
00341 solver_disableproblem(solv, v);
00342 if (v < 0)
00343 solver_reenablepolicyrules(solv, -(v + 1));
00344 }
00345
00346 POOL_DEBUG(SAT_DEBUG_SCHUBI, "----- makeruledecisions end; size decisionq: %d -----\n",solv->decisionq.count);
00347 }
00348
00349
00350
00351
00352
00353
00354
00355
00356
00357 static void
00358 enabledisablelearntrules(Solver *solv)
00359 {
00360 Pool *pool = solv->pool;
00361 Rule *r;
00362 Id why, *whyp;
00363 int i;
00364
00365 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "enabledisablelearntrules called\n");
00366 for (i = solv->learntrules, r = solv->rules + i; i < solv->nrules; i++, r++)
00367 {
00368 whyp = solv->learnt_pool.elements + solv->learnt_why.elements[i - solv->learntrules];
00369 while ((why = *whyp++) != 0)
00370 {
00371 assert(why > 0 && why < i);
00372 if (solv->rules[why].d < 0)
00373 break;
00374 }
00375
00376 if (why && r->d >= 0)
00377 {
00378 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
00379 {
00380 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "disabling ");
00381 solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
00382 }
00383 solver_disablerule(solv, r);
00384 }
00385 else if (!why && r->d < 0)
00386 {
00387 IF_POOLDEBUG (SAT_DEBUG_SOLUTIONS)
00388 {
00389 POOL_DEBUG(SAT_DEBUG_SOLUTIONS, "re-enabling ");
00390 solver_printruleclass(solv, SAT_DEBUG_SOLUTIONS, r);
00391 }
00392 solver_enablerule(solv, r);
00393 }
00394 }
00395 }
00396
00397
00398
00399
00400
00401
00402
00403
00404
00405
00406
00407
00408 static void
00409 makewatches(Solver *solv)
00410 {
00411 Rule *r;
00412 int i;
00413 int nsolvables = solv->pool->nsolvables;
00414
00415 sat_free(solv->watches);
00416
00417 solv->watches = sat_calloc(2 * nsolvables, sizeof(Id));
00418 #if 1
00419
00420 for (i = 1, r = solv->rules + solv->nrules - 1; i < solv->nrules; i++, r--)
00421 #else
00422 for (i = 1, r = solv->rules + 1; i < solv->nrules; i++, r++)
00423 #endif
00424 {
00425 if (!r->w2)
00426 continue;
00427
00428
00429 r->n1 = solv->watches[nsolvables + r->w1];
00430 solv->watches[nsolvables + r->w1] = r - solv->rules;
00431
00432 r->n2 = solv->watches[nsolvables + r->w2];
00433 solv->watches[nsolvables + r->w2] = r - solv->rules;
00434 }
00435 }
00436
00437
00438
00439
00440
00441
00442
00443
00444
00445
00446 static inline void
00447 addwatches_rule(Solver *solv, Rule *r)
00448 {
00449 int nsolvables = solv->pool->nsolvables;
00450
00451 r->n1 = solv->watches[nsolvables + r->w1];
00452 solv->watches[nsolvables + r->w1] = r - solv->rules;
00453
00454 r->n2 = solv->watches[nsolvables + r->w2];
00455 solv->watches[nsolvables + r->w2] = r - solv->rules;
00456 }
00457
00458
00459
00460
00461
00462
00463
00464
00465
00466
00467
00468 #define DECISIONMAP_TRUE(p) ((p) > 0 ? (decisionmap[p] > 0) : (decisionmap[-p] < 0))
00469 #define DECISIONMAP_FALSE(p) ((p) > 0 ? (decisionmap[p] < 0) : (decisionmap[-p] > 0))
00470 #define DECISIONMAP_UNDEF(p) (decisionmap[(p) > 0 ? (p) : -(p)] == 0)
00471
00472
00473
00474
00475
00476
00477
00478
00479
00480
00481
00482
00483
00484
00485
00486
00487
00488 static Rule *
00489 propagate(Solver *solv, int level)
00490 {
00491 Pool *pool = solv->pool;
00492 Id *rp, *next_rp;
00493 Rule *r;
00494 Id p, pkg, other_watch;
00495 Id *dp;
00496 Id *decisionmap = solv->decisionmap;
00497
00498 Id *watches = solv->watches + pool->nsolvables;
00499
00500 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate -----\n");
00501
00502
00503 while (solv->propagate_index < solv->decisionq.count)
00504 {
00505
00506
00507
00508
00509 pkg = -solv->decisionq.elements[solv->propagate_index++];
00510
00511 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00512 {
00513 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagate for decision %d level %d\n", -pkg, level);
00514 solver_printruleelement(solv, SAT_DEBUG_PROPAGATE, 0, -pkg);
00515 }
00516
00517
00518 for (rp = watches + pkg; *rp; rp = next_rp)
00519 {
00520 r = solv->rules + *rp;
00521 if (r->d < 0)
00522 {
00523
00524 if (pkg == r->w1)
00525 next_rp = &r->n1;
00526 else
00527 next_rp = &r->n2;
00528 continue;
00529 }
00530
00531 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00532 {
00533 POOL_DEBUG(SAT_DEBUG_PROPAGATE," watch triggered ");
00534 solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
00535 }
00536
00537
00538
00539
00540
00541
00542 if (pkg == r->w1)
00543 {
00544 other_watch = r->w2;
00545 next_rp = &r->n1;
00546 }
00547 else
00548 {
00549 other_watch = r->w1;
00550 next_rp = &r->n2;
00551 }
00552
00553
00554
00555
00556
00557 if (DECISIONMAP_TRUE(other_watch))
00558 continue;
00559
00560
00561
00562
00563
00564
00565 if (r->d)
00566 {
00567
00568
00569
00570
00571
00572
00573
00574
00575 if (r->p
00576 && r->p != other_watch
00577 && !DECISIONMAP_FALSE(r->p))
00578 {
00579 p = r->p;
00580 }
00581 else
00582 {
00583
00584
00585
00586 for (dp = pool->whatprovidesdata + r->d; (p = *dp++) != 0;)
00587 {
00588 if (p != other_watch
00589 && !DECISIONMAP_FALSE(p))
00590 break;
00591 }
00592 }
00593
00594 if (p)
00595 {
00596
00597
00598
00599
00600 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00601 {
00602 if (p > 0)
00603 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> move w%d to %s\n", (pkg == r->w1 ? 1 : 2), solvid2str(pool, p));
00604 else
00605 POOL_DEBUG(SAT_DEBUG_PROPAGATE," -> move w%d to !%s\n", (pkg == r->w1 ? 1 : 2), solvid2str(pool, -p));
00606 }
00607
00608 *rp = *next_rp;
00609 next_rp = rp;
00610
00611 if (pkg == r->w1)
00612 {
00613 r->w1 = p;
00614 r->n1 = watches[p];
00615 }
00616 else
00617 {
00618 r->w2 = p;
00619 r->n2 = watches[p];
00620 }
00621 watches[p] = r - solv->rules;
00622 continue;
00623 }
00624
00625
00626 }
00627
00628
00629
00630
00631
00632 if (DECISIONMAP_FALSE(other_watch))
00633 return r;
00634
00635 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00636 {
00637 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " unit ");
00638 solver_printrule(solv, SAT_DEBUG_PROPAGATE, r);
00639 }
00640
00641 if (other_watch > 0)
00642 decisionmap[other_watch] = level;
00643 else
00644 decisionmap[-other_watch] = -level;
00645
00646 queue_push(&solv->decisionq, other_watch);
00647 queue_push(&solv->decisionq_why, r - solv->rules);
00648
00649 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
00650 {
00651 if (other_watch > 0)
00652 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to install %s\n", solvid2str(pool, other_watch));
00653 else
00654 POOL_DEBUG(SAT_DEBUG_PROPAGATE, " -> decided to conflict %s\n", solvid2str(pool, -other_watch));
00655 }
00656
00657 }
00658
00659 }
00660
00661 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "----- propagate end-----\n");
00662
00663 return 0;
00664 }
00665
00666
00667
00668
00669
00670
00671
00672
00673
00674
00675
00676 static int
00677 analyze(Solver *solv, int level, Rule *c, int *pr, int *dr, int *whyp)
00678 {
00679 Pool *pool = solv->pool;
00680 Queue r;
00681 int rlevel = 1;
00682 Map seen;
00683 Id d, v, vv, *dp, why;
00684 int l, i, idx;
00685 int num = 0, l1num = 0;
00686 int learnt_why = solv->learnt_pool.count;
00687 Id *decisionmap = solv->decisionmap;
00688
00689 queue_init(&r);
00690
00691 POOL_DEBUG(SAT_DEBUG_ANALYZE, "ANALYZE at %d ----------------------\n", level);
00692 map_init(&seen, pool->nsolvables);
00693 idx = solv->decisionq.count;
00694 for (;;)
00695 {
00696 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
00697 solver_printruleclass(solv, SAT_DEBUG_ANALYZE, c);
00698 queue_push(&solv->learnt_pool, c - solv->rules);
00699 d = c->d < 0 ? -c->d - 1 : c->d;
00700 dp = d ? pool->whatprovidesdata + d : 0;
00701
00702 for (i = -1; ; i++)
00703 {
00704 if (i == -1)
00705 v = c->p;
00706 else if (d == 0)
00707 v = i ? 0 : c->w2;
00708 else
00709 v = *dp++;
00710 if (v == 0)
00711 break;
00712
00713 if (DECISIONMAP_TRUE(v))
00714 continue;
00715 vv = v > 0 ? v : -v;
00716 if (MAPTST(&seen, vv))
00717 continue;
00718 l = solv->decisionmap[vv];
00719 if (l < 0)
00720 l = -l;
00721 MAPSET(&seen, vv);
00722 if (l == 1)
00723 l1num++;
00724 else if (l == level)
00725 num++;
00726 else
00727 {
00728 queue_push(&r, v);
00729 if (l > rlevel)
00730 rlevel = l;
00731 }
00732 }
00733 l1retry:
00734 if (!num && !--l1num)
00735 break;
00736 for (;;)
00737 {
00738 assert(idx > 0);
00739 v = solv->decisionq.elements[--idx];
00740 vv = v > 0 ? v : -v;
00741 if (MAPTST(&seen, vv))
00742 break;
00743 }
00744 MAPCLR(&seen, vv);
00745 if (num && --num == 0)
00746 {
00747 *pr = -v;
00748 if (!l1num)
00749 break;
00750 POOL_DEBUG(SAT_DEBUG_ANALYZE, "got %d involved level 1 decisions\n", l1num);
00751 for (i = 0; i < r.count; i++)
00752 {
00753 v = r.elements[i];
00754 MAPCLR(&seen, v > 0 ? v : -v);
00755 }
00756
00757 l1num++;
00758 goto l1retry;
00759 }
00760 why = solv->decisionq_why.elements[idx];
00761 if (why <= 0)
00762 goto l1retry;
00763 c = solv->rules + why;
00764 }
00765 map_free(&seen);
00766
00767 if (r.count == 0)
00768 *dr = 0;
00769 else if (r.count == 1 && r.elements[0] < 0)
00770 *dr = r.elements[0];
00771 else
00772 *dr = pool_queuetowhatprovides(pool, &r);
00773 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
00774 {
00775 POOL_DEBUG(SAT_DEBUG_ANALYZE, "learned rule for level %d (am %d)\n", rlevel, level);
00776 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, *pr);
00777 for (i = 0; i < r.count; i++)
00778 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, r.elements[i]);
00779 }
00780
00781 queue_push(&solv->learnt_pool, 0);
00782 if (whyp)
00783 *whyp = learnt_why;
00784 solv->stats_learned++;
00785 return rlevel;
00786 }
00787
00788
00789
00790
00791
00792
00793
00794
00795
00796
00797 void
00798 solver_reset(Solver *solv)
00799 {
00800 Pool *pool = solv->pool;
00801 int i;
00802 Id v;
00803
00804
00805 for (i = solv->decisionq.count - 1; i >= 0; i--)
00806 {
00807 v = solv->decisionq.elements[i];
00808 solv->decisionmap[v > 0 ? v : -v] = 0;
00809 }
00810 solv->decisionq_why.count = 0;
00811 solv->decisionq.count = 0;
00812 solv->recommends_index = -1;
00813 solv->propagate_index = 0;
00814 solv->recommendations.count = 0;
00815 solv->branches.count = 0;
00816
00817
00818 enabledisablelearntrules(solv);
00819
00820
00821 makeruledecisions(solv);
00822 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "decisions so far: %d\n", solv->decisionq.count);
00823 }
00824
00825
00826
00827
00828
00829
00830
00831 static void
00832 analyze_unsolvable_rule(Solver *solv, Rule *r, Id *lastweakp)
00833 {
00834 Pool *pool = solv->pool;
00835 int i;
00836 Id why = r - solv->rules;
00837
00838 IF_POOLDEBUG (SAT_DEBUG_UNSOLVABLE)
00839 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, r);
00840 if (solv->learntrules && why >= solv->learntrules)
00841 {
00842 for (i = solv->learnt_why.elements[why - solv->learntrules]; solv->learnt_pool.elements[i]; i++)
00843 if (solv->learnt_pool.elements[i] > 0)
00844 analyze_unsolvable_rule(solv, solv->rules + solv->learnt_pool.elements[i], lastweakp);
00845 return;
00846 }
00847 if (MAPTST(&solv->weakrulemap, why))
00848 if (!*lastweakp || why > *lastweakp)
00849 *lastweakp = why;
00850
00851 if (why < solv->rpmrules_end)
00852 return;
00853
00854 if (why >= solv->jobrules && why < solv->jobrules_end)
00855 why = -(solv->ruletojob.elements[why - solv->jobrules] + 1);
00856
00857 if (why > solv->infarchrules && why < solv->infarchrules_end)
00858 {
00859 Id name = pool->solvables[-solv->rules[why].p].name;
00860 while (why > solv->infarchrules && pool->solvables[-solv->rules[why - 1].p].name == name)
00861 why--;
00862 }
00863 if (why > solv->duprules && why < solv->duprules_end)
00864 {
00865 Id name = pool->solvables[-solv->rules[why].p].name;
00866 while (why > solv->duprules && pool->solvables[-solv->rules[why - 1].p].name == name)
00867 why--;
00868 }
00869
00870
00871 if (solv->problems.count)
00872 {
00873 for (i = solv->problems.count - 1; i >= 0; i--)
00874 if (solv->problems.elements[i] == 0)
00875 break;
00876 else if (solv->problems.elements[i] == why)
00877 return;
00878 }
00879 queue_push(&solv->problems, why);
00880 }
00881
00882
00883
00884
00885
00886
00887
00888
00889
00890
00891 static int
00892 analyze_unsolvable(Solver *solv, Rule *cr, int disablerules)
00893 {
00894 Pool *pool = solv->pool;
00895 Rule *r;
00896 Map seen;
00897 Id d, v, vv, *dp, why;
00898 int l, i, idx;
00899 Id *decisionmap = solv->decisionmap;
00900 int oldproblemcount;
00901 int oldlearntpoolcount;
00902 Id lastweak;
00903
00904 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "ANALYZE UNSOLVABLE ----------------------\n");
00905 solv->stats_unsolvable++;
00906 oldproblemcount = solv->problems.count;
00907 oldlearntpoolcount = solv->learnt_pool.count;
00908
00909
00910
00911
00912 queue_push(&solv->problems, 0);
00913
00914 r = cr;
00915 map_init(&seen, pool->nsolvables);
00916 queue_push(&solv->learnt_pool, r - solv->rules);
00917 lastweak = 0;
00918 analyze_unsolvable_rule(solv, r, &lastweak);
00919 d = r->d < 0 ? -r->d - 1 : r->d;
00920 dp = d ? pool->whatprovidesdata + d : 0;
00921 for (i = -1; ; i++)
00922 {
00923 if (i == -1)
00924 v = r->p;
00925 else if (d == 0)
00926 v = i ? 0 : r->w2;
00927 else
00928 v = *dp++;
00929 if (v == 0)
00930 break;
00931 if (DECISIONMAP_TRUE(v))
00932 continue;
00933 vv = v > 0 ? v : -v;
00934 l = solv->decisionmap[vv];
00935 if (l < 0)
00936 l = -l;
00937 MAPSET(&seen, vv);
00938 }
00939 idx = solv->decisionq.count;
00940 while (idx > 0)
00941 {
00942 v = solv->decisionq.elements[--idx];
00943 vv = v > 0 ? v : -v;
00944 if (!MAPTST(&seen, vv))
00945 continue;
00946 why = solv->decisionq_why.elements[idx];
00947 assert(why > 0);
00948 queue_push(&solv->learnt_pool, why);
00949 r = solv->rules + why;
00950 analyze_unsolvable_rule(solv, r, &lastweak);
00951 d = r->d < 0 ? -r->d - 1 : r->d;
00952 dp = d ? pool->whatprovidesdata + d : 0;
00953 for (i = -1; ; i++)
00954 {
00955 if (i == -1)
00956 v = r->p;
00957 else if (d == 0)
00958 v = i ? 0 : r->w2;
00959 else
00960 v = *dp++;
00961 if (v == 0)
00962 break;
00963 if (DECISIONMAP_TRUE(v))
00964 continue;
00965 vv = v > 0 ? v : -v;
00966 l = solv->decisionmap[vv];
00967 if (l < 0)
00968 l = -l;
00969 MAPSET(&seen, vv);
00970 }
00971 }
00972 map_free(&seen);
00973 queue_push(&solv->problems, 0);
00974
00975 if (lastweak)
00976 {
00977 Id v;
00978
00979 solv->problems.count = oldproblemcount;
00980 solv->learnt_pool.count = oldlearntpoolcount;
00981 if (lastweak >= solv->jobrules && lastweak < solv->jobrules_end)
00982 v = -(solv->ruletojob.elements[lastweak - solv->jobrules] + 1);
00983 else
00984 v = lastweak;
00985 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "disabling ");
00986 solver_printruleclass(solv, SAT_DEBUG_UNSOLVABLE, solv->rules + lastweak);
00987 if (lastweak >= solv->choicerules && lastweak < solv->choicerules_end)
00988 solver_disablechoicerules(solv, solv->rules + lastweak);
00989 solver_disableproblem(solv, v);
00990 if (v < 0)
00991 solver_reenablepolicyrules(solv, -(v + 1));
00992 solver_reset(solv);
00993 return 1;
00994 }
00995
00996
00997 queue_push(&solv->learnt_pool, 0);
00998 solv->problems.elements[oldproblemcount] = oldlearntpoolcount;
00999
01000 if (disablerules)
01001 {
01002 for (i = oldproblemcount + 1; i < solv->problems.count - 1; i++)
01003 solver_disableproblem(solv, solv->problems.elements[i]);
01004
01005 solver_reset(solv);
01006 return 1;
01007 }
01008 POOL_DEBUG(SAT_DEBUG_UNSOLVABLE, "UNSOLVABLE\n");
01009 return 0;
01010 }
01011
01012
01013
01014
01015
01016
01017
01018
01019
01020
01021
01022 static void
01023 revert(Solver *solv, int level)
01024 {
01025 Pool *pool = solv->pool;
01026 Id v, vv;
01027 while (solv->decisionq.count)
01028 {
01029 v = solv->decisionq.elements[solv->decisionq.count - 1];
01030 vv = v > 0 ? v : -v;
01031 if (solv->decisionmap[vv] <= level && solv->decisionmap[vv] >= -level)
01032 break;
01033 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "reverting decision %d at %d\n", v, solv->decisionmap[vv]);
01034 if (v > 0 && solv->recommendations.count && v == solv->recommendations.elements[solv->recommendations.count - 1])
01035 solv->recommendations.count--;
01036 solv->decisionmap[vv] = 0;
01037 solv->decisionq.count--;
01038 solv->decisionq_why.count--;
01039 solv->propagate_index = solv->decisionq.count;
01040 }
01041 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] <= -level)
01042 {
01043 solv->branches.count--;
01044 while (solv->branches.count && solv->branches.elements[solv->branches.count - 1] >= 0)
01045 solv->branches.count--;
01046 }
01047 solv->recommends_index = -1;
01048 }
01049
01050
01051
01052
01053
01054
01055
01056 static inline void
01057 watch2onhighest(Solver *solv, Rule *r)
01058 {
01059 int l, wl = 0;
01060 Id d, v, *dp;
01061
01062 d = r->d < 0 ? -r->d - 1 : r->d;
01063 if (!d)
01064 return;
01065 dp = solv->pool->whatprovidesdata + d;
01066 while ((v = *dp++) != 0)
01067 {
01068 l = solv->decisionmap[v < 0 ? -v : v];
01069 if (l < 0)
01070 l = -l;
01071 if (l > wl)
01072 {
01073 r->w2 = dp[-1];
01074 wl = l;
01075 }
01076 }
01077 }
01078
01079
01080
01081
01082
01083
01084
01085
01086
01087
01088
01089
01090
01091
01092
01093
01094
01095
01096 static int
01097 setpropagatelearn(Solver *solv, int level, Id decision, int disablerules, Id ruleid)
01098 {
01099 Pool *pool = solv->pool;
01100 Rule *r;
01101 Id p = 0, d = 0;
01102 int l, why;
01103
01104 assert(ruleid >= 0);
01105 if (decision)
01106 {
01107 level++;
01108 if (decision > 0)
01109 solv->decisionmap[decision] = level;
01110 else
01111 solv->decisionmap[-decision] = -level;
01112 queue_push(&solv->decisionq, decision);
01113 queue_push(&solv->decisionq_why, -ruleid);
01114 }
01115 for (;;)
01116 {
01117 r = propagate(solv, level);
01118 if (!r)
01119 break;
01120 if (level == 1)
01121 return analyze_unsolvable(solv, r, disablerules);
01122 POOL_DEBUG(SAT_DEBUG_ANALYZE, "conflict with rule #%d\n", (int)(r - solv->rules));
01123 l = analyze(solv, level, r, &p, &d, &why);
01124 assert(l > 0 && l < level);
01125 POOL_DEBUG(SAT_DEBUG_ANALYZE, "reverting decisions (level %d -> %d)\n", level, l);
01126 level = l;
01127 revert(solv, level);
01128 r = solver_addrule(solv, p, d);
01129 assert(r);
01130 assert(solv->learnt_why.count == (r - solv->rules) - solv->learntrules);
01131 queue_push(&solv->learnt_why, why);
01132 if (d)
01133 {
01134
01135 watch2onhighest(solv, r);
01136 addwatches_rule(solv, r);
01137 }
01138 else
01139 {
01140
01141 queue_push(&solv->ruleassertions, r - solv->rules);
01142 }
01143
01144 solv->decisionmap[p > 0 ? p : -p] = p > 0 ? level : -level;
01145 queue_push(&solv->decisionq, p);
01146 queue_push(&solv->decisionq_why, r - solv->rules);
01147 IF_POOLDEBUG (SAT_DEBUG_ANALYZE)
01148 {
01149 POOL_DEBUG(SAT_DEBUG_ANALYZE, "decision: ");
01150 solver_printruleelement(solv, SAT_DEBUG_ANALYZE, 0, p);
01151 POOL_DEBUG(SAT_DEBUG_ANALYZE, "new rule: ");
01152 solver_printrule(solv, SAT_DEBUG_ANALYZE, r);
01153 }
01154 }
01155 return level;
01156 }
01157
01158
01159
01160
01161
01162
01163
01164
01165
01166
01167
01168
01169
01170 static int
01171 selectandinstall(Solver *solv, int level, Queue *dq, int disablerules, Id ruleid)
01172 {
01173 Pool *pool = solv->pool;
01174 Id p;
01175 int i;
01176
01177 if (dq->count > 1)
01178 policy_filter_unwanted(solv, dq, POLICY_MODE_CHOOSE);
01179 if (dq->count > 1)
01180 {
01181
01182
01183
01184
01185 for (i = 0; i < dq->count; i++)
01186 if (solver_is_supplementing(solv, pool->solvables + dq->elements[i]))
01187 {
01188 dq->elements[0] = dq->elements[i];
01189 dq->count = 1;
01190 break;
01191 }
01192 }
01193 if (dq->count > 1)
01194 {
01195
01196 for (i = 1; i < dq->count; i++)
01197 queue_push(&solv->branches, dq->elements[i]);
01198 queue_push(&solv->branches, -level);
01199 }
01200 p = dq->elements[0];
01201
01202 POOL_DEBUG(SAT_DEBUG_POLICY, "installing %s\n", solvid2str(pool, p));
01203
01204 return setpropagatelearn(solv, level, p, disablerules, ruleid);
01205 }
01206
01207
01208
01209
01210
01211
01212
01213
01214
01215
01216
01217
01218
01219
01220
01221
01222
01223
01224
01225 Solver *
01226 solver_create(Pool *pool)
01227 {
01228 Solver *solv;
01229 solv = (Solver *)sat_calloc(1, sizeof(Solver));
01230 solv->pool = pool;
01231 solv->installed = pool->installed;
01232
01233 transaction_init(&solv->trans, pool);
01234 queue_init(&solv->ruletojob);
01235 queue_init(&solv->decisionq);
01236 queue_init(&solv->decisionq_why);
01237 queue_init(&solv->problems);
01238 queue_init(&solv->suggestions);
01239 queue_init(&solv->recommendations);
01240 queue_init(&solv->orphaned);
01241 queue_init(&solv->learnt_why);
01242 queue_init(&solv->learnt_pool);
01243 queue_init(&solv->branches);
01244 queue_init(&solv->covenantq);
01245 queue_init(&solv->weakruleq);
01246 queue_init(&solv->ruleassertions);
01247
01248 map_init(&solv->recommendsmap, pool->nsolvables);
01249 map_init(&solv->suggestsmap, pool->nsolvables);
01250 map_init(&solv->noupdate, solv->installed ? solv->installed->end - solv->installed->start : 0);
01251 solv->recommends_index = 0;
01252
01253 solv->decisionmap = (Id *)sat_calloc(pool->nsolvables, sizeof(Id));
01254 solv->nrules = 1;
01255 solv->rules = sat_extend_resize(solv->rules, solv->nrules, sizeof(Rule), RULES_BLOCK);
01256 memset(solv->rules, 0, sizeof(Rule));
01257
01258 return solv;
01259 }
01260
01261
01262
01263
01264
01265
01266
01267 void
01268 solver_free(Solver *solv)
01269 {
01270 transaction_free(&solv->trans);
01271 queue_free(&solv->job);
01272 queue_free(&solv->ruletojob);
01273 queue_free(&solv->decisionq);
01274 queue_free(&solv->decisionq_why);
01275 queue_free(&solv->learnt_why);
01276 queue_free(&solv->learnt_pool);
01277 queue_free(&solv->problems);
01278 queue_free(&solv->solutions);
01279 queue_free(&solv->suggestions);
01280 queue_free(&solv->recommendations);
01281 queue_free(&solv->orphaned);
01282 queue_free(&solv->branches);
01283 queue_free(&solv->covenantq);
01284 queue_free(&solv->weakruleq);
01285 queue_free(&solv->ruleassertions);
01286
01287 map_free(&solv->recommendsmap);
01288 map_free(&solv->suggestsmap);
01289 map_free(&solv->noupdate);
01290 map_free(&solv->weakrulemap);
01291 map_free(&solv->noobsoletes);
01292
01293 map_free(&solv->updatemap);
01294 map_free(&solv->fixmap);
01295 map_free(&solv->dupmap);
01296 map_free(&solv->dupinvolvedmap);
01297 map_free(&solv->droporphanedmap);
01298 map_free(&solv->cleandepsmap);
01299
01300 sat_free(solv->decisionmap);
01301 sat_free(solv->rules);
01302 sat_free(solv->watches);
01303 sat_free(solv->obsoletes);
01304 sat_free(solv->obsoletes_data);
01305 sat_free(solv->multiversionupdaters);
01306 sat_free(solv->choicerules_ref);
01307 sat_free(solv);
01308 }
01309
01310
01311
01312
01313
01314
01315
01316
01317
01318
01319 void
01320 solver_run_sat(Solver *solv, int disablerules, int doweak)
01321 {
01322 Queue dq;
01323 Queue dqs;
01324 int systemlevel;
01325 int level, olevel;
01326 Rule *r;
01327 int i, j, n;
01328 Solvable *s;
01329 Pool *pool = solv->pool;
01330 Id p, *dp;
01331 int minimizationsteps;
01332 int installedpos = solv->installed ? solv->installed->start : 0;
01333
01334 IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
01335 {
01336 POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
01337 for (i = 1; i < solv->nrules; i++)
01338 solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
01339 }
01340
01341 POOL_DEBUG(SAT_DEBUG_SOLVER, "initial decisions: %d\n", solv->decisionq.count);
01342
01343 IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
01344 solver_printdecisions(solv);
01345
01346
01347 level = 1;
01348 systemlevel = level + 1;
01349 POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n");
01350
01351 queue_init(&dq);
01352 queue_init(&dqs);
01353
01354
01355
01356
01357
01358
01359
01360
01361
01362
01363
01364
01365
01366 minimizationsteps = 0;
01367 for (;;)
01368 {
01369
01370
01371
01372 if (level == 1)
01373 {
01374 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
01375 if ((r = propagate(solv, level)) != 0)
01376 {
01377 if (analyze_unsolvable(solv, r, disablerules))
01378 continue;
01379 queue_free(&dq);
01380 queue_free(&dqs);
01381 return;
01382 }
01383 }
01384
01385
01386
01387
01388 if (level < systemlevel)
01389 {
01390 POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving job rules\n");
01391 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
01392 {
01393 Id l;
01394 if (r->d < 0)
01395 continue;
01396 queue_empty(&dq);
01397 FOR_RULELITERALS(l, dp, r)
01398 {
01399 if (l < 0)
01400 {
01401 if (solv->decisionmap[-l] <= 0)
01402 break;
01403 }
01404 else
01405 {
01406 if (solv->decisionmap[l] > 0)
01407 break;
01408 if (solv->decisionmap[l] == 0)
01409 queue_push(&dq, l);
01410 }
01411 }
01412 if (l || !dq.count)
01413 continue;
01414
01415 if (dq.count > 1 && solv->installed && !solv->updatemap_all)
01416 {
01417 int j, k;
01418 for (j = k = 0; j < dq.count; j++)
01419 {
01420 Solvable *s = pool->solvables + dq.elements[j];
01421 if (s->repo == solv->installed)
01422 {
01423 dq.elements[k++] = dq.elements[j];
01424 if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start))
01425 {
01426 k = 0;
01427 break;
01428 }
01429 }
01430 }
01431 if (k)
01432 dq.count = k;
01433 }
01434 olevel = level;
01435 level = selectandinstall(solv, level, &dq, disablerules, i);
01436 if (level == 0)
01437 {
01438 queue_free(&dq);
01439 queue_free(&dqs);
01440 return;
01441 }
01442 if (level <= olevel)
01443 break;
01444 }
01445 systemlevel = level + 1;
01446 if (i < solv->jobrules_end)
01447 continue;
01448 }
01449
01450
01451
01452
01453
01454 if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled)
01455 {
01456 Repo *installed = solv->installed;
01457 int pass;
01458
01459 POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n");
01460
01461
01462 for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
01463 {
01464 int passlevel = level;
01465
01466 for (i = installedpos, n = installed->start; n < installed->end; i++, n++)
01467 {
01468 Rule *rr;
01469 Id d;
01470
01471 if (i == installed->end)
01472 i = installed->start;
01473 s = pool->solvables + i;
01474 if (s->repo != installed)
01475 continue;
01476
01477 if (solv->decisionmap[i] > 0)
01478 continue;
01479 if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start))
01480 continue;
01481 r = solv->rules + solv->updaterules + (i - installed->start);
01482 rr = r;
01483 if (!rr->p || rr->d < 0)
01484 rr -= solv->installed->end - solv->installed->start;
01485 if (!rr->p)
01486 rr = r;
01487 if (!rr->p)
01488 continue;
01489
01490
01491
01492
01493
01494 queue_empty(&dq);
01495 if (!MAPTST(&solv->noupdate, i - installed->start) && (solv->decisionmap[i] < 0 || solv->updatemap_all || (solv->updatemap.size && MAPTST(&solv->updatemap, i - installed->start)) || rr->p != i))
01496 {
01497 if (solv->noobsoletes.size && solv->multiversionupdaters
01498 && (d = solv->multiversionupdaters[i - installed->start]) != 0)
01499 {
01500
01501 queue_push(&dq, i);
01502 while ((p = pool->whatprovidesdata[d++]) != 0)
01503 if (solv->decisionmap[p] >= 0)
01504 queue_push(&dq, p);
01505 policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE);
01506 p = dq.elements[0];
01507 if (p != i && solv->decisionmap[p] == 0)
01508 {
01509 rr = solv->rules + solv->featurerules + (i - solv->installed->start);
01510 if (!rr->p)
01511 rr = rr - solv->featurerules + solv->updaterules;
01512 dq.count = 1;
01513 }
01514 else
01515 dq.count = 0;
01516 }
01517 else
01518 {
01519
01520 FOR_RULELITERALS(p, dp, rr)
01521 {
01522 if (solv->decisionmap[p] > 0)
01523 {
01524 dq.count = 0;
01525 break;
01526 }
01527 if (!solv->decisionmap[p])
01528 queue_push(&dq, p);
01529 }
01530 }
01531 }
01532
01533 if (dq.count)
01534 {
01535 olevel = level;
01536 level = selectandinstall(solv, level, &dq, disablerules, rr - solv->rules);
01537 if (level == 0)
01538 {
01539 queue_free(&dq);
01540 queue_free(&dqs);
01541 return;
01542 }
01543 if (level <= olevel)
01544 {
01545 if (level == 1 || level < passlevel)
01546 break;
01547 if (level < olevel)
01548 n = installed->start;
01549 i--;
01550 n--;
01551 continue;
01552 }
01553 }
01554
01555 if (solv->decisionmap[i] == 0)
01556 {
01557 olevel = level;
01558 if (solv->cleandepsmap.size && MAPTST(&solv->cleandepsmap, i - installed->start))
01559 {
01560 POOL_DEBUG(SAT_DEBUG_POLICY, "cleandeps erasing %s\n", solvid2str(pool, i));
01561 level = setpropagatelearn(solv, level, -i, disablerules, 0);
01562 }
01563 else
01564 {
01565 POOL_DEBUG(SAT_DEBUG_POLICY, "keeping %s\n", solvid2str(pool, i));
01566 level = setpropagatelearn(solv, level, i, disablerules, r - solv->rules);
01567 }
01568 if (level == 0)
01569 {
01570 queue_free(&dq);
01571 queue_free(&dqs);
01572 return;
01573 }
01574 if (level <= olevel)
01575 {
01576 if (level == 1 || level < passlevel)
01577 break;
01578 if (level < olevel)
01579 n = installed->start;
01580 i--;
01581 n--;
01582 continue;
01583 }
01584 }
01585 }
01586 if (n < installed->end)
01587 {
01588 installedpos = i;
01589 break;
01590 }
01591 installedpos = installed->start;
01592 }
01593 systemlevel = level + 1;
01594 if (pass < 2)
01595 continue;
01596 }
01597
01598 if (level < systemlevel)
01599 systemlevel = level;
01600
01601
01602
01603
01604 POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
01605 for (i = 1, n = 1; n < solv->nrules; i++, n++)
01606 {
01607 if (i == solv->nrules)
01608 i = 1;
01609 r = solv->rules + i;
01610 if (r->d < 0)
01611 continue;
01612 queue_empty(&dq);
01613 if (r->d == 0)
01614 {
01615
01616
01617 if (r->p < 0 || r->w2 <= 0)
01618 continue;
01619 if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
01620 continue;
01621 queue_push(&dq, r->p);
01622 queue_push(&dq, r->w2);
01623 }
01624 else
01625 {
01626
01627
01628
01629
01630
01631
01632 if (r->p < 0)
01633 {
01634 if (solv->decisionmap[-r->p] <= 0)
01635 continue;
01636 }
01637 else
01638 {
01639 if (solv->decisionmap[r->p] > 0)
01640 continue;
01641 if (solv->decisionmap[r->p] == 0)
01642 queue_push(&dq, r->p);
01643 }
01644 dp = pool->whatprovidesdata + r->d;
01645 while ((p = *dp++) != 0)
01646 {
01647 if (p < 0)
01648 {
01649 if (solv->decisionmap[-p] <= 0)
01650 break;
01651 }
01652 else
01653 {
01654 if (solv->decisionmap[p] > 0)
01655 break;
01656 if (solv->decisionmap[p] == 0)
01657 queue_push(&dq, p);
01658 }
01659 }
01660 if (p)
01661 continue;
01662 }
01663 IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
01664 {
01665 POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
01666 solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
01667 }
01668
01669
01670 assert(dq.count > 1);
01671
01672 olevel = level;
01673 level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules);
01674 if (level == 0)
01675 {
01676 queue_free(&dq);
01677 queue_free(&dqs);
01678 return;
01679 }
01680 if (level < systemlevel || level == 1)
01681 break;
01682
01683 n = 0;
01684 }
01685
01686 if (n != solv->nrules)
01687 continue;
01688
01689
01690
01691 if (doweak)
01692 {
01693 int qcount;
01694
01695 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
01696 queue_empty(&dq);
01697 queue_empty(&dqs);
01698 for (i = 1; i < pool->nsolvables; i++)
01699 {
01700 if (solv->decisionmap[i] < 0)
01701 continue;
01702 if (solv->decisionmap[i] > 0)
01703 {
01704
01705 Id *recp, rec, pp, p;
01706 s = pool->solvables + i;
01707 if (solv->ignorealreadyrecommended && s->repo == solv->installed)
01708 continue;
01709
01710 if (s->recommends)
01711 {
01712 recp = s->repo->idarraydata + s->recommends;
01713 while ((rec = *recp++) != 0)
01714 {
01715 qcount = dq.count;
01716 FOR_PROVIDES(p, pp, rec)
01717 {
01718 if (solv->decisionmap[p] > 0)
01719 {
01720 dq.count = qcount;
01721 break;
01722 }
01723 else if (solv->decisionmap[p] == 0)
01724 {
01725 queue_pushunique(&dq, p);
01726 }
01727 }
01728 }
01729 }
01730 }
01731 else
01732 {
01733 s = pool->solvables + i;
01734 if (!s->supplements)
01735 continue;
01736 if (!pool_installable(pool, s))
01737 continue;
01738 if (!solver_is_supplementing(solv, s))
01739 continue;
01740 queue_push(&dqs, i);
01741 }
01742 }
01743
01744
01745
01746 if ((dqs.count || dq.count) && solv->installed)
01747 {
01748 Map obsmap;
01749 Id obs, *obsp, po, ppo;
01750
01751 map_init(&obsmap, pool->nsolvables);
01752 for (p = solv->installed->start; p < solv->installed->end; p++)
01753 {
01754 s = pool->solvables + p;
01755 if (s->repo != solv->installed || !s->obsoletes)
01756 continue;
01757 if (solv->decisionmap[p] <= 0)
01758 continue;
01759 if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
01760 continue;
01761 obsp = s->repo->idarraydata + s->obsoletes;
01762
01763 while ((obs = *obsp++) != 0)
01764 FOR_PROVIDES(po, ppo, obs)
01765 MAPSET(&obsmap, po);
01766 }
01767 for (i = j = 0; i < dqs.count; i++)
01768 if (!MAPTST(&obsmap, dqs.elements[i]))
01769 dqs.elements[j++] = dqs.elements[i];
01770 dqs.count = j;
01771 for (i = j = 0; i < dq.count; i++)
01772 if (!MAPTST(&obsmap, dq.elements[i]))
01773 dq.elements[j++] = dq.elements[i];
01774 dq.count = j;
01775 map_free(&obsmap);
01776 }
01777
01778
01779 if (solv->ignorealreadyrecommended && dqs.count)
01780 {
01781
01782 for (i = 0; i < solv->decisionq.count; i++)
01783 {
01784 p = solv->decisionq.elements[i];
01785 if (p < 0)
01786 continue;
01787 s = pool->solvables + p;
01788 if (s->repo && s->repo != solv->installed)
01789 solv->decisionmap[p] = -solv->decisionmap[p];
01790 }
01791
01792 for (i = j = 0; i < dqs.count; i++)
01793 {
01794 p = dqs.elements[i];
01795 s = pool->solvables + p;
01796 if (!s->supplements)
01797 continue;
01798 if (!solver_is_supplementing(solv, s))
01799 dqs.elements[j++] = p;
01800 }
01801 dqs.count = j;
01802
01803 for (i = 0; i < solv->decisionq.count; i++)
01804 {
01805 p = solv->decisionq.elements[i];
01806 if (p < 0)
01807 continue;
01808 s = pool->solvables + p;
01809 if (s->repo && s->repo != solv->installed)
01810 solv->decisionmap[p] = -solv->decisionmap[p];
01811 }
01812 }
01813
01814
01815
01816
01817 if (dqs.count && solv->noobsoletes.size)
01818 {
01819 for (i = j = 0; i < dqs.count; i++)
01820 {
01821 p = dqs.elements[i];
01822 if (MAPTST(&solv->noobsoletes, p))
01823 {
01824 Id p2, pp2;
01825 s = pool->solvables + p;
01826 FOR_PROVIDES(p2, pp2, s->name)
01827 if (solv->decisionmap[p2] > 0 && pool->solvables[p2].name == s->name)
01828 break;
01829 if (p2)
01830 continue;
01831 }
01832 dqs.elements[j++] = p;
01833 }
01834 dqs.count = j;
01835 }
01836
01837
01838 if (dqs.count)
01839 {
01840 for (i = 0; i < dqs.count; i++)
01841 queue_pushunique(&dq, dqs.elements[i]);
01842 }
01843
01844 if (dq.count)
01845 {
01846 Map dqmap;
01847 int decisioncount = solv->decisionq.count;
01848
01849 if (dq.count == 1)
01850 {
01851
01852 p = dq.elements[0];
01853 if (dqs.count)
01854 POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
01855 else
01856 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
01857 queue_push(&solv->recommendations, p);
01858 level = setpropagatelearn(solv, level, p, 0, 0);
01859 continue;
01860 }
01861
01862
01863 policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
01864
01865
01866 map_init(&dqmap, pool->nsolvables);
01867 for (i = 0; i < dq.count; i++)
01868 MAPSET(&dqmap, dq.elements[i]);
01869
01870
01871 for (i = 0; i < dqs.count; i++)
01872 {
01873 p = dqs.elements[i];
01874 if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
01875 continue;
01876 POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
01877 queue_push(&solv->recommendations, p);
01878 olevel = level;
01879 level = setpropagatelearn(solv, level, p, 0, 0);
01880 if (level <= olevel)
01881 break;
01882 }
01883 if (i < dqs.count || solv->decisionq.count < decisioncount)
01884 {
01885 map_free(&dqmap);
01886 continue;
01887 }
01888
01889
01890
01891
01892 for (i = 0; i < decisioncount; i++)
01893 {
01894 Id rec, *recp, pp;
01895 p = solv->decisionq.elements[i];
01896 if (p < 0)
01897 continue;
01898 s = pool->solvables + p;
01899 if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
01900 continue;
01901 if (!s->recommends)
01902 continue;
01903 recp = s->repo->idarraydata + s->recommends;
01904 while ((rec = *recp++) != 0)
01905 {
01906 queue_empty(&dq);
01907 FOR_PROVIDES(p, pp, rec)
01908 {
01909 if (solv->decisionmap[p] > 0)
01910 {
01911 dq.count = 0;
01912 break;
01913 }
01914 else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
01915 queue_pushunique(&dq, p);
01916 }
01917 if (!dq.count)
01918 continue;
01919 if (dq.count > 1)
01920 {
01921
01922 for (i = 1; i < dq.count; i++)
01923 queue_push(&solv->branches, dq.elements[i]);
01924 queue_push(&solv->branches, -level);
01925 }
01926 p = dq.elements[0];
01927 POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
01928 queue_push(&solv->recommendations, p);
01929 olevel = level;
01930 level = setpropagatelearn(solv, level, p, 0, 0);
01931 if (level <= olevel || solv->decisionq.count < decisioncount)
01932 break;
01933 }
01934 if (rec)
01935 break;
01936 }
01937 map_free(&dqmap);
01938
01939 continue;
01940 }
01941 }
01942
01943 if (solv->dupmap_all && solv->installed)
01944 {
01945 int installedone = 0;
01946
01947
01948 POOL_DEBUG(SAT_DEBUG_SOLVER, "deciding orphaned packages\n");
01949 for (i = 0; i < solv->orphaned.count; i++)
01950 {
01951 p = solv->orphaned.elements[i];
01952 if (solv->decisionmap[p])
01953 continue;
01954 olevel = level;
01955 if (solv->droporphanedmap_all)
01956 continue;
01957 if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))
01958 continue;
01959 POOL_DEBUG(SAT_DEBUG_SOLVER, "keeping orphaned %s\n", solvid2str(pool, p));
01960 level = setpropagatelearn(solv, level, p, 0, 0);
01961 installedone = 1;
01962 if (level < olevel)
01963 break;
01964 }
01965 if (installedone || i < solv->orphaned.count)
01966 continue;
01967 for (i = 0; i < solv->orphaned.count; i++)
01968 {
01969 p = solv->orphaned.elements[i];
01970 if (solv->decisionmap[p])
01971 continue;
01972 POOL_DEBUG(SAT_DEBUG_SOLVER, "removing orphaned %s\n", solvid2str(pool, p));
01973 olevel = level;
01974 level = setpropagatelearn(solv, level, -p, 0, 0);
01975 if (level < olevel)
01976 break;
01977 }
01978 if (i < solv->orphaned.count)
01979 continue;
01980 }
01981
01982 if (solv->solution_callback)
01983 {
01984 solv->solution_callback(solv, solv->solution_callback_data);
01985 if (solv->branches.count)
01986 {
01987 int i = solv->branches.count - 1;
01988 int l = -solv->branches.elements[i];
01989 Id why;
01990
01991 for (; i > 0; i--)
01992 if (solv->branches.elements[i - 1] < 0)
01993 break;
01994 p = solv->branches.elements[i];
01995 POOL_DEBUG(SAT_DEBUG_SOLVER, "branching with %s\n", solvid2str(pool, p));
01996 queue_empty(&dq);
01997 for (j = i + 1; j < solv->branches.count; j++)
01998 queue_push(&dq, solv->branches.elements[j]);
01999 solv->branches.count = i;
02000 level = l;
02001 revert(solv, level);
02002 if (dq.count > 1)
02003 for (j = 0; j < dq.count; j++)
02004 queue_push(&solv->branches, dq.elements[j]);
02005 olevel = level;
02006 why = -solv->decisionq_why.elements[solv->decisionq_why.count];
02007 assert(why >= 0);
02008 level = setpropagatelearn(solv, level, p, disablerules, why);
02009 if (level == 0)
02010 {
02011 queue_free(&dq);
02012 queue_free(&dqs);
02013 return;
02014 }
02015 continue;
02016 }
02017
02018 break;
02019 }
02020
02021
02022 if (solv->branches.count)
02023 {
02024 int l = 0, lasti = -1, lastl = -1;
02025 Id why;
02026
02027 p = 0;
02028 for (i = solv->branches.count - 1; i >= 0; i--)
02029 {
02030 p = solv->branches.elements[i];
02031 if (p < 0)
02032 l = -p;
02033 else if (p > 0 && solv->decisionmap[p] > l + 1)
02034 {
02035 lasti = i;
02036 lastl = l;
02037 }
02038 }
02039 if (lasti >= 0)
02040 {
02041
02042 p = solv->branches.elements[lasti];
02043 solv->branches.elements[lasti] = 0;
02044 POOL_DEBUG(SAT_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, solvid2str(pool, p));
02045 minimizationsteps++;
02046
02047 level = lastl;
02048 revert(solv, level);
02049 why = -solv->decisionq_why.elements[solv->decisionq_why.count];
02050 assert(why >= 0);
02051 olevel = level;
02052 level = setpropagatelearn(solv, level, p, disablerules, why);
02053 if (level == 0)
02054 {
02055 queue_free(&dq);
02056 queue_free(&dqs);
02057 return;
02058 }
02059 continue;
02060 }
02061 }
02062
02063 break;
02064 }
02065
02066 POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
02067
02068 POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
02069 queue_free(&dq);
02070 queue_free(&dqs);
02071 #if 0
02072 solver_printdecisionq(solv, SAT_DEBUG_RESULT);
02073 #endif
02074 }
02075
02076
02077
02078
02079
02080
02081
02082
02083
02084
02085
02086 static void
02087 removedisabledconflicts(Solver *solv, Queue *removed)
02088 {
02089 Pool *pool = solv->pool;
02090 int i, n;
02091 Id p, why, *dp;
02092 Id new;
02093 Rule *r;
02094 Id *decisionmap = solv->decisionmap;
02095
02096 POOL_DEBUG(SAT_DEBUG_SCHUBI, "removedisabledconflicts\n");
02097 queue_empty(removed);
02098 for (i = 0; i < solv->decisionq.count; i++)
02099 {
02100 p = solv->decisionq.elements[i];
02101 if (p > 0)
02102 continue;
02103 why = solv->decisionq_why.elements[i];
02104 if (why == 0)
02105 {
02106
02107 continue;
02108 }
02109
02110
02111 assert(why > 0);
02112 r = solv->rules + why;
02113 if (r->d < 0 && decisionmap[-p])
02114 {
02115
02116 POOL_DEBUG(SAT_DEBUG_SCHUBI, "removing conflict for package %s[%d]\n", solvid2str(pool, -p), -p);
02117 queue_push(removed, -p);
02118 queue_push(removed, decisionmap[-p]);
02119 decisionmap[-p] = 0;
02120 }
02121 }
02122 if (!removed->count)
02123 return;
02124
02125
02126 new = 0;
02127 for (i = n = 1, r = solv->rules + i; n < solv->nrules; i++, r++, n++)
02128 {
02129 if (i == solv->nrules)
02130 {
02131 i = 1;
02132 r = solv->rules + i;
02133 }
02134 if (r->d < 0)
02135 continue;
02136 if (!r->w2)
02137 {
02138 if (r->p < 0 && !decisionmap[-r->p])
02139 new = r->p;
02140 }
02141 else if (!r->d)
02142 {
02143
02144 if (r->p < 0 && decisionmap[-r->p] == 0 && DECISIONMAP_FALSE(r->w2))
02145 new = r->p;
02146 else if (r->w2 < 0 && decisionmap[-r->w2] == 0 && DECISIONMAP_FALSE(r->p))
02147 new = r->w2;
02148 }
02149 else
02150 {
02151 if (r->p < 0 && decisionmap[-r->p] == 0)
02152 new = r->p;
02153 if (new || DECISIONMAP_FALSE(r->p))
02154 {
02155 dp = pool->whatprovidesdata + r->d;
02156 while ((p = *dp++) != 0)
02157 {
02158 if (new && p == new)
02159 continue;
02160 if (p < 0 && decisionmap[-p] == 0)
02161 {
02162 if (new)
02163 {
02164 new = 0;
02165 break;
02166 }
02167 new = p;
02168 }
02169 else if (!DECISIONMAP_FALSE(p))
02170 {
02171 new = 0;
02172 break;
02173 }
02174 }
02175 }
02176 }
02177 if (new)
02178 {
02179 POOL_DEBUG(SAT_DEBUG_SCHUBI, "re-conflicting package %s[%d]\n", solvid2str(pool, -new), -new);
02180 decisionmap[-new] = -1;
02181 new = 0;
02182 n = 0;
02183 }
02184 }
02185 }
02186
02187 static inline void
02188 undo_removedisabledconflicts(Solver *solv, Queue *removed)
02189 {
02190 int i;
02191 for (i = 0; i < removed->count; i += 2)
02192 solv->decisionmap[removed->elements[i]] = removed->elements[i + 1];
02193 }
02194
02195
02196
02197
02198
02199
02200
02201 static void
02202 weaken_solvable_deps(Solver *solv, Id p)
02203 {
02204 int i;
02205 Rule *r;
02206
02207 for (i = 1, r = solv->rules + i; i < solv->rpmrules_end; i++, r++)
02208 {
02209 if (r->p != -p)
02210 continue;
02211 if ((r->d == 0 || r->d == -1) && r->w2 < 0)
02212 continue;
02213 queue_push(&solv->weakruleq, i);
02214 }
02215 }
02216
02217
02218
02219
02220
02221
02222 static void
02223 findrecommendedsuggested(Solver *solv)
02224 {
02225 Pool *pool = solv->pool;
02226 Queue redoq, disabledq;
02227 int goterase, i;
02228 Solvable *s;
02229 Rule *r;
02230 Map obsmap;
02231
02232 map_init(&obsmap, pool->nsolvables);
02233 if (solv->installed)
02234 {
02235 Id obs, *obsp, p, po, ppo;
02236 for (p = solv->installed->start; p < solv->installed->end; p++)
02237 {
02238 s = pool->solvables + p;
02239 if (s->repo != solv->installed || !s->obsoletes)
02240 continue;
02241 if (solv->decisionmap[p] <= 0)
02242 continue;
02243 if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
02244 continue;
02245 obsp = s->repo->idarraydata + s->obsoletes;
02246
02247 while ((obs = *obsp++) != 0)
02248 FOR_PROVIDES(po, ppo, obs)
02249 MAPSET(&obsmap, po);
02250 }
02251 }
02252
02253 queue_init(&redoq);
02254 queue_init(&disabledq);
02255 goterase = 0;
02256
02257 for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
02258 {
02259 if (r->d < 0)
02260 continue;
02261 if (r->p >= 0)
02262 continue;
02263 queue_push(&disabledq, i);
02264 solver_disablerule(solv, r);
02265 goterase++;
02266 }
02267
02268 if (goterase)
02269 {
02270 enabledisablelearntrules(solv);
02271 removedisabledconflicts(solv, &redoq);
02272 }
02273
02274
02275
02276
02277
02278
02279
02280 if (redoq.count || solv->dontinstallrecommended || !solv->dontshowinstalledrecommended || solv->ignorealreadyrecommended)
02281 {
02282 Id rec, *recp, p, pp;
02283
02284
02285 solv->recommends_index = -1;
02286 MAPZERO(&solv->recommendsmap);
02287 for (i = 0; i < solv->decisionq.count; i++)
02288 {
02289 p = solv->decisionq.elements[i];
02290 if (p < 0)
02291 continue;
02292 s = pool->solvables + p;
02293 if (s->recommends)
02294 {
02295 recp = s->repo->idarraydata + s->recommends;
02296 while ((rec = *recp++) != 0)
02297 {
02298 FOR_PROVIDES(p, pp, rec)
02299 if (solv->decisionmap[p] > 0)
02300 break;
02301 if (p)
02302 {
02303 if (!solv->dontshowinstalledrecommended)
02304 {
02305 FOR_PROVIDES(p, pp, rec)
02306 if (solv->decisionmap[p] > 0)
02307 MAPSET(&solv->recommendsmap, p);
02308 }
02309 continue;
02310 }
02311 FOR_PROVIDES(p, pp, rec)
02312 MAPSET(&solv->recommendsmap, p);
02313 }
02314 }
02315 }
02316 for (i = 1; i < pool->nsolvables; i++)
02317 {
02318 if (solv->decisionmap[i] < 0)
02319 continue;
02320 if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
02321 continue;
02322 if (MAPTST(&obsmap, i))
02323 continue;
02324 s = pool->solvables + i;
02325 if (!MAPTST(&solv->recommendsmap, i))
02326 {
02327 if (!s->supplements)
02328 continue;
02329 if (!pool_installable(pool, s))
02330 continue;
02331 if (!solver_is_supplementing(solv, s))
02332 continue;
02333 }
02334 if (solv->dontinstallrecommended)
02335 queue_push(&solv->recommendations, i);
02336 else
02337 queue_pushunique(&solv->recommendations, i);
02338 }
02339
02340 policy_filter_unwanted(solv, &solv->recommendations, POLICY_MODE_SUGGEST);
02341 }
02342
02343
02344
02345
02346
02347 if (1)
02348 {
02349 Id sug, *sugp, p, pp;
02350
02351
02352 solv->recommends_index = -1;
02353 MAPZERO(&solv->suggestsmap);
02354 for (i = 0; i < solv->decisionq.count; i++)
02355 {
02356 p = solv->decisionq.elements[i];
02357 if (p < 0)
02358 continue;
02359 s = pool->solvables + p;
02360 if (s->suggests)
02361 {
02362 sugp = s->repo->idarraydata + s->suggests;
02363 while ((sug = *sugp++) != 0)
02364 {
02365 FOR_PROVIDES(p, pp, sug)
02366 if (solv->decisionmap[p] > 0)
02367 break;
02368 if (p)
02369 {
02370 if (!solv->dontshowinstalledrecommended)
02371 {
02372 FOR_PROVIDES(p, pp, sug)
02373 if (solv->decisionmap[p] > 0)
02374 MAPSET(&solv->suggestsmap, p);
02375 }
02376 continue;
02377 }
02378 FOR_PROVIDES(p, pp, sug)
02379 MAPSET(&solv->suggestsmap, p);
02380 }
02381 }
02382 }
02383 for (i = 1; i < pool->nsolvables; i++)
02384 {
02385 if (solv->decisionmap[i] < 0)
02386 continue;
02387 if (solv->decisionmap[i] > 0 && solv->dontshowinstalledrecommended)
02388 continue;
02389 if (MAPTST(&obsmap, i))
02390 continue;
02391 s = pool->solvables + i;
02392 if (!MAPTST(&solv->suggestsmap, i))
02393 {
02394 if (!s->enhances)
02395 continue;
02396 if (!pool_installable(pool, s))
02397 continue;
02398 if (!solver_is_enhancing(solv, s))
02399 continue;
02400 }
02401 queue_push(&solv->suggestions, i);
02402 }
02403 policy_filter_unwanted(solv, &solv->suggestions, POLICY_MODE_SUGGEST);
02404 }
02405
02406
02407 if (redoq.count)
02408 undo_removedisabledconflicts(solv, &redoq);
02409 queue_free(&redoq);
02410
02411
02412 for (i = 0; i < disabledq.count; i++)
02413 solver_enablerule(solv, solv->rules + disabledq.elements[i]);
02414 queue_free(&disabledq);
02415 map_free(&obsmap);
02416 }
02417
02418 void
02419 solver_calculate_noobsmap(Pool *pool, Queue *job, Map *noobsmap)
02420 {
02421 int i;
02422 Id how, what, select;
02423 Id p, pp;
02424 for (i = 0; i < job->count; i += 2)
02425 {
02426 how = job->elements[i];
02427 if ((how & SOLVER_JOBMASK) != SOLVER_NOOBSOLETES)
02428 continue;
02429 what = job->elements[i + 1];
02430 select = how & SOLVER_SELECTMASK;
02431 if (!noobsmap->size)
02432 map_grow(noobsmap, pool->nsolvables);
02433 FOR_JOB_SELECT(p, pp, select, what)
02434 MAPSET(noobsmap, p);
02435 }
02436 }
02437
02438
02439
02440
02441 static inline void
02442 solver_addjobrule(Solver *solv, Id p, Id d, Id job, int weak)
02443 {
02444 solver_addrule(solv, p, d);
02445 queue_push(&solv->ruletojob, job);
02446 if (weak)
02447 queue_push(&solv->weakruleq, solv->nrules - 1);
02448 }
02449
02450
02451
02452
02453
02454
02455
02456 void
02457 solver_solve(Solver *solv, Queue *job)
02458 {
02459 Pool *pool = solv->pool;
02460 Repo *installed = solv->installed;
02461 int i;
02462 int oldnrules;
02463 Map addedmap;
02464 Map installcandidatemap;
02465 Id how, what, select, name, weak, p, pp, d;
02466 Queue q;
02467 Solvable *s;
02468 Rule *r;
02469 int now, solve_start;
02470 int hasdupjob = 0;
02471
02472 solve_start = sat_timems(0);
02473
02474
02475 POOL_DEBUG(SAT_DEBUG_STATS, "solver started\n");
02476 POOL_DEBUG(SAT_DEBUG_STATS, "fixsystem=%d updatesystem=%d dosplitprovides=%d, noupdateprovide=%d noinfarchcheck=%d\n", solv->fixsystem, solv->updatesystem, solv->dosplitprovides, solv->noupdateprovide, solv->noinfarchcheck);
02477 POOL_DEBUG(SAT_DEBUG_STATS, "distupgrade=%d distupgrade_removeunsupported=%d\n", solv->distupgrade, solv->distupgrade_removeunsupported);
02478 POOL_DEBUG(SAT_DEBUG_STATS, "allowuninstall=%d, allowdowngrade=%d, allowarchchange=%d, allowvendorchange=%d\n", solv->allowuninstall, solv->allowdowngrade, solv->allowarchchange, solv->allowvendorchange);
02479 POOL_DEBUG(SAT_DEBUG_STATS, "promoteepoch=%d, novirtualconflicts=%d, allowselfconflicts=%d\n", pool->promoteepoch, pool->novirtualconflicts, pool->allowselfconflicts);
02480 POOL_DEBUG(SAT_DEBUG_STATS, "obsoleteusesprovides=%d, implicitobsoleteusesprovides=%d, obsoleteusescolors=%d\n", pool->obsoleteusesprovides, pool->implicitobsoleteusesprovides, pool->obsoleteusescolors);
02481 POOL_DEBUG(SAT_DEBUG_STATS, "dontinstallrecommended=%d, ignorealreadyrecommended=%d, dontshowinstalledrecommended=%d\n", solv->dontinstallrecommended, solv->ignorealreadyrecommended, solv->dontshowinstalledrecommended);
02482
02483
02484 if (!pool->whatprovides)
02485 pool_createwhatprovides(pool);
02486
02487
02488 policy_create_obsolete_index(solv);
02489
02490
02491 queue_free(&solv->job);
02492 queue_init_clone(&solv->job, job);
02493
02494
02495 solv->fixmap_all = solv->fixsystem;
02496 solv->updatemap_all = solv->updatesystem;
02497 solv->droporphanedmap_all = solv->distupgrade_removeunsupported;
02498 solv->dupmap_all = solv->distupgrade;
02499
02500
02501
02502
02503
02504
02505
02506 solver_calculate_noobsmap(pool, job, &solv->noobsoletes);
02507
02508 map_init(&addedmap, pool->nsolvables);
02509 MAPSET(&addedmap, SYSTEMSOLVABLE);
02510
02511 map_init(&installcandidatemap, pool->nsolvables);
02512 queue_init(&q);
02513
02514 now = sat_timems(0);
02515
02516
02517
02518
02519
02520 if (installed)
02521 {
02522
02523 for (i = 0; i < job->count; i += 2)
02524 {
02525 how = job->elements[i];
02526 what = job->elements[i + 1];
02527 select = how & SOLVER_SELECTMASK;
02528 switch (how & SOLVER_JOBMASK)
02529 {
02530 case SOLVER_VERIFY:
02531 if (select == SOLVER_SOLVABLE_ALL)
02532 solv->fixmap_all = 1;
02533 FOR_JOB_SELECT(p, pp, select, what)
02534 {
02535 s = pool->solvables + p;
02536 if (!solv->installed || s->repo != solv->installed)
02537 continue;
02538 if (!solv->fixmap.size)
02539 map_grow(&solv->fixmap, solv->installed->end - solv->installed->start);
02540 MAPSET(&solv->fixmap, p - solv->installed->start);
02541 }
02542 break;
02543 case SOLVER_UPDATE:
02544 if (select == SOLVER_SOLVABLE_ALL)
02545 solv->updatemap_all = 1;
02546 FOR_JOB_SELECT(p, pp, select, what)
02547 {
02548 s = pool->solvables + p;
02549 if (!solv->installed || s->repo != solv->installed)
02550 continue;
02551 if (!solv->updatemap.size)
02552 map_grow(&solv->updatemap, solv->installed->end - solv->installed->start);
02553 MAPSET(&solv->updatemap, p - solv->installed->start);
02554 }
02555 break;
02556 default:
02557 break;
02558 }
02559 }
02560
02561 oldnrules = solv->nrules;
02562 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for installed solvables ***\n");
02563 FOR_REPO_SOLVABLES(installed, p, s)
02564 solver_addrpmrulesforsolvable(solv, s, &addedmap);
02565 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for installed solvables\n", solv->nrules - oldnrules);
02566 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for updaters of installed solvables ***\n");
02567 oldnrules = solv->nrules;
02568 FOR_REPO_SOLVABLES(installed, p, s)
02569 solver_addrpmrulesforupdaters(solv, s, &addedmap, 1);
02570 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for updaters of installed solvables\n", solv->nrules - oldnrules);
02571 }
02572
02573
02574
02575
02576
02577
02578 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for packages involved with a job ***\n");
02579 oldnrules = solv->nrules;
02580 for (i = 0; i < job->count; i += 2)
02581 {
02582 how = job->elements[i];
02583 what = job->elements[i + 1];
02584 select = how & SOLVER_SELECTMASK;
02585
02586 switch (how & SOLVER_JOBMASK)
02587 {
02588 case SOLVER_INSTALL:
02589 FOR_JOB_SELECT(p, pp, select, what)
02590 {
02591 MAPSET(&installcandidatemap, p);
02592 solver_addrpmrulesforsolvable(solv, pool->solvables + p, &addedmap);
02593 }
02594 break;
02595 case SOLVER_DISTUPGRADE:
02596 if (select == SOLVER_SOLVABLE_ALL)
02597 {
02598 solv->dupmap_all = 1;
02599 solv->updatemap_all = 1;
02600 }
02601 if (!solv->dupmap_all)
02602 hasdupjob = 1;
02603 break;
02604 default:
02605 break;
02606 }
02607 }
02608 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules for packages involved in a job\n", solv->nrules - oldnrules);
02609
02610
02611
02612
02613
02614 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** create rpm rules for suggested/enhanced packages ***\n");
02615 oldnrules = solv->nrules;
02616 solver_addrpmrulesforweak(solv, &addedmap);
02617 POOL_DEBUG(SAT_DEBUG_STATS, "added %d rpm rules because of weak dependencies\n", solv->nrules - oldnrules);
02618
02619
02620
02621
02622
02623
02624
02625
02626
02627 IF_POOLDEBUG (SAT_DEBUG_STATS)
02628 {
02629 int possible = 0, installable = 0;
02630 for (i = 1; i < pool->nsolvables; i++)
02631 {
02632 if (pool_installable(pool, pool->solvables + i))
02633 installable++;
02634 if (MAPTST(&addedmap, i))
02635 possible++;
02636 }
02637 POOL_DEBUG(SAT_DEBUG_STATS, "%d of %d installable solvables considered for solving\n", possible, installable);
02638 }
02639
02640 solver_unifyrules(solv);
02641 solv->rpmrules_end = solv->nrules;
02642
02643 POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule memory usage: %d K\n", solv->nrules * (int)sizeof(Rule) / 1024);
02644 POOL_DEBUG(SAT_DEBUG_STATS, "rpm rule creation took %d ms\n", sat_timems(now));
02645
02646
02647
02648 if (hasdupjob)
02649 solver_createdupmaps(solv);
02650
02651
02652
02653
02654
02655
02656
02657
02658
02659
02660
02661
02662
02663 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add feature rules ***\n");
02664 solv->featurerules = solv->nrules;
02665 if (installed)
02666 {
02667
02668 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
02669 {
02670 if (s->repo != installed)
02671 {
02672 solver_addrule(solv, 0, 0);
02673 continue;
02674 }
02675 solver_addupdaterule(solv, s, 1);
02676 }
02677
02678 assert(solv->nrules - solv->featurerules == installed->end - installed->start);
02679 }
02680 solv->featurerules_end = solv->nrules;
02681
02682
02683
02684
02685
02686
02687
02688
02689 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add update rules ***\n");
02690 solv->updaterules = solv->nrules;
02691
02692 if (installed)
02693 {
02694
02695 for (i = installed->start, s = pool->solvables + i; i < installed->end; i++, s++)
02696 {
02697 Rule *sr;
02698
02699 if (s->repo != installed)
02700 {
02701 solver_addrule(solv, 0, 0);
02702 continue;
02703 }
02704 solver_addupdaterule(solv, s, 0);
02705
02706
02707
02708 r = solv->rules + solv->nrules - 1;
02709 sr = r - (installed->end - installed->start);
02710
02711
02712 if (!sr->p || (sr->p == i && !sr->d && !sr->w2))
02713 queue_push(&solv->orphaned, i);
02714 if (!r->p)
02715 {
02716 assert(solv->dupmap_all && !sr->p);
02717 continue;
02718 }
02719 if (!solver_samerule(solv, r, sr))
02720 {
02721
02722 if (solv->allowuninstall)
02723 {
02724
02725 memset(r, 0, sizeof(*r));
02726 queue_push(&solv->weakruleq, sr - solv->rules);
02727 }
02728 else
02729 {
02730
02731 memset(sr, 0, sizeof(*sr));
02732 }
02733 }
02734 else if (solv->allowuninstall)
02735 {
02736
02737 queue_push(&solv->weakruleq, r - solv->rules);
02738 queue_push(&solv->weakruleq, sr - solv->rules);
02739 }
02740 else
02741 solver_disablerule(solv, sr);
02742 }
02743
02744 assert(solv->nrules - solv->updaterules == installed->end - installed->start);
02745 }
02746 solv->updaterules_end = solv->nrules;
02747
02748
02749
02750
02751
02752
02753 POOL_DEBUG(SAT_DEBUG_SCHUBI, "*** Add JOB rules ***\n");
02754
02755 solv->jobrules = solv->nrules;
02756 for (i = 0; i < job->count; i += 2)
02757 {
02758 oldnrules = solv->nrules;
02759
02760 how = job->elements[i];
02761 what = job->elements[i + 1];
02762 weak = how & SOLVER_WEAK;
02763 select = how & SOLVER_SELECTMASK;
02764 switch (how & SOLVER_JOBMASK)
02765 {
02766 case SOLVER_INSTALL:
02767 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sinstall %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02768 if (select == SOLVER_SOLVABLE)
02769 {
02770 p = what;
02771 d = 0;
02772 }
02773 else
02774 {
02775 queue_empty(&q);
02776 FOR_JOB_SELECT(p, pp, select, what)
02777 queue_push(&q, p);
02778 if (!q.count)
02779 {
02780
02781 queue_push(&q, -SYSTEMSOLVABLE);
02782 }
02783 p = queue_shift(&q);
02784 d = !q.count ? 0 : pool_queuetowhatprovides(pool, &q);
02785 }
02786 solver_addjobrule(solv, p, d, i, weak);
02787 break;
02788 case SOLVER_ERASE:
02789 POOL_DEBUG(SAT_DEBUG_JOB, "job: %s%serase %s\n", weak ? "weak " : "", how & SOLVER_CLEANDEPS ? "clean deps " : "", solver_select2str(pool, select, what));
02790 if ((how & SOLVER_CLEANDEPS) != 0 && !solv->cleandepsmap.size && solv->installed)
02791 map_grow(&solv->cleandepsmap, solv->installed->end - solv->installed->start);
02792 if (select == SOLVER_SOLVABLE && solv->installed && pool->solvables[what].repo == solv->installed)
02793 {
02794
02795
02796
02797
02798 name = pool->solvables[what].name;
02799 FOR_PROVIDES(p, pp, name)
02800 {
02801 if (p == what)
02802 continue;
02803 s = pool->solvables + p;
02804 if (s->name != name)
02805 continue;
02806
02807 if (s->repo == solv->installed)
02808 continue;
02809
02810 if (MAPTST(&installcandidatemap, p))
02811 continue;
02812 solver_addjobrule(solv, -p, 0, i, weak);
02813 }
02814 }
02815 FOR_JOB_SELECT(p, pp, select, what)
02816 solver_addjobrule(solv, -p, 0, i, weak);
02817 break;
02818
02819 case SOLVER_UPDATE:
02820 POOL_DEBUG(SAT_DEBUG_JOB, "job: %supdate %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02821 break;
02822 case SOLVER_VERIFY:
02823 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sverify %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02824 break;
02825 case SOLVER_WEAKENDEPS:
02826 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sweaken deps %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02827 if (select != SOLVER_SOLVABLE)
02828 break;
02829 s = pool->solvables + what;
02830 weaken_solvable_deps(solv, what);
02831 break;
02832 case SOLVER_NOOBSOLETES:
02833 POOL_DEBUG(SAT_DEBUG_JOB, "job: %sno obsolete %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02834 break;
02835 case SOLVER_LOCK:
02836 POOL_DEBUG(SAT_DEBUG_JOB, "job: %slock %s\n", weak ? "weak " : "", solver_select2str(pool, select, what));
02837 FOR_JOB_SELECT(p, pp, select, what)
02838 {
02839 s = pool->solvables + p;
02840 solver_addjobrule(solv, installed && s->repo == installed ? p : -p, 0, i, weak);
02841 }
02842 break;
02843 case SOLVER_DISTUPGRADE:
02844 POOL_DEBUG(SAT_DEBUG_JOB, "job: distupgrade %s\n", solver_select2str(pool, select, what));
02845 break;
02846 case SOLVER_DROP_ORPHANED:
02847 POOL_DEBUG(SAT_DEBUG_JOB, "job: drop orphaned %s\n", solver_select2str(pool, select, what));
02848 if (select == SOLVER_SOLVABLE_ALL)
02849 solv->droporphanedmap_all = 1;
02850 FOR_JOB_SELECT(p, pp, select, what)
02851 {
02852 s = pool->solvables + p;
02853 if (!installed || s->repo != installed)
02854 continue;
02855 if (!solv->droporphanedmap.size)
02856 map_grow(&solv->droporphanedmap, installed->end - installed->start);
02857 MAPSET(&solv->droporphanedmap, p - installed->start);
02858 }
02859 break;
02860 case SOLVER_USERINSTALLED:
02861 POOL_DEBUG(SAT_DEBUG_JOB, "job: user installed %s\n", solver_select2str(pool, select, what));
02862 break;
02863 default:
02864 POOL_DEBUG(SAT_DEBUG_JOB, "job: unknown job\n");
02865 break;
02866 }
02867
02868
02869
02870
02871
02872 IF_POOLDEBUG (SAT_DEBUG_JOB)
02873 {
02874 int j;
02875 if (solv->nrules == oldnrules)
02876 POOL_DEBUG(SAT_DEBUG_JOB, " - no rule created\n");
02877 for (j = oldnrules; j < solv->nrules; j++)
02878 {
02879 POOL_DEBUG(SAT_DEBUG_JOB, " - job ");
02880 solver_printrule(solv, SAT_DEBUG_JOB, solv->rules + j);
02881 }
02882 }
02883 }
02884 assert(solv->ruletojob.count == solv->nrules - solv->jobrules);
02885 solv->jobrules_end = solv->nrules;
02886
02887
02888 if (!solv->noinfarchcheck)
02889 {
02890 solver_addinfarchrules(solv, &addedmap);
02891 if (pool->obsoleteusescolors)
02892 {
02893
02894
02895 for (i = solv->infarchrules; i < solv->infarchrules_end; i++)
02896 queue_push(&solv->weakruleq, i);
02897 }
02898 }
02899 else
02900 solv->infarchrules = solv->infarchrules_end = solv->nrules;
02901
02902 if (hasdupjob)
02903 {
02904 solver_addduprules(solv, &addedmap);
02905 solver_freedupmaps(solv);
02906 }
02907 else
02908 solv->duprules = solv->duprules_end = solv->nrules;
02909
02910 if (1)
02911 solver_addchoicerules(solv);
02912 else
02913 solv->choicerules = solv->choicerules_end = solv->nrules;
02914
02915
02916
02917
02918
02919
02920
02921 map_free(&addedmap);
02922 map_free(&installcandidatemap);
02923 queue_free(&q);
02924
02925 POOL_DEBUG(SAT_DEBUG_STATS, "%d rpm rules, %d job rules, %d infarch rules, %d dup rules, %d choice rules\n", solv->rpmrules_end - 1, solv->jobrules_end - solv->jobrules, solv->infarchrules_end - solv->infarchrules, solv->duprules_end - solv->duprules, solv->choicerules_end - solv->choicerules);
02926
02927
02928 map_init(&solv->weakrulemap, solv->nrules);
02929 for (i = 0; i < solv->weakruleq.count; i++)
02930 {
02931 p = solv->weakruleq.elements[i];
02932 MAPSET(&solv->weakrulemap, p);
02933 }
02934
02935
02936 solv->learntrules = solv->nrules;
02937
02938
02939 makewatches(solv);
02940
02941
02942
02943 for (i = 1, r = solv->rules + i; i < solv->nrules; i++, r++)
02944 if (r->p && !r->w2 && (r->d == 0 || r->d == -1))
02945 queue_push(&solv->ruleassertions, i);
02946
02947
02948 solver_disablepolicyrules(solv);
02949
02950
02951 makeruledecisions(solv);
02952 POOL_DEBUG(SAT_DEBUG_SOLVER, "problems so far: %d\n", solv->problems.count);
02953
02954
02955
02956
02957
02958
02959
02960 now = sat_timems(0);
02961 solver_run_sat(solv, 1, solv->dontinstallrecommended ? 0 : 1);
02962 POOL_DEBUG(SAT_DEBUG_STATS, "solver took %d ms\n", sat_timems(now));
02963
02964
02965
02966
02967 findrecommendedsuggested(solv);
02968
02969
02970
02971
02972 solver_prepare_solutions(solv);
02973
02974
02975
02976
02977 transaction_calculate(&solv->trans, &solv->decisionq, &solv->noobsoletes);
02978
02979 POOL_DEBUG(SAT_DEBUG_STATS, "final solver statistics: %d problems, %d learned rules, %d unsolvable\n", solv->problems.count / 2, solv->stats_learned, solv->stats_unsolvable);
02980 POOL_DEBUG(SAT_DEBUG_STATS, "solver_solve took %d ms\n", sat_timems(solve_start));
02981 }
02982
02983
02984
02985
02986
02987
02988
02989
02990
02991 void
02992 solver_calc_duchanges(Solver *solv, DUChanges *mps, int nmps)
02993 {
02994 Map installedmap;
02995
02996 solver_create_state_maps(solv, &installedmap, 0);
02997 pool_calc_duchanges(solv->pool, &installedmap, mps, nmps);
02998 map_free(&installedmap);
02999 }
03000
03001
03002
03003
03004
03005
03006
03007 int
03008 solver_calc_installsizechange(Solver *solv)
03009 {
03010 Map installedmap;
03011 int change;
03012
03013 solver_create_state_maps(solv, &installedmap, 0);
03014 change = pool_calc_installsizechange(solv->pool, &installedmap);
03015 map_free(&installedmap);
03016 return change;
03017 }
03018
03019 void
03020 solver_trivial_installable(Solver *solv, Queue *pkgs, Queue *res)
03021 {
03022 Map installedmap;
03023 solver_create_state_maps(solv, &installedmap, 0);
03024 pool_trivial_installable_noobsoletesmap(solv->pool, &installedmap, pkgs, res, solv->noobsoletes.size ? &solv->noobsoletes : 0);
03025 map_free(&installedmap);
03026 }
03027