Improve generation of require/forbid of formula

eg improve require(f);require(f) or require(f) then use f
This commit is contained in:
David Greenspan
2014-12-26 06:26:31 -08:00
parent fdd4d22c8d
commit f31f9c7bcb
2 changed files with 97 additions and 4 deletions

View File

@@ -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]) {

View File

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