function Solver::runSat

1 call to Solver::runSat()

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

File

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

Class

Solver

@author Nils Adermann <naderman@naderman.de>

Namespace

Composer\DependencyResolver

Code

private function runSat() : void {
    $this->propagateIndex = 0;
    
    /*
     * here's the main loop:
     * 1) propagate new decisions (only needed once)
     * 2) fulfill root requires/fixed packages
     * 3) fulfill all unresolved rules
     * 4) minimalize solution if we had choices
     * if we encounter a problem, we rewind to a safe level and restart
     * with step 1
     */
    $level = 1;
    $systemLevel = $level + 1;
    while (true) {
        if (1 === $level) {
            $conflictRule = $this->propagate($level);
            if (null !== $conflictRule) {
                $this->analyzeUnsolvable($conflictRule);
                return;
            }
        }
        // handle root require/fixed package rules
        if ($level < $systemLevel) {
            $iterator = $this->rules
                ->getIteratorFor(RuleSet::TYPE_REQUEST);
            foreach ($iterator as $rule) {
                if ($rule->isEnabled()) {
                    $decisionQueue = [];
                    $noneSatisfied = true;
                    foreach ($rule->getLiterals() as $literal) {
                        if ($this->decisions
                            ->satisfy($literal)) {
                            $noneSatisfied = false;
                            break;
                        }
                        if ($literal > 0 && $this->decisions
                            ->undecided($literal)) {
                            $decisionQueue[] = $literal;
                        }
                    }
                    if ($noneSatisfied && \count($decisionQueue) > 0) {
                        // if any of the options in the decision queue are fixed, only use those
                        $prunedQueue = [];
                        foreach ($decisionQueue as $literal) {
                            if (isset($this->fixedMap[abs($literal)])) {
                                $prunedQueue[] = $literal;
                            }
                        }
                        if (\count($prunedQueue) > 0) {
                            $decisionQueue = $prunedQueue;
                        }
                    }
                    if ($noneSatisfied && \count($decisionQueue) > 0) {
                        $oLevel = $level;
                        $level = $this->selectAndInstall($level, $decisionQueue, $rule);
                        if (0 === $level) {
                            return;
                        }
                        if ($level <= $oLevel) {
                            break;
                        }
                    }
                }
            }
            $systemLevel = $level + 1;
            // root requires/fixed packages left
            $iterator->next();
            if ($iterator->valid()) {
                continue;
            }
        }
        if ($level < $systemLevel) {
            $systemLevel = $level;
        }
        $rulesCount = \count($this->rules);
        $pass = 1;
        $this->io
            ->writeError('Looking at all rules.', true, IOInterface::DEBUG);
        for ($i = 0, $n = 0; $n < $rulesCount; $i++, $n++) {
            if ($i === $rulesCount) {
                if (1 === $pass) {
                    $this->io
                        ->writeError("Something's changed, looking at all rules again (pass #{$pass})", false, IOInterface::DEBUG);
                }
                else {
                    $this->io
                        ->overwriteError("Something's changed, looking at all rules again (pass #{$pass})", false, null, IOInterface::DEBUG);
                }
                $i = 0;
                $pass++;
            }
            $rule = $this->rules->ruleById[$i];
            $literals = $rule->getLiterals();
            if ($rule->isDisabled()) {
                continue;
            }
            $decisionQueue = [];
            // 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
            //
            foreach ($literals as $literal) {
                if ($literal <= 0) {
                    if (!$this->decisions
                        ->decidedInstall($literal)) {
                        continue 2;
                        // next rule
                    }
                }
                else {
                    if ($this->decisions
                        ->decidedInstall($literal)) {
                        continue 2;
                        // next rule
                    }
                    if ($this->decisions
                        ->undecided($literal)) {
                        $decisionQueue[] = $literal;
                    }
                }
            }
            // need to have at least 2 item to pick from
            if (\count($decisionQueue) < 2) {
                continue;
            }
            $level = $this->selectAndInstall($level, $decisionQueue, $rule);
            if (0 === $level) {
                return;
            }
            // something changed, so look at all rules again
            $rulesCount = \count($this->rules);
            $n = -1;
        }
        if ($level < $systemLevel) {
            continue;
        }
        // minimization step
        if (\count($this->branches) > 0) {
            $lastLiteral = null;
            $lastLevel = null;
            $lastBranchIndex = 0;
            $lastBranchOffset = 0;
            for ($i = \count($this->branches) - 1; $i >= 0; $i--) {
                [
                    $literals,
                    $l,
                ] = $this->branches[$i];
                foreach ($literals as $offset => $literal) {
                    if ($literal > 0 && $this->decisions
                        ->decisionLevel($literal) > $l + 1) {
                        $lastLiteral = $literal;
                        $lastBranchIndex = $i;
                        $lastBranchOffset = $offset;
                        $lastLevel = $l;
                    }
                }
            }
            if ($lastLiteral !== null) {
                assert($lastLevel !== null);
                unset($this->branches[$lastBranchIndex][self::BRANCH_LITERALS][$lastBranchOffset]);
                $level = $lastLevel;
                $this->revert($level);
                $why = $this->decisions
                    ->lastReason();
                $level = $this->setPropagateLearn($level, $lastLiteral, $why);
                if ($level === 0) {
                    return;
                }
                continue;
            }
        }
        break;
    }
}