package cnf;

import java.io.FileReader;
import java.io.FileWriter;
import java.io.IOException;
import java.io.Reader;
import java.io.Writer;

/**
 * Utility processes.
 * 
 * @author Greg Dennis (gdennis@mit.edu)
 */
public final class Processes {

    private static final String SOLVER_DIR = "solvers";
    private static final String FILE_SEPARATOR = System.getProperty("file.separator");
    private static String inDir(String filename) {
        return SOLVER_DIR + FILE_SEPARATOR + filename;
    }
    private static final String PROOF_PATH = inDir("proof.prf");
    
    private static final Runtime RUNTIME = Runtime.getRuntime();

    private Processes() {}
    
    /**
     * Writes the specified cnf to the specified file.
     */
    public static void cnfToFile(CNF cnf, String filename) throws IOException {
        Writer w = new FileWriter(inDir(filename));
        DimacsIO.writeCNF(cnf, w);
        w.flush();
        w.close();
    }
    
    /**
     * Solve the CNF is the specified CNF file and write the solution to
     * the specifies solution file.
     */
    public static SolveStats solve(String cnfFilename, String solFilename) throws IOException {
        CNFProcess berkmin = new CNFProcess(
                inDir("berkmin") + " -s " + inDir(solFilename) + " " + inDir(cnfFilename));
                //inDir("mchaff") + " -s " + inDir(solFilename) + " " + inDir(cnfFilename) + " mchaff.smj");
        BerkMinListener bl = new BerkMinListener(berkmin, inDir(solFilename));
        berkmin.setListener(bl);
        //long time = System.currentTimeMillis();
        berkmin.execute();
        //long duration = System.currentTimeMillis() - time;
        SolveStats stats = new SolveStats(bl.duration(), bl.isSat());
        return stats;
    }
    
    public static class SolveStats {
        public final double duration;
        public final boolean sat;
        
        private SolveStats(double duration, boolean sat) {
            this.duration = duration;
            this.sat = sat;
        }
    }

    /**
     * Counts the number of solutions
     */
    public static int count(String cnfFilename, String solFilename) throws IOException {
        CNFProcess mchaff = new CNFProcess(
                inDir("mchaff") + " -s " + inDir(solFilename) + " " + inDir(cnfFilename) + " mchaff.smj");
        CountSolverListener cl = new CountSolverListener(mchaff, inDir(solFilename));
        mchaff.setListener(cl);
        mchaff.execute();
        return cl.count();
    }

    /**
     * Runs unsat core and returns the number of clauses in the CNF.
     */
    public static int unsat(String cnfFilename) throws IOException {
        String cnfPath = inDir(cnfFilename);
        String lastCnfIter = cnfPath;
        int lastNumClauses = countClauses(lastCnfIter);
        
        for (int i = 1;; i++) {
            //System.out.println("ucore: " + lastNumClauses);
            
            // run zchaff
            CNFProcess zchaff = new CNFProcess(inDir("zchaff") + " -a " + PROOF_PATH + " " + lastCnfIter);
            SimpleSolverListener sl = new SimpleSolverListener(zchaff, null);
            zchaff.setListener(sl);
            zchaff.execute();
        
            // extract unsat core
            String currCnfIter = cnfPath + "_" + i;
            CNFProcess zcore = new CNFProcess(inDir("zcore") + " " + lastCnfIter + " " + PROOF_PATH + " " + currCnfIter);
            zcore.execute();
            int currNumClauses = countClauses(currCnfIter);

            // if reached fixed point, break
            if (lastNumClauses == currNumClauses) {
                //System.out.println("fixed point!");
                break;
            }
            
            // otherwise, prepare for next iteration
            lastCnfIter = currCnfIter;
            lastNumClauses = currNumClauses;
        }
           
        return lastNumClauses;
    }
    
    private static int countClauses(String cnfFile) throws IOException {
        Reader r = new FileReader(cnfFile);
        int numClauses = DimacsIO.countClauses(r);
        r.close();
        return numClauses;
    }
    
}