Add decision making (most up-to-date strategy) + comments

Author: ysbaddaden

src/commands/lock.cr

@@ -8,7 +8,16 @@ module Shards
         resolver : Resolver,
         versions : Hash(String, Spec)
 
+      private def sat
+        @sat ||= SAT.new
+      end
+
+      private def pkgs
+        @pkgs ||= {} of String => Pkg
+      end
+
       def run
+        # 1. build dependency graph:
         Shards.logger.info { "Collecting dependencies..." }
 
         spent = Time.measure do
@@ -21,7 +30,8 @@ module Shards
           "Collected #{pkgs.size} dependencies (total: #{total} specs, duration: #{spent})"
         end
 
-        Shards.logger.info { "Building SAT clauses..." }
+        # 2. translate dependency graph as CNF clauses (conjunctive normal form):
+        Shards.logger.debug { "Building clauses..." }
 
         spent = Time.measure do
           # the package to install dependencies for:
@@ -39,7 +49,7 @@ module Shards
             end
           end
 
-          # version conflicts (we want only 1 version per package):
+          # version conflicts (we want at most 1 version for each package):
           pkgs.each do |name, pkg|
             pkg.versions.keys.each_combination(2) do |(a, b)|
               sat.add_clause ["~#{name}:#{a}", "~#{name}:#{b}"]
@@ -52,33 +62,71 @@ module Shards
         #   STDERR.puts sat.clause_to_s(clause)
         # end
 
+        # 3. distances (for decision making)
+        # compute distance for each version from a reference version:
+        distances = {} of String => Int32
+        distances[spec.name] = 0
+
+        # TODO: should be the distance from a given version or a range of
+        #       versions, not necessarily from the latest one (e.g. for
+        #       conservative updates).
+        # TODO: consider adding some weight (e.g. to update some dependencies).
+        pkgs.each do |name, pkg|
+          pkg.versions.keys.each_with_index do |version, index|
+            distances["#{name}:#{version}"] = index
+          end
+        end
+
+        # 4. solving + decision
+        # FIXME: some nested dependencies seem to be selected despite being extraneous (missing clauses?)
         Shards.logger.info { "Solving dependencies..." }
         count = 0
 
+        solution = nil
+        solution_distance = Int32::MAX
+
         spent = Time.measure do
-          sat.solve do |solution|
-            # p solution
+          sat.solve do |proposal|
             count += 1
+
+            # 4 (bis). decision making
+            # decide the proposal quality (most up-to-date):
+            distance = proposal.reduce(0) { |a, e| a + distances[e] }
+
+            # better solution?
+            if distance < solution_distance
+              solution = proposal.dup
+              solution_distance = distance
+              Shards.logger.debug { "Select proposal (distance=#{solution_distance}): #{solution.sort.join(' ')}" }
+
+            # fewer dependencies?
+            elsif distance == solution_distance && proposal.size < solution.not_nil!.size
+              solution = proposal.dup
+              solution_distance = distance
+              Shards.logger.debug { "Select smaller proposal (distance=#{solution_distance}): #{solution.sort.join(' ')}" }
+            end
           end
         end
 
-        if count == 0
-          Shards.logger.error { "Failed to find a solution (duration: #{spent})" }
+        # 5.
+        if solution
+          Shards.logger.info { "Analyzed #{count} solutions (duration: #{spent}" }
+          Shards.logger.info { "Found solution:" }
+          solution
+            .compact_map { |variable| variable.split(':') if variable.index(':') }
+            .sort { |a, b| a[0] <=> b[0] }
+            .each { |p| puts "#{p[0]}: #{p[1]}" }
         else
-          Shards.logger.info { "Found #{count} solutions (duration: #{spent}" }
+          Shards.logger.error { "Failed to find a solution (duration: #{spent})" }
         end
       end
 
-      private def sat
-        @sat ||= SAT.new
-      end
-
       private def add_dependencies(negation, dependencies)
         dependencies.each do |d|
           versions = Versions.resolve(pkgs[d.name].versions.keys, {d.version})
 
           # FIXME: looks like we couldn't resolve a constraint here; maybe it's
-          # related to a git refs, or something?
+          #        related to a git refs?
           next if versions.empty?
 
           clause = [negation]
@@ -87,18 +135,18 @@ module Shards
         end
       end
 
-      private def pkgs
-        @pkgs ||= {} of String => Pkg
-      end
-
+      # TODO: try and limit versions to what's actually reachable, in order to
+      #       reduce the dependency graph, which will reduce the number of
+      #       solutions, thus reduce the overall solving time.
       private def dig(dependencies, resolve = false)
         dependencies.each do |dependency|
           next if pkgs.has_key?(dependency.name)
 
           resolver = Shards.find_resolver(dependency)
           versions = resolver.available_versions
 
-          # resolve main spec constraints (avoids useless branches in the dependency graph):
+          # resolve main spec constraints (avoids impossible branches in the
+          # dependency graph):
           versions = Versions.resolve(versions, {dependency.version}) if resolve
 
           pkg = Pkg.new(resolver, resolver.specs(Versions.sort(versions)))

src/sat.cr

@@ -53,16 +53,16 @@ module Shards
       @clauses << clause
     end
 
-    protected def literal_to_s(literal : Literal) : String
+    private def literal_to_s(literal : Literal) : String
       String.build { |str| literal_to_s(str, literal) }
     end
 
-    protected def literal_to_s(io : IO, literal : Literal) : Nil
+    private def literal_to_s(io : IO, literal : Literal) : Nil
       io << '~' unless literal & 1 == 0
       io << @variables[literal >> 1]
     end
 
-    protected def clause_to_s(clause : Clause) : String
+    private def clause_to_s(clause : Clause) : String
       String.build do |str|
         clause.each_with_index do |literal, index|
           str << ' ' unless index == 0
@@ -71,7 +71,7 @@ module Shards
       end
     end
 
-    protected def assignment_to_s(assignment, brief = false)
+    private def assignment_to_s(assignment, brief = false)
       String.build do |str|
         assignment.each_with_index do |a, index|
           if a.selected?
@@ -83,33 +83,47 @@ module Shards
       end
     end
 
-    protected def to_variables(assignment, brief = false)
-      assignment.each_with_index.compact_map do |(a, index)|
+    private def to_variables(result, assignment, brief = false)
+      result.clear
+
+      assignment.each_with_index do |a, index|
         if a.selected?
-          @variables[index]
+          result << @variables[index]
         elsif !brief && a.not_selected?
-          "~#{@variables[index]}"
+          result << "~#{@variables[index]}"
         end
-      end.to_a
+      end
     end
 
-    # Solves SAT and yields solutions.
+    # Solves SAT and yields proposed solution.
+    #
+    # Reuses the yielded array for performance reasons (avoids many
+    # allocations); you must duplicate the array if you want to memorize a
+    # solution. For example:
+    #
+    # ```
+    # solution = nil
+    # ast.solve { |proposal| solution = proposal.dup }
+    # ```
     def solve(brief = true, verbose = false) : Nil
       watchlist = setup_watchlist
       assignment = Array(Assignment).new(@variables.size) { Assignment::UNDEFINED }
 
+      result = [] of String
+
       solve(watchlist, assignment, 0, verbose) do |solution|
-        yield to_variables(solution, brief)
+        to_variables(result, solution, brief)
+        yield result
       end
     end
 
     # Iteratively solve SAT by assigning to variables d, d+1, ..., n-1.
     # Assumes variables 0, ..., d-1 are assigned so far.
     private def solve(watchlist, assignment, d, verbose)
-      # The state list wil keep track of what values for which variables
-      # we have tried so far. A value of 0 means nothing has been tried yet,
-      # a value of 1 means False has been tried but not True, 2 means True
-      # but not False, and 3 means both have been tried.
+      # The state list keeps track of what values for which variables we have
+      # tried so far. A value of 0 means nothing has been tried yet, a value of
+      # 1 means False has been tried but not True, 2 means True but not False,
+      # and 3 means both have been tried.
       n = @variables.size
       state = Array(Literal).new(n) { Literal.new(0) }
 
@@ -120,7 +134,7 @@ module Shards
           next
         end
 
-        # Let's try assigning a value to v. Here would be the place to insert
+        # Let's try assigning a value to 'v'. Here would be the place to insert
         # heuristics of which value to try first.
         tried_something = false
 
@@ -130,7 +144,7 @@ module Shards
 
             tried_something = true
 
-            # set the bit indicating a has been tried for d:
+            # set the bit indicating 'a' has been tried for 'd':
             state[d] |= 1 << a
             assignment[d] = Assignment.from_value(a)
 
@@ -174,8 +188,8 @@ module Shards
 
     # Updates the watch list after literal 'false_literal' was just assigned
     # `false`, by making any clause watching false_literal watch something else.
-    # Returns False it is impossible to do so, meaning a clause is contradicted by
-    # the current assignment.
+    # Returns `false` if it's impossible to do so, meaning a clause is
+    # contradicted by the current assignment.
     private def update_watchlist(watchlist, false_literal, assignment, verbose)
       while clause = watchlist[false_literal].first?
         found_alternative = false