import java.util.Vector;
import java.util.Collections;
import java.util.Iterator;
import java.util.StringTokenizer;
import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;

// each literal is a string containing atoms or negation of atoms
// for example "p" or "~q". 
// Literals are case sensitive. i.e., q and Q are different
class Literal 
{
    private String atom = "";
    public Literal()
    {
        
    }
    public Literal(String s)
    {
        atom = s;
    }
    
    public void set(String s)
    {
        atom = s;
    }
    public String get()
    {
        return atom;
    }
    public Literal getNot() // get the NOT of the literal
    {
        String s = "";
        if(atom.charAt(0) == '~')           // then this is a negative literal
        {
            s = s + atom.substring(1);      // make it positive
        }
        else                                // this is a positive literal
        {
            s = "~" + atom;                 // make it negataive
        }
        return new Literal(s);
    }
    
    public boolean equals(Object o)
    {
        return atom.equals(((Literal)o).get());
    }    
}

class Clause implements Comparable
{
    /*  literals are stored as Vector of Literal objects
        A zero sized vector means the clause to be False
     */
    private Vector literals = new Vector();
    private int parent[] = {-1,-1}; // parent clauses (from which this has been resolved)
    private int index = -1;         // original index of this clause in the sequence

    // Constructors
    public Clause()
    {
        
    }
    
    public Clause(Vector l)
    {
        literals = l;
    }
    
    // Initialization
    public void init()
    {
        literals = new Vector(); 
        parent[0] = parent[1] = -1; 
        index = -1;         
    }
    
    // set and get methods
    public void setLiterals(Vector l) 
    {
        literals = l;
    }
    
    public Vector getLiterals()
    {
        return literals;
    }
    
    // adds one or more disjunction 
    public void addLiterals(Literal l) 
    {
        literals.add(l);
    }
    
    public void setParents(int p1, int p2)
    {
        parent[0] = p1;
        parent[1] = p2;
    }
    public int[] getParents()
    {
        return parent;
    }
    
    public void setIndex(int i)
    {
        index = i;
    }
    public  int getIndex()
    {
        return index;
    }
    
    public Clause isResolvable(Clause c) // is c resolvable with this
    {
       	/*** TO BE IMPLEMENTED  ***/
        /* for each literal in Clause c, find whether a negative exists in "this.literals"
         *      if found then 
         *               resolve two clauses using resolution rule 
         *               return resolved clause
         * if not found then 
         *       return null;
         */
    } // end public Clause isResolvable(Clause c)
    
    public Clause resolve(Clause c) // resolve c with this
    {
        return isResolvable(c);
    }
    public boolean equals(Object o)
    {
        Vector v1 = ((Clause)o).getLiterals();
        Vector v2 = this.literals;
        int i;
        // Check whether all of v1 is in v2
        for(i = 0; i < v1.size() ; i ++)
        {
            if(!v2.contains(v1.get(i)))
                return false;
        }
        // Check whether all of v2 is in v1
        for(i = 0; i < v2.size() ; i ++)
        {
            if(!v1.contains(v2.get(i)))
                return false;
        }
        return true;
    }
    public int compareTo(Object o)
    {
        return this.index - ((Clause)o).getIndex();
    }
    public String toString()
    {
        String s = "";
        if(literals.size() > 0)
        {
            for(int i = 0; i < literals.size(); i ++)
            {
               s += ((Literal)literals.get(i)).get() + " ";
            }
        }
        else
        {
            s = "False";
        }
        return s;
    }
    
}
public class TheoremProver {
    
    private Vector clauses = new Vector();
    private Vector finalClauses = new Vector();
    int lastIndex = 0;
    /** Creates a new instance of TheoremProver */
    public TheoremProver() {
    }
    // read initial clauses from file
    public void readClauses(String fname)
    {
        try{
            BufferedReader in = new BufferedReader(new FileReader(fname));
            String line = "";
            Vector literals = new Vector();
            boolean toAdd = true;
            int index = 0;
            
            // read lines from the file
            while((line = in.readLine()) != null)
            {
                //tokenize the literals in each line and add to literal
                index ++; // new clause
                
                StringTokenizer st = new StringTokenizer(line," ");
                literals = new Vector();
                toAdd = true;
                while(st.hasMoreTokens())
                {
                    String s = st.nextToken();                  // next literal to be inserted
                    if(s.equalsIgnoreCase("TRUE"))              // then a true clause, ommit the whole clause 
                    {
                        toAdd = false;
                        break;
                    }
                    else if (s.equalsIgnoreCase("FALSE"))       // then ommit this literal (makes no sense adding)
                    {
                    }
                    else literals.add(new Literal(s));
                }
                // now create a new clause
                if(toAdd) // then add this clause
                {
                    Clause cl = new Clause(literals);
                    cl.setIndex(index-1);
                    // add to the list of the current clauses
                    clauses.add(cl); 
                    System.out.println(cl.toString());
                }
            }
        }
        catch (IOException e) {
            System.out.println(e.getMessage());
        }        
    }
    
    // apply resolution
        public boolean resolve()
    {
        /*** TO BE IMPLEMENTED ***/
        /* for each clause c1, find another clause c2 that may be resolved with c1
         *      let r be the resolved clause 
         *      set parents of r to be c1 and c2
         *      add r to the clause list if it is not already there
         *      if r == 'FALSE' then return true
         * return false (no 'FALSE' clause found)
         */                                
    }//public void resolve()

    
    // write resolved clauses to file
    public void writeClauses(boolean success, String outFile)
    {
                    
        try{
            BufferedWriter out = new BufferedWriter(new FileWriter(outFile));
            if(success == false)
            {
                out.write("Theorem could not be proved");
            }
            else
            {
                int i,j;
                // Add only the relevant clauses to the final clause
                             
		finalClauses = new Vector();
                Vector v = new Vector();
                v.add(clauses.get(clauses.size()-1)); //Add the False Clause
                //Apply BFS to get all related clauses
                while(!v.isEmpty())
                {
                    Clause c = (Clause)v.remove(0); 
                    if(!finalClauses.contains(c))
                    {
                        finalClauses.add(c);        
                        System.out.println("index: " + c.getIndex() + ", parents: " + c.getParents()[0] + "," + c.getParents()[1]);
                        System.out.println("Clause size: " + clauses.size());
                        if(c.getParents()[0] != -1) 
                        {                        
                            v.add(clauses.get(c.getParents()[0]));
                            v.add(clauses.get(c.getParents()[1]));
                        }
                    }
                }
                                
                System.out.println("FinalClauses size: " + finalClauses.size());
                Collections.sort(finalClauses);
                for(i = 0; i < finalClauses.size(); i ++)
                {
                    Clause cl = (Clause)finalClauses.get(i);
                    System.out.println(cl.toString());                    
                    
                    out.write((cl.getIndex() + 1)+".\t");
                    out.write(cl.toString()+"\t");
                    if(cl.getParents()[0] != -1) // then has parents
                    {
                        out.write("{" + (cl.getParents()[0] + 1) + "," + (cl.getParents()[1] + 1) + "}\n");
                    }
                    else
                    {
                        out.write("{}\n");
                    }
                }//for(i = 0; i < finalClauses.length; i ++)
                out.write("size of final clause set: " + lastIndex + "\n");
            }//else
            out.close();
        }//try
        catch(IOException e)
        {
            System.out.println(e.getMessage());
        }        
    }
    
    
     
    public static void main(String[] args) {
    
        if(args.length != 2) 
        {
            System.out.println("Total args = " + args.length);
            System.out.println("Usage: <input_file> <output_file>");	    
            return;
        }
        else 
        {
            TheoremProver tp = new TheoremProver();	    
            tp.readClauses(args[0]);
            boolean success = tp.resolve();
            tp.writeClauses(success, args[1]);                            
            System.out.println("Run complete..Please see output");
        }
    }    
}