/* If you're interested in the source, have a look at index.html?comments=true. */

tc = {
counter : 0,
register : function(constName) {
this[constName] = --this.counter;
},
getName : function(num) {
for (var n in this) {
if (this[n] == num && n != "counter") return n;
}
}
}
Array.prototype.isArray = true;
Array.prototype.toString = function() {
return "["+this.join(",")+"]";
}
Array.prototype.contains = function(element) {
for (var i=0; i<this.length; i++) if (this[i] == element) return true;
return false;
}
Array.prototype.remove = function(element) {
for (var i=0; i<this.length; i++) {
if (this[i] == element) {
while (i+1 < this.length) {
this[i] = this[i+1];
i++;
}
this[i] = null;
this.length -= 1;
break;
}
}
return element;
}
Array.prototype.insert = function(element, index) {
if (this.splice) return this.splice(index, 0, element);
for (var i=this.length; i>this.index; i--) this[i] = this[i-1];
this.length += 1;
this[i] = element;
return [element];
}
Array.prototype.copy = function() {
var result = [];
for (var i=0; i<this.length; i++) result[i] = this[i];
return result;
}
Array.prototype.copyDeep = function() {
var result = [];
for (var i=0; i<this.length; i++) {
if (this[i].isArray) result[i] = this[i].copyDeep();
else result[i] = this[i];
}
return result;
}
Array.prototype.negate = function() {
return [tc.NEGATION, this];
}
Array.prototype.substitute = function(origTerm, newTerm, shallow) {
if (this[0] < 0) {
if (this.length == 2) {
this[1].substitute(origTerm, newTerm, shallow);
return this;
}
if (!this[1].isArray) {
if (this[1] != origTerm) this[2].substitute(origTerm, newTerm, shallow);
return this;
}
this[1].substitute(origTerm, newTerm, shallow);
this[2].substitute(origTerm, newTerm, shallow);
return this;
}
for (var i=0; i<this.length; i++) {
if (this[i].isArray) {
if (this[i].equals(origTerm)) this[i] = newTerm;
else if (this[i][0] % 3 != 2 || !shallow) this[i].substitute(origTerm, newTerm, shallow);
}
else if (this[i] == origTerm) this[i] = newTerm;
}
return this;
}
Array.prototype.unify = function(formula) {
if (this.length != 2) return false;
if (this[0] != formula[0]) return false;
if (this[0] == tc.NEGATION) return this[1].unify(formula[1]);
if (this[1].length != formula[1].length) return false;
var unifier = [];
var terms1 = this[1].copyDeep();
var terms2 = formula[1].copyDeep();
var t1, t2;
while (t1 = terms1.shift(), t2 = terms2.shift()) {
if (t1 == t2) {
continue;
}
if (t1.isArray && t2.isArray) {
if (t1[0] != t2[0]) return false;
for (var i=1; i<t1.length; i++) {
terms1.push(t1[i]);
terms2.push(t2[i]);
}
continue;
}
if (t1 % 3 != 0 && t2 % 3 != 0) {
return false;
}
if (t1 % 3 != 0) {
var temp = t1; t1 = t2; t2 = temp;
}
if (t2.isArray) {
var terms, termss = [t2];
while (terms = termss.shift()) {
for (var i=0; i<terms.length; i++) {
if (terms[i].isArray) termss.push(terms[i]);
else if (terms[i] == t1) return false;
}
}
}
var terms, termss = [unifier, terms1, terms2];
while (terms = termss.shift()) {
for (var i=0; i<terms.length; i++) {
if (terms[i].isArray) termss.push(terms[i]);
else if (terms[i] == t1) terms[i] = t2;
}
}
unifier.push(t1); unifier.push(t2);
}
return unifier;
}
Array.prototype.normalize = function() {
switch (this[0]) {
case tc.CONJUNCTION : {
var sub1 = this[1].normalize();
var sub2 = this[2].normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.CONJUNCTION, sub1, sub2] : [tc.CONJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity * sub2.__complexity;
return res;
}
case tc.DISJUNCTION : {
var sub1 = this[1].normalize();
var sub2 = this[2].normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.DISJUNCTION, sub1, sub2] : [tc.DISJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity + sub2.__complexity;
return res;
}
case tc.IMPLICATION : {
var sub1 = this[1].negate().normalize();
var sub2 = this[2].normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.DISJUNCTION, sub1, sub2] : [tc.DISJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity + sub2.__complexity;
return res;
}
case tc.BIIMPLICATION : {
var sub1 = [tc.CONJUNCTION, this[1], this[2]].normalize();
var sub2 = [tc.CONJUNCTION, this[1].negate(), this[2].negate()].normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.DISJUNCTION, sub1, sub2] : [tc.DISJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity + sub2.__complexity;
return res;
}
case tc.UNIVERSAL : case tc.EXISTENTIAL : {
var sub1 = this[2].normalize();
var res = [this[0], this[1], sub1];
res.__complexity = sub1.__complexity;
return res;
}
case tc.NEGATION : {
switch (this[1][0]) {
case tc.CONJUNCTION : {
var sub1 = this[1][1].negate().normalize();
var sub2 = this[1][2].negate().normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.DISJUNCTION, sub1, sub2] : [tc.DISJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity + sub2.__complexity;
return res;
}
case tc.DISJUNCTION : {
var sub1 = this[1][1].negate().normalize();
var sub2 = this[1][2].negate().normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.CONJUNCTION, sub1, sub2] : [tc.CONJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity * sub2.__complexity;
return res;
}
case tc.IMPLICATION : {
var sub1 = this[1][1].normalize();
var sub2 = this[1][2].negate().normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.CONJUNCTION, sub1, sub2] : [tc.CONJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity * sub2.__complexity;
return res;
}
case tc.BIIMPLICATION : {
var sub1 = [tc.CONJUNCTION, this[1][1], this[1][2].negate()].normalize();
var sub2 = [tc.CONJUNCTION, this[1][1].negate(), this[1][2]].normalize();
var res = (sub1.__complexity <= sub2.__complexity) ? [tc.DISJUNCTION, sub1, sub2] : [tc.DISJUNCTION, sub2, sub1];
res.__complexity = sub1.__complexity + sub2.__complexity;
return res;
}
case tc.UNIVERSAL : case tc.EXISTENTIAL : {
var sub = this[1][2].negate().normalize();
var res = [(this[1][0] == tc.UNIVERSAL) ? tc.EXISTENTIAL : tc.UNIVERSAL, this[1][1], sub];
res.__complexity = sub.__complexity;
return res;
}
case tc.NEGATION : {
return this[1][1].normalize();
}
}
}
default : {
this.__complexity = 1;
return this;
}
}
}
Array.prototype.getFreeVariables = function() {
var result = [];
this.__boundVars = [];
var fla, flas = [this];
while ((fla = flas.shift())) {
if (fla.length == 3) {
if (!fla[1].isArray) {
fla[2].__boundVars = fla.__boundVars;
fla[2].__boundVars.push(fla[1]);
flas.push(fla[2]);
}
else {
flas.push(fla[1]);
flas.push(fla[2]);
}
}
else {
if (fla[0] == tc.NEGATION) flas.push(fla[1]);
else {
var terms, termss = [fla[1]];
while ((terms = termss.shift())) {
for (var i=0; i<terms.length; i++) {
if (terms[i].isArray) termss.push(terms[i]);
else if (term % 3 == 0 && !fla.__boundVars.contains(terms[i]) && !result.contains(terms[i])) result.push(terms[i]);
}
}
}
}
delete fla.__boundVars;
}
return result;
}
Array.prototype.getBoundVariables = function() {
var result = [];
var fla, flas = [this];
while ((fla = flas.shift())) {
if (fla.length == 3) {
if (!fla[1].isArray) {
if (!result.contains(fla[1])) result.push(fla[1]);
flas.push(fla[2]);
continue;
}
flas.push(fla[1]);
flas.push(fla[2]);
continue;
}
if (fla[0] == tc.NEGATION) flas.push(fla[1]);
}
return result;
}
Array.prototype.getConstants = function(withArity) {
var result = [], resultWithArity = [];
var fla, flas = [this];
while ((fla = flas.shift())) {
if (fla.length == 3) {
if (!fla[1].isArray) {
flas.push(fla[2]);
continue;
}
flas.push(fla[1]);
flas.push(fla[2]);
continue;
}
if (fla[0] == tc.NEGATION) {
flas.push(fla[1]);
continue;
}
var term, terms = fla[1].copyDeep();
while ((term = terms.shift())) {
if (term.isArray) {
for (var i=1; i<term.length; i++) terms.push(term[i]);
if (result.contains(term[0])) continue;
result.push(term[0]);
if (withArity) resultWithArity.push({ constant : term[0], arity : term.length-1 });
}
else if (term % 3 == 2 && !result.contains(term)) {
result.push(term);
if (withArity) resultWithArity.push({ constant : term, arity : 0 });
}
}
}
return withArity ? resultWithArity : result;
}
Array.prototype.getPredicates = function(withArity) {
var result = [], resultWithArity = [];
var fla, flas = [this];
while ((fla = flas.shift())) {
if (fla.length == 3) {
if (!fla[1].isArray) {
flas.push(fla[2]);
continue;
}
flas.push(fla[1]);
flas.push(fla[2]);
continue;
}
if (fla[0] == tc.NEGATION) {
flas.push(fla[1]);
continue;
}
if (!result.contains(fla[0])) {
result.push(fla[0]);
if (withArity) resultWithArity.push({ predicate : fla[0], arity : fla[1].length });
}
}
return withArity ? resultWithArity : result;
}
Array.prototype.equals = function(formula) {
if (this.length != formula.length) return false;
for (var i=0; i<this.length; i++) {
if (this[i].isArray) {
if (!formula[i].isArray) return false;
if (!this[i].equals(formula[i])) return false;
}
else if (this[i] != formula[i]) return false;
}
return true;
}
tc.register("PREDICATE");
tc.register("CONSTANT");
tc.register("VARIABLE");
tc.register("NEGATION");
tc.register("CONJUNCTION");
tc.register("DISJUNCTION");
tc.register("IMPLICATION");
tc.register("BIIMPLICATION");
tc.register("UNIVERSAL");
tc.register("EXISTENTIAL");
function Translator() {
this.logSymbols = [];
this.logSymbols[tc.NEGATION]      = "<img src='neg.png' alt='\\neg' align='bottom'>";
this.logSymbols[tc.CONJUNCTION]   = "<img src='wedge.png' alt='\\land' align='bottom'>";
this.logSymbols[tc.DISJUNCTION]   = "<img src='vee.png' alt='\\lor' align='bottom'>";
this.logSymbols[tc.IMPLICATION]   = "<img src='to.png' alt='\\to' align='bottom'>";
this.logSymbols[tc.BIIMPLICATION] = "<img src='leftrightarrow.png' alt='\\leftrightarrow' align='bottom'>";
this.logSymbols[tc.UNIVERSAL]     = "<img src='forall.png' alt='\\forall' align='bottom'>";
this.logSymbols[tc.EXISTENTIAL]   = "<img src='exists.png' alt='\\exists' align='bottom'>";
this.nonlogSymbols = [];
this.nonlogSymbols[tc.VARIABLE]  = ["x","y","z","w","u","t","s"];
this.nonlogSymbols[tc.CONSTANT]  = ["a","b","c","d","e"];
this.nonlogSymbols[tc.PREDICATE] = ["P","Q","R","S","A","B","C","D","E"];
this.error = "";
var html2symMap;
var sym2htmlMap;
var arities = [];
var translator = this;
this.init = function() {
this.error = "";
html2symMap = {};
sym2htmlMap = {};
arities = [];
}
this.latex2fla = function(str) {
var boundVars = arguments[1] || [];
str = str.replace(/[{}]/g, "");
str = str.replace(/\\\s/g, "")
str = str.replace(/\s/g, "");
str = str.replace(/\\/g, "%");
str = str.replace(/%to/g, "%rightarrow");
str = str.replace(/%lor/g, "%vee");
str = str.replace(/%land/g, "%wedge");
str = str.replace(/%lnot/g, "%neg");
var nonlogical = /[^\d\(\),%]\d*/g;                                nonlogical.lastIndex = 0;
var reTest = /%wedge|%vee|%rightarrow|%leftrightarrow/.test(str);
if (reTest) {
var subStringsInBrackets = [];
var bracketDepth = 0;
var storingAtIndex = -1;
var nstr = "";
for (var i=0; i<str.length; i++) {
if (str.charAt(i) == "(") {
bracketDepth++;
if (bracketDepth == 1) {
storingAtIndex = subStringsInBrackets.length;
subStringsInBrackets[storingAtIndex] = "";
nstr += "%" + storingAtIndex;
}
}
if (storingAtIndex == -1) nstr += str.charAt(i);
else subStringsInBrackets[storingAtIndex] += str.charAt(i);
if (str.charAt(i) == ")") {
bracketDepth--;
if (bracketDepth == 0) storingAtIndex = -1;
}
}
reTest = nstr.match(/%leftrightarrow/) || nstr.match(/%rightarrow/) || nstr.match(/%vee/) || nstr.match(/%wedge/);
if (reTest) {
var result = [];
switch (reTest[0]) {
case "%leftrightarrow" : result[0] = tc.BIIMPLICATION; break;
case "%rightarrow" : result[0] = tc.IMPLICATION; break;
case "%vee" : result[0] = tc.DISJUNCTION; break;
case "%wedge" : result[0] = tc.CONJUNCTION; break;
}
nstr = nstr.replace(reTest[0], "%split");
for (var i=0; i<subStringsInBrackets.length; i++) {
nstr = nstr.replace("%"+i, subStringsInBrackets[i]);
}
var subFormulas = nstr.split("%split");
if (!subFormulas[1]) return exit("argument missing for operator "+reTest[0]+" in "+str);
result.push(this.latex2fla(subFormulas[0], boundVars));
result.push(this.latex2fla(subFormulas[1], boundVars));
return this.error ? null : result;
}
}
if (str.indexOf("%neg") == 0) {
var result = [tc.NEGATION, this.latex2fla(str.substr(4), boundVars)];
return this.error ? null : result;
}
reTest = /(%forall|%exists)([^\d\(\),%]\d*)/.exec(str);
if (reTest && reTest.index == 0) {
var result = [];
result[0] = (reTest[1] == "%forall") ? tc.UNIVERSAL : tc.EXISTENTIAL;
if (html2symMap[reTest[2]] && this.getHtmlType(reTest[2]) != tc.VARIABLE) {
return exit(reTest[2] + " can't be used both as variable and as " + (this.getHtmlType(reTest[2]) == tc.CONSTANT ? "constant" : "predicate"));
}
result[1] = this.html2sym(reTest[2], tc.VARIABLE);
if (!str.substr(reTest[0].length)) return exit("There is nothing in the scope of "+str);
boundVars.push(reTest[2]);
result[2] = this.latex2fla(str.substr(reTest[0].length), boundVars);
return this.error? null : result;
}
reTest = /[^\d\(\),%]\d*/.exec(str);
if (reTest && reTest.index == 0) {
var result = [];
if (html2symMap[reTest[0]] && this.getHtmlType(reTest[0]) != tc.PREDICATE) {
return exit(reTest[0] + " can't be used both as predicate and as " + (this.getHtmlType(reTest[0]) == tc.CONSTANT ? "constant" : "variable"));
}
result[0] = this.html2sym(reTest[0], tc.PREDICATE);
var termstr = str.substr(reTest.length);
result[1] = (termstr == '') ? [] : (parseTexTerms(termstr, boundVars) || []);
if (arities[result[0]] !== undefined && arities[result[0]] != result[1].length) return exit("Please don't use " + reTest[0] + "with varying arity. That confuses me.");
arities[result[0]] = result[1].length;
return this.error? null : result;
}
if (str.match(/^\((.*)\)$/)) {
return this.latex2fla(str.replace(/^\((.*)\)$/, "$1"), boundVars);
}
exit("Parse Error.\n'" + str + "' is not a well-formed formula.");
}
this.fla2html = function(formula) {
try {
if (formula.length == 3) {
if (!formula[1].isArray) {
var str = this.logSymbols[formula[0]];
str += this.sym2html(formula[1]);
str += this.fla2html(formula[2]);
return str;
}
var str = "(";
str += this.fla2html(formula[1]);
str += this.logSymbols[formula[0]];
str += this.fla2html(formula[2]);
str += ")";
return str;
}
if (formula[0] == tc.NEGATION) {
return this.logSymbols[tc.NEGATION] + this.fla2html(formula[1]);
}
var str = this.sym2html(formula[0]);
for (var i=0; i<formula[1].length; i++) str += this.term2html(formula[1][i]);
return str;
}
catch(e) {
return "?";
}
}
this.term2html = function(term) {
if (!term.isArray) return this.sym2html(term);
var args = [];
for (var i=1; i<term.length; i++) {
args.push(term[i].isArray ? this.term2html(term[i]) : this.sym2html(term[i]));
}
return this.sym2html(term[0]) + "(" + args.join(",") + ")";
}
this.sym2html = function(internal) {
if (sym2htmlMap[internal]) return sym2htmlMap[internal];
var type = this.getType(internal);
if (!type) return null;
var readable = getNewSymbol(type);
html2symMap[readable] = internal;
sym2htmlMap[internal] = readable;
return readable;
}
this.html2sym = function(readable, type) {
if (html2symMap[readable]) return html2symMap[readable];
var internal = (type == tc.PREDICATE) ?  4 :
(type == tc.CONSTANT) ? 2 :
(type == tc.VARIABLE) ? 3 :
exit("unknown type: "+type);
while (sym2htmlMap[internal]) internal += 3;
html2symMap[readable] = internal;
sym2htmlMap[internal] = readable;
return internal;
}
this.getType = function(symbol) {
return (symbol % 3 == 1) ? tc.PREDICATE : (symbol % 3 == 2) ? tc.CONSTANT : tc.VARIABLE;
}
this.getHtmlType = function(symbol) {
symbol = html2symMap[symbol];
if (!symbol) return null;
return (symbol % 3 == 1) ? tc.PREDICATE : (symbol % 3 == 2) ? tc.CONSTANT : tc.VARIABLE;
}
function getNewSymbol(type) {
for (var i=0; i<translator.nonlogSymbols[type].length; i++) {
if (!html2symMap[translator.nonlogSymbols[type][i]]) return translator.nonlogSymbols[type][i];
}
var i=2;
while (html2symMap[translator.nonlogSymbols[type][0]+i]) i++;
return translator.nonlogSymbols[type][0]+i;
}
function parseTexTerms(str, boundVars) {
var nonlogical = /[^\(\),%]\d*/g;
var result = [];
str = str.replace(/^\((.+)\)$/, "$1");
do {
var nextTerm;
nonlogical.lastIndex = 0;
var reTest = nonlogical.exec(str);
if (!reTest || reTest.index != 0) return exit("I expected a (sequence of) term(s) instead of '" + str + "'");
if (translator.getHtmlType(reTest[0]) == tc.VARIABLE) {
if (!boundVars.contains(reTest[0])) return exit("Please don't use " + reTest[0] + " both as variable and as constant. That confuses me.");
nextTerm = translator.html2sym(reTest[0], tc.VARIABLE);
}
else if (translator.getHtmlType(reTest[0]) == tc.PREDICATE) return exit(reTest[0] + " can't be used both as individual constant and as predicate.");
else nextTerm = translator.html2sym(reTest[0], tc.CONSTANT);
str = str.substr(reTest[0].length);
if (str.indexOf("(") == 0) {
var args = "", openBrackets = 0, spos = 0;
do {
args += str.charAt(spos);
if (str.charAt(spos) == "(") openBrackets++;
else if (str.charAt(spos) == ")") openBrackets--;
spos++;
} while (openBrackets && spos < str.length);
nextTerm = [nextTerm].concat(parseTexTerms(args, boundVars));
if (arities[reTest[0]] !== undefined && arities[reTest[0]] != nextTerm.length-1) return exit("Please don't use " + reTest[0] + " with varying arity. That confuses me.");
arities[reTest[0]] = nextTerm.length-1;
str = str.substr(args.length);
}
else {
if (arities[reTest[0]] !== undefined && arities[reTest[0]] != 0) return exit("Please don't use " + reTest[0] + " with varying arity. That confuses me.");
arities[reTest[0]] = 0;
}
result.push(nextTerm);
if (str.indexOf(",") == 0) str = str.substr(1);
} while (str.length > 0);
return result;
}
function exit(str) {
if (translator.error) return;
translator.error = str.replace(/%/g,"\\");
}
}
translator = new Translator();
tc.register("LITERAL");
tc.register("ALPHA");
tc.register("DELTA");
tc.register("BETA");
tc.register("GAMMA");
prover = {
fastMode : false,
nodeLimitFactor : 4,
start : function(formula) {
this.formula = formula;
this.depthLimit = 1;
this.limitReached = false;
this.steps = 0;
this.alternatives = [];
this.tree = new Tree(formula);
this.modelFinder = new ModelFinder(formula);
this.counterModel = null;
this.nextStep();
},
stop : function() {
this.stopTimeout = true;
this.status("Proof halted");
},
status : function(str) {
},
finished : function(state) {
},
nextStep : function() {
this.steps++;
var numBranches = this.tree.openBranches.length + this.tree.closedBranches.length;
this.status("step " + this.steps + ": " + numBranches + " branches, " + this.tree.numNodes + " nodes, " + this.alternatives.length + " alternatives, search depth " + this.depthLimit);
if (this.steps % 20 == 19) {
var counterModel = this.modelFinder.search(10);
if (counterModel) {
this.counterModel = counterModel;
return this.finished(0);
}
if (false && this.steps == 1019) {
this.tree = new Tree(this.formula);
this.fastMode = true;
}
if (this.steps % 1000 == 999) {
this.depthLimit++;
this.decreaseLimit = this.steps + 200;
}
else if (this.steps == this.decreaseLimit) {
this.depthLimit--;
}
}
else {
var result = this.tree.openBranches[0].expand();
switch (result) {
case 1 : {
if (this.tree.openBranches.length == 0) return this.finished(1);
break;
}
case 0 : {
if (this.tree.openBranches[0].nodes.length > this.depthLimit * this.nodeLimitFactor) {
prover.limitReached = true;
this.backtrack();
}
break;
}
case -1 : {
return this.finished(0);
}
}
}
if (this.stopTimeout) this.stopTimeout = false;
else setTimeout("prover.nextStep()", this.debug ? numBranches*100 : numBranches*5);
},
backtrack : function() {
if (this.alternatives.length == 0) {
if (!this.limitReached) {
return false;
}
this.depthLimit++;
this.tree = new Tree(this.formula);
this.limitReached = false;
return true;
}
this.tree = this.alternatives.shift();
return true;
}
}
function Tree(rootFormula) {
if (!rootFormula) return;
if (!rootFormula.normalized) {
rootFormula.normalized = rootFormula.normalize();
}
this.rootFormula = rootFormula;
this.firstNewVariable = 3;
var vars = rootFormula.normalized.getBoundVariables();
for (var i=0; i<vars.length; i++) if (vars[i] >= this.firstNewVariable) this.firstNewVariable = vars[i] + 3;
var consts = rootFormula.normalized.getConstants();
consts.sort(function(a,b){ return a-b });
this.rootNode = new Node(rootFormula.normalized);
this.openBranches = [new Branch(this, [this.rootNode], [this.rootNode], [], [], consts)];
this.closedBranches = [];
this.numNodes = 0;
}
Tree.prototype.closeBranch = function(branch, complementary1, complementary2) {
for (var n=complementary1; n; n=n.developedFrom) n.used = true;
for (var n=complementary2; n; n=n.developedFrom) n.used = true;
toRoot:
for (var i=branch.nodes.length-1; branch.nodes[i].developedFrom; i--) {
if (branch.nodes[i].developedFrom.type != tc.BETA) continue;
for (var j=0; j<this.openBranches.length; j++) {
if (this.openBranches[j] == branch) continue;
if (this.openBranches[j].nodes[i] && this.openBranches[j].nodes[i].developedFrom == branch.nodes[i].developedFrom
&& this.openBranches[j].nodes[i] != branch.nodes[i]) {
if (branch.nodes[i].used) break toRoot;
this.openBranches.remove(this.openBranches[j]);
break;
}
}
}
this.openBranches.remove(branch);
this.closedBranches.push(branch);
}
Tree.prototype.copy = function() {
function cloneObjectGraph(obj) {
var copy = new obj.constructor;
obj._mark = copy;
for (var i in obj) {
if (i == '_mark') continue;
var pval = obj[i];
if (typeof pval == "object" && pval != null) {
pval = pval._mark ? pval._mark : cloneObjectGraph(pval);
}
copy[i] = pval;
}
return copy;
}
function removeMarksFromObjectGraph(obj) {
delete obj._mark;
for (var i in obj) {
var pval = obj[i];
if (typeof pval == "object" && pval != null && pval._mark) {
removeMarksFromObjectGraph(pval);
}
}
}
var copy = cloneObjectGraph(this);
removeMarksFromObjectGraph(this);
return copy;
}
Tree.prototype.substitute = function(substitution) {
var branches = this.openBranches.concat(this.closedBranches);
for (var i=0; i<substitution.length; i+=2) {
for (var b=0; b<branches.length; b++) {
for (var n=0; n<branches[b].nodes.length; n++) {
branches[b].nodes[n].formula.substitute(substitution[i], substitution[i+1]);
}
branches[b].freeVariables.remove(substitution[i]);
}
}
}
Tree.prototype.toString = function() {
for (var i=0; i<this.closedBranches.length; i++) this.closedBranches[i].nodes[this.closedBranches[i].nodes.length-1].__markClosed = true;
var branches = this.closedBranches.concat(this.openBranches);
var res = "<table><tr><td align='center' style='font-family:monospace'>"+getTree(branches[0].nodes[0])+"</td</tr></table>";
for (var i=0; i<this.closedBranches.length; i++) delete this.closedBranches[i].nodes[this.closedBranches[i].nodes.length-1].__markClosed;
return res;
function getTree(node) {
var recursionDepth = arguments[1] || 0;
if (++recursionDepth > 50) return "<b>...<br>[max recursion]</b>";
var children = [];
for (var i=0; i<branches.length; i++) {
for (var j=0; j<branches[i].nodes.length; j++) {
if (branches[i].nodes[j-1] != node) continue;
if (!children.contains(branches[i].nodes[j])) children.push(branches[i].nodes[j]);
}
}
var res = node + (node.__markClosed ? "<br>x<br>" : "<br>");
if (children[1]) res += "<table><tr><td align='center' valign='top' style='font-family:monospace; border-top:1px solid #999; padding:3px; border-right:1px solid #999'>" + getTree(children[0], recursionDepth) + "</td>\n<td align='center' valign='top' style='padding:3px; border-top:1px solid #999; font-family:monospace'>" + getTree(children[1], recursionDepth) + "</td>\n</tr></table>";
else if (children[0]) res += getTree(children[0], recursionDepth);
return res;
}
}
function Branch(tree, nodes, unexpanded, literals, freeVariables, constants) {
this.tree = tree;
this.nodes = nodes;
this.unexpanded = unexpanded;
this.literals = literals || [];
this.freeVariables = freeVariables || [];
this.constants = constants || [];
this.id = self.__branchId ? self.__branchId++ : (self.__branchId = 1);
}
Branch.prototype.expand = function(fastMode) {
var node = this.unexpanded.shift();
if (!node) {
return prover.backtrack() ? 0 : -1;
}
switch (node.type) {
case tc.ALPHA : {
this.addNode(node.getSubNode(2));
this.addNode(node.getSubNode(1));
break;
}
case tc.BETA : {
this.tree.openBranches.unshift(this.copy());
this.tree.openBranches[0].addNode(node.getSubNode(1));
this.addNode(node.getSubNode(2));
if (fastMode) this.tree.openBranches[0].merge();
break;
}
case tc.GAMMA : {
if (this.freeVariables.length == prover.depthLimit) {
prover.limitReached = true;
prover.backtrack(true);
return 0;
}
var newVariable = this.freeVariables.length ? this.freeVariables[this.freeVariables.length-1] + 3 : this.tree.firstNewVariable;
this.freeVariables.push(newVariable);
var newFormula = node.formula[2].copyDeep().substitute(node.formula[1], newVariable);
this.addNode(new Node(newFormula, node));
this.unexpanded.push(node);
break;
}
case tc.DELTA : {
var newTerm = this.constants.length ? this.constants[this.constants.length-1] + 3 : 2;
this.constants.push(newTerm);
var freeVars = fastMode ? node.formula.getFreeVariables() : this.freeVariables.copy();
if (freeVars.length !== 0) {
freeVars.unshift(newTerm);
newTerm = freeVars;
}
var newFormula = node.formula[2].copyDeep().substitute(node.formula[1], newTerm);
this.addNode(new Node(newFormula, node));
break;
}
case tc.LITERAL : {
var negatedFormula = (node.formula[0] == tc.NEGATION) ? node.formula[1] : node.formula.negate();
var unifier;
if (!node.unifyWith) {
if (this.literals.length == 0) {
this.literals.unshift(node);
return 0;
}
var unifyCandidates = [];
for (var i=0; i<this.literals.length; i++) {
var unif = negatedFormula.unify(this.literals[i].formula);
if (unif.isArray) {
unifyCandidates.push(this.literals[i]);
if (!unifier) unifier = unif;
}
}
if (!unifier) {
this.literals.unshift(node);
return 0;
}
var considerAlternatives = false;
VARLOOP:
for (var i=0; i<unifier.length; i+=2) {
var variable = unifier[i];
for (var j=0; j<this.tree.openBranches.length; j++) {
var branch = this.tree.openBranches[j];
if (branch != this && branch.freeVariables.contains(variable)) {
considerAlternatives = true;
break VARLOOP;
}
}
}
if (considerAlternatives) {
for (var i=1; i<unifyCandidates.length; i++) {
this.unexpanded.unshift(node);
node.unifyWith = unifyCandidates[i];
prover.alternatives.unshift(this.tree.copy());
this.unexpanded.shift();
}
if (this.unexpanded.length) {
this.literals.unshift(node);
prover.alternatives.unshift(this.tree.copy());
this.literals.shift();
}
}
else {
}
node.unifyWith = unifyCandidates[0];
}
else unifier = negatedFormula.unify(node.unifyWith.formula);
this.tree.substitute(unifier);
this.tree.closeBranch(this, node, node.unifyWith);
node.complementary = node.unifyWith;
node.unifyWith.complementary = node;
return 1;
}
}
return fastMode ? this.merge() : 0;
}
Branch.prototype.copy = function() {
var nb = new Branch(this.tree, this.nodes.copy(), this.unexpanded.copy(), this.literals.copy(), this.freeVariables.copy(), this.constants.copy());
return nb;
}
Branch.prototype.addNode = function(node) {
this.nodes.push(node);
this.tree.numNodes++;
var order = {};
order[tc.LITERAL] = 1; order[tc.ALPHA] = 2; order[tc.BETA] = 3; order[tc.DELTA] = 4; order[tc.GAMMA] = 5;
var pos = 0;
while (pos < this.unexpanded.length) {
if (order[node.type] <= order[this.unexpanded[pos].type]) break;
pos++;
}
this.unexpanded.insert(node, pos);
}
Branch.prototype.merge = function() {
var branches = this.tree.closedBranches.concat(this.tree.openBranches);
for (var i=0; i<branches.length; i++) {
if (branches[i] == this) continue;
var merge = true;
nodeLoop:
for (var j=0; j<branches[i].nodes.length; j++) {
for (var k=0; k<this.nodes.length; k++) {
if (this.nodes[k].formula.equals(branches[i].nodes[j].formula)) continue nodeLoop;
}
merge = false;
break;
}
if (merge) {
if (!this.tree.mergedBranches) this.tree.mergedBranches = [];
this.tree.mergedBranches.push(this);
this.mergedWith = branches[i];
this.mergePoint = branches[i].nodes[branches[i].nodes.length-1];
this.tree.openBranches.remove(this);
return 1;
}
}
return 0;
}
Branch.prototype.toString = function() {
return this.unexpanded + "-" + this.literals;
}
function Node(formula, developedFrom) {
this.formula = formula;
this.developedFrom = developedFrom || null;
if (!formula) return;
switch (formula[0]) {
case tc.CONJUNCTION : this.type = tc.ALPHA; break;
case tc.DISJUNCTION : this.type = tc.BETA; break;
case tc.UNIVERSAL : this.type = tc.GAMMA; break;
case tc.EXISTENTIAL : this.type = tc.DELTA; break;
default: this.type = tc.LITERAL; break;
}
}
Node.prototype.getSubNode = function(subIndex) {
return new Node(this.formula[subIndex], this);
}
Node.prototype.toString = function() {
return translator.fla2html(this.formula);
}
function ModelFinder(formula) {
var rootNode = new Node(formula.normalize());
this.model = {
domain : [],
interpretation : [],
toString : function() {
var str = "<table>";
str += "<tr><td>Domain: </td><td align='left'>{ ";
str += this.domain.join(", ");
str += " }</td></tr>";
for (var p in this.interpretation) {
if (Array.prototype[p]) continue;
var inter = this.interpretation[p];
if (typeof inter == "boolean") var extension = inter;
else if (!inter.isArray) var extension = inter;
else {
var ext = getExtension(inter, this.domain);
var extension = "{ ";
if (translator.getType(p) == tc.CONSTANT) {
for (var i=0; i<ext.length; i++) {
extension += "&lt;" + ext[i].join(", ") + "&gt;"
if (i < ext.length-1) extension += ", ";
}
}
else {
var els = [];
for (var i=0; i<ext.length; i++) {
if (ext[i][ext[i].length-1] === false) continue;
if (ext[i].length == 2) els.push(ext[i][0]);
else els.push("&lt;" + ext[i].splice(0, ext[i].length-1).join(", ") + "&gt;");
}
extension += els.join(", ");
}
extension += " }";
}
str += "<tr><td align='right' class='formula'>" + translator.term2html(p) + ": </td><td align='left'>" + extension + "</td></tr>";
}
str += "</table>";
return str;
function getExtension(inter, domain) {
var res = [];
for (var i=0; i<domain.length; i++) {
if (inter[domain[i]] == undefined) continue;
if (inter[domain[i]].isArray) {
var subExt = getExtension(inter[domain[i]], domain);
for (var j=0; j<subExt.length; j++) res.push([domain[i]].concat(subExt[j]));
}
else res.push([domain[i], inter[domain[i]]]);
}
return res;
}
}
}
var model = this.model;
var consts = rootNode.formula.getConstants(true);
var preds = rootNode.formula.getPredicates(true);
this.isModel = function() {
return interpret(rootNode);
}
function interpret(node) {
switch (node.type) {
case tc.ALPHA : return interpret(node.getSubNode(1)) && interpret(node.getSubNode(2));
case tc.BETA : return interpret(node.getSubNode(1)) || interpret(node.getSubNode(2));
case tc.GAMMA : {
var matrixNode = new Node(node.formula[2]);
for (var i=0; i<model.domain.length; i++) {
model.interpretation[node.formula[1]] = model.domain[i];
var res = interpret(matrixNode)
delete model.interpretation[node.formula[1]];
if (!res) return false;
}
return true;
}
case tc.DELTA : {
var matrixNode = new Node(node.formula[2]);
for (var i=0; i<model.domain.length; i++) {
model.interpretation[node.formula[1]] = model.domain[i];
var res = interpret(matrixNode)
delete model.interpretation[node.formula[1]];
if (res) return true;
}
return false;
}
case tc.LITERAL : {
var fla = (node.formula[0] == tc.NEGATION) ? node.formula[1] : node.formula;
var inter = model.interpretation[fla[0]];
for (var i=0; i<fla[1].length; i++) {
var tval = fla[1][i].isArray ? interpret(fla[1][i]) : model.interpretation[fla[1][i]];
inter = inter[tval];
if (inter === undefined) break;
}
return (node.formula[0] == tc.NEGATION) ? !inter : !!inter;
}
default : {
var inter = model.interpretation[node[0]];
for (var i=1; i<node.length; i++) {
var tval = node[i].isArray ? interpret(node[i]) : model.interpretation[node[i]];
inter = inter[tval];
}
return inter;
}
}
}
this.search = function(numModels) {
for (var i=0; i<numModels; i++) {
if (!nextInterpretation()) initDomain(model.domain.length+1);
if (this.isModel()) {
return model;
}
}
return null;
}
function nextInterpretation() {
var arr = arguments[0] || model.interpretation;
for (var i=0; i<arr.length; i++) {
if (arr[i] === undefined) continue;
if (arr[i].isArray) {
if (nextInterpretation(arr[i])) return true;
continue;
}
if (typeof arr[i] == "boolean") {
if ((arr[i] = !arr[i])) return true;
continue;
}
if (++arr[i] < model.domain.length) return true;
arr[i] = 0;
}
return false;
}
function initDomain(numIndividuals) {
model.domain = [];
for (var i=0; i<numIndividuals; i++) model.domain.push(i);
for (var i=0; i<preds.length; i++) {
if (preds[i].arity == 0) {
model.interpretation[preds[i].predicate] = false;
continue;
}
var arrs = [model.interpretation[preds[i].predicate] = []];
for (var n=1; n<preds[i].arity; n++) {
var narrs = [];
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<numIndividuals; d++) narrs.push(arrs[j][d] = []);
}
arrs = narrs;
}
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<numIndividuals; d++) arrs[j][d] = false;
}
}
for (var i=0; i<consts.length; i++) {
if (consts[i].arity == 0) {
model.interpretation[consts[i].constant] = 0;
continue;
}
var arrs = [model.interpretation[consts[i].constant] = []];
for (var n=2; n<consts[i].arity; n++) {
var narrs = [];
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<numIndividuals; d++) narrs.push(arrs[j][d] = []);
}
arrs = narrs;
}
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<numIndividuals; d++) arrs[j][d] = 0;
}
}
}
}
function SenTree(fvTree) {
this.nodes = [];
this.rootNode = null;
this.isClosed = (fvTree.openBranches.length == 0);
var tree = this;
var freeVariables = [];
var constants = [];
initNodes();
for (var i=0; i<freeVariables.length; i++) {
var newConst = (constants.length != 0) ? constants[constants.length-1] + 3 : 2;
constants.push(newConst);
this.substitute(freeVariables[i], newConst);
}
replaceSkolemTerms();
removeUnusedNodes();
function initNodes() {
tree.rootNode = tree.nodes[0] = fvTree.rootNode;
tree.rootNode.base = SenNode;
tree.rootNode.base();
tree.rootNode.formula = fvTree.rootFormula;
for (var i=0; i<fvTree.closedBranches.length; i++) {
fvTree.closedBranches[i].nodes[fvTree.closedBranches[i].nodes.length-1].closedEnd = true;
}
var branches = fvTree.closedBranches.concat(fvTree.openBranches);
for (var b=0; b<branches.length; b++) {
for (var i=0; i<branches[b].freeVariables.length; i++) {
if (!freeVariables.contains(branches[b].freeVariables[i])) freeVariables.push(branches[b].freeVariables[i]);
}
freeVariables.sort(function(a,b){ return a-b });
for (var i=0; i<branches[b].constants.length; i++) {
if (!constants.contains(branches[b].constants[i])) constants.push(branches[b].constants[i]);
}
constants.sort(function(a,b){ return a-b });
var par;
for (var n=0; n<branches[b].nodes.length; n++) {
var node = branches[b].nodes[n];
if (node.isSenNode) {
par = node.swappedWith || node;
continue;
}
var from = node.developedFrom;
switch (from.formula[0]) {
case tc.UNIVERSAL : case tc.EXISTENTIAL : {
var inst = 3;
var normMatrix = from.formula[2].normalize();
var a1, a2, arrs1 = [node.formula], arrs2 = [normMatrix];
sLoop:
while (a1 = arrs1.shift(), a2 = arrs2.shift()) {
for (var i=0; i<a2.length; i++) {
if (a2[i].isArray) {
arrs1.unshift(a1[i]);
arrs2.unshift(a2[i]);
continue;
}
if (a2[i] != from.formula[1]) continue;
inst = a1[i];
break sLoop;
}
}
node.formula = from.formula[2].copyDeep().substitute(from.formula[1], inst);
tree.appendChild(par, node);
par = node;
break;
}
case tc.CONJUNCTION : {
if (from.__removeMe) {
if (par == from) par = from.parent;
node.developedFrom = from.developedFrom;
if (!from.isRemoved) tree.remove(from);
}
var f1 = from.formula[1].copyDeep();
var f2 = from.formula[2].copyDeep();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.developedFrom == node.developedFrom) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.developedFrom == node.developedFrom && node.formula == f1) tree.reverse(par, node);
else par = node;
break;
}
case tc.DISJUNCTION : {
var f1 = from.formula[1].copyDeep();
var f2 = from.formula[2].copyDeep();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.children && par.children.length) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.children.length == 2 && node.formula == f1) par.children.reverse();
par = node;
break;
}
case tc.IMPLICATION : {
var f1 = from.formula[1].copyDeep().negate();
var f2 = from.formula[2].copyDeep();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.children && par.children.length) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.children.length == 2 && node.formula == f1) par.children.reverse();
par = node;
break;
}
case tc.BIIMPLICATION : {
var f1 = [tc.CONJUNCTION, from.formula[1], from.formula[2]].copyDeep();
var f2 = [tc.CONJUNCTION, from.formula[1].negate(), from.formula[2].negate()].copyDeep();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.children && par.children.length) ? f2 : f1;
}
node.__removeMe = true;
tree.appendChild(par, node);
if (par.children.length == 2 && node.formula == f1) par.children.reverse();
par = node;
break;
}
case tc.NEGATION : {
switch (from.formula[1][0]) {
case tc.UNIVERSAL : case tc.EXISTENTIAL : {
var inst = 3;
var normMatrix = from.formula[1][2].negate().normalize();
var a1, a2, arrs1 = [node.formula], arrs2 = [normMatrix];
sLoop:
while (a1 = arrs1.shift(), a2 = arrs2.shift()) {
for (var i=0; i<a2.length; i++) {
if (a2[i].isArray) {
arrs1.unshift(a1[i]);
arrs2.unshift(a2[i]);
continue;
}
if (a2[i] != from.formula[1][1]) continue;
inst = a1[i];
break sLoop;
}
}
node.formula = from.formula[1][2].negate().copyDeep().substitute(from.formula[1][1], inst);
tree.appendChild(par, node);
par = node;
break;
}
case tc.CONJUNCTION : {
var f1 = from.formula[1][1].copyDeep().negate();
var f2 = from.formula[1][2].copyDeep().negate();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.children && par.children.length) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.children.length == 2 && node.formula == f1) par.children.reverse();
par = node;
break;
}
case tc.DISJUNCTION : {
var f1 = from.formula[1][1].copyDeep().negate();
var f2 = from.formula[1][2].copyDeep().negate();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.developedFrom == node.developedFrom) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.developedFrom == from && node.formula == f1) tree.reverse(par, node);
else par = node;
break;
}
case tc.IMPLICATION : {
var f1 = from.formula[1][1].copyDeep();
var f2 = from.formula[1][2].copyDeep().negate();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.developedFrom == node.developedFrom) ? f2 : f1;
}
tree.appendChild(par, node);
if (par.developedFrom == from && node.formula == f1) tree.reverse(par, node);
else par = node;
break;
}
case tc.BIIMPLICATION : {
var f1 = [tc.CONJUNCTION, from.formula[1][1], from.formula[1][2].negate()].copyDeep();
var f2 = [tc.CONJUNCTION, from.formula[1][1].negate(), from.formula[1][2]].copyDeep();
if (!node.formula.equals(f1.normalize())) node.formula = f2;
else if (!node.formula.equals(f2.normalize())) node.formula = f1;
else {
node.formula = (par.children && par.children.length) ? f2 : f1;
}
node.__removeMe = true;
tree.appendChild(par, node);
if (par.children.length == 2 && node.formula == f1) par.children.reverse();
par = node;
break;
}
case tc.NEGATION : {
if (!from.dneTo) {
var newNode = new Node(from.formula[1][1].copyDeep(), from);
newNode.base = SenNode;
newNode.base();
newNode.developedFrom = from;
from.dneTo = newNode;
var dneToPar = (from.children[0] && from.children[0].developedFrom == from.developedFrom) ? from.children[0] : from;
newNode.parent = dneToPar;
newNode.children = dneToPar.children;
for (var i=0; i<newNode.children.length; i++) newNode.children[i].parent = newNode;
dneToPar.children = [newNode];
newNode.used = from.used;
tree.nodes.push(newNode);
if (par == dneToPar) par = newNode;
}
node.developedFrom = from.dneTo;
par = (par == from) ? from.dneTo : par;
n -= 1;
break;
}
default : {
tree.appendChild(par, node);
par = node;
}
}
break;
}
default : {
tree.appendChild(par, node);
par = node;
}
}
}
}
}
function removeUnusedNodes() {
if (!tree.isClosed) return;
for (var i=0; i<tree.nodes.length; i++) {
if (!tree.nodes[i].used) continue;
var node = tree.nodes[i];
if (node.formula[0] == tc.NEGATION && node.formula[1][0] == tc.NEGATION && node.children[0]) node.children[0].used = true;
if (!node.developedFrom) continue;
var expansion = tree.getExpansion(node);
for (var j=0; j<expansion.length; j++) expansion[j].used = true;
}
for (var i=0; i<tree.nodes.length; i++) {
if (!tree.nodes[i].used) tree.remove(tree.nodes[i--]);
}
}
function replaceSkolemTerms() {
var okConstants = tree.rootNode.formula.getConstants();
var translations = {};
for (var n=0; n<tree.nodes.length; n++) {
var terms = getComplexTerms(tree.nodes[n].formula);
termLoop:
for (var c=0; c<terms.length; c++) {
if (okConstants.contains(terms[c][0])) continue termLoop;
var termstr = terms[c].toString();
if (!translations[termstr]) {
translations[termstr] = constants[constants.length-1] + 3;
constants.push(translations[termstr]);
}
tree.nodes[n].formula.substitute(terms[c], translations[termstr], true);
}
}
function getComplexTerms(formula) {
var result = [];
var flas = [formula];
var fla;
while ((fla = flas.shift())) {
if (fla.length == 3 && fla[0] < 0) {
if (!fla[1].isArray) {
flas.unshift(fla[2]);
continue;
}
flas.unshift(fla[1]);
flas.unshift(fla[2]);
continue;
}
if (fla[0] == tc.NEGATION) flas.unshift(fla[1]);
else {
for (var i=0; i<fla[1].length; i++) {
if (!fla[1][i].isArray) continue;
result.push(fla[1][i]);
flas.unshift(fla[1][i]);
}
}
}
return result;
}
}
}
SenTree.prototype.appendChild = function(oldNode, newNode) {
if (!newNode.isSenNode) {
newNode.base = SenNode;
newNode.base();
}
newNode.parent = oldNode;
oldNode.children.push(newNode);
if (oldNode.closedEnd) {
oldNode.closedEnd = false;
newNode.closedEnd = true;
}
this.nodes.push(newNode);
return newNode;
}
SenTree.prototype.remove = function(node) {
if (node.parent.children.length == 1) {
node.parent.children = node.children;
if (node.children[0]) node.children[0].parent = node.parent;
if (node.children[1]) node.children[1].parent = node.parent;
}
else {
if (node.children.length > 1) return alert("can't remove a node with two children that itself has a sibling");
var i = (node == node.parent.children[0]) ? 0 : 1;
if (node.children[0]) {
node.parent.children[i] = node.children[0];
node.children[0].parent = node.parent;
}
else node.parent.children.remove(node);
}
this.nodes.remove(node);
node.isRemoved = true;
}
SenTree.prototype.toString = function() {
return "<table><tr><td align='center' style='font-family:monospace'>"+getTree(this.rootNode)+"</td</tr></table>";
function getTree(node) {
var recursionDepth = arguments[1] || 0;
if (++recursionDepth > 40) return "<b>...<br>[max recursion]</b>";
var res = node + (node.closedEnd ? "<br>x<br>" : "<br>");
if (node.children[1]) res += "<table><tr><td align='center' valign='top' style='font-family:monospace; border-top:1px solid #999; padding:3px; border-right:1px solid #999'>" + getTree(node.children[0], recursionDepth) + "</td>\n<td align='center' valign='top' style='padding:3px; border-top:1px solid #999; font-family:monospace'>" + getTree(node.children[1], recursionDepth) + "</td>\n</tr></table>";
else if (node.children[0]) res += getTree(node.children[0], recursionDepth);
return res;
}
}
SenTree.prototype.substitute = function(oldTerm, newTerm) {
for (var i=0; i<this.nodes.length; i++) {
this.nodes[i].formula.substitute(oldTerm, newTerm);
}
}
SenTree.prototype.reverse = function(node1, node2) {
node2.parent = node1.parent;
node1.parent = node2;
if (node2.parent.children[0] == node1) node2.parent.children[0] = node2;
else node2.parent.children[1] = node2;
node1.children = node2.children;
node2.children = [node1];
if (node1.children[0]) node1.children[0].parent = node1;
if (node1.children[1]) node1.children[1].parent = node1;
if (node2.closedEnd) {
node2.closedEnd = false;
node1.closedEnd = true;
}
node2.swappedWith = node1;
node1.swappedWith = node2;
}
SenTree.prototype.getExpansion = function(node) {
if (!node.developedFrom) return [node];
var from = node.developedFrom;
var fromOp = from.formula[0];
if (fromOp == tc.NEGATION) {
fromOp = (from.formula[1][0] == tc.CONJUNCTION) ? tc.DISJUNCTION
: (from.formula[1][0] == tc.DISJUNCTION || from.formula[1][0] == tc.IMPLICATION) ? tc.CONJUNCTION :
from.formula[1][0];
}
switch (fromOp) {
case tc.CONJUNCTION : {
if (node.children[0] && node.children[0].developedFrom == from) return [node, node.children[0]];
if (node.parent.developedFrom == from) return [node.parent, node];
return [node];
}
case tc.DISJUNCTION :
case tc.IMPLICATION : {
return node.parent.children;
}
case tc.BIIMPLICATION : {
var res = (node.children[0] && node.children[0].developedFrom == from) ? [node, node.children[0]]
: (node.parent.developedFrom == from) ? [node.parent, node]
: [node];
if (!res[0].parent.children[1]) return res;
var i = (res[0].parent.children[0] == res[0]) ? 1 : 0;
res.push(res[0].parent.children[i]);
if (res[0].parent.children[i].children[0] && res[0].parent.children[i].children[0].developedFrom == from) res.push(res[0].parent.children[i].children[0]);
return res;
}
default : {
return [node];
}
}
}
SenTree.prototype.getCounterModel = function() {
var endNode = null;
for (var i=0; i<this.nodes.length; i++) {
if (this.nodes[i].children.length || this.nodes[i].closedEnd) continue;
endNode = this.nodes[i];
break;
}
if (!endNode) return null;
var modelFinder = new ModelFinder(this.rootNode.formula);
var model = modelFinder.model;
var node = endNode;
do {
var fla = node.formula;
while (fla[0] == tc.NEGATION) fla = fla[1];
if (fla[0] < 0) continue;
var terms = fla[1].copy();
for (var t=0; t<terms.length; t++) {
var term = translator.term2html(terms[t]);
if (model.domain.contains(term)) continue;
model.domain.push(term);
if (terms[t].isArray) {
for (var i=1; i<terms[t].length; i++) terms.push(terms[t][i]);
}
else model.interpretation[terms[t]] = term;
}
} while ((node = node.parent));
if (model.domain.length == 0) model.domain = [2];
node = endNode;
do {
var fla = node.formula;
var tv = true;
while (fla[0] == tc.NEGATION) {
fla = fla[1];
tv = !tv;
}
if (fla[0] < 0) continue;
var pred = fla[0];
var terms = fla[1];
if (terms.length == 0) {
model.interpretation[pred] = tv;
continue;
}
var subTerms = terms.copy();
for (var t=0; t<subTerms.length; t++) {
var term = subTerms[t];
if (!term.isArray) continue;
var functor = term[0], args = term.slice(1);
if (!model.interpretation[functor]) {
var arrs = [model.interpretation[functor] = []];
for (var n=2; n<args.length; n++) {
var narrs = [];
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<model.domain.length; d++) narrs.push(arrs[j][model.domain[d]] = []);
}
arrs = narrs;
}
for (var j=0; j<arrs.length; j++) {
for (var d=0; d<model.domain.length; d++) arrs[j][model.domain[d]] = model.domain[0];
}
}
var arrs = [model.interpretation[functor]];
for (var i=1; i<term.length-1; i++) {
var sTerm = translator.term2html(term[i]);
arrs[i] = arrs[i-1][sTerm];
}
var lastSTerm = translator.term2html(term[term.length-1]);
arrs[arrs.length-1][lastSTerm] = translator.term2html(term);
for (var i=1; i<term.length; i++) subTerms.push(term[i]);
}
if (!model.interpretation[pred]) model.interpretation[pred] = [];
var arrs = [model.interpretation[pred]];
for (var i=0; i<terms.length-1; i++) {
var term = translator.term2html(terms[i]);
if (!arrs[i][term]) arrs[i][term] = [];
arrs[i+1] = arrs[i][term];
}
var lastTerm = translator.term2html(terms[terms.length-1])
arrs[arrs.length-1][lastTerm] = tv;
} while ((node = node.parent));
if (modelFinder.isModel()) {
return model;
}
return null;
}
function SenNode() {
this.isSenNode = true;
this.parent = null;
this.children = [];
}
function TreePainter(senTree, rootAnchor) {
this.paintInterval = 700;
this.branchPadding = 30;
this.branchingHeight = 40;
this.pixelDistanceOnLine = 4;
this.lineColor = "#600";
this.formulaCSS = "formula";
this.nodeCSS = "treeNode";
this.nodeHiParentCSS = "treeNodeHiParent"
this.nodeHiChildCSS = "treeNodeHiChild"
this.tree = senTree;
this.rootAnchor = rootAnchor;
this.rootAnchor.innerHTML = "";
this.minX = this.branchPadding - rootAnchor.offsetLeft;
var curNodeNumber = 0;
var freePixels = [];
var highlighted = [];
var painter = this;
TreePainter.instance = this;
this.paintTree = function() {
var node = getNextUnpainted(this.tree);
if (!node) {
this.highlight([]);
return this.finished();
}
var paintNodes = this.tree.getExpansion(node);
for (var i=0; i<paintNodes.length; i++) {
if (!paintNodes[i]) alert(node +" from " + node.developedFrom + " => "+paintNodes+ ", childr: "+node.children+", par: "+node.parent+", par.children: "+node.parent.children);
this.paint(paintNodes[i]);
}
this.highlight(paintNodes, node.developedFrom);
this.paintTimer = setTimeout("TreePainter.instance.paintTree()", this.paintInterval);
};
this.stop = function() {
clearTimeout(this.paintTimer);
}
this.finished = function() {}
this.paint = function(node) {
if (!node.parent || node.parent.children.length == 2) {
var parContainer = node.parent ? node.parent.container : this.rootAnchor;
node.container = document.createElement('div');
parContainer.appendChild(node.container);
if (node.parent) parContainer.subContainers.push(node.container);
node.container.subContainers = [];
node.container.style.width = "100%";
node.container.style.position = "absolute";
node.container.style.left = "0px";
node.container.style.top = node.parent ? parContainer.h + this.branchingHeight + "px" : "0px";
node.container.w = node.container.h = 0;
node.container.str = "{ "+node+ " }" + (self.__strid ? self.__strid++ : (self.__strid = 1));
}
else node.container = node.parent.container;
node.nodeNumber = ++curNodeNumber;
var html = curNodeNumber + ".&nbsp;&nbsp;<span class='" + this.formulaCSS + "'>" + translator.fla2html(node.formula) + "</span>";
html += node.developedFrom ? "&nbsp;&nbsp;(" + node.developedFrom.nodeNumber + ")" : "&nbsp;&nbsp;&nbsp;&nbsp;";
if (node.closedEnd) html += "<br><b>x</b>";
node.div = document.createElement('div');
node.div.innerHTML = html;
node.div.className = this.nodeCSS;
node.div.style.position = "absolute";
document.body.appendChild(node.div);
node.div.w = node.div.offsetWidth;
node.div.h = node.div.offsetHeight;
document.body.removeChild(node.div);
node.container.appendChild(node.div);
node.div.style.left = -node.div.w/2 + "px";
node.div.style.top = node.container.h + "px";
node.container.h += node.div.h + 3;
if (node.children.length == 0) node.container.h += this.branchPadding;
node.container.w = Math.max(node.container.w, node.div.w);
var par = node.container;
while ((par = par.parentNode).subContainers) {
if (!par.subContainers[1]) continue;
var overlap = getOverlap(par);
if (overlap) {
var x1 = parseInt(par.subContainers[0].style.left) - Math.ceil(overlap/2);
var x2 = parseInt(par.subContainers[1].style.left) + Math.ceil(overlap/2);
par.subContainers[0].style.left = x1 + "px";
par.subContainers[1].style.left = x2 + "px";
if (par.pixels) for (var i=0; i<par.pixels.length; i++) freePixels.push(par.removeChild(par.pixels[i]));
var line1 = this.drawLine(par, 0, par.h, x1, par.h + this.branchingHeight);
var line2 = this.drawLine(par, 0, par.h, x2, par.h + this.branchingHeight);
par.pixels = line1.concat(line2);
}
}
var minX = 0;
var con, cons = [this.rootAnchor.firstChild];
while ((con = cons.shift())) {
con.__x = (con.parentNode.__x || 0) + parseInt(con.style.left);
if (con.__x - con.w < minX) minX = con.__x - con.w/2;
cons = cons.concat(con.subContainers);
}
if (minX < this.minX) {
this.rootAnchor.firstChild.style.left = this.rootAnchor.firstChild.__x + (this.minX - minX) + "px";
}
}
this.highlight = function(children, parent) {
while (highlighted.length) highlighted.shift().div.className = this.nodeCSS;
for (var i=0; i<children.length; i++) children[i].div.className = this.nodeHiChildCSS;
highlighted = children.copy();
if (parent) {
parent.div.className = this.nodeHiParentCSS;
highlighted.push(parent);
}
}
this.drawLine = function(el, x1, y1, x2, y2) {
var distX = x2 - x1;
var distY = y2 - y1;
var dist = Math.sqrt(distX*distX + distY*distY);
var pxX = distX/dist;
var pxY = distY/dist;
var drawn = 1;
var dotX = x1;
var dotY = y1;
var pixels = [];
while (drawn < dist) {
if ((dotX != Math.round(x1 + drawn*pxX) || dotY != Math.round(y1 + drawn*pxY)) && (drawn % this.pixelDistanceOnLine == 0)) {
dotX = Math.round(x1 + drawn*pxX);
dotY = Math.round(y1 + drawn*pxY);
if (freePixels.length > 0) {
var pixel = freePixels.shift();
el.appendChild(pixel);
}
else {
var pixel = document.createElement("div");
el.appendChild(pixel);
pixel.style.position = "absolute";
pixel.style.width = "1px";
pixel.style.height = "1px";
pixel.style.clip = "rect(0 1px 1px 0)";
pixel.style.backgroundColor = this.lineColor;
}
pixel.style.left = dotX + "px";
pixel.style.top = dotY + "px";
pixels.push(pixel);
}
drawn++;
}
return pixels;
}
function getNextUnpainted(tree) {
var nodes = [tree.rootNode];
var node;
while ((node = nodes.shift())) {
do {
if (!node.div) return node;
if (node.children.length == 2) nodes.unshift(node.children[1]);
} while ((node = node.children[0]));
}
return null;
}
function getOverlap(par) {
var overlap = 0;
var co1, co2, co1s = [par.subContainers[0]], co2s;
par.__x = 0; par.__y = 0;
while ((co1 = co1s.shift())) {
co2s = [par.subContainers[1]];
while ((co2 = co2s.shift())) {
co1.__x = co1.parentNode.__x + parseInt(co1.style.left);
co1.__y = co1.parentNode.__y + parseInt(co1.style.top);
co2.__x = co2.parentNode.__x + parseInt(co2.style.left);
co2.__y = co2.parentNode.__y + parseInt(co2.style.top);
if ((co1.__y >= co2.__y) && (co1.__y < co2.__y + co2.h) || (co2.__y >= co1.__y) && (co2.__y < co1.__y + co1.h)) {
var overlap12 = (co1.__x + co1.w/2 + painter.branchPadding) - (co2.__x - co2.w/2);
overlap = Math.max(overlap, overlap12);
}
co2s = co2s.concat(co2.subContainers);
}
co1s = co1s.concat(co1.subContainers);
}
return Math.floor(overlap);
}
}
function laTeX2html(str) {
str = str.replace(/\s*/g, '');
str = str.replace(/\\forall[\{ ]?\}?/g, translator.logSymbols[tc.UNIVERSAL]);
str = str.replace(/\\exists[\{ ]?\}?/g, translator.logSymbols[tc.EXISTENTIAL]);
str = str.replace(/(\\neg|\\lnot)[\{ ]?\}?/g, translator.logSymbols[tc.NEGATION]);
str = str.replace(/(\\vee|\\lor)[\{ ]?\}?/g, translator.logSymbols[tc.DISJUNCTION]);
str = str.replace(/(\\wedge|\\land)[\{ ]?\}?/g, translator.logSymbols[tc.CONJUNCTION]);
str = str.replace(/(\\to|\\rightarrow)[\{ ]?\}?/g, translator.logSymbols[tc.IMPLICATION]);
str = str.replace(/\\leftrightarrow[\{ ]?\}?/g, translator.logSymbols[tc.BIIMPLICATION]);
str = str.replace(/([^'])(\\[^<]*)/, '$1<span class="latex">$2</span>');
str = str.replace(/^(\\[^<]*)/, '<span class="latex">$1</span>');
return str;
}
document.forms[0].flaField.onkeyup = document.forms[0].flaField.onfocus = function(e) {
document.getElementById("renderedFla").innerHTML = laTeX2html(document.forms[0].flaField.value);
if (typeof this.selectionStart == "number") this._caretPosition = this.selectionStart;
else if (document.selection && !document.all) {
var range = this.createTextRange();
range.setEndPoint("EndToStart", document.selection.createRange());
this._caretPosition = range.text.length;
}
}
document.forms[0].flaField.onkeyup();
onload = function(e) {
var symButtons = [tc.NEGATION, tc.CONJUNCTION, tc.DISJUNCTION, tc.IMPLICATION, tc.BIIMPLICATION, tc.UNIVERSAL, tc.EXISTENTIAL];
for (var i=0; i<symButtons.length; i++) {
var div = document.createElement("div");
div.className = "symbutton";
div.innerHTML = translator.logSymbols[symButtons[i]];
div.onmousedown = function(e) { this.style.borderStyle = "inset"; }
div.onmouseup = div.onmouseout = function(e) { this.style.borderStyle = "outset"; }
div.onclick = symButtonClick;
document.getElementById("symboltd").appendChild(div);
}
function symButtonClick(e) {
var field = document.forms[0].flaField;
if (field._caretPosition === undefined) field._caretPosition = field.value.length;
var command = this.firstChild.getAttribute("alt");
field.value = field.value.substr(0, field._caretPosition) + command + field.value.substr(field._caretPosition);
field._caretPosition += command.length;
if (field._caretPosition == field.value.length) field.focus();
else field.onkeyup();
}
document.forms[0].onsubmit = function(e) {
try {
this.flaField.onkeyup();
translator.init();
var formula = translator.latex2fla(this.flaField.value);
if (!formula) {
alert("Invalid formula.\n"+translator.error);
return false;
}
document.getElementById("intro").style.display = "none";
document.getElementById("model").style.display = "none";
document.getElementById("rootAnchor").style.display = "none";
document.getElementById("statusBox").style.display = "block";
document.getElementById("statusHeader").innerHTML = "Proving...";
document.getElementById("statusStop").style.display = "inline";
document.getElementById("statusStop").firstChild.nodeValue = 'stop';
document.getElementById("paintStop").firstChild.nodeValue = 'stop';
prover.start(formula.negate());
}
catch (e) {
alert("Error: " + e);
};
return false;
}
prover.status = function(str) {
document.getElementById("status").innerHTML = str;
}
prover.finished = function(treeClosed) {
document.getElementById("statusHeader").innerHTML = "<span class='formula'>" + translator.fla2html(this.formula[1]) + "</span> is " + (treeClosed ? "valid." : "invalid.");
document.getElementById("statusStop").style.display = "none";
prover.status("");
var sentenceTree = new SenTree(this.tree);
if (!treeClosed) {
if (!this.counterModel) this.counterModel = sentenceTree.getCounterModel();
if (this.counterModel) {
document.getElementById("model").style.display = "block";
document.getElementById("model").innerHTML = "<b>Countermodel:</b><br>" + this.counterModel;
return;
}
}
document.getElementById("rootAnchor").style.display = "block";
document.getElementById("paintBar").style.display = "block";
self.painter = new TreePainter(sentenceTree, document.getElementById("rootAnchor"));
self.painter.finished = function() {
document.getElementById("paintBar").style.display = "none";
}
self.painter.paintTree();
}
document.getElementById("statusStop").onclick = function(e) {
if (this.firstChild.nodeValue == 'stop') {
prover.stop();
this.firstChild.nodeValue = 'continue';
return;
}
this.firstChild.nodeValue = 'stop';
prover.nextStep();
}
document.getElementById("paintStop").onclick = function(e) {
if (this.firstChild.nodeValue == 'stop') {
painter.stop();
this.firstChild.nodeValue = 'continue';
return;
}
this.firstChild.nodeValue = 'stop';
painter.paintTree();
}
document.getElementById("paintFaster").onclick = function(e) {
if (this.firstChild.nodeValue == 'faster') {
painter.oldInterval = painter.paintInterval;
painter.paintInterval = 100;
this.firstChild.nodeValue = 'slower';
return;
}
painter.paintInterval = painter.oldInterval;
this.firstChild.nodeValue = 'faster';
}
if (location.search.match(/\?f=/)) {
document.forms[0].flaField.value = unescape(location.search.substr(3));
document.forms[0].onsubmit();
}
}