From f31f9c7bcb89e5511b3e2fbc144ad451c2ef85b2 Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Fri, 26 Dec 2014 06:26:31 -0800
Subject: [PATCH] Improve generation of require/forbid of formula

eg improve require(f);require(f) or require(f) then use f
---
 packages/logic-solver/logic.js       | 25 +++++++--
 packages/logic-solver/logic_tests.js | 76 ++++++++++++++++++++++++++++
 2 files changed, 97 insertions(+), 4 deletions(-)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index a22d6167a7..bdd62bd344 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -266,16 +266,27 @@ Logic.Solver.prototype._requireForbidImpl = function (isRequire, formulas) {
   var self = this;
   check(formulas, [Logic.FormulaOrTerm]);
   var sign = isRequire ? 1 : -1;
-  _.each(_.flatten(arguments), function (f) {
+  _.each(formulas, function (f) {
     if (f instanceof Logic.NotFormula) {
       self._requireForbidImpl(!isRequire, [f.operand]);
     } else if (f instanceof Logic.Formula) {
       var info = self._getFormulaInfo(f);
-      if (info.varNum !== null) {
+      if ((isRequire && info.isRequired) ||
+          (!isRequire && info.isForbidden)) {
+        // do nothing
+      } else if ((isRequire && info.isForbidden) ||
+                 (!isRequire && info.isRequired)) {
+        self._addClause(new Logic.Clause([])); // never satisfied
+      } else if (info.varNum !== null) {
         self._addClause(new Logic.Clause(sign*info.varNum));
       } else {
         self._addClauses(self._callGenerate(isRequire, f));
       }
+      if (isRequire) {
+        info.isRequired = true;
+      } else {
+        info.isForbidden = true;
+      }
     } else if (Match.test(f, Logic.Term)) {
       var t = self.toNumTerm(f);
       if (t === sign*self._T || t === -sign*self._F) {
@@ -346,7 +357,9 @@ Logic.Solver.prototype._getFormulaInfo = function (formula) {
       varName: null,
       varNum: null,
       occursPositively: false,
-      occursNegatively: false
+      occursNegatively: false,
+      isRequired: false,
+      isForbidden: false
     };
   }
   return self._formulaInfo[guid];
@@ -369,7 +382,11 @@ Logic.Solver.prototype._formulaToTerm = function (formula) {
     return Logic.not(self._formulaToTerm(formula.operand));
   } else if (formula instanceof Logic.Formula) {
     var info = this._getFormulaInfo(formula);
-    if (info.varNum === null) {
+    if (info.isRequired) {
+      return self._T;
+    } else if (info.isForbidden) {
+      return self._F;
+    } else if (info.varNum === null) {
       // generate a Solver-local formula name like "or1"
       var type = formula.type;
       if (! this._nextFormulaNumByType[type]) {
diff --git a/packages/logic-solver/logic_tests.js b/packages/logic-solver/logic_tests.js
index 73359d93cf..fbab2dc55d 100644
--- a/packages/logic-solver/logic_tests.js
+++ b/packages/logic-solver/logic_tests.js
@@ -373,3 +373,79 @@ Tinytest.add("logic-solver - Logic.xor", function (test) {
      "-$xor1 v $xor2"]
   ]);
 });
+
+Tinytest.add("logic-solver - require/forbid generation", function (test) {
+  runClauseTests(test, [
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(Logic.or(f, "C"));
+      debugger;
+      s.forbid(f);
+    },
+    ["A v -$and1", "B v -$and1", "$and1 v C", "-A v -B v $and1", "-$and1"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(Logic.or(Logic.not(f), "C"));
+      s.require(f);
+    },
+    ["-A v -B v $and1", "-$and1 v C", "A v -$and1", "B v -$and1", "$and1"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(f);
+      s.require(f);
+    },
+    ["A", "B"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.forbid(f);
+      s.forbid(f);
+    },
+    ["-A v -B"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(f);
+      s.forbid(f);
+      s.forbid(f);
+    },
+    ["A", "B", ""],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.forbid(f);
+      s.require(f);
+      s.require(f);
+    },
+    ["-A v -B", ""],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(f);
+      s.require(Logic.or(f, "C"));
+    },
+    ["$T", "A", "B", "$T v C"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(f);
+      s.require(Logic.or(Logic.not(f), "C"));
+    },
+    ["$T", "A", "B", "-$T v C"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.forbid(f);
+      s.require(Logic.or(Logic.not(f), "C"));
+    },
+    ["-$F", "-A v -B", "-$F v C"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.require(f);
+      s.forbid(f);
+      s.require(Logic.or(f, "C"));
+    },
+    ["$T", "A", "B", "", "$T v C"],
+    function (s) {
+      var f = Logic.and("A", "B");
+      s.forbid(f);
+      s.require(f);
+      s.require(Logic.or(f, "C"));
+    },
+    ["$T", "-A v -B", "", "$T v C"]
+  ]);
+});