Generated variable names start with $

Not backtick, or nothing
This commit is contained in:
David Greenspan
2014-12-22 19:26:49 -08:00
parent 66d07d40af
commit 0721dfadd2
2 changed files with 18 additions and 18 deletions

View File

@@ -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;

View File

@@ -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"]
]);
});