package sbdd;

import java.util.AbstractSet;
import java.util.Collection;
import java.util.Iterator;
import java.util.Map.Entry;

import lite.BDDSolver;
import lite.ITLSolver;

public class SBDDSet extends  AbstractSet<Entry<ITLSolver, SBDDEntry>> {
	
	/*
	 * Hash Table for Subterm BDD
	 *    this is also State DB with SBDDEntry
	 */
	
	public SBDDEntry[] sbddArray ;
	public int hash;
	private int hash0;
	private int hashSize = 1024*256;
	public Object lastEntry;
	SBDDFactory sf;
	int size = 0;
	// Multiple SBDDSet is not recomended, but just in case, we make variable
	// order is shared among existing SBDDSet.
	static final int INITIAL_SUBTERMS = 10;
	static int subterms = INITIAL_SUBTERMS;

	SBDDSet() {
		sbddArray = new SBDDEntry [hashSize];
	}
	
	SBDDSet(SBDDFactory sf) {
		sbddArray = new SBDDEntry [hashSize];
		this.sf = sf;
	}
	
	SBDDSet(SBDDFactory sf, int size) {
		sbddArray = new SBDDEntry [size];
		hashSize = size;
		this.sf = sf;
	}
	
	SBDDSet(Collection<SBDDEntry> c) {
		sbddArray = (SBDDEntry[]) c.toArray();
	}
	
	@Override
	public Iterator<Entry<ITLSolver, SBDDEntry>> iterator() {
		hash0 = hash-1+hashSize;
		return new Iterator<Entry<ITLSolver, SBDDEntry>>() {

			public boolean hasNext() {
				return (sbddArray[hash%hashSize]!=null && hash!=hash0) ;
			}

			public SBDDEntry next() {
				return sbddArray[hash++%hashSize];
			}

			public void remove() {
			}
			
		};
	}

	@Override
	public  boolean contains(Object e) {
		return get(e)!=null;
	}
	
	public SBDDEntry get(Object e) {
		SBDDEntry value;
		lastEntry = null;
		hash = e.hashCode()%hashSize;
		hash0 = hash-1+hashSize;
		while(sbddArray[hash%hashSize]!=null && hash!=hash0) {
			if ((value=sbddArray[hash%hashSize]).equals(e)) return value;
			hash ++;
		}
		if (hash!=hash0) lastEntry = e;
		return null;
		// return super.contains(e);
	}
	
	
	@Override
	public int size() {
		return size;
	}

	@Override
	public boolean add(Entry<ITLSolver, SBDDEntry> e) {
		// check hash is already set by contains
		if (lastEntry!=e) {
			if (get(e)!=null||hash==hash0) return false;
		}
		sbddArray[hash%hashSize] = (SBDDEntry) e;
		lastEntry = null;
		e.getValue().id = size++;
		ITLSolver var = ((BDDSolver)e.getKey()).var;
		if (var.order==-1) var.order = subterms ++;
		return true;
	}

	public BDDSolver put(ITLSolver key) {
		BDDSolver std = key.toSBDD(sf);
		SBDDEntry e = new SBDDEntry(std);
		SBDDEntry r;
		if ((r=get(e))!=null) {
			return (BDDSolver)r.key;
		} else {
			add(e);
		}
		return std;
	}


	public String toString() {
		String s = "SBDDSet[\n";
		for(int i = 0;i<sbddArray.length;i++) {
			if (sbddArray[i]!=null) {
				SBDDEntry e  = sbddArray[i];
				s += i+"\t"/*+"\thash="+(e.key.hashCode()%hashSize)*/+":"+e.key+"\n";
			}
		}
		return s+"]";
	}

	public SBDDEntry getEntry(ITLSolver key) {
		BDDSolver std = key.toSBDD(sf);
		SBDDEntry e = new SBDDEntry(std);
		SBDDEntry r;
		if((r= get(e))!=null) return r;
		add(e);
		return e;
	}


}