packages/logic-solver/logic_tests.js
Tinytest.add("logic-solver - require", function (test) {
var s = new Logic.Solver;
s.require('foo');
test.equal(s._clauseData(), [[3]]);
test.equal(s._clauseStrings(), ["foo"]);
s.forbid('foo');
test.equal(s._clauseData(), [[3], [-3]]);
test.equal(s._clauseStrings(), ["foo", "-foo"]);
s.require([['foo'], '-bar'], '--foo', 'foo');
test.equal(s._clauseData(), [[3], [-3], [3], [-4], [3], [3]]);
test.equal(s._clauseStrings(), ["foo", "-foo", "foo",
"-bar", "foo", "foo"]);
});
Tinytest.add("logic-solver - _clauseStrings", function (test) {
var s = new Logic.Solver;
s.require('foo');
test.equal(s._clauseStrings(), ["foo"]);
s.require('-myPackage 1.0.0');
test.equal(s._clauseStrings(), ["foo", '-"myPackage 1.0.0"']);
});
Tinytest.add("logic-solver - illegal NameTerms", function (test) {
var s = new Logic.Solver;
test.throws(function () {
s.require('');
});
test.throws(function () {
s.require('-');
});
test.throws(function () {
s.require('0');
});
test.throws(function () {
s.require('$x');
});
test.throws(function () {
s.require('-1');
});
test.throws(function () {
s.require('---123');
});
});
Tinytest.add("logic-solver - toNameTerm, toNumTerm", function (test) {
var s = new Logic.Solver;
test.equal(s.toNumTerm("foo"), 3);
test.equal(s.toNumTerm("-foo"), -3);
test.equal(s.toNameTerm(3), "foo");
test.equal(s.toNameTerm(-3), "-foo");
test.equal(s.toNameTerm("-----foo"), "-foo");
});
var formatLines = function (stringArray) {
return JSON.stringify(stringArray).replace(/","/g, '",\n "');
};
var checkClauses = function (test, f, expected) {
check(f, Function);
check(expected, [String]);
var s = new Logic.Solver;
f(s);
test.equal(formatLines(s._clauseStrings()),
formatLines(expected));
};
var runClauseTests = function (test, funcsAndExpecteds) {
check(funcsAndExpecteds.length % 2, 0);
for (var i = 0; i < funcsAndExpecteds.length; i++) {
var f = funcsAndExpecteds[i];
i++;
var expected = funcsAndExpecteds[i];
checkClauses(test, f, expected);
}
};
Tinytest.add("logic-solver - bad NumTerms", function (test) {
test.throws(function () {
var s = new Logic.Solver;
s.require(3);
});
test.throws(function () {
var s = new Logic.Solver;
s.require(-3);
});
test.throws(function () {
var s = new Logic.Solver;
s.require(0);
});
test.throws(function () {
var s = new Logic.Solver;
s.require(Logic.or(3));
});
});
Tinytest.add("logic-solver - true and false", function (test) {
runClauseTests(test, [
// Clauses that forbid $F and require $T are automatically
// generated as the first two clauses. Using each of them
// causes the relevant clause to be included in the output.
function (s) {
s.require(Logic.or(Logic.TRUE, Logic.not(Logic.TRUE)));
},
["$T", "$T v -$T"],
function (s) {
s.require(Logic.or(Logic.not(Logic.TRUE),
Logic.not(Logic.FALSE)));
},
["-$F", "$T", "-$T v -$F"],
// requiring or forbidding $T, $F, or the negation of one
// of those is optimizated. this is helpful when formulas
// expand to one of these (e.g. Logic.and() => $T => []).
function (s) { s.require(Logic.TRUE); }, [],
function (s) { s.require(Logic.FALSE); }, [""],
function (s) { s.require(Logic.not(Logic.TRUE)); }, [""],
function (s) { s.require(Logic.not(Logic.FALSE)); }, [],
function (s) { s.forbid(Logic.TRUE); }, [""],
function (s) { s.forbid(Logic.FALSE); }, [],
function (s) { s.forbid(Logic.not(Logic.TRUE)); }, [],
function (s) { s.forbid(Logic.not(Logic.FALSE)); }, [""]
]);
});
Tinytest.add("logic-solver - Logic.or", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.or('A', 'B'));
},
["A v B"],
function (s) {
s.require(Logic.or(['A', 'B']));
},
["A v B"],
function (s) {
s.require(Logic.or(['A'], ['B']));
},
["A v B"],
function (s) {
s.require('A');
s.require(Logic.or('-C', 'D', 3));
},
["A", "-C v D v A"],
function (s) {
s.forbid(Logic.or('A', '-B'));
},
["-A", "B"],
function (s) {
s.forbid(Logic.or());
},
[],
function (s) {
s.require(Logic.or());
},
[""]
]);
});
Tinytest.add("logic-solver - Formula sharing", function (test) {
var f = Logic.or("A", "B");
var s1 = new Logic.Solver;
var s2 = new Logic.Solver;
s1.require("X");
s1.require(f);
s2.forbid(f);
test.equal(s1._clauseData(), [[3], [4, 5]]);
test.equal(s2._clauseData(), [[-3], [-4]]);
});
Tinytest.add("logic-solver - nested Logic.or", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.or(Logic.or("A", "B"), Logic.or("C", "D")));
},
["A v B v -$or1", "C v D v -$or2", "$or1 v $or2"]
]);
});
Tinytest.add("logic-solver - Logic.not term", function (test) {
test.equal(Logic.not("foo"), "-foo");
test.equal(Logic.not("-foo"), "foo");
test.equal(Logic.not("--foo"), "-foo");
test.equal(Logic.not(1), -1);
test.equal(Logic.not(-1), 1);
});
Tinytest.add("logic-solver - Logic.not formula", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.not(Logic.or("A", "B")));
},
["-A", "-B"],
function (s) {
s.forbid(Logic.not(Logic.or("A", "B")));
},
["A v B"],
function (s) {
s.require(Logic.or(Logic.not(Logic.or("A", "B")), "C"));
},
["-A v $or1", "-B v $or1", "-$or1 v C"]
]);
});
Tinytest.add("logic-solver - Require/forbid after formula gen", function (test) {
runClauseTests(test, [
function (s) {
// Use a formula in the positive and then require it. Requiring
// the formula does not regenerate its clauses, it just requires
// the formula's variable ($or1).
var f = Logic.or("A", "B");
s.require(Logic.or(f, "C"));
s.require(f);
},
["A v B v -$or1","$or1 v C","$or1"]
]);
runClauseTests(test, [
function (s) {
// Use a formula in the posiive and then forbid it.
// Forbidding a formula that has not been used in the
// negative before requires generating new clauses.
var f = Logic.or("A", "B");
s.require(Logic.or(f, "C"));
s.forbid(f);
},
["A v B v -$or1","$or1 v C","-A v $or1","-B v $or1","-$or1"]
]);
runClauseTests(test, [
function (s) {
// Use a formula in the negative and then forbid it.
var f = Logic.or("A", "B");
s.require(Logic.or(Logic.not(f), "C"));
s.forbid(f);
},
["-A v $or1","-B v $or1","-$or1 v C","-$or1"]
]);
runClauseTests(test, [
function (s) {
// Use a formula in the negative and then require it.
var f = Logic.or("A", "B");
s.require(Logic.or(Logic.not(f), "C"));
s.require(f);
},
["-A v $or1","-B v $or1","-$or1 v C","A v B v -$or1","$or1"]
]);
runClauseTests(test, [
function (s) {
var f = Logic.or("A", "B");
s.require(Logic.and(f, "C"));
s.require(f);
},
// Arguments to AND are generated in place, meaning that if `f`
// is used elsewhere, its clauses will be generated twice.
// Oh well. It's a trade-off. The same applies to OR when
// generating the false case.
["A v B",
"C",
"A v B"]
]);
});
Tinytest.add("logic-solver - Logic.and", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.and('A', 'B'));
},
["A", "B"],
function (s) {
s.require(Logic.and(['A', 'B']));
},
["A", "B"],
function (s) {
s.require(Logic.and(['A'], ['-B'], 'C'));
},
["A", "-B", "C"],
function (s) {
s.forbid(Logic.and('A', '-B', 'C'));
},
["-A v B v -C"],
function (s) {
s.forbid(Logic.and());
},
[""],
function (s) {
s.require(Logic.and());
},
[],
function (s) {
s.require(Logic.or(Logic.and(Logic.or("A", "B"),
Logic.or("-A", "C")),
"-D"));
},
["A v B v -$and1",
"-A v C v -$and1",
"$and1 v -D"],
function (s) {
s.require(Logic.or(Logic.not(Logic.and(Logic.or("A", "B"),
Logic.or("-A", "C"))),
"-D"));
},
["-$or1 v -$or2 v $and1",
"A v $or2",
"-C v $or2",
"-A v $or1",
"-B v $or1",
"-$and1 v -D"]
]);
});
Tinytest.add("logic-solver - Logic.xor", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.xor()); },
[""],
function (s) {
s.forbid(Logic.xor()); },
[],
function (s) {
s.require(Logic.or(Logic.xor(), Logic.xor())); },
["-$F", "$F v $F"],
function (s) {
s.require(Logic.xor("A")); },
["A"],
function (s) {
s.forbid(Logic.xor("A")); },
["-A"],
function (s) {
s.require(Logic.xor("A", "B")); },
["A v B", "-A v -B"],
function (s) {
s.forbid(Logic.xor("A", "B")); },
["A v -B", "-A v B"],
function (s) {
s.require(Logic.xor(["A", []], ["B"], [])); },
["A v B", "-A v -B"],
function (s) {
s.require(Logic.xor("A", "B", "C")); },
["A v B v C", "A v -B v -C", "-A v B v -C", "-A v -B v C"],
function (s) {
s.forbid(Logic.xor("A", "B", "C")); },
["-A v -B v -C", "-A v B v C", "A v -B v C", "A v B v -C"],
function (s) {
s.require(Logic.xor("A", "B", "C", "D")); },
["A v B v C v -$xor1",
"A v -B v -C v -$xor1",
"-A v B v -C v -$xor1",
"-A v -B v C v -$xor1",
"$xor1 v D",
"-A v -B v -C v $xor1",
"-A v B v C v $xor1",
"A v -B v C v $xor1",
"A v B v -C v $xor1",
"-$xor1 v -D"],
function (s) {
s.forbid(Logic.xor("A", "B", "C", "D")); },
["A v B v C v -$xor1",
"A v -B v -C v -$xor1",
"-A v B v -C v -$xor1",
"-A v -B v C v -$xor1",
"$xor1 v -D",
"-A v -B v -C v $xor1",
"-A v B v C v $xor1",
"A v -B v C v $xor1",
"A v B v -C v $xor1",
"-$xor1 v D"],
function (s) {
s.require(Logic.xor("A", "B", "C", "D", "E")); },
["A v B v C v -$xor1",
"A v -B v -C v -$xor1",
"-A v B v -C v -$xor1",
"-A v -B v C v -$xor1",
"D v E v -$xor2",
"-D v -E v -$xor2",
"$xor1 v $xor2",
"-A v -B v -C v $xor1",
"-A v B v C v $xor1",
"A v -B v C v $xor1",
"A v B v -C v $xor1",
"D v -E v $xor2",
"-D v E v $xor2",
"-$xor1 v -$xor2"],
function (s) {
s.forbid(Logic.xor("A", "B", "C", "D", "E")); },
["A v B v C v -$xor1",
"A v -B v -C v -$xor1",
"-A v B v -C v -$xor1",
"-A v -B v C v -$xor1",
"D v -E v $xor2",
"-D v E v $xor2",
"$xor1 v -$xor2",
"-A v -B v -C v $xor1",
"-A v B v C v $xor1",
"A v -B v C v $xor1",
"A v B v -C v $xor1",
"D v E v -$xor2",
"-D v -E v -$xor2",
"-$xor1 v $xor2"]
]);
});
Tinytest.add("logic-solver - require/forbid generation", function (test) {
runClauseTests(test, [
function (s) {
var f = Logic.and("A", "B");
s.require(Logic.or(f, "C"));
s.forbid(f);
},
["A v -$and1", "B v -$and1", "$and1 v C", "-A v -B v $and1", "-$and1"],
function (s) {
var f = Logic.and("A", "B");
s.require(Logic.or(Logic.not(f), "C"));
s.require(f);
},
["-A v -B v $and1", "-$and1 v C", "A v -$and1", "B v -$and1", "$and1"],
function (s) {
var f = Logic.and("A", "B");
s.require(f);
s.require(f);
},
["A", "B"],
function (s) {
var f = Logic.and("A", "B");
s.forbid(f);
s.forbid(f);
},
["-A v -B"],
function (s) {
var f = Logic.and("A", "B");
s.require(f);
s.forbid(f);
s.forbid(f);
},
["A", "B", ""],
function (s) {
var f = Logic.and("A", "B");
s.forbid(f);
s.require(f);
s.require(f);
},
["-A v -B", ""],
function (s) {
var f = Logic.and("A", "B");
s.require(f);
s.require(Logic.or(f, "C"));
},
["$T", "A", "B", "$T v C"],
function (s) {
var f = Logic.and("A", "B");
s.require(f);
s.require(Logic.or(Logic.not(f), "C"));
},
["$T", "A", "B", "-$T v C"],
function (s) {
var f = Logic.and("A", "B");
s.forbid(f);
s.require(Logic.or(Logic.not(f), "C"));
},
["-$F", "-A v -B", "-$F v C"],
function (s) {
var f = Logic.and("A", "B");
s.require(f);
s.forbid(f);
s.require(Logic.or(f, "C"));
},
["$T", "A", "B", "", "$T v C"],
function (s) {
var f = Logic.and("A", "B");
s.forbid(f);
s.require(f);
s.require(Logic.or(f, "C"));
},
["$T", "-A v -B", "", "$T v C"]
]);
});
Tinytest.add("logic-solver - Logic.atMostOne", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.atMostOne()); },
[],
function (s) {
s.forbid(Logic.atMostOne()); },
[""],
function (s) {
s.require(Logic.atMostOne("A")); },
[],
function (s) {
s.forbid(Logic.atMostOne("A")); },
[""],
function (s) {
s.require(Logic.atMostOne("A", "B")); },
["-A v -B"],
function (s) {
s.forbid(Logic.atMostOne("A", "B")); },
["A", "B"],
function (s) {
s.require(Logic.atMostOne("A", "B", "C")); },
["-A v -B", "-A v -C", "-B v -C"],
function (s) {
s.forbid(Logic.atMostOne("A", "B", "C")); },
["A v B", "A v C", "B v C"],
function (s) {
s.require(Logic.atMostOne("A", "B", "C", "D")); },
// If D is true, then all of A,B,C must be false.
// Two of A,B,C must be false.
["-A v $or1",
"-B v $or1",
"-C v $or1",
"-$or1 v -D",
"-A v -B",
"-A v -C",
"-B v -C"],
function (s) {
s.forbid(Logic.atMostOne("A", "B", "C", "D")); },
// If any two of A,B,C are false (lines 3,4,5), then we'll need
// one of A,B,C and D to be true (lines 1,2 by implication of
// line 6). (This isn't the reasoning that generated the clauses,
// but it's one way to think of it.)
["A v B v C v $atMostOne1",
"D v $atMostOne1",
"A v B v $atMostOne2",
"A v C v $atMostOne2",
"B v C v $atMostOne2",
"-$atMostOne1 v -$atMostOne2"],
function (s) {
s.require(Logic.atMostOne("A", "B", "C", "D", "E")); },
["-A v $or1",
"-B v $or1",
"-C v $or1",
"-D v $or2",
"-E v $or2",
"-$or1 v -$or2",
"-A v -B",
"-A v -C",
"-B v -C",
"-D v -E"],
function (s) {
s.forbid(Logic.atMostOne("A", "B", "C", "D", "E")); },
["A v B v C v $atMostOne1",
"D v E v $atMostOne1",
"A v B v $atMostOne2",
"A v C v $atMostOne2",
"B v C v $atMostOne2",
"D v $atMostOne3",
"E v $atMostOne3",
"-$atMostOne1 v -$atMostOne2 v -$atMostOne3"]
]);
});
Tinytest.add("logic-solver - Logic.implies, Logic.equiv", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.implies("A", "B")); },
["-A v B"],
function (s) {
s.forbid(Logic.implies("A", "B")); },
["A", "-B"],
function (s) {
s.require(Logic.or(Logic.implies("A", "B"), "C")); },
["-A v B v -$implies1", "$implies1 v C"],
function (s) {
s.require(Logic.or(Logic.implies(Logic.or("A", "D"), "B"), "C")); },
["-$or1 v B v -$implies1",
"-A v $or1",
"-D v $or1",
"$implies1 v C"],
function (s) {
s.require(Logic.equiv("A", "B")); },
["A v -B",
"-A v B"],
function (s) {
s.forbid(Logic.equiv("A", "B")); },
["A v B",
"-A v -B"],
function (s) {
s.require(Logic.equiv(Logic.or("A", "B"),
Logic.or("C", "D"))); },
["A v B v -$or1",
"-C v $or2",
"-D v $or2",
"$or1 v -$or2",
"-A v $or1",
"-B v $or1",
"C v D v -$or2",
"-$or1 v $or2"]
]);
});
Tinytest.add("logic-solver - Logic.exactlyOne", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.exactlyOne()); },
[""],
function (s) {
s.forbid(Logic.exactlyOne()); },
[],
function (s) {
s.require(Logic.exactlyOne("A")); },
["A"],
function (s) {
s.forbid(Logic.exactlyOne("A")); },
["-A"],
function (s) {
s.require(Logic.exactlyOne("A", "B")); },
["A v B", "-A v -B"],
function (s) {
s.forbid(Logic.exactlyOne("A", "B")); },
["A v -B", "-A v B"],
function (s) {
s.require(Logic.exactlyOne("A", "B", "C")); },
["-A v -B",
"-A v -C",
"-B v -C",
"A v B v C"],
function (s) {
s.forbid(Logic.exactlyOne("A", "B", "C")); },
["A v B v $atMostOne1",
"A v C v $atMostOne1",
"B v C v $atMostOne1",
"-A v $or1",
"-B v $or1",
"-C v $or1",
"-$atMostOne1 v -$or1"]
]);
});
var equalBitFormulas = function (test, bits1, bits2) {
test.isTrue(bits1 instanceof Logic.Bits);
test.isTrue(bits2 instanceof Logic.Bits);
// the elements of bits1 and bits2 will have to be
// terms (or the same Formula objects) for this to
// compare by value
test.equal(bits1.bits, bits2.bits);
};
Tinytest.add("logic-solver - Logic.constantBits", function (test) {
equalBitFormulas(test, Logic.constantBits(0), new Logic.Bits([]));
equalBitFormulas(test, Logic.constantBits(1), new Logic.Bits(["$T"]));
equalBitFormulas(test, Logic.constantBits(2), new Logic.Bits(["$F", "$T"]));
equalBitFormulas(test, Logic.constantBits(3), new Logic.Bits(["$T", "$T"]));
equalBitFormulas(test, Logic.constantBits(4), new Logic.Bits(["$F", "$F", "$T"]));
equalBitFormulas(test, Logic.constantBits(5), new Logic.Bits(["$T", "$F", "$T"]));
});
Tinytest.add("logic-solver - Logic.equalBits", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits([]))); },
[],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits([]))); },
[""],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
["-A"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
["-A"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
["A"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
["A"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A", "B", "C"]),
new Logic.Bits([]))); },
["-A", "-B", "-C"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits(["A", "B", "C"]))); },
["-A", "-B", "-C"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A", "B", "C"]),
new Logic.Bits([]))); },
["A v B v C"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits([]),
new Logic.Bits(["A", "B", "C"]))); },
["A v B v C"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["A v -B", "-A v B"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["A v B", "-A v -B"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A", "B"]),
new Logic.Bits(["X", "Y"]))); },
["A v -X", "-A v X",
"B v -Y", "-B v Y"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A", "B"]),
new Logic.Bits(["X", "Y"]))); },
["A v X v $equiv1",
"-A v -X v $equiv1",
"B v Y v $equiv2",
"-B v -Y v $equiv2",
"-$equiv1 v -$equiv2"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A", "B"]),
new Logic.Bits(["X"]))); },
["A v -X", "-A v X", "-B"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A", "B"]),
new Logic.Bits(["X"]))); },
["A v X v $equiv1",
"-A v -X v $equiv1",
"-$equiv1 v B"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits(["X", "Y"]))); },
["A v -X", "-A v X", "-Y"],
function (s) {
s.forbid(Logic.equalBits(new Logic.Bits(["A"]),
new Logic.Bits(["X", "Y"]))); },
["A v X v $equiv1",
"-A v -X v $equiv1",
"-$equiv1 v Y"],
function (s) {
s.require(Logic.equalBits(new Logic.Bits([Logic.or("A", "B")]),
new Logic.Bits([Logic.or("C", "D")]))); },
["A v B v -$or1",
"-C v $or2",
"-D v $or2",
"$or1 v -$or2",
"-A v $or1",
"-B v $or1",
"C v D v -$or2",
"-$or1 v $or2"]
]);
});
Tinytest.add("logic-solver - Logic.lessThan[OrEqual]", function (test) {
runClauseTests(test, [
function (s) {
s.require(Logic.lessThan(new Logic.Bits([]),
new Logic.Bits([]))); },
[""],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits([]),
new Logic.Bits([]))); },
[],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits([]),
new Logic.Bits([]))); },
[],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits([]),
new Logic.Bits([]))); },
[""],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
[""],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
["-A"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
[],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits([]))); },
["A"],
function (s) {
s.require(Logic.lessThan(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
["A"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
[],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
["-A"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits([]),
new Logic.Bits(["A"]))); },
[""],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["-A v B",
"A v B",
"-A v -B"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["-A v B"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["-B v A"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits(["B"]))); },
["-B v A",
"B v A",
"-B v -A"],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["B", "A"]),
new Logic.Bits(["Y", "X"]))); },
["-A v X",
"A v X v -$xor1",
"-A v -X v -$xor1",
"$xor1 v -B v Y",
"B v Y v -$xor2",
"-B v -Y v -$xor2",
"$xor2 v $xor1"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["B", "A"]),
new Logic.Bits(["Y", "X"]))); },
["-A v X",
"A v X v -$xor1",
"-A v -X v -$xor1",
"$xor1 v -B v Y"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["B", "A"]),
new Logic.Bits(["Y", "X"]))); },
["-X v A",
"X v A v -$xor1",
"-X v -A v -$xor1",
"$xor1 v -Y v B"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["B", "A"]),
new Logic.Bits(["Y", "X"]))); },
["-X v A",
"X v A v -$xor1",
"-X v -A v -$xor1",
"$xor1 v -Y v B",
"Y v B v -$xor2",
"-Y v -B v -$xor2",
"$xor2 v $xor1"],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits(["Y", "X"]))); },
["X v -A v Y",
"A v Y v -$xor1",
"-A v -Y v -$xor1",
"$xor1 v X"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits(["Y", "X"]))); },
["X v -A v Y"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["A"]),
new Logic.Bits(["Y", "X"]))); },
["-X",
"-Y v A"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["A"]),
new Logic.Bits(["Y", "X"]))); },
["-X",
"-Y v A",
"Y v A",
"-Y v -A"],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["B", "A"]),
new Logic.Bits(["X"]))); },
["-A",
"-B v X",
"B v X",
"-B v -X"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["B", "A"]),
new Logic.Bits(["X"]))); },
["-A",
"-B v X"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["B", "A"]),
new Logic.Bits(["X"]))); },
["A v -X v B"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["B", "A"]),
new Logic.Bits(["X"]))); },
["A v -X v B",
"X v B v -$xor1",
"-X v -B v -$xor1",
"$xor1 v A"],
function (s) {
s.require(Logic.lessThan(new Logic.Bits(["C", "B", "A"]),
new Logic.Bits(["Z", "Y", "X"]))); },
["-A v X",
"A v X v -$xor1",
"-A v -X v -$xor1",
"$xor1 v -B v Y",
"B v Y v -$xor2",
"-B v -Y v -$xor2",
"$xor2 v $xor1 v -C v Z",
"C v Z v -$xor3",
"-C v -Z v -$xor3",
"$xor3 v $xor2 v $xor1"],
function (s) {
s.require(Logic.lessThanOrEqual(new Logic.Bits(["C", "B", "A"]),
new Logic.Bits(["Z", "Y", "X"]))); },
["-A v X",
"A v X v -$xor1",
"-A v -X v -$xor1",
"$xor1 v -B v Y",
"B v Y v -$xor2",
"-B v -Y v -$xor2",
"$xor2 v $xor1 v -C v Z"],
function (s) {
s.forbid(Logic.lessThan(new Logic.Bits(["C", "B", "A"]),
new Logic.Bits(["Z", "Y", "X"]))); },
["-X v A",
"X v A v -$xor1",
"-X v -A v -$xor1",
"$xor1 v -Y v B",
"Y v B v -$xor2",
"-Y v -B v -$xor2",
"$xor2 v $xor1 v -Z v C"],
function (s) {
s.forbid(Logic.lessThanOrEqual(new Logic.Bits(["C", "B", "A"]),
new Logic.Bits(["Z", "Y", "X"]))); },
["-X v A",
"X v A v -$xor1",
"-X v -A v -$xor1",
"$xor1 v -Y v B",
"Y v B v -$xor2",
"-Y v -B v -$xor2",
"$xor2 v $xor1 v -Z v C",
"Z v C v -$xor3",
"-Z v -C v -$xor3",
"$xor3 v $xor2 v $xor1"]
]);
});
Tinytest.add("logic-solver - half/full sum/carry", function (test) {
runClauseTests(test, [
function (s) {
s.require(new Logic.HalfAdderSum("A", "B")); },
["A v B", "-A v -B"],
function (s) {
s.forbid(new Logic.HalfAdderSum("A", "B")); },
["A v -B", "-A v B"],
function (s) {
s.require(Logic.or(new Logic.HalfAdderSum("A", "B"), "C")); },
["A v B v -$hsum1",
"-A v -B v -$hsum1",
"$hsum1 v C"],
function (s) {
s.require(new Logic.HalfAdderCarry("A", "B")); },
["A", "B"],
function (s) {
s.forbid(new Logic.HalfAdderCarry("A", "B")); },
["-A v -B"],
function (s) {
s.require(Logic.or(new Logic.HalfAdderCarry("A", "B"), "C")); },
["A v -$hcarry1",
"B v -$hcarry1",
"$hcarry1 v C"]
]);
runClauseTests(test, [
function (s) {
s.require(new Logic.FullAdderSum("A", "B", "C")); },
["A v B v C",
"A v -B v -C",
"-A v B v -C",
"-A v -B v C"],
function (s) {
s.forbid(new Logic.FullAdderSum("A", "B", "C")); },
["-A v -B v -C",
"-A v B v C",
"A v -B v C",
"A v B v -C"],
function (s) {
s.require(Logic.or(new Logic.FullAdderSum("A", "B", "C"), "D")); },
["A v B v C v -$fsum1",
"A v -B v -C v -$fsum1",
"-A v B v -C v -$fsum1",
"-A v -B v C v -$fsum1",
"$fsum1 v D"],
function (s) {
s.require(new Logic.FullAdderCarry("A", "B", "C")); },
["A v B",
"A v C",
"B v C"],
function (s) {
s.forbid(new Logic.FullAdderCarry("A", "B", "C")); },
["-A v -B",
"-A v -C",
"-B v -C"],
function (s) {
s.require(Logic.or(new Logic.FullAdderCarry("A", "B", "C"), "D")); },
["A v B v -$fcarry1",
"A v C v -$fcarry1",
"B v C v -$fcarry1",
"$fcarry1 v D"]
]);
});
Tinytest.add("logic-solver - sum of terms", function (test) {
runClauseTests(test, [
function (s) {
s.require(
// XY = A + B + C
Logic.equalBits(new Logic.Bits(["Y", "X"]),
Logic.sum("A", "B", "C")));
},
["-A v -B v -C v $fsum1",
"-A v B v C v $fsum1",
"A v -B v C v $fsum1",
"A v B v -C v $fsum1",
"Y v -$fsum1",
"A v B v C v -$fsum1",
"A v -B v -C v -$fsum1",
"-A v B v -C v -$fsum1",
"-A v -B v C v -$fsum1",
"-Y v $fsum1",
"-A v -B v $fcarry1",
"-A v -C v $fcarry1",
"-B v -C v $fcarry1",
"X v -$fcarry1",
"A v B v -$fcarry1",
"A v C v -$fcarry1",
"B v C v -$fcarry1",
"-X v $fcarry1"],
function (s) {
s.require(
// AB + C = XYZ
Logic.equalBits(new Logic.Bits(["Z", "Y", "X"]),
Logic.sum(new Logic.Bits(["B", "A"]), "C")));
},
["B v -C v $hsum1",
"-B v C v $hsum1",
"Z v -$hsum1",
"B v C v -$hsum1",
"-B v -C v -$hsum1",
"-Z v $hsum1",
"A v -$hcarry2 v $hsum2",
"-A v $hcarry2 v $hsum2",
"B v -$hcarry2",
"C v -$hcarry2",
"-B v -C v $hcarry2",
"Y v -$hsum2",
"A v $hcarry2 v -$hsum2",
"-A v -$hcarry2 v -$hsum2",
"-Y v $hsum2",
"-A v -$hcarry2 v $hcarry1",
"X v -$hcarry1",
"A v -$hcarry1",
"B v -$hcarry1",
"C v -$hcarry1",
"-X v $hcarry1"],
function (s) {
s.require(
// 8X + 15Y = ZABCDE
Logic.equalBits(new Logic.Bits(["E", "D", "C", "B", "A", "Z"]),
Logic.weightedSum(["X", "Y"], [8, 15])));
},
// C, D, and E all = Y
// AB = X + Y
// Z = 0
["E v -Y",
"-E v Y",
"D v -Y",
"-D v Y",
"C v -Y",
"-C v Y",
"X v -Y v $hsum1",
"-X v Y v $hsum1",
"B v -$hsum1",
"X v Y v -$hsum1",
"-X v -Y v -$hsum1",
"-B v $hsum1",
"-X v -Y v $hcarry1",
"A v -$hcarry1",
"X v -$hcarry1",
"Y v -$hcarry1",
"-A v $hcarry1",
"-Z"],
function (s) {
// A + B < 2
s.require(Logic.lessThan(Logic.sum("A", "B"), Logic.constantBits(2)));
},
["-$F",
"$T",
"-A v -B v $hcarry1",
"-$hcarry1 v $T",
"$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",
"$hsum1 v $F v -$xor2",
"-$hsum1 v -$F v -$xor2",
"A v B v -$hsum1",
"-A v -B v -$hsum1",
"$xor2 v $xor1"]
]);
});
Tinytest.add("logic-solver - MiniSat", function (test) {
var M = new Logic._MiniSat;
// Unique solution is (1,2,3,4) = (0,1,0,0)
test.isTrue(M.addClause([-4]));
test.isTrue(M.addClause([-1, -2]));
test.isTrue(M.addClause([4, -1, 2]));
test.isTrue(M.addClause([1, 2, 3]));
test.isTrue(M.addClause([1, 2, -3, 4]));
test.isTrue(M.addClause([1, -2, -3]));
test.isTrue(M.solve());
test.equal(M.getSolution(), [null, false, true, false, false]);
M.addClause([1, -2, 3, 4]);
test.isFalse(M.solve());
test.isFalse(M.addClause([4]));
});
Tinytest.add("logic-solver - MiniSat solveAssuming", function (test) {
var M = new Logic._MiniSat;
M.ensureVar(1);
test.isTrue(M.solveAssuming(1));
test.equal(M.getSolution(), [null, true]);
test.isTrue(M.solveAssuming(1));
test.equal(M.getSolution(), [null, true]);
test.isTrue(M.addClause([-1]));
test.isTrue(M.addClause([2, -2]));
test.isTrue(M.solve());
test.equal(M.getSolution(), [null, false, false]); // empirically
test.isTrue(M.solveAssuming(2));
test.equal(M.getSolution(), [null, false, true]);
test.isTrue(M.solve());
});
Tinytest.add("logic-solver - simple solve", function (test) {
var s = new Logic.Solver;
// Unique solution is (A,B,C,D) = (0,1,0,0)
s.require("-D");
s.require(Logic.or("-A", "-B"));
s.require(Logic.or("D", "-A", "B"));
s.require(Logic.or("A", "B", "C"));
s.require(Logic.or("A", "B", "-C", "D"));
s.require(Logic.or("A", "-B", "-C"));
var sol = s.solve();
test.equal(s._minisat._clauses.length, 8); // includes "$T" and "-$F"
test.isTrue(sol);
test.equal(sol.getMap(), {
A: false, B: true, C: false, D: false
});
s.require(Logic.or("A", "-B", "C", "D"));
var sol2 = s.solve();
test.isFalse(sol2);
// make sure we only added the new clause
test.equal(s._minisat._clauses.length, 9);
});
Tinytest.add("logic-solver - getVarNum", function (test) {
var s = new Logic.Solver();
s.require("A");
var a = s.getVarNum("A");
test.isTrue(a > 0); // this also confirms it's a number
test.equal(s.getVarNum("B", true), 0); // noCreate = true
var b = s.getVarNum("B");
test.notEqual(a, b);
var a2 = s.getVarNum("A");
var b2 = s.getVarNum("B");
test.equal(a, a2);
test.equal(b, b2);
});
Tinytest.add("logic-solver - assumptions", function (test) {
var s = new Logic.Solver;
s.getVarNum("A");
s.getVarNum("B");
s.getVarNum("C");
s.getVarNum("D");
// MiniSat could return any assignment of the variables here,
// but we happen to know that it uses all-false as a starting
// point for search.
test.equal(s.solve().getMap(), { A: false, B: false, C: false, D: false });
var atLeastOne = Logic.or("A", "B", "C", "D");
// which of A,B,C,D comes back true is totally arbitrary, but it's
// deterministic as long as we don't touch anything.
test.equal(s.solveAssuming(atLeastOne).getMap(),
{ A: false, B: true, C: false, D: false });
test.equal(formatLines(s._clauseStrings()),
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(["$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(["$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"]));
// require a formula that was previously just temporarily assumed!
s.require(atLeastOne);
test.equal(s.solve().getMap(),
// any one could be true
{ A: false, B: true, C: false, D: false });
test.equal(formatLines(s._clauseStrings()),
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",
"$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(["$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",
"$or1",
"D v -$assump4"]));
var sum = Logic.sum("A", "B", "C", "D");
var atLeast2 = Logic.greaterThanOrEqual(sum, Logic.constantBits(2));
test.equal(s.solveAssuming(atLeast2).getMap(),
// any two or more, including D
{ A: false, B: true, C: false, D: true });
s.require(atLeast2);
var atLeast3 = Logic.greaterThanOrEqual(sum, Logic.constantBits(3));
test.equal(s.solveAssuming(atLeast3).getMap(),
// any three or more, including D
{ A: true, B: true, C: false, D: true });
s.require(atLeast3);
var atLeast4 = Logic.greaterThanOrEqual(sum, Logic.constantBits(4));
test.equal(s.solveAssuming(atLeast4).getMap(),
{ A: true, B: true, C: true, D: true });
s.forbid("C");
test.equal(s.solve().getMap(),
{ A: true, B: true, C: false, D: true });
});
Tinytest.add("logic-solver - eight queens", function (test) {
var boardSquare = function (r, c) {
return String(r) + ',' + String(c);
};
Logic._disablingTypeChecks(function () {
var solver = new Logic.Solver;
var nums = Array.from({length: 8}, (_, i) => i + 1); // 1..8
nums.forEach(function (x) {
// one per row x, one per column x
solver.require(Logic.exactlyOne(nums.map(function (y) {
return boardSquare(x, y);
})));
solver.require(Logic.exactlyOne(nums.map(function (y) {
return boardSquare(y, x);
})));
});
// At most one queen per diagonal. A diagonal
// consists of squares whose row + column sums
// to a constant, or the horizontal flip of
// such a set of squares.
for (var flip = 0; flip <= 1; flip++) {
for (var sum = 2; sum <= 16; sum++) {
var vars = [];
for (var r = 1; r <= sum-1; r++) {
var c = sum - r;
if (flip)
c = 9-c;
if (r >= 1 && r <= 8 && c >= 1 && c <= 8) {
vars.push(boardSquare(r,c));
}
}
solver.require(Logic.atMostOne(vars));
}
}
var solution = solver.solve().getTrueVars();
// solution might be, for example,
// ["16", "24", "31", "45", "58", "62", "77", "83"]
test.equal(solution.length, 8);
test.isTrue(/^([1-8],[1-8] ){7}[1-8],[1-8]$/.test(solution.join(' ')));
var assertEightDifferent = function (transformFunc) {
test.equal([...new Set(solution.map(transformFunc))].length, 8);
};
// queens occur in eight different rows, eight different columns
assertEightDifferent(function (queen) { return queen.charAt(0); });
assertEightDifferent(function (queen) { return queen.charAt(2); });
// queens' row/col have eight different sums, eight different differences
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) - Number(queen.charAt(2));
});
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) + Number(queen.charAt(2));
});
});
});
Tinytest.add("logic-solver - Sudoku", function (test) {
var v = function (row, col, value) {
return row + "," + col + "=" + value;
};
Logic._disablingTypeChecks(function () {
//console.profile('sudoku');
var solver = new Logic.Solver();
// All rows, columns, and digits are 0-based internally.
for (var x = 0; x < 9; x++) {
// Find the top-left of box x. For example, Box 0 has a top-left
// of (0,0). Box 3 has a top-left of (3,0).
var boxRow = Math.floor(x/3)*3;
var boxCol = (x%3)*3;
for (var y = 0; y < 9; y++) {
var numberInEachSquare = [];
var columnHavingYInRowX = [];
var rowHavingYInColumnX = [];
var squareHavingYInBoxX = [];
for (var z = 0; z < 9; z++) {
numberInEachSquare.push(v(x,y,z));
columnHavingYInRowX.push(v(x,z,y));
rowHavingYInColumnX.push(v(z,x,y));
squareHavingYInBoxX.push(v(
boxRow + Math.floor(z/3),
boxCol + (z%3),
y));
}
solver.require(Logic.exactlyOne(numberInEachSquare));
solver.require(Logic.exactlyOne(columnHavingYInRowX));
solver.require(Logic.exactlyOne(rowHavingYInColumnX));
solver.require(Logic.exactlyOne(squareHavingYInBoxX));
}
}
// Input a pretty hard Sudoku from here:
// http://www.menneske.no/sudoku/eng/showpuzzle.html?number=6903541
var puzzle = [
"....839..",
"1......3.",
"..4....7.",
".42.3....",
"6.......4",
"....7..1.",
".2.......",
".8...92..",
"...25...6"
];
for (var r = 0; r < 9; r++) {
var str = puzzle[r];
for (var c = 0; c < 9; c++) {
// zero-based digit
var digit = str.charCodeAt(c) - 49;
if (digit >= 0 && digit < 9) {
solver.require(v(r, c, digit));
}
}
}
var solution = solver.solve().getTrueVars();
var solutionString = solution.map(function (v) {
return String(Number(v.slice(-1)) + 1);
}).join('').match(/.{9}/g).join('\n');
test.equal(solutionString, [
"765483921",
"198726435",
"234915678",
"842531769",
"617892354",
"359674812",
"926147583",
"581369247",
"473258196"
].join('\n'));
//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(','), "x$0,x$1,x$3");
});
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();
Object.entries(allPackageVersions).forEach(function ([pkg, versions]) {
versions = versions.map(function (v) {
return pkg + "@" + 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(pkg, Logic.or(versions)));
});
Object.entries(dependencies).forEach(function ([packageVersion, depMap]) {
Object.entries(depMap).forEach(function ([package2, compatibleVersions]) {
// 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.
// NOTE: This is not the best way to express constraints. It's
// not what we do in the real package constraint solver.
allPackageVersions[package2].forEach(function (v) {
if (! compatibleVersions.includes(v)) {
solver.require(Logic.implies(packageVersion,
Logic.not(package2 + "@" + v)));
}
});
});
});
var optimize = function (solver, costVectorMap) {
var solution = solver.solve();
if (! solution) {
return null;
}
var terms = [];
var weightVectors = [];
var vectorLength = null;
Object.entries(costVectorMap).forEach(function ([key, vector]) {
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 = weightVectors.map(function(vector){
return vector[i]
});
solution = solver.minimizeWeightedSum(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 solution.getTrueVars().filter(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"]);
});
});
Tinytest.add("logic-solver - minimize", function (test) {
var s = new Logic.Solver();
s.require(Logic.or("A", "B", "C", "D"));
// cost is equal to the number of false variables
var costTerms = ["-A", "-B", "-C", "-D"];
var costWeights = 1;
var solution1 = s.solve();
// nothing forces the cost (= the number of false variables)
// to be greater than 0, but MiniSat will always discover
// a sparser solution than (1,1,1,1) first.
test.isTrue(solution1.getWeightedSum(costTerms, costWeights) > 0);
var solution2 = s.minimizeWeightedSum(solution1, costTerms, costWeights);
test.isFalse(solution1 === solution2);
test.equal(solution2.getWeightedSum(costTerms, costWeights), 0);
test.equal(solution2.getTrueVars(), ["A", "B", "C", "D"]);
});
Tinytest.add("logic-solver - maximize", function (test) {
var s = new Logic.Solver();
// Find subset of {2, 5, 10, 11, 15} that sums to as close
// as possible to 19 without going over.
var costWeights = [2, 5, 10, 11, 15];
// name variables after the weights
var costTerms = costWeights.map(function (w) {
return "#"+w;
});
var ws = Logic.weightedSum(costTerms, costWeights);
s.require(Logic.lessThanOrEqual(ws, Logic.constantBits(19)));
var sol = s.solve();
var sol2 = s.maximizeWeightedSum(sol, costTerms, costWeights, ws);
test.equal(sol2.getTrueVars(), ["#11", "#2", "#5"]);
});
Tinytest.add("logic-solver - weightedSum", function (test) {
var s = new Logic.Solver();
s.require(Logic.equalBits(
Logic.weightedSum(["A", "B"], [1, 4]),
Logic.constantBits(5)));
var sol = s.solve();
test.isTrue(sol);
test.equal(sol.getTrueVars(), ["A", "B"]);
});
Tinytest.add("logic-solver - type-checking", function (test) {
// on by default
test.throws(function () {
Logic.or({});
}, /is not a Formula or Term/);
// ... but can turn it off (this shouldn't throw)
Logic._disablingTypeChecks(function () {
Logic.or({});
});
});