/*   treeIdentity.js

Uses threads in a tree like structure to constuct interpretations
______________________________________________________________

*/
		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 branches = threads
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 = "   Finished, open branches?"
var endNum
if (typeof endNum != 'number') endNum = 6000
if (typeof branchMax != 'number') branchMax = 6000


	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   MAKE MORE EFFICIENT BY CLEANING THE NET *before* FINISHING CHECKcLOSE()
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
contraI = false
if (sent.charAt(1) == 'I') contraI = ( sent.length == 4 && sent.charAt(2) == sent.charAt(3)) ? true : false // check to see if we have self contradiction ~Ixx
if (!contraI) {
elim = ''
sent = ( type == '~' ) ? sent.substring(1) : '~'+ sent
		outer:
	for ( var i=0; i<t.length; i++ ) { // i is the array number      MAKE MORE EFFICIENT BY EXCLUDING ARRAYS NOT PAIRED WITH ARRAYx???
			inner:
		for ( var j=0; j<t[i].length; j++ ) { // j is the sentence number in array i
   		if (t[i][j].sent == sent) {
   			if ( i == arrayX ) {// if the array is self contradictory we can dump it at beginning of outer in checkClose()
   				contraI = true
   				break outer
   				}
   			else {
   				elim += '(' + i + ')'
   				rewrite = true
   				}
   			break inner
   			}
			}   
		}
	}
}

	var opn,contraI
	ids = new Array
	ids[0] = ''
function checkClose(arrayX,sent,type) { // *misnomer*: checks to see if a thread is FINISHED (open or closed)



if ( arrayX == '1' && sent == 'Cd' ) { //REMOVE
   status = 'Cd'
}



if (branches.length < branchMax) { // begin of check
var rewrite = false, chkI = false //, eqCons = '', addIDs = ''
cleanseNet(arrayX,sent,type)
if ( type == 'a' ) {
	if (sent.charAt(0) == 'I' ) { //To identify constants
		if ( sent.charAt(1) == sent.charAt(2) ) {
			return false // end checkClose() if Ixx is the added sentence
			}
		else ids[arrayX] += '(' + sent.substring(1,3) + ')' // names in added Identity alpabetized
		chkI = true
		}
	}
	var y = branches.split('|') // creates an array of branches
	var x = ',' + arrayX + ',' 
	outer:
for ( var i=1; i<y.length-1; i++ ) { // loop over threads (y[i] gives the thread array numbers)
   if (y[i].indexOf(x)>-1) { // if branch y[i] includes arrayX
   	if ( contraI ) {
  	 		y[i] = ''
   		rewrite = true
   		opn = false
   		continue outer
			}
		else {  
		opn = (splitTrack==1 && checkOpen == true ) ? true : false // check for open (so far finished) branch unless branching (e.g., for =) incomplete, i.e., splitTrack == 0
   	var z = y[i].split(',')
   	var consInB = ''
   	var noID = ( idThrd(z) == '' ) ? true : false // true for id's between names in the arrays of z of i's thread
   	var arrayI = new Array // an array of thread's nodes with atomic sentences that may require ids (defined in sentences loop)
   	var arrayIneg = new Array // an array of thread's nodes with neg atomic sentences that may require ids (defined in sentences loop)
   		inner:   	
	for ( var j=1; j<z.length-1; j++ ) { // z[j] ranges over all array numbers in branch i
		if (elim.indexOf( '(' + z[j] + ')' ) > -1) { // cleans in accordance with cleanseNet()
			y[i]=''
			rewrite = true
			opn = false
			continue outer
			}
countUp(" ...checking for closure...")
   		consInB += Constant[z[j]] // add  constants in array z[j] to the constants in the thread
   		if ( noID ) continue inner
   			sentences:
   		for ( var k=0; k<t[z[j]].length; k++ ) { // k ranges over the array z[j]'s elements
   			var currNode = t[z[j]][k]
   			var currSent = currNode.sent
   			if (chkI ) {
   				if ( currNode.mc == null  ) arrayI[arrayI.length] = currSent
   				else if ( currNode.mc == '~'  ) arrayIneg[arrayIneg.length] = currSent.substring(1)
   				}
   			var compareSent, truncSent  // misnomer: these will be a string of names only
   			if ( type == 'a' && currNode.mc == '~' && sent.charAt(0)==currSent.charAt(1) && sent.length+1 == currSent.length )  {
   				compareSent = currSent.substring(2) // current sentence a possible negation of sent (mod identity of names)
   				truncSent = sent.substring(1)
   				}
				else if ( type == '~' && currNode.mc == null && sent.charAt(1)==currSent.charAt(0) && sent.length == currSent.length+1 ) { // sent a possible negation of current sent (mod identity of names)
					truncSent = sent.substring(2)
					compareSent = currSent.substring(1)
					}
				else continue sentences // move on to next sentence in array z[j] and thread y[i]
   			if ( compareSent == truncSent || Eq(compareSent, truncSent) ) {  // if strings of names are idnetical or in equivalence class we've a contradiction 
    				y[i] = ''
   				rewrite = true
   				opn = false
   				continue outer
   				}
   			}
   		}
   	if (arrayI.length>0 && arrayIneg.length>0) { //there are sentences to consider for ids
   		for ( var k=0; k<arrayI.length; k++ ) {
   			for ( var l=0; l<arrayIneg.length; l++ ) {
   				if ( arrayI[k].charAt(0) == arrayIneg[l].charAt(0) && Eq( arrayI[k].substring(1),arrayIneg[l].substring(1) ) ) {
   					y[i] = ''
   					rewrite = true
   					opn = false
   					continue outer
   					}
   				}
   			}	
   		}
   	}
	if (checkOpen) {
   	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') {
   				countUp("Looking 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 // branch is not finished
   					continue outer
   					}
   				}
			  }
			}
		}
	if (opn) {
   	msg += "\nThere is a finished, open thread: " + i + " of " + branches // TESTING PURPOSES
   	quit = true
  		result = 'open'
   	break outer
 		}
   }
}
if (rewrite) branches = y.join('|')
} // end of check
else {
	endNum = counter
	countUp(" ... the thread count is getting high...")
	}
}

	var pass // global variable to keep track of passes (through workArray() ) as mlo's change 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
			}
	}
}

	var idsInCurrThrd, idStrg = ''
function idThrd(z) { // to determine the equivalence classes of thrd from ids[0] and z the array of arrays in thread
	for ( var j=1; j<z.length-1; j++ ) { // z[j] ranges over all array numbers in branch i from checkClose()
		idStrg += ids[z[j]]
		}
	idsInCurrThrd = (idStrg.length>0) ? idStrg.substring(1,3) : ''
	idStrg = idStrg.substring(4)
	while ( idStrg.length>0 ) {
   	var a = idStrg.charAt(1), b = idStrg.charAt(2), i1 = idsInCurrThrd.indexOf(a),i2 =idsInCurrThrd.indexOf(b)  // the next two to names to consider
		if ( i1 > -1 &&  i2 == -1 ) idsInCurrThrd = idsInCurrThrd.substring(0,i1) + b + idsInCurrThrd.substring(i1)
		else if ( i2 > -1 &&  i1 == -1 ) idsInCurrThrd = idsInCurrThrd.substring(0,i2) + a + idsInCurrThrd.substring(i2)
		else if ( i2 == -1 &&  i1 == -1 )  idsInCurrThrd += '|' + a + b
		idStrg = idStrg.substring(4) // truncate finished portion
		}
return idsInCurrThrd
}

function Eq(s1,s2) {  // s1 and s2 are strings of names, assumes idThrd()'s been run
w = idsInCurrThrd.split('|')	
	outer1:
for ( var j=0; j<s1.length; j++ ) { // j ranging over position in the strings s1 and s2
	var c1 = s1.charAt(j), c2 = s2.charAt(j) //, equal = true
	if ( c1 == c2 ) continue
   for ( var i=0; i<w.length; i++ ) {  // w[j] ranges over thrd's equivalence classes of names
   	var i1 = w[i].indexOf(c1), i2 = w[i].indexOf(c2)
		if ( i1 >-1 || i2 >-1  ) {
			if ( i1 >-1 && i2 >-1 ) continue outer1
			else return false
			}
		}
	return false
	}
return true
}

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
ids[arrayNum] = ''
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][t[arrayNum].length] = newNode2
	sent2 = newNode2.sent
	//ids[arrayNum] = ''
	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)
	}
stuff += branches + '\n' // REMOVE
pass = 0
}

function countUp(message) {
	counter++
	if (counter%100 == 0) status = counter + message
	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
		}
	}
}


	var counter = 0
	var splitTrack = 1 //  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
countUp("Working the tree")
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 == '&' ) {
   		addNode(T, dropParen(node.comp1))
   		node.mc = 'f' // the node is finished, this gives it a check
   		addNode(T, dropParen(node.comp2))
   		}
		else if ( pass < 1 ) continue
		else if ( mc == 'v' ) {
			node.mc = 'f'
			branching()
			addArray(currArray,dropParen(node.comp1))
			addArray(currArray,dropParen(node.comp2))
			}		
		else if ( mc == '>' ) {
			node.mc = 'f'
			branching()
			addArray(currArray,'~' + node.comp1)
			addArray(currArray,dropParen(node.comp2))
			}
		else if ( mc == '=' ) {
			node.mc = 'f'
			branching()
			addArray(currArray, dropParen(node.comp1), dropParen(node.comp2) )
			addArray(currArray,'~' + node.comp1, '~' + node.comp2)
			}
		else if ( mc == '~=' ) {
			branching()
			node.mc = 'f'
			addArray(currArray, '~' + node.comp1, dropParen(node.comp2) )
			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)
		}
}

	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
}