/*   tree.js

______________________________________________________________

*/
		var gaff = false // REMOVE
var branches = '|,0,|'
var arrayNum = 0
var currArray
var constants = 'abcdefghijklmnopqrstu'
var Constant = new Array // this array gives the constants in each array of the brances
Constant[0]='' // need to set Constant[0] -- all other members set by addArray() and altered with addNode()
var consInTree // the collection of all constants used at any time
var checkOpen = false
var stuff = '' // REMOVE
var msg = ""
var endNum
if (typeof endNum != 'number') endNum = 3000
if (typeof branchMax != 'number') branchMax = 10000


	var t = new Array
function addNode(T,s) { // t refers to an array of nodes, s to the given sentence
newNode = new Node(s)
T[T.length] = newNode
s = newNode.sent
for ( var i=0; i<s.length; i++ ) {
	var x =s.charAt(i)
   if ( constants.indexOf(x)>-1 && Constant[currArray].indexOf(x)==-1 ) { // keeps track of any constants added in the new Node
   	Constant[currArray] += x
   	addConstant(x)
   	}
}
if (newNode.mc == null ) checkClose(currArray,s,'a')
else if (newNode.mc == '~') checkClose(currArray,s,'~')
return newNode.mc
}

	var elim // the contradictory arrays to the current sent in arrayX 
function cleanseNet(arrayX,sent,type) { // this takes the new sentence and does a linear treck thru the net to see if there is ANY new contradiction between sent and another sentence
elim = ''
sent = ( type == '~' ) ? sent.substring(1) : '~'+ sent
		outer:
	for ( var i=0; i<t.length; i++ ) { // i is the array number
			inner:
		for ( var j=0; j<t[i].length; j++ ) { // j is the sentence number in array i
   		if (t[i][j].sent == sent) {
   			elim += '(' + i + ')'
   			rewrite = true
   			break inner
   			}
			}   
		}
}


	var opn, rewrite
function checkClose(arrayX,sent,type) { // *misnomer*: checks to see if a branch is FINISHED (open or closed)
if (branches.length < branchMax) { // begin of check
rewrite = false
cleanseNet(arrayX,sent,type)
var y = branches.split('|') // creates an array of branches
var x = ',' + arrayX + ',' 
//if ( type == 'a' ) sent = '~' + sent // to look for contradiction
//else sent = sent.substring(1)
	outer:
for ( var i=1; i<y.length-1; i++ ) { // loop over branches (y[i] gives the branch numbers)
   if (y[i].indexOf(x)>-1) { // if branch y[i] includes arrayX
		opn = (splitTrack==1 && checkOpen == true ) ? true : false // asume an open (finished) branch unless branching for = incomplete, i.e., splitTrack == 0
   	var z = y[i].split(',')
   	var consInB = ''
   		inner:   	
	for ( var j=1; j<z.length-1; j++ ) { // z[j] ranges over all arrays in branch i
		if (elim.indexOf( '(' + z[j] + ')' ) > -1) {
			y[i]=''
			opn = false
			continue outer
			}
		counter++
		status = counter
		if (counter > endNum) { 
			quit = true
			if (quit) break outer // added stop
			}
   		consInB += Constant[z[j]]
   		/*for ( var k=0; k<t[z[j]].length; k++ ) { // k ranges over the array z[j]'s elements
   			if (t[z[j]][k].sent == sent) {
    				y[i] = ''
   				rewrite = true
   				opn = false
   				break inner //??????? outer?
   				}
   			}
   			*/
   		}
if (opn) { //opn == true iff both splitTrack==1 && checkOpen == true
   	for ( var j=1; j<z.length-1; j++ ) { // z[j] ranges over all arrays in branch i
   		for ( var k=0; k<t[z[j]].length; k++ ) { // k ranges over the array z[j]'s elements
   			var mainC = t[z[j]][k].mc
   			if ( splitTrack == 1 && mainC != null && mainC != '~' && mainC != 'f') {
   				counter++
					status = '' + counter + ": Working to check for finished open threads."
					if (mainC.charAt(0) == '^' && consInB.length>0) {
					for ( var l=0; l<consInB.length; l++ ) {
   					if ( mainC.indexOf(consInB.charAt(l)) < 0 ) {
   						opn = false  // branch is not finished
   						continue outer
							}
						}
					}
					else {opn = false 
								continue outer // branch is not finished
								} 
   			}
			}
		}
	}
		if (opn) {
   		msg += "\nThere is a finished, open branch: " + i + " of " + branches // TESTING PURPOSES
   		quit = true
   		result = 'open'
   		break outer
 			}
   	}
	}
if (rewrite) branches = y.join('|')
} // end of check
else {
	pass = 0
	quit = true
	}
}

	var pass // global variable to keep track of passes from & to ^.
function workTree() { // work through Arrays starting with 0
if ( typeof consInTree != 'string' ) consInTree = Constant[0]
for ( pass=0; pass<4; pass++ ) {
	if (quit) break
		loop:
	for ( var i=0; i<=arrayNum; i++ ) {
		if (quit) break
		if (branches.indexOf(',' + i + ',')==-1) continue loop
		currArray = i
   	workArray(t[i])
		}
		if ( retry && !quit ) {
	if ( gaff == true ) stuffIt() // REMOVE!!!!!!!!!!
			pass = 0
			retry = false
			}
	}
}

function addArray(arrayX,sent1,sent2) { // adds an array branching from all offspring of current arrayX; the sentences added shown... 
if (sent2 != null ) splitTrack = 0
arrayNum++
t[arrayNum] = new Array
var newNode1 = new Node(sent1)
t[arrayNum][0] = newNode1
sent1 = newNode1.sent
Constant[arrayNum] = ''
for ( var i=0; i<sent1.length; i++ ) {
	var x = sent1.charAt(i)
   if ( constants.indexOf(x)>-1 && Constant[arrayNum].indexOf(x)==-1 ) {
   	Constant[arrayNum] += x
   	addConstant(x)
   	}
}
if (newNode1.mc == null ) checkClose(arrayNum,sent1,'a')
else if (newNode1.mc == '~') checkClose(arrayNum,sent1,'~')
if (sent2!=null) {
	splitTrack++
	var newNode2 = new Node(sent2)
	t[arrayNum][1] = newNode2
	sent2 = newNode2.sent
	for ( var i=0; i<sent2.length; i++ ) {
		var x = sent2.charAt(i)
   	if ( constants.indexOf(x)>-1 && Constant[arrayNum].indexOf(x)==-1 ) {
   		Constant[arrayNum] += x
   		addConstant(x)
		}
	}
	if (newNode2.mc == null ) checkClose(arrayNum,sent2,'a')
	else if (newNode2.mc == '~') checkClose(arrayNum,sent2,'~')
	}
}

function addConstant(x) {
 if (consInTree.indexOf(x)==-1) consInTree += x
 consInTree = consInTree.split('').sort().join('')
}

//testing...REMOVE
	var info
function stuffIt() {
for ( var i=0; i<t.length; i++ ) {
	stuff += 't[' + i + ']:\n'
for ( var j=0; j<t[i].length; j++ ) {
   stuff += '' + j + ': ' + t[i][j].sent + ' ' + t[i][j].mc + '\n'
}
	stuff += '\n\n'
}
stuff += branches + '\n\n'

for ( var i=0; i<Constant.length; i++ ) {
   stuff += "Constant["+ i + "] = " + Constant[i] + "\n"
}

stuff += "\nconsInTree = " + consInTree

info += stuff
}



function branching() { // adds the info about the new array onto the current branch n; e.g., "|,0,|" goes to "|,0,1,|,0,2,|"
var i = 0
var n = currArray, m = '' + (arrayNum+1), o = '' + (arrayNum+2)
while ( branches.indexOf(','+ n + ',',i) >-1 ) {
   var k = branches.indexOf(','+ n + ',',i)
   var b = branches.lastIndexOf('|',k)
   var e = branches.indexOf('|',k)
   var ss = branches.substring(b,e)
   branches = branches.substring(0,e) + m + ',' + ss + o + ',' + branches.substring(e)
   i = (b + 2*ss.length + 3 + m.length + o.length)
	}
}

	var counter = 0
	var splitTrack = 1 // counter to keep track of branching for = (which is not finised on a branch until a second node is added
	var quit = false
	var retry = false // variable which will reset pass in workArray to 0 if true
function workArray(T) { // expands the tree about an array of a branch
	counter++
	status = counter // REMOVE
	if ( counter > endNum ) {
		if ( confirm("I\'m not absolutely sure, but I think your answer is NOT logically equivalent to any correct answer.\n\nDo you want to keep checking? (Press \"Cancel\" to abort the test, \"OK\" to continue.)")  ) counter=endNum-200
		else {
			quit = true
			counter = 0
			return false
		}
	}
if ( opn ) {
   	quit = true
		return false
		} 
	for ( var i=0; i<T.length; i++ ) {
   	var node = T[i]
   	var mc = node.mc
   	if ( mc == 'f' || mc == null || mc == '~' ) continue
   	if ( mc == '&' ) {
   		splitTrack = 0
   		addNode(T, dropParen(node.comp1)) 											// splitTrack = ???
   		splitTrack++
   		addNode(T, dropParen(node.comp2))
   		node.mc = 'f' // the node is finished, this gives it a check
   		}
		else if ( pass < 1 ) continue
		else if ( mc == 'v' ) {
			node.mc = 'f'
			branching()
			addArray(currArray,dropParen(node.comp1))
			if (!quit) addArray(currArray,dropParen(node.comp2))
			}	
		else if ( mc == '>' ) {
			node.mc = 'f'
			branching()
			addArray(currArray,'~' + node.comp1)
			if (!quit) addArray(currArray,dropParen(node.comp2))
			}
		else if ( mc == '=' ) {
			node.mc = 'f'
			branching()
			addArray(currArray, dropParen(node.comp1), dropParen(node.comp2) )
			if (!quit) addArray(currArray,'~' + node.comp1, '~' + node.comp2)
			}
		else if ( mc == '~=' ) {
			branching()
			node.mc = 'f'
			addArray(currArray, '~' + node.comp1, dropParen(node.comp2) )
			if (!quit) addArray(currArray,dropParen(node.comp1), '~' + node.comp2)
			}
		else if ( pass < 2 ) continue
		else if ( mc == '%' ) {
   		c = null
			for ( var k=0; k<21; k++ ) { 
   			if (consInTree.indexOf(constants.charAt(k))==-1) {
   				var c = constants.charAt(k)
   				break
   				}
				}
			if ( c == null ) quit = true
 			else {
				node.mc = 'f'
 				var v = node.sent.charAt(2) // the variable of quantification
				var sI = sub(c,v,node.sent)
   			addNode(T, sI)
   			}
		}
		else if ( pass < 3 ) continue
		else if ( node.mc.charAt(0) == '^' ) {
			var v = node.sent.charAt(2) // the variable of quantification
			consInBs = detCons(currArray)
			if ( consInBs.length == 0 ) consInBs = 'a'
			for ( var j=0; j<consInBs.length; j++ ) {
				var c = consInBs.charAt(j)
   			if ( node.mc.indexOf(c) == -1) {
   				var sI = sub(c,v,node.sent)
   				node.mc += c
   				var simp = addNode(T, sI)
   				if ( simp != '~' && simp != null  ) retry = true 
   				}
				}
			}
		}
}

function detCons(n) { // n is array number; returns constants in any branch through that array
var y = branches.split('|')
var x = ',' + n + ','
var all = ''
var consts = ''
for ( var i=1; i<y.length-1; i++ ) {
   if (y[i].indexOf(x)>-1) all += y[i]
	}
for ( var j=0; j<21; j++ ) {	 // looping through constants
	var c = constants.charAt(j)
   for ( var i=0; i<=arrayNum; i++ ) { // looping thru the array
   	if (all.indexOf(',' + i + ',')>-1 && Constant[parseInt(i)].indexOf(c)>-1 ) consts += c
		}
	}
return consts
}

function sub(c,v,sent) { // removes quantifier -- mlo -- of sent  and substitutes c for v
sent = sent.substring(4)
for ( var i=0; i<sent.length; i++ ) {
   if ( sent.charAt(i) == v ) sent = sent.substring(0,i) + c + sent.substring(i+1)
	}
return dropParen(sent)
}

function Node(s) { //set the tree node giving a sentence, instantiated constants, main connective
while ( s.substring(0,2) == '~~' ) {
	s = s.substring(2) // removes double negations from far left
	s = dropParen(s)
	}
mainLO(s)  // ow known as c
	if ( c == '~'  ) { // no '~~'s allowed by dblNeg. So, 
		if ( s.charAt(2) == '%') {
			s = '(^' + s.charAt(3) + ')~' + s.substring(5)
			this.mc = '^'
			this.sent = s
			}
		else if ( s.charAt(2) == '^') {
			s = '(%' + s.charAt(3) + ')~' + s.substring(5)
			this.mc = '%'
			this.sent = s
			}
		else if ( s.charAt(1) == '(' || s.charAt(1) == '[' ) { // to work toward ~> or ~v
			mainLO(s.substring(2,s.length-1))
			var comp1 = s.substring(2,p+2); var comp2 = s.substring(p+3,s.length-1)
			if ( c == 'v' ) {
				s = '~' + comp1 + '&~' + comp2
				this.sent = s
				this.mc = '&'
				this.comp1 = '~' + comp1
				this.comp2 = '~' + comp2
				}
			else if ( c == '>' ) {
				s = comp1 + '&~' + comp2
				this.sent = s
				this.mc = '&'
				this.comp1 = comp1
				this.comp2 = '~' + comp2
				}
			else if ( c == '&' ) {
				s = '~' + comp1 + 'v~' + comp2
				this.sent = s
				this.mc = 'v'
				this.comp1 = '~' + comp1
				this.comp2 = '~' + comp2
				}
			else if ( c == '=' ) {
				this.mc = '~='
				this.sent = s
				this.comp1 = comp1
				this.comp2 = comp2
			}
		}	 
	else {
		this.sent = s
		this.mc = '~'
		}
	}
	else if ( c == '^' || c == '%' ) {
		this.mc = c
		this.sent = s
		this.comp1 = s.substring(4)
		}
	else {
		this.mc = c
		this.sent = s
		this.comp1 = s.substring(0,p)
		this.comp2 = s.substring(p+1)
		}
// this.cons = setInsVals(s)...	
// setConstants in Ti
}
	var p,c // global variables determined by mainLO: c = main conn, p = position
	var BiC = new Array('&','v','=','>')
function mainLO(text) {
	text = dropParen(deSpace(text))
	var left = 0; 
	p = 0; c = null
	outer: 
	 for ( var i=0; i<text.length; i++ ) {
    	if (  text.charAt(i)=='(' || text.charAt(i)=='[' )  left++
    	else if ( text.charAt(i)==')' || text.charAt(i)==']' )   left--
      else if ( left == 0 )   {
       	for ( var j=0; j<4; j++ ) {
       		if ( text.charAt(i) == BiC[j] ) {
          		c = BiC[j];
          		p = i;
          		break outer;
       		}     
       	}
       }
     }
if ( p != 0) return c
else return unaryTest(text)
}

function unaryTest(text) {
	if ( text.charAt(1) == '%' ) { p = 1; c = '%' } 
	else if ( text.charAt(1) == '^' ) { p = 1; c = '^' } 
	else if ( text.charAt(0) == '~' ) {  c = '~' } 
	return c
}