/*
 * To change this template, choose Tools | Templates
 * and open the template in the editor.
 */
package transformacie;

import data.*;

/**
 *
 * @author chislim
 */
public class PrenexovyTvar
{

    String _ss = "";
    public int lavy = 1;

    public PrenexovyTvar()
    {
       Uzol.f.vypis3("\n\nPRENEXOVY TVAR \n");
    }
    
    public void runPrenexovyTvar(Uzol a)
    {
     
        _ss = "";
        prenex(a);

        Uzol.f.vynulujSs();
        a.vypis();

        
        while (!((Uzol.f.getSs()).equals(_ss))) 
        {
            Uzol.f.vypis3("\n");
            _ss = Uzol.f.getSs();
            prenex(a);
            Uzol.f.vynulujSs();
            a.vypis();
          
        }
        
    }

    public void prenex(Uzol u) 
    {
       
        Uzol v;
        v = u;
       
        while (!(v instanceof UzolOperacia))
        {
           
            if (v instanceof UzolOperand) 
            {
                break;
            }
            v = v.lavy;
        }

        if (v instanceof UzolOperacia) 
        {
            najdiKvant(v);
        }

    }

    public void najdiKvant(Uzol u)
    {
       
        if (u instanceof UzolUnarny) 
        {
 
            if ((((UzolUnarny) u).getUnarna() == Utils.velky) || (((UzolUnarny) u).getUnarna() == Utils.maly)) 
            {
                Uzol syn = u.otec;
                Uzol no = najdiNovehoOtca(u);
                
                if (najdiNajblizsiuOperaciu(syn) != null) 
                {
                    if (pocetNegacii(syn)==1) 
                    {
                        if (((UzolUnarny) u).getUnarna() == Utils.velky)
                            {
                                ((UzolUnarny) u).setUnarna(Utils.maly);
                            }   
                        else    ((UzolUnarny) u).setUnarna(Utils.velky);
                    }
                    //f.vypis("najblizisia operacia je "+((UzolOperacia)najdiNajblizsiuOperaciu(syn)).sign);
                    //  f.vypis("nie je to null");
                    
                    if (najdiNajblizsiuOperaciu(syn) instanceof UzolOperacia) 
                    {
                       
                        if (((UzolOperacia) najdiNajblizsiuOperaciu(syn)).getSign() == Utils.implikacia) 
                        {
                            //      f.vypis("menenie");
                            
                            if ((lavySyn(u)) && (((UzolUnarny) u).getUnarna() == Utils.velky))
                            {
                                ((UzolUnarny) u).setUnarna(Utils.maly);
                            } 
                            else if ((lavySyn(u)) && (((UzolUnarny) u).getUnarna() == Utils.maly))
                            {
                                ((UzolUnarny) u).setUnarna(Utils.velky);
                            }
                        }
                    }
                }
                
                //zmazanie z povodnej pozicie                
                u.lavy.setOtec(u.otec);
               
                if (u.otec instanceof UzolUnarny)
                {
                    ((UzolUnarny) u.otec).setLavySyn(u.lavy);
                }
               
                if (u.otec instanceof UzolOperacia) 
                {
                   
                    if (u.equals(u.otec.lavy)) 
                    {
                        ((UzolOperacia) u.otec).setLavySyn(u.lavy);
                    } 
                    else
                    {
                        ((UzolOperacia) u.otec).setPravySyn(u.lavy);
                    }
                }

                //danie o uroven vyssie
                u.setOtec(no.otec);
                ((UzolUnarny) u).setLavySyn(no);
               
                if (no.otec instanceof UzolOperacia) 
                {
                   
                    if (no.equals(no.otec.lavy))
                    {
                        no.otec.lavy = u;
                    } 
                    else 
                    {
                        no.otec.pravy = u;
                    }
                } 
                else 
                {
                    no.otec.lavy = u;
                }
                no.setOtec(u);


            }
        }
        
        lavy = 1;
        
        if (u.lavy != null) 
        {
            najdiKvant(u.lavy);
        }

        if (u.pravy != null) 
        {
            najdiKvant(u.pravy);
        }
    }

    public Uzol najdiNovehoOtca(Uzol u) 
    {
        
        Uzol w = u;
        
        while ((!(w.otec instanceof UzolOperacia)) && (w.otec != null))
        {
            w = w.otec;
        }

        if (w.otec != null)
        {
            w = w.otec;

            if (w.otec instanceof UzolUnarny) 
            {
                
                if ((((UzolUnarny) w.otec).getUnarna() != Utils.negacia) || (((UzolUnarny) w.otec).getUnarna() == 'R')) 
                {
                    return w;
                }
                else 
                {
                    return w.otec;
                }
            }
           
            if (w.otec instanceof UzolOperacia) 
            {
                return w;
            }
        }
        return u;
    }

    public Uzol najdiNajblizsiuOperaciu(Uzol u)
    {
        
        Uzol w = u;
        
        while ((!(w instanceof UzolOperacia)) && (w.otec != null)) 
        {
            w = w.otec;
        }
        return w;
    }
    
      public int pocetNegacii(Uzol u)
    {
        int poc=0;
        
        Uzol w = u;
        
        while ((!(w instanceof UzolOperacia)) && (w.otec != null)) 
        {
            if (w instanceof UzolUnarny)
                if (((UzolUnarny)w).getUnarna()==Utils.negacia) poc++;
            w = w.otec;
            
        }
        return poc;
    }

    public boolean lavySyn(Uzol u)
    {
        Uzol w = u;

        while ((!(w.otec instanceof UzolOperacia)) && (w.otec != null)) 
        {
            w = w.otec;
        }

        if (w.otec != null) 
        {
           
            if (w.equals(w.otec.lavy)) 
            {
                return true;
            } 
            else 
            {
                return false;
            }
        }
        return true;
    }
}
