function Solver::propagate

Makes a decision and propagates it to all rules.

Evaluates each term affected by the decision (linked through watches) If we find unit rules we make new decisions based on them

Return value

Rule|null A rule on conflict, otherwise null.

2 calls to Solver::propagate()

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

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

setpropagatelearn

File

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

Class

Solver

@author Nils Adermann <naderman@naderman.de>

Namespace

Composer\DependencyResolver

Code

protected function propagate(int $level) : ?Rule {
    while ($this->decisions
        ->validOffset($this->propagateIndex)) {
        $decision = $this->decisions
            ->atOffset($this->propagateIndex);
        $conflict = $this->watchGraph
            ->propagateLiteral($decision[Decisions::DECISION_LITERAL], $level, $this->decisions);
        $this->propagateIndex++;
        if ($conflict !== null) {
            return $conflict;
        }
    }
    return null;
}