From 3281ac7d9e86fbcfb51cfc985c18249ffed81ac7 Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Tue, 23 Dec 2014 14:32:46 -0800
Subject: [PATCH] Add Logic.and; fix formula generation
MIME-Version: 1.0
Content-Type: text/plain; charset=UTF-8
Content-Transfer-Encoding: 8bit

We weren’t generating formulas when they were used by other formulas.  When we generate a clause for a formula, like “A v B v -$or1”, we need to only suppress formula generation for the -$or1 term, not the entire clause.  This matters when A and B are formula vars (eg “$and1 v $and2 v -$or1”).
---
 packages/logic-solver/logic.js       | 150 +++++++++++++++++----------
 packages/logic-solver/logic_tests.js |  51 +++++++++
 2 files changed, 147 insertions(+), 54 deletions(-)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index 4476ce961e..ee1f06ed17 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -46,8 +46,13 @@ Logic.TRUE = "$T";
 Logic.FALSE = "$F";
 
 Logic.Formula = function () {};
-// Returns a list of clauses that together require the
-// Formula to be true.  (Does not add them to the solver.)
+// Returns a list of Clauses that together require the Formula to be
+// true.  A single Clause may also be returned.  The implementation
+// should call makeClause(formulaOrArray, ...)  on the Formulas and
+// Terms of the clause in order to construct Clause objects to return.
+// makeClause is provided by the caller (the Solver) and returns a
+// Clause object that uses variable numbers specific to that Solver
+// instance.
 Logic.Formula.prototype._genTrue = function (makeClause) { return []; };
 // Returns a list of clauses that together require the
 // Formula to be false.
@@ -184,64 +189,69 @@ Logic.Solver.prototype.toNameTerm = function (t) {
   }
 };
 
-Logic.Solver.prototype._addClause = function (cls, _internal) {
+Logic.Solver.prototype._addClause = function (cls, _extraTerms) {
   var self = this;
 
   check(cls, Logic.Clause);
 
-  if (! _internal) {
-    var usedF = false;
-    var usedT = false;
-
-    _.each(cls.terms, function (t) {
-      var v = (t < 0) ? -t : t;
-      if (v === 1) {
-        usedF = true;
-      } else if (v === 2) {
-        usedT = true;
-      } else if (v < 1 || v >= self._num2name.length) {
-        throw new Error("Bad variable number: " + v);
-      } else if (_.has(self._ungeneratedFormulas, v)) {
-        // using a Formula's var, maybe have to generate clauses
-        // for the Formula
-        var formula = self._ungeneratedFormulas[v];
-        var info = self._getFormulaInfo(formula);
-        var positive = t > 0;
-        if (positive && ! info.occursPositively) {
-          // generate clauses for the formula.
-          // Eg, if we use variable `X` which represents the formula
-          // `A v B`, add the clause `A v B v -X`.
-          info.occursPositively = true;
-          var clauses = formula._genTrue(_.bind(self._makeClause, self));
-          self._addClauses(_.map(clauses, function (clause) {
-            return clause.append(-v);
-          }), true);
-        } else if ((! positive) && ! info.occursNegatively) {
-          // Eg, if we have the term `-X` where `X` represents the
-          // formula `A v B`, add the clauses `-A v X` and `-B v X`.
-          info.occursNegatively = true;
-          var clauses = formula._genFalse(_.bind(self._makeClause, self));
-          self._addClauses(_.map(clauses, function (clause) {
-            return clause.append(v);
-          }), true);
-        }
-        if (info.occursPositively && info.occursNegatively) {
-          delete self._ungeneratedFormulas[v];
-        }
-      }
-    });
-
-    this._F_used = (this._F_used || usedF);
-    this._T_used = (this._T_used || usedT);
+  var extraTerms = null;
+  if (_extraTerms) {
+    extraTerms = _extraTerms;
+    check(extraTerms, [Logic.Term]);
   }
 
+  var usedF = false;
+  var usedT = false;
+
+  var numRealTerms = cls.terms.length;
+  if (extraTerms) {
+    cls = cls.append(extraTerms);
+  }
+
+  _.each(cls.terms, function (t, i) {
+    var v = (t < 0) ? -t : t;
+    if (v === 1) {
+      usedF = true;
+    } else if (v === 2) {
+      usedT = true;
+    } else if (v < 1 || v >= self._num2name.length) {
+      throw new Error("Bad variable number: " + v);
+    } else if ((i < numRealTerms) && _.has(self._ungeneratedFormulas, v)) {
+      // using a Formula's var; maybe have to generate clauses
+      // for the Formula
+      var formula = self._ungeneratedFormulas[v];
+      var info = self._getFormulaInfo(formula);
+      var positive = t > 0;
+      if (positive && ! info.occursPositively) {
+        // generate clauses for the formula.
+        // Eg, if we use variable `X` which represents the formula
+        // `A v B`, add the clause `A v B v -X`.
+        info.occursPositively = true;
+        var clauses = self._callGenTrue(formula);
+        self._addClauses(clauses, [-v]);
+      } else if ((! positive) && ! info.occursNegatively) {
+        // Eg, if we have the term `-X` where `X` represents the
+        // formula `A v B`, add the clauses `-A v X` and `-B v X`.
+        info.occursNegatively = true;
+        var clauses = self._callGenFalse(formula);
+        self._addClauses(clauses, [v]);
+      }
+      if (info.occursPositively && info.occursNegatively) {
+        delete self._ungeneratedFormulas[v];
+      }
+    }
+  });
+
+  this._F_used = (this._F_used || usedF);
+  this._T_used = (this._T_used || usedT);
+
   this.clauses.push(cls);
 };
 
-Logic.Solver.prototype._addClauses = function (array, _internal) {
+Logic.Solver.prototype._addClauses = function (array, _extraTerms) {
   check(array, [Logic.Clause]);
   var self = this;
-  _.each(array, function (cls) { self._addClause(cls, _internal); });
+  _.each(array, function (cls) { self._addClause(cls, _extraTerms); });
 };
 
 Logic.Solver.prototype.require = function (formulaOrArray/*, ...*/) {
@@ -256,7 +266,7 @@ Logic.Solver.prototype.require = function (formulaOrArray/*, ...*/) {
       if (info.varNum !== null) {
         self._addClause(new Logic.Clause(info.varNum));
       } else {
-        self._addClauses(f._genTrue(_.bind(self._makeClause, self)));
+        self._addClauses(self._callGenTrue(f));
       }
     } else if (Match.test(f, Logic.Term)) {
       self._addClause(new Logic.Clause(self.toNumTerm(f)));
@@ -276,7 +286,7 @@ Logic.Solver.prototype.forbid = function (formulaOrArray/*, ...*/) {
       if (info.varNum !== null) {
         self._addClause(new Logic.Clause(-info.varNum));
       } else {
-        self._addClauses(f._genFalse(_.bind(self._makeClause, self)));
+        self._addClauses(self._callGenFalse(f));
       }
     } else if (Match.test(f, Logic.Term)) {
       self._addClause(new Logic.Clause(-self.toNumTerm(f)));
@@ -284,6 +294,16 @@ Logic.Solver.prototype.forbid = function (formulaOrArray/*, ...*/) {
   });
 };
 
+// Helpers for invoking _genTrue and _genFalse on a Formula.
+Logic.Solver.prototype._callGenTrue = function (formula) {
+  var ret = formula._genTrue(_.bind(this._makeClause, this));
+  return _.isArray(ret) ? ret : [ret];
+};
+Logic.Solver.prototype._callGenFalse = function (formula) {
+  var ret = formula._genFalse(_.bind(this._makeClause, this));
+  return _.isArray(ret) ? ret : [ret];
+};
+
 // Get clause data as an array of arrays of integers,
 // for testing and debugging purposes.
 Logic.Solver.prototype._clauseData = function () {
@@ -405,12 +425,12 @@ Logic.OrFormula = function (operands) {
 Logic._defineFormula(Logic.OrFormula, 'or', {
   _genTrue: function (makeClause) {
     // eg A v B v C
-    return [makeClause(this.operands)];
+    return makeClause(this.operands);
   },
   _genFalse: function (makeClause) {
     // eg -A; -B; -C
-    return _.map(this.operands, function (formula) {
-      return makeClause(Logic.not(formula));
+    return _.map(this.operands, function (o) {
+      return makeClause(Logic.not(o));
     });
   }
 });
@@ -428,3 +448,25 @@ Logic._defineFormula(Logic.NotFormula, 'not', {
     throw new Error("'not' is special and doesn't gen");
   }
 });
+
+Logic.and = function (termOrArray/*, ...*/) {
+  return new Logic.AndFormula(_.flatten(arguments));
+};
+
+Logic.AndFormula = function (operands) {
+  check(operands, [Logic.FormulaOrTerm]);
+  this.operands = operands;
+};
+
+Logic._defineFormula(Logic.AndFormula, 'and', {
+  _genTrue: function (makeClause) {
+    // eg A; B; C
+    return _.map(this.operands, function (o) {
+      return makeClause(o);
+    });
+  },
+  _genFalse: function (makeClause) {
+    // eg -A v -B v -C
+    return makeClause(_.map(this.operands, Logic.not));
+  }
+});
diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js
index 526ef7f84c..7563f8bb83 100644
--- a/packages/logic-solver/logic_tests.js
+++ b/packages/logic-solver/logic_tests.js
@@ -223,3 +223,54 @@ Tinytest.add("logic-solver - Require/forbid after formula gen", function (test)
     ["-A v $or1","-B v $or1","-$or1 v C","A v B v -$or1","$or1"]
   ]);
 });
+
+
+Tinytest.add("logic-solver - Logic.and", function (test) {
+  runClauseTests(test, [
+    function (s) {
+      s.require(Logic.and('A', 'B'));
+    },
+    ["A", "B"],
+    function (s) {
+      s.require(Logic.and(['A', 'B']));
+    },
+    ["A", "B"],
+    function (s) {
+      s.require(Logic.and(['A'], ['-B']));
+    },
+    ["A", "-B"],
+    function (s) {
+      s.forbid(Logic.and('A', '-B'));
+    },
+    ["-A v B"],
+    function (s) {
+      s.forbid(Logic.and());
+    },
+    [""],
+    function (s) {
+      s.require(Logic.and());
+    },
+    [],
+    function (s) {
+      s.require(Logic.or(Logic.and(Logic.or("A", "B"),
+                                   Logic.or("-A", "C")),
+                         "-D"));
+    },
+    ["A v B v -$or1",
+     "$or1 v -$and1",
+     "-A v C v -$or2",
+     "$or2 v -$and1",
+     "$and1 v -D"],
+    function (s) {
+      s.require(Logic.or(Logic.not(Logic.and(Logic.or("A", "B"),
+                                             Logic.or("-A", "C"))),
+                         "-D"));
+    },
+    ["-A v $or1",
+     "-B v $or1",
+     "A v $or2",
+     "-C v $or2",
+     "-$or1 v -$or2 v $and1",
+     "-$and1 v -D"]
+  ]);
+});