From ea4f8c23d27af5171c9c352c07106fe4fff233cc Mon Sep 17 00:00:00 2001 From: Dirk Schumacher Date: Sun, 4 Mar 2018 06:38:14 +0100 Subject: [PATCH] Fix a bug where only positive assumptions were accepted --- index.js | 2 +- package.json | 2 +- test.js | 4 ++-- 3 files changed, 4 insertions(+), 4 deletions(-) diff --git a/index.js b/index.js index 8ba6135..d5bfd4d 100644 --- a/index.js +++ b/index.js @@ -21,7 +21,7 @@ const isValidAssumptions = (assumptions, nvars) => { // TODO: check for duplicates return Array.isArray(assumptions) && assumptions.every(Number.isInteger) && - assumptions.every(x => x >= 1 && x <= nvars) + assumptions.map(Math.abs).every(x => x >= 1 && x <= nvars) } const picosat_sat = (formula, assumptions) => { diff --git a/package.json b/package.json index 3faf441..083a91d 100644 --- a/package.json +++ b/package.json @@ -1,6 +1,6 @@ { "name": "picosat", - "version": "1.0.1", + "version": "1.0.2", "description": "picosat SAT solver", "main": "index.js", "files": [ diff --git a/test.js b/test.js index a06aa46..4defe30 100644 --- a/test.js +++ b/test.js @@ -12,11 +12,11 @@ test("it solves a simple problem", (t) => { test("it supports assumptions", (t) => { const formula = [[1, 2], [-1, 2]] - const assumptions = [1, 2] + const assumptions = [-1, 2] const result = picosat_sat(formula, assumptions) t.equal(result.satisfiable, true) t.equal(result.solution.length, 2) - t.equal(result.solution[0], 1) + t.equal(result.solution[0], -1) t.equal(result.solution[1], 2) t.end() })