package network.server;

import network.Requisition;
import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.InputStream;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.net.Socket;
import java.util.List;
import java.util.StringTokenizer;
import java.util.Vector;

public class Control extends Thread {

	private Socket connection;
	private static int count=0;
	ObjectOutputStream objoutstream;
	ObjectInputStream objinstream;


	public Control(Socket s) {
		connection = s;

	} 

	public void run() {

		try {

			Requisition req_received,req_answer;

			// objetos que permitem controlar fluxo de comunicação

			this.objoutstream = new ObjectOutputStream(connection.getOutputStream() );
			this.objinstream = new ObjectInputStream(connection.getInputStream() );


			System.out.println("Receiving proof obligation...");

			req_received = (Requisition) this.objinstream.readObject();


			System.out.println("The prover is working");


			req_answer = this.callprover(req_received);



			this.objoutstream.writeObject(req_answer);

			System.out.println("Answer sended!");
			
			this.connection.close();
			


		}


		catch (Exception e) {


			e.printStackTrace();
		}


	}

	protected Requisition callprover(Requisition req) {
		
		Requisition req_answer = new Requisition();
		
		StringBuffer output = new StringBuffer();
		
		String path_po_file = new String(java.lang.System.getProperty("java.io.tmpdir") + File.separator+"proof"+(count++)+".smt");


		
		
		// write the proof obligation to file
		try{

			FileWriter fstream = new FileWriter(path_po_file);
			BufferedWriter out = new BufferedWriter(fstream);
			
			String pO = req.getProofobligation();
			String novapO = "";
			for (int i=0; i< pO.length() ;i++) {
				if (pO.charAt(i) == 13) {
					novapO = novapO + ' ';
				}
				else {
					novapO = novapO + pO.charAt(i);
				}
			}
			
			out.write(novapO);
			out.close();
		} catch (IOException e) {
			System.err.println("Error writing the file from proof obligation.");
		}

		
		
		// call the prover  

		try {
			String[] tmp = req.getProvername().split(" ");
			
			String [] commands = new String[ tmp.length + 1 ];
			for(int i=0;i<tmp.length;i++)
				commands[i]=tmp[i];
			commands[tmp.length]=path_po_file;
			
			
			
			String arquivo = commands[commands.length -1];
			String parametros = "";
			
			//String[] commands = new String[]{req.getProvername().split(" "),path_po_file };
			//System.out.println("Comando executado"+req.getProvername());
			
			for (int i=0; i < commands.length -1; i++) {
				parametros = parametros + commands[i] + " ";
			}
			
			System.out.println(parametros  + arquivo);
			Process child = Runtime.getRuntime().exec(parametros  + arquivo);

			// Get the input stream and read from it
			System.out.println("Waiting answer!");

			InputStream in = child.getInputStream();
			InputStream erro = child.getErrorStream();
			
			int c;

			while ((c = in.read()) != -1) {
				output.append((char)c);
			}
			in.close();
			String error = "";
			
			int k;
			if (error!= null) {
				while ((k = erro.read()) != -1) {
					error = error + ((char)k);
				}
				erro.close();
			}
			if (error != "")
				System.err.println("Error Message in Prover: " + error);


		} catch (IOException e) {
			e.printStackTrace();
			System.err.println("Error calling the prover!");
		}
		System.out.println("OUT " + output.toString());
		String[] lines = returnLines(output.toString());

		String respostaHarvey = "";
		if (lines.length > 0) {
			respostaHarvey = lines[lines.length - 1];
		}
		
		req_answer.setResult( new String( respostaHarvey) ); 
		
		return req_answer;

	}
	
	private static String[] returnLines(String str)
	{
		String lineSep = System.getProperty("line.separator");
		
		StringTokenizer st = new StringTokenizer(str,lineSep);
		List<String> list = new Vector<String>();
		while (st.hasMoreTokens()) {
			list.add(st.nextToken());
		}
		String[] retorno = list.toArray(new String[0]);        
		return retorno;
	}

}