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

Solution#evaluate; optimize/minimize

Browse Source
This commit is contained in:
David Greenspan
2015-01-05 21:34:26 -08:00
parent f48e042a9e
commit a8268b659a
3 changed files with 476 additions and 78 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1,6 +1,13 @@
Logic = {};
check = function () {};
// Disabling type checks speeds things up a LOT (several times faster).
_check = check;
// defaults to true. Returns the old value.
Logic._setAssertionsEnabled = function (areThey) {
var oldAreThey = (_check === check);
_check = areThey ? check : function () {};
return oldAreThey;
};
Logic._MiniSat = MiniSat; // Expose for testing and poking around
@@ -31,7 +38,7 @@ Logic.Term = Match.OneOf(Logic.NameTerm, Logic.NumTerm);
// you will get a Term back (of the same type, NameTerm
// or NumTerm).
Logic.not = function (operand) {
check(operand, Logic.FormulaOrTerm);
_check(operand, Logic.FormulaOrTerm);
if (operand instanceof Logic.Formula) {
return new Logic.NotFormula(operand);
} else {
@@ -74,7 +81,7 @@ Logic.FormulaOrTerm = Match.OneOf(Logic.Formula, Logic.Term);
Logic.Clause = function (/*formulaOrArray, ...*/) {
var terms = _.flatten(arguments);
check(terms, [Logic.NumTerm]);
_check(terms, [Logic.NumTerm]);
this.terms = terms; // immutable [NumTerm]
};
@@ -111,24 +118,33 @@ Logic.Solver = function () {
var self = this;
var termifier = {
term: _.bind(self._formulaToTerm, self),
term: function (formula) {
return self._formulaToTerm(formula);
},
clause: function (/*args*/) {
var formulas = _.flatten(arguments);
check(formulas, [Logic.FormulaOrTerm]);
return new Logic.Clause(_.map(formulas, termifier.term));
_check(formulas, [Logic.FormulaOrTerm]);
return new Logic.Clause(_.map(formulas, this.term));
},
generate: _.bind(self._generateFormula, self)
generate: function (isTrue, formula) {
return self._generateFormula(isTrue, formula, this);
}
};
self._termifier = termifier;
};
// Get a var number for vname, assigning it a number if it is new.
Logic.Solver.prototype.getVarNum = function (vname, _internal) {
// Setting "_createInternals" to true grants the ability to create $ variables.
// Setting "_noCreate" to true refuses to create new variables.
Logic.Solver.prototype.getVarNum = function (vname, _createInternals, _noCreate) {
var key = ' '+vname;
if (_.has(this._name2num, key)) {
return this._name2num[key];
} else {
if (vname.charAt(0) === "$" && ! _internal) {
if (_noCreate) {
throw new Error("No such variable: " + vname);
}
if (vname.charAt(0) === "$" && ! _createInternals) {
throw new Error("Only generated variable names can start with $");
}
var vnum = this._num2name.length;
@@ -139,7 +155,7 @@ Logic.Solver.prototype.getVarNum = function (vname, _internal) {
};
Logic.Solver.prototype.getVarName = function (vnum) {
check(vnum, Match.Integer);
_check(vnum, Match.Integer);
var num2name = this._num2name;
if (vnum < 1 || vnum >= num2name.length) {
throw new Error("Bad variable num: " + vnum);
@@ -152,14 +168,16 @@ Logic.Solver.prototype.getVarName = function (vnum) {
// when a Formula creates Clauses for a Solver, since Clauses require
// NumTerms. Takes a Term or an array. For example, [-3, "-foo"] might
// become [-3, -4].
Logic.Solver.prototype.toNumTerm = function (t) {
Logic.Solver.prototype.toNumTerm = function (t, _noCreate) {
var self = this;
if (_.isArray(t)) {
check(t, [Logic.Term]);
return _.map(t, _.bind(self.toNumTerm, self));
_check(t, [Logic.Term]);
return _.map(t, function (x) {
return self.toNumTerm(x);
});
} else {
check(t, Logic.Term);
_check(t, Logic.Term);
}
if (typeof t === 'number') {
@@ -170,7 +188,7 @@ Logic.Solver.prototype.toNumTerm = function (t) {
t = t.slice(1);
not = ! not;
}
var n = self.getVarNum(t);
var n = self.getVarNum(t, false, _noCreate);
return (not ? -n : n);
}
};
@@ -181,10 +199,10 @@ Logic.Solver.prototype.toNameTerm = function (t) {
var self = this;
if (_.isArray(t)) {
check(t, [Logic.Term]);
_check(t, [Logic.Term]);
return _.map(t, _.bind(self.toNameTerm, self));
} else {
check(t, Logic.Term);
_check(t, Logic.Term);
}
if (typeof t === 'string') {
@@ -210,12 +228,12 @@ Logic.Solver.prototype.toNameTerm = function (t) {
Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
var self = this;
check(cls, Logic.Clause);
_check(cls, Logic.Clause);
var extraTerms = null;
if (_extraTerms) {
extraTerms = _extraTerms;
check(extraTerms, [Logic.Term]);
_check(extraTerms, [Logic.Term]);
}
var usedF = false;
@@ -254,7 +272,7 @@ Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
// (when you use -5) will be generated.
Logic.Solver.prototype._useFormulaTerm = function (t) {
var self = this;
check(t, Logic.NumTerm);
_check(t, Logic.NumTerm);
var v = (t < 0) ? -t : t;
if (_.has(self._ungeneratedFormulas, v)) {
@@ -284,7 +302,7 @@ Logic.Solver.prototype._useFormulaTerm = function (t) {
};
Logic.Solver.prototype._addClauses = function (array, _extraTerms) {
check(array, [Logic.Clause]);
_check(array, [Logic.Clause]);
var self = this;
_.each(array, function (cls) { self._addClause(cls, _extraTerms); });
};
@@ -299,7 +317,7 @@ Logic.Solver.prototype.forbid = function (/*formulaOrArray, ...*/) {
Logic.Solver.prototype._requireForbidImpl = function (isRequire, formulas) {
var self = this;
check(formulas, [Logic.FormulaOrTerm]);
_check(formulas, [Logic.FormulaOrTerm]);
_.each(formulas, function (f) {
if (f instanceof Logic.NotFormula) {
self._requireForbidImpl(!isRequire, [f.operand]);
@@ -322,9 +340,9 @@ Logic.Solver.prototype._requireForbidImpl = function (isRequire, formulas) {
});
};
Logic.Solver.prototype._generateFormula = function (isTrue, formula) {
Logic.Solver.prototype._generateFormula = function (isTrue, formula, _termifier) {
var self = this;
check(formula, Logic.FormulaOrTerm);
_check(formula, Logic.FormulaOrTerm);
if (formula instanceof Logic.NotFormula) {
return self._generateFormula(!isTrue, formula.operand);
@@ -337,7 +355,8 @@ Logic.Solver.prototype._generateFormula = function (isTrue, formula) {
(!isTrue && info.isRequired)) {
return [new Logic.Clause()]; // never satisfied clause
} else {
var ret = formula.generateClauses(isTrue, self._termifier);
var ret = formula.generateClauses(isTrue,
_termifier || self._termifier);
return _.isArray(ret) ? ret : [ret];
}
} else { // Term
@@ -392,10 +411,13 @@ Logic.Solver.prototype._clauseStrings = function () {
});
};
Logic.Solver.prototype._getFormulaInfo = function (formula) {
Logic.Solver.prototype._getFormulaInfo = function (formula, _noCreate) {
var self = this;
var guid = formula.guid();
if (! self._formulaInfo[guid]) {
if (_noCreate) {
return null;
}
self._formulaInfo[guid] = {
// We generate a variable when a Formula is used. If the
// variable is only used positively or only used negatively, we
@@ -418,10 +440,10 @@ Logic.Solver.prototype._formulaToTerm = function (formula) {
var self = this;
if (_.isArray(formula)) {
check(formula, [Logic.FormulaOrTerm]);
_check(formula, [Logic.FormulaOrTerm]);
return _.map(formula, _.bind(self._formulaToTerm, self));
} else {
check(formula, Logic.FormulaOrTerm);
_check(formula, Logic.FormulaOrTerm);
}
if (formula instanceof Logic.NotFormula) {
@@ -453,8 +475,8 @@ Logic.Solver.prototype._formulaToTerm = function (formula) {
};
Logic._defineFormula = function (constructor, typeName, methods) {
check(constructor, Function);
check(typeName, String);
_check(constructor, Function);
_check(typeName, String);
Meteor._inherits(constructor, Logic.Formula);
constructor.prototype.type = typeName;
if (methods) {
@@ -474,7 +496,7 @@ Logic.or = function (/*formulaOrArray, ...*/) {
};
Logic.OrFormula = function (operands) {
check(operands, [Logic.FormulaOrTerm]);
_check(operands, [Logic.FormulaOrTerm]);
this.operands = operands;
};
@@ -495,7 +517,7 @@ Logic._defineFormula(Logic.OrFormula, 'or', {
});
Logic.NotFormula = function (operand) {
check(operand, Logic.FormulaOrTerm);
_check(operand, Logic.FormulaOrTerm);
this.operand = operand;
};
@@ -515,7 +537,7 @@ Logic.and = function (/*formulaOrArray, ...*/) {
};
Logic.AndFormula = function (operands) {
check(operands, [Logic.FormulaOrTerm]);
_check(operands, [Logic.FormulaOrTerm]);
this.operands = operands;
};
@@ -557,7 +579,7 @@ Logic.xor = function (/*formulaOrArray, ...*/) {
};
Logic.XorFormula = function (operands) {
check(operands, [Logic.FormulaOrTerm]);
_check(operands, [Logic.FormulaOrTerm]);
this.operands = operands;
};
@@ -618,7 +640,7 @@ Logic.atMostOne = function (/*formulaOrArray, ...*/) {
};
Logic.AtMostOneFormula = function (operands) {
check(operands, [Logic.FormulaOrTerm]);
_check(operands, [Logic.FormulaOrTerm]);
this.operands = operands;
};
@@ -671,14 +693,14 @@ Logic._defineFormula(Logic.AtMostOneFormula, 'atMostOne', {
});
Logic.implies = function (A, B) {
check(arguments.length, 2);
_check(arguments.length, 2);
return new Logic.ImpliesFormula(A, B);
};
Logic.ImpliesFormula = function (A, B) {
check(A, Logic.FormulaOrTerm);
check(B, Logic.FormulaOrTerm);
check(arguments.length, 2);
_check(A, Logic.FormulaOrTerm);
_check(B, Logic.FormulaOrTerm);
_check(arguments.length, 2);
this.A = A;
this.B = B;
};
@@ -690,14 +712,14 @@ Logic._defineFormula(Logic.ImpliesFormula, 'implies', {
});
Logic.equiv = function (A, B) {
check(arguments.length, 2);
_check(arguments.length, 2);
return new Logic.EquivFormula(A, B);
};
Logic.EquivFormula = function (A, B) {
check(A, Logic.FormulaOrTerm);
check(B, Logic.FormulaOrTerm);
check(arguments.length, 2);
_check(A, Logic.FormulaOrTerm);
_check(B, Logic.FormulaOrTerm);
_check(arguments.length, 2);
this.A = A;
this.B = B;
};
@@ -720,7 +742,7 @@ Logic.exactlyOne = function (/*formulaOrArray, ...*/) {
};
Logic.ExactlyOneFormula = function (operands) {
check(operands, [Logic.FormulaOrTerm]);
_check(operands, [Logic.FormulaOrTerm]);
this.operands = operands;
};
@@ -740,12 +762,12 @@ Logic._defineFormula(Logic.ExactlyOneFormula, 'exactlyOne', {
// a non-negative integer. Least significant bit is first. That is,
// the kth array element has a place value of 2^k.
Logic.Bits = function (formulaArray) {
check(formulaArray, [Logic.FormulaOrTerm]);
_check(formulaArray, [Logic.FormulaOrTerm]);
this.bits = formulaArray; // public, immutable
};
Logic.constantBits = function (wholeNumber) {
check(wholeNumber, Logic.WholeNumber);
_check(wholeNumber, Logic.WholeNumber);
var result = [];
while (wholeNumber) {
result.push((wholeNumber & 1) ? Logic.TRUE : Logic.FALSE);
@@ -754,15 +776,23 @@ Logic.constantBits = function (wholeNumber) {
return new Logic.Bits(result);
};
Logic.variableBits = function (baseName, nbits) {
var result = [];
for (var i = 0; i < nbits; i++) {
result.push(baseName + i);
}
return new Logic.Bits(result);
};
// bits1 <= bits2
Logic.lessThanOrEqual = function (bits1, bits2) {
return new Logic.LessThanOrEqualFormula(bits1, bits2);
};
Logic.LessThanOrEqualFormula = function (bits1, bits2) {
check(bits1, Logic.Bits);
check(bits2, Logic.Bits);
check(arguments.length, 2);
_check(bits1, Logic.Bits);
_check(bits2, Logic.Bits);
_check(arguments.length, 2);
this.bits1 = bits1;
this.bits2 = bits2;
};
@@ -839,9 +869,9 @@ Logic.lessThan = function (bits1, bits2) {
};
Logic.LessThanFormula = function (bits1, bits2) {
check(bits1, Logic.Bits);
check(bits2, Logic.Bits);
check(arguments.length, 2);
_check(bits1, Logic.Bits);
_check(bits2, Logic.Bits);
_check(arguments.length, 2);
this.bits1 = bits1;
this.bits2 = bits2;
};
@@ -871,9 +901,9 @@ Logic.equalBits = function (bits1, bits2) {
};
Logic.EqualBitsFormula = function (bits1, bits2) {
check(bits1, Logic.Bits);
check(bits2, Logic.Bits);
check(arguments.length, 2);
_check(bits1, Logic.Bits);
_check(bits2, Logic.Bits);
_check(arguments.length, 2);
this.bits1 = bits1;
this.bits2 = bits2;
};
@@ -898,9 +928,9 @@ Logic._defineFormula(Logic.EqualBitsFormula, 'equalBits', {
});
Logic.HalfAdderSum = function (formula1, formula2) {
check(formula1, Logic.FormulaOrTerm);
check(formula2, Logic.FormulaOrTerm);
check(arguments.length, 2);
_check(formula1, Logic.FormulaOrTerm);
_check(formula2, Logic.FormulaOrTerm);
_check(arguments.length, 2);
this.a = formula1;
this.b = formula2;
};
@@ -912,9 +942,9 @@ Logic._defineFormula(Logic.HalfAdderSum, 'hsum', {
});
Logic.HalfAdderCarry = function (formula1, formula2) {
check(formula1, Logic.FormulaOrTerm);
check(formula2, Logic.FormulaOrTerm);
check(arguments.length, 2);
_check(formula1, Logic.FormulaOrTerm);
_check(formula2, Logic.FormulaOrTerm);
_check(arguments.length, 2);
this.a = formula1;
this.b = formula2;
};
@@ -926,10 +956,10 @@ Logic._defineFormula(Logic.HalfAdderCarry, 'hcarry', {
});
Logic.FullAdderSum = function (formula1, formula2, formula3) {
check(formula1, Logic.FormulaOrTerm);
check(formula2, Logic.FormulaOrTerm);
check(formula3, Logic.FormulaOrTerm);
check(arguments.length, 3);
_check(formula1, Logic.FormulaOrTerm);
_check(formula2, Logic.FormulaOrTerm);
_check(formula3, Logic.FormulaOrTerm);
_check(arguments.length, 3);
this.a = formula1;
this.b = formula2;
this.c = formula3;
@@ -942,10 +972,10 @@ Logic._defineFormula(Logic.FullAdderSum, 'fsum', {
});
Logic.FullAdderCarry = function (formula1, formula2, formula3) {
check(formula1, Logic.FormulaOrTerm);
check(formula2, Logic.FormulaOrTerm);
check(formula3, Logic.FormulaOrTerm);
check(arguments.length, 3);
_check(formula1, Logic.FormulaOrTerm);
_check(formula2, Logic.FormulaOrTerm);
_check(formula3, Logic.FormulaOrTerm);
_check(arguments.length, 3);
this.a = formula1;
this.b = formula2;
this.c = formula3;
@@ -966,7 +996,7 @@ Logic._defineFormula(Logic.FullAdderCarry, 'fcarry', {
// to give weight 1; the second is bits to give weight 2;
// and so on. Returns a Bits.
var binaryWeightedSum = function (varsByWeight) {
check(varsByWeight, [[Logic.FormulaOrTerm]]);
_check(varsByWeight, [[Logic.FormulaOrTerm]]);
// initialize buckets to a two-level clone of varsByWeight
var buckets = _.map(varsByWeight, _.clone);
var lowestWeight = 0; // index of the first non-empty array
@@ -1010,8 +1040,8 @@ var pushToNth = function (arrayOfArrays, n, newItem) {
};
Logic.weightedSum = function (formulas, weights) {
check(formulas, [Logic.FormulaOrTerm]);
check(weights, [Logic.WholeNumber]);
_check(formulas, [Logic.FormulaOrTerm]);
_check(weights, [Logic.WholeNumber]);
if (! (formulas.length === weights.length && formulas.length)) {
throw new Error("Formula array and weight array must be same length (> 0)");
}
@@ -1027,13 +1057,18 @@ Logic.weightedSum = function (formulas, weights) {
whichBit++;
}
});
for (var i = 0; i < binaryWeighted.length; i++) {
if (! binaryWeighted[i]) {
binaryWeighted[i] = [];
}
}
return new Logic.Bits(binaryWeightedSum(binaryWeighted));
};
Logic.sum = function (/*formulaOrBitsOrArray, ...*/) {
var things = _.flatten(arguments);
check(things, [Match.OneOf(Logic.FormulaOrTerm, Logic.Bits)]);
_check(things, [Match.OneOf(Logic.FormulaOrTerm, Logic.Bits)]);
var binaryWeighted = [];
_.each(things, function (x) {
@@ -1092,7 +1127,7 @@ Logic.Solver.prototype.solve = function (_assumpVar) {
};
Logic.Solver.prototype.solveAssuming = function (formula) {
check(formula, Logic.FormulaOrTerm);
_check(formula, Logic.FormulaOrTerm);
// Wrap the formula in a formula of type Assumption, so that
// we always generate a var like `$assump123`, regardless
@@ -1121,7 +1156,7 @@ Logic.Solver.prototype.solveAssuming = function (formula) {
};
Logic.Assumption = function (formula) {
check(formula, Logic.FormulaOrTerm);
_check(formula, Logic.FormulaOrTerm);
this.formula = formula;
};
@@ -1137,8 +1172,23 @@ Logic._defineFormula(Logic.Assumption, 'assump', {
Logic.Solution = function (_solver, _assignment) {
this._solver = _solver;
this._assignment = _assignment;
var self = this;
self._solver = _solver;
self._assignment = _assignment;
// save a snapshot of which formulas have variables designated
// for them, but where we haven't generated clauses that constrain
// those variables in both the positive and the negative direction.
self._ungeneratedFormulas = _.clone(_solver._ungeneratedFormulas);
self._formulaValueCache = {};
self._termifier = _.extend(
{}, _solver._termifier, {
term: function (formula) {
// numeric $T or $F
return self.evaluate(formula) ? 2 : 1;
}
});
};
// Get a map of variables to their assignments,
@@ -1175,3 +1225,82 @@ Logic.Solution.prototype.getTrueVars = function () {
result.sort();
return result;
};
Logic.Solution.prototype.evaluate = function (formulaOrBits) {
var self = this;
_check(formulaOrBits, Match.OneOf(Logic.FormulaOrTerm, Logic.Bits));
if (formulaOrBits instanceof Logic.Bits) {
var ret = 0;
_.each(formulaOrBits.bits, function (f, i) {
if (self.evaluate(f)) {
ret += 1 << i;
}
});
return ret;
}
var solver = self._solver;
var assignment = self._assignment;
var formula = formulaOrBits;
if (formula instanceof Logic.NotFormula) {
return ! self.evaluate(formula.operand);
} else if (formula instanceof Logic.Formula) {
var cachedResult = self._formulaValueCache[formula.guid()];
if (typeof cachedResult === 'boolean') {
return cachedResult;
} else {
var value;
var info = solver._getFormulaInfo(formula, true);
if (info && info.varNum && info.varNum < assignment.length &&
! _.has(self._ungeneratedFormulas, info.varNum)) {
// as an optimization, read the value of the formula directly
// from a variable if the formula's clauses were completely
// generated at the time of solving.
value = assignment[info.varNum];
} else {
var clauses = solver._generateFormula(true, formula, self._termifier);
var value = _.all(clauses, function (cls) {
return _.any(cls.terms, function (t) {
return self.evaluate(t);
});
});
}
self._formulaValueCache[formula.guid()] = value;
return value;
}
} else {
// Term; convert to numeric (possibly negative), but throw
// an error if the name is not found.
var numTerm = solver.toNumTerm(formula, true);
var v = numTerm;
var isNot = false;
if (numTerm < 0) {
v = -v;
isNot = true;
}
if (v < 1 || v >= assignment.length) {
var vname = v;
if (v >= 1 && v < solver._num2name.length) {
vname = solver._num2name[v];
}
throw new Error("Variable not part of solution: " + vname);
}
var ret = assignment[v];
if (isNot) {
ret = ! ret;
}
return ret;
}
};
Logic.Solution.prototype.getWeightedSum = function (formulas, weights) {
_check(formulas, [Logic.FormulaOrTerm]);
_check(weights, [Logic.WholeNumber]);
var total = 0;
if (formulas.length !== weights.length) {
throw new Error("formulas and weights arrays must be same length");
}
for (var i = 0; i < formulas.length; i++) {
total += weights[i] * (this.evaluate(formulas[i]) ? 1 : 0);
}
return total;
};

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

@@ -1254,6 +1254,8 @@ Tinytest.add("logic-solver - eight queens", function (test) {
return String(r) + String(c);
};
var oldAssertionsEnabled = Logic._setAssertionsEnabled(false);
var solver = new Logic.Solver;
var nums = _.range(1, 9); // 1..8
_.each(nums, function (x) {
@@ -1305,6 +1307,7 @@ Tinytest.add("logic-solver - eight queens", function (test) {
return Number(queen.charAt(0)) + Number(queen.charAt(1));
});
Logic._setAssertionsEnabled(oldAssertionsEnabled);
});
@@ -1313,6 +1316,7 @@ Tinytest.add("logic-solver - Sudoku", function (test) {
return row + "," + col + "=" + value;
};
var oldAssertionsEnabled = Logic._setAssertionsEnabled(false);
//console.profile('sudoku');
var solver = new Logic.Solver();
@@ -1384,5 +1388,270 @@ Tinytest.add("logic-solver - Sudoku", function (test) {
"473258196"
].join('\n'));
Logic._setAssertionsEnabled(oldAssertionsEnabled);
//console.profileEnd('sudoku');
});
Tinytest.add("logic-solver - goes to eleven", function (test) {
var solver = new Logic.Solver();
var eleven = Logic.constantBits(11);
var x = Logic.variableBits("x", 5);
solver.require(Logic.lessThanOrEqual(x, eleven));
solver.require(Logic.lessThanOrEqual(eleven, x));
test.equal(solver.solve().getTrueVars().join(','), "x0,x1,x3");
});
Tinytest.add("logic-solver - evaluate", function (test) {
var isTrue = function (x) {
test.isTrue(x === true); // require exact "true"
};
var isFalse = function (x) {
test.isFalse(x !== false); // require exact "false"
};
var s = new Logic.Solver();
s.require("A", "-B");
var f = Logic.and("A", "-B");
s.require(f);
var g = Logic.and("A", "B");
s.forbid(g);
var h1 = Logic.xor("A", "B");
var h2 = Logic.and("A", "B");
s.require(Logic.or("$T", h1));
s.require(Logic.or("$T", h2));
var sol = s.solve();
isTrue(sol.evaluate("A"));
isFalse(sol.evaluate("-A"));
isTrue(sol.evaluate("--A"));
isFalse(sol.evaluate("B"));
isTrue(sol.evaluate("-B"));
isTrue(sol.evaluate(f));
isFalse(sol.evaluate(g));
isTrue(sol.evaluate(h1));
isFalse(sol.evaluate(h2));
isFalse(sol.evaluate(Logic.not(h1)));
isTrue(sol.evaluate(Logic.not(h2)));
isTrue(sol.evaluate(Logic.exactlyOne("A", "B")));
isFalse(sol.evaluate(Logic.exactlyOne("-A", "B")));
s.require(Logic.or("$T", Logic.not(h1)));
s.require(Logic.or("$T", Logic.not(h2)));
isTrue(sol.evaluate(h1));
isFalse(sol.evaluate(h2));
test.throws(function () {
sol.evaluate("C");
});
s.require("D");
test.throws(function () {
sol.evaluate("D");
});
test.throws(function () {
sol.evaluate(Logic.or("D", "$T"));
});
test.equal(sol.evaluate(
new Logic.Bits(["A", "B", "-A", "$F", "-B"])), 17);
var numClauses = s.clauses.length;
test.equal(sol.evaluate(Logic.weightedSum([Logic.or("A", "B"),
"A", "A", "-B"],
[7, 7, 7, 7])), 28);
test.equal(s.clauses.length, numClauses);
});
Tinytest.add("logic-solver - toy packages", function (test) {
var withSolver = function (func) {
var solver = new Logic.Solver();
_.each(allPackageVersions, function (versions, package) {
versions = _.map(versions, function (v) {
return package + "@" + v;
});
// e.g. atMostOne(["foo@1.0.0", "foo@1.0.1", "foo@2.0.0"])
solver.require(Logic.atMostOne(versions));
// e.g. equiv("foo", or(["foo@1.0.0", ...]))
solver.require(Logic.equiv(package, Logic.or(versions)));
});
_.each(dependencies, function (depMap, packageVersion) {
_.each(depMap, function (compatibleVersions, package2) {
// e.g. implies("bar@1.2.4", "foo")
solver.require(Logic.implies(packageVersion, package2));
// Now ban all incompatible versions of package2 if
// we select this packageVersion
_.each(allPackageVersions[package2], function (v) {
if (! _.contains(compatibleVersions, v)) {
solver.require(Logic.implies(packageVersion,
Logic.not(package2 + "@" + v)));
}
});
});
});
var minimize = function (solver, solution, costTerms, costWeights) {
var weightedSum = Logic.weightedSum(costTerms, costWeights);
var curSolution = solution;
var curCost = curSolution.getWeightedSum(costTerms, costWeights);
while (curCost > 0) {
var decreaseCost = Logic.lessThan(weightedSum,
Logic.constantBits(curCost));
var newSolution = solver.solveAssuming(decreaseCost);
if (! newSolution) {
return curSolution;
}
solver.require(decreaseCost);
curSolution = newSolution;
curCost = curSolution.getWeightedSum(costTerms, costWeights);
}
return curSolution;
};
var optimize = function (solver, costVectorMap) {
var solution = solver.solve();
if (! solution) {
return null;
}
var terms = [];
var weightVectors = [];
var vectorLength = null;
_.each(costVectorMap, function (vector, key) {
terms.push(key);
weightVectors.push(vector);
if (vectorLength === null) {
vectorLength = vector.length;
} else {
if (vectorLength !== vector.length) {
throw new Error("Uneven vector lengths: " + vectorLength +
" and " + vector.length);
}
}
});
for (var i = 0; i < vectorLength; i++) {
var weights = _.pluck(weightVectors, i);
solution = minimize(solver, solution, terms, weights);
}
return solution;
};
var solve = function (optionalCosts) {
var solution = (optionalCosts ? optimize(solver, optionalCosts) :
solver.solve());
if (! solution) {
return solution; // null
} else {
// only return variables like "foo@1.0.0", not "foo"
return _.filter(solution.getTrueVars(), function (v) {
return v.indexOf('@') >= 0;
});
}
};
func(solver, solve);
};
var allPackageVersions = {
'foo': ['1.0.0', '1.0.1', '2.0.0'],
'bar': ['1.2.3', '1.2.4', '1.2.5'],
'baz': ['3.0.0']
};
// Exact dependencies.
var dependencies = {
'bar@1.2.3': { foo: ['1.0.0'] },
'bar@1.2.4': { foo: ['1.0.1'] },
'bar@1.2.5': { foo: ['2.0.0'] },
'baz@3.0.0': { foo: ['1.0.0', '1.0.1'],
bar: ['1.2.4', '1.2.5'] }
};
withSolver(function (solver, solve) {
// Ask for "bar@1.2.5", get both it and "foo@2.0.0"
solver.require("bar@1.2.5");
test.equal(solve(), ["bar@1.2.5", "foo@2.0.0"]);
});
withSolver(function (solver, solve) {
// Ask for "foo@1.0.1" and *some* version of bar!
solver.require("foo@1.0.1");
solver.require("bar");
test.equal(solve(), ["bar@1.2.4", "foo@1.0.1"]);
});
withSolver(function (solver, solve) {
// Ask for versions that can't be combined
solver.require("foo@1.0.1");
solver.require("bar@1.2.3");
test.equal(solve(), null);
});
withSolver(function (solver, solve) {
// Ask for baz, automatically get versions of foo and bar
// such that foo satisfies bar's dependency!
solver.require("baz");
test.equal(solve(), ["bar@1.2.4",
"baz@3.0.0",
"foo@1.0.1"]);
});
withSolver(function (solver, solve) {
// pick earliest versions
solver.require("foo");
solver.require("bar");
test.equal(solve({ "foo@1.0.0": [0],
"foo@1.0.1": [1],
"foo@2.0.0": [2],
"bar@1.2.3": [0],
"bar@1.2.4": [1],
"bar@1.2.5": [2] }),
["bar@1.2.3", "foo@1.0.0"]);
});
withSolver(function (solver, solve) {
// pick latest versions
solver.require("foo");
solver.require("bar");
test.equal(solve({ "foo@1.0.0": [2],
"foo@1.0.1": [1],
"foo@2.0.0": [0],
"bar@1.2.3": [2],
"bar@1.2.4": [1],
"bar@1.2.5": [0] }),
["bar@1.2.5", "foo@2.0.0"]);
});
withSolver(function (solver, solve) {
// pick earliest versions (but give solver a
// cost vector with extra stuff)
solver.require("foo");
solver.require("bar");
test.equal(solve({ "foo@1.0.0": [1, 0],
"foo@1.0.1": [1, 1],
"foo@2.0.0": [1, 2],
"bar@1.2.3": [2, 0],
"bar@1.2.4": [2, 1],
"bar@1.2.5": [2, 2] }),
["bar@1.2.3", "foo@1.0.0"]);
});
withSolver(function (solver, solve) {
// pick latest versions (but give solver a
// bigger vector to work with)
solver.require("foo");
solver.require("bar");
test.equal(solve({ "foo@1.0.0": [1, 2],
"foo@1.0.1": [1, 1],
"foo@2.0.0": [1, 0],
"bar@1.2.3": [2, 2],
"bar@1.2.4": [2, 1],
"bar@1.2.5": [2, 0] }),
["bar@1.2.5", "foo@2.0.0"]);
});
});

2
packages/logic-solver/minisat_wrapper.js
View File

@@ -37,7 +37,7 @@ MiniSat.prototype.ensureVar = function (v) {
};
MiniSat.prototype.addClause = function (terms) {
check(terms, [Logic.NumTerm]);
_check(terms, [Logic.NumTerm]);
this._clauses.push(terms);
return this._native.savingStack(function (native, C) {
var termsPtr = C.allocate((terms.length+1)*4, 'i32', C.ALLOC_STACK);