From 2d660ab92a79bc285c184a4304545eb517e5bdbb Mon Sep 17 00:00:00 2001 From: David Greenspan Date: Mon, 22 Dec 2014 10:30:04 -0800 Subject: [PATCH] Give clauses a nicer string representation --- packages/logic-solver/logic.js | 88 +++++++++++++++++++++++++--- packages/logic-solver/logic_tests.js | 31 ++++++++-- 2 files changed, 107 insertions(+), 12 deletions(-) diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js index a9f7581cd4..4d31528d8d 100644 --- a/packages/logic-solver/logic.js +++ b/packages/logic-solver/logic.js @@ -25,7 +25,7 @@ Logic.Term = Match.Where(function (x) { // A Term that is represented as a number, not a name. // (Subtype of Term.) -Logic._NTerm = Match.Where(function (x) { +Logic.NTerm = Match.Where(function (x) { check(x, Match.Integer); return (x !== 0); }); @@ -75,8 +75,8 @@ Logic.Formula._genFalse = function (formula, solver) { Logic.Clause = function (termOrArray/*, ...*/) { var terms = _.flatten(arguments); - check(terms, [Logic._NTerm]); - this.terms = terms; // immutable [_NTerm] + check(terms, [Logic.NTerm]); + this.terms = terms; // immutable [NTerm] }; Logic.Solver = function () { @@ -111,19 +111,34 @@ Logic.Solver.prototype.getVarNum = function (vname, _internal) { } }; -// Converts Terms to _NTerms +Logic.Solver.prototype.getVarName = function (vnum) { + var num2name = this._num2name; + if (vnum < 1 || vnum >= num2name.length) { + throw new Error("Bad variable num: " + vnum); + } else { + return num2name[vnum]; + } +}; + +// Converts Terms to NTerms (if they aren't already). This is done +// when a Formula creates Clauses for a Solver, since Clauses require +// NTerms. Takes a Term or an array. For example, [-3, "-foo"] might +// become [-3, -4]. Logic.Solver.prototype._toN = function (t) { var self = this; if (_.isArray(t)) { + check(t, [Logic.Term]); return _.map(t, function (tt) { return self._toN(tt); }); + } else { + check(t, Logic.Term); } if (typeof t === 'number') { return t; - } else if (typeof t === 'string') { + } else { // string var not = false; while (t.charAt(0) === '-') { t = t.slice(1); @@ -131,8 +146,39 @@ Logic.Solver.prototype._toN = function (t) { } var n = self.getVarNum(t); return (not ? -n : n); + } +}; + +// Converts Terms to string form. +Logic.Solver.prototype._toName = function (t) { + var self = this; + + if (_.isArray(t)) { + check(t, [Logic.Term]); + return _.map(t, function (tt) { + return self._toName(tt); + }); } else { - throw new Error("Expected number or string"); + check(t, Logic.Term); + } + + if (typeof t === 'string') { + // canonicalize, removing leading "--" + while (t.slice(0, 2) == '--') { + t = t.slice(2); + } + return t; + } else { // number + var not = false; + if (t < 0) { + not = true; + t = -t; + } + t = self.getVarName(t); + if (not) { + t = '-' + t; + } + return t; } }; @@ -168,6 +214,8 @@ Logic.Solver.prototype.forbid = function (formulaOrArray/*, ...*/) { }); }; +// Get clause data as an array of arrays of integers, +// for testing and debugging purposes. Logic.Solver.prototype._clauseData = function () { var clauses = _.pluck(this.clauses, 'terms'); if (! this._T_used) { @@ -179,6 +227,32 @@ Logic.Solver.prototype._clauseData = function () { return clauses; }; +// Get clause data as an array of human-readable strings, +// for testing and debugging purposes. +// A clause might look like "A v -B" (where "v" represents +// and OR operator). +Logic.Solver.prototype._clauseStrings = function () { + var self = this; + var clauseData = self._clauseData(); + return _.map(clauseData, function (clause) { + return _.map(clause, function (nterm) { + var str = self._toName(nterm); + if (/\s/.test(str)) { + // write name in quotes for readability. we don't bother + // making this string machine-parsable in the general case. + var sign = ''; + if (str.charAt(0) === '-') { + // temporarily remove '-' + sign = '-'; + str = str.slice(1); + } + str = sign + '"' + str + '"'; + } + return str; + }).join(' v '); + }); +}; + Logic.or = function (termOrArray/*, ...*/) { return new Logic.OrFormula(_.flatten(arguments)); }; @@ -192,6 +266,6 @@ Logic.OrFormula.prototype._genTrue = function (solver) { }; Logic.OrFormula.prototype._genFalse = function (solver) { return _.map(this.terms, function (t) { - return [new Logic.Clause(-solver._toN(t))]; + return new Logic.Clause(-solver._toN(t)); }); }; diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js index c0f0d9a3cb..01882b58cb 100644 --- a/packages/logic-solver/logic_tests.js +++ b/packages/logic-solver/logic_tests.js @@ -4,22 +4,43 @@ Tinytest.add("logic-solver - require", function (test) { 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 this canonicalization that is part of _toName + // (though not actually used by _clauseStrings because + // Clauses use numeric Terms). + test.equal(s._toName("-----foo"), "-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 - Logic.Or", function (test) { var s = new Logic.Solver; - s.require(Logic.or('a', 'b')); - test.equal(s._clauseData(), [[3, 4]]); + s.require(Logic.or('A', 'B')); + test.equal(s._clauseStrings(), ["A v B"]); - s.require(Logic.or('-c', 'd', 3)); + s.require(Logic.or('-C', 'D', 3)); test.equal(s._clauseData(), [[3, 4], [-5, 6, 3]]); + test.equal(s._clauseStrings(), ["A v B", "-C v D v A"]); - s.forbid(Logic.or('a', '-b')); - test.equal(s._clauseData(), [[3, 4], [-5, 6, 3], [-3], [4]]); + s.forbid(Logic.or('A', '-B')); + test.equal(s._clauseStrings(), ["A v B", "-C v D v A", + "-A", "B"]); });