Mercurial > hg > Applications > JavaLite
changeset 67:4ced2af1ff09 bdd-order
BDD Order fix
author | kono |
---|---|
date | Sun, 13 Jan 2008 19:48:42 +0900 |
parents | 96b1c8c2f9b9 |
children | e769488a5d78 |
files | Changes src/lite/BDDSolver.java src/lite/ITLCommander.java src/lite/ITLNodeParser.java src/lite/ITLSolver.java src/lite/MacroSolver.java src/lite/PredicateSolver.java src/sbdd/BDDSatisfier.java src/sbdd/SBDDTest.java |
diffstat | 9 files changed, 133 insertions(+), 55 deletions(-) [+] |
line wrap: on
line diff
--- 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
--- 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()); }
--- 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();
--- 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"); }
--- 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
--- 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(); }
--- 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
--- 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+" ");
--- 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); }