Prevent stack overflow in logic-solver

Turn recursive addClauses->useFormulaTerm->addClauses into iterative.
Also do a couple tweaks that seem to improve performance.

The "stack overflow bug" case is now hovering around 10-20 seconds.
(It's a failure case, but it sure takes a while to fail.)

packages/constraint-solver/datatypes.js

@@ -36,7 +36,10 @@ CS.PackageAndVersion.fromString = function (str) {
 // and flags, like "isWeak".
 
 CS.Dependency = function (packageConstraint, flags) {
-  check(packageConstraint, Match.OneOf(PV.PackageConstraint, String));
+  if (typeof packageConstraint !== 'string') {
+    // this `if` is because Match.OneOf is really, really slow when it fails
+    check(packageConstraint, Match.OneOf(PV.PackageConstraint, String));
+  }
   if (typeof packageConstraint === 'string') {
     packageConstraint = PV.parsePackageConstraint(packageConstraint);
   }

packages/constraint-solver/input-tests.js

@@ -339,9 +339,14 @@ Tinytest.add("constraint solver - input - fake PackageConstraint", function (tes
 });
 
 Tinytest.add("constraint solver - input - stack overflow bug", function (test) {
-  doTest(test, STACK_OVERFLOW_BUG_INPUT, {
+  // This case is taken from the "solver-error" branch of the meteor/rectangles
-    // XXX put the right answer here, when this test stops throwing an error!
+  // repo.  It's an app running from a release (new-version-solver-2) with an
-  });
+  // unsatisfiable constraint in .meteor/packages.  It caused a stack overflow
+  // before logic-solver got smarter about avoiding recursion in formula
+  // generation, and it also tests the case where an unsatisfiable constraint is
+  // in .meteor/packages.
+  doFailTest(test, STACK_OVERFLOW_BUG_INPUT,
+             /constraint follower-livedata@0.9.0 is not satisfied by follower-livedata/);
 });
 
 

packages/logic-solver/logic.js

@@ -355,7 +355,8 @@ Logic.Solver.prototype.toNameTerm = function (t) {
   }
 };
 
-Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
+Logic.Solver.prototype._addClause = function (cls, _extraTerms,
+                                              _useTermOverride) {
   var self = this;
 
   _check(cls, Logic.Clause);
@@ -387,7 +388,11 @@ Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
     } else if (v < 1 || v >= self._num2name.length) {
       throw new Error("Bad variable number: " + v);
     } else if (i < numRealTerms) {
-      self._useFormulaTerm(t);
+      if (_useTermOverride) {
+        _useTermOverride(t);
+      } else {
+        self._useFormulaTerm(t);
+      }
     }
   }
 
@@ -407,45 +412,90 @@ Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
 // "-X v 5; -Y v 5" are equivalent to "-5 => -X; -5 => -Y" (or
 // "X => 5; Y => 5").
 
-Logic.Solver.prototype._useFormulaTerm = function (t) {
+Logic.Solver.prototype._useFormulaTerm = function (t, _addClausesOverride) {
   var self = this;
   _check(t, Logic.NumTerm);
   var v = (t < 0) ? -t : t;
 
-  if (_.has(self._ungeneratedFormulas, v)) {
+  if (! _.has(self._ungeneratedFormulas, v)) {
-    // using a Formula's var; maybe have to generate clauses
+    return;
-    // for the Formula
+  }
-    var formula = self._ungeneratedFormulas[v];
+
-    var info = self._getFormulaInfo(formula);
+  // using a Formula's var; maybe have to generate clauses
-    var positive = t > 0;
+  // for the Formula
-    if (positive && ! info.occursPositively) {
+  var formula = self._ungeneratedFormulas[v];
-      // generate clauses for the formula.
+  var info = self._getFormulaInfo(formula);
-      // Eg, if we use variable `X` which represents the formula
+  var positive = t > 0;
-      // `A v B`, add the clause `A v B v -X`.
+
-      // By using the extraTerms argument to addClauses, we avoid
+  // To avoid overflowing the JS stack, defer calls to addClause.
-      // treating this as a negative occurrence of X.
+  // The way we get overflows is when Formulas are deeply nested
-      info.occursPositively = true;
+  // (which happens naturally when you call Logic.sum or
-      var clauses = self._generateFormula(true, formula);
+  // Logic.weightedSum on a long list of terms), which causes
-      self._addClauses(clauses, [-v]);
+  // addClause to call useFormulaTerm to call addClause, and so
-    } else if ((! positive) && ! info.occursNegatively) {
+  // on.  Approach:  The outermost useFormulaTerm keeps a list
-      // Eg, if we have the term `-X` where `X` represents the
+  // of clauses to add, and then adds them in a loop using a
-      // formula `A v B`, add the clauses `-A v X` and `-B v X`.
+  // special argument to addClause that passes a special argument
-      // By using the extraTerms argument to addClauses, we avoid
+  // to useFormulaTerm that causes those clauses to go into the
-      // treating this as a positive occurrence of X.
+  // list too.  Code outside of `_useFormulaTerm` and `_addClause(s)`
-      info.occursNegatively = true;
+  // does not have to pass these special arguments to call them.
-      var clauses = self._generateFormula(false, formula);
+  var deferredAddClauses = null;
-      self._addClauses(clauses, [v]);
+  var addClauses;
-    }
+  if (! _addClausesOverride) {
-    if (info.occursPositively && info.occursNegatively) {
+    deferredAddClauses = [];
-      delete self._ungeneratedFormulas[v];
+    addClauses = function (clauses, extraTerms) {
-    }
+      deferredAddClauses.push({clauses: clauses,
+                               extraTerms: extraTerms});
+    };
+  } else {
+    addClauses = _addClausesOverride;
+  }
+
+  if (positive && ! info.occursPositively) {
+    // generate clauses for the formula.
+    // Eg, if we use variable `X` which represents the formula
+    // `A v B`, add the clause `A v B v -X`.
+    // By using the extraTerms argument to addClauses, we avoid
+    // treating this as a negative occurrence of X.
+    info.occursPositively = true;
+    var clauses = self._generateFormula(true, formula);
+    addClauses(clauses, [-v]);
+  } else if ((! positive) && ! info.occursNegatively) {
+    // Eg, if we have the term `-X` where `X` represents the
+    // formula `A v B`, add the clauses `-A v X` and `-B v X`.
+    // By using the extraTerms argument to addClauses, we avoid
+    // treating this as a positive occurrence of X.
+    info.occursNegatively = true;
+    var clauses = self._generateFormula(false, formula);
+    addClauses(clauses, [v]);
+  }
+  if (info.occursPositively && info.occursNegatively) {
+    delete self._ungeneratedFormulas[v];
+  }
+
+  if (! (deferredAddClauses && deferredAddClauses.length)) {
+    return;
+  }
+
+  var useTerm = function (t) {
+    self._useFormulaTerm(t, addClauses);
+  };
+  // This is the loop that turns recursion into iteration.
+  // When addClauses calls useTerm, which calls useFormulaTerm,
+  // the nested useFormulaTerm will add any clauses to our
+  // own deferredAddClauses list.
+  while (deferredAddClauses.length) {
+    var next = deferredAddClauses.pop();
+    self._addClauses(next.clauses, next.extraTerms, useTerm);
   }
 };
 
-Logic.Solver.prototype._addClauses = function (array, _extraTerms) {
+Logic.Solver.prototype._addClauses = function (array, _extraTerms,
+                                               _useTermOverride) {
   _check(array, [Logic.Clause]);
   var self = this;
-  _.each(array, function (cls) { self._addClause(cls, _extraTerms); });
+  _.each(array, function (cls) {
+    self._addClause(cls, _extraTerms, _useTermOverride);
+  });
 };
 
 Logic.Solver.prototype.require = function (/*formulaOrArray, ...*/) {
@@ -1159,12 +1209,13 @@ var binaryWeightedSum = function (varsByWeight) {
       bucket.push(sum);
       pushToNth(buckets, lowestWeight+1, carry);
     } else {
-      // Not clear whether it's better to take the three
+      // Whether we take variables from the start or end of the
-      // vars from the start or end of the bucket, but
+      // bucket determines the shape of the tree.  Taking them from
-      // based on a quick test, the end seems faster for solving.
+      // the beginning seems faster (one particular case took 10
-      var c = bucket.pop();
+      // seconds instead of 22 seconds).
-      var b = bucket.pop();
+      var a = bucket.shift();
-      var a = bucket.pop();
+      var b = bucket.shift();
+      var c = bucket.shift();
       var sum = new Logic.FullAdderSum(a, b, c);
       var carry = new Logic.FullAdderCarry(a, b, c);
       bucket.push(sum);
@@ -1321,7 +1372,6 @@ Logic._defineFormula(Logic.Assumption, 'assump', {
   }
 });
 
-
 Logic.Solution = function (_solver, _assignment) {
   var self = this;
   self._solver = _solver;

packages/logic-solver/logic_tests.js

@@ -321,11 +321,11 @@ Tinytest.add("logic-solver - Logic.and", function (test) {
                                              Logic.or("-A", "C"))),
                          "-D"));
     },
-    ["-A v $or1",
+    ["-$or1 v -$or2 v $and1",
-     "-B v $or1",
      "A v $or2",
      "-C v $or2",
-     "-$or1 v -$or2 v $and1",
+     "-A v $or1",
+     "-B v $or1",
      "-$and1 v -D"]
   ]);
 });
@@ -583,9 +583,9 @@ Tinytest.add("logic-solver - Logic.implies, Logic.equiv", function (test) {
     ["-A v B v -$implies1", "$implies1 v C"],
     function (s) {
       s.require(Logic.or(Logic.implies(Logic.or("A", "D"), "B"), "C")); },
-    ["-A v $or1",
+    ["-$or1 v B v -$implies1",
+     "-A v $or1",
      "-D v $or1",
-     "-$or1 v B v -$implies1",
      "$implies1 v C"],
     function (s) {
       s.require(Logic.equiv("A", "B")); },
@@ -1064,11 +1064,11 @@ Tinytest.add("logic-solver - sum of terms", function (test) {
      "B v C v -$hsum1",
      "-B v -C v -$hsum1",
      "-Z v $hsum1",
-     "-B v -C v $hcarry2",
      "A v -$hcarry2 v $hsum2",
+     "-A v $hcarry2 v $hsum2",
      "B v -$hcarry2",
      "C v -$hcarry2",
-     "-A v $hcarry2 v $hsum2",
+     "-B v -C v $hcarry2",
      "Y v -$hsum2",
      "A v $hcarry2 v -$hsum2",
      "-A v -$hcarry2 v -$hsum2",
@@ -1114,17 +1114,17 @@ Tinytest.add("logic-solver - sum of terms", function (test) {
      "$T",
      "-A v -B v $hcarry1",
      "-$hcarry1 v $T",
-     "A v -$hcarry1",
-     "B v -$hcarry1",
      "$hcarry1 v $T v -$xor1",
      "-$hcarry1 v -$T v -$xor1",
+     "A v -$hcarry1",
+     "B v -$hcarry1",
      "A v -B v $hsum1",
      "-A v B v $hsum1",
      "$xor1 v -$hsum1 v $F",
-     "A v B v -$hsum1",
-     "-A v -B v -$hsum1",
      "$hsum1 v $F v -$xor2",
      "-$hsum1 v -$F v -$xor2",
+     "A v B v -$hsum1",
+     "-A v -B v -$hsum1",
      "$xor2 v $xor1"]
   ]);
 });
@@ -1201,29 +1201,29 @@ Tinytest.add("logic-solver - assumptions", function (test) {
   test.equal(s.solveAssuming(atLeastOne).getMap(),
              { A: false, B: true, C: false, D: false });
   test.equal(formatLines(s._clauseStrings()),
-             formatLines(["A v B v C v D v -$or1",
+             formatLines(["$or1 v -$assump1",
-                          "$or1 v -$assump1"]));
+                          "A v B v C v D v -$or1"]));
 
   // assume the same thing again
   test.equal(s.solveAssuming(atLeastOne).getMap(),
              { A: false, B: true, C: false, D: false });
   test.equal(formatLines(s._clauseStrings()),
-             formatLines(["A v B v C v D v -$or1",
+             formatLines(["$or1 v -$assump1",
-                          "$or1 v -$assump1",
+                          "A v B v C v D v -$or1",
                           "$or1 v -$assump2"]));
 
   var none = Logic.and("-A", "-B", "-C", "-D");
   test.equal(s.solveAssuming(none).getMap(),
              { A: false, B: false, C: false, D: false });
   test.equal(formatLines(s._clauseStrings()),
-             formatLines(["A v B v C v D v -$or1",
+             formatLines(["$or1 v -$assump1",
-                          "$or1 v -$assump1",
+                          "A v B v C v D v -$or1",
                           "$or1 v -$assump2",
+                          "$and1 v -$assump3",
                           "-A v -$and1",
                           "-B v -$and1",
                           "-C v -$and1",
-                          "-D v -$and1",
+                          "-D v -$and1"]));
-                          "$and1 v -$assump3"]));
 
   // require a formula that was previously just temporarily assumed!
   s.require(atLeastOne);
@@ -1231,28 +1231,28 @@ Tinytest.add("logic-solver - assumptions", function (test) {
              // any one could be true
              { A: false, B: true, C: false, D: false });
   test.equal(formatLines(s._clauseStrings()),
-             formatLines(["A v B v C v D v -$or1",
+             formatLines(["$or1 v -$assump1",
-                          "$or1 v -$assump1",
+                          "A v B v C v D v -$or1",
                           "$or1 v -$assump2",
+                          "$and1 v -$assump3",
                           "-A v -$and1",
                           "-B v -$and1",
                           "-C v -$and1",
                           "-D v -$and1",
-                          "$and1 v -$assump3",
                           "$or1"]));
 
   test.equal(s.solveAssuming("D").getMap(),
              // at least D is true; other than that, anything goes
              { A: false, B: true, C: false, D: true });
   test.equal(formatLines(s._clauseStrings()),
-             formatLines(["A v B v C v D v -$or1",
+             formatLines(["$or1 v -$assump1",
-                          "$or1 v -$assump1",
+                          "A v B v C v D v -$or1",
                           "$or1 v -$assump2",
+                          "$and1 v -$assump3",
                           "-A v -$and1",
                           "-B v -$and1",
                           "-C v -$and1",
                           "-D v -$and1",
-                          "$and1 v -$assump3",
                           "$or1",
                           "D v -$assump4"]));