package heuristics;

import java.util.HashSet;
import java.util.Set;

import odd.ODDNode;
import odd.ODDUtils;
import jdd.DebugJDD;
import jdd.JDD;
import jdd.JDDNode;
import jdd.JDDVars;
import parser.State;
import parser.VarList;
import parser.ast.ModulesFile;
import prism.PrismLangException;

public class ECContainerMTBDD implements ECContainer
{

	private VarInfo varInfo;
	private JDDNode inEC;
	private JDDNode eCs;
	private Set<State> inserted;
//	private ODDNode odd;
	
	public ECContainerMTBDD(VarInfo varInfo) throws PrismLangException {
		this.varInfo = varInfo;
		inEC = JDD.ZERO;
		JDD.Ref(inEC);
		eCs = JDD.Constant(-1);
		inserted = new HashSet<State>();
//		JDD.Ref(eCs);
//		System.out.println("***********CREATING***************");
	}	
	
//	@Override
//	public void insertJDD(State s, int ec)
//	{
//		
//		JDDNode dd = varInfo.state2JDD(s);
//		JDD.Ref(dd);
////		System.out.println("Before setting inEC ");
//		inEC = JDD.ITE(dd, JDD.ONE, inEC);
////		JDD.Ref(JDD.ONE);
//		
////		JDD.Ref(inEC);
//		JDDNode tmpConst = JDD.Constant(ec);
////		System.out.println("Before setting eCs ");
//		eCs = JDD.ITE(dd, tmpConst, eCs);
////		JDD.Ref(tmpConst);
//		
////		JDD.Deref(dd);
////		JDD.Ref(dd);
////		System.out.println("DD after insert: " + dd);
////		JDD.Deref(dd);
//		
//	}
	
	@Override
	public void insert(State s, int ec) {
		JDDNode dd = varInfo.state2JDD(s);
		JDD.Ref(dd);
		JDD.Ref(inEC);
		JDD.Ref(eCs);
		inEC = JDD.ITE(dd, JDD.ONE, inEC);
		eCs = JDD.ITE(dd, JDD.Constant(ec), eCs);
	}
	
	@Override
	public Integer getEC(State s) {
		JDDNode dd = varInfo.state2JDD(s);
		JDD.Ref(dd);
		JDD.Ref(inEC);
		boolean isInEC = JDD.Restrict(inEC, dd).getValue() > 0.0;
		if (isInEC) {
			JDD.Ref(eCs);
			int ec = ((Double)JDD.Restrict(eCs, dd).getValue()).intValue();
			return ec;
		}
		else {
			JDD.Deref(dd);
			return null;
		}
	}
	
	public void printAllInserted() {
		System.out.println("States inserted into some EC:");
		for (State s: inserted) {
			System.out.println(s);
		}
	}
	
//	public void insert(State s, int ec) {
//		inserted.add(s);
//		long index = varInfo.state2Index(s);
//		JDDVars vars = varInfo.getJDDVars();
//		inEC = JDD.SetVectorElement(inEC, vars, index, 1);
//		eCs = JDD.SetVectorElement(eCs, vars, index, ec);
//	}

	public Integer getECJDD(State s)
	{
//		System.out.println("before state2JDD");
		JDDNode dd = varInfo.state2JDD(s);
		JDD.Ref(dd);
//		JDD.Ref(dd);
//		System.out.println("after state2JDD");
//		System.out.println("Receiving " + DebugJDD.getRefCount(dd) + " ~ " + dd);
//		System.out.println("Before resticting inEC in get");
		JDDNode restrict = JDD.Restrict(inEC, dd);
		
		JDD.Ref(inEC);
		boolean isInEC = restrict.getValue() > 0.0;
		JDD.Deref(restrict);
//		System.out.println("restrict equal to dd" + restrict.equals(dd));
		JDD.Ref(inEC);
		
//		JDD.Ref(dd);
		if (isInEC) {
//			JDD.Ref(dd);
//			System.out.println("Before resticting eCs in get");
			JDDNode tmp = JDD.Restrict(eCs, dd);
			JDD.Ref(eCs);
			Double doubleVal = tmp.getValue();
			JDD.Deref(tmp);
//			JDD.Ref(eCs);
//			JDD.Deref(dd);
//			System.out.println("In the end after inEC " + DebugJDD.getRefCount(dd));
//			System.out.println("DD Refcount after get: " + dd + " state: " + s);
			return doubleVal.intValue();
		}
		else {
//			JDD.Deref(dd);
//			JDD.Deref(dd);
//			System.out.println("After resticting inEC in get");
//			System.out.println("DD Refcount after get: " + dd + " state: " + s);
//			System.out.println("In the end not inEC " + DebugJDD.getRefCount(dd));
			return null;
		}
	}
	
//	@Override
//	public Integer getEC(State s)
//	{
//		long index = varInfo.state2Index(s);
//		JDDVars vars = varInfo.getJDDVars();
//		boolean isInEC = JDD.GetVectorElement(inEC, vars, index) > 0.0;
//		if (isInEC) {
//			Double value = JDD.GetVectorElement(eCs, vars, index);
//			return value.intValue();
//		}
//		else {
//			return null;
//		}
//	}
	
	public void derefAll() {
//		System.out.println("DEREFING");
		JDD.Deref(inEC);
		JDD.Deref(eCs);
	}
}
