# HG changeset patch
# User kono
# Date 1200563374 -32400
# Node ID aebc899bdc62fdf4825efacb9f8094bec1e9105c
# Parent  400185be1a604fe967c9b4aa18f8572aae453fc3
*** empty log message ***

diff -r 400185be1a60 -r aebc899bdc62 src/sbdd/SBDDSet.java
--- a/src/sbdd/SBDDSet.java	Thu Jan 17 15:00:37 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Thu Jan 17 18:49:34 2008 +0900
@@ -9,6 +9,12 @@
 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;
@@ -16,7 +22,9 @@
 	public Object lastEntry;
 	SBDDFactory sf;
 	int size = 0;
-	private int order = 10;
+	// Multiple SBDDSet is not recomended, but just in case, we make variable
+	// order is shared among existing SBDDSet.
+	private static int order = 10;
 
 	SBDDSet() {
 		sbddArray = new SBDDEntry [hashSize];
diff -r 400185be1a60 -r aebc899bdc62 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Thu Jan 17 15:00:37 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Thu Jan 17 18:49:34 2008 +0900
@@ -19,7 +19,7 @@
 		//test.satTest();
 		test.verifyTest();
 		//test.mainLoop();
-		test.bddTest();
+		//test.bddTest();
 	}
 	
 	
@@ -91,9 +91,10 @@
 		//sat.showVerify("a?(x;(b?x:c)):false");
 		// sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
-		sat.p.parse("include('data/example').");
+		//sat.p.parse("include('data/example').");
 		//System.out.println(p.parseCommand.sat.state);
-		sat.p.parse("do(10)");
+		//sat.p.parse("do(10)");
+		sat.showVerify("length(2),[]p");
 	}
 
 	public void mainLoop() {