Skip to content

Commit

Permalink
Improve way to disable "check" in Logic
Browse files Browse the repository at this point in the history 
for speed
  • Loading branch information
@dgreensp
dgreensp committed Jan 28, 2015
1 parent 712856b commit 2de487f
Show file tree
Hide file tree
Showing 2 changed files with 139 additions and 118 deletions.
18 changes: 13 additions & 5 deletions packages/logic-solver/logic.js
View file
Original file line number Diff line number Diff line change
@@ -1,12 +1,16 @@
Logic = {};

// Disabling type checks speeds things up a LOT (several times faster).
// Type checks are disabled when `_check` is set to a no-op function
// instead of `check`.
_check = check;
// defaults to true. Returns the old value.
Logic._setAssertionsEnabled = function (areThey) {
var oldAreThey = (_check === check);
_check = areThey ? check : function () {};
return oldAreThey;
Logic._disablingTypeChecks = function (f) {
try {
_check = function () {};
return f();
} finally {
_check = check;
}
};

Logic._MiniSat = MiniSat; // Expose for testing and poking around
Expand Down Expand Up @@ -489,6 +493,7 @@ Logic.or = function (/*formulaOrArray, ...*/) {
if (args.length === 0) {
return Logic.FALSE;
} else if (args.length === 1) {
_check(args[0], Logic.FormulaOrTerm);
return args[0];
} else {
return new Logic.OrFormula(args);
Expand Down Expand Up @@ -530,6 +535,7 @@ Logic.and = function (/*formulaOrArray, ...*/) {
if (args.length === 0) {
return Logic.TRUE;
} else if (args.length === 1) {
_check(args[0], Logic.FormulaOrTerm);
return args[0];
} else {
return new Logic.AndFormula(args);
Expand Down Expand Up @@ -572,6 +578,7 @@ Logic.xor = function (/*formulaOrArray, ...*/) {
if (args.length === 0) {
return Logic.FALSE;
} else if (args.length === 1) {
_check(args[0], Logic.FormulaOrTerm);
return args[0];
} else {
return new Logic.XorFormula(args);
Expand Down Expand Up @@ -735,6 +742,7 @@ Logic.exactlyOne = function (/*formulaOrArray, ...*/) {
if (args.length === 0) {
return Logic.FALSE;
} else if (args.length === 1) {
_check(args[0], Logic.FormulaOrTerm);
return args[0];
} else {
return new Logic.ExactlyOneFormula(args);
Expand Down
239 changes: 126 additions & 113 deletions packages/logic-solver/logic_tests.js
View file
Original file line number Diff line number Diff line change
Expand Up @@ -1254,60 +1254,59 @@ 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) {
// one per row x, one per column x
solver.require(Logic.exactlyOne(_.map(nums, function (y) {
return boardSquare(x, y);
})));
solver.require(Logic.exactlyOne(_.map(nums, function (y) {
return boardSquare(y, x);
})));
});
Logic._disablingTypeChecks(function () {

var solver = new Logic.Solver;
var nums = _.range(1, 9); // 1..8
_.each(nums, function (x) {
// one per row x, one per column x
solver.require(Logic.exactlyOne(_.map(nums, function (y) {
return boardSquare(x, y);
})));
solver.require(Logic.exactlyOne(_.map(nums, 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));
// 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));
}
solver.require(Logic.atMostOne(vars));
}
}

var solution = solver.solve().getTrueVars();
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(_.uniq(_.map(solution, 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(1); });
// queens' row/col have eight different sums, eight different differences
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) - Number(queen.charAt(1));
});
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) + Number(queen.charAt(1));
// 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(_.uniq(_.map(solution, 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(1); });
// queens' row/col have eight different sums, eight different differences
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) - Number(queen.charAt(1));
});
assertEightDifferent(function (queen) {
return Number(queen.charAt(0)) + Number(queen.charAt(1));
});
});

Logic._setAssertionsEnabled(oldAssertionsEnabled);
});


Expand All @@ -1316,80 +1315,80 @@ Tinytest.add("logic-solver - Sudoku", function (test) {
return row + "," + col + "=" + value;
};

var oldAssertionsEnabled = Logic._setAssertionsEnabled(false);
//console.profile('sudoku');
Logic._disablingTypeChecks(function () {
//console.profile('sudoku');

var solver = new Logic.Solver();
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));
// 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));
}
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));
// 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 = _.map(solution, 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'));

Logic._setAssertionsEnabled(oldAssertionsEnabled);
//console.profileEnd('sudoku');
var solution = solver.solve().getTrueVars();
var solutionString = _.map(solution, 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) {
Expand Down Expand Up @@ -1670,3 +1669,17 @@ Tinytest.add("logic-solver - maximize", function (test) {
var sol2 = s.maximize(sol, costTerms, costWeights, ws);
test.equal(sol2.getTrueVars(), ["#11", "#2", "#5"]);
});

Tinytest.add("logic-solver - type-checking", function (test) {
// on by default
test.throws(function () {
Logic.or({});
}, function (e) {
return e instanceof Match.Error;
});

// ... but can turn it off (this shouldn't throw)
Logic._disablingTypeChecks(function () {
Logic.or({});
});
});

0 comments on commit 2de487f

Please sign in to comment.