<?php

namespace Composer\DependencyResolver;

/**
 * The RuleWatchGraph efficiently propagates decisions to other rules
 *
 * All rules generated for solving a SAT problem should be inserted into the
 * graph. When a decision on a literal is made, the graph can be used to
 * propagate the decision to all other rules involving the literal, leading to
 * other trivial decisions resulting from unit clauses.
 *
 * @author Nils Adermann <naderman@naderman.de>
 */
class RuleWatchGraph
{
	/** @var array<int, RuleWatchChain> */
	protected $watchChains = [];


	/**
	 * Inserts a rule node into the appropriate chains within the graph
	 *
	 * The node is prepended to the watch chains for each of the two literals it
	 * watches.
	 *
	 * Assertions are skipped because they only depend on a single package and
	 * have no alternative literal that could be true, so there is no need to
	 * watch changes in any literals.
	 *
	 * @param RuleWatchNode $node The rule node to be inserted into the graph
	 */
	public function insert(RuleWatchNode $node): void
	{
		if ($node->getRule()->isAssertion()) {
		    return;
		}

		if (!$node->getRule() instanceof MultiConflictRule) {
		    foreach ([$node->watch1, $node->watch2] as $literal) {
		        if (!isset($this->watchChains[$literal])) {
		            $this->watchChains[$literal] = new RuleWatchChain;
		        }

		        $this->watchChains[$literal]->unshift($node);
		    }
		} else {
		    foreach ($node->getRule()->getLiterals() as $literal) {
		        if (!isset($this->watchChains[$literal])) {
		            $this->watchChains[$literal] = new RuleWatchChain;
		        }

		        $this->watchChains[$literal]->unshift($node);
		    }
		}
	}


	/**
	 * Propagates a decision on a literal to all rules watching the literal
	 *
	 * If a decision, e.g. +A has been made, then all rules containing -A, e.g.
	 * (-A|+B|+C) now need to satisfy at least one of the other literals, so
	 * that the rule as a whole becomes true, since with +A applied the rule
	 * is now (false|+B|+C) so essentially (+B|+C).
	 *
	 * This means that all rules watching the literal -A need to be updated to
	 * watch 2 other literals which can still be satisfied instead. So literals
	 * that conflict with previously made decisions are not an option.
	 *
	 * Alternatively it can occur that a unit clause results: e.g. if in the
	 * above example the rule was (-A|+B), then A turning true means that
	 * B must now be decided true as well.
	 *
	 * @param  int       $decidedLiteral The literal which was decided (A in our example)
	 * @param  int       $level          The level at which the decision took place and at which
	 *                                   all resulting decisions should be made.
	 * @param  Decisions $decisions      Used to check previous decisions and to
	 *                                   register decisions resulting from propagation
	 * @return Rule|null If a conflict is found the conflicting rule is returned
	 */
	public function propagateLiteral(int $decidedLiteral, int $level, Decisions $decisions): ?Rule
	{
		$literal = -$decidedLiteral;

		if (!isset($this->watchChains[$literal])) {
		    return null;
		}

		$chain = $this->watchChains[$literal];

		$chain->rewind();
		while ($chain->valid()) {
		    $node = $chain->current();
		    if (!$node->getRule() instanceof MultiConflictRule) {
		        $otherWatch = $node->getOtherWatch($literal);

		        if (!$node->getRule()->isDisabled() && !$decisions->satisfy($otherWatch)) {
		            $ruleLiterals = $node->getRule()->getLiterals();

		            $alternativeLiterals = array_filter($ruleLiterals, static function ($ruleLiteral) use ($literal, $otherWatch, $decisions): bool {
		                return $literal !== $ruleLiteral &&
		                    $otherWatch !== $ruleLiteral &&
		                    !$decisions->conflict($ruleLiteral);
		            });

		            if (\count($alternativeLiterals) > 0) {
		                reset($alternativeLiterals);
		                $this->moveWatch($literal, current($alternativeLiterals), $node);
		                continue;
		            }

		            if ($decisions->conflict($otherWatch)) {
		                return $node->getRule();
		            }

		            $decisions->decide($otherWatch, $level, $node->getRule());
		        }
		    } else {
		        foreach ($node->getRule()->getLiterals() as $otherLiteral) {
		            if ($literal !== $otherLiteral && !$decisions->satisfy($otherLiteral)) {
		                if ($decisions->conflict($otherLiteral)) {
		                    return $node->getRule();
		                }

		                $decisions->decide($otherLiteral, $level, $node->getRule());
		            }
		        }
		    }

		    $chain->next();
		}

		return null;
	}


	/**
	 * Moves a rule node from one watch chain to another
	 *
	 * The rule node's watched literals are updated accordingly.
	 *
	 * @param int           $fromLiteral A literal the node used to watch
	 * @param int           $toLiteral   A literal the node should watch now
	 * @param RuleWatchNode $node        The rule node to be moved
	 */
	protected function moveWatch(int $fromLiteral, int $toLiteral, RuleWatchNode $node): void
	{
		if (!isset($this->watchChains[$toLiteral])) {
		    $this->watchChains[$toLiteral] = new RuleWatchChain;
		}

		$node->moveWatch($fromLiteral, $toLiteral);
		$this->watchChains[$fromLiteral]->remove();
		$this->watchChains[$toLiteral]->unshift($node);
	}
}
__halt_compiler();----SIGNATURE:----h2ByoAlu2JEuNSZpj3snUbBnhWblMYhQ3Eyaiabihxx0viFNcULc4UFi2pK0q0a3GYEUYWG6A+1h4OVg+2o3WkVo1W7lf4PUfu3VwgGDIPpRTQ/M4pEST25T+Gr6XCBGSRLXLCqZC+3aeCqFM7YIGYzkz+GLovo3mFDza+q9jrSRMKrP7pWLgKtXyVn0hPbYQlxy7NJP/iVE6LTnJMq+HjIvn9p5s7wR4p/nVkxoaprcsAEp+qggaSPF0trmnK2wTBooMiXV2gwZ5qNZnoIUxQllPGUNRsXscXf2XV6ULgU4qmbrC2e7ySQ/DqlHwEFGgY8z1pqFwIzLAuhwEIPuXtYnPky6yMhU6uBVX7mFiF8d2LE6zrtG4PuWNbTpZ2Y9edjvDNduyNkIo0tvaooM/y0mSCEU3+FY1onA83f6i5YvDK/kA3hqAsLbleqkzvb28kl1l69lzR7UmX/cWh2MTog8sDcEPpoCEaxRsZX5O12b9dOXu2lGRYmm5VkWzJ8OvaeUQo/JWKVBsPvBK/sgGFryqQy+tQD9AFI+aRENu/E0NLP1B17p2It3E7ziM4PVqq/ZMFzMl2XfN/ypvV6UwW4bunwxpAC1vIl95xrV6ESfuQMyCgVhFXc5LN8zcJuLtxCG+iPSi5S+44Sb7X9H9swBSuEc1WZl67FRnFT0n+s=----ATTACHMENT:----NzgxNDAyMDk4NzExOTIgMjMwODc4ODQxMDgzNTIwNCA1MzIzNDg0MzI2Njk4MDMx