$watchChains
$watchChains :
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.
insert(\Composer\DependencyResolver\RuleWatchNode $node)
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.
| \Composer\DependencyResolver\RuleWatchNode | $node | The rule node to be inserted into the graph |
propagateLiteral(integer $decidedLiteral, integer $level, \Composer\DependencyResolver\Decisions $decisions) : \Composer\DependencyResolver\Rule|null
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.
| integer | $decidedLiteral | The literal which was decided (A in our example) |
| integer | $level | The level at which the decision took place and at which all resulting decisions should be made. |
| \Composer\DependencyResolver\Decisions | $decisions | Used to check previous decisions and to register decisions resulting from propagation |
If a conflict is found the conflicting rule is returned
moveWatch( $fromLiteral, $toLiteral, $node)
Moves a rule node from one watch chain to another
The rule node's watched literals are updated accordingly.
| $fromLiteral | mixed A literal the node used to watch |
|
| $toLiteral | mixed A literal the node should watch now |
|
| $node | mixed The rule node to be moved |