package edu.neu.ccs.util;

import gen.RelationNr;
import gen.Type;
import gen.TypeInstance;

import java.io.BufferedWriter;
import java.io.File;
import java.io.FileWriter;
import java.io.IOException;
import java.io.Writer;
import java.util.LinkedList;
import java.util.List;

/**
 * Solving SDG using Linear programming
 * @author Charu Chandra
 *
 */
public class SDGlp {

	// Truth table
	private static int[][] tt = {{0, 0, 0},
		{0, 0, 1},
		{0, 1, 0},
		{0, 1, 1},
		{1, 0, 0},
		{1, 0, 1},
		{1, 1, 0},
		{1, 1, 1}};
	private double[][] m_matrix;
	private Type m_type;
	private int m_noOfVars;


	//Constructor
	public SDGlp(Type type, int n){
		initialize(type,n);
		m_type = type;
		m_noOfVars = n;
	}

	/**
	 * Creates the matrix for future reference
	 * @param type
	 * @param n
	 */
	private void initialize(Type type, int n){
		edu.neu.ccs.demeterf.demfgen.lib.List<TypeInstance> instances = type.instances;
		m_matrix = new double[n+1][instances.length()];
		long totalCons = Binomial.binomial(n, 3) * 6;

		for(int k = 0;k <= n; k++){
			int count = 0;
			for(TypeInstance r: instances){
				int relation = r.r.v;
				int noOfSatCons = 0;
				for(int[] row: tt){
					//Find if the truth table row is satisfied or not
					int r1 = ShannonCofactor.computeSC(relation, 0, row[2]);
					int r2 = ShannonCofactor.computeSC(r1, 1, row[1]);
					int r3 = ShannonCofactor.computeSC(r2, 2, row[0]);
					// If the row is satisfied, find the number of constraints satisfied 
					// if k variables are set to true and sum it up with the results got so far
					if(r3 == 255)
						noOfSatCons += getSatCons(row,k,n);
				}
				//Add to the matrix
				m_matrix[k][count] = (double)noOfSatCons/totalCons;
				count++;
			}
		}
		System.out.println("No of relations: " + instances.length());
	}

	/**
	 * Get the number of satisfied constraints.
	 * Calculation e.g.
	 * 001 - (n-k) (n-1-k) (k)
	 * 110 - (k) (k-1) (n-k)
	 * @param row
	 * @param k
	 * @param n
	 * @return
	 */
	private int getSatCons(int[] row,int k, int n){
		int zeros = 0;
		int ones = 0;
		int result = 1;
		for(int i: row){
			if(i == 0){
				result *= (n - zeros - k);
				zeros ++;
			}
			else{
				result *= (k - ones);
				ones ++;
			}   
		}
		if(result == -1) return 0;
		return result;
	}
	/**
	 * Creates equations for buyer
	 * max t
	 * SUMMATION sij * li >=t
	 * SUMMATION li = 1
	 * @param n
	 * @param noOfRel
	 * @param result
	 * @return a java.util.List of String
	 */
	private List<String> createEqnsForBuyer(int n, int noOfRel, List<String> result){
		//max t
		result.add("t;");

		//SUMMATION sij * li >=t
		for(int i = 0;i < noOfRel; i++){
			String eqn = "";
			for(int j = 0; j <= n; j++){
				eqn += m_matrix[j][i] + " l" + j + " + ";
			}
			eqn = eqn.substring(0, eqn.length() - 3) + " > t;";
			result.add(eqn);
		}

		//SUMMATION li = 1
		String probEqn = "";
		//l can only be an integer since number of variables set to true can only obtain one value
		String lIntValue = "int";  

		for(int k = 0;k <= n;k++){
			probEqn += "l" + k + " + ";
			lIntValue += " l" + k + ",";
		}
		probEqn = probEqn.substring(0, probEqn.length() - 3) + " = 1;";
		lIntValue += lIntValue.substring(0, lIntValue.length() - 1) + ";";
		result.add(probEqn);
		result.add(lIntValue);

		System.out.println("Eqns for buyer: "+ result);
		return result;
	}

	/**
	 * Creates equations for seller
	 * min t
	 * SUMMATION sij * mj >=t
	 * SUMMATION mj = 1
	 * @param n
	 * @param noOfRel
	 * @param result
	 * @return a java.util.List of String
	 */
	private List<String> createEqnsForSeller(int n,int noOfRel, List<String> result){
		//min t
		result.add("-t;");

		//SUMMATION sij * mj >=t
		for(int j = 0;j <= n; j++){
			String eqn = "";
			for(int i = 0; i < noOfRel; i++){
				eqn += m_matrix[j][i] + " m" + i + " + ";
			}

			eqn = eqn.substring(0, eqn.length() - 3) + " < t;";
			result.add(eqn);
		}

		//SUMMATION mj = 1
		String probEqn = "";
		for(int k = 0;k < noOfRel;k++){
			probEqn += "m" + k + " + ";
		}
		probEqn = probEqn.substring(0, probEqn.length() - 3) + " = 1;";
		result.add(probEqn);
		System.out.println("Eqns for seller: "+ result);
		return result;
	}
	
	/**
	 * Writes the equations to a file inside result folder with name list_of_relations separated by '_' + "buyer"/"seller" + no_of_vars
	 * For example: Relation 170 and 119 with 100 number of variables for a buyer:
	 *     the file will appear inside result folder as 170_119_buyer_100
	 * @param buyer - if the equations are for buyer or for seller
	 * @throws IOException
	 */
	public void writeEqnsToFile(boolean buyer) throws IOException{
		java.util.List<String> eqns = new LinkedList<String>();
		if(buyer)
			eqns = createEqnsForBuyer(m_noOfVars, m_type.instances.length(), eqns);
		else
			eqns = createEqnsForSeller(m_noOfVars, m_type.instances.length(), eqns);
		
		String str = "";  	

		for(String eqn: eqns){
			str += eqn;
		}

		System.out.println("new string: " + str);
		String fileName = getFileName(buyer);
		
		File file = new File("./result/" + fileName);
		Writer output = null;
		
		if(!file.exists())
			file.createNewFile();
		else{
			file.delete();
			file.createNewFile();
		}
		
		output = new BufferedWriter(new FileWriter(file));
		output.write(str);
		output.close();
	}
	
	/**
	 * Gets the file name in the format list_of_relations separated by '_' + "buyer"/"seller" + no_of_vars
	 * @param buyer
	 * @return
	 */
	private String getFileName(boolean buyer){
		String name = "";
		for(TypeInstance instance :  m_type.instances){
			name += instance.r.v + "_";
		}
		
		if(buyer)
			name += "buyer_";
		else
			name += "seller_";
		
		name += m_noOfVars;
		
		return name;
	}
	
	/*public static void main(String[] args) throws IOException{
		edu.neu.ccs.demeterf.demfgen.lib.List<TypeInstance> instances = edu.neu.ccs.demeterf.demfgen.lib.List.create(new TypeInstance(new RelationNr(170)));
		instances = instances.append(new TypeInstance(new RelationNr(119)));
		instances = instances.append(new TypeInstance(new RelationNr(22)));
		
		Type type = new Type(instances);
		
		SDGlp lp = new SDGlp(type,100);
		
		lp.writeEqnsToFile(false);
	}*/
}