|
|
|
@ -1748,12 +1748,14 @@ class Solver
|
|
|
|
|
|
|
|
|
|
while (true) {
|
|
|
|
|
|
|
|
|
|
$conflictRule = $this->propagate($level);
|
|
|
|
|
if ($conflictRule !== null) {
|
|
|
|
|
if ($this->analyzeUnsolvable($conflictRule, $disableRules)) {
|
|
|
|
|
continue;
|
|
|
|
|
} else {
|
|
|
|
|
return;
|
|
|
|
|
if (1 === $level) {
|
|
|
|
|
$conflictRule = $this->propagate($level);
|
|
|
|
|
if ($conflictRule !== null) {
|
|
|
|
|
if ($this->analyzeUnsolvable($conflictRule, $disableRules)) {
|
|
|
|
|
continue;
|
|
|
|
|
} else {
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
@ -1989,7 +1991,11 @@ class Solver
|
|
|
|
|
return;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
if ($level < $systemLevel || $level == 1) {
|
|
|
|
|
// open suse sat-solver uses this, but why is $level == 1 trouble?
|
|
|
|
|
// SYSTEMSOLVABLE related? we don't have that, so should work
|
|
|
|
|
//if ($level < $systemLevel || $level == 1) {
|
|
|
|
|
|
|
|
|
|
if ($level < $systemLevel) {
|
|
|
|
|
break; // trouble
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
@ -1997,9 +2003,6 @@ class Solver
|
|
|
|
|
$n = -1;
|
|
|
|
|
}
|
|
|
|
|
|
|
|
|
|
// $this->printDecisionMap();
|
|
|
|
|
// $this->printDecisionQueue();
|
|
|
|
|
|
|
|
|
|
// minimization step
|
|
|
|
|
if (count($this->branches)) {
|
|
|
|
|
|
|
|
|
|