source: experiments/frams/logic/data/scripts/synthetic_tableau.inc @ 963

//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;
}