Mercurial > hg > Applications > JavaLite

comparison src/lite/BDDSolver.java @ 67:4ced2af1ff09 bdd-order

Find changesets by keywords (author, files, the commit message), revision number or hash, or revset expression.
BDD Order fix
author kono
date Sun, 13 Jan 2008 19:48:42 +0900
parents 80db395eeb30
children 854477cf9aa9
comparison
equal deleted inserted replaced
66:96b1c8c2f9b9 67:4ced2af1ff09
28 id = BDDID.Variable; 28 id = BDDID.Variable;
29 } 29 }
30 30
31 public BDDSolver(BDDID id, int hash) { 31 public BDDSolver(BDDID id, int hash) {
32 // primitives 32 // primitives
33
34 this.var = null;
35 this.var = null;
36 this.var = null;
37
38 this.id = id; 33 this.id = id;
39 this.hash = hash; 34 this.hash = hash;
40 } 35 }
41 36
42 public BDDSolver(ITLSolver v, ITLSolver high, ITLSolver low, BDDID id) { 37 public BDDSolver(ITLSolver v, ITLSolver high, ITLSolver low, BDDID id) {
55 if (var==null) { 50 if (var==null) {
56 if (id!=null) return id.toString(); 51 if (id!=null) return id.toString();
57 else return "null"; 52 else return "null";
58 } 53 }
59 if (id==BDDID.BDD) { 54 if (id==BDDID.BDD) {
60 if (high.id==BDDID.True&&low.id==BDDID.False) 55 if (high.id==BDDID.True) {
61 return var.toString(); 56 if (low.id==BDDID.False) return var.toString();
62 else if (high.id==BDDID.False&&low.id==BDDID.True) 57 return "("+var+";"+low+")";
58 } else if (high.id==BDDID.False&&low.id==BDDID.True)
63 return "~("+var+")"; 59 return "~("+var+")";
60 else if (low.id==BDDID.False) {
61 return "("+var+","+high+")";
62 }
64 return "("+var+"?"+high+":"+low+")"; 63 return "("+var+"?"+high+":"+low+")";
65 } 64 }
66 return var.toString(); 65 return var.toString();
67 } 66 }
68 67
134 public ITLSolver and(SBDDFactoryInterface sf,BDDSolver right) { 133 public ITLSolver and(SBDDFactoryInterface sf,BDDSolver right) {
135 switch(id) { 134 switch(id) {
136 case True: return right; 135 case True: return right;
137 case False: return sf.falseNode(); 136 case False: return sf.falseNode();
138 } 137 }
139 switch(order(var,right.var)) { 138
140 case 0: 139 int order = order(var,right.var);
140 if (order==0)
141 return sf.bddNode(var,high.and(sf,right.high),low.and(sf,right.low)); 141 return sf.bddNode(var,high.and(sf,right.high),low.and(sf,right.low));
142 case 1: 142 else if (order>0)
143 return right.and(sf,this); 143 return right.and(sf,this);
144 case -1: 144 else
145 default:
146 return sf.bddNode(var,high.and(sf,right),low.and(sf,right)); 145 return sf.bddNode(var,high.and(sf,right),low.and(sf,right));
147 }
148 } 146 }
149 147
150 public ITLSolver or(SBDDFactoryInterface sf,BDDSolver right) { 148 public ITLSolver or(SBDDFactoryInterface sf,BDDSolver right) {
151 switch(id) { 149 switch(id) {
152 case True: return sf.trueNode(); 150 case True: return sf.trueNode();
153 case False: return right; 151 case False: return right;
154 } 152 }
155 switch(order(var,right.var)) { 153 int order = order(var,right.var);
156 case 0: 154 if (order==0)
157 return sf.bddNode(var,high.or(sf,right.high),low.or(sf,right.low)); 155 return sf.bddNode(var,high.or(sf,right.high),low.or(sf,right.low));
158 case 1: 156 else if (order>0)
159 return right.or(sf,this); 157 return right.or(sf,this);
160 case -1: 158 else
161 default:
162 return sf.bddNode(var,high.or(sf,right),low.or(sf,right)); 159 return sf.bddNode(var,high.or(sf,right),low.or(sf,right));
163 }
164 } 160 }
165 161
166 162
167 public ITLSolver not(SBDDFactoryInterface sf) { 163 public ITLSolver not(SBDDFactoryInterface sf) {
168 switch(id) { 164 switch(id) {
171 } 167 }
172 return sf.bddNode(var,high.toSBDD(sf).not(sf),low.toSBDD(sf).not(sf)); 168 return sf.bddNode(var,high.toSBDD(sf).not(sf),low.toSBDD(sf).not(sf));
173 } 169 }
174 170
175 int order(ITLSolver a,ITLSolver b) { 171 int order(ITLSolver a,ITLSolver b) {
172 // should use hash? or more intelligent order
176 return a.toString().compareTo(b.toString()); 173 return a.toString().compareTo(b.toString());
177 } 174 }
178 175
179 public BDDSolver toSBDD(SBDDFactoryInterface sf) { 176 public BDDSolver toSBDD(SBDDFactoryInterface sf) {
180 return this; 177 return this;