Mercurial > hg > Applications > JavaLite

changeset 57:e416e9def04d

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
*** empty log message ***
author kono
date Tue, 08 Jan 2008 02:15:16 +0900
parents 57259d2b9484
children 4102a550bd52
files src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/lite/ITLNodeScanner.java src/sbdd/SBDDFactory.java src/sbdd/SBDDTest.java
diffstat 5 files changed, 36 insertions(+), 74 deletions(-) [+]
line wrap: on
line diff
--- a/src/lite/ITLCommander.java	Mon Jan 07 22:02:16 2008 +0900
+++ b/src/lite/ITLCommander.java	Tue Jan 08 02:15:16 2008 +0900
@@ -1,16 +1,22 @@
 package lite;
 
 import java.util.LinkedList;
-
+import sbdd.BDDSatisfier;
 import logicNode.parser.Command;
 
 public class ITLCommander<Node extends ITLSolver> implements Command<Node> {
 
 
 	private ITLNodeFactoryInterface<Node> lf;
+	
+	BDDSatisfier sat;
 
-	public ITLCommander(ITLNodeFactoryInterface<Node> lf) {
+	private ITLNodeParser<Node> parser;
+
+
+	public ITLCommander(ITLNodeFactoryInterface<Node> lf, ITLNodeParser<Node> parser) {
 		this.lf = lf;
+		this.parser = parser;
 	}
 
 	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
@@ -28,6 +34,19 @@
 				n = lf.orNode(lf.emptyNode(),lf.nextNode(n));
 			}
 			return (Node)n;
+		} else if (predicate.toString() == "ex") {
+			if (sat==null) sat = new BDDSatisfier();
+			// System.out.println(args.get(0)+":"+args.get(1));
+			System.out.println(args.get(0));
+			sat.verify(args.get(1));
+			return lf.trueNode();
+		} else if (predicate.toString() == "def") {
+			parser.define(args.get(0).toString(),args.get(1).toString());
+			return lf.trueNode();
+		} else if (predicate.toString() == "include") {
+			String file = args.getFirst().toString();
+			parser.parseFile(file);
+			return lf.trueNode();
 		}
 		System.out.println("Unknown Command Predicate:"+predicate+" Value:"+value+" Args:"+args);
 		return value;
--- a/src/lite/ITLNodeParser.java	Mon Jan 07 22:02:16 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Tue Jan 08 02:15:16 2008 +0900
@@ -25,7 +25,7 @@
 		Token<Node> emptyToken = dict.reserve("empty",TokenID.Empty);
 		emptyNode = emptyToken.value = logicNodeFactory.emptyNode();
 		
-		parseCommand = new ITLCommander<Node>(lf);
+		parseCommand = new ITLCommander<Node>(lf,this);
 		
 			define("not(P)","~P");                               // not
 			define("P->Q","(not(P);Q))");                         // imply
@@ -71,6 +71,7 @@
 			
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("def(Head,Body,Order)","true",50,parseCommand);
+			define("include(path)","true",50,parseCommand);
 
 	}
 
@@ -88,13 +89,15 @@
 		super.scanner = scanner;
 
 		dict.reserve("&",TokenID.Chop);
-		
-		
 		dict.reserve("@",TokenID.Next);
+		dict.reserve("proj",TokenID.Projection);
 		
 		dict.reserve("length",TokenID.Length);
+		dict.reserve("less",TokenID.Less);
 		dict.reserve("*",TokenID.Closure);
-		dict.reserve("proj",TokenID.Projection);
+		dict.reserve("ex",TokenID.Exec);
+		dict.reserve("include",TokenID.Include);
+		dict.reserve("def",TokenID.Define);
 	}
 
 	@Override
@@ -150,6 +153,10 @@
 		case Empty:
 		case Chop:
 		case Length:
+		case Less:
+		case Exec:
+		case Define:
+		case Include:
 		case Closure:
 		case Projection:
 			n = makeVariable(nextToken);
@@ -164,4 +171,5 @@
 	public ITLSolver emptyNode() {
 		return emptyNode;
 	}
+
 }
--- a/src/lite/ITLNodeScanner.java	Mon Jan 07 22:02:16 2008 +0900
+++ b/src/lite/ITLNodeScanner.java	Tue Jan 08 02:15:16 2008 +0900
@@ -1,82 +1,16 @@
 package lite;
 
-import java.util.regex.Pattern;
 
 import logicNode.LogicNode;
 import logicNode.parser.Dictionary;
 import logicNode.parser.LogicNodeScanner;
-import logicNode.parser.Token;
-import logicNode.parser.TokenID;
 
 public class ITLNodeScanner<Node extends LogicNode> extends LogicNodeScanner<Node> {
 
 
-	/*
-
-		System.out.println(p.parse("p & q"));
-		System.out.println(p.parse("p & @q"));
-		System.out.println(p.parse("<>(p)"));
-		System.out.println(p.parse("[](p)"));
-		System.out.println(p.parse("empty & q"));
-		System.out.println(p.parse("fin(p)=[](<>(p))"));
-		System.out.println(p.parse("length(3)"));
-		System.out.println(p.parse("[](more)"));
-		
-	 */
-	
-	
-	// 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 anyPat = Pattern.compile("(.)");
-
 	public ITLNodeScanner(Dictionary<Node> dict) {
 		super(dict);
 	}
 	
-	public Token<Node> nextToken() {
-		String s;
-		nextToken = null;
-		while(hasRemaining()) {
-			// scan.region(0,cb.length());
-			scan.reset();
-			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(namePat))!=null||(s=next(stringPat))!=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(next(anyPat)!=null) {  // skip until eol, in case of buffer full
-					if (!hasRemaining()) break;
-				}
-				continue;
-			} else if ((s=next(anyPat))!=null) {
-				continue;
-			} else {
-				lineno++;
-				cb.get(); // discard one ( new line )
-			}
-		}
-		return nextToken;
-	}
-
 
 }
--- a/src/sbdd/SBDDFactory.java	Mon Jan 07 22:02:16 2008 +0900
+++ b/src/sbdd/SBDDFactory.java	Tue Jan 08 02:15:16 2008 +0900
@@ -40,10 +40,10 @@
 	
 
 	public ITLSolver bddNode(ITLSolver lvar, ITLSolver solver, ITLSolver solver2) {
-		// too slow?
+		// too slow and we don't need it (?)
 		//solver = hash.put(solver);
 		//solver2 = hash.put(solver2);
-		//if (solver==solver2) return solver;
+		if (solver==solver2) return solver;
 		ITLSolver v =  new BDDSolver(lvar,solver,solver2,BDDID.BDD);
 		return hash.put(v); 
 	}
--- a/src/sbdd/SBDDTest.java	Mon Jan 07 22:02:16 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Tue Jan 08 02:15:16 2008 +0900
@@ -58,6 +58,7 @@
 		sat.showVerify("fin(p)=([](<>(p)))");
 		}
 		sat.showVerify("fin(p)");
+		// sat.p.parse("include('data/example').");
 		System.out.println(sat.state);
 	}