package network.client;

import java.io.BufferedInputStream;
import java.io.DataInputStream;
import java.io.File;
import java.io.FileInputStream;
import java.io.FileNotFoundException;
import java.io.IOException;
import java.io.ObjectInputStream;
import java.io.ObjectOutputStream;
import java.net.Socket;
import java.util.*;

import zb2smt.ZB2SMTUtils;

import network.Requisition;


public class ProofClient  /*implements Runnable*/ {

	ArrayList <Thread> listofTrhead = new ArrayList<Thread>();    
	ArrayList <String> listofServer = new ArrayList<String>();
	//File file = new File(System.getProperty("user.dir")+ "/network/Config");
	File file = new File(System.getProperty("user.dir")+ ZB2SMTUtils.fs + ZB2SMTUtils.smtSolversStr +  ZB2SMTUtils.fs +"Config");
	FileInputStream fis = null;
	BufferedInputStream bis = null;
	DataInputStream dis = null;
	String proofobligation;
	String result;

	public static void main(String[] args) {

		ProofClient maintrhead = new ProofClient("(= 1 1)");
		try {
			System.out.print(maintrhead.proveRemotely());
		}
		catch (Exception e) {
			e.printStackTrace();
		}
		System.exit(0);

	}

	public  ProofClient(String proofobligation) {

		this.proofobligation = proofobligation;

	}


	public synchronized  String proveRemotely() throws Exception  {

		try {

			fis = new FileInputStream(file);

			// Here BufferedInputStream is added for fast reading.
			bis = new BufferedInputStream(fis);
			dis = new DataInputStream(bis);

			// dis.available() returns 0 if the file does not have more lines.
			while (dis.available() != 0) {

				// this statement reads the line from the file, create a requisition, send this requisition to remote theorem prover and 
				// print the answer
				// the console.

				String[] result = dis.readLine().split("@");
				if (result.length > 1) {
					Requisition req =new Requisition( new String(result[0]),proofobligation,new String(""));
					Thread t = new Conection(result[1],req, this);
					//System.out.println("Path e param:"+result[0] +"host"+result[1]+"FIM");
					try {	
					t.start();
					}
					catch (Exception e) {
						e.printStackTrace();
						return "Error";
					}

					listofTrhead.add(t);
				}


			}



			// dispose all the resources after using them.
			fis.close();
			bis.close();
			dis.close();

		} catch (FileNotFoundException e) {
			e.printStackTrace();
		} catch (IOException e) {
			e.printStackTrace();
		}


		try {

			this.wait() ;

		} catch (InterruptedException e) {
			// TODO Auto-generated catch block

			e.printStackTrace();

			System.err.println("This program can't wait");

		}


		//System.out.println("Resultado:"+result);


		return result;



	}


	public  synchronized void stopOthers(Object obj){

		int size = listofTrhead.size();

		for (int count = 0 ;  count < size ; count++ )
			if(listofTrhead.get(count)!= obj)				
				listofTrhead.get(count).stop();

		this.result = new String (((Conection) obj).req.getResult());


	}


	class Conection extends Thread{ 

		Socket socket;
		ObjectOutputStream objoutstream ;
		ObjectInputStream objinstream;
		String hostname; 
		Requisition req;
		ProofClient father;



		public  Conection(String hostname, Requisition req, ProofClient father){
			this.hostname = hostname; 
			this.req = req;
			this.father = father;

		}

		public void run(){

			Requisition req_answer=null;

			try{
				socket = new Socket(hostname, 2525);

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

				System.out.println("Sending the proof obligation");

				objoutstream.writeObject((Requisition) req);

				System.out.println("Waiting answer");

				req_answer = (Requisition) objinstream.readObject();

				/*System.out.println(req_answer.getProvername());
	                System.out.println(req_answer.getProofobligation());
	                System.out.println(req_answer.getResult());*/

				req_answer = new Requisition("","",req_answer.getResult() );

				req.setResult(req_answer.getResult());

				father.result = req_answer.getResult();

				synchronized(father) {father.notify(); father.stopOthers(this);  }


				//System.out.println("Result"+req.getResult() );
			}catch (Exception e) {
				e.printStackTrace();
				synchronized(father) {father.notify();}
				System.err.println("Cannot call the remote prover.");
			}



		}
	}




}