--- a/Changes	Thu Dec 27 00:40:28 2007 +0900
+++ b/Changes	Thu Dec 27 19:03:14 2007 +0900
@@ -1,3 +1,9 @@
+Thu Dec 27 00:47:45 JST 2007
+
+あぁ、なんか、はまりすぎ。ITLのparserだけで、まだ、
+かなりかかりそう。で、その後に、展開器と、状態の
+格納か。そういえば、JBDDってのがあったはずだが...
+
 Thu Dec 20 12:53:23 JST 2007
 
 Boolean Satisfier は出来ました。

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ChopSolver.java	Thu Dec 27 19:03:14 2007 +0900
@@ -0,0 +1,17 @@
+package lite;
+
+public class ChopSolver extends ITLSolver {
+
+	private ITLSolver former;
+	private ITLSolver later;
+
+	public ChopSolver(ITLSolver former, ITLSolver later) {
+		this.former = former;
+		this.later = later;
+	}
+
+	public String toString() {
+		return "("+former+" & "+later+")";
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/EmptySolver.java	Thu Dec 27 19:03:14 2007 +0900
@@ -0,0 +1,8 @@
+package lite;
+
+public class EmptySolver extends ITLSolver {
+
+	public String toString() {
+		return "empty";
+	}
+}

--- a/src/lite/ExistsSolver.java	Thu Dec 27 00:40:28 2007 +0900
+++ b/src/lite/ExistsSolver.java	Thu Dec 27 19:03:14 2007 +0900
@@ -22,7 +22,7 @@
 	}
 	
 	public String toString() {
-		return "exists("+var+","+node+")";
+		return "exists("+var+",("+node+"))";
 	}
 
 	@Override

--- a/src/lite/ITLNodeParser.java	Thu Dec 27 00:40:28 2007 +0900
+++ b/src/lite/ITLNodeParser.java	Thu Dec 27 19:03:14 2007 +0900
@@ -3,11 +3,16 @@
 import logicNode.parser.Dictionary;
 import logicNode.parser.LogicNodeScope;
 import logicNode.parser.MacroNodeParser;
+import logicNode.parser.Token;
+import logicNode.parser.TokenID;
 
 public class ITLNodeParser<Node> extends MacroNodeParser<Node> {
 
 	public ITLNodeFactoryInterface<Node> logicNodeFactory;
 	public ITLNodeScanner<Node> scanner;
+	private Token<Node> chopToken;
+	private Token<Node> atToken;
+	private Token<Node> emptyToken;
 	
 	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
 		this();
@@ -30,5 +35,9 @@
 		scope = new LogicNodeScope<Node>(dict);
 		initReservedWord();
 		scanner = new ITLNodeScanner<Node>(dict);
+		
+		chopToken = dict.reserve("&",TokenID.Chop);
+		atToken   = dict.reserve("@",TokenID.Next);
+		emptyToken   = dict.reserve("empty",TokenID.Empty);
 	}
 }

--- a/src/lite/ITLNodeScanner.java	Thu Dec 27 00:40:28 2007 +0900
+++ b/src/lite/ITLNodeScanner.java	Thu Dec 27 19:03:14 2007 +0900
@@ -4,12 +4,9 @@
 
 import logicNode.parser.Dictionary;
 import logicNode.parser.LogicNodeScanner;
-import logicNode.parser.Token;
 
 public class ITLNodeScanner<Node> extends LogicNodeScanner<Node> {
 
-	private Token<Node> chopToken;
-	private Token<Node> atToken;
 
 	/*
 
@@ -29,13 +26,11 @@
 			"\\<\\-\\>|def"
 			);
 	public final static Pattern namePat  = Pattern.compile("[a-zA-Z]\\w*");
-	public final static Pattern intPat  = Pattern.compile("[-+]*[0-9]+");
 	
 	public ITLNodeScanner(Dictionary<Node> dict) {
 		super(dict);
 
-		chopToken = dict.reserve("&");
-		atToken   = dict.reserve("@");
 	}
 
+
 }

--- a/src/lite/ITLSolverTest.java	Thu Dec 27 00:40:28 2007 +0900
+++ b/src/lite/ITLSolverTest.java	Thu Dec 27 19:03:14 2007 +0900
@@ -1,12 +1,21 @@
 package lite;
 
+import logicNode.parser.Dictionary;
+import logicNode.parser.Token;
+
 
 public class ITLSolverTest {
 
 	static ITLNodeParser<ITLSolver> p;
+	static ITLNodeScanner<ITLSolver> scan;
 	
 	public static void main(String arg[]) {
 		ITLNodeFactory lf = new ITLNodeFactory();
+		
+		initScanner();
+		
+		
+		
 		p = new ITLNodeParser<ITLSolver>(lf);
 		
 		System.out.println(p.parse("p & q"));
@@ -22,6 +31,18 @@
 		sat("true");
 	}
 
+	public static void initScanner() {
+		Dictionary<ITLSolver> dict = new Dictionary<ITLSolver>();
+		scan = new ITLNodeScanner<ITLSolver>(dict);
+	}
+
+	public static void scan(String exp) {
+		for(Token<ITLSolver> t : scan.scanToken(exp)) {
+			System.out.print(t+" ");
+		}
+		System.out.println();
+	}
+	
 	public static void sat(String expr) {
 		ITLSolver n;
 		n = p.parse(expr);

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/NextSolver.java	Thu Dec 27 19:03:14 2007 +0900
@@ -0,0 +1,14 @@
+package lite;
+
+public class NextSolver extends ITLSolver {
+
+	ITLSolver node;
+	public NextSolver(ITLSolver node) {
+		this.node = node;
+	}
+		
+	public String toString() {
+		return "@("+node+")";
+	}
+
+}