|
@@ -368,14 +368,14 @@ class Solver
|
|
|
}
|
|
|
|
|
|
if (!isset($this->watches[$rule->watch1])) {
|
|
|
- $this->watches[$rule->watch1] = 0;
|
|
|
+ $this->watches[$rule->watch1] = null;
|
|
|
}
|
|
|
|
|
|
$rule->next1 = $this->watches[$rule->watch1];
|
|
|
$this->watches[$rule->watch1] = $rule;
|
|
|
|
|
|
if (!isset($this->watches[$rule->watch2])) {
|
|
|
- $this->watches[$rule->watch2] = 0;
|
|
|
+ $this->watches[$rule->watch2] = null;
|
|
|
}
|
|
|
|
|
|
$rule->next2 = $this->watches[$rule->watch2];
|
|
@@ -413,7 +413,10 @@ class Solver
|
|
|
$literal = $literals[0];
|
|
|
|
|
|
if (!$this->decided($literal->getPackage())) {
|
|
|
-
|
|
|
+ $this->decisionQueue[] = $literal;
|
|
|
+ $this->decisionQueueWhy[] = $rule;
|
|
|
+ $this->addDecision($literal, 1);
|
|
|
+ continue;
|
|
|
}
|
|
|
|
|
|
if ($this->decisionsSatisfy($literal)) {
|
|
@@ -611,6 +614,12 @@ class Solver
|
|
|
protected $decisionMap = array();
|
|
|
protected $branches = array();
|
|
|
|
|
|
+ protected function literalFromId($id)
|
|
|
+ {
|
|
|
+ $package = $this->pool->packageById($id);
|
|
|
+ return new Literal($package, $id > 0);
|
|
|
+ }
|
|
|
+
|
|
|
protected function addDecision(Literal $l, $level)
|
|
|
{
|
|
|
if ($l->isWanted()) {
|
|
@@ -620,6 +629,16 @@ class Solver
|
|
|
}
|
|
|
}
|
|
|
|
|
|
+ protected function addDecisionId($literalId, $level)
|
|
|
+ {
|
|
|
+ $packageId = abs($literalId);
|
|
|
+ if ($literalId > 0) {
|
|
|
+ $this->decisionMap[$packageId] = $level;
|
|
|
+ } else {
|
|
|
+ $this->decisionMap[$packageId] = -$level;
|
|
|
+ }
|
|
|
+ }
|
|
|
+
|
|
|
protected function decisionsContain(Literal $l)
|
|
|
{
|
|
|
return (isset($this->decisionMap[$l->getPackageId()]) && (
|
|
@@ -628,6 +647,15 @@ class Solver
|
|
|
));
|
|
|
}
|
|
|
|
|
|
+ protected function decisionsContainId($literalId)
|
|
|
+ {
|
|
|
+ $packageId = abs($literalId);
|
|
|
+ return (isset($this->decisionMap[$packageId]) && (
|
|
|
+ $this->decisionMap[$packageId] > 0 && $literalId > 0 ||
|
|
|
+ $this->decisionMap[$packageId] < 0 && $literalId < 0
|
|
|
+ ));
|
|
|
+ }
|
|
|
+
|
|
|
protected function decisionsSatisfy(Literal $l)
|
|
|
{
|
|
|
return ($l->isWanted() && isset($this->decisionMap[$l->getPackageId()]) && $this->decisionMap[$l->getPackageId()] > 0) ||
|
|
@@ -642,6 +670,15 @@ class Solver
|
|
|
));
|
|
|
}
|
|
|
|
|
|
+ protected function decisionsConflictId($literalId)
|
|
|
+ {
|
|
|
+ $packageId = abs($literalId);
|
|
|
+ return (isset($this->decisionMap[$packageId]) && (
|
|
|
+ $this->decisionMap[$packageId] > 0 && !$literalId < 0 ||
|
|
|
+ $this->decisionMap[$packageId] < 0 && $literalId > 0
|
|
|
+ ));
|
|
|
+ }
|
|
|
+
|
|
|
protected function decided(PackageInterface $p)
|
|
|
{
|
|
|
return isset($this->decisionMap[$p->getId()]);
|
|
@@ -690,7 +727,7 @@ class Solver
|
|
|
|
|
|
$otherWatch = $rule->getOtherWatch($literal);
|
|
|
|
|
|
- if ($this->decisionsContain($otherWatch)) {
|
|
|
+ if ($this->decisionsContainId($otherWatch)) {
|
|
|
continue;
|
|
|
}
|
|
|
|
|
@@ -717,13 +754,13 @@ class Solver
|
|
|
}
|
|
|
|
|
|
// yay, we found a unit clause! try setting it to true
|
|
|
- if ($this->decisionsConflict($otherWatch)) {
|
|
|
+ if ($this->decisionsConflictId($otherWatch)) {
|
|
|
return $rule;
|
|
|
}
|
|
|
|
|
|
- $this->addDecision($otherWatch, $level);
|
|
|
+ $this->addDecisionId($otherWatch, $level);
|
|
|
|
|
|
- $this->decisionQueue[] = $otherWatch;
|
|
|
+ $this->decisionQueue[] = $this->literalFromId($otherWatch);
|
|
|
$this->decisionQueueWhy[] = $rule;
|
|
|
}
|
|
|
}
|
|
@@ -753,6 +790,11 @@ class Solver
|
|
|
return $this->setPropagateLearn($level, $literals[0], $disableRules, $rule);
|
|
|
}
|
|
|
|
|
|
+ private function analyzeUnsolvable($conflictRule, $disableRules)
|
|
|
+ {
|
|
|
+ return false;
|
|
|
+ }
|
|
|
+
|
|
|
private function runSat($disableRules = true, $installRecommended = false)
|
|
|
{
|
|
|
$this->propagateIndex = 0;
|
|
@@ -868,7 +910,8 @@ class Solver
|
|
|
}
|
|
|
|
|
|
// only process updates in first pass
|
|
|
- if (0 === $pass && !isset($this->updateMap[$literal->getPackageId()])) {
|
|
|
+ /** TODO: && or || ? **/
|
|
|
+ if (0 === $pass || !isset($this->updateMap[$literal->getPackageId()])) {
|
|
|
continue;
|
|
|
}
|
|
|
|
|
@@ -980,7 +1023,7 @@ class Solver
|
|
|
}
|
|
|
}
|
|
|
}
|
|
|
-$this->printRules();
|
|
|
+
|
|
|
//
|
|
|
// /*
|
|
|
// * decide
|
|
@@ -1074,761 +1117,4 @@ $this->printRules();
|
|
|
//
|
|
|
}
|
|
|
}
|
|
|
-
|
|
|
-// void
|
|
|
-// solver_run_sat(Solver *solv, int disablerules, int doweak)
|
|
|
-// {
|
|
|
-// Queue dq; /* local decisionqueue */
|
|
|
-// Queue dqs; /* local decisionqueue for supplements */
|
|
|
-// int systemlevel;
|
|
|
-// int level, olevel;
|
|
|
-// Rule *r;
|
|
|
-// int i, j, n;
|
|
|
-// Solvable *s;
|
|
|
-// Pool *pool = solv->pool;
|
|
|
-// Id p, *dp;
|
|
|
-// int minimizationsteps;
|
|
|
-// int installedpos = solv->installed ? solv->installed->start : 0;
|
|
|
-//
|
|
|
-// IF_POOLDEBUG (SAT_DEBUG_RULE_CREATION)
|
|
|
-// {
|
|
|
-// POOL_DEBUG (SAT_DEBUG_RULE_CREATION, "number of rules: %d\n", solv->nrules);
|
|
|
-// for (i = 1; i < solv->nrules; i++)
|
|
|
-// solver_printruleclass(solv, SAT_DEBUG_RULE_CREATION, solv->rules + i);
|
|
|
-// }
|
|
|
-//
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "initial decisions: %d\n", solv->decisionq.count);
|
|
|
-//
|
|
|
-// IF_POOLDEBUG (SAT_DEBUG_SCHUBI)
|
|
|
-// solver_printdecisions(solv);
|
|
|
-//
|
|
|
-// /* start SAT algorithm */
|
|
|
-// level = 1;
|
|
|
-// systemlevel = level + 1;
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "solving...\n");
|
|
|
-//
|
|
|
-// queue_init(&dq);
|
|
|
-// queue_init(&dqs);
|
|
|
-//
|
|
|
-// /*
|
|
|
-// * here's the main loop:
|
|
|
-// * 1) propagate new decisions (only needed once)
|
|
|
-// * 2) fulfill jobs
|
|
|
-// * 3) try to keep installed packages
|
|
|
-// * 4) fulfill all unresolved rules
|
|
|
-// * 5) install recommended packages
|
|
|
-// * 6) minimalize solution if we had choices
|
|
|
-// * if we encounter a problem, we rewind to a safe level and restart
|
|
|
-// * with step 1
|
|
|
-// */
|
|
|
-//
|
|
|
-// minimizationsteps = 0;
|
|
|
-// for (;;)
|
|
|
-// {
|
|
|
-// /*
|
|
|
-// * initial propagation of the assertions
|
|
|
-// */
|
|
|
-// if (level == 1)
|
|
|
-// {
|
|
|
-// POOL_DEBUG(SAT_DEBUG_PROPAGATE, "propagating (propagate_index: %d; size decisionq: %d)...\n", solv->propagate_index, solv->decisionq.count);
|
|
|
-// if ((r = propagate(solv, level)) != 0)
|
|
|
-// {
|
|
|
-// if (analyze_unsolvable(solv, r, disablerules))
|
|
|
-// continue;
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// }
|
|
|
-//
|
|
|
-// /*
|
|
|
-// * resolve jobs first
|
|
|
-// */
|
|
|
-// if (level < systemlevel)
|
|
|
-// {
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving job rules\n");
|
|
|
-// for (i = solv->jobrules, r = solv->rules + i; i < solv->jobrules_end; i++, r++)
|
|
|
-// {
|
|
|
-// Id l;
|
|
|
-// if (r->d < 0) /* ignore disabled rules */
|
|
|
-// continue;
|
|
|
-// queue_empty(&dq);
|
|
|
-// FOR_RULELITERALS(l, dp, r)
|
|
|
-// {
|
|
|
-// if (l < 0)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[-l] <= 0)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[l] > 0)
|
|
|
-// break;
|
|
|
-// if (solv->decisionmap[l] == 0)
|
|
|
-// queue_push(&dq, l);
|
|
|
-// }
|
|
|
-// }
|
|
|
-// if (l || !dq.count)
|
|
|
-// continue;
|
|
|
-// /* prune to installed if not updating */
|
|
|
-// if (dq.count > 1 && solv->installed && !solv->updatemap_all)
|
|
|
-// {
|
|
|
-// int j, k;
|
|
|
-// for (j = k = 0; j < dq.count; j++)
|
|
|
-// {
|
|
|
-// Solvable *s = pool->solvables + dq.elements[j];
|
|
|
-// if (s->repo == solv->installed)
|
|
|
-// {
|
|
|
-// dq.elements[k++] = dq.elements[j];
|
|
|
-// if (solv->updatemap.size && MAPTST(&solv->updatemap, dq.elements[j] - solv->installed->start))
|
|
|
-// {
|
|
|
-// k = 0; /* package wants to be updated, do not prune */
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// if (k)
|
|
|
-// dq.count = k;
|
|
|
-// }
|
|
|
-// olevel = level;
|
|
|
-// level = selectandinstall(solv, level, &dq, disablerules, i);
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// if (level <= olevel)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// systemlevel = level + 1;
|
|
|
-// if (i < solv->jobrules_end)
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-//
|
|
|
-//
|
|
|
-// /*
|
|
|
-// * installed packages
|
|
|
-// */
|
|
|
-// if (level < systemlevel && solv->installed && solv->installed->nsolvables && !solv->installed->disabled)
|
|
|
-// {
|
|
|
-// Repo *installed = solv->installed;
|
|
|
-// int pass;
|
|
|
-//
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "resolving installed packages\n");
|
|
|
-// /* we use two passes if we need to update packages
|
|
|
-// * to create a better user experience */
|
|
|
-// for (pass = solv->updatemap.size ? 0 : 1; pass < 2; pass++)
|
|
|
-// {
|
|
|
-// int passlevel = level;
|
|
|
-// /* start with installedpos, the position that gave us problems last time */
|
|
|
-// for (i = installedpos, n = installed->start; n < installed->end; i++, n++)
|
|
|
-// {
|
|
|
-// Rule *rr;
|
|
|
-// Id d;
|
|
|
-//
|
|
|
-// if (i == installed->end)
|
|
|
-// i = installed->start;
|
|
|
-// s = pool->solvables + i;
|
|
|
-// if (s->repo != installed)
|
|
|
-// continue;
|
|
|
-//
|
|
|
-// if (solv->decisionmap[i] > 0)
|
|
|
-// continue;
|
|
|
-// if (!pass && solv->updatemap.size && !MAPTST(&solv->updatemap, i - installed->start))
|
|
|
-// continue; /* updates first */
|
|
|
-// r = solv->rules + solv->updaterules + (i - installed->start);
|
|
|
-// rr = r;
|
|
|
-// if (!rr->p || rr->d < 0) /* disabled -> look at feature rule */
|
|
|
-// rr -= solv->installed->end - solv->installed->start;
|
|
|
-// if (!rr->p) /* identical to update rule? */
|
|
|
-// rr = r;
|
|
|
-// if (!rr->p)
|
|
|
-// continue; /* orpaned package */
|
|
|
-//
|
|
|
-// /* XXX: noupdate check is probably no longer needed, as all jobs should
|
|
|
-// * already be satisfied */
|
|
|
-// /* Actually we currently still need it because of erase jobs */
|
|
|
-// /* if noupdate is set we do not look at update candidates */
|
|
|
-// queue_empty(&dq);
|
|
|
-// 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))
|
|
|
-// {
|
|
|
-// if (solv->noobsoletes.size && solv->multiversionupdaters
|
|
|
-// && (d = solv->multiversionupdaters[i - installed->start]) != 0)
|
|
|
-// {
|
|
|
-// /* special multiversion handling, make sure best version is chosen */
|
|
|
-// queue_push(&dq, i);
|
|
|
-// while ((p = pool->whatprovidesdata[d++]) != 0)
|
|
|
-// if (solv->decisionmap[p] >= 0)
|
|
|
-// queue_push(&dq, p);
|
|
|
-// policy_filter_unwanted(solv, &dq, POLICY_MODE_CHOOSE);
|
|
|
-// p = dq.elements[0];
|
|
|
-// if (p != i && solv->decisionmap[p] == 0)
|
|
|
-// {
|
|
|
-// rr = solv->rules + solv->featurerules + (i - solv->installed->start);
|
|
|
-// if (!rr->p) /* update rule == feature rule? */
|
|
|
-// rr = rr - solv->featurerules + solv->updaterules;
|
|
|
-// dq.count = 1;
|
|
|
-// }
|
|
|
-// else
|
|
|
-// dq.count = 0;
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// /* update to best package */
|
|
|
-// FOR_RULELITERALS(p, dp, rr)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[p] > 0)
|
|
|
-// {
|
|
|
-// dq.count = 0; /* already fulfilled */
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// if (!solv->decisionmap[p])
|
|
|
-// queue_push(&dq, p);
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// /* install best version */
|
|
|
-// if (dq.count)
|
|
|
-// {
|
|
|
-// olevel = level;
|
|
|
-// level = selectandinstall(solv, level, &dq, disablerules, rr - solv->rules);
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// if (level <= olevel)
|
|
|
-// {
|
|
|
-// if (level == 1 || level < passlevel)
|
|
|
-// break; /* trouble */
|
|
|
-// if (level < olevel)
|
|
|
-// n = installed->start; /* redo all */
|
|
|
-// i--;
|
|
|
-// n--;
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-// }
|
|
|
-// /* if still undecided keep package */
|
|
|
-// if (solv->decisionmap[i] == 0)
|
|
|
-// {
|
|
|
-// olevel = level;
|
|
|
-// if (solv->cleandepsmap.size && MAPTST(&solv->cleandepsmap, i - installed->start))
|
|
|
-// {
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "cleandeps erasing %s\n", solvid2str(pool, i));
|
|
|
-// level = setpropagatelearn(solv, level, -i, disablerules, 0);
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "keeping %s\n", solvid2str(pool, i));
|
|
|
-// level = setpropagatelearn(solv, level, i, disablerules, r - solv->rules);
|
|
|
-// }
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// if (level <= olevel)
|
|
|
-// {
|
|
|
-// if (level == 1 || level < passlevel)
|
|
|
-// break; /* trouble */
|
|
|
-// if (level < olevel)
|
|
|
-// n = installed->start; /* redo all */
|
|
|
-// i--;
|
|
|
-// n--;
|
|
|
-// continue; /* retry with learnt rule */
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// if (n < installed->end)
|
|
|
-// {
|
|
|
-// installedpos = i; /* retry problem solvable next time */
|
|
|
-// break; /* ran into trouble */
|
|
|
-// }
|
|
|
-// installedpos = installed->start; /* reset installedpos */
|
|
|
-// }
|
|
|
-// systemlevel = level + 1;
|
|
|
-// if (pass < 2)
|
|
|
-// continue; /* had trouble, retry */
|
|
|
-// }
|
|
|
-//
|
|
|
-// if (level < systemlevel)
|
|
|
-// systemlevel = level;
|
|
|
-//
|
|
|
-// /*
|
|
|
-// * decide
|
|
|
-// */
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "deciding unresolved rules\n");
|
|
|
-// for (i = 1, n = 1; n < solv->nrules; i++, n++)
|
|
|
-// {
|
|
|
-// if (i == solv->nrules)
|
|
|
-// i = 1;
|
|
|
-// r = solv->rules + i;
|
|
|
-// if (r->d < 0) /* ignore disabled rules */
|
|
|
-// continue;
|
|
|
-// queue_empty(&dq);
|
|
|
-// if (r->d == 0)
|
|
|
-// {
|
|
|
-// /* binary or unary rule */
|
|
|
-// /* need two positive undecided literals */
|
|
|
-// if (r->p < 0 || r->w2 <= 0)
|
|
|
-// continue;
|
|
|
-// if (solv->decisionmap[r->p] || solv->decisionmap[r->w2])
|
|
|
-// continue;
|
|
|
-// queue_push(&dq, r->p);
|
|
|
-// queue_push(&dq, r->w2);
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// /* make sure that
|
|
|
-// * all negative literals are installed
|
|
|
-// * no positive literal is installed
|
|
|
-// * i.e. the rule is not fulfilled and we
|
|
|
-// * just need to decide on the positive literals
|
|
|
-// */
|
|
|
-// if (r->p < 0)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[-r->p] <= 0)
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[r->p] > 0)
|
|
|
-// continue;
|
|
|
-// if (solv->decisionmap[r->p] == 0)
|
|
|
-// queue_push(&dq, r->p);
|
|
|
-// }
|
|
|
-// dp = pool->whatprovidesdata + r->d;
|
|
|
-// while ((p = *dp++) != 0)
|
|
|
-// {
|
|
|
-// if (p < 0)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[-p] <= 0)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[p] > 0)
|
|
|
-// break;
|
|
|
-// if (solv->decisionmap[p] == 0)
|
|
|
-// queue_push(&dq, p);
|
|
|
-// }
|
|
|
-// }
|
|
|
-// if (p)
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-// IF_POOLDEBUG (SAT_DEBUG_PROPAGATE)
|
|
|
-// {
|
|
|
-// POOL_DEBUG(SAT_DEBUG_PROPAGATE, "unfulfilled ");
|
|
|
-// solver_printruleclass(solv, SAT_DEBUG_PROPAGATE, r);
|
|
|
-// }
|
|
|
-// /* dq.count < 2 cannot happen as this means that
|
|
|
-// * the rule is unit */
|
|
|
-// assert(dq.count > 1);
|
|
|
-//
|
|
|
-// olevel = level;
|
|
|
-// level = selectandinstall(solv, level, &dq, disablerules, r - solv->rules);
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// if (level < systemlevel || level == 1)
|
|
|
-// break; /* trouble */
|
|
|
-// /* something changed, so look at all rules again */
|
|
|
-// n = 0;
|
|
|
-// }
|
|
|
-//
|
|
|
-// if (n != solv->nrules) /* ran into trouble, restart */
|
|
|
-// continue;
|
|
|
-//
|
|
|
-// /* at this point we have a consistent system. now do the extras... */
|
|
|
-//
|
|
|
-// if (doweak)
|
|
|
-// {
|
|
|
-// int qcount;
|
|
|
-//
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended packages\n");
|
|
|
-// queue_empty(&dq); /* recommended packages */
|
|
|
-// queue_empty(&dqs); /* supplemented packages */
|
|
|
-// for (i = 1; i < pool->nsolvables; i++)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[i] < 0)
|
|
|
-// continue;
|
|
|
-// if (solv->decisionmap[i] > 0)
|
|
|
-// {
|
|
|
-// /* installed, check for recommends */
|
|
|
-// Id *recp, rec, pp, p;
|
|
|
-// s = pool->solvables + i;
|
|
|
-// if (solv->ignorealreadyrecommended && s->repo == solv->installed)
|
|
|
-// continue;
|
|
|
-// /* XXX need to special case AND ? */
|
|
|
-// if (s->recommends)
|
|
|
-// {
|
|
|
-// recp = s->repo->idarraydata + s->recommends;
|
|
|
-// while ((rec = *recp++) != 0)
|
|
|
-// {
|
|
|
-// qcount = dq.count;
|
|
|
-// FOR_PROVIDES(p, pp, rec)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[p] > 0)
|
|
|
-// {
|
|
|
-// dq.count = qcount;
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// else if (solv->decisionmap[p] == 0)
|
|
|
-// {
|
|
|
-// queue_pushunique(&dq, p);
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// }
|
|
|
-// else
|
|
|
-// {
|
|
|
-// s = pool->solvables + i;
|
|
|
-// if (!s->supplements)
|
|
|
-// continue;
|
|
|
-// if (!pool_installable(pool, s))
|
|
|
-// continue;
|
|
|
-// if (!solver_is_supplementing(solv, s))
|
|
|
-// continue;
|
|
|
-// queue_push(&dqs, i);
|
|
|
-// }
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* filter out all packages obsoleted by installed packages */
|
|
|
-// /* this is no longer needed if we have reverse obsoletes */
|
|
|
-// if ((dqs.count || dq.count) && solv->installed)
|
|
|
-// {
|
|
|
-// Map obsmap;
|
|
|
-// Id obs, *obsp, po, ppo;
|
|
|
-//
|
|
|
-// map_init(&obsmap, pool->nsolvables);
|
|
|
-// for (p = solv->installed->start; p < solv->installed->end; p++)
|
|
|
-// {
|
|
|
-// s = pool->solvables + p;
|
|
|
-// if (s->repo != solv->installed || !s->obsoletes)
|
|
|
-// continue;
|
|
|
-// if (solv->decisionmap[p] <= 0)
|
|
|
-// continue;
|
|
|
-// if (solv->noobsoletes.size && MAPTST(&solv->noobsoletes, p))
|
|
|
-// continue;
|
|
|
-// obsp = s->repo->idarraydata + s->obsoletes;
|
|
|
-// /* foreach obsoletes */
|
|
|
-// while ((obs = *obsp++) != 0)
|
|
|
-// FOR_PROVIDES(po, ppo, obs)
|
|
|
-// MAPSET(&obsmap, po);
|
|
|
-// }
|
|
|
-// for (i = j = 0; i < dqs.count; i++)
|
|
|
-// if (!MAPTST(&obsmap, dqs.elements[i]))
|
|
|
-// dqs.elements[j++] = dqs.elements[i];
|
|
|
-// dqs.count = j;
|
|
|
-// for (i = j = 0; i < dq.count; i++)
|
|
|
-// if (!MAPTST(&obsmap, dq.elements[i]))
|
|
|
-// dq.elements[j++] = dq.elements[i];
|
|
|
-// dq.count = j;
|
|
|
-// map_free(&obsmap);
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* filter out all already supplemented packages if requested */
|
|
|
-// if (solv->ignorealreadyrecommended && dqs.count)
|
|
|
-// {
|
|
|
-// /* turn off all new packages */
|
|
|
-// for (i = 0; i < solv->decisionq.count; i++)
|
|
|
-// {
|
|
|
-// p = solv->decisionq.elements[i];
|
|
|
-// if (p < 0)
|
|
|
-// continue;
|
|
|
-// s = pool->solvables + p;
|
|
|
-// if (s->repo && s->repo != solv->installed)
|
|
|
-// solv->decisionmap[p] = -solv->decisionmap[p];
|
|
|
-// }
|
|
|
-// /* filter out old supplements */
|
|
|
-// for (i = j = 0; i < dqs.count; i++)
|
|
|
-// {
|
|
|
-// p = dqs.elements[i];
|
|
|
-// s = pool->solvables + p;
|
|
|
-// if (!s->supplements)
|
|
|
-// continue;
|
|
|
-// if (!solver_is_supplementing(solv, s))
|
|
|
-// dqs.elements[j++] = p;
|
|
|
-// }
|
|
|
-// dqs.count = j;
|
|
|
-// /* undo turning off */
|
|
|
-// for (i = 0; i < solv->decisionq.count; i++)
|
|
|
-// {
|
|
|
-// p = solv->decisionq.elements[i];
|
|
|
-// if (p < 0)
|
|
|
-// continue;
|
|
|
-// s = pool->solvables + p;
|
|
|
-// if (s->repo && s->repo != solv->installed)
|
|
|
-// solv->decisionmap[p] = -solv->decisionmap[p];
|
|
|
-// }
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* multiversion doesn't mix well with supplements.
|
|
|
-// * filter supplemented packages where we already decided
|
|
|
-// * to install a different version (see bnc#501088) */
|
|
|
-// if (dqs.count && solv->noobsoletes.size)
|
|
|
-// {
|
|
|
-// for (i = j = 0; i < dqs.count; i++)
|
|
|
-// {
|
|
|
-// p = dqs.elements[i];
|
|
|
-// if (MAPTST(&solv->noobsoletes, p))
|
|
|
-// {
|
|
|
-// Id p2, pp2;
|
|
|
-// s = pool->solvables + p;
|
|
|
-// FOR_PROVIDES(p2, pp2, s->name)
|
|
|
-// if (solv->decisionmap[p2] > 0 && pool->solvables[p2].name == s->name)
|
|
|
-// break;
|
|
|
-// if (p2)
|
|
|
-// continue; /* ignore this package */
|
|
|
-// }
|
|
|
-// dqs.elements[j++] = p;
|
|
|
-// }
|
|
|
-// dqs.count = j;
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* make dq contain both recommended and supplemented pkgs */
|
|
|
-// if (dqs.count)
|
|
|
-// {
|
|
|
-// for (i = 0; i < dqs.count; i++)
|
|
|
-// queue_pushunique(&dq, dqs.elements[i]);
|
|
|
-// }
|
|
|
-//
|
|
|
-// if (dq.count)
|
|
|
-// {
|
|
|
-// Map dqmap;
|
|
|
-// int decisioncount = solv->decisionq.count;
|
|
|
-//
|
|
|
-// if (dq.count == 1)
|
|
|
-// {
|
|
|
-// /* simple case, just one package. no need to choose */
|
|
|
-// p = dq.elements[0];
|
|
|
-// if (dqs.count)
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
|
|
|
-// else
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
|
|
|
-// queue_push(&solv->recommendations, p);
|
|
|
-// level = setpropagatelearn(solv, level, p, 0, 0);
|
|
|
-// continue; /* back to main loop */
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* filter packages, this gives us the best versions */
|
|
|
-// policy_filter_unwanted(solv, &dq, POLICY_MODE_RECOMMEND);
|
|
|
-//
|
|
|
-// /* create map of result */
|
|
|
-// map_init(&dqmap, pool->nsolvables);
|
|
|
-// for (i = 0; i < dq.count; i++)
|
|
|
-// MAPSET(&dqmap, dq.elements[i]);
|
|
|
-//
|
|
|
-// /* install all supplemented packages */
|
|
|
-// for (i = 0; i < dqs.count; i++)
|
|
|
-// {
|
|
|
-// p = dqs.elements[i];
|
|
|
-// if (solv->decisionmap[p] || !MAPTST(&dqmap, p))
|
|
|
-// continue;
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "installing supplemented %s\n", solvid2str(pool, p));
|
|
|
-// queue_push(&solv->recommendations, p);
|
|
|
-// olevel = level;
|
|
|
-// level = setpropagatelearn(solv, level, p, 0, 0);
|
|
|
-// if (level <= olevel)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// if (i < dqs.count || solv->decisionq.count < decisioncount)
|
|
|
-// {
|
|
|
-// map_free(&dqmap);
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* install all recommended packages */
|
|
|
-// /* more work as we want to created branches if multiple
|
|
|
-// * choices are valid */
|
|
|
-// for (i = 0; i < decisioncount; i++)
|
|
|
-// {
|
|
|
-// Id rec, *recp, pp;
|
|
|
-// p = solv->decisionq.elements[i];
|
|
|
-// if (p < 0)
|
|
|
-// continue;
|
|
|
-// s = pool->solvables + p;
|
|
|
-// if (!s->repo || (solv->ignorealreadyrecommended && s->repo == solv->installed))
|
|
|
-// continue;
|
|
|
-// if (!s->recommends)
|
|
|
-// continue;
|
|
|
-// recp = s->repo->idarraydata + s->recommends;
|
|
|
-// while ((rec = *recp++) != 0)
|
|
|
-// {
|
|
|
-// queue_empty(&dq);
|
|
|
-// FOR_PROVIDES(p, pp, rec)
|
|
|
-// {
|
|
|
-// if (solv->decisionmap[p] > 0)
|
|
|
-// {
|
|
|
-// dq.count = 0;
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// else if (solv->decisionmap[p] == 0 && MAPTST(&dqmap, p))
|
|
|
-// queue_pushunique(&dq, p);
|
|
|
-// }
|
|
|
-// if (!dq.count)
|
|
|
-// continue;
|
|
|
-// if (dq.count > 1)
|
|
|
-// {
|
|
|
-// /* multiple candidates, open a branch */
|
|
|
-// for (i = 1; i < dq.count; i++)
|
|
|
-// queue_push(&solv->branches, dq.elements[i]);
|
|
|
-// queue_push(&solv->branches, -level);
|
|
|
-// }
|
|
|
-// p = dq.elements[0];
|
|
|
-// POOL_DEBUG(SAT_DEBUG_POLICY, "installing recommended %s\n", solvid2str(pool, p));
|
|
|
-// queue_push(&solv->recommendations, p);
|
|
|
-// olevel = level;
|
|
|
-// level = setpropagatelearn(solv, level, p, 0, 0);
|
|
|
-// if (level <= olevel || solv->decisionq.count < decisioncount)
|
|
|
-// break; /* we had to revert some decisions */
|
|
|
-// }
|
|
|
-// if (rec)
|
|
|
-// break; /* had a problem above, quit loop */
|
|
|
-// }
|
|
|
-// map_free(&dqmap);
|
|
|
-//
|
|
|
-// continue; /* back to main loop so that all deps are checked */
|
|
|
-// }
|
|
|
-// }
|
|
|
-//
|
|
|
-// if (solv->dupmap_all && solv->installed)
|
|
|
-// {
|
|
|
-// int installedone = 0;
|
|
|
-//
|
|
|
-// /* let's see if we can install some unsupported package */
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "deciding orphaned packages\n");
|
|
|
-// for (i = 0; i < solv->orphaned.count; i++)
|
|
|
-// {
|
|
|
-// p = solv->orphaned.elements[i];
|
|
|
-// if (solv->decisionmap[p])
|
|
|
-// continue; /* already decided */
|
|
|
-// olevel = level;
|
|
|
-// if (solv->droporphanedmap_all)
|
|
|
-// continue;
|
|
|
-// if (solv->droporphanedmap.size && MAPTST(&solv->droporphanedmap, p - solv->installed->start))
|
|
|
-// continue;
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "keeping orphaned %s\n", solvid2str(pool, p));
|
|
|
-// level = setpropagatelearn(solv, level, p, 0, 0);
|
|
|
-// installedone = 1;
|
|
|
-// if (level < olevel)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// if (installedone || i < solv->orphaned.count)
|
|
|
-// continue; /* back to main loop */
|
|
|
-// for (i = 0; i < solv->orphaned.count; i++)
|
|
|
-// {
|
|
|
-// p = solv->orphaned.elements[i];
|
|
|
-// if (solv->decisionmap[p])
|
|
|
-// continue; /* already decided */
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "removing orphaned %s\n", solvid2str(pool, p));
|
|
|
-// olevel = level;
|
|
|
-// level = setpropagatelearn(solv, level, -p, 0, 0);
|
|
|
-// if (level < olevel)
|
|
|
-// break;
|
|
|
-// }
|
|
|
-// if (i < solv->orphaned.count)
|
|
|
-// continue; /* back to main loop */
|
|
|
-// }
|
|
|
-//
|
|
|
-// if (solv->solution_callback)
|
|
|
-// {
|
|
|
-// solv->solution_callback(solv, solv->solution_callback_data);
|
|
|
-// if (solv->branches.count)
|
|
|
-// {
|
|
|
-// int i = solv->branches.count - 1;
|
|
|
-// int l = -solv->branches.elements[i];
|
|
|
-// Id why;
|
|
|
-//
|
|
|
-// for (; i > 0; i--)
|
|
|
-// if (solv->branches.elements[i - 1] < 0)
|
|
|
-// break;
|
|
|
-// p = solv->branches.elements[i];
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "branching with %s\n", solvid2str(pool, p));
|
|
|
-// queue_empty(&dq);
|
|
|
-// for (j = i + 1; j < solv->branches.count; j++)
|
|
|
-// queue_push(&dq, solv->branches.elements[j]);
|
|
|
-// solv->branches.count = i;
|
|
|
-// level = l;
|
|
|
-// revert(solv, level);
|
|
|
-// if (dq.count > 1)
|
|
|
-// for (j = 0; j < dq.count; j++)
|
|
|
-// queue_push(&solv->branches, dq.elements[j]);
|
|
|
-// olevel = level;
|
|
|
-// why = -solv->decisionq_why.elements[solv->decisionq_why.count];
|
|
|
-// assert(why >= 0);
|
|
|
-// level = setpropagatelearn(solv, level, p, disablerules, why);
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// continue;
|
|
|
-// }
|
|
|
-// /* all branches done, we're finally finished */
|
|
|
-// break;
|
|
|
-// }
|
|
|
-//
|
|
|
-// /* minimization step */
|
|
|
-// if (solv->branches.count)
|
|
|
-// {
|
|
|
-// int l = 0, lasti = -1, lastl = -1;
|
|
|
-// Id why;
|
|
|
-//
|
|
|
-// p = 0;
|
|
|
-// for (i = solv->branches.count - 1; i >= 0; i--)
|
|
|
-// {
|
|
|
-// p = solv->branches.elements[i];
|
|
|
-// if (p < 0)
|
|
|
-// l = -p;
|
|
|
-// else if (p > 0 && solv->decisionmap[p] > l + 1)
|
|
|
-// {
|
|
|
-// lasti = i;
|
|
|
-// lastl = l;
|
|
|
-// }
|
|
|
-// }
|
|
|
-// if (lasti >= 0)
|
|
|
-// {
|
|
|
-// /* kill old solvable so that we do not loop */
|
|
|
-// p = solv->branches.elements[lasti];
|
|
|
-// solv->branches.elements[lasti] = 0;
|
|
|
-// POOL_DEBUG(SAT_DEBUG_SOLVER, "minimizing %d -> %d with %s\n", solv->decisionmap[p], lastl, solvid2str(pool, p));
|
|
|
-// minimizationsteps++;
|
|
|
-//
|
|
|
-// level = lastl;
|
|
|
-// revert(solv, level);
|
|
|
-// why = -solv->decisionq_why.elements[solv->decisionq_why.count];
|
|
|
-// assert(why >= 0);
|
|
|
-// olevel = level;
|
|
|
-// level = setpropagatelearn(solv, level, p, disablerules, why);
|
|
|
-// if (level == 0)
|
|
|
-// {
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// return;
|
|
|
-// }
|
|
|
-// continue; /* back to main loop */
|
|
|
-// }
|
|
|
-// }
|
|
|
-// /* no minimization found, we're finally finished! */
|
|
|
-// break;
|
|
|
-// }
|
|
|
-//
|
|
|
-// POOL_DEBUG(SAT_DEBUG_STATS, "solver statistics: %d learned rules, %d unsolvable, %d minimization steps\n", solv->stats_learned, solv->stats_unsolvable, minimizationsteps);
|
|
|
-//
|
|
|
-// POOL_DEBUG(SAT_DEBUG_STATS, "done solving.\n\n");
|
|
|
-// queue_free(&dq);
|
|
|
-// queue_free(&dqs);
|
|
|
-// #if 0
|
|
|
-// solver_printdecisionq(solv, SAT_DEBUG_RESULT);
|
|
|
-// #endif
|
|
|
-// }
|
|
|
-}
|
|
|
+}
|