From 3bac7c4424b63b8584f344e029a3340da4b78633 Mon Sep 17 00:00:00 2001
From: Natalie Weizenbaum <nweiz@google.com>
Date: Tue, 10 May 2016 10:47:43 -0700
Subject: [PATCH] Draft of Deducer.add(Required)

---
 lib/src/solver/backtracking_solver.dart |  74 +++++-----
 lib/src/solver/deducer.dart             | 176 ++++++++++++++++++++++++
 lib/src/solver/deduction_builder.dart   |  61 ++++++++
 lib/src/solver/fact.dart                |  68 +++++++++
 solve.dart                              | 147 ++++++++++++++++++++
 5 files changed, 491 insertions(+), 35 deletions(-)
 create mode 100644 lib/src/solver/deducer.dart
 create mode 100644 lib/src/solver/deduction_builder.dart
 create mode 100644 lib/src/solver/fact.dart
 create mode 100644 solve.dart

diff --git a/lib/src/solver/backtracking_solver.dart b/lib/src/solver/backtracking_solver.dart
index b051a0fc..adeb53b5 100644
--- a/lib/src/solver/backtracking_solver.dart
+++ b/lib/src/solver/backtracking_solver.dart
@@ -48,6 +48,7 @@ import '../source_registry.dart';
 import '../source/hosted.dart';
 import '../source/unknown.dart';
 import '../utils.dart';
+import 'deduction.dart';
 import 'version_queue.dart';
 import 'version_selection.dart';
 import 'version_solver.dart';
@@ -103,6 +104,8 @@ class BacktrackingSolver {
   /// trigger backtracking.
   final _versions = <VersionQueue>[];
 
+  final _deductions = new Set<Deduction>();
+
   /// The current set of package versions the solver has selected, along with
   /// metadata about those packages' dependencies.
   ///
@@ -165,6 +168,10 @@ class BacktrackingSolver {
 
       _validateSdkConstraint(root.pubspec);
 
+      for (var dep in depsFor(rootID)) {
+        _deductions.add(new Required(dep));
+      }
+
       logSolve();
       var packages = await _solve();
 
@@ -269,27 +276,24 @@ class BacktrackingSolver {
   /// Selects matching versions of unselected packages, or backtracks if there
   /// are no such versions.
   Future<List<PackageId>> _solve() async {
-    // TODO(nweiz): Use real while loops when issue 23394 is fixed.
-    await Future.doWhile(() async {
+    // If there are no more packages to traverse, we've traversed the whole
+    // graph.
+    while (_selection.nextUnselected != null) {
       // Avoid starving the event queue by waiting for a timer-level event.
       await new Future(() {});
 
-      // If there are no more packages to traverse, we've traversed the whole
-      // graph.
-      var ref = _selection.nextUnselected;
-      if (ref == null) return false;
-
       var queue;
       try {
-        queue = await _versionQueueFor(ref);
+        queue = await _versionQueueFor(_selection.nextUnselected);
       } on SolveFailure catch (error) {
-        // TODO(nweiz): adjust the priority of [ref] in the unselected queue
-        // since we now know it's problematic. We should reselect it as soon as
-        // we've selected a different version of one of its dependers.
+        // TODO(nweiz): adjust the priority of the selected package in the
+        // unselected queue since we now know it's problematic. We should
+        // reselect it as soon as we've selected a different version of one of
+        // its dependers.
 
-        // There are no valid versions of [ref] to select, so we have to
+        // There are no valid versions of the package to select, so we have to
         // backtrack and unselect some previously-selected packages.
-        if (await _backtrack()) return true;
+        if (await _backtrack()) continue;
 
         // Backtracking failed, which means we're out of possible solutions.
         // Throw the error that caused us to try backtracking.
@@ -309,8 +313,7 @@ class BacktrackingSolver {
       _versions.add(queue);
 
       logSolve();
-      return true;
-    });
+    }
 
     // If we got here, we successfully found a solution.
     return _selection.ids.where((id) => !id.isMagic).toList();
@@ -343,6 +346,8 @@ class BacktrackingSolver {
     try {
       allowed = await cache.getVersions(ref);
     } on PackageNotFoundException catch (error) {
+      _deductions.add(new Disallowed(ref, [Cause.packageNotFound]));
+
       // Show the user why the package was being requested.
       throw new DependencyNotFoundException(
           ref.name, error, _selection.getDependenciesOn(ref.name).toList());
@@ -368,20 +373,16 @@ class BacktrackingSolver {
     // Bail if there is nothing to backtrack to.
     if (_versions.isEmpty) return false;
 
-    // TODO(nweiz): Use real while loops when issue 23394 is fixed.
-
     // Advance past the current version of the leaf-most package.
-    await Future.doWhile(() async {
+    while (true) {
       // Move past any packages that couldn't have led to the failure.
-      await Future.doWhile(() async {
-        if (_versions.isEmpty || _versions.last.hasFailed) return false;
+      while (!_versions.isEmpty && !_versions.last.hasFailed) {
         var queue = _versions.removeLast();
         assert(_selection.ids.last == queue.current);
         await _selection.unselectLast();
-        return true;
-      });
+      }
 
-      if (_versions.isEmpty) return false;
+      if (_versions.isEmpty) break;
 
       var queue = _versions.last;
       var name = queue.current.name;
@@ -405,13 +406,12 @@ class BacktrackingSolver {
       if (foundVersion) {
         await _selection.select(queue.current);
         logSolve();
-        return false;
-      } else {
-        logSolve('no more versions of $name, backtracking');
-        _versions.removeLast();
-        return true;
+        break;
       }
-    });
+
+      logSolve('no more versions of $name, backtracking');
+      _versions.removeLast();
+    }
 
     if (!_versions.isEmpty) _attemptedSolutions++;
     return !_versions.isEmpty;
@@ -422,15 +422,19 @@ class BacktrackingSolver {
   ///
   /// If the first version is valid, no rewinding will be done. If no version is
   /// valid, this throws a [SolveFailure] explaining why.
-  Future _findValidVersion(VersionQueue queue) {
-    // TODO(nweiz): Use real while loops when issue 23394 is fixed.
-    return Future.doWhile(() async {
+  Future _findValidVersion(VersionQueue queue) async {
+    var versions = <PackageId>[];
+    Cause cause;
+
+    while (true) {
       try {
         await _checkVersion(queue.current);
-        return false;
+        break;
       } on SolveFailure {
+        Cause newCause;
+
         var name = queue.current.name;
-        if (await queue.advance()) return true;
+        if (await queue.advance()) continue;
 
         // If we've run out of valid versions for this package, mark its oldest
         // depender as failing. This ensures that we look at graphs in which the
@@ -445,7 +449,7 @@ class BacktrackingSolver {
         // encountered while trying to find one.
         rethrow;
       }
-    });
+    }
   }
 
   /// Checks whether the package identified by [id] is valid relative to the
diff --git a/lib/src/solver/deducer.dart b/lib/src/solver/deducer.dart
new file mode 100644
index 00000000..4027315a
--- /dev/null
+++ b/lib/src/solver/deducer.dart
@@ -0,0 +1,176 @@
+class Deducer {
+  final SourceRegistry _sources;
+
+  final _allIds = <PackageRef, List<PackageId>>{};
+
+  final _required = <String, Required>{};
+
+  final _disallowed = <PackageRef, Set<Disallowed>>{};
+
+  final _dependenciesByDepender = <PackageRef, Set<Dependency>>{};
+
+  final _dependenciesByAllowed = <PackageRef, Set<Dependency>>{};
+
+  final _incompatibilities = <PackageId, Set<Incompatibility>>{};
+
+  final _toProcess = new Queue<Fact>();
+
+  void setAllIds(List<PackageId> ids) {
+    var ref = ids.first.toRef();
+    assert(ids.every((id) => id.toRef() == ref));
+    _allIds[ref] = ids;
+  }
+
+  void add(Fact initial) {
+    _toProcess.add(initial);
+
+    while (!_toProcess.isEmpty) {
+      var fact = _toProcess.removeFirst();
+      if (fact is Required) {
+        fact = _intersectRequired(fact);
+        if (fact == null) continue;
+
+        if (!_checkDisallowed(fact)) continue;
+
+        _trimDependencies(fact);
+        _trimIncompatibilities(fact);
+      } else if (fact is Disallowed) {
+        if (!_mergeDisallowed(fact)) continue;
+
+        _trimRequired(fact);
+      }
+    }
+  }
+
+  // Merge [fact] with an existing requirement for the same package, if
+  // one exists.
+  //
+  // Returns the (potentially modified) fact, or `null` if no new information
+  // was added.
+  Required _intersectRequired(Required fact) {
+    var existing = _required[fact.name];
+    if (existing == null) {
+      _required[fact.name] = fact;
+      return fact;
+    }
+
+    var intersection = _intersectDeps(existing.allowed, fact.allowed);
+    if (intersection == null) {
+      throw "Incompatible constraints!";
+    }
+
+    if (intersection.constraint == existing.allowed.constraint) return null;
+
+    _required[fact.name] = new Required(intersection, [existing, fact]);
+    return _required[fact.name];
+  }
+
+  // Returns whether [fact] should continue to be processed as-is.
+  bool _checkDisallowed(Required fact) {
+    var disallowed = _disallowed[fact.allowed.toRef()];
+    if (disallowed == null) return true;
+
+    var newDep = _depMinus(fact.allowed, disallowed);
+    if (newDep == null) throw "Incompatible constriants!";
+
+    if (newDep.constraint == fact.allowed.constraint) return true;
+
+    _toProcess.add(new Required(newDep, [fact, disallowed]));
+    return false;
+  }
+
+  void _trimDependencies(Required fact) {
+    var factRef = fact.allowed.toRef();
+    for (var dependency in _dependenciesByDepender[factRef].toList()) {
+      // Remove any dependencies from versions incompatible with [fact.allowed],
+      // since they'll never be relevant anyway.
+      if (!_depAllows(fact.allowed, dependency.depender)) {
+        // TODO: should we keep some sort of first-class representation of the
+        // cause draft so that removing a dependency removes all its
+        // consequences?
+        _removeDependency(dependency);
+      }
+    }
+
+    for (var dependency in _dependenciesByAllowed[factRef].toList()) {
+      // Remove any dependencies whose allowed versions are completely
+      // incompatible with [fact.allowed], since they'll never be relevant
+      // anyway.
+      var intersection = _intersectDeps(dependency.allowed, fact.allowed);
+      if (intersection == null) {
+        _removeDependency(dependency);
+        _toProcess.add(new Disallowed(dependency.depender, [dependency, fact]));
+        continue;
+      }
+
+      _toProcess.add(new Dependency(
+          dependency.depender, dependency.allowed.withConstraint(intersection),
+          [dependency, fact]);
+    }
+  }
+
+  void _trimIncompatibilities(Required fact) {
+    // Remove any incompatibilities that are no longer relevant.
+    var relevant = _incompatibilities[fact.allowed.toRef()].toList();
+    for (var incompatibility in relevant) {
+      PackageDep same;
+      PackageDep different;
+      if (incompatibility.package1.name == fact.allowed.name) {
+        same = incompatibility.package1;
+        different = incompatibility.package2;
+      } else {
+        assert(incompatibility.package2.name == fact.allowed.name);
+        same = incompatibility.package2;
+        different = incompatibility.package1;
+      }
+
+      // The versions of [fact.allowed] that are compatible with [different].
+      var compatible = fact.allowed.constraint.difference(same.constraint);
+      _removeIncompatibility(incompatibility);
+
+      if (compatible.isEmpty) {
+        // If [fact] only allows versions in [same], then [different] is totally
+        // disallowed.
+
+        // TODO: make [Disallowed] take a PackageDep?
+        for (var id in _idsForDep(same.withConstraint(compatible))) {
+          _toProcess.add(new Disallowed(id, [incompatibility, fact]));
+        }
+      } else if (!fact.allowed.allowsAll(compatible)) {
+        // If [fact] allows versions outside of [same], then we can reframe this
+        // incompatibility as a dependency from [different]. This is safe
+        // because [fact.allowed] needs to be selected anyway.
+        //
+        // There's no need to do this if *all* the versions allowed by [fact]
+        // are outside of [same], since one of those versions is already
+        // required.
+
+        // TODO: make [Dependency] take a PackageDep?
+        var newAllowed = same.withConstraint(compatible);
+        for (var id in _idsForDep(newAllowed)) {
+          _toProcess.add(
+              new Dependency(id, newAllowed, [incompatibility, fact]));
+        }
+      }
+    }
+  }
+
+  bool _mergeDisallowed(Disallowed fact) {
+    var set = _disallowed.putIfAbsent(fact.asRef(), () => new Set());
+    return set.add(fact);
+  }
+
+  /// Returns [dep] without matching of [ids], or `null` if this would produce
+  /// an empty constraint.
+  ///
+  /// This should use [_allIds] to carve out slices where possible. Algorithm
+  /// TBD.
+  PackageDep _depMinus(PackageDep dep, Iterable<PackageId> ids);
+
+  /// Intersect two deps, return `null` if they aren't compatible (diff name, diff
+  /// source, diff desc, or non-overlapping).
+  PackageDep _intersectDeps(PackageDep dep1, PackageDep dep2);
+
+  /// Returns whether [dep] allows [id] (name, source, description, constraint).
+  bool _depAllowed(PackageDep dep, PackageId id);
+}
diff --git a/lib/src/solver/deduction_builder.dart b/lib/src/solver/deduction_builder.dart
new file mode 100644
index 00000000..ed484245
--- /dev/null
+++ b/lib/src/solver/deduction_builder.dart
@@ -0,0 +1,61 @@
+import "../package.dart";
+import "deduction.dart";
+import "version_solver.dart";
+
+class DeductionBuilder {
+  final _ids = <PackageId>[];
+  final _failures = <SolveFailure>[];
+
+  DeductionBuilder(PackageId id, SolveFailure failure) {
+    _ids.add(id);
+    _failures.add(failure);
+  }
+
+  bool add(PackageId id, SolveFailure failure) {
+    assert(id.toRef() == _ids.first.toRef());
+    if (failure.runtimeType != _failures.first.runtimeType) return false;
+    if (failure.package != _failures.first.package) return false;
+
+    _failures.add(failure);
+  }
+
+  List<Deduction> build() {
+    if (_failures.first is BadSdkVersionException) {
+      return [new Required(_excludesIds, [Cause.badSdkVersion])];
+    }
+
+    if (_failures.first is UnknownSourceException) {
+      // TODO: we should include information about what package was depended on.
+      return [new Required(_excludesIds, [Cause.unknownSource])];
+    }
+
+    if (_failures.first is DisjointConstraintException ||
+        _failures.first is SourceMismatchException ||
+        _failures.first is DescriptionMismatchException) {
+      return [new Dependency(_includesIds, _allowed)];
+    }
+
+    // TODO: what to do about NoVersionExceptions?
+    return [];
+  }
+
+  PackageDep get _excludesIds {
+    
+  }
+
+  PackageDep get _includesIds {
+    
+  }
+
+  PackageDep get _allowed {
+    var dependencies = _failures.map((failure) {
+      return failure.dependencies
+          .firstWhere((dep) => dep.depender.name == _ids.first.name);
+    }).toList();
+
+    var constraint = dependencies.reduce(
+        (dep1, dep2) => dep1.dep.constraint.union(dep2.dep.constraint));
+
+    return new dependencies.first.dep.withConstraint(constraint);
+  }
+}
diff --git a/lib/src/solver/fact.dart b/lib/src/solver/fact.dart
new file mode 100644
index 00000000..334af3bb
--- /dev/null
+++ b/lib/src/solver/fact.dart
@@ -0,0 +1,68 @@
+import '../package.dart';
+
+abstract class Cause {
+  static const rootDependency = const _RootCause("root dependency");
+  static const explicitDependency = const _RootCause("explicit dependency");
+  static const packageNotFound = const _RootCause("package not found");
+  static const badSdkVersion = const _RootCause("bad SDK version");
+  static const unknownSource = const _RootCause("unknown dependency source");
+}
+
+class _RootCause implements Cause {
+  final String _name;
+
+  const _RootCause(this._name);
+
+  String toString() => _name;
+}
+
+/// A context-independent truth about the package graph.
+abstract class Fact implements Cause {
+  List<Cause> get causes;
+}
+
+/// A package version covered by [allowed] is required.
+class Required implements Fact {
+  final List<Cause> causes;
+
+  final PackageDep allowed;
+
+  Required(this.allowed, [Iterable<Cause> causes])
+      : causes = causes?.toList() ?? [Cause.rootDependency];
+}
+
+/// [package] can never be selected.
+class Disallowed implements Fact {
+  final List<Cause> causes;
+
+  final PackageId package;
+
+  Disallowed(this.package, Iterable<Cause> causes)
+      : causes = causes.toList();
+}
+
+/// [depender] a package version covered by [allowed].
+class Dependency implements Fact {
+  final List<Cause> causes;
+
+  final PackageId depender;
+
+  final PackageDep allowed;
+
+  Dependency(this.depender, this.allowed, [Iterable<Cause> causes])
+      : causes = causes?.toList() ?? [Cause.explicitDependency];
+}
+
+/// No versions covered by [package1] may be selected along with any versions
+/// covered by [package2].
+class Incompatibility implements Fact {
+  final List<Cause> causes;
+
+  final PackageDep package1;
+  final PackageDep package2;
+
+  Incompatible(this.package1, this.package2, Iterable<Cause> causes)
+      : causes = causes.toList() {
+    assert(package1.name != package2.name);
+  }
+}
diff --git a/solve.dart b/solve.dart
new file mode 100644
index 00000000..3c417929
--- /dev/null
+++ b/solve.dart
@@ -0,0 +1,147 @@
+import 'package:collection/collection.dart';
+
+abstract class Step {
+  final List<Step> parents;
+
+  factory Step(String message) = _MessageStep;
+}
+
+class _MessageStep implements Step {
+  final String _message;
+
+  _MessageStep(this._message);
+
+  String toString() {
+    var dependency = allowed.length == 1
+        ? allowed.first.toString()
+        : "one of ${allowed.join(', ')}";
+    return "because (${parents.join(' and ')}) $_message";
+  }
+}
+
+class Version {
+  final String name;
+  final int version;
+
+  Version(this.name, this.version);
+
+  bool operator ==(other) => other is Version && other.name == name && other.version == version;
+  int get hashCode => toString().hashCode;
+
+  String toString() => "$name$version";
+}
+
+class Constraint implements Step {
+  String get package => dependers.first.name;
+
+  String get target => allowed.first.name;
+
+  final List<Step> parents;
+  final List<Version> dependers;
+  final List<Version> allowed;
+
+  Constraint(this.dependers, this.allowed, [this.parents = const []]);
+
+  String toString() {
+    var depender = dependers.length == 1
+        ? dependers.first.toString()
+        : "${dependers.first.version}-${dependers.last.version}";
+
+    var dependency = allowed.length == 1
+        ? allowed.first.toString()
+        : "one of ${allowed.join(', ')}";
+
+    return "$depender needs $dependency";
+  }
+}
+
+class Clause implements Step {
+  final List<Step> parents;
+  final List<Version> allowed;
+
+  Clause(this.parents, this.allowed);
+
+  String toString() {
+    var dependency = allowed.length == 1
+        ? allowed.first.toString()
+        : "one of ${allowed.join(', ')}";
+    return "because (${parents.join(' and ')}) we need $dependency";
+  }
+}
+
+class Solver {
+  final List<Constraint> constraints;
+  final Map<String, Set<int>> versions;
+  final List<Clause> clauses;
+  final List<Version> selected;
+
+  Solver(this.constraints, this.versions, [this.clauses = const [], List<Version> selected])
+      : selected = selected ?? [] {
+    var clause = _findUnitClause();
+    while (clause != null) {
+      var version = clause.allowed.single;
+      selected.add(version);
+      clauses.removeWhere((clause) => clause.allowed.contains(version));
+
+      constraints.removeWhere((constraint) {
+        // Make the selected package's dependencies into clauses.
+        if (constraint.package == version.name) {
+          clauses.add(new Clause([clause, constraint], constraint.allowed));
+          return true;
+        }
+
+        // If a dependency includes the selected version, it's satisfied and can
+        // be removed.
+        if (constraint.allowed.contains(version)) return true;
+
+        // If a constraint doesn't allow this version, we can't select any of
+        // the constraint's dependers.
+        if (constraint.target == version.name) {
+          // TODO: Should we somehow record that we removed these versions here
+          // for this reason?
+          versions[constraint.target]
+              .removeAll(constraint.dependers.map((version) => version.version));
+          if (versions[constraint.target].isEmpty) 
+            // TODO: backtrack here
+            throw "out of versions of ${version.name}";
+          }
+          return true;
+        }
+
+        return false;
+      });
+
+      // If a clause includes the selected version, it's satisfied and can be
+      // removed.
+      clauses.removeWhere((clause) => clause.allowed.contains(version));
+    }
+  }
+
+  Clause _findUnitClause() {
+    var clause = clauses.firstWhere((clause) => clause.allowed.length == 1, orElse: () => null);
+    if (clause == null) return null;
+
+    clauses.remove(clause);
+    return clause;
+  }
+
+  String toString() => constraints.join("\n") + "\n" + clauses.join("\n");
+}
+
+void main() {
+  var solver = new Solver([
+    new Constraint([new Version('a', 1)], [new Version('b', 2), new Version('b', 3)]),
+    new Constraint([new Version('a', 1)], [new Version('c', 2)]),
+    new Constraint([new Version('b', 2)], [new Version('c', 3)]),
+    new Constraint([new Version('b', 3)], [new Version('c', 2), new Version('c', 3)])
+  ], {
+    'a': new Set.from([1]),
+    'b': new Set.from([2, 3]),
+    'c': new Set.from([2, 3])
+  });
+
+  print(solver);
+  print('=' * 100);
+
+  solver.select(new Version('a', 1));
+}
\ No newline at end of file
-- 
GitLab