From 3ebeb5f0e6eab4e08b5ddd7771a34a257fe1180c Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Wed, 25 Feb 2015 20:14:40 -0800
Subject: [PATCH] Start making changes from Glasser initial review

---
 packages/logic-solver/logic.js | 48 ++++++++++++++++++++++------------
 1 file changed, 31 insertions(+), 17 deletions(-)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index 7bb4af25b5..ceb2f88aa3 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -5,16 +5,19 @@ Logic = {};
 // instead of `check`.
 _check = check;
 Logic._disablingTypeChecks = function (f) {
+  var oldCheck = _check;
   try {
     _check = function () {};
     return f();
   } finally {
-    _check = check;
+    _check = oldCheck;
   }
 };
 
 Logic._MiniSat = MiniSat; // Expose for testing and poking around
 
+////////// Type Declarations
+
 // WholeNumber: a non-negative integer (0 is allowed)
 Logic.WholeNumber = Match.Where(function (x) {
   return Match.test(x, Match.Integer) && x >= 0;
@@ -37,6 +40,11 @@ Logic.NameTerm = Match.Where(function (x) {
 // keep it to either one or zero of them.
 Logic.Term = Match.OneOf(Logic.NameTerm, Logic.NumTerm);
 
+Logic.FormulaOrTerm = Match.OneOf(Logic.Formula, Logic.Term);
+
+////////// End Type Declarations
+
+
 // Takes a Formula or Term, returns a Formula or Term.
 // Unlike other operators, if you give it a Term,
 // you will get a Term back (of the same type, NameTerm
@@ -60,7 +68,19 @@ Logic.not = function (operand) {
 Logic.TRUE = "$T";
 Logic.FALSE = "$F";
 
+// Abstract base class.  Subclasses are created using _defineFormula.
 Logic.Formula = function () {};
+
+Logic._defineFormula = function (constructor, typeName, methods) {
+  _check(constructor, Function);
+  _check(typeName, String);
+  Meteor._inherits(constructor, Logic.Formula);
+  constructor.prototype.type = typeName;
+  if (methods) {
+    _.extend(constructor.prototype, methods);
+  }
+};
+
 // Returns a list of Clauses that together require the Formula to be
 // true, or false (depending on isTrue; both cases must be
 // implemented).  A single Clause may also be returned.  The
@@ -81,8 +101,11 @@ Logic.Formula.prototype.guid = function () {
   return this._guid;
 };
 
-Logic.FormulaOrTerm = Match.OneOf(Logic.Formula, Logic.Term);
-
+// A "clause" is a disjunction of terms, e.g. "A or B or (not C)",
+// which we write "A v B v -C".  Logic.Clause is mainly an internal
+// Solver data structure, which is the final result of formula
+// generation and mapping variable names to numbers, before passing
+// the clauses to MiniSat.
 Logic.Clause = function (/*formulaOrArray, ...*/) {
   var terms = _.flatten(arguments);
   _check(terms, [Logic.NumTerm]);
@@ -100,12 +123,13 @@ Logic.Solver = function () {
   this._name2num = {}; // (' '+vname) -> vnum
 
   // true and false
-  this._F = this.getVarNum("$F", true); // 1
-  this._T = this.getVarNum("$T", true); // 2
+  this._F = this.getVarNum(Logic.FALSE, true); // 1
+  this._T = this.getVarNum(Logic.TRUE, true); // 2
   this._F_used = false;
   this._T_used = false;
-  // (it's important that these clauses are elements 0 and 1
-  // of the clauses array)
+  // It's important that these clauses are elements 0 and 1
+  // of the clauses array, so that they can optionally be stripped
+  // off.  For example, _clauseData takes advantage of this fact.
   this.clauses.push(new Logic.Clause(-this._F));
   this.clauses.push(new Logic.Clause(this._T));
 
@@ -478,16 +502,6 @@ Logic.Solver.prototype._formulaToTerm = function (formula) {
   }
 };
 
-Logic._defineFormula = function (constructor, typeName, methods) {
-  _check(constructor, Function);
-  _check(typeName, String);
-  Meteor._inherits(constructor, Logic.Formula);
-  constructor.prototype.type = typeName;
-  if (methods) {
-    _.extend(constructor.prototype, methods);
-  }
-};
-
 Logic.or = function (/*formulaOrArray, ...*/) {
   var args = _.flatten(arguments);
   if (args.length === 0) {