function Solver::analyze

Return value

array{int, int, GenericRule, int}

1 call to Solver::analyze()

Solver::setPropagateLearn in vendor/composer/composer/src/Composer/DependencyResolver/Solver.php

setpropagatelearn

File

vendor/composer/composer/src/Composer/DependencyResolver/Solver.php, line 345

Class

Solver

@author Nils Adermann <naderman@naderman.de>

Namespace

Composer\DependencyResolver

Code

protected function analyze(int $level, Rule $rule) : array {
    $analyzedRule = $rule;
    $ruleLevel = 1;
    $num = 0;
    $l1num = 0;
    $seen = [];
    $learnedLiteral = null;
    $otherLearnedLiterals = [];
    $decisionId = \count($this->decisions);
    $this->learnedPool[] = [];
    while (true) {
        $this->learnedPool[\count($this->learnedPool) - 1][] = $rule;
        foreach ($rule->getLiterals() as $literal) {
            // multiconflictrule is really a bunch of rules in one, so some may not have finished propagating yet
            if ($rule instanceof MultiConflictRule && !$this->decisions
                ->decided($literal)) {
                continue;
            }
            // skip the one true literal
            if ($this->decisions
                ->satisfy($literal)) {
                continue;
            }
            if (isset($seen[abs($literal)])) {
                continue;
            }
            $seen[abs($literal)] = true;
            $l = $this->decisions
                ->decisionLevel($literal);
            if (1 === $l) {
                $l1num++;
            }
            elseif ($level === $l) {
                $num++;
            }
            else {
                // not level1 or conflict level, add to new rule
                $otherLearnedLiterals[] = $literal;
                if ($l > $ruleLevel) {
                    $ruleLevel = $l;
                }
            }
        }
        unset($literal);
        $l1retry = true;
        while ($l1retry) {
            $l1retry = false;
            if (0 === $num && 0 === --$l1num) {
                // all level 1 literals done
                break 2;
            }
            while (true) {
                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--;
                $decision = $this->decisions
                    ->atOffset($decisionId);
                $literal = $decision[Decisions::DECISION_LITERAL];
                if (isset($seen[abs($literal)])) {
                    break;
                }
            }
            unset($seen[abs($literal)]);
            if (0 !== $num && 0 === --$num) {
                if ($literal < 0) {
                    $this->testFlagLearnedPositiveLiteral = true;
                }
                $learnedLiteral = -$literal;
                if (0 === $l1num) {
                    break 2;
                }
                foreach ($otherLearnedLiterals as $otherLiteral) {
                    unset($seen[abs($otherLiteral)]);
                }
                // only level 1 marks left
                $l1num++;
                $l1retry = true;
            }
            else {
                $decision = $this->decisions
                    ->atOffset($decisionId);
                $rule = $decision[Decisions::DECISION_REASON];
                if ($rule instanceof MultiConflictRule) {
                    // there is only ever exactly one positive decision in a MultiConflictRule
                    foreach ($rule->getLiterals() as $ruleLiteral) {
                        if (!isset($seen[abs($ruleLiteral)]) && $this->decisions
                            ->satisfy(-$ruleLiteral)) {
                            $this->learnedPool[\count($this->learnedPool) - 1][] = $rule;
                            $l = $this->decisions
                                ->decisionLevel($ruleLiteral);
                            if (1 === $l) {
                                $l1num++;
                            }
                            elseif ($level === $l) {
                                $num++;
                            }
                            else {
                                // not level1 or conflict level, add to new rule
                                $otherLearnedLiterals[] = $ruleLiteral;
                                if ($l > $ruleLevel) {
                                    $ruleLevel = $l;
                                }
                            }
                            $seen[abs($ruleLiteral)] = true;
                            break;
                        }
                    }
                    $l1retry = true;
                }
            }
        }
        $decision = $this->decisions
            ->atOffset($decisionId);
        $rule = $decision[Decisions::DECISION_REASON];
    }
    $why = \count($this->learnedPool) - 1;
    if (null === $learnedLiteral) {
        throw new SolverBugException("Did not find a learnable literal in analyzed rule {$analyzedRule}.");
    }
    array_unshift($otherLearnedLiterals, $learnedLiteral);
    $newRule = new GenericRule($otherLearnedLiterals, Rule::RULE_LEARNED, $why);
    return [
        $learnedLiteral,
        $ruleLevel,
        $newRule,
        $why,
    ];
}