--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLNodeFactory.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,75 @@
+package lite;
+
+import java.util.LinkedList;
+
+import logicNode.parser.LogicNodeParser;
+import logicNode.parser.MacroNodeParser;
+
+public class ITLNodeFactory implements	ITLNodeFactoryInterface<ITLSolver> {
+
+	public ITLSolver chopNode(ITLSolver former, ITLSolver later) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver emptyNode() {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver nextNode(ITLSolver node) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver macroNode(ITLSolver macro, String body) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver predicateNode(ITLSolver predicate, LinkedList<ITLSolver> arg, MacroNodeParser<ITLSolver> name) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver andNode(ITLSolver left, ITLSolver right) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver existsNode(ITLSolver var, ITLSolver node) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver falseNode() {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver notNode(ITLSolver node) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver orNode(ITLSolver left, ITLSolver right) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver predicateNode(ITLSolver predicate, LinkedList<ITLSolver> arg, LogicNodeParser<ITLSolver> parser) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver trueNode() {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public ITLSolver variableNode(String name, boolean value) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLNodeFactoryInterface.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,11 @@
+package lite;
+
+import logicNode.MacroNodeFactoryInterface;
+
+public interface ITLNodeFactoryInterface<T> extends MacroNodeFactoryInterface<T> {
+
+	public T chopNode(T former, T later) ;
+	public T emptyNode();
+	public T nextNode(T node);
+	
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLNodeParser.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,20 @@
+package lite;
+
+import logicNode.parser.MacroNodeParser;
+
+public class ITLNodeParser<Node> extends MacroNodeParser<Node> {
+
+	public ITLNodeFactoryInterface<Node> logicNodeFactory;
+	public ITLNodeScanner<Node> scanner;
+	
+	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
+		this();
+		logicNodeFactory = lf;
+		super.logicNodeFactory = logicNodeFactory;
+		initialize();
+	}
+
+	public ITLNodeParser() {
+		super();
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLNodeScanner.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,13 @@
+package lite;
+
+import logicNode.parser.Dictionary;
+import logicNode.parser.LogicNodeScanner;
+
+public class ITLNodeScanner<T> extends LogicNodeScanner<T> {
+
+	public ITLNodeScanner(Dictionary<T> dict) {
+		super(dict);
+		// TODO Auto-generated constructor stub
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLSatisfier.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,40 @@
+package lite;
+
+import verifier.Backtrack;
+import verifier.ChoicePointList;
+import verifier.Continuation;
+import verifier.LogicSolver;
+import verifier.Next;
+import verifier.Satisfier;
+
+public class ITLSatisfier implements ChoicePointList<ITLSolver>, Next {
+
+	public ITLSatisfier(ITLSolver true_) {
+		// TODO Auto-generated constructor stub
+	}
+
+	public void addChoicePoint(ITLSolver cp) {
+		// TODO Auto-generated method stub
+		
+	}
+
+	public void deleteChoicePoint(ITLSolver cp) {
+		// TODO Auto-generated method stub
+		
+	}
+
+	public boolean hasChoicePoint(ITLSolver cp) {
+		// TODO Auto-generated method stub
+		return false;
+	}
+
+	public LogicSolver next(Satisfier sat, Continuation next, LogicSolver value) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	public Object satisfiable(ITLSolver n) {
+		// TODO Auto-generated method stub
+		return null;
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLSolver.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,28 @@
+package lite;
+
+import verifier.Backtrack;
+import verifier.Continuation;
+import verifier.LogicSolver;
+import verifier.Satisfier;
+
+public class ITLSolver extends LogicSolver {
+
+	@Override
+	public ITLSolver sat(Satisfier sat, Continuation next) throws Backtrack {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public String toString() {
+		// TODO Auto-generated method stub
+		return null;
+	}
+
+	@Override
+	public boolean value() {
+		// TODO Auto-generated method stub
+		return false;
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/lite/ITLSolverTest.java	Wed Dec 26 11:48:51 2007 +0900
@@ -0,0 +1,35 @@
+package lite;
+
+
+public class ITLSolverTest {
+
+	static ITLNodeParser<ITLSolver> p;
+	static ITLSolver true_;
+	
+	public static void main(String arg[]) {
+		ITLNodeFactory lf = new ITLNodeFactory();
+		true_= lf.trueNode();
+		
+		p = new ITLNodeParser<ITLSolver>(lf);
+		sat("false");
+		sat("true");
+	}
+
+	public static void sat(String expr) {
+		ITLSolver n;
+		n = p.parse(expr);
+		if (n!=null) {
+			ITLSatisfier sat = new ITLSatisfier(true_);
+
+			System.out.print(n);
+
+			if (sat.satisfiable(n)!=null) {
+				System.out.println(" is satisfiable.");
+			} else {
+				System.out.println(" is unsatisfiable.");
+			}
+		} else {
+			System.out.println("can't parse '"+expr+"'.");
+		}
+	}
+}