github/meteor
1
1
Fork 0
mirror of https://github.com/meteor/meteor.git synced 2026-05-02 03:01:46 -04:00
Code Issues Packages Projects Releases Wiki Activity

Prevent stack overflow in logic-solver

Browse Source 
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.)
This commit is contained in:
David Greenspan
2015-03-09 21:59:04 -07:00
parent eb9698ae7b
commit 5810fd6c81
4 changed files with 126 additions and 68 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
packages/constraint-solver/datatypes.js
View File

@@ -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);
}

11
packages/constraint-solver/input-tests.js
View File

@@ -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, {
// XXX put the right answer here, when this test stops throwing an error!
});
// This case is taken from the "solver-error" branch of the meteor/rectangles
// 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/);
});

128
packages/logic-solver/logic.js
View File

@@ -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)) {
// using a Formula's var; maybe have to generate clauses
// for the Formula
var formula = self._ungeneratedFormulas[v];
var info = self._getFormulaInfo(formula);
var positive = t > 0;
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);
self._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);
self._addClauses(clauses, [v]);
}
if (info.occursPositively && info.occursNegatively) {
delete self._ungeneratedFormulas[v];
}
if (! _.has(self._ungeneratedFormulas, v)) {
return;
}
// using a Formula's var; maybe have to generate clauses
// for the Formula
var formula = self._ungeneratedFormulas[v];
var info = self._getFormulaInfo(formula);
var positive = t > 0;
// To avoid overflowing the JS stack, defer calls to addClause.
// The way we get overflows is when Formulas are deeply nested
// (which happens naturally when you call Logic.sum or
// Logic.weightedSum on a long list of terms), which causes
// addClause to call useFormulaTerm to call addClause, and so
// on. Approach: The outermost useFormulaTerm keeps a list
// of clauses to add, and then adds them in a loop using a
// special argument to addClause that passes a special argument
// to useFormulaTerm that causes those clauses to go into the
// list too. Code outside of `_useFormulaTerm` and `_addClause(s)`
// does not have to pass these special arguments to call them.
var deferredAddClauses = null;
var addClauses;
if (! _addClausesOverride) {
deferredAddClauses = [];
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
// vars from the start or end of the bucket, but
// based on a quick test, the end seems faster for solving.
var c = bucket.pop();
var b = bucket.pop();
var a = bucket.pop();
// Whether we take variables from the start or end of the
// bucket determines the shape of the tree. Taking them from
// the beginning seems faster (one particular case took 10
// seconds instead of 22 seconds).
var a = bucket.shift();
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;

50
packages/logic-solver/logic_tests.js
View File

@@ -321,11 +321,11 @@ Tinytest.add("logic-solver - Logic.and", function (test) {
Logic.or("-A", "C"))),
"-D"));
},
["-A v $or1",
"-B v $or1",
["-$or1 v -$or2 v $and1",
"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",
"$or1 v -$assump1"]));
formatLines(["$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",
"$or1 v -$assump1",
formatLines(["$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",
"$or1 v -$assump1",
formatLines(["$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"]));
"-D v -$and1"]));
// 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",
"$or1 v -$assump1",
formatLines(["$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",
"$or1 v -$assump1",
formatLines(["$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"]));