--- a/src/lite/ITLNodeFactory.java	Sun Jan 06 18:41:36 2008 +0900
+++ b/src/lite/ITLNodeFactory.java	Sun Jan 06 21:02:24 2008 +0900
@@ -1,7 +1,10 @@
 package lite;
 
 import java.util.LinkedList;
+import java.util.Set;
+import java.util.Map.Entry;
 
+import sbdd.BDDInterface;
 import sbdd.SBDDFactoryInterface;
 
 import logicNode.parser.Command;
@@ -95,4 +98,8 @@
 	public ITLSolver bddNode(ITLSolver cond, ITLSolver high, ITLSolver low) {
 		return new BDDSolver((VariableSolver)cond,high,low);
 	}
+
+	public Set<Entry<ITLSolver, BDDInterface>> set() {
+		return null;
+	}
 }

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/BDDID.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,15 @@
+package sbdd;
+
+public enum BDDID {
+
+
+	Exists, 
+	True   ,
+	False  ,
+	Variable,
+	Chop,
+	Next,
+	Empty,
+	Projection, BDD;
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/BDDInterface.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,7 @@
+package sbdd;
+
+import lite.BDDSolver;
+
+public interface BDDInterface {
+	public BDDSolver toSBDD(SBDDFactoryInterface sf);
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/BDDSatisfier.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,44 @@
+package sbdd;
+
+
+
+import java.util.LinkedList;
+import java.util.Set;
+import java.util.Map.Entry;
+
+import verifier.Backtrack;
+import lite.Continuation;
+import lite.ITLSatisfier;
+import lite.ITLSolver;
+import lite.Next;
+
+public class BDDSatisfier extends ITLSatisfier {
+
+
+	/**
+	 * 
+	 */
+	private static final long serialVersionUID = 1L;
+	public 	Set<SBDDEntry> state;
+	public  LinkedList<SBDDEntry> queue;
+	
+	public BDDSatisfier(ITLSolver p) {
+		lf = new SBDDFactory();
+		this.empty = p; // have to be the same in the parser
+		state = lf.set();
+		true_  = SBDDFactory.trueSolver;
+	}
+
+	
+	class allNext implements Next {
+		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			if (value!=null) {
+				SBDDEntry e = state.get(value);
+				if (!e.expanded) {
+					queue.add(e);
+				}
+			}
+			throw backtrack;
+		}
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDEntry.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,25 @@
+package sbdd;
+
+
+import lite.ITLSolver;
+
+
+public class SBDDEntry {
+
+	public static int count = 0;
+	
+	public ITLSolver key;
+	boolean expanded = false;
+	
+	public SBDDEntry(ITLSolver now) {
+		this.key = now;
+	}
+
+	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);
+	}
+	
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDFactory.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,125 @@
+package sbdd;
+
+
+import java.util.Set;
+
+import lite.BDDSolver;
+import lite.ITLNodeFactory;
+import lite.ITLSolver;
+import logicNode.parser.TokenID;
+
+
+public class SBDDFactory implements SBDDFactoryInterface {
+
+	public static final ITLSolver trueSolver   = new BDDSolver(ITLNodeFactory.trueSolver,BDDID.True,TokenID.True.hash);
+	public static final ITLSolver falseSolver  = new BDDSolver(ITLNodeFactory.falseSolver,BDDID.False,TokenID.False.hash);
+	public static final ITLSolver chopSolver   = new BDDSolver(BDDID.Chop,TokenID.Chop.hash);
+	public static final ITLSolver existsSolver = new BDDSolver(BDDID.Exists,TokenID.Exists.hash);
+	public static final ITLSolver nextSolver   = new BDDSolver(BDDID.Next,TokenID.Next.hash);
+	public static final ITLSolver emptySolver  = new BDDSolver(ITLNodeFactory.emptySolver,BDDID.Empty,TokenID.Empty.hash);
+	public static final ITLSolver projSolver   = new BDDSolver(BDDID.Projection,TokenID.Projection.hash);
+	public SBDDSet hash;
+	ITLNodeFactory itlf;
+	
+	SBDDFactory() {
+		hash = new SBDDSet(this);
+		itlf = new ITLNodeFactory();
+		
+		hash.put(falseSolver);
+		hash.put(trueSolver);
+		hash.put(existsSolver);
+		hash.put(nextSolver);
+		hash.put(chopSolver);
+		hash.put(emptySolver);
+		hash.put(projSolver);
+	}
+	
+
+	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) {
+		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
+		return hash.put(v); 
+	}
+
+	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2) {
+		ITLSolver v =  itlf.chopNode(solver.toSBDD(this),solver2.toSBDD(this));
+		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Chop);
+		return hash.put(b);
+	}
+
+	public ITLSolver emptyNode() {
+		return emptySolver;
+	}
+
+	public ITLSolver existsNode(ITLSolver solver, ITLSolver solver2) {
+		ITLSolver v =  itlf.existsNode(solver,solver2);
+		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Exists);
+		return hash.put(b);
+	}
+
+	public ITLSolver falseNode() {
+		return falseSolver;
+	}
+
+	public ITLSolver nextNode(ITLSolver solver) {
+		ITLSolver v =  itlf.nextNode(solver);
+		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Next);
+		return hash.put(b);
+	}
+
+	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2) {
+		ITLSolver v =  itlf.projectionNode(solver,solver2);
+		BDDSolver b = new BDDSolver(v,trueSolver,falseSolver,BDDID.Projection);
+		return hash.put(b);
+	}
+
+	public ITLSolver trueNode() {
+		return trueSolver;
+	}
+
+	public ITLSolver variableNode(String name, boolean value) {
+		ITLSolver v =  new BDDSolver(itlf.variableNode(name, value),trueSolver,falseSolver,BDDID.Variable);
+		return hash.put(v); 
+	}
+
+
+	public ITLSolver andNode(ITLSolver left, ITLSolver right) {
+
+		BDDSolver lb = left.toSBDD(this);
+		BDDSolver rb = right.toSBDD(this);
+		if (lb==falseSolver||rb==falseSolver)
+			return falseSolver;
+		if (lb==trueSolver)
+			return rb;
+		lb =  (BDDSolver) lb.and(this, rb);
+		return hash.put(lb);
+	}
+
+
+	public ITLSolver notNode(ITLSolver node) {
+		BDDSolver nb = node.toSBDD(this);
+		if (nb==falseSolver) return trueSolver;
+		if (nb==trueSolver)	 return falseSolver;
+		nb = (BDDSolver) nb.not(this);
+		return hash.put(nb);
+	}
+
+
+	public ITLSolver orNode(ITLSolver left, ITLSolver right) {
+		BDDSolver lb = left.toSBDD(this);
+		BDDSolver rb = right.toSBDD(this);
+		if (lb==trueSolver||rb==trueSolver)
+			return trueSolver;
+		if (lb==falseSolver)
+			return rb;
+		lb = (BDDSolver) lb.or(this, rb);
+		return hash.put(lb);
+	}
+
+
+	public SBDDSet set() {
+		return hash;
+	}
+
+
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDFactoryInterface.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,32 @@
+package sbdd;
+
+import lite.ITLSolver;
+
+
+public interface SBDDFactoryInterface {
+
+	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2);
+
+	public ITLSolver chopNode(ITLSolver solver, ITLSolver solver2);
+
+	public ITLSolver emptyNode();
+
+	public ITLSolver existsNode(ITLSolver solver, ITLSolver solver2);
+
+	public ITLSolver falseNode();
+
+	public ITLSolver nextNode(ITLSolver solver);
+
+	public ITLSolver projectionNode(ITLSolver solver, ITLSolver solver2);
+
+	public ITLSolver trueNode();
+
+	public ITLSolver variableNode(String name, boolean value);
+
+	public ITLSolver andNode(ITLSolver left, ITLSolver right);
+	public ITLSolver orNode(ITLSolver left,ITLSolver right);
+	public ITLSolver notNode(ITLSolver node);
+
+	public SBDDSet set();
+
+}
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDHash.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,53 @@
+package sbdd;
+
+
+import java.util.AbstractMap;
+import java.util.Set;
+
+import lite.*;
+import logicNode.parser.TokenID;
+
+public class SBDDHash extends AbstractMap<ITLSolver,BDDInterface> {
+
+	SBDDSet sbddset;
+	private SBDDFactoryInterface sf;
+	int lastVar ;
+	
+	SBDDHash() {
+		sbddset = new SBDDSet();
+		lastVar = TokenID.Projection.hash+ 1;
+	}
+	
+	SBDDHash(Set<Entry<ITLSolver, BDDInterface>> sbddset) {
+		this.sbddset = (SBDDSet) sbddset;
+		sf = new SBDDFactory();
+	}
+	
+	public SBDDHash(SBDDFactoryInterface factory) {
+		this();
+	}
+
+	@Override
+	public BDDSolver put(ITLSolver key,BDDInterface value) {
+		BDDSolver std = key.toSBDD(sf);
+		SBDDEntry e = new SBDDEntry(std,std);
+		if (sbddset.contains(e)) {
+			return std;
+		} else {
+			if (sbddset.add(e)) {
+				value.setHash(sbddset.hash);
+			}
+		}
+		return std;
+	}
+
+
+	@Override
+	public Set<Entry<ITLSolver, BDDInterface>> entrySet() {
+		return sbddset;
+	}
+
+	public String toString() {
+		return sbddset.toString();
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDSet.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,114 @@
+package sbdd;
+
+import java.util.AbstractSet;
+import java.util.Collection;
+import java.util.Iterator;
+import java.util.Set;
+
+import lite.BDDSolver;
+import lite.ITLSolver;
+
+public class SBDDSet extends  AbstractSet<SBDDEntry>
+		implements Set<SBDDEntry> {
+	public SBDDEntry[] sbddArray ;
+	public int hash;
+	private int hash0;
+	private int hashSize = 1024;
+	public Object lastEntry;
+	SBDDFactory sf;
+
+	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<SBDDEntry> iterator() {
+		return new Iterator<SBDDEntry>() {
+
+			public boolean hasNext() {
+				return (hash!=hash0 && sbddArray[hash % hashSize]!=null) ;
+			}
+
+			public SBDDEntry next() {
+				return sbddArray[hash++ % hashSize];
+			}
+
+			public void remove() {
+			}
+			
+		};
+	}
+
+	@Override
+	public  boolean contains(Object e) {
+		lastEntry = null;
+		hash = e.hashCode()%hashSize;
+		hash0 = hash-1+hashSize;
+		while(sbddArray[hash%hashSize]!=null && hash!=hash0) {
+			if (sbddArray[hash%hashSize].equals(e)) return true;
+			hash ++;
+		}
+		if (hash!=hash0) lastEntry = e;
+		return false;
+		// return super.contains(e);
+	}
+	
+	
+	@Override
+	public int size() {
+		return hashSize;
+	}
+
+	@Override
+	public boolean add(SBDDEntry e) {
+		// check hash is already set by contains
+		if (lastEntry!=e) {
+			if (contains(e)||hash==hash0) return false;
+		}
+		sbddArray[hash%hashSize] = (SBDDEntry) e;
+		return true;
+	}
+
+	public BDDSolver put(ITLSolver key) {
+		BDDSolver std = key.toSBDD(sf);
+		SBDDEntry e = new SBDDEntry(std);
+		if (contains(e)) {
+			return std;
+		} else {
+			add(e);
+		}
+		return std;
+	}
+
+
+	public String toString() {
+		String s = "SBDDSet[\n";
+		/*
+		for(Entry<ITLSolver, BDDInterface>e : sbddset) {
+			s += e.getValue().hashCode()+":"+e.getValue()+"\n";
+		} */
+		for(int i = 0;i<sbddArray.length;i++) {
+			if (sbddArray[i]!=null) {
+				SBDDEntry e  = sbddArray[i];
+				s += "\t"+i+"\thash="+e.key.hashCode()+":"+e.key+"\n";
+			}
+		}
+		return s+"]";
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/sbdd/SBDDTest.java	Sun Jan 06 21:02:24 2008 +0900
@@ -0,0 +1,73 @@
+package sbdd;
+
+import verifier.Backtrack;
+import lite.BDDSolver;
+import lite.Continuation;
+import lite.ITLNodeFactory;
+import lite.ITLNodeFactoryInterface;
+import lite.ITLNodeParser;
+import lite.ITLSatisfier;
+import lite.ITLSolver;
+import lite.Next;
+
+public class SBDDTest {
+
+
+
+	ITLNodeParser<ITLSolver> p;
+	ITLSatisfier sat;
+	SBDDFactory sf;
+	ITLNodeFactoryInterface<ITLSolver> lf;
+    
+	public static void main(String arg[]) {
+
+		SBDDTest test = new SBDDTest();
+		
+		test.bddTest();
+		test.satTest();
+	}
+	
+	SBDDTest() {
+
+		lf = new ITLNodeFactory();
+		p = new ITLNodeParser<ITLSolver>(lf);
+		sf = new SBDDFactory();
+		sat = new BDDSatisfier(p.emptyNode);
+	}
+	
+	public void bddTest() {
+
+	    BDDSolver b;
+		ITLSolver s = p.parse("p&q");
+		b = s.toSBDD(sf);
+		System.out.println(b);
+	}
+	
+	public void satTest() {
+
+		SBDDTest test = new SBDDTest();
+		
+		test.showAllNext("p&q");
+		test.showAllNext("true&q");
+		test.showAllNext("~(true& ~q)");
+		test.showAllNext("proj(length(3),<>(p))");
+
+	}
+
+	public void showAllNext(String s) {
+		ITLSolver n = p.parse(s);
+		BDDSolver b = n.toSBDD(sf);
+		System.out.println(b);
+		sat.develop(b, new Print());
+		System.out.println(sf.hash);
+		System.out.println();
+	}
+	
+	class Print implements Next {
+		public ITLSolver next(ITLSatisfier sat, Continuation next, ITLSolver value) throws Backtrack {
+			System.out.println(" "+sat.choicePoint()+" -> "+value);
+			throw sat.backtrack;
+		}
+	}
+		
+}