package heuristics;

import java.util.HashMap;
import java.util.HashSet;
import java.util.Map;
import java.util.Set;

import jdd.DebugJDD;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import parser.State;
import parser.VarList;
import parser.ast.ModulesFile;
import prism.PrismException;

public class VarInfo
{
	private JDDVars vars;
	private String[] varNames;
	private int[] varRangeLow;
	private int[] varRangeHigh;
	private VarList varList;
	
	private Map<Long,State> index2State;
	private Map<State,JDDNode> storeJDDNode;
	
	/**
	 * VarInfo converts variables of a module to (MT)BDD variables.
	 * Variables in a module characterize states take integer values of a given interval.
	 * 
	 * BDD variables are boolean and are used to 
	 * locate the leave in the BDD corresponding to the some state
	 * 
	 * Let m be the length of the range of some module variable,
	 * then for this module variable, there are ceil(log2(m)) BDD variables.
	 * Some of the range might not be used, but these areas will be pruned away by BDD techniques.
	 * 
	 * @param mf module (file) for which variables are transformed to BDD variables
	 * @throws PrismException
	 */
	
	public VarInfo(ModulesFile mf) throws PrismException {
		varList = new VarList(mf);
		varNames = new String[varList.getTotalNumBits()];
		varRangeLow = new int[varList.getNumVars()];
		varRangeHigh = new int[varList.getNumVars()];
		vars = new JDDVars();
		index2State = new HashMap<Long,State>();
		int ddVars = 0;
		for (int i = 0; i < varList.getNumVars(); i++) {
			varRangeLow[i] = varList.getLow(i);
			varRangeHigh[i] = varList.getHigh(i);
			for (int j = 0; j < varList.getRangeLogTwo(i); j++) {
				JDDNode tmpVar = JDD.Var(ddVars);
				vars.addVar(tmpVar);
				varNames[ddVars] = varList.getName(i) + "." + j;
				ddVars++;
			}
		}
		storeJDDNode = new HashMap<State,JDDNode>();
	}
	
	public void derefAll() {
		for (int i = 0; i < vars.n(); i++) {
			JDD.Deref(vars.getVar(i));
		}
	}
	
	public JDDVars getJDDVars() {
		return vars;
	}
	
	public String[] getVarNames() {
		return varNames;
	}
	
	public VarList getModuleVarList() {
		return varList;
	}
	
	public void printRefCounts() {
		for (int i = 0; i < vars.n(); i++) {
			System.out.println("Var " + i + " rc: " + DebugJDD.getRefCount(vars.getVar(i)));
		}
	}
	
	public long state2Index(State s) throws PrismException {
		int k = 0;
		boolean[] bits = new boolean[vars.n()];
		for (int i =0; i < s.varValues.length; i++) {
			if (s.varValues[i] instanceof Boolean) {
				bits[k] = (Boolean) s.varValues[i];
				k++;
			}
			else if (s.varValues[i] instanceof Integer) {
				int value = (Integer)s.varValues[i];
				for (int j = varList.getRangeLogTwo(i) - 1; j >= 0; j--) {
					if (value % 2 == 1) bits[k] = true;
					else bits[k] = false;
					value = value / 2;
					k++;
				}
			}
			else {
				throw new PrismException(s.varValues[i] + " is neither bool nor int");
			}
		}
		long n = 0, l = bits.length;
		for (int i = 0; i < l; ++i) {
		    n = (n << 1) + (bits[i] ? 1 : 0);
		}
		return n;
	}
	
	public JDDNode state2JDD(State s) {
	  JDDNode stored = storeJDDNode.get(s);
	  if (stored != null) {
		  JDD.Ref(stored);
		  return stored;
	  }
	  else {
		  JDDNode dd = JDD.Constant(1);
		  int k = 0;
		  for (int i = 0; i < s.varValues.length; i++) {
		  if (s.varValues[i] instanceof Boolean) {
		    JDD.Ref(vars.getVar(k));
		    if ((Boolean) s.varValues[i]) {
		      dd = JDD.And(dd, vars.getVar(k));
		    } else {
		      dd = JDD.And(dd, JDD.Not(vars.getVar(k)));
		    }
		    k++;
		  } else if (s.varValues[i] instanceof Integer) {
		    int value = (Integer) s.varValues[i];
		    boolean[] bits = new boolean[varList.getRangeLogTwo(i)];
		    for (int j = varList.getRangeLogTwo(i) - 1; j >= 0; j--) {
		    if (value % 2 == 1)
		      bits[j] = true;
		    else
		      bits[j] = false;
		      value = value / 2;
		    }
		    for (int j = 0; j < varList.getRangeLogTwo(i); j++) {
		      JDD.Ref(vars.getVar(k));
		      if (bits[j]) {
		        dd = JDD.And(dd, vars.getVar(k));
		      } else {
		        dd = JDD.And(dd, JDD.Not(vars.getVar(k)));
		      }
		      k++;
		    }
	      } else {
	        //TODO: handle this properly, this should not happen
		    //    throw new PrismException(s.varValues[i] + " is neither bool nor int");
	      }
	    }
		JDD.Ref(dd);
	    storeJDDNode.put(s, dd);
	    return dd;
	  }
  }

	public JDDNode state2JDD_old(State s) {
//		System.out.println("Before creating constant");
		JDDNode dd = JDD.Constant(1);
//		System.out.println("After creating constant");
		JDD.Ref(dd);
		int k = 0;
		for (int i =0; i < s.varValues.length; i++) {
			if (s.varValues[i] instanceof Boolean) {
				JDD.Deref(dd);
				JDD.Ref(vars.getVar(k));
				if ((Boolean)s.varValues[i]) {
					JDDNode tmp = JDD.And(dd, vars.getVar(k));
					dd = tmp;
				}
				else {
					JDDNode tmp = JDD.And(dd,JDD.Not(vars.getVar(k)));
					dd =  tmp;
					JDD.Ref(vars.getVar(k));
				}
				JDD.Ref(dd);
				k++;
			}
			else if (s.varValues[i] instanceof Integer) {
				int value = (Integer)s.varValues[i];
				boolean[] bits = new boolean[varList.getRangeLogTwo(i)];
				for (int j = varList.getRangeLogTwo(i) - 1; j >= 0; j--) {
					if (value % 2 == 1) bits[j] = true;
					else bits[j] = false;
					value = value / 2;
				}
				for (int j = 0; j < varList.getRangeLogTwo(i); j++) {
//					JDD.Ref(dd);
					JDDNode olddd = dd;
					JDD.Ref(vars.getVar(k));
					
					if (bits[j]) {
						JDDNode con1 = dd;
						JDDNode con2 = vars.getVar(k);
						
						dd = JDD.And(con1,con2);
						
//						JDD.Deref(con1);
					}
					else {
						JDDNode con1 = dd;
						
						
						
						JDDNode con2 = JDD.Not(vars.getVar(k));
						JDD.Ref(vars.getVar(k));
						
//						System.out.println("Before and" + con1 + " | " + con2 );
						dd = JDD.And(con1,con2);
//						System.out.println("After not "  + con1 + " | " + con2 );
//						JDD.Deref(con1);
						
					}
//					JDD.Deref(olddd);
//					JDD.Ref(dd);
					k++;
				}
			}
			else {
				//TODO: handle this properly, this should not happen
//				throw new PrismException(s.varValues[i] + " is neither bool nor int");
			}
		}
		return dd;
	}
	
}
