RequirementMachine: Use trie to find overlapping rules

Author: slavapestov

lib/AST/RequirementMachine/RewriteSystem.cpp

@@ -127,28 +127,6 @@ bool RewriteSystem::addRule(MutableTerm lhs, MutableTerm rhs) {
     MergedAssociatedTypes.emplace_back(lhs, rhs);
   }
 
-  // Since we added a new rule, we have to check for overlaps between the
-  // new rule and all existing rules.
-  for (unsigned j : indices(Rules)) {
-    // A rule does not overlap with itself.
-    if (i == j)
-      continue;
-
-    // We don't have to check for overlap with deleted rules.
-    if (Rules[j].isDeleted())
-      continue;
-
-    // The overlap check is not commutative so we have to check both
-    // directions.
-    Worklist.emplace_back(i, j);
-    Worklist.emplace_back(j, i);
-
-    if (DebugCompletion) {
-      llvm::dbgs() << "$ Queued up (" << i << ", " << j << ") and ";
-      llvm::dbgs() << "(" << j << ", " << i << ")\n";
-    }
-  }
-
   // Tell the caller that we added a new rule.
   return true;
 }

lib/AST/RequirementMachine/RewriteSystem.h

@@ -13,7 +13,7 @@
 #ifndef SWIFT_REWRITESYSTEM_H
 #define SWIFT_REWRITESYSTEM_H
 
-#include <algorithm>
+#include "llvm/ADT/DenseSet.h"
 
 #include "ProtocolGraph.h"
 #include "Symbol.h"
@@ -48,12 +48,6 @@ class Rule final {
   const Term &getLHS() const { return LHS; }
   const Term &getRHS() const { return RHS; }
 
-  OverlapKind checkForOverlap(const Rule &other,
-                              MutableTerm &t,
-                              MutableTerm &v) const {
-    return LHS.checkForOverlap(other.LHS, t, v);
-  }
-
   /// Returns if the rule was deleted.
   bool isDeleted() const {
     return deleted;
@@ -114,9 +108,8 @@ class RewriteSystem final {
   /// See RewriteSystem::processMergedAssociatedTypes() for details.
   std::vector<std::pair<MutableTerm, MutableTerm>> MergedAssociatedTypes;
 
-  /// A list of pending pairs for checking overlap in the completion
-  /// procedure.
-  std::deque<std::pair<unsigned, unsigned>> Worklist;
+  /// Pairs of rules which have already been checked for overlap.
+  llvm::DenseSet<std::pair<unsigned, unsigned>> CheckedOverlaps;
 
   /// Set these to true to enable debugging output.
   unsigned DebugSimplify : 1;
@@ -176,8 +169,9 @@ class RewriteSystem final {
   void dump(llvm::raw_ostream &out) const;
 
 private:
-  Optional<std::pair<MutableTerm, MutableTerm>>
-  computeCriticalPair(const Rule &lhs, const Rule &rhs) const;
+  std::pair<MutableTerm, MutableTerm>
+  computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
+                      const Rule &lhs, const Rule &rhs) const;
 
   Symbol mergeAssociatedTypes(Symbol lhs, Symbol rhs) const;
   void processMergedAssociatedTypes();

lib/AST/RequirementMachine/RewriteSystemCompletion.cpp

@@ -67,95 +67,6 @@ Symbol Symbol::prependPrefixToConcreteSubstitutions(
     }, ctx);
 }
 
-/// Check if this term overlaps with \p other for the purposes
-/// of the Knuth-Bendix completion algorithm.
-///
-/// An overlap occurs if one of the following two cases holds:
-///
-/// 1) If this == TUV and other == U.
-/// 2) If this == TU and other == UV.
-///
-/// In both cases, we return the subterms T and V, together with
-/// an 'overlap kind' identifying the first or second case.
-///
-/// If both rules have identical left hand sides, either case could
-/// apply, but we arbitrarily pick case 1.
-///
-/// Note that this relation is not commutative; we need to check
-/// for overlap between both (X and Y) and (Y and X).
-OverlapKind
-Term::checkForOverlap(Term other,
-                      MutableTerm &t,
-                      MutableTerm &v) const {
-  if (*this == other) {
-    // If this term is equal to the other term, we have an overlap.
-    t = MutableTerm();
-    v = MutableTerm();
-    return OverlapKind::First;
-  }
-
-  if (size() > other.size()) {
-    // If this term is longer than the other term, check if it contains
-    // the other term.
-    auto first1 = begin();
-    while (first1 <= end() - other.size()) {
-      if (std::equal(other.begin(), other.end(), first1)) {
-        // We have an overlap.
-        t = MutableTerm(begin(), first1);
-        v = MutableTerm(first1 + other.size(), end());
-
-        // If both T and V are empty, we have two equal terms, which
-        // should have been handled above.
-        assert(!t.empty() || !v.empty());
-        assert(t.size() + other.size() + v.size() == size());
-
-        return OverlapKind::First;
-      }
-
-      ++first1;
-    }
-  }
-
-  // Finally, check if a suffix of this term is equal to a prefix of
-  // the other term.
-  unsigned count = std::min(size(), other.size());
-  auto first1 = end() - count;
-  auto last2 = other.begin() + count;
-
-  // Initial state, depending on size() <=> other.size():
-  //
-  // ABC   -- count = 3, first1 = this[0], last2 = other[3]
-  // XYZ
-  //
-  // ABC   -- count = 2, first1 = this[1], last2 = other[2]
-  //  XY
-  //
-  // ABC   -- count = 3, first1 = this[0], last2 = other[3]
-  // XYZW
-
-  // Advance by 1, since we don't need to check for full containment
-  ++first1;
-  --last2;
-
-  while (last2 != other.begin()) {
-    if (std::equal(other.begin(), last2, first1)) {
-      t = MutableTerm(begin(), first1);
-      v = MutableTerm(last2, other.end());
-
-      assert(!t.empty());
-      assert(!v.empty());
-      assert(t.size() + other.size() - v.size() == size());
-
-      return OverlapKind::Second;
-    }
-
-    ++first1;
-    --last2;
-  }
-
-  return OverlapKind::None;
-}
-
 /// If we have two symbols [P:T] and [Q:T], produce a merged symbol:
 ///
 /// - If P inherits from Q, this is just [P:T].
@@ -359,7 +270,9 @@ void RewriteSystem::processMergedAssociatedTypes() {
   MergedAssociatedTypes.clear();
 }
 
-/// Compute a critical pair from two rewrite rules.
+/// Compute a critical pair from the left hand sides of two rewrite rules,
+/// where \p rhs begins at \p from, which must be an iterator pointing
+/// into \p lhs.
 ///
 /// There are two cases:
 ///
@@ -388,15 +301,11 @@ void RewriteSystem::processMergedAssociatedTypes() {
 /// concrete substitution 'X' to get 'A.X'; the new concrete term
 /// is now rooted at the same level as A.B in the rewrite system,
 /// not just B.
-Optional<std::pair<MutableTerm, MutableTerm>>
-RewriteSystem::computeCriticalPair(const Rule &lhs, const Rule &rhs) const {
-  MutableTerm t, v;
-
-  switch (lhs.checkForOverlap(rhs, t, v)) {
-  case OverlapKind::None:
-    return None;
-
-  case OverlapKind::First: {
+std::pair<MutableTerm, MutableTerm>
+RewriteSystem::computeCriticalPair(ArrayRef<Symbol>::const_iterator from,
+                                   const Rule &lhs, const Rule &rhs) const {
+  auto end = lhs.getLHS().end();
+  if (from + rhs.getLHS().size() < end) {
     // lhs == TUV -> X, rhs == U -> Y.
 
     // Note: This includes the case where the two rules have exactly
@@ -405,31 +314,31 @@ RewriteSystem::computeCriticalPair(const Rule &lhs, const Rule &rhs) const {
     // In this case, T and V are both empty.
 
     // Compute the term TYV.
+    MutableTerm t(lhs.getLHS().begin(), from);
     t.append(rhs.getRHS());
-    t.append(v);
+    t.append(from + rhs.getLHS().size(), lhs.getLHS().end());
     return std::make_pair(MutableTerm(lhs.getRHS()), t);
-  }
-
-  case OverlapKind::Second: {
+  } else {
     // lhs == TU -> X, rhs == UV -> Y.
 
-    if (v.back().isSuperclassOrConcreteType()) {
-      v.back() = v.back().prependPrefixToConcreteSubstitutions(
-          t, Context);
-    }
+    // Compute the term T.
+    MutableTerm t(lhs.getLHS().begin(), from);
 
     // Compute the term XV.
-    MutableTerm xv;
-    xv.append(lhs.getRHS());
-    xv.append(v);
+    MutableTerm xv(lhs.getRHS());
+    xv.append(rhs.getLHS().begin() + (lhs.getLHS().end() - from),
+              rhs.getLHS().end());
+
+    if (xv.back().isSuperclassOrConcreteType()) {
+      xv.back() = xv.back().prependPrefixToConcreteSubstitutions(
+          t, Context);
+    }
 
     // Compute the term TY.
     t.append(rhs.getRHS());
+
     return std::make_pair(xv, t);
   }
-  }
-
-  llvm_unreachable("Bad overlap kind");
 }
 
 /// Computes the confluent completion using the Knuth-Bendix algorithm.
@@ -448,64 +357,97 @@ RewriteSystem::computeConfluentCompletion(unsigned maxIterations,
                                           unsigned maxDepth) {
   unsigned steps = 0;
 
-  // The worklist must be processed in first-in-first-out order, to ensure
-  // that we resolve all overlaps among the initial set of rules before
-  // moving on to overlaps between rules introduced by completion.
-  while (!Worklist.empty()) {
-    // Check if we've already done too much work.
-    if (Rules.size() > maxIterations)
-      return std::make_pair(CompletionResult::MaxIterations, steps);
-
-    auto next = Worklist.front();
-    Worklist.pop_front();
-
-    const auto &lhs = Rules[next.first];
-    const auto &rhs = Rules[next.second];
-
-    if (DebugCompletion) {
-      llvm::dbgs() << "$ Check for overlap: (#" << next.first << ") ";
-      llvm::dbgs() << lhs << "\n";
-      llvm::dbgs() << "                -vs- (#" << next.second << ") ";
-      llvm::dbgs() << rhs << ":\n";
-    }
+  bool again = false;
+
+  do {
+    std::vector<std::pair<MutableTerm, MutableTerm>> resolvedCriticalPairs;
+
+    // For every rule, looking for other rules that overlap with this rule.
+    for (unsigned i = 0, e = Rules.size(); i < e; ++i) {
+      const auto &lhs = Rules[i];
+      if (lhs.isDeleted())
+        continue;
+
+      // Look up every suffix of this rule in the trie using findAll(). This
+      // will find both kinds of overlap:
+      //
+      // 1) rules whose left hand side is fully contained in [from,to)
+      // 2) rules whose left hand side has a prefix equal to [from,to)
+      auto from = lhs.getLHS().begin();
+      auto to = lhs.getLHS().end();
+      while (from < to) {
+        Trie.findAll(from, to, [&](unsigned j) {
+          // We don't have to consider the same pair of rules more than once,
+          // since those critical pairs were already resolved.
+          if (!CheckedOverlaps.insert(std::make_pair(i, j)).second)
+            return;
+
+          const auto &rhs = Rules[j];
+          if (rhs.isDeleted())
+            return;
+
+          if (from == lhs.getLHS().begin()) {
+            // While every rule will have an overlap of the first kind
+            // with itself, it's not useful to consider since the
+            // resulting trivial pair is always trivial.
+            if (i == j)
+              return;
+
+            // If the first rule's left hand side is a proper prefix
+            // of the second rule's left hand side, don't do anything.
+            //
+            // We will find the 'opposite' overlap later, where the two
+            // rules are swapped around. Then it becomes an overlap of
+            // the first kind, and will be handled as such.
+            if (rhs.getLHS().size() > lhs.getLHS().size())
+              return;
+          }
 
-    auto pair = computeCriticalPair(lhs, rhs);
-    if (!pair) {
-      if (DebugCompletion) {
-        llvm::dbgs() << " no overlap\n\n";
-      }
-      continue;
-    }
+          // Try to repair the confluence violation by adding a new rule.
+          resolvedCriticalPairs.push_back(computeCriticalPair(from, lhs, rhs));
 
-    MutableTerm first, second;
+          if (DebugCompletion) {
+            const auto &pair = resolvedCriticalPairs.back();
 
-    // We have a critical pair (X, Y).
-    std::tie(first, second) = *pair;
+            llvm::dbgs() << "$ Overlapping rules: (#" << i << ") ";
+            llvm::dbgs() << lhs << "\n";
+            llvm::dbgs() << "                -vs- (#" << j << ") ";
+            llvm::dbgs() << rhs << ":\n";
+            llvm::dbgs() << "$$ First term of critical pair is "
+                         << pair.first << "\n";
+            llvm::dbgs() << "$$ Second term of critical pair is "
+                         << pair.second << "\n\n";
+          }
+        });
 
-    if (DebugCompletion) {
-      llvm::dbgs() << "$$ First term of critical pair is " << first << "\n";
-      llvm::dbgs() << "$$ Second term of critical pair is " << second << "\n\n";
+        ++from;
+      }
     }
-    unsigned i = Rules.size();
 
-    // Try to repair the confluence violation by adding a new rule
-    // X == Y.
-    if (!addRule(first, second))
-      continue;
+    again = false;
+    for (const auto &pair : resolvedCriticalPairs) {
+      // Check if we've already done too much work.
+      if (Rules.size() > maxIterations)
+        return std::make_pair(CompletionResult::MaxIterations, steps);
 
-    // Only count a 'step' once we add a new rule.
-    ++steps;
+      if (!addRule(pair.first, pair.second))
+        continue;
 
-    const auto &newRule = Rules[i];
-    if (newRule.getDepth() > maxDepth)
-      return std::make_pair(CompletionResult::MaxDepth, steps);
+      // Check if the new rule is too long.
+      if (Rules.back().getDepth() > maxDepth)
+        return std::make_pair(CompletionResult::MaxDepth, steps);
 
-    // If this new rule merges any associated types, process the merge now
+      // Only count a 'step' once we add a new rule.
+      ++steps;
+      again = true;
+    }
+
+    // If the added rules merged any associated types, process the merges now
     // before we continue with the completion procedure. This is important
     // to perform incrementally since merging is required to repair confluence
     // violations.
     processMergedAssociatedTypes();
-  }
+  } while (again);
 
   return std::make_pair(CompletionResult::Success, steps);
 }