# HG changeset patch
# User kono
# Date 1200221322 -32400
# Node ID 4ced2af1ff09ec907e1411e9bae9d4ef291c50ba
# Parent  96b1c8c2f9b9630ce5f03ef82a1357aadfe036a3
BDD Order fix

diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 Changes
--- a/Changes	Fri Jan 11 14:31:02 2008 +0900
+++ b/Changes	Sun Jan 13 19:48:42 2008 +0900
@@ -1,7 +1,12 @@
+Sun Jan 13 19:20:10 JST 2008
+
+あぁ、ordered BDD になってないよ〜
+
 Fri Jan 11 14:23:21 JST 2008
 
 (empty & Hoge)が、なんかはびこって、項の大きさを大きくしているらしい。
-つうか、これがあると収束しないです。
+つうか、これがあると収束しないです。でも、それを取るぐらいではだめ
+ならしい。
 
 projection(C,I) のtermination は、I 項のverification が収束すること
 に依存しているので、I項に Projection が入っていると、projection の
@@ -16,6 +21,7 @@
 入れた時点でtrueにして良い。こうすれば、queue の中には unique
 な項しか入らないことになる。
 
+どうも、BDDのor で、うまく (empty & true ) を処理できてないっぽい。
 
 Thu Jan 10 13:28:26 JST 2008
 
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/BDDSolver.java
--- a/src/lite/BDDSolver.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/BDDSolver.java	Sun Jan 13 19:48:42 2008 +0900
@@ -30,11 +30,6 @@
 
 	public BDDSolver(BDDID id, int hash) {
 		// primitives
-		
-		this.var = null;
-		this.var = null;
-		this.var = null;
-		
 		this.id = id;
 		this.hash = hash;
 	}
@@ -57,10 +52,14 @@
 			else return "null";
 		}
 		if (id==BDDID.BDD) {
-			if (high.id==BDDID.True&&low.id==BDDID.False)
-				return var.toString();
-			else if (high.id==BDDID.False&&low.id==BDDID.True)
+			if (high.id==BDDID.True) {
+				if (low.id==BDDID.False) return var.toString();
+				return "("+var+";"+low+")";
+			} else if (high.id==BDDID.False&&low.id==BDDID.True)
 				return "~("+var+")";
+			else if (low.id==BDDID.False) {
+				return "("+var+","+high+")";
+			}
 			return "("+var+"?"+high+":"+low+")";
 		}
 		return var.toString();
@@ -136,15 +135,14 @@
 		case True: return right;
 		case False: return sf.falseNode();
 		}
-		switch(order(var,right.var)) {
-		case 0:
+
+		int order = order(var,right.var);
+		if (order==0) 
 			return sf.bddNode(var,high.and(sf,right.high),low.and(sf,right.low));
-		case 1:
+		else if (order>0) 
 			return right.and(sf,this);
-		case -1:
-		default:
+		else
 			return sf.bddNode(var,high.and(sf,right),low.and(sf,right));
-		}
 	}
 
 	public ITLSolver or(SBDDFactoryInterface sf,BDDSolver right) {
@@ -152,15 +150,13 @@
 		case True: return sf.trueNode();
 		case False: return right;
 		}
-		switch(order(var,right.var)) {
-		case 0:
+		int order = order(var,right.var);
+		if (order==0) 
 			return sf.bddNode(var,high.or(sf,right.high),low.or(sf,right.low));
-		case 1:
+		else if (order>0) 
 			return right.or(sf,this);
-		case -1:
-		default:
+		else
 			return sf.bddNode(var,high.or(sf,right),low.or(sf,right));
-		}
 	}
 
 
@@ -173,6 +169,7 @@
 	}
 
 	int order(ITLSolver a,ITLSolver b) {
+		// should use hash? or more intelligent order
 		return a.toString().compareTo(b.toString());
 	}
 	
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/ITLCommander.java
--- a/src/lite/ITLCommander.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/ITLCommander.java	Sun Jan 13 19:48:42 2008 +0900
@@ -17,37 +17,42 @@
 	}
 
 	public Node exec(Node predicate, Node value, LinkedList<Node> args) {
-		if (predicate.toString() == "length") {
-			Node n = lf.emptyNode();
-			int length = Integer.parseInt(args.get(0).toString());
-			for(int i =0;i<length;i++) {
-				n = lf.nextNode(n);
-			}
-			return (Node)n;
-		} else if (predicate.toString() == "less") {
+		
+		// All names used here have to be reserved. Otherwise, parser generated name becomes 
+		// different string at run time, as a result, name=="less" will fail even if name contains "less". 
+		// If we reseve it, paredicateNode.varaibleNode.name contains pregenerated String which is 
+		// equivalent to used here. Of course name.equal("less") works fine, but it is time consuming. 
+		// Although it is practically allowed but I cannot accept.
+		
+		// We can also define Command as internal interface class in ITLNodeParser. In this case
+		// reserve operation is not required, like "length" macro.
+
+		String name = predicate.toString();
+		
+		if (name=="less") {
 			Node n = lf.falseNode();
 			int length = Integer.parseInt(args.get(0).toString());
 			for(int i =0;i<length;i++) {
 				n = lf.orNode(lf.emptyNode(),lf.nextNode(n));
 			}
 			return (Node)n;
-		} else if (predicate.toString() == "ex") {
+		} else if (name == "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") {
+		} else if (name == "def") {
 			parser.define(args.get(0).toString(),args.get(1).toString());
 			return lf.trueNode();
-		} else if (predicate.toString() == "verbose") {
+		} else if (name == "verbose") {
 			if (Integer.parseInt(args.get(0).toString())==0) {
 				sat.verbose = false;
 			} else {
 				sat.verbose = true;
 			}
 			return lf.trueNode();
-		} else if (predicate.toString() == "include") {
+		} else if (name == "include") {
 			String file = args.getFirst().toString();
 			parser.parseFile(file);
 			return lf.trueNode();
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/ITLNodeParser.java
--- a/src/lite/ITLNodeParser.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/ITLNodeParser.java	Sun Jan 13 19:48:42 2008 +0900
@@ -2,6 +2,8 @@
 
 import java.util.LinkedList;
 
+import sbdd.SBDDFactory;
+
 import logicNode.parser.Command;
 import logicNode.parser.Dictionary;
 import logicNode.parser.LogicNodeScope;
@@ -15,6 +17,7 @@
 	public ITLNodeScanner<Node> scanner;
 	public ITLCommander<Node> parseCommand;
 	public Node emptyNode;
+	private Node periodNode;
 	
 	public ITLNodeParser(ITLNodeFactoryInterface<Node> lf) {
 
@@ -69,8 +72,8 @@
 // def(P<=Q,Q=>P)");
 // loop stuff and quantifiers
 			define("*(A) ","proj(A,true),fin(A)");  // weak closure
-			//define("+(A) ","A& *(empty;A)");   // strong closure
-			define("+(A) ","A & proj(A,true)");   // strong closure
+			define("+(A) ","A& *(empty;A)");   // strong closure
+			//define("+(A) ","A & proj(A,true)");   // strong closure
 			define("while(Cond,Do)"," *(((Cond->Do) , (~Cond->empty))))");
 			define("repeat(Do,until,Cond)"," (*((Do;empty)) ,@ halt(Cond)))");
 			define("all(P,Q)","not(exists(P,not(Q)))");
@@ -81,8 +84,6 @@
 			define("evenp(P)","(*(((P,skip) & skip;empty,P)) & (empty;skip)))"); 
 			define("phil(L,R)","+('[]'((~L, ~R)) & @ (L, ~R,@ (L,R, @ (R,'[]'( ~L)))) ))");
 
-			// share([a,b,c]) is too difficult
-			
 			define("ex(N,Exp)","true",50,parseCommand);
 			define("def(Head,Body,Order)","true",50,parseCommand);
 			define("include(path)","true",50,parseCommand);
@@ -91,6 +92,26 @@
 			define("verbose(I)", "true",50,parseCommand);                    
 			
 			define("^(r)","r"); // interval variable (we cannot handle now)
+			
+			periodNode = logicNodeFactory.variableNode(".", true);
+			// only one of the is true (should allow all false case?)
+			define("share(L)","[](share0(L))");
+			define("share0(L)","true",50, new Command<Node>() {
+				@SuppressWarnings({ "unchecked", "unchecked" })
+				public Node exec(Node predicate, Node value, LinkedList<Node> args) {
+					Node allFalse = (Node)SBDDFactory.trueSolver;
+					value= (Node)SBDDFactory.falseSolver;
+					LinkedList<ITLSolver> list = args.get(0).arguments();
+					if (list.isEmpty()) return value;
+					for(ITLSolver n:  list) {
+						Node n1 = (Node)n;
+						value = logicNodeFactory.bddNode(n1, allFalse, value);
+						allFalse = logicNodeFactory.bddNode(n1, 
+								(Node)SBDDFactory.falseSolver,allFalse);
+					}
+					return value;
+				}
+			});
 
 	}
 
@@ -111,13 +132,12 @@
 		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("ex",TokenID.Exec);
-		dict.reserve("include",TokenID.Include);
-		dict.reserve("def",TokenID.Define);
-		dict.reserve("verbose",TokenID.Less);
+		// parseCommand requires reserved word for string comparison
+		dict.reserve("less");
+		dict.reserve("ex");
+		dict.reserve("include");
+		dict.reserve("def");
+		dict.reserve("verbose");
 	}
 
 	@Override
@@ -131,6 +151,26 @@
 	}
 
 	@Override
+	public Node expr3() {
+		Node n = super.expr3();
+		while(nextToken.type==TokenID.Question) {
+			nextToken();
+			Node cond = n;
+			Node high = expr3();
+			if (nextToken.type!=TokenID.Colon) {
+				error(": expected");
+				return logicNodeFactory.trueNode();
+			}
+			nextToken();
+			Node low = expr3();
+			n = logicNodeFactory.orNode(
+					logicNodeFactory.andNode(cond, high),
+					logicNodeFactory.andNode(logicNodeFactory.notNode(cond), low));
+		}
+		return n;
+	}
+
+	@Override
 	public Node expr4() {
 		if (nextToken.type == TokenID.Next) {
 			nextToken();
@@ -139,6 +179,17 @@
 		return super.expr4();
 	}
 	
+	@Override
+	public Node term() {
+		if (nextToken.type==TokenID.BParen) {
+			Node predicate = periodNode;
+			nextToken();
+			LinkedList<Node> arg = arguments();
+			return logicNodeFactory.predicateNode(predicate, arg);
+		}
+		return super.term();
+	}
+	
 	public Node exprI2() {
 		Node n = exprM1();
 		while(nextToken.type == TokenID.Chop) {
@@ -153,14 +204,15 @@
 	protected LinkedList<Node> arguments() {
 		Node n;
 		LinkedList<Node> arg = new LinkedList<Node>();
-		while(nextToken.type!=TokenID.CloseParen) {
+		while(nextToken.type!=TokenID.CloseParen&&nextToken.type!=TokenID.CloseBParen) {
 			if (nextToken.type==TokenID.NULL) break;
 			n = exprI2();
 			arg.add(n);
 			if (nextToken.type == TokenID.And)
 				nextToken();
 		}
-		if (nextToken.type==TokenID.CloseParen) nextToken();
+		if (nextToken.type==TokenID.CloseParen||
+				nextToken.type==TokenID.CloseBParen) nextToken();
 		else {
 			scanner.error(") expected");
 		}
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/ITLSolver.java
--- a/src/lite/ITLSolver.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/ITLSolver.java	Sun Jan 13 19:48:42 2008 +0900
@@ -37,7 +37,7 @@
 	}
 	
 	@Override
-	public LinkedList<? extends ITLSolver> arguments() {
+	public LinkedList<ITLSolver> arguments() {
 		return null;
 	}
 	@Override
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/MacroSolver.java
--- a/src/lite/MacroSolver.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/MacroSolver.java	Sun Jan 13 19:48:42 2008 +0900
@@ -47,7 +47,7 @@
 	}
 	
 	@Override
-	public LinkedList<? extends ITLSolver> arguments() {
+	public LinkedList<ITLSolver> arguments() {
 		return predicate.arguments();
 	}
 
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/lite/PredicateSolver.java
--- a/src/lite/PredicateSolver.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/lite/PredicateSolver.java	Sun Jan 13 19:48:42 2008 +0900
@@ -19,7 +19,7 @@
 	}
 
 	@Override
-	public LinkedList<? extends ITLSolver> arguments() {
+	public LinkedList<ITLSolver> arguments() {
 		return arg;
 	}
 	@Override
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/sbdd/BDDSatisfier.java
--- a/src/sbdd/BDDSatisfier.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/sbdd/BDDSatisfier.java	Sun Jan 13 19:48:42 2008 +0900
@@ -80,8 +80,7 @@
 			if (value!=null) {
 				SBDDEntry e = state.getEntry(value);
 				if (e.expanded) {
-						// skip
-					System.out.print(".");
+					System.out.print((e.key==sat.true_)?"t":".");
 				} else 	{
 					queue.add(e); e.expanded = true;
 					System.out.print(e.id+" ");
diff -r 96b1c8c2f9b9 -r 4ced2af1ff09 src/sbdd/SBDDTest.java
--- a/src/sbdd/SBDDTest.java	Fri Jan 11 14:31:02 2008 +0900
+++ b/src/sbdd/SBDDTest.java	Sun Jan 13 19:48:42 2008 +0900
@@ -16,8 +16,8 @@
 
 		SBDDTest test = new SBDDTest();
 		
-		// test.bddTest();
-		// test.satTest();
+		//test.bddTest();
+		//test.satTest();
 		test.verifyTest();
 	}
 	
@@ -28,9 +28,21 @@
 	}
 	
 	public void bddTest() {
-
+		bddTest("a,b,c,a");
+		bddTest("a;b;c;b");
+		bddTest("(a,b);(~a,b)");
+		bddTest("a?b:c");
+		bddTest("(true&b)?((true&empty);((true&a)?(true&empty):c)):false");
+		bddTest("a?((true&empty);(b?(true&empty):c)):false");
+		bddTest("a?(x;(b?x:c)):false");
+		bddTest("A?(x;(B?x:C)):false");
+		bddTest("A,x");
+		bddTest("x,A");
+	}
+	
+	public void bddTest(String exp) {
 	    BDDSolver b;
-		ITLSolver s = p.parse("p&q");
+		ITLSolver s = p.parse(exp);
 		b = s.toSBDD(sf);
 		System.out.println(b);
 	}
@@ -67,8 +79,15 @@
 		sat.showVerify("even(p)");
 		sat.showVerify("Q, keep( @Q = ~Q)");
 		}
+		//sat.showVerify("share([a,b,c])");
+		//sat.showVerify("less(3)");
+		//sat.showVerify("*(a)");
+
+		//sat.showVerify("a?(x;(b?x:c)):false");
 		sat.showVerify("+(a & b)");
 		//System.out.println(sat.state);
+		sat.showVerify("ex(10,p)");
+		sat.p.parseCommand.sat.verbose=false;
 		sat.p.parse("include('data/example').");
 		// System.out.println(p.parseCommand.sat.state);
 	}