# HG changeset patch
# User kono
# Date 1200535759 -32400
# Node ID c263dc76d1a788b528a1b43df571104c291752a2
# Parent  70cc3ff5c73ba5f135bf554c5a0eee69ebc907a7
comments

diff -r 70cc3ff5c73b -r c263dc76d1a7 src/sbdd/BDDSatisfier.java
--- a/src/sbdd/BDDSatisfier.java	Thu Jan 17 11:09:15 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Thu Jan 17 11:09:19 2008 +0900
@@ -31,6 +31,15 @@
 	boolean falsifiable,satisfiable;
 
 	/**
+	 * Tableau expansion verifier for ITL with Subterm BDD.
+	 * 
+	 * develop() try to find satisfiable choice point list for the ITL
+	 * formula. allNext() stores generated next time ITL formula in
+	 * a queue and SBDD Hash table ( SBDDEntry ). verify() repeats
+	 * develop() over the queue, until no more new states are generated.
+	 * 
+	 * If we have no true in SBDD Hash, the formula is unsatisfiable.
+	 * These are checked by BDDDiagnosis.
 	 * 
 	 */
 	private static final long serialVersionUID = 1L;
@@ -39,10 +48,7 @@
 	public void init() {
 		lf = new ITLNodeFactory();
 		p = new ITLNodeParser<ITLSolver>((ITLNodeFactoryInterface<ITLSolver>) lf);
-		// p.setExecutor(this);
 		sf = new SBDDFactory();
-		// empty = ITLNodeFactory.emptySolver;
-		// empty = SBDDFactory.emptySolver;
 		empty = lf.emptyNode();
 	}
 	
diff -r 70cc3ff5c73b -r c263dc76d1a7 src/sbdd/SBDDEntry.java
--- a/src/sbdd/SBDDEntry.java	Thu Jan 17 11:09:15 2008 +0900
+++ b/src/sbdd/SBDDEntry.java	Thu Jan 17 11:09:19 2008 +0900
@@ -16,6 +16,21 @@
 	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>();
diff -r 70cc3ff5c73b -r c263dc76d1a7 src/sbdd/SBDDFactory.java
--- a/src/sbdd/SBDDFactory.java	Thu Jan 17 11:09:15 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Thu Jan 17 11:09:19 2008 +0900
@@ -12,10 +12,6 @@
 
 	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 projSolver   = new BDDSolver(BDDID.Projection,TokenID.Projection.hash);
 	public static final ITLSolver emptySolver  = new BDDSolver(ITLNodeFactory.emptySolver,trueSolver,falseSolver,BDDID.BDD);
 	public SBDDSet hash;
 	ITLNodeFactory itlf;
@@ -27,22 +23,14 @@
 	void init() {
 		hash = new SBDDSet(this);
 		itlf = new ITLNodeFactory();
-		// emptySolver = new BDDSolver(ITLNodeFactory.emptySolver,BDDID.Empty,TokenID.Empty.hash);
-		
+
 		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) {
-		// too slow and we don't need it (?)
-		//solver = hash.put(solver);
-		//solver2 = hash.put(solver2);
 		if (solver==solver2) return solver;
 		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
 		return hash.put(v); 
diff -r 70cc3ff5c73b -r c263dc76d1a7 src/sbdd/SBDDSet.java
--- a/src/sbdd/SBDDSet.java	Thu Jan 17 11:09:15 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Thu Jan 17 11:09:19 2008 +0900
@@ -110,10 +110,6 @@
 
 	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];