function Solver::setPropagateLearn

setpropagatelearn

add free decision (a positive literal) to decision queue increase level and propagate decision return if no conflict.

in conflict case, analyze conflict rule, add resulting rule to learnt rule set, make decision from learnt rule (always unit) and re-propagate.

returns the new solver level or 0 if unsolvable

2 calls to Solver::setPropagateLearn()

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

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

File

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

Class

Solver

@author Nils Adermann <naderman@naderman.de>

Namespace

Composer\DependencyResolver

Code

private function setPropagateLearn(int $level, int $literal, Rule $rule) : int {
    $level++;
    $this->decisions
        ->decide($literal, $level, $rule);
    while (true) {
        $rule = $this->propagate($level);
        if (null === $rule) {
            break;
        }
        if ($level === 1) {
            $this->analyzeUnsolvable($rule);
            return 0;
        }
        // conflict
        [
            $learnLiteral,
            $newLevel,
            $newRule,
            $why,
        ] = $this->analyze($level, $rule);
        if ($newLevel <= 0 || $newLevel >= $level) {
            throw new SolverBugException("Trying to revert to invalid level " . $newLevel . " from level " . $level . ".");
        }
        $level = $newLevel;
        $this->revert($level);
        $this->rules
            ->add($newRule, RuleSet::TYPE_LEARNED);
        $this->learnedWhy[spl_object_hash($newRule)] = $why;
        $ruleNode = new RuleWatchNode($newRule);
        $ruleNode->watch2OnHighest($this->decisions);
        $this->watchGraph
            ->insert($ruleNode);
        $this->decisions
            ->decide($learnLiteral, $level, $newRule);
    }
    return $level;
}