source: experiments/frams/logic/data/scripts/formulas_processing.inc

//This file contains formulas processing functions such as subformulas and variables ``getters''.

function getSubFormulasIndexed(formInd)
{
        var i;
        var stack = Vector.new();
        var setOfSubforms = Vector.new();
        setOfSubforms.add(formInd);
        if(formInd[0] < 4)
        {
                stack = getIndexedMainArgs(formInd);
                for(i = 0; i < stack.size; i++)
                {
                        if(findPlainList(setOfSubforms, stack[i]) == -1)
                                setOfSubforms.add(stack[i]);
                }
        }

        while(stack.size > 0)   
        {
                if(stack[0][0] < 4)
                {       
                        var tempForms = Vector.new();
                        tempForms = getIndexedMainArgs(stack[0]);
                        for(i = 0; i < tempForms.size; i++)
                        {
                                if(findPlainList(setOfSubforms, tempForms[i]) == -1)
                                {
                                        setOfSubforms.add(tempForms[i]);
                                        stack.add(tempForms[i]);
                                }
                        }
                }
                stack.remove(0);
        }
        
        return setOfSubforms;
}

function getVariablesIndexed(setOfSubforms)
{
        var i;
        var variables = Vector.new();
        
        for(i = 0; i < setOfSubforms.size; i++)
                if(setOfSubforms[i][0] > 3 && variables.find(setOfSubforms[i]) == -1)
                        variables.add(setOfSubforms[i]);
        
        
        return variables;
}

function getIndexedMainArgs(formInd)
{
        
        var argsList = Vector.new();
        if(formInd[0] > 0 && formInd[0]  < 4)
        {
                var firstArgStart = Vector.new();
                firstArgStart.add(formInd[1]);
                var firstArg = Vector.new();
                var secondArg = Vector.new();
                
                
                if(firstArgStart[0] > 3)
                {
                        argsList.add(firstArgStart);
                        secondArg = plainListRight(formInd, formInd.size - 2);
                        argsList.add(secondArg);
                }
                else
                {
                        var i;
                        var p = 2, p_temp = 2, e = 1;
                        var check_conj = 1;

                        
                        while(check_conj == 1)
                        {       
                                for(i = e; i < p; i++)
                                {
                                        if(formInd[i] == 0)
                                        {
                                                p_temp++;
                                        }
                                        if(formInd[i] > 0 && formInd[i] < 4)
                                        {
                                                p_temp += 2;
                                        }       
                                }
                                
                                if(p == p_temp)
                                        check_conj = 0;
                                                
                                e = p;
                                p = p_temp;     
                        }
                                
                        firstArg = plainListSubList(formInd, 1, p - 1);
                        argsList.add(firstArg);
                        secondArg = plainListRight(formInd, formInd.size - p);
                        argsList.add(secondArg);
                }
                
                return argsList;
        }
        else
        {
                if(formInd[0] == 0)
                {
                        argsList.add(plainListRight(formInd, formInd.size - 1));
                        return argsList;
                }
                else
                {
                        Simulator.print("There is no proper operator");
                        return Vector.new();
                }
        }
        
}