//This file contains literals processing functions such as: entangled literals ``get'' function,
//literals clauses sorting, reduction and filtering functions.


function getEntangledLiterals(inferencesIndexed, formulasIndexed)
{
	var i,j,l;
	var k = 0;
	var entangledLiterals = Vector.new();
	
	for(i = 0; i < inferencesIndexed.size; i++)
	{
		entangledLiterals.add(Vector.new());
		while(k < formulasIndexed.size)
		{
			for(j = 1; j < inferencesIndexed[i].size; j++)
			{
				var negFormIndexed = plainListCopyInsert(formulasIndexed[k], 0, [0]);
				if(verifyPlainListsIdentity(inferencesIndexed[i][j][0], formulasIndexed[k]) || verifyPlainListsIdentity(inferencesIndexed[i][j][0], negFormIndexed))
				{
					for(l = 0; l < inferencesIndexed[i][j][1].size; l++)
						entangledLiterals[i].add(deepCopyList(inferencesIndexed[i][j][1][l]));
					
					continue;
				}
			}
			k++;
		}
		k = 0;
	}
	return entangledLiterals;
}


function cleanEntangledLiterals(entangledLiterals)
{
	var i,j,k;
	var cleaned = Vector.new();
	var check = 0;
	var tempEntangled = Vector.new();
	
	for(i = 0; i < entangledLiterals.size; i++)
	{
		tempEntangled.add(Vector.new());
		
		for(j = 0; j < entangledLiterals[i].size; j++)
			if(findPlainList(tempEntangled[tempEntangled.size - 1], (entangledLiterals[i][j])) == -1)
				tempEntangled[tempEntangled.size - 1].add(entangledLiterals[i][j]);
	}
	
	cleaned.add(tempEntangled[0]);
	for(i = 1; i < tempEntangled.size; i++)
	{
		
		check = 0;
		for(j = 0; j < cleaned.size; j++)
		{
			if(tempEntangled[i].size != cleaned[j].size)
				continue;
			else		
				for(k = 0; k < tempEntangled[i].size; k++)
					if(findPlainList(cleaned[j], tempEntangled[i][k]) == -1)
						continue 2;
						
			check = 1;		
		}
		if(check == 0)
			cleaned.add(tempEntangled[i]);
	}
	return cleaned;
}

function filterOutNonConsistentLiteralsLists(listsOfLiterals)
{
	var i,j,k;
	var result = Vector.new();
	for(i = 0; i < listsOfLiterals.size; i++)
	{
		for(j = 0; j < listsOfLiterals[i].size; j++)
		{
			for(k = j+1; k < listsOfLiterals[i].size; k++ )
			{
				if(verifyPlainListsIdentity(listsOfLiterals[i][j],  plainListCopyInsert(listsOfLiterals[i][k], 0, [0])) == 1 || verifyPlainListsIdentity(plainListCopyInsert(listsOfLiterals[i][j], 0, [0]), listsOfLiterals[i][k]) == 1)
					continue 3;
			}	
		}
		result.add(listsOfLiterals[i]);
	}
	return result;
}

function filterOutRepeatingLiteralsLists(listsOfLiterals)
{
	var result = Vector.new();
	var i,j,k;
	
	for(i = 0; i < listsOfLiterals.size; i++)
	{
		for(j = 0; j < result.size; j++)
		{
			if(listsOfLiterals[i].size == result[j].size)
			{
				
				for(k = 0; k < listsOfLiterals[i].size; k++)
				{
					if(verifyPlainListsIdentity(listsOfLiterals[i][k], result[j][k]) == 0)
						continue 2;
					
				}
				continue 2;
			}
			else
				continue;
		}
		result.add(deepCopyList(listsOfLiterals[i]));
	}
	
	return result;
}


function getSymmetricalDifferences(literalsSets)
{
	var literalsSetsDeepCopy = deepCopyList(literalsSets);
	
	var i,j;
	var mem = 0;
	var indexMem = Vector.new();
	var ijs = Vector.new();
	
	for(i = 0; i < literalsSetsDeepCopy.size; i++)
	{
		mem = 0;
		
		for(j=0; j < literalsSetsDeepCopy.size; j++)
		{
			if(i!=j)
			{	
				var tempIjs = Vector.new();
				if(i > j)
				{
					tempIjs.add(j);
					tempIjs.add(i);	
				}
				else
				{
					tempIjs.add(i);
					tempIjs.add(j);	
				}
				if((literalsSetsDeepCopy[i].size == literalsSetsDeepCopy[j].size)  && (findPlainList(ijs, tempIjs) == -1))
				{
					ijs.add(tempIjs);
					var sd = symDiffOfTwoLiteralsSets(literalsSetsDeepCopy[i], literalsSetsDeepCopy[j]);
					if(sd[0] != null)
					{
						mem = 1;
						literalsSetsDeepCopy.add(sd);
						if(indexMem.find(j) == -1)
							indexMem.add(j);
					}
				}
			}	
		}
		
		if(mem == 1)
		{
			if(indexMem.find(i)==-1)
				indexMem.add(i);
			
		}
	}
	var remliteralsSetsDeepCopy = listRemove(indexMem, literalsSetsDeepCopy);
	return remliteralsSetsDeepCopy;
}


function symDiffOfTwoLiteralsSets(set1, set2)
{
	
	if(set1.size==set2.size)
	{
		var i;
		var candidateSet = deepCopyList(set1);
		
		var j;
		var diffCounter = 0;	
		for(j = 0; j < set2.size; j++)
		{
			if(findPlainList(candidateSet, set2[j]) == -1)
			{
				if(set2[j].size == 2)
				{
					var find = findPlainList(candidateSet, [set2[j][1]]);
						if(find != -1)
						{
							diffCounter++;
							candidateSet.remove(find);
						}
						else
							return [null];
				}
				else if(set2[j].size == 1)
					 {
					 	var find = findPlainList(candidateSet, plainListCopyInsert(set2[j], 0, [0]));
					 	if(find != -1)
						{
							diffCounter++;
							candidateSet.remove(find);
						}
						else
							return [null];
					 }	
			}
			
			if(diffCounter > 1)
				return [null];	
		}
		if(diffCounter == 0)
			return [null];
		
		if(diffCounter==1)
			return candidateSet;
	}
	else
	{
		Simulator.print("The compared sets of literals are of different sizes!");
		return [null];
	}
}

function removeLiteralsSupSets(setsOfLiterals)
{
	var i;
	
	var sorted = sortLiteralsListsBySize(setsOfLiterals);
	for(i = sorted.size - 1; i > -1; i--)
	{
		var j;
		for(j = i - 1; j > -1; j--)
		{

			if(sorted[i].size > sorted[j].size)
			{
				var k;
				
				for(k = 0; k < sorted[j].size; k++)
				{
					if(findPlainList(sorted[i], sorted[j][k]) == -1)
						continue 2;
					
				}
				sorted.remove(i);
				continue 2;
			}
			
		}
	}
	return sorted;
}


function generateBaseHypotheses(entangledLiterals)
{
	var i;
	var literalsCounter = 0;
	var stack = Vector.new();
	var product = Vector.new();
	var tempLiteral = Vector.new();
	var check = 0;
	
	while(!(stack.size == 0 && literalsCounter == entangledLiterals[0].size))
	{ 
		tempLiteral = deepCopyList(entangledLiterals[stack.size][literalsCounter]);
		
		if(tempLiteral[0] != 0)
			tempLiteral = plainListCopyInsert(tempLiteral, 0, [0]);
		else
			tempLiteral = [tempLiteral[1]];
		
		for(i = 0; i < stack.size; i++)
		{	
			if(stack[i][1] != null)
			if(verifyPlainListsIdentity(stack[i][1], tempLiteral) == 1)	
			{
				stack.add([literalsCounter, null]);
				check = 1;
				break;
			}	
		}
		if(check == 0)
		{
			stack.add([literalsCounter, tempLiteral]);
		}
		else
			check = 0;	
	
		if(stack.size == entangledLiterals.size)	
		{	
			product.add(Vector.new());
			
			for(i = 0; i < stack.size; i++)
			{
				if(stack[i][1] != null)
					product[product.size - 1].add(stack[i][1]);
				else
					continue;
			}
			
			literalsCounter = stack[stack.size - 1][0] + 1;
			stack.remove(stack.size - 1);
				
			if(literalsCounter == entangledLiterals[stack.size].size)
			{
				if(stack.size != 0)
				{
					literalsCounter = stack[stack.size - 1][0] + 1;
					while(stack.size != 0 && literalsCounter == entangledLiterals[stack.size - 1].size)
					{
						stack.remove(stack.size - 1);
			
						if(stack.size > 0)
							literalsCounter = stack[stack.size - 1][0] + 1;
						else
							break;
					}
					if(stack.size > 0)
						stack.remove(stack.size - 1);
				}
			}
		}
		else
			literalsCounter = 0;
	}
	
	return product;
}



function sortLiteralsListsBySize(literalsLists)
{
	var i;
	var ranks = Vector.new();
	var numbers = Vector.new();
	var ordered = Vector.new();
	
	for(i = 0; i < literalsLists.size; i++)
	{
		var count = literalsLists[i].size;
		numbers.add(count);
		ranks.add([count,i]);
	}
	var sorted = Vector.new();
	quickSort(numbers,sorted);
	while(sorted.size > 0)
	{
		for(i = 0; i < ranks.size; i++)
			if(sorted[0] == ranks[i][0])
			{
				ordered.add(literalsLists[ranks[i][1]]);
				sorted.remove(0);
				ranks.remove(i);
				break;
			}
	}
	return ordered;
}

function sortLiteralsWithinSets(setOfLiteralsSetsIndexed)
{
	var new = Vector.new();
	var i;
	
	for(i = 0; i < setOfLiteralsSetsIndexed.size; i++)
		new.add(sortLiterals(setOfLiteralsSetsIndexed[i]));
		
	return new;
}

function sortLiterals(setOfLiterals)
{
	var numeric = Vector.new();
	var sortedNum = Vector.new();
	var sortedLiterals = Vector.new();
	var i;
	
	numeric = convertLiteralsToNumbers(setOfLiterals);
	quickSort(numeric,sortedNum);
	sortedLiterals = convertNumbersToLiterals(sortedNum);
	
	return sortedLiterals;
}