# HG changeset patch
# User kono
# Date 1200509154 -32400
# Node ID 854477cf9aa997471f25df4cfaca662f73a30335
# Parent  75c0ecc1f09a5f52e7dff5cc5de3f99c14385a21
*** empty log message ***

diff -r 75c0ecc1f09a -r 854477cf9aa9 Changes
--- a/Changes	Thu Jan 17 03:20:48 2008 +0900
+++ b/Changes	Thu Jan 17 03:45:54 2008 +0900
@@ -1,3 +1,9 @@
+Thu Jan 17 03:43:53 JST 2008
+
+order を出現順に直しました。
+
+BDDSolver は、ITLSolver と違うので、継承したらだめなのね。
+
 Wed Jan 16 14:32:09 JST 2008
 
 diag も書きましたが、テストする気がしない...
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/BDDSolver.java
--- a/src/lite/BDDSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/BDDSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -169,8 +169,11 @@
 	}
 
 	int order(ITLSolver a,ITLSolver b) {
+		/*
 		// should use hash? or more intelligent order
 		return a.toString().compareTo(b.toString());
+		*/
+		return a.order-b.order;
 	}
 	
 	public BDDSolver toSBDD(SBDDFactoryInterface sf) {
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/ChopSolver.java
--- a/src/lite/ChopSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/ChopSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -159,7 +159,6 @@
 	}
 
 	public boolean equals(Object o) {
-		if (o.hashCode()!=hashCode()) return false;
 		if (o.getClass()==this.getClass()) {
 			ChopSolver v = (ChopSolver)o;
 			return former.equals(v.former)&& later.equals(v.later);
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/EmptySolver.java
--- a/src/lite/EmptySolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/EmptySolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -1,11 +1,16 @@
 package lite;
 
+import parser.TokenID;
 import sbdd.SBDDFactoryInterface;
 import verifier.Backtrack;
 
 public class EmptySolver extends ITLSolver {
 
 	String name = "empty";
+
+	public EmptySolver() {
+		order = TokenID.Empty.hash;
+	}
 	
 	public String toString() {
 		return name;
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/FalseSolver.java
--- a/src/lite/FalseSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/FalseSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -6,6 +6,10 @@
 
 public class FalseSolver extends ITLSolver {
 
+	public FalseSolver() {
+		order = TokenID.False.hash;
+	}
+	
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return next.sat(null);
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/ITLSolver.java
--- a/src/lite/ITLSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/ITLSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -12,6 +12,7 @@
 	
 	public boolean value;
 	public int hash=-1;
+	public int order=-1;
 	
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return null;
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/MacroSolver.java
--- a/src/lite/MacroSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/MacroSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -15,8 +15,6 @@
 	private String body;
 	private MacroNodeParserInterface<ITLSolver> parser;
 	private Command<ITLSolver> command;
-	public int order;
-
 
 	public MacroSolver(ITLSolver macro, String body, int order,
 			Command<ITLSolver> command,
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/lite/TrueSolver.java
--- a/src/lite/TrueSolver.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/lite/TrueSolver.java	Thu Jan 17 03:45:54 2008 +0900
@@ -6,11 +6,14 @@
 
 public class TrueSolver extends ITLSolver {
 
+	public TrueSolver() {
+		order = TokenID.True.hash;
+	}
+
 	@Override
 	public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
 		return next.sat(sat.true_);
 	}
-
 	
 	public String toString() {
 		return "true";
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/sbdd/SBDDFactory.java
--- a/src/sbdd/SBDDFactory.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Thu Jan 17 03:45:54 2008 +0900
@@ -12,10 +12,10 @@
 
 	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 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;
@@ -31,11 +31,11 @@
 		
 		hash.put(falseSolver);
 		hash.put(trueSolver);
-		hash.put(existsSolver);
-		hash.put(nextSolver);
-		hash.put(chopSolver);
+		//hash.put(existsSolver);
+		//hash.put(nextSolver);
+		//hash.put(chopSolver);
 		hash.put(emptySolver);
-		hash.put(projSolver);
+		//hash.put(projSolver);
 	}
 	
 
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/sbdd/SBDDSet.java
--- a/src/sbdd/SBDDSet.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/sbdd/SBDDSet.java	Thu Jan 17 03:45:54 2008 +0900
@@ -16,6 +16,7 @@
 	public Object lastEntry;
 	SBDDFactory sf;
 	int size = 0;
+	private int order = 10;
 
 	SBDDSet() {
 		sbddArray = new SBDDEntry [hashSize];
@@ -89,6 +90,8 @@
 		sbddArray[hash%hashSize] = (SBDDEntry) e;
 		lastEntry = null;
 		e.getValue().id = size++;
+		ITLSolver var = ((BDDSolver)e.getKey()).var;
+		if (var.order==-1) var.order = order ++;
 		return true;
 	}
 
diff -r 75c0ecc1f09a -r 854477cf9aa9 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Thu Jan 17 03:20:48 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Thu Jan 17 03:45:54 2008 +0900
@@ -16,10 +16,10 @@
 
 		SBDDTest test = new SBDDTest();
 		
-		//test.bddTest();
 		//test.satTest();
 		test.verifyTest();
 		//test.mainLoop();
+		test.bddTest();
 	}
 	
 	
@@ -41,6 +41,7 @@
 		bddTest("A?(x;(B?x:C)):false");
 		bddTest("A,x");
 		bddTest("x,A");
+		System.out.println(sf.hash);
 	}
 	
 	public void bddTest(String exp) {