Document the RuleWatchGraph

src/Composer/DependencyResolver/RuleWatchGraph.php

@@ -13,6 +13,13 @@
 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 rule, leading to
+ * other trivial decisions resulting from unit clauses.
+ *
  * @author Nils Adermann <naderman@naderman.de>
  */
 class RuleWatchGraph
@@ -20,8 +27,16 @@ class RuleWatchGraph
     protected $watchChains = array();
 
     /**
-     * Alters watch chains for a rule.
+     * 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 chnages in any literals.
+     *
+     * @param RuleWatchNode $node The rule node to be inserted into the graph
      */
     public function insert(RuleWatchNode $node)
     {
@@ -38,13 +53,41 @@ class RuleWatchGraph
         }
     }
 
-    public function contains($literal)
+    /**
+     * 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 essentialy (+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 Callable $decisionsSatisfyCallback A callback which checks if a
+     *     literal has already been positively decided and the rule is thus
+     *     already true and can be skipped.
+     * @param Callable $conflictCallback A callback which checks if a literal
+     *     would conflict with previously made decisions on the same package
+     * @param Callable $decideCallback A callback which is responsible for
+     *     registering decided literals resulting from unit clauses
+     * @return Rule|null If a conflict is found the conflicting rule is returned
+     */
+    public function propagateLiteral($decidedLiteral, $level, $decisionsSatisfyCallback, $conflictCallback, $decideCallback)
     {
-        return isset($this->watchChains[$literal]);
-    }
+        // we invert the decided literal here, example:
+        // A was decided => (-A|B) now requires B to be true, so we look for
+        // rules which are fulfilled by -A, rather than A.
+        $literal = -$decidedLiteral;
 
-    public function propagateLiteral($literal, $level, $skipCallback, $conflictCallback, $decideCallback)
-    {
         if (!isset($this->watchChains[$literal])) {
             return null;
         }
@@ -56,7 +99,7 @@ class RuleWatchGraph
             $node = $chain->current();
             $otherWatch = $node->getOtherWatch($literal);
 
-            if (!$node->getRule()->isDisabled() && !call_user_func($skipCallback, $otherWatch)) {
+            if (!$node->getRule()->isDisabled() && !call_user_func($decisionsSatisfyCallback, $otherWatch)) {
                 $ruleLiterals = $node->getRule()->getLiterals();
 
                 $alternativeLiterals = array_filter($ruleLiterals, function ($ruleLiteral) use ($literal, $otherWatch, $conflictCallback) {
@@ -84,6 +127,15 @@ class RuleWatchGraph
         return null;
     }
 
+    /**
+     * Moves a rule node from one watch chain to another
+     *
+     * The rule node's watched literals are updated accordingly.
+     *
+     * @param $fromLiteral A literal the node used to watch
+     * @param $toLiteral A literal the node should watch now
+     * @param $node The rule node to be moved
+     */
     protected function moveWatch($fromLiteral, $toLiteral, $node)
     {
         if (!isset($this->watchChains[$toLiteral])) {

src/Composer/DependencyResolver/Solver.php

@@ -289,16 +289,8 @@ class Solver
     protected function propagate($level)
     {
         while ($this->propagateIndex < count($this->decisionQueue)) {
-            // we invert the decided literal here, example:
-            // A was decided => (-A|B) now requires B to be true, so we look for
-            // rules which are fulfilled by -A, rather than A.
-
-            $literal = -$this->decisionQueue[$this->propagateIndex];
-
-            $this->propagateIndex++;
-
             $conflict = $this->watchGraph->propagateLiteral(
-                $literal,
+                $this->decisionQueue[$this->propagateIndex++],
                 $level,
                 array($this, 'decisionsContain'),
                 array($this, 'decisionsConflict'),