From 0721dfadd2f6ae3348e7bc06bfbf91f0f2236e2e Mon Sep 17 00:00:00 2001
From: David Greenspan <dgreenspan@alum.mit.edu>
Date: Mon, 22 Dec 2014 19:26:49 -0800
Subject: [PATCH] Generated variable names start with $

Not backtick, or nothing
---
 packages/logic-solver/logic.js       | 16 ++++++++--------
 packages/logic-solver/logic_tests.js | 20 ++++++++++----------
 2 files changed, 18 insertions(+), 18 deletions(-)

diff --git a/packages/logic-solver/logic.js b/packages/logic-solver/logic.js
index 7e241719bb..7f57be3c5c 100644
--- a/packages/logic-solver/logic.js
+++ b/packages/logic-solver/logic.js
@@ -42,8 +42,8 @@ Logic.not = function (operand) {
   }
 };
 
-Logic.TRUE = "`T";
-Logic.FALSE = "`F";
+Logic.TRUE = "$T";
+Logic.FALSE = "$F";
 
 Logic.Formula = function () {};
 // Returns a list of clauses that together require the
@@ -82,8 +82,8 @@ 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("$F", true); // 1
+  this._T = this.getVarNum("$T", true); // 2
   this._F_used = false;
   this._T_used = false;
   // (it's important that these clauses are elements 0 and 1
@@ -105,8 +105,8 @@ Logic.Solver.prototype.getVarNum = function (vname, _internal) {
   if (_.has(this._name2num, key)) {
     return this._name2num[key];
   } else {
-    if (vname.charAt(0) === "`" && ! _internal) {
-      throw new Error("Only generated variable names can start with `");
+    if (vname.charAt(0) === "$" && ! _internal) {
+      throw new Error("Only generated variable names can start with $");
     }
     var vnum = this._num2name.length;
     this._name2num[key] = vnum;
@@ -372,8 +372,8 @@ Logic.Solver.prototype._formulaToTerm = function (formula) {
         this._nextFormulaNumByType[type] = 1;
       }
       var numForVarName = this._nextFormulaNumByType[type]++;
-      info.varName = formula.type + numForVarName;
-      info.varNum = this.getVarNum(info.varName);
+      info.varName = "$" + formula.type + numForVarName;
+      info.varNum = this.getVarNum(info.varName, 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 d43e3b85ff..9983ab1708 100644
--- a/packages/logic-solver/logic_tests.js
+++ b/packages/logic-solver/logic_tests.js
@@ -72,18 +72,18 @@ Tinytest.add("logic-solver - bad NumTerms", function (test) {
 
 Tinytest.add("logic-solver - true and false", function (test) {
   runClauseTests(test, [
-    // Clauses that forbid `F and require `T are automatically
+    // Clauses that forbid $F and require $T are automatically
     // generated as the first two clauses.  Using each of them
     // causes the relevant clause to be included in the output.
     function (s) {
       s.require(Logic.not(Logic.TRUE));
     },
-    ["`T", "-`T"],
+    ["$T", "-$T"],
     function (s) {
       s.require(Logic.or(Logic.not(Logic.TRUE),
                          Logic.not(Logic.FALSE)));
     },
-    ["-`F", "`T", "-`T v -`F"]
+    ["-$F", "$T", "-$T v -$F"]
   ]);
 });
 
@@ -140,7 +140,7 @@ Tinytest.add("logic-solver - nested Logic.or", function (test) {
     function (s) {
       s.require(Logic.or(Logic.or("A", "B"), Logic.or("C", "D")));
     },
-    ["A v B v -or1", "C v D v -or2", "or1 v or2"]
+    ["A v B v -$or1", "C v D v -$or2", "$or1 v $or2"]
   ]);
 });
 
@@ -165,7 +165,7 @@ Tinytest.add("logic-solver - Logic.not formula", function (test) {
     function (s) {
       s.require(Logic.or(Logic.not(Logic.or("A", "B")), "C"));
     },
-    ["-A v or1", "-B v or1", "-or1 v C"]
+    ["-A v $or1", "-B v $or1", "-$or1 v C"]
   ]);
 });
 
@@ -174,12 +174,12 @@ Tinytest.add("logic-solver - Require/forbid after formula gen", function (test)
     function (s) {
       // Use a formula in the positive and then require it.  Requiring
       // the formula does not regenerate its clauses, it just requires
-      // the formula's variable (or1).
+      // the formula's variable ($or1).
       var f = Logic.or("A", "B");
       s.require(Logic.or(f, "C"));
       s.require(f);
     },
-    ["A v B v -or1","or1 v C","or1"]
+    ["A v B v -$or1","$or1 v C","$or1"]
   ]);
 
   runClauseTests(test, [
@@ -191,7 +191,7 @@ Tinytest.add("logic-solver - Require/forbid after formula gen", function (test)
       s.require(Logic.or(f, "C"));
       s.forbid(f);
     },
-    ["A v B v -or1","or1 v C","-A v or1","-B v or1","-or1"]
+    ["A v B v -$or1","$or1 v C","-A v $or1","-B v $or1","-$or1"]
   ]);
 
   runClauseTests(test, [
@@ -201,7 +201,7 @@ Tinytest.add("logic-solver - Require/forbid after formula gen", function (test)
       s.require(Logic.or(Logic.not(f), "C"));
       s.forbid(f);
     },
-    ["-A v or1","-B v or1","-or1 v C","-or1"]
+    ["-A v $or1","-B v $or1","-$or1 v C","-$or1"]
   ]);
 
   runClauseTests(test, [
@@ -211,6 +211,6 @@ Tinytest.add("logic-solver - Require/forbid after formula gen", function (test)
       s.require(Logic.or(Logic.not(f), "C"));
       s.require(f);
     },
-    ["-A v or1","-B v or1","-or1 v C","A v B v -or1","or1"]
+    ["-A v $or1","-B v $or1","-$or1 v C","A v B v -$or1","$or1"]
   ]);
 });