package cnf;

import java.io.BufferedReader;
import java.io.BufferedWriter;
import java.io.IOException;
import java.io.Reader;
import java.io.Writer;
import java.util.Iterator;
import java.util.StringTokenizer;

/**
 * A class for reading and writing formulas and solutions in the DIMACS format.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class DimacsIO {

    private DimacsIO() {}
    
    /**
     * Writes the specified CNF with the specified writer.
     */
    public static void writeCNF(CNF cnf, Writer writer) throws IOException {
        BufferedWriter w = new BufferedWriter(writer);
        w.write("p cnf " + cnf.numVariables() + " " + cnf.numClauses());
        
        for (Iterator i = cnf.clauses().iterator(); i.hasNext();) {
            Clause clause = (Clause)i.next();
            w.newLine();
            
            for(Iterator j = clause.literals().iterator(); j.hasNext();) {
                int litInt = ((Literal)j.next()).intValue();
                w.write(Integer.toString(litInt) + " ");
            }
            
            w.write("0");
        }
        
        w.newLine();
        w.flush();
    }
    
    /**
     * Reads the and returns a CNF from the specified reader.
     */
    public static CNF readCNF(Reader cnfReader) throws IOException {
        BufferedReader r = new BufferedReader(cnfReader);
        CNF cnf = new CNF();
        Clause currClause = new Clause();
        
        for(String line = r.readLine(); line != null; line = r.readLine()) {
            StringTokenizer st = new StringTokenizer(line);
            String first = st.nextToken();
            if (first.equals("p") || first.equals("c")) {
                System.out.println(line);
                continue;
            }
            currClause = handleToken(first, currClause, cnf);
            
            while(st.hasMoreTokens()) {
                currClause = handleToken(st.nextToken(), currClause, cnf);
            }
        }
        
        return cnf;
    }
    
    private static Clause handleToken(String token, Clause clause, CNF cnf) {
        int n = Integer.parseInt(token);
        if (n == 0) {
            cnf.addClause(clause);
            return new Clause();
        } else {
            clause.addLiteral(Literal.getLiteral(n));
            return clause;
        }
    }
    
    /**
     * Counts the clauses in the specified CNF reader, quicker than
     * reading in the entire CNF.
     */
    public static int countClauses(Reader cnfReader) throws IOException {
        BufferedReader r = new BufferedReader(cnfReader);
        int count = 0;
        
        for(String line = r.readLine(); line != null; line = r.readLine()) {
            StringTokenizer st = new StringTokenizer(line);
            String first = st.nextToken();
            if (first.equals("p") || first.equals("c")) continue;
            if (Integer.parseInt(first) == 0) count++;
            
            while(st.hasMoreTokens()) {
                if (Integer.parseInt(st.nextToken()) == 0) count++;
            }
            
        }
        return count;
    }
    
    /**
     * Reads the specified solution read from the specified reader
     * to determine whether the it indicates the CNF was satisfiable.
     */
    public static boolean isSatisfiable(Reader reader) throws IOException {
        BufferedReader r = new BufferedReader(reader);
        boolean sat = Integer.parseInt(r.readLine()) == 1;
        r.close();
        return sat;
    }
    
}