
/*
 * Prekladac.java
 *
 * Created on Utorok, 2008, február 26, 19:57
 */
package data;
import java.io.*;
import transformacie.Distributivita;

import transformacie.MechanickyPrepis;
import transformacie.PosunNegaciiNadol;
import transformacie.PrenexovyTvar;
import transformacie.Premenovanie;
import transformacie.UpravaKvantifikatorov;
import transformacie.ZrusenieImplikacii;


/**
 *
 * @author  chislim
 */
public class Prekladac extends javax.swing.JFrame
{

    /** Creates new form Prekladac */
    public Prekladac() 
    {
        initComponents();
    }

    /** This method is called from within the constructor to
     * initialize the form.
     * WARNING: Do NOT modify this code. The content of this method is
     * always regenerated by the Form Editor.
     */
    // <editor-fold defaultstate="collapsed" desc="Generated Code">//GEN-BEGIN:initComponents
    private void initComponents() {

        setDefaultCloseOperation(javax.swing.WindowConstants.EXIT_ON_CLOSE);
        setTitle("prekladac kalkul -> Datalog");

        javax.swing.GroupLayout layout = new javax.swing.GroupLayout(getContentPane());
        getContentPane().setLayout(layout);
        layout.setHorizontalGroup(
            layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGap(0, 535, Short.MAX_VALUE)
        );
        layout.setVerticalGroup(
            layout.createParallelGroup(javax.swing.GroupLayout.Alignment.LEADING)
            .addGap(0, 409, Short.MAX_VALUE)
        );

        pack();
    }// </editor-fold>//GEN-END:initComponents
    /**
     * @param args the command line arguments
     */
    

    
    public static void main(String args[])  throws IOException
    {
        String s="";

            final Formular f = new Formular(args[1]);

        java.awt.EventQueue.invokeLater(new Runnable() 
        {
            public void run() 
            {
                f.setVisible(true);
            }
        });

        String line="";
        BufferedReader in;
        try {
        in = new BufferedReader(new FileReader(args[0]));
        line = in.readLine();
        in.close();
   
        } catch (IOException e) {
        e.printStackTrace();
        }
        s=Utils.texToString(line);
      
       
         s = Utils.zmazanieMedzier(s);
        //s=Utils.upravaZatvoriek(s);

        System.out.println(s);

        if (!Utils.spravneUzatvorkovanie(s)) 
        {
            System.out.println("zle uzatvorkovanie");
        }
        else
        {
        
        Uzol a = new UzolUnarny(null, "ROOT ");
        Uzol.f=f;
    
        Parser parser = new Parser(s, f);
        parser.runParser(0, s.length() - 1, a);
        a.vypis();

        Premenovanie premenovanie = new Premenovanie();
        premenovanie.runPremenovanie(a);
        a.vypis();

        PrenexovyTvar prenexovyTvar = new PrenexovyTvar();
        prenexovyTvar.runPrenexovyTvar(a);
 
        ZrusenieImplikacii zrusenieImplikacii = new ZrusenieImplikacii();
        zrusenieImplikacii.runZrusenieImplikacii(a);
        a.vypis();

        UpravaKvantifikatorov upravaKvantifikatorov = new UpravaKvantifikatorov();
        upravaKvantifikatorov.runUpravaKvantifikatorov(a);
        a.vypis();

        PosunNegaciiNadol posunNegaciiNadol = new PosunNegaciiNadol();
        posunNegaciiNadol.runPosunNegaciiNadol(a);
        a.vypis();

        Distributivita distributivita = new Distributivita();
        distributivita.runDistributivita(a);
        a.vypis();

        MechanickyPrepis mechanickyPrepis = new MechanickyPrepis();
        mechanickyPrepis.runMechanickyPrepis(a);
        
        Formular.out.close();
        }
    }
    // Variables declaration - do not modify//GEN-BEGIN:variables
    // End of variables declaration//GEN-END:variables
}



//testovacie vstupy  
// s="∀F((∃V∃C∃L(objednavky(jozo, V)∧dodava(F, V, C, L)))⇒dodava_nieco_jozovi(F))";       
        //    s="∀F((∃F∃C∃L(objednavky(jozo, F)∧∃L(dodava(F, F, C, L))))⇒dodava_nieco_jozovi(F))";              

    
        //s="∀F1(¬∃V∃C∃L(¬objednavky(jozo, V)∧¬dodava(F, V, C, L))⇒dodava_nieco_jozovi(F))⇒vysledok(F))"  ; 
        //s="∀F((∃V∃C∃L(objednavky(jozo, V)∨dodava(F, V, C, L))∧¬dodava_nieco_jozovi(F))⇒vysledok(F))"  ;         
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V)∨DRUHY(F, V, C, L))∧(TRETI(jozo, V)∧STVRTY(F, V, C, L)))⇒vysledok(F))"  ;  
        //s="∀F((∃V∃C∃L(¬dodava_nieco_jozovi(F)∧(¬objednavky(jozo, V)∨¬dodava(F, V, C, L))))⇒vysledok(F))"  ;         
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V)∧DRUHY(F, V, C, L))∧(TRETI(jozo, V)∨STVRTY(F, V, C, L)))⇒vysledok(F))"  ;  

        //s = "∀F((∃V∃C∃L(JEDEN(jozo, V)∨DRUHY(F, V, C, L))∧(TRETI(jozo, V)∨STVRTY(F, V, C, L)))⇒dodava_nieco_jozovi(F))";
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V)∨DRUHY(F, V, C, L))∧(TRETI(jozo, V)∧STVRTY(F, V, C, L)))⇒vysledok(F))"  ;  
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V)∨DRUHY(F, V, C, L))∧TRETI(jozo, V))⇒vysledok(F))"  ;          
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V))∧(TRETI(jozo, V)∧STVRTY(F, V, C, L)))⇒vysledok(F))"  ;  
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V))∧(TRETI(jozo, V)∨∃L(STVRTY(F, V, C, L))))⇒vysledok(F))"  ;          
        //s="∀F((∃V∃C∃L(JEDEN(jozo, V))∨(TRETI(jozo, V)∨STVRTY(F, V, C, L)))⇒vysledok(F))"  ; 


        //s="∀F((∃V∃C∃L(JEDEN(jozo, V)∨(JEDEN(jozo, V)∧DRUHY(F, V, C, L)))∨(TRETI(jozo, V)∧(JEDEN(jozo, V)∨DRUHY(F, V, C, L))))⇒dodava_nieco_jozovi(F))"  ;  

        //s="∀F((¬∀V∃C¬∃L(JEDEN(jozo, V)⇒(**JEDEN(jozo, V)⇒**DRUHY(F, V, C, L)))⇒(TRETI(jozo, V)⇒(*JEDEN(jozo, V)⇒*DRUHY(F, V, C, L))))⇒dodava_nieco_jozovi(F))"  ;  
        //s="∀V1¬(∃V1¬∃C12∃L123¬(objednavky(jozo,V1)∨¬dodava(F,V1, C, L))⇒dodava_nieco_jozovi(F))";
        // s="∀C(((∃C∃T¬(¬dodava(F,pc1,C,L1)∧(C<=15000)))∨(∃C∃E¬(¬dodava(F, pc1, C, L)∧L<=4)))⇒dodava_pc1_do4_alebo_do15000(F))";
        //s="∀F(dodavatel(F,bratislava)⇒dodavatel_ba(F))";       
        //s="∀C(∀F∀pc1(dodava(F, pc1, C, L))⇒dodava_pc1_do4_alebo_do15000(F))";   
        //s="∀C(∀F(dodava(F, pc1, C, L))⇒dodava_pc1_do4_alebo_do15000(F))";   
        //s="∀C((¬dodava(F, pc1, C, L))⇒dodava_pc1_do4_alebo_do15000(F))";   
        //s="∀C(dodava(F, pc1, C, L)⇒dodava_pc1_do4_alebo_do15000(F))";           
       /// s="∀F(∃V∃T∃G¬(((objednavky(jozo,V)∧¬dodava(F,2V, C1, L1))))⇒dodava_jozovi(F))";
        //s="∀F(∃V∀T∀G(((objednavky(jozo,V)∧¬dodava(F,2V, C1, L1))))⇒dodava_jozovi(F))";
        //s="∀F(∀V∀T∃G¬(((objednavky(jozo,V)∧¬dodava(F,2V, C1, L1))))⇒dodava_jozovi(F))";
   //     s="∀F(∀V∃T∃G¬(((objednavky(jozo,V)∧ ∀V(dodava(F,V, T, G)))))⇒dodava_jozovi(F))";
        
        //s="∀F(∀V∃T∃G¬(((objednavky(jozo,V)∧ ∀V(dodava(F,V,G)))))⇒dodava_jozovi(F))";        
        
        //s="∀F(∃V∃C∃L(((A(X1)⇒B(X2))∧(C(X3)⇒D(X4)))∧((E(X5)⇒F(X6))∧(G(X7)⇒H(X8))))⇒vysledok(F))"  ;
      //   s="∀F(∃V∃C∃L(((A(X1)⇒B(X2))∧(C(X3)⇒D(X4)))∨((E(X5)⇒F(X6))∧G(X7)))⇒vysledok(F))"  ;
     //   s="∀F(∃V∃C∃L(((A(X1)⇒B(X2))∧(C(X3)⇒D(X4)))∨((E(X5)⇒F(X6))∧(G(X7)⇒H(X8))))⇒vysledok(F))"  ;
        
        
       // s="∀X3(∀X1∃X2((a(X1)⇒b(X2))∧(c(X2)⇒d(X3)))⇒implikacie(X3))"  ; 

        //prednasky 

        //s="∀F (dodavatel(F, bratislava) ⇒ dodavatel_ba(F))"; 
      //   s="∀F ((∃V∃C∃L (objednavky(jozo, V) ∧ dodava(F, V, C, L))) ⇒ dodava_nieco_jozovi(F))";
        //  s="∀F (((∃C∃L1(dodava(F, pc1, C, L1) ∧ (C<=15000))) ∨ (∃L∃C2(dodava(F, pc1, C2, L) ∧ (L<=4))))⇒ dodava_pc1_do4_alebo_do15000(F))"; 
     //   s="∀F (∃V∃C1∃L1 (objednavky(jozo, V) ∧ ¬dodava(F, V, C1, L1))⇒ dodava_jozovi(F))"; 
       // s="∀X ((man(X) ∧ ((∀Y (animal(Y) ⇒ loves(X, Y))) ⇒ ∃Y(loves(Y, X)))) ⇒ loved_by_someone(X))"; 
       //  s="∀P∀A∀I∀K∀O∀D ((lubi(P,A) ∨ navstivil(I,P,K,O,D)) ⇒ pijani(P))";
      //   s="∀P∀I∀K∀O∀D ((navstivil(I, P, K, O, D) ∧ ¬ nelubi_nic(P))⇒ niekde_necapovali_nic(P))";     


 //  s="∀P(((pijani(P) ∧ ¬ navstivil(I, P, K, O, D)) ∨ (pijani(P) ∧ vsade_capovali_nieco(P))) ⇒ stastni_pijani(P))";
        
         //s="∀P∀K(((pijani(P) ∧ krcmy(K)) ∧ ¬ (∃A (capuje(K,A) ∧ lubi(P,A))))  ⇒ nelubi_nic(P, K))"; //1
        // ∀P∀A∀I∀K∀O∀D [(lubi(P,A) ∨ navstivil(I,P,K,O,D))
         
 // s="∀P∀K(((        (∃A∃I∃K∃O∃D ((lubi(P,A) ∨ navstivil(I,P,K,O,D)))) ∧  (∃A2 (capuje(K,A2)))     ) ∧ ¬ (∃A3 (capuje(K,A1) ∧ lubi(P,A3))))  ⇒ nelubi_nic(P, K))"; //1
         
         //s="∀P∀K(((pijani(P) ∧ krcmy(K)) ∧ (∃A( capuje(K,A) ⇒ ¬lubi(P,A))))  ⇒ nelubi_nic(P, K))"; //2         
          //s="∀P∀K∀A (∀O∀D ¬(navstivil(K,O,D) ⇒ ∀A (¬lubi(P, A) ∧ ¬capuje(K, A))) ⇒ lubi_nieco(P, K))";
    //   s="∀F ((∃M (dodavatel(F, M) ∧ ∀V (objednavky(jozo, V))) ⇒ ∃C∃L dodava(F, V, C, L)) ⇒ dodava_vsetko_jozovi(F))";
  
  //s="∀F (((∃C∃L1(dodava(F, pc1, C, L1) ∧ C<=15000)) ∨ (∃L∃C2(dodava(F, pc1, C2, L) ∧ L<=4))) ⇒ dodava_pc1_do4_alebo_do15000(F))";
 // s="∀F (∃V∃C1∃L1∃M (objednavky(jozo, V) ∧ (dodavatel(F, M) ∧ ¬dodava(F, V, C1, L1)))⇒ dodava_jozovi(F))"      ;
// s="∀F ((∃M ((dodavatel(F, M)) ∧ ∀V (objednavky(jozo, V))) ⇒ ∃C∃L (dodava(F, V, C, L))) ⇒ dodava_vsetko_jozovi(F))";
 //s="∀F (∃M (dodavatel(F, M) ∧ ∀V (objednavky(jozo, V) ⇒ ∃C∃L (dodava(F, V, C, L)))) ⇒ dodava_vsetko_jozovi(F))";
 //s="∀F (∃M (dodavatel(F, M) ∧ ¬(∃V (objednavky(jozo, V)) ∧¬(∃C∃L (dodava(F, V, C, L))))) ⇒ dodava_vsetko_jozovi(F)) ";