package sbdd;


import lite.ITLSolver;
import java.util.Iterator;
import java.util.LinkedList;
import java.util.Map.Entry;


public class SBDDEntry implements Entry<ITLSolver,SBDDEntry> {

	public ITLSolver key;
	boolean expanded = false;
	int id;
	LinkedList<SBDDEntry>nexts;
	public boolean falsifiable;
	public boolean satisfiable;
	
	/*
	 * Hash Table Entry for Subterm BDD
	 *      subterm? high : low
	 * 
	 * Subterm BDD represents a state in ITL, which is an ITL
	 * formula. It is ordered, so if it is the same it has same
	 * tree and the same hash entry.
	 *      
	 * All subterm is ITLSolver now. getValue() returns itself.
	 * key subterm has sequence number (order field), it is used
	 * as variable order in BDDSolver.
	 * 
	 * nexts contains possible next states. used in BDDDiagnosis.
	 */
	
	public SBDDEntry(ITLSolver now) {
		this.key = now;
		nexts = new LinkedList<SBDDEntry>();
	}

	public boolean	equals(Object e0) {
		if (e0.getClass()!=this.getClass()) return false;
		SBDDEntry e = (SBDDEntry) e0;
		return key==null?e.key==null: key.equals(e.key);
	}
	
	public int hashCode() {
		return key.hashCode();
	}

	public ITLSolver getKey() {
		return key;
	}

	public SBDDEntry getValue() {
		return this;
	}

	public SBDDEntry setValue(SBDDEntry e) {
		key = e.key;
		expanded = e.expanded;
		return this;
	}
	
	public boolean addNext(SBDDEntry e) {
		if (nexts.contains(e)) return false;
		return nexts.add(e);
	}

	// Iterate over possible next
	public Iterable<SBDDEntry> nexts() {
		return new Iterable<SBDDEntry>() {
			int i = 0;
			public Iterator<SBDDEntry> iterator() {
				return new Iterator<SBDDEntry>() {
					public boolean hasNext() {
						return nexts.size()>i;
					}
					public SBDDEntry next() {
						return nexts.get(i++);
					}
					public void remove() {
					}
				};
			}
		};
	}
}