source: experiments/frams/logic/data/scripts/literals_processing.inc @ 480

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