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