import java.util.*;
import java.io.*;
import java.nio.channels.*;
/**
 * In its own thread, Solver gets a SubProblem from Msat, asks
 * SATSolver to solve the subproblem, reports to Msat when the
 * SATSolver is finished, and repeats with a new SubProblem
 * if Msat gives one.
 *
 * @author Danielle Eckard and Dr. Lobo
 * @version 2008.01.17
 */

public class Solver extends Thread {

    boolean free = true;
    String answer; // satisfied?
    Msat coordinator;
    GregDLLSolver satsolver; //!!!!!!User: change SATSolver to the name of your class!!!!!!!!
    //SATSolver satsolver;
    SubProblem myProblem;
    int counter;  // counter used to create unique files


    /**
     * Constructor for Solver
     *
     * @param c the Msat coordinator
     */
    public Solver (Msat c ) {
        coordinator = c;
        myProblem = new SubProblem();
        answer = "";
    }

    /**
     * Run method needed for running threads.  Run's the Solver on the thread
     * while getting the next subproblem (if one exists) from the Msat coordinator.
     * Tests each subproblem to see if a satisfying assignment exists.
     */
    public void run ( ) {

        boolean done = false;
        counter = 1;
	while (!done) {
            myProblem = coordinator.getSubProblem ( );

            if (myProblem == null)
		{
            	System.out.println ("Thread " + Thread.currentThread().getId() 
			+ " tried to get a subproblem at " + 
                        System.nanoTime() + " but got none.");
		
                done = true;
		}
            else {

            	//System.out.println ("Thread " + Thread.currentThread().getId() + " will work on assignemnt " + myProblem.getAssignment());
                //File filename = toText();
                counter ++;
                /**
                 * !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
                 * !!!!!!User: BruteForceSATSolver replaced by the name of your solver class!!!!!!!!
                 * !!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!!
                 */
                 //satsolver = new GregDLLSolver(filename.getPath());
		 satsolver = new GregDLLSolver(myProblem);

                 answer = (satsolver.solve()); 
                 coordinator.workCompleted( this );

                } // end else
            } // end while
    } // end run

 
    /**
     * Converts the subproblem to a text file in the form of a new
     * formula.  It does this by taking the assigned variables in the
     * subproblem and adds the clauses to the end of the formula in order
     * to force these variables to their assigned boolean value.
     *
     * @return the new text file
     */
/** private File toText()
    {
    	// the partial assignment
    	Assignment assignment = myProblem.getAssignment();
    	// the variable ID's of the assigned variables
    	ArrayList <Integer> assigned = assignment.getAssignedVarIds();
    	// the name of the file cooresponding to the formula
    	String filename = coordinator.getFormula().getInputFile();
    	// the name of the new file
    	String front = "";
    	File temp = new File(front);

    	try {
    		// making a unique filename
    		front = filename.substring(0, filename.length()-4);
    		front = front + "temp" + Thread.currentThread().getId() + counter + ".cnf";
    		temp = new File(front);
    		FileReader fr = new FileReader(filename);
    		FileWriter fw = new FileWriter(temp, true);
    		BufferedWriter bw = new BufferedWriter(fw);
    		BufferedReader br = new BufferedReader(fr);
    		String reader = br.readLine();
    		// skip comments
    		while(reader != null && reader.charAt(0)!= 'p')
    		{
    			reader = br.readLine();
    		}
    		String [] readerArray = reader.split(" ");
    		reader = "";
    		reader += readerArray[0] + " " + readerArray[1] + " " + readerArray[2] + " ";
    		int numClauses = new Integer (readerArray[3]) + assigned.size();
    		reader += numClauses;
    		bw.write(reader + "\n");
    		reader = br.readLine();
    		// copy clauses from original formula
    		while(reader != null)
    		{
    			bw.write(reader + "\n");
    			reader = br.readLine();
    		}
    		//add new clauses
    		for (int i=0; i<assigned.size();i++)
    		{
    			int varNum = assigned.get(i);
    			String clause = "";
    			if (assignment.getValue(varNum)==0)
    				clause += "-";
    			clause += varNum + " 0\n";
    			bw.write(clause);
    		}
    		bw.close();
    	}
    	catch (Exception e)
    	{
    		System.out.println("Failed to create file.");
    		System.out.println(e.toString());
    	}
    	return temp;
    }// end toText

**/


    /**
     * Returns the current assignment of the subproblem that this solver is working on.
     *
     * @return the current assignment of the subproblem this solver is working on
     */
    public Assignment getAssignment ( ) {
        if (myProblem != null)
            return myProblem.getAssignment();
        else
            return null;
    }// end getAssignment

    /**
     * returns the answer
     *
     * @return the answer
     */
    public String getAnswer ( ) {
        return answer;
    } // end getAnswer



} // end Solver