package fr.lifl.stc.stan.implicitFlow.QuineMcCluskey;

import java.util.Vector;

import fr.lifl.stc.stan.implicitFlow.data.BooleanExpression;
import fr.lifl.stc.stan.implicitFlow.data.BooleanVariable;
import fr.lifl.stc.stan.implicitFlow.data.Minterm;

/**
 * 
 * @author dorina
 *
 */

public class Minimization {
	
	/**
	 * the boolean expression to be minimized
	 */
	BooleanExpression be;
	
	/**
	 * number of distinct boolean variables
	 */
	int n;
	
	/**
	 * vector containing all the distinct boolean variables  
	 */
	Vector<BooleanVariable> booleanVariables;
	
	/**
	 * implicants[i][j] => implicants of size i that contain j number of true variables
	 */
	Vector<Implicant>[][] implicants;
	
	/**
	 * 
	 */
	Vector<Implicant> initialImplicants;
	/**
	 * vector of ireductible prime implicants
	 */
	Vector<Implicant> ired;
	
	/**
	 * essential prime implicants
	 */
	Vector<Implicant> essentialPI;
	
	
	public static StatsMinimization stats = new StatsMinimization();
	
	/**
	 * 
	 * @param be
	 */
	@SuppressWarnings("unchecked")
	public Minimization(BooleanExpression be){
		
		this.be = be;
		this.ired = new Vector<Implicant>();
		
		this.booleanVariables = be.getDistinctBooleanVariables();
		this.n = this.booleanVariables.size();
		
		stats.inc(n);
		stats.setMax(n);
		
		//System.out.println("n = "+n);
		
		implicants = new Vector[n+1][];
		for(int i = 0 ; i < implicants.length; i++) {
			//FIXME
			//implicants[i] = new Vector[n-i+1];
			implicants[i] = new Vector[n+1-i];
			
			for(int j = 0; j < implicants[i].length; j++)
				implicants[i][j]= new Vector<Implicant>();
		}
		
		this.initialImplicants = new Vector<Implicant>();
		this.essentialPI = new Vector<Implicant>();
		Minterm[] min = be.getMinterms();
		for(int i = 0 ; i < min.length; i++) {
			Implicant tmp = new Implicant(min[i], this.booleanVariables);
			add(tmp);
			this.initialImplicants.add(tmp);
		}
	}
	
	/**
	 * 
	 * @param impl
	 */
	private void add(Implicant impl) {
		this.add(impl, impl.getSize(this.n), impl.getNumberTrueVariables());
	}
	
	/**
	 * 
	 * @param impl
	 * @param size
	 * @param noTrue
	 */
	private void add(Implicant impl, int size, int noTrue){
		//System.out.println(impl+"   "+size+"   "+noTrue);
		if(implicants[size][noTrue] == null ) {
			implicants[size][noTrue] = new Vector<Implicant>();
			implicants[size][noTrue].add(impl);
			return;
		}
		Vector<Implicant> tmp = implicants[size][noTrue];
		int i = 0;
		for(; i < tmp.size(); i++)
			if(impl.equals(tmp.elementAt(i)))
				break;
		if(i == tmp.size())
			tmp.add(impl);
	}
	
	public void minimize(){
		this.computeAllPrimeImplicants();
		this.computeEssentialPrimeImplicants();
	}
	
	/**
	 * 
	 * phase 1
	 */
	public void computeAllPrimeImplicants() {
		int currentSize = 0;
		
		while(currentSize < this.implicants.length) {
			//modif && currentSize < this.implicants.length) {
			
			//modif = false;
			for(int i = 0 ; i < this.implicants[currentSize].length-1; i++) {
				Vector<Implicant> jj = this.implicants[currentSize][i];
				Vector<Implicant> kk = this.implicants[currentSize][i+1];
				for(int j = 0; j < jj.size(); j++) {
					Implicant tmp1 = jj.elementAt(j);
					for(int k = 0; k < kk.size(); k++) {
						Implicant tmp2 = kk.elementAt(k);
						if(tmp1.isAdjacent(tmp2)) {
							//foundAdj = true;
							this.add(new Implicant(tmp1, tmp2));
							tmp2.setReductibleEnabled();
							tmp1.setReductibleEnabled();							
						}
					}
					
				}
			}
			for(int i = 0 ; i < this.implicants[currentSize].length; i++) {
				Vector<Implicant> jj = this.implicants[currentSize][i];
				for(int k = 0; k < jj.size(); k++) {
					Implicant tmp = jj.elementAt(k);
					if(!tmp.isReductible()) {
						ired.add(tmp);
						
					}
				}		
			}
			
			currentSize++;
		}
		
		//take the rest
		for(int j = currentSize; j < this.implicants.length; j++) {
			for(int i = 0 ; i < this.implicants[j].length; i++) {
				Vector<Implicant> jj = this.implicants[j][i];
				for(int k = 0; k < jj.size(); k++) {
					Implicant tmp = jj.elementAt(k);
					if(!tmp.isReductible()) {
						ired.add(tmp);
						
					}
				}
			}
		}
	}
	
	public void printAllPrimeImplicants(){
		
	}
	
	/**
	 * phase 2
	 *
	 */
	public void computeEssentialPrimeImplicants() {
		
		//compute coverage table
		boolean [][]coverage = new boolean[this.ired.size()][this.initialImplicants.size()];
		for(int i = 0; i < coverage.length; i++) {
			Implicant prime = this.ired.elementAt(i);
			for(int j = 0; j < coverage[i].length; j++) {
				if(prime.covers(this.initialImplicants.elementAt(j)))
					coverage[i][j] = true;
				else
					coverage[i][j] = false;
			}
		}
		
		int min;
		int col;
		while (  notEmpty(coverage) ) {
			
			//find min
			col = -1;
			min = 10000;
			
			for(int i = 0 ; i < coverage[0].length; i++){
				int noTrue = 0;
				for(int j = 0; j < coverage.length; j++)
					if(coverage[j][i])
						noTrue++;
				if(noTrue>0 && noTrue < min){
					min = noTrue;
					col = i;
				}
			}
			
			//if min > 1 ???
			
			for(int i = 0; i < coverage.length; i++) {
				if(coverage[i][col]) {
					essentialPI.add(this.ired.elementAt(i));
					coverage[i][col] = false;
					for(int j = 0; j < coverage[i].length; j++)
						if(coverage[i][j]) {
							for(int k = 0; k < coverage.length; k++)
								coverage[k][j]=false;
						}
				}
			}
			
		}
		//if(essentialPI)
	}
	
	static boolean notEmpty(boolean b[][]) {
		for(int i = 0 ; i < b.length; i++)
			for(int j = 0; j < b.length; j++)
				if(b[i][j])
					return true;
		return false;
	}
	
	public Minterm []getEssentialMinterms() {
		Minterm [] m = new Minterm[this.essentialPI.size()];
		for(int i = 0 ; i < this.essentialPI.size(); i++) {
			m[i] = this.essentialPI.elementAt(i).toMinterm(this.booleanVariables);
		}
		return m;
	}
	
}