changeset 71:01356168f25f

*** empty log message ***
author kono
date Tue, 15 Jan 2008 15:25:06 +0900
parents 416e4d272e79
children 87b179e60443
files src/data/example src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/sbdd/BDDSatisfier.java
diffstat 4 files changed, 9 insertions(+), 35 deletions(-) [+]
line wrap: on
line diff
--- a/src/data/example	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/data/example	Tue Jan 15 15:25:06 2008 +0900
@@ -109,7 +109,7 @@
 ex(203,(^r,length(4))).		% distinguish different state?
 ex(204,('[a]'(^r))).		% non-deterministic?
 ex(205,('[a]'(^r = length(2)))). 		% imitate length?
-ex(206,('[a]'(^r = length(4)),(^r& ^r))).
+ex(206,('[a]'(^(r) = length(4)),(^(r)& ^(r)))).
 ex(207,('[a]'(^r = (length(4);empty)),* ^r)).
 ex(208,('[]'(^r = (
          a,@ ^r;
--- a/src/lite/ITLCommander.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/lite/ITLCommander.java	Tue Jan 15 15:25:06 2008 +0900
@@ -71,6 +71,7 @@
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
 		} else if (name == "verbose") {
+			// verbose(true) / verbose(off)
 			Node n= null;
 			checkSat();
 			try {
--- a/src/lite/ITLNodeParser.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Tue Jan 15 15:25:06 2008 +0900
@@ -86,7 +86,7 @@
 
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("do(N)","true",50,parseCommand);
-			define("def(Head,Body,Order)","true",50,parseCommand);
+			define("def(Head,Body)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
 			
 			define("ex0(N,Exp)","skipped");
@@ -158,6 +158,10 @@
 
 	@Override
 	public Node expr3() {
+		if (nextToken.type == TokenID.Next) {
+			nextToken();
+			return logicNodeFactory.nextNode(expr3());
+		}
 		Node n = super.expr3();
 		while(nextToken.type==TokenID.Question) {
 			nextToken();
@@ -176,14 +180,6 @@
 		return n;
 	}
 
-	@Override
-	public Node expr4() {
-		if (nextToken.type == TokenID.Next) {
-			nextToken();
-			return logicNodeFactory.nextNode(expr4());
-		}
-		return super.expr4();
-	}
 	
 	@Override
 	public Node term() {
@@ -224,30 +220,7 @@
 		}
 		return arg;
 	}
-	/*
-	@Override
-	protected Node term() {
-		Node n;
-		switch (nextToken.type) {
-		case Next:
-		case Empty:
-		case Chop:
-		case Length:
-		case Less:
-		case Exec:
-		case Define:
-		case Include:
-		case Closure:
-		case Projection:
-			n = makeVariable(nextToken);
-			break;
-		default:
-			return super.term();
-		}
-		nextToken();
-		return n;
-	}
-     */
+	
 	public ITLSolver emptyNode() {
 		return emptyNode;
 	}
--- a/src/sbdd/BDDSatisfier.java	Mon Jan 14 16:48:48 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Tue Jan 15 15:25:06 2008 +0900
@@ -147,7 +147,7 @@
 			develop(e.key, allNext);
 			if (!verbose) System.out.println();
 		}
-		if (!verbose) {
+		if (verbose) {
 			if (!falsfiable) {
 				System.out.println("valid");
 			}