diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js index 5b26963121..d40f5c25b4 100644 --- a/packages/logic-solver/logic.js +++ b/packages/logic-solver/logic.js @@ -250,8 +250,8 @@ Logic.Solver = function () { self._name2num = {}; // (' '+vname) -> vnum // true and false - var F = self.getVarNum(Logic.NAME_FALSE, true); // 1 - var T = self.getVarNum(Logic.NAME_TRUE, true); // 2 + var F = self.getVarNum(Logic.NAME_FALSE, false, true); // 1 + var T = self.getVarNum(Logic.NAME_TRUE, false, true); // 2 if (F !== Logic.NUM_FALSE || T !== Logic.NUM_TRUE) { throw new Error("Assertion failure: $T and $F have wrong numeric value"); } @@ -278,14 +278,14 @@ Logic.Solver = function () { }; // Get a var number for vname, assigning it a number if it is new. -// Setting "_createInternals" to true grants the ability to create $ variables. -// Setting "_noCreate" to true causes the function to return 0 instead of +// Setting "noCreate" to true causes the function to return 0 instead of // creating a new variable. -Logic.Solver.prototype.getVarNum = function (vname, _createInternals, _noCreate) { +// Setting "_createInternals" to true grants the ability to create $ variables. +Logic.Solver.prototype.getVarNum = function (vname, noCreate, _createInternals) { var key = ' '+vname; if (_.has(this._name2num, key)) { return this._name2num[key]; - } else if (_noCreate) { + } else if (noCreate) { return 0; } else { if (vname.charAt(0) === "$" && ! _createInternals) { @@ -328,7 +328,7 @@ Logic.Solver.prototype.toNumTerm = function (t, noCreate) { t = t.slice(1); not = ! not; } - var n = self.getVarNum(t, false, noCreate); + var n = self.getVarNum(t, noCreate); if (! n) { return 0; // must be the noCreate case } else { @@ -653,7 +653,7 @@ Logic.Solver.prototype._formulaToTerm = function (formula) { } var numForVarName = this._nextFormulaNumByType[type]++; info.varName = "$" + formula.type + numForVarName; - info.varNum = this.getVarNum(info.varName, true); + info.varNum = this.getVarNum(info.varName, false, true); this._ungeneratedFormulas[info.varNum] = formula; } return info.varNum; diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js index a62615c3ee..615374d755 100644 --- a/packages/logic-solver/logic_tests.js +++ b/packages/logic-solver/logic_tests.js @@ -1184,6 +1184,21 @@ Tinytest.add("logic-solver - simple solve", function (test) { 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");