--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/Command.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,8 @@
+package parser;
+
+import java.util.LinkedList;
+
+
+public interface Command<Node> {
+	Node exec(Node predicate, Node value, LinkedList<Node>args);
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/Dictionary.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,26 @@
+package parser;
+
+import java.util.HashMap;
+
+public class Dictionary<Node> extends HashMap<String,Token<Node>> {
+
+	private static final long serialVersionUID = 1L;
+
+	public Token<Node> reserve(String name,TokenID type) {
+		Token<Node> t = new Token<Node>(name,type);
+		this.put(name, t);
+		return t;
+	}
+	
+
+	public Token<Node> reserve(String name,TokenID type, int order) {
+		Token<Node> t = new Token<Node>(name,type,order);
+		this.put(name, t);
+		return t;
+	}
+
+
+	public Token<Node> reserve(String string) {
+		return reserve(string,TokenID.Any);
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/ExecutorInterface.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,7 @@
+package parser;
+
+public interface ExecutorInterface<Node> {
+
+	public void verify(Node n);
+
+}
\ No newline at end of file

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeFactoryInterface.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,30 @@
+package parser;
+
+import java.util.LinkedList;
+
+public interface LogicNodeFactoryInterface<T> {
+    public T andNode(T left, T right) ;
+
+    public T orNode(T left, T right) ;
+    
+    public T notNode(T node) ;
+
+    public T bddNode(T cond, T high, T value);
+    
+    public T variableNode(String name,boolean value);
+    
+    public T existsNode(T var,T node);
+
+    public T trueNode();
+
+    public T falseNode() ;
+    
+    public T predicateNode(T predicate, LinkedList<T> arg);
+    
+    public T numberNode(int num);
+
+	public T macroNode(T macro, String body, int order, Command<T>command, 
+			MacroNodeParserInterface<T> parser);
+	
+}
+

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeParser.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,275 @@
+package parser;
+
+import java.io.FileNotFoundException;
+import java.io.InputStream;
+import java.util.LinkedList;
+
+import verifier.LogicSolver;
+
+
+public class LogicNodeParser<Node extends LogicSolver> {
+
+	/*
+	 * Simple Logic Node Parser
+	 * 
+	 *    Syntax is based on Prolog implementation of LITE verifier, but
+	 *    it is not an operator order grammer parser. Currently we use
+	 *    object comparison, but it is better to use id, because we can
+	 *    use switch statements.
+	 *    
+	 *    Tokenize is done by Scanner. Nested parsing (necesssary for macro
+	 *    expansion) is done by scanner.push()/pop().
+	 *    
+	 *    Scope is handled by association linked list based scope. Use scope.push()/pop()
+	 *    and scope.getLocalName(s).
+	 *    
+	 *    All nodes are created by logicnNodeFactory. In order to handle various
+	 *    logic, constructed Node is parameterized.
+	 *    
+	 *               2007/12 Shinji Kono
+	 */
+	
+	public LogicNodeFactoryInterface<Node> logicNodeFactory;
+	public LogicNodeScanner<Node> scanner;
+	public Dictionary<Node> dict;
+	public LogicNodeScope<Node> scope;
+	public int position;
+	public int end;
+	public Token<Node> nextToken;
+	private ExecutorInterface<Node> exec = new NullExecutor<Node>();
+
+	public LogicNodeParser() {
+		super();
+		initialize();
+	}
+
+	public LogicNodeParser(String string, LogicNodeFactoryInterface<Node> lf) {
+		super();
+		logicNodeFactory = lf;
+		initialize();
+		scanner.set(string);
+	}
+
+	public void initReservedWord() {
+		dict.reserve(",",TokenID.And);
+		dict.reserve(";",TokenID.Or);
+
+		dict.reserve("(",TokenID.Paren);
+		dict.reserve(")",TokenID.CloseParen);
+		dict.reserve("{",TokenID.CurParen);
+		dict.reserve("}",TokenID.CloseCurParen);
+		dict.reserve("[",TokenID.BParen);
+		dict.reserve("]",TokenID.CloseBParen);
+		dict.reserve("~",TokenID.Not);
+		dict.reserve(".",TokenID.Period);
+		dict.reserve("?",TokenID.Question);
+		dict.reserve(":",TokenID.Colon);
+		dict.reserve("exists",TokenID.Exists);
+		dict.reserve("true",TokenID.True);
+		dict.reserve("false",TokenID.False);
+	}
+
+	public void initialize() {
+		dict = new Dictionary<Node>();
+		scope = new LogicNodeScope<Node>(null,dict);
+		initReservedWord();
+		scanner = new LogicNodeScanner<Node>(dict);
+	}
+
+	public Node parse() {
+		if (scanner==null) return null;
+		nextToken();
+		return expr1();
+	}
+
+	public Node parse(String exp) {
+		Node n;
+		scanner = scanner.pushScanner(exp);
+		n = parse();
+		scanner = scanner.popScanner();
+		nextToken = scanner.nextToken;
+		return n;
+		
+	}
+
+	public void parseFile(String file) {
+		try {
+			scanner = scanner.pushScannerFile(file);
+		} catch (FileNotFoundException e) {
+			error("Can't open "+file);
+			return;
+		}
+		doParse();
+	}
+	
+	public void parse(InputStream file) {
+		scanner = scanner.pushScannerFile(file);
+		doParse();
+	}
+
+	public Node doParse() {
+		Node n;
+		do {
+			n=parse();
+			exec.verify(n);
+		} while(scanner.hasRemaining());
+		scanner = scanner.popScanner();
+		nextToken = scanner.nextToken;
+		return n;
+	}
+
+	public Node expr1() {
+	    Node n = expr2();
+		while(nextToken.type == TokenID.Or) {
+			nextToken();
+			n = logicNodeFactory.orNode(n, expr2());
+		}
+		return n;
+	}
+
+	public Node expr2() {
+		Node n = expr3();
+		while(nextToken.type == TokenID.And) {
+			nextToken();
+			n = logicNodeFactory.andNode(n, expr3());
+		}
+		return n;
+	}
+
+	public Node expr3() {
+		if (nextToken.type==TokenID.Not) {
+			nextToken();
+			return logicNodeFactory.notNode(expr3());
+		} else if (nextToken.type==TokenID.Exists) {
+			return quantifier();
+		}
+		return expr4();
+	}
+
+	/*
+	 * exists(x,(x,a))
+	 *      this operator has a local scope
+	 */
+	public Node quantifier() {
+		LinkedList<Node> arg;
+		nextToken();
+		if (nextToken.type==TokenID.Paren) {
+			// symbolc x havs been already converted to a variable when it was
+			// evaluated as a macro argument. We cannot make it local here.
+			// Do it in exists evaluation. 
+			nextToken();
+			arg = arguments();
+			if (arg.size()!=2 /* || !arg.get(0).isVariable() */) {
+				error("bad quantifier");
+				return logicNodeFactory.trueNode();
+			}
+			return logicNodeFactory.existsNode(arg.get(0),arg.get(1));
+		} else {
+			error("( expected");
+			return logicNodeFactory.trueNode();
+		}
+	}
+
+	public Node expr4() {
+		Node n = term();
+		if (nextToken.type==TokenID.Paren) {
+			// predicate ( or macro )
+			nextToken();
+			n = logicNodeFactory.predicateNode(n,arguments());
+		}
+		return n;
+	}
+
+	protected LinkedList<Node> arguments() {
+		Node n;
+		LinkedList<Node> arg = new LinkedList<Node>();
+		while(nextToken.type!=TokenID.CloseParen) {
+			n = expr3();
+			arg.add(n);
+			if (nextToken.type == TokenID.And)
+				nextToken();
+		}
+		if (nextToken.type==TokenID.CloseParen) nextToken();
+		else {
+			scanner.error(") expected");
+		}
+		return arg;
+	}
+
+	protected Node term() {
+		Node n = null;
+		switch (nextToken.type) {
+		case Paren:
+			nextToken();
+			n = expr1();
+			if (nextToken.type==TokenID.CloseParen) {
+			} else { // syntax error;
+				scanner.error(") expected but got "+nextToken);
+				return logicNodeFactory.trueNode();
+			}
+			break;
+		case CurParen:
+			nextToken();
+			n = expr1();
+			if (nextToken.type==TokenID.CloseCurParen) {
+			} else { // syntax error;
+				scanner.error("} expected");
+			}
+			break;
+		case NUMBER:
+			n = logicNodeFactory.numberNode(Integer.parseInt(nextToken.name));
+			break;
+		case True:
+			n = logicNodeFactory.trueNode();
+			break;
+		case False:
+			n = logicNodeFactory.falseNode();
+			break;
+		case NULL: case Period:
+			break;
+		default:
+			if (nextToken.type.isVariable()) 
+				n = makeVariable(nextToken);
+			else {
+				// error("Internal ununderstandable term '"+nextToken+"' type: "+nextToken.type+".");
+				n = makeVariable(nextToken); // skip any
+			}
+		}
+		nextToken();
+		return n;
+	}
+	/*
+	 * All names in LogicNode are variables. A token represents
+	 * name. To get the variable, use this method.
+	 */
+	protected Node makeVariable(Token<Node> t) {
+		Node n;
+		if ((n=t.value())==null) {
+			n =  logicNodeFactory.variableNode(t.realName(),true);
+			t.setValue(n);
+		}
+		// n.token = t;
+		return n;
+	}
+
+	/*
+	 * Syntactical Short cut for scanner.textToken()
+	 * 
+	 * It never returns null, to check EOF, 
+	 *     nextToken.type==TokenID.NULL
+	 */
+	public Token<Node> nextToken() {
+		return nextToken = scanner.nextToken();
+	}
+
+	public void setExecutor(ExecutorInterface<Node> exec) {
+		this.exec = exec;
+	}
+
+	public void error(String err) {
+		scanner.error(err);
+	}
+
+
+	
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeParserTest.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,53 @@
+package parser;
+
+import verifier.LogicSolver;
+import verifier.LogicSolverFactory;
+
+public class LogicNodeParserTest {
+	
+	static MacroNodeParser<LogicSolver> parser;
+	
+	public static void main(String arg[]) {
+		LogicNodeParser<LogicSolver> p;
+		LogicSolver n;
+		LogicNodeFactoryInterface<LogicSolver> lf = new LogicSolverFactory(); 
+		if (true) {
+		p = new LogicNodeParser<LogicSolver>("a,(b;~c)",lf);
+		n = p.parse();
+		if (n!=null) System.out.print(n); System.out.println(".");
+		}
+		
+		p = new LogicNodeParser<LogicSolver>("exists(x,(a,x))",lf);
+		n = p.parse();
+		if (n!=null) System.out.print(n); System.out.println(".");
+		
+		parser = (MacroNodeParser<LogicSolver>) p;
+		n = parser.parse();
+		if (n!=null) System.out.print(n); System.out.println(".");
+		
+		sat("~exists(x,(x,b))");
+		
+		parser.define("forall(x,body)", "~exists(x,(~body))");
+		sat("forall(a,(a,~a))");
+		
+		parser.define("P->Q","(not (P);Q))",300);             // imply
+		sat("p->q");
+		parser.define("not R","~R",50);
+		sat("p->q");
+		
+		parser.define("P and Q", "(P,Q)",200);
+		
+		sat("p , q , r");
+		sat("p and q and r");
+		sat("p -> q and r");
+		sat("p and q and r -> s");				
+		sat("p and q -> r -> s");		
+		sat("p -> q -> r and s");
+		sat("p -> q and r and s");
+	}
+	
+	public static void sat(String s) {
+		LogicSolver n = parser.parse(s);
+		if (n!=null) System.out.print(n); System.out.println(".");
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeScanner.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,291 @@
+package parser;
+
+import java.io.FileNotFoundException;
+import java.io.FileReader;
+import java.io.IOException;
+import java.io.InputStream;
+import java.io.InputStreamReader;
+import java.nio.CharBuffer;
+import java.util.Iterator;
+import java.util.regex.Matcher;
+import java.util.regex.Pattern;
+
+
+public class LogicNodeScanner<Node> {
+
+	/*
+	 * Tokenizer for LogicNode Parser
+	 *     Pattern/Matcher implementation
+	 *     
+	 *     sannerStack is used for nested parsing.
+	 *         scanner.push();
+	 *         parser.parse(exp);
+	 *         nextToken = scanner.pop();
+	 *         
+	 *     2007/12 Shinji Kono    
+	 */
+	
+	public int lineno;
+	public Matcher scan;
+	public Token<Node> nextToken;
+	public Dictionary<Node> dict;
+	public LogicNodeScanner next;
+	protected CharBuffer cb;
+	private InputStreamReader file;
+	private String filename;
+	public LogicNodeScanner<Node> prev;
+	public Token<Node> nullToken ;
+
+	public LogicNodeScanner(Dictionary<Node> dict) {
+		this.dict = dict;
+		nullToken = new Token<Node>("",TokenID.NULL,0);
+	}
+	
+	/*
+	 * Scanner Container for Stack
+	 */
+	public LogicNodeScanner(LogicNodeScanner<Node> prev, Dictionary<Node> dict, Token<Node> nullToken) {
+		this.prev = prev;
+		this.dict = dict;
+		this.nullToken = nullToken;
+	}
+
+
+	// Pattern must contain exact 1 group
+	public static Pattern tokenPat = Pattern.compile(
+			"(\\&\\&|[*\\?\\:\\^.()+{},;~\\&@]|\\[\\]|\\:\\=|\\<\\=|\\<\\>|\\=\\>|\\=|" +
+			"\\<\\-\\>|\\-\\>|\\<\\-|\\[|\\])"
+			);
+	public static Pattern namePat  = Pattern.compile("([a-zA-Z]\\w*)");
+	public static final Pattern numPat  = Pattern.compile("([0-9]+)");
+	public static final Pattern stringPat1  = Pattern.compile("\\\"([^\"]*)\\\"");
+	public static final Pattern stringPat  = Pattern.compile("\\'([^\\']*)\\'");
+	public static final Pattern commentPat  = Pattern.compile("(%.*)");
+	public static final Pattern errorPat = Pattern.compile("([^\\s])");
+	public static final Pattern anyPat = Pattern.compile("(.)");
+	private static final int BufferSize = 4096;
+
+	/*
+	 * Get next token
+	 * 
+	 *    No looking up method nor put back. It never returns null but
+	 *    may return nullToken. So nextToken.type is always valid.
+	 *    nullToken means the end of the input.
+	 *    
+	 *    Token is a syntax element and it may have macro binidng as
+	 *    predicate, infix or prefix operaotor. To get the value, use
+	 *    makeVariable(). Operator order for infix and prefix is in
+	 *    Token.order. TokenID.order is default order for fix element and
+	 *    currently never used.
+	 *    
+	 *    When matcher hit an end of the input, hasRemaining() method try
+	 *    to extend the input using extendInput().
+	 */
+	
+	public Token<Node> nextToken() {
+		String s;
+		nextToken = nullToken;
+		while(hasRemaining()) {
+			scan.reset(); // to tell CharBuffer is modified
+			if ((s=next(tokenPat))!=null) {
+				Token<Node> t;
+				if ((t = dict.get(s))==null) {
+					dict.put(s, t = new Token<Node>(s,TokenID.Any));
+				}
+				return nextToken = t;
+			} else if ((s=next(stringPat))!=null||(s=next(namePat))!=null) {
+				Token<Node> t;
+				if ((t = dict.get(s))==null) {
+					dict.put(s, t = new Token<Node>(s,TokenID.VARIABLE));
+				}
+				return nextToken = t;
+			} else if ((s=next(numPat))!=null) {
+				return nextToken = new Token<Node>(s,TokenID.NUMBER);
+			} else if ((s=next(stringPat1))!=null) {
+				return nextToken = new Token<Node>(s,TokenID.STRING);
+			} else if ((s=next(commentPat))!=null) {
+				while(cb.hasRemaining()&&next(anyPat)!=null); // skip until eol (in case of buffer full)
+				continue;
+			} else if ((s=next(errorPat))!=null) {
+				error("Don't understand '"+s+"'");
+				continue;
+			} else if ((s=next(anyPat))!=null) {
+				// skip space
+				continue;
+			} else {
+				lineno++;
+				cb.get(); // discard one ( new line )
+			}
+		}
+		return nextToken;
+	}
+
+	protected String next(Pattern pattern) {
+		String s = null;
+		while(true) {
+			Boolean match = scan.usePattern(pattern).lookingAt();
+			if (scan.hitEnd()) {
+				if (extendInput()) {
+					// input is extended try again
+					scan.reset();
+					continue;
+				}
+				// no extension.
+			}
+			if (match) {
+				s = scan.group(1);
+				// fix position in CharBuffer
+				// scan.end() is relative position
+				cb.position(cb.position()+scan.end());
+				// scan.reset(); will be done on top of nextToken()
+			}
+			if (scan.hitEnd()) {
+				// previous extendInput is failed because of Buffer full.
+				// Now we have a space. Try again
+				extendInput();scan.hitEnd();
+			}
+			return s;
+		}
+	}
+	
+	public boolean hasRemaining() {
+		return cb.hasRemaining()||extendInput();
+	}
+
+	/*
+	 *    Extend Input data
+	 */
+	protected boolean extendInput() {
+		if (file!=null && cb.position()!=0) {
+			// move remaining data to the top, set position for next read
+			cb.compact();
+			try {
+				if (file.read(cb)>0) {
+					cb.flip();    // prepare for get (but we don't...) 
+					return true;
+				} else {
+					throw new IOException();
+				}
+			} catch (IOException e) {
+				file = null ; 
+				cb.flip();
+			}
+		}
+		return false;
+	}
+
+	protected LogicNodeScanner<Node> pushScanner(String exp) {
+		// Save current matcher for nested parsing
+		return new LogicNodeScanner<Node>(this,dict,nullToken).set(exp);
+	}
+	
+	protected LogicNodeScanner<Node> pushScannerFile(String newfile) throws FileNotFoundException {
+		// Save current matcher for nested file
+		return new LogicNodeScanner<Node>(this,dict,nullToken).setFile(newfile);
+	}
+
+	public LogicNodeScanner<Node> pushScannerFile(InputStream newfile) {
+		return new LogicNodeScanner<Node>(this,dict,nullToken).setFile(newfile);
+	}
+
+	protected LogicNodeScanner<Node> popScanner() {
+		return prev;
+	}
+
+	private LogicNodeScanner<Node> findFileName() {
+		for(LogicNodeScanner<Node> s = this;s!=null ; s = s.prev) {
+			if (s.filename!=null) return s;
+		}
+		return null;
+	}
+	/*
+	 * Read From String
+	 */
+	
+	public LogicNodeScanner<Node> set(String exp) {
+		cb = CharBuffer.wrap(exp);
+		scan = tokenPat.matcher(cb);
+		filename = null; file = null;
+		nextToken = nullToken;
+		return this;
+	}
+	
+	/*
+	 * Read From File
+	 *    We cannot read symbol bigger than Buffersize
+	 */
+	public LogicNodeScanner<Node> setFile(String file) throws FileNotFoundException {
+		this.filename = file;
+		nextToken = nullToken;
+		set(new FileReader(file));
+		return this;
+	}
+	
+	public LogicNodeScanner<Node> set(InputStreamReader file) {
+		this.file = file;
+		cb = CharBuffer.allocate(BufferSize);
+		try {
+			if (file.read(cb) <= 0) {
+				throw new IOException();
+			}
+		} catch (IOException e) {
+			file = null; cb = null;
+			set("");
+			return this;
+		} finally {
+			cb.flip();
+		}
+		scan = tokenPat.matcher(cb);
+		lineno = 0;
+		return this;
+	}
+	
+	public void error(String err) {
+		LogicNodeScanner<Node> s = findFileName();
+		if (s!=null) {
+			System.err.print(s.filename+":"+s.lineno+": ");
+		}
+		System.err.println("error: "+err);
+	}
+	
+	/*
+	 * Iterator for Test Routing
+	 *    for(Token<Node> t: scanner.scanToken(FileReader(file)) { ... }
+	 */
+
+	public Iterable<Token<Node>> scanToken(String exp) {
+		set(exp);
+		return iterator();
+	}
+	
+	public Iterable<Token<Node>> scanToken(FileReader file) {
+		set(file);
+		return iterator();
+	}
+
+	private Iterable<Token<Node>> iterator() {
+		return new Iterable<Token<Node>>() {
+			public Iterator<Token<Node>> iterator() {
+				return new Iterator<Token<Node>>() {
+					public boolean hasNext() {
+						return hasRemaining();
+					}
+					public Token<Node> next() {
+						return nextToken();
+					}
+					public void remove() {
+					}
+				};
+			}
+		};
+	}
+
+	private LogicNodeScanner<Node> setFile(InputStream newfile) {
+		this.filename = newfile.toString();
+		nextToken = nullToken;
+		set(new InputStreamReader(newfile));
+		return this;
+	}
+
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeScannerTest.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,48 @@
+package parser;
+
+import java.io.FileNotFoundException;
+import java.io.FileReader;
+
+import verifier.LogicSolver;
+
+public class LogicNodeScannerTest {
+	
+	public static LogicNodeScanner<LogicSolver> scan;
+
+	public static void main(String arg[]) {
+		initScanner();
+		if (arg.length==0) {
+			arg = new String[1];
+			arg[0] = "test";
+		}
+		for(String file: arg) {
+			try {
+				scan(new FileReader(file));
+			} catch (FileNotFoundException e) {
+				scan(file);
+			}
+		}
+	}
+	
+	public static void initScanner() {
+		Dictionary<LogicSolver> dict = new Dictionary<LogicSolver>();
+		scan = new LogicNodeScanner<LogicSolver>(dict);
+	}
+
+
+	public static void scan(String exp) {
+		for(Token<LogicSolver> t : scan.scanToken(exp)) {
+			System.out.print(t+" ");
+		}
+		System.out.println();
+	}
+	
+	public static void scan(FileReader file) {
+		for(Token<LogicSolver> t : scan.scanToken(file)) {
+			System.out.print(t+" ");
+			System.out.println();
+		}
+	}
+	
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/LogicNodeScope.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,48 @@
+package parser;
+
+import java.util.TreeMap;
+
+/*
+ * Scope mechnism for local variable
+ *    exists(x,(x,y))
+ *    previous x token is stored in assocation list
+ *    pop() remove local x token and restore previous x
+ *    previous x may be null. 
+ */
+public class LogicNodeScope<Node> {
+	public TreeMap<String,Token<Node>> scope;
+	public Dictionary<Node> dict;
+	public LogicNodeScope<Node> prev;
+	
+
+	public LogicNodeScope(LogicNodeScope<Node>prev, Dictionary<Node> dict) {
+		this.dict = dict;
+		this.prev = prev;
+		this.scope = new TreeMap<String,Token<Node>>();
+	}
+	
+
+	// enter the scope
+	public LogicNodeScope<Node> push() {
+		return new LogicNodeScope<Node>(this,dict);
+	}
+	
+	// exit the scope
+	public LogicNodeScope<Node> pop() {
+		// restore local variable name
+		for(String name: scope.keySet()) {
+			Token<Node> t = scope.get(name);
+			dict.put(name, t); // overwrite
+		}
+		return prev;
+	}
+	
+	// make new local name in this scope
+	public Token<Node> getLocalName(String name) {
+		Token<Node> n = new Token<Node>(name);
+		Token<Node> t=dict.get(name);
+		scope.put(name, t); // remember original
+		dict.put(name,n);   // overwrite entry with new one
+		return n;
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/MacroNodeParser.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,291 @@
+package parser;
+
+import java.util.LinkedList;
+
+import verifier.LogicSolver;
+
+public class MacroNodeParser<Node extends LogicSolver>
+     extends LogicNodeParser<Node> 
+	 implements MacroNodeParserInterface<Node> {
+
+	/*
+	 * Logic Node Parser with Macro Expansion
+	 *       parser.define("head(var)","body = var");
+	 *       "head(x+1)" is replcaed by "body = (x+1)" and parsed
+	 *       
+	 *  A macro definition is stored in MacroNode. The MacroNode is stored in
+	 *  dict by MacroNodeFactory.predicateNode(); MacroNode has to know the parser
+	 *  to parse expanded macro. It is possible to parse macro body before expansion,
+	 *  but its implementation is sligtly complex.      
+	 */
+	
+	public LogicNodeFactoryInterface<Node> logicNodeFactory;
+	
+	public MacroNodeParser() {
+		super();
+	}
+
+	public MacroNodeParser(String str, LogicNodeFactoryInterface<Node> lf) {
+		this();
+		logicNodeFactory = lf;
+		super.logicNodeFactory = logicNodeFactory;
+		initialize();
+		scanner = scanner.pushScanner(str);
+	}
+	
+	public MacroNodeParser(LogicNodeFactoryInterface<Node> lf) {
+		this();
+		logicNodeFactory = lf;
+		super.logicNodeFactory = logicNodeFactory;
+		initialize();
+	}
+
+	@Override
+	public Node expr2() {
+		Node n = exprM1();
+		while(nextToken.type == TokenID.And) {
+			nextToken();
+			n = logicNodeFactory.andNode(n, exprM1());
+		}
+		return n;
+	}
+
+	/*
+	 *   Recurseive Decent with operator order
+	 *      n1 op n2 op2 ...
+	 *      
+	 *      When the nextToken is a macro, nextToken.type is
+	 *      TokenID.VARIABLE, that is nextToken.type.order==1. 
+	 *      MacroNode constructor assign the order in Token.order. 
+	 *      Don't use Token.type.order.
+	 */
+	public Node exprM1() {
+		return exprM2(expr3());
+	}
+	
+	public Node exprM2(Node n1) {
+		while (nextToken.isInfix()) {
+			Node op = makeVariable(nextToken);
+			LinkedList<Node> arg = new LinkedList<Node>();
+			arg.add(n1);
+			nextToken();
+			Node n2 = expr3();
+			if (!nextToken.isInfix()) {
+				arg.add(n2);
+				return logicNodeFactory.predicateNode(op, arg);
+			} 
+			if (op.order() > nextToken.order) {    // a + b * 
+				arg.add(exprM2(n2));
+				return logicNodeFactory.predicateNode(op, arg);
+			} else {                               // a * b + 
+				arg.add(n2);
+				n1 = logicNodeFactory.predicateNode(op, arg);
+			}
+		}
+		return n1;
+	}
+
+
+	@Override
+	public Node expr3() {
+		if (nextToken.type==TokenID.Not) {
+			nextToken();
+			return logicNodeFactory.notNode(expr3());
+		} else if (nextToken.isPrefix()) {
+			Node op = makeVariable(nextToken);
+			LinkedList<Node> arg = new LinkedList<Node>();
+			nextToken();
+			arg.add(expr3());
+			return logicNodeFactory.predicateNode(op, arg );
+		} else if (nextToken.type==TokenID.Exists) {
+			return quantifier();
+		}
+		return expr4();
+	}
+
+	@Override
+	public Node expr4() {
+	    if (nextToken.syntax==TokenID.ALIAS) {
+		    LinkedList<Node> arg = new LinkedList<Node>(); // empty
+		    Node op = makeVariable(nextToken);
+		    nextToken();
+		    return logicNodeFactory.predicateNode(op, arg );
+	    }
+		Node n = term();
+		if (nextToken.type==TokenID.Paren) {
+			// predicate ( or macro )
+			nextToken();
+			n = logicNodeFactory.predicateNode(n,arguments());
+		} else if (nextToken.syntax==TokenID.ALIAS) {
+			LinkedList<Node> arg = new LinkedList<Node>(); // empty
+			Node op = makeVariable(nextToken);
+			nextToken();
+			return logicNodeFactory.predicateNode(op, arg );
+		}
+		return n;
+	}
+
+	@Override
+	protected LinkedList<Node> arguments() {
+		Node n;
+		LinkedList<Node> arg = new LinkedList<Node>();
+		while(nextToken.type!=TokenID.CloseParen) {
+			n = exprM1();
+			arg.add(n);
+			if (nextToken.type == TokenID.And)
+				nextToken();
+		}
+		if (nextToken.type==TokenID.CloseParen) nextToken();
+		else {
+			scanner.error(") expected");
+		}
+		return arg;
+	}
+
+	/*
+	 * 
+	 * Expand macro body with args. Called from PredicateNode Factory (if it is a macro)
+	 */
+	
+	public Node eval(LinkedList<? extends Node> args, Node predicate, String body, 
+			LinkedList<? extends Node> vars) {
+		Node result;
+		int i = 0;
+		
+		if (vars==null) {
+			// TermMacro case
+			return parse(body);
+		}
+		// prepare new scope
+		scope = scope.push();
+		for(Node var: vars) {
+			Node value;
+			if (i<args.size()) {
+				value =	args.get(i++);
+			} else {
+				value =	logicNodeFactory.trueNode();
+				scanner.error("Macro "+predicate+" Argument mismatch");
+			}
+			// make new token in the dictionary
+			Token<Node> local = scope.getLocalName(var.toString());
+			// assign new value
+			local.setMacro(value);
+		}
+		// parse it in new bindings
+		result = parse(body);
+		scope = scope.pop();
+		
+		return result;
+	}
+
+	/*
+	 * Make macro definition (store in the token in the dictionary)
+	 */
+	public void define(String macro, String body) {
+		define(macro, body, 0, null);
+	}
+
+	public void define(String macro, String body, int order) {
+		define(macro, body, order, null);
+	}
+	
+	/* macro with command */
+	public void define(String macro, String body, int order, Command<Node> command) {
+		Node m = parseMarcoHead(macro,order);
+		Node n = logicNodeFactory.macroNode(m, body, order, command, this);
+
+		Token<Node> t;
+		LogicSolver p = m.predicate();
+		if (p!=null && (t = dict.get(p.toString()))!=null) {
+			t.setMacro(n);
+		} else {
+			scanner.error("Internal error in define(\""+macro+"\",\""+n+"\")");
+		}
+	}
+
+	/*
+	 * Macro Head parser
+	 */
+	private Node parseMarcoHead(String exp, int order) {
+		Node n;
+		scanner = scanner.pushScanner(exp);
+		nextToken();
+		Token<Node> n1 = scanner.nextToken;
+		n = term();
+
+		if (nextToken.type==TokenID.Paren) {
+			nextToken();
+			n = logicNodeFactory.predicateNode(n,parameter());
+			if (n.arguments().size()==1) {
+				// all one argument predicates are prefix
+				n1.setPrefix();
+			}
+		} else if (nextToken.type==TokenID.NULL) {
+			// No parameter
+			n = logicNodeFactory.predicateNode(n,null);
+			n1.syntax = TokenID.ALIAS;
+		} else {
+			Token<Node> opToken = nextToken;
+			Node op;
+			nextToken();
+			Token<Node> n2 = nextToken;
+			LinkedList<Node> arg = new LinkedList<Node>();
+			scope = scope.push();
+			if (nextToken.type!=TokenID.NULL) {
+				// Assuming infix operator
+				opToken.setInfix();
+				opToken.order = order;
+				op = makeVariable(opToken);
+				oneParameter(arg,n1);
+				oneParameter(arg,n2);
+			} else {
+				op = makeVariable(n1);
+				n1.setPrefix();
+				n1.order = order;
+				oneParameter(arg,opToken);
+			}
+			scope = scope.pop();
+			n = logicNodeFactory.predicateNode(op,arg);
+		}
+
+		scanner = scanner.popScanner();
+		nextToken = scanner.nextToken;
+		return n;
+	}
+
+	/*
+	 * Function parameter 
+	 *    parameters are defined in local scope
+	 */
+	private LinkedList<Node> parameter() {
+		LinkedList<Node> arg = new LinkedList<Node>();
+
+		scope = scope.push();
+		while(nextToken.type!=TokenID.CloseParen) {
+			if (nextToken.type==TokenID.NULL) break;
+			oneParameter(arg,nextToken);
+			nextToken();
+			if (nextToken.type == TokenID.And)
+				nextToken();
+		}
+		if (nextToken.type==TokenID.CloseParen) nextToken();
+		else {
+			 scanner.error(") expected");
+		}
+		scope = scope.pop();
+		return arg;
+	}
+
+	public void oneParameter(LinkedList<Node> arg, Token<Node> nextToken) {
+		Token<Node> t;
+		Node v;
+		// If next token is a macro, parameter name is going to be replaced.
+		// We have to know the real symbol name.
+		
+		// more check is necessary
+		t = scope.getLocalName(nextToken.realName());
+		t.setVariable(true);
+		v = makeVariable(t);
+		arg.add(v);
+	}
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/MacroNodeParserInterface.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,11 @@
+package parser;
+
+import java.util.LinkedList;
+
+public interface MacroNodeParserInterface<Node> {
+	
+	public Node eval(LinkedList<? extends Node> args, Node predicate, String body, 
+			LinkedList<? extends Node> name) ;
+	
+	public void define(String head,String body);
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/NullExecutor.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,8 @@
+package parser;
+
+public class NullExecutor<Node> implements ExecutorInterface<Node> {
+
+	public void verify(Node n) {
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/Token.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,87 @@
+package parser;
+
+public class Token<Node> {
+	
+	
+	public String name;
+	public TokenID type;
+	public Node value;
+	public TokenID syntax;
+	public  int order;
+	public static int count = 0;
+	
+	public Token(String str) {
+		this(str,TokenID.UNKNOWN,0);
+	}
+	
+	public Token(String s, TokenID b) {
+		this(s, b, b.order);
+	}
+
+	public Token(String s, TokenID b, int order) {
+		this.name=s;
+		this.type = b;
+		this.order = order;
+		count++;
+	}
+
+
+	public String name() {
+		return name;
+	}
+
+	public boolean isVariable() {
+		return type==TokenID.VARIABLE;
+	}
+	
+	public void setVariable(boolean b) {
+		type = TokenID.VARIABLE;
+	}
+	
+	public boolean isVariableType() {
+		return type.isVariable();
+	}
+	
+	public Node value() {
+		return value;
+	}
+	
+	public void setValue(Node v) {
+		value = v;
+	}
+	
+	public void setMacro(Node m) {
+		type = TokenID.MACRO;
+		value = m;
+	}
+	
+	public String toString() {
+		return "Token("+name+","+type+")";
+	}
+
+	public String realName() {
+		if (type==TokenID.MACRO) {
+			return value.toString();
+		} else {
+			return name;
+		}
+	}
+
+	public void setInfix() {
+		syntax = TokenID.INFIX;		
+	}
+
+	public boolean isInfix() {
+		return syntax==TokenID.INFIX;
+	}
+
+
+	public void setPrefix() {
+		syntax = TokenID.PREFIX;
+	}
+	
+	public boolean isPrefix() {
+		return syntax==TokenID.PREFIX;
+	}
+
+}

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/parser/TokenID.java	Thu Jan 17 03:20:48 2008 +0900
@@ -0,0 +1,48 @@
+package parser;
+
+public enum TokenID {
+
+	Space		(0,0),
+	Or			(600,0),
+	And             (500,0),   // Comma
+	Not             (50,0),
+	Paren           (0,0),
+	CloseParen      (0,0),
+	CurParen		(0,0),
+	CloseCurParen	(0,0),
+	Exists          (50,2),
+	True            (0,1),
+	False           (0,0),
+	UNKNOWN			(1,0),
+	VARIABLE		(1,0),
+	PREDICATE		(1,0),
+	MACRO			(1,0),
+	Any				(0,0), 
+	Chop (900,4), Next(60,3), Empty(0,5), NUMBER(0,0),
+	STRING(0,0), INFIX(100,0), PREFIX(50,0), NULL(0,0), 
+	Length(50,0), Closure(50,0), Projection(50,6), 
+	Exec(50,0), Include(50,0), Period(0,0), Less(50,0), Define(50,0),
+	ALIAS(0,0), BParen(0,0),CloseBParen(0,0), Question(0,0), Colon(0,0);
+
+	public final int order;
+	public final int hash;
+
+    TokenID(int order,int hash) {
+		this.order = order;
+		this.hash = hash;
+	}
+    
+    public boolean isVariable() {
+    	switch(this) {
+    	case VARIABLE: case PREDICATE: case MACRO: case INFIX:
+    		return true;
+    	default:
+    		return false;
+    	}
+	}
+    
+    public boolean isInfix() {
+    	return this==INFIX;
+    }
+
+}