function Solver::analyzeUnsolvable

2 calls to Solver::analyzeUnsolvable()

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 519

Class

Solver

@author Nils Adermann <naderman@naderman.de>

Namespace

Composer\DependencyResolver

Code

private function analyzeUnsolvable(Rule $conflictRule) : void {
    $problem = new Problem();
    $problem->addRule($conflictRule);
    $ruleSeen = [];
    $this->analyzeUnsolvableRule($problem, $conflictRule, $ruleSeen);
    $this->problems[] = $problem;
    $seen = [];
    $literals = $conflictRule->getLiterals();
    foreach ($literals as $literal) {
        // skip the one true literal
        if ($this->decisions
            ->satisfy($literal)) {
            continue;
        }
        $seen[abs($literal)] = true;
    }
    foreach ($this->decisions as $decision) {
        $decisionLiteral = $decision[Decisions::DECISION_LITERAL];
        // skip literals that are not in this rule
        if (!isset($seen[abs($decisionLiteral)])) {
            continue;
        }
        $why = $decision[Decisions::DECISION_REASON];
        $problem->addRule($why);
        $this->analyzeUnsolvableRule($problem, $why, $ruleSeen);
        $literals = $why->getLiterals();
        foreach ($literals as $literal) {
            // skip the one true literal
            if ($this->decisions
                ->satisfy($literal)) {
                continue;
            }
            $seen[abs($literal)] = true;
        }
    }
}