//This file contains synthetic tableau generation functions and support methods.

function generateSyntheticInfFromSetIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
{
	var i,j;
	
	var tableau = generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed);
	
	var inferences = Vector.new();
	getSyntheticInferences(tableau, inferences);
	
	return inferences;
}

function generateSyntheticTableauIndexed(formulasIndexed, subformulasIndexed, variablesIndexed)
{
	var i;
	var stack = Vector.new();
	var tableau = Vector.new();
	var stop = 0;
	var result = Vector.new();
	
		tableau.add([1]);
		tableau.add([1]);
		
		
		stack.add(tableau[0]);
		stack.add(tableau[1]);
		
		var branching = createSyntheticBranchingIndexed(variablesIndexed[0]);
		tableau.get(tableau.size - 2).add(branching[0]);
		tableau.get(tableau.size - 1).add(branching[1]);
		
		result.add(tableau[0]);
		result.add(tableau[1]);
	
		tableau = stack[0];
		
	while(stack.size > 0)
	{
		applyRulesToInferenceIndexed(tableau, subformulasIndexed);
		stop = searchFormsThroughInference(formulasIndexed, tableau);
		stack.remove(0);
		
		if(stop == 1)
		{		
			if(stack.size > 0)
			{
				tableau = stack[0];
				continue;
			}	
		}	
		if(variablesIndexed.size > tableau[0])
		{	
			var branching = createSyntheticBranchingIndexed(variablesIndexed[tableau[0]]);
			
			tableau.add([tableau[0] + 1]);
			tableau.add([tableau[0] + 1]);
			
			for(i = 1; i < tableau.size - 2; i++)
			{	
				tableau[tableau.size - 1].add(tableau[i]);
				tableau[tableau.size - 2].add(tableau[i]);
			}
			
			tableau[tableau.size - 1].add(branching[0]);
			tableau[tableau.size - 2].add(branching[1]);
			
			stack.add(tableau[tableau.size - 2]);
			stack.add(tableau[tableau.size - 1]);
			
			var tableau_size_temp = tableau.size - 2; 
		
			for(i = 0; i < tableau_size_temp; i++)
			{
				tableau.remove(0);
			}
			tableau = stack[0];	
		}
	}	
	return result;
}



function createSyntheticBranchingIndexed(variableIndexed)
{	
	var branching = Vector.new();
	
	branching.add([[variableIndexed[0]],[[variableIndexed[0]]]]);
	branching.add([[0,variableIndexed[0]], [[0, variableIndexed[0]]]]);
	
	return branching;
}

function applyRulesToInferenceIndexed(inferenceIndexed, subformulasIndexed)
{
	var i,j;
	var check = 1;
	var tempForms = Vector.new();
	var merged = Vector.new();
		
	while(check == 1)
	{
		check = 0;
		merged = mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed);
		//TODO modernizne temp
		for(i = 1; i < inferenceIndexed.size; i++)
		{
			for(j = 1; j < inferenceIndexed.size; j++)
			{
					tempForms.add(syntheticNegRule(inferenceIndexed[i]));
					tempForms.add(syntheticImplANBRule(inferenceIndexed[i], inferenceIndexed[j]));
					tempForms.add(syntheticAltNANBRule(inferenceIndexed[i], inferenceIndexed[j]));
					tempForms.add(syntheticConjABRule(inferenceIndexed[i], inferenceIndexed[j]));	
			}
				
			for(j = 1; j < merged.size; j++)
			{
				tempForms.add(syntheticImplNARule(inferenceIndexed[i], merged[j]));
				tempForms.add(syntheticImplBRule(merged[j], inferenceIndexed[i]));
				tempForms.add(syntheticAltARule(inferenceIndexed[i], merged[j]));
				tempForms.add(syntheticAltBRule(merged[j], inferenceIndexed[i]));
				tempForms.add(syntheticConjNARule(inferenceIndexed[i], merged[j]));
				tempForms.add(syntheticConjNBRule(merged[j], inferenceIndexed[i]));
			}
		}
		for(i = 0; i < tempForms.size; i++)
		{
			if(validateSynthesizedFormulaIndexed(tempForms[i], subformulasIndexed) == 1)
			{
				for(j = 1; j < inferenceIndexed.size; j++)
					if(verifyPlainListsIdentity(tempForms[i][0], inferenceIndexed[j][0]) == 1)
						continue 2;
							
				inferenceIndexed.add(tempForms[i]);
				check = 1;
			}
			
		}
		
		merged.clear();
		tempForms.clear();
	}
}
function searchFormsThroughInference(formulasIndexed, inferenceIndexed)
{
	var i,j;
	var stop = 0;
	var negFormIndexed = Vector.new();
	
	for(i = 0; i < formulasIndexed.size; i++)
	{
		
		for(j = 1; j < inferenceIndexed.size; j++)
		{
			negFormIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
			if(verifyPlainListsIdentity(formulasIndexed[i], inferenceIndexed[j][0]) == 1 || verifyPlainListsIdentity(negFormIndexed, inferenceIndexed[j][0]) == 1)
			{
				stop = 1;
				continue 2;
			}
		}
		return 0;
	}
	
	return stop;
}

function mergeInferencesSubformulasIndexed(inferenceIndexed, subformulasIndexed)
{
	var result = Vector.new();
	var i,j;
		
	for(i = 0; i < inferenceIndexed.size; i++)
	{
		result.add(inferenceIndexed[i]);
	}
		
	for(i = 0; i < subformulasIndexed.size; i++)
	{
		for(j = 1; j < inferenceIndexed.size; j++)
		{
			if(subformulasIndexed[i] == inferenceIndexed[j][0])
			{
				continue 2;
			}
		}
		
		result.add(Vector.new());
		result.get(result.size - 1).add(subformulasIndexed[i]);					
	}
	
	return result;
	
}


function validateSynthesizedFormulaIndexed(formulaIndexed, subformulasIndexed)
{
	if(formulaIndexed.size < 2)
		return 0;
		
	if(findPlainList(subformulasIndexed, formulaIndexed[0]) != -1)
	{
		return 1;
	}
	else
	{
		
		if(formulaIndexed[0][0] == 0)
		{
			var tempFormula = plainListRight(formulaIndexed[0], formulaIndexed[0].size - 1);
			if(findPlainList(subformulasIndexed, tempFormula) != -1)
				return 1;
		}
	}
	return 0;
	
}

function getSyntheticInferences(tableau, inferences)
{
	
	if(typeof(tableau.get(0)) == "Vector")
	{
		var i;
		
		for(i = 0; i < tableau.size; i++)
			getSyntheticInferences(tableau.get(i), inferences);
			
		return inferences;
	}
	else
	{
		inferences.add(tableau);
		return inferences;
	}
}



function getFailures(inferencesIndexed, formulasIndexed)
{
	var partialTableau = Vector.new();
	var branchesNum = Vector.new();
	var i;
	
	for(i = 0; i < inferencesIndexed.size; i++)
	{
		if(syntheticInferenceFailure(inferencesIndexed[i], formulasIndexed) == 1)
		{
			partialTableau.add(inferencesIndexed[i]);
			branchesNum.add(i);
		}
	}		
	return [partialTableau,branchesNum];
}


function syntheticInferenceFailure(inferenceIndexed, formulasIndexed)
{
	var i,j;
	
	for(i = 1; i < inferenceIndexed.size; i++)
		if(verifyPlainListsIdentity(formulasIndexed[formulasIndexed.size - 1], inferenceIndexed[i][0]))
			return 0;
	
	var negFormulaIndexed = Vector.new();	
	for(i = 0; i < formulasIndexed.size - 1; i++)
		for(j = 1; j < inferenceIndexed.size; j++)
		{
			negFormulaIndexed = plainListCopyInsert(formulasIndexed[i], 0, [0]);
			if(verifyPlainListsIdentity(negFormulaIndexed, inferenceIndexed[j][0]))
				return 0;
		}	
		
	return 1;
}

function checkTableauSuccess(inferences, formulas)
{
	var i;
	for(i = 0; i < inferences.size; i++)
	{
		if(syntheticInferenceFailure(inferences.get(i), formulas) == 1)
		{
				return 0;
		}
	}
		
	return 1;
}

function checkTableValidity(inferences, formulas)
{
	var i;
	for(i = 0;  i < inferences.size; i++)
		{
			if(checkSyntheticInferenceValidity(inferences[i], formulas) == 0)
			{
				return 0;
			}
		}
		
	return 1;
} 

function checkSyntheticInferenceValidity(inference, formulas)
{
	var i,j;
	
	for(i = 0; i < formulas.size; i++)
	{
		for(j = 1; j < inference.size; j++)
		{
			if((verifyPlainListsIdentity(plainListCopyInsert(formulas[i],0,[0]), inference[j][0]) == 1)||( verifyPlainListsIdentity(formulas[i], inference[j][0]) == 1))
			{
				continue 2;
				
			}
		}	
		return 0;
	}
	
	return 1;
}