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

No longer shift vars by 1 in MiniSat C wrapper

Browse Source 
See 26e00d4d75
This commit is contained in:
David Greenspan
2015-03-05 08:23:24 -08:00
parent 023d471831
commit 90c6b3e1bb
3 changed files with 15 additions and 9 deletions
Download Patch File Download Diff File Expand all files Collapse all files

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

@@ -1199,14 +1199,14 @@ Tinytest.add("logic-solver - assumptions", function (test) {
// 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: false, C: true, D: false });
{ 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"]));
// assume the same thing again
test.equal(s.solveAssuming(atLeastOne).getMap(),
{ A: false, B: false, C: true, D: false });
{ 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",
@@ -1229,7 +1229,7 @@ Tinytest.add("logic-solver - assumptions", function (test) {
s.require(atLeastOne);
test.equal(s.solve().getMap(),
// any one could be true
{ A: true, B: false, C: false, D: false });
{ 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",
@@ -1243,7 +1243,7 @@ Tinytest.add("logic-solver - assumptions", function (test) {
test.equal(s.solveAssuming("D").getMap(),
// at least D is true; other than that, anything goes
{ A: true, B: false, C: false, D: true });
{ 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",
@@ -1259,12 +1259,13 @@ Tinytest.add("logic-solver - assumptions", function (test) {
var sum = Logic.sum("A", "B", "C", "D");
var atLeast2 = Logic.greaterThanOrEqual(sum, Logic.constantBits(2));
test.equal(s.solveAssuming(atLeast2).getMap(),
{ A: true, B: false, C: false, D: true });
// 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: false, C: true, D: true });
{ 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(),

4
packages/logic-solver/minisat.js
View File

File diff suppressed because one or more lines are too long

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

@@ -103,6 +103,11 @@ MiniSat.prototype.retireVar = function (v) {
this._C._retireVar(v);
};
// The "conflict clause" feature of MiniSat is not what it sounds
// like, unfortunately -- it doesn't help explain conflicts.
// It only tells us which assumption vars are to blame for a failed
// solveAssuming (and we only ever pass one var).
// We keep this function around in case we discover a use for it.
MiniSat.prototype.getConflictClause = function () {
var C = this._C;
var numTerms = C._getConflictClauseSize();
@@ -110,7 +115,7 @@ MiniSat.prototype.getConflictClause = function () {
var terms = [];
for (var i = 0; i < numTerms; i++) {
var t = C.getValue(clausePtr + i*4, 'i32');
var v = (t >>> 1) + 1;
var v = (t >>> 1);
var s = (t & 1) ? -1 : 1;
terms[i] = v * s;
}