Turn assertions into solver bug exceptions with more info
parent
9c649a2652
commit
37d271271d
|
@ -764,20 +764,20 @@ class Solver
|
||||||
|
|
||||||
protected function addDecision(Literal $l, $level)
|
protected function addDecision(Literal $l, $level)
|
||||||
{
|
{
|
||||||
assert($this->decisionMap[$l->getPackageId()] == 0);
|
$this->addDecisionId($l->getId(), $level);
|
||||||
|
|
||||||
if ($l->isWanted()) {
|
|
||||||
$this->decisionMap[$l->getPackageId()] = $level;
|
|
||||||
} else {
|
|
||||||
$this->decisionMap[$l->getPackageId()] = -$level;
|
|
||||||
}
|
|
||||||
}
|
}
|
||||||
|
|
||||||
protected function addDecisionId($literalId, $level)
|
protected function addDecisionId($literalId, $level)
|
||||||
{
|
{
|
||||||
$packageId = abs($literalId);
|
$packageId = abs($literalId);
|
||||||
|
|
||||||
assert($this->decisionMap[$packageId] == 0);
|
$previousDecision = $this->decisionMap[$packageId];
|
||||||
|
if ($previousDecision != 0) {
|
||||||
|
$literal = $this->literalFromId($literalId);
|
||||||
|
throw new SolverBugException(
|
||||||
|
"Trying to decide $literal on level $level, even though ".$literal->getPackage()." was previously decided as ".(int) $previousDecision."."
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
if ($literalId > 0) {
|
if ($literalId > 0) {
|
||||||
$this->decisionMap[$packageId] = $level;
|
$this->decisionMap[$packageId] = $level;
|
||||||
|
@ -986,9 +986,6 @@ class Solver
|
||||||
*/
|
*/
|
||||||
private function setPropagateLearn($level, Literal $literal, $disableRules, Rule $rule)
|
private function setPropagateLearn($level, Literal $literal, $disableRules, Rule $rule)
|
||||||
{
|
{
|
||||||
assert($rule != null);
|
|
||||||
assert($literal != null);
|
|
||||||
|
|
||||||
$level++;
|
$level++;
|
||||||
|
|
||||||
$this->addDecision($literal, $level);
|
$this->addDecision($literal, $level);
|
||||||
|
@ -1010,14 +1007,20 @@ class Solver
|
||||||
// conflict
|
// conflict
|
||||||
list($learnLiteral, $newLevel, $newRule, $why) = $this->analyze($level, $rule);
|
list($learnLiteral, $newLevel, $newRule, $why) = $this->analyze($level, $rule);
|
||||||
|
|
||||||
assert($newLevel > 0);
|
if ($newLevel <= 0 || $newLevel >= $level) {
|
||||||
assert($newLevel < $level);
|
throw new SolverBugException(
|
||||||
|
"Trying to revert to invalid level ".(int) $newLevel." from level ".(int) $level."."
|
||||||
|
);
|
||||||
|
} else if (!$newRule) {
|
||||||
|
throw new SolverBugException(
|
||||||
|
"No rule was learned from analyzing $rule at level $level."
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
$level = $newLevel;
|
$level = $newLevel;
|
||||||
|
|
||||||
$this->revert($level);
|
$this->revert($level);
|
||||||
|
|
||||||
assert($newRule != null);
|
|
||||||
$this->addRule(RuleSet::TYPE_LEARNED, $newRule);
|
$this->addRule(RuleSet::TYPE_LEARNED, $newRule);
|
||||||
|
|
||||||
$this->learnedWhy[$newRule->getId()] = $why;
|
$this->learnedWhy[$newRule->getId()] = $why;
|
||||||
|
@ -1050,6 +1053,7 @@ class Solver
|
||||||
|
|
||||||
protected function analyze($level, $rule)
|
protected function analyze($level, $rule)
|
||||||
{
|
{
|
||||||
|
$analyzedRule = $rule;
|
||||||
$ruleLevel = 1;
|
$ruleLevel = 1;
|
||||||
$num = 0;
|
$num = 0;
|
||||||
$l1num = 0;
|
$l1num = 0;
|
||||||
|
@ -1100,7 +1104,12 @@ class Solver
|
||||||
}
|
}
|
||||||
|
|
||||||
while (true) {
|
while (true) {
|
||||||
assert($decisionId > 0);
|
if ($decisionId <= 0) {
|
||||||
|
throw new SolverBugException(
|
||||||
|
"Reached invalid decision id $decisionId while looking through $rule for a literal present in the analyzed rule $analyzedRule."
|
||||||
|
);
|
||||||
|
}
|
||||||
|
|
||||||
$decisionId--;
|
$decisionId--;
|
||||||
|
|
||||||
$literal = $this->decisionQueue[$decisionId];
|
$literal = $this->decisionQueue[$decisionId];
|
||||||
|
@ -1135,13 +1144,14 @@ class Solver
|
||||||
|
|
||||||
$why = count($this->learnedPool) - 1;
|
$why = count($this->learnedPool) - 1;
|
||||||
|
|
||||||
if (count($learnedLiterals) === 1 && $learnedLiterals[0] === null) {
|
if (!$learnedLiterals[0]) {
|
||||||
$newRule = new Rule(array(), Rule::RULE_LEARNED, $why);
|
throw new SolverBugException(
|
||||||
} else {
|
"Did not find a learnable literal in analyzed rule $analyzedRule."
|
||||||
assert($learnedLiterals[0] !== null);
|
);
|
||||||
$newRule = new Rule($learnedLiterals, Rule::RULE_LEARNED, $why);
|
|
||||||
}
|
}
|
||||||
|
|
||||||
|
$newRule = new Rule($learnedLiterals, Rule::RULE_LEARNED, $why);
|
||||||
|
|
||||||
return array($learnedLiterals[0], $ruleLevel, $newRule, $why);
|
return array($learnedLiterals[0], $ruleLevel, $newRule, $why);
|
||||||
}
|
}
|
||||||
|
|
||||||
|
|
|
@ -0,0 +1,28 @@
|
||||||
|
<?php
|
||||||
|
|
||||||
|
/*
|
||||||
|
* This file is part of Composer.
|
||||||
|
*
|
||||||
|
* (c) Nils Adermann <naderman@naderman.de>
|
||||||
|
* Jordi Boggiano <j.boggiano@seld.be>
|
||||||
|
*
|
||||||
|
* For the full copyright and license information, please view the LICENSE
|
||||||
|
* file that was distributed with this source code.
|
||||||
|
*/
|
||||||
|
|
||||||
|
namespace Composer\DependencyResolver;
|
||||||
|
|
||||||
|
/**
|
||||||
|
* @author Nils Adermann <naderman@naderman.de>
|
||||||
|
*/
|
||||||
|
class SolverBugException extends \RuntimeException
|
||||||
|
{
|
||||||
|
protected $problems;
|
||||||
|
|
||||||
|
public function __construct($message)
|
||||||
|
{
|
||||||
|
parent::__construct(
|
||||||
|
$message."\nThis exception was most likely caused by a bug in Composer.\n".
|
||||||
|
"Please report the command you ran, the exact error you received, and your composer.json on https://github.com/composer/composer/issues - thank you!\n");
|
||||||
|
}
|
||||||
|
}
|
Loading…
Reference in New Issue