package statement;

import expression.Node;

public class Handling {
    private Node expression;
    private World first;
    private int currentLvl = 0;

    public Handling(Node expression) {
        this.expression = expression;
        first = new World();
        first.addExpInWorld(this.expression, currentLvl);
        if(handlingWorld(first))
            System.out.println("INSAT");
        else
            System.out.println("SAT");
    }

    public Boolean handlingWorld(World w) {
        currentLvl++;

        if(handlingSeparating(w))
            return true;

        currentLvl++;

        if(handlingBranching(w))
            return true;

        for (int i = 0; i < w.involvedSize(); i++) {
            if(handlingWorld(w.getInvolved(i)))
                return true;
        }

        return false;
    }

    private Boolean handlingSeparating(World w) {
        for (int i = 0; i < w.getSize(); i++) //separated while
            if(!w.isHandling(i))
                if(!separatingPattern(w, i) && w.isTerminal(i) && conflictInWorld(w, i))
                    return true;
        return false;
    }

    private Boolean handlingBranching(World w) {
        for (int i = 0; i < w.getSize(); i++) { //branching while
            if(!w.isHandling(i)) {
                if(branchingPattern(w, i)) {
                    currentLvl++;
                    if(handlingSeparating(w))
                        return true;
                    //currentLvl--;
                }
            }
        }
        return false;
    }

    private Boolean separatingPattern(World w, int i) {
        Node expression = w.getExpression(i);

        if(!expression.haveChild())
            return false;
        Node child = expression.getLeftChild();

        switch (expression.getNode()) {
            case '!' :
                if(!child.haveChild())
                    return false;
                switch (child.getNode()) {
                    case '!' :
                        w.addExpInWorld(child.getLeftChild(), currentLvl);
                        w.handling(i, currentLvl);
                        return true;
                    case '|' :
                        w.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
                        w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
                        w.handling(i, currentLvl);
                        return true;
                    case '>' :
                        w.addExpInWorld(child.getLeftChild(), currentLvl);
                        w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
                        w.handling(i, currentLvl);
                        return true;
                    default:
                        return false;
                }
            case '&' :
                w.addExpInWorld(child, currentLvl);
                w.addExpInWorld(expression.getRigthChild(), currentLvl);
                w.handling(i, currentLvl);
                return true;
            case 'L' :
                if(!w.haveInvolve())
                    return false;
                w.addExpInInvolveWorlds(child, currentLvl);
                return true;
            default:
                return false;
        }
    }

    private Boolean branchingPattern(World w, int i) {
        Node expression = w.getExpression(i);
        int lvl = currentLvl;

        if(!expression.haveChild()) {
            return false;
        }
        Node child = expression.getLeftChild();

        switch (expression.getNode()) {
            case '!' :
                if(!child.haveChild()) {
                    return false;
                }
                switch (child.getNode()) {
                    case '&' :
                        w.handling(i, currentLvl);
                        w.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
                        if(handlingWorld(w)) {
                            removeLvlModification(first, lvl);
                            w.handling(i, currentLvl);
                            w.addExpInWorld(new Node(child.getRigthChild(), null, '!', child.getRigthChild().getLvl()+1), currentLvl);
                            if(handlingWorld(w)) {
                                return true;
                            }
                        }

                        return false;
                    case 'L' :
                        w.handling(i, currentLvl);
                        World x = new World();
                        w.addInvolve(x);
                        x.addExpInWorld(new Node(child.getLeftChild(), null, '!', child.getLeftChild().getLvl()+1), currentLvl);
                        if(handlingWorld(w)) {
                            return true;
                        }
                        return false;
                    default:
                        return false;
                }
            case '|' :
                w.handling(i, currentLvl);
                w.addExpInWorld(child, currentLvl);
                if(handlingWorld(w)) {
                    removeLvlModification(w, lvl);
                    w.handling(i, currentLvl);
                    w.addExpInWorld(expression.getRigthChild(), currentLvl);
                    if (handlingWorld(w)) {
                        return true;
                    }
                }
                return false;
            case '>' :
                w.handling(i, currentLvl);
                w.addExpInWorld(new Node(child, null, '!', child.getLvl()+1), currentLvl);
                if(handlingWorld(w)) {
                    removeLvlModification(w, lvl);
                    w.handling(i, currentLvl);
                    w.addExpInWorld(expression.getRigthChild(), currentLvl);
                    if (handlingWorld(w)) {
                        return true;
                    }
                }
                return false;
            default:
                return false;
        }
    }

    private Boolean conflictInWorld(World w, int i) {
        int comparator = w.getExpression(i).value();
        int comparatorSymbole = w.getExpression(i).symbole();

        for (int j = 0; j < w.getSize(); j++) {
            Node exp = w.getExpression(j);
            if(exp.isTerminal() && comparatorSymbole == exp.symbole() && exp.value() != comparator) {
                return true;
            }
        }
        return false;
    }

    private void removeLvlModification(World w, int lvl) {
        currentLvl = lvl;

        for (int i = w.getSize()-1; i >= 0; i--) {
            if(w.getWhileLvl(i) >= lvl) {
                w.removeExpression(i);
            } else if(w.getHandling(i) >= lvl) {
                w.handling(i,0);
            }
        }

        for (int i = w.involvedSize()-1; i >= 0; i--) {
            removeLvlModification(w.getInvolved(i), lvl);
            if(w.getInvolved(i).isEmpty())
                w.removeInvolve(i);
        }
    }
} // L(a|b)>(La|Lb)