|
42
|
1 package lite;
|
|
|
2
|
|
45
|
3 import sbdd.BDDID;
|
|
44
|
4 import sbdd.SBDDFactoryInterface;
|
|
42
|
5 import verifier.Backtrack;
|
|
|
6
|
|
|
7 public class BDDSolver extends ITLSolver {
|
|
|
8
|
|
|
9 /*
|
|
|
10 * var?high:low
|
|
|
11 */
|
|
|
12 public ITLSolver var;
|
|
|
13 public BDDSolver high; // true
|
|
|
14 public BDDSolver low; // flase
|
|
45
|
15 public BDDID id;
|
|
42
|
16
|
|
|
17 public BDDSolver(ITLSolver var, BDDSolver high, BDDSolver low) {
|
|
|
18 this.var = var;
|
|
|
19 this.high = high;
|
|
|
20 this.low = low;
|
|
45
|
21 id = BDDID.Variable;
|
|
42
|
22 }
|
|
|
23
|
|
|
24 public BDDSolver(ITLSolver var, ITLSolver high, ITLSolver low) {
|
|
|
25 this.var = var;
|
|
|
26 this.high = (BDDSolver) high;
|
|
|
27 this.low = (BDDSolver) low;
|
|
45
|
28 id = BDDID.Variable;
|
|
|
29 }
|
|
|
30
|
|
|
31 public BDDSolver(BDDID id, int hash) {
|
|
|
32 // primitives
|
|
|
33
|
|
|
34 this.var = null;
|
|
|
35 this.var = null;
|
|
|
36 this.var = null;
|
|
|
37
|
|
|
38 this.id = id;
|
|
|
39 this.hash = hash;
|
|
|
40 }
|
|
|
41
|
|
|
42 public BDDSolver(ITLSolver v, ITLSolver high, ITLSolver low, BDDID id) {
|
|
|
43 // for modal node with id
|
|
|
44 this(v,high,low);
|
|
|
45 this.id = id;
|
|
42
|
46 }
|
|
|
47
|
|
46
|
48 public BDDSolver(ITLSolver v, BDDID id, int hash) {
|
|
|
49 this(v,null,null);
|
|
|
50 this.id = id;
|
|
|
51 this.hash = hash;
|
|
|
52 }
|
|
|
53
|
|
42
|
54 public String toString() {
|
|
46
|
55 if (var==null) {
|
|
|
56 if (id!=null) return id.toString();
|
|
|
57 else return "null";
|
|
|
58 }
|
|
48
|
59 if (id==BDDID.BDD) {
|
|
63
|
60 if (high.id==BDDID.True&&low.id==BDDID.False)
|
|
|
61 return var.toString();
|
|
|
62 else if (high.id==BDDID.False&&low.id==BDDID.True)
|
|
|
63 return "~("+var+")";
|
|
48
|
64 return "("+var+"?"+high+":"+low+")";
|
|
|
65 }
|
|
42
|
66 return var.toString();
|
|
|
67 }
|
|
|
68
|
|
|
69 public boolean value() {
|
|
|
70 return var.value()? high.value() : low.value();
|
|
|
71 }
|
|
|
72
|
|
|
73
|
|
|
74 public ITLSolver sat(ITLSatisfier sat, Continuation next) throws Backtrack {
|
|
53
|
75 if (id!=BDDID.Variable&&id!=BDDID.BDD) {
|
|
43
|
76 return var.sat(sat,next);
|
|
|
77 }
|
|
42
|
78 return var.sat(sat, new Continuation(sat,next,this));
|
|
|
79 }
|
|
|
80
|
|
|
81 @Override
|
|
|
82 public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
|
|
|
83 if (value==null) {
|
|
|
84 return low.sat(sat, next);
|
|
45
|
85 } else if (value==sat.true_) {
|
|
42
|
86 return high.sat(sat, next);
|
|
|
87 } else {
|
|
|
88 return high.sat(sat, new Continuation(sat,next,
|
|
|
89 new BDDSolver2(value)));
|
|
|
90 }
|
|
|
91 }
|
|
|
92
|
|
|
93 class BDDSolver2 implements Next {
|
|
|
94 ITLSolver cond;
|
|
|
95 public BDDSolver2(ITLSolver value) {
|
|
|
96 cond = value;
|
|
|
97 }
|
|
|
98
|
|
|
99 public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver value) throws Backtrack {
|
|
|
100 return low.sat(sat, new Continuation(sat,next,
|
|
|
101 new BDDSolver3(cond,value)));
|
|
|
102 }
|
|
|
103 }
|
|
|
104
|
|
|
105 class BDDSolver3 implements Next {
|
|
|
106 ITLSolver cond, high;
|
|
|
107 public BDDSolver3(ITLSolver cond, ITLSolver value) {
|
|
|
108 this.cond = cond;
|
|
|
109 high = value;
|
|
|
110 }
|
|
|
111
|
|
|
112 public ITLSolver next(ITLSatisfier sat,Continuation next, ITLSolver low) throws Backtrack {
|
|
45
|
113 if (low==sat.true_ && high==sat.true_)
|
|
42
|
114 return next.sat(low);
|
|
|
115 if (low==null && high==null)
|
|
|
116 return next.sat(null);
|
|
|
117 if (low == high) {
|
|
|
118 return next.sat(low);
|
|
|
119 } else {
|
|
|
120 // lf.bddNode(cond,high,low) won't work
|
|
45
|
121 if (low==null) low = sat.lf.falseNode();
|
|
|
122 if (high==null) high = sat.lf.falseNode();
|
|
|
123 // if (cond==null) cond = sat.lf.falseNode();
|
|
64
|
124 ITLSolver value = sat.lf.orNode(
|
|
42
|
125 sat.lf.andNode(cond, high),
|
|
64
|
126 sat.lf.andNode(sat.lf.notNode(cond), low));
|
|
|
127 if (value==sat.false_) value = null;
|
|
|
128 return next.sat(value);
|
|
42
|
129 }
|
|
|
130 }
|
|
|
131 }
|
|
|
132
|
|
|
133
|
|
45
|
134 public ITLSolver and(SBDDFactoryInterface sf,BDDSolver right) {
|
|
|
135 switch(id) {
|
|
|
136 case True: return right;
|
|
|
137 case False: return sf.falseNode();
|
|
|
138 }
|
|
48
|
139 switch(order(var,right.var)) {
|
|
42
|
140 case 0:
|
|
48
|
141 return sf.bddNode(var,high.and(sf,right.high),low.and(sf,right.low));
|
|
42
|
142 case 1:
|
|
|
143 return right.and(sf,this);
|
|
|
144 case -1:
|
|
|
145 default:
|
|
48
|
146 return sf.bddNode(var,high.and(sf,right),low.and(sf,right));
|
|
42
|
147 }
|
|
|
148 }
|
|
|
149
|
|
45
|
150 public ITLSolver or(SBDDFactoryInterface sf,BDDSolver right) {
|
|
|
151 switch(id) {
|
|
|
152 case True: return sf.trueNode();
|
|
|
153 case False: return right;
|
|
|
154 }
|
|
48
|
155 switch(order(var,right.var)) {
|
|
42
|
156 case 0:
|
|
48
|
157 return sf.bddNode(var,high.or(sf,right.high),low.or(sf,right.low));
|
|
42
|
158 case 1:
|
|
|
159 return right.or(sf,this);
|
|
|
160 case -1:
|
|
|
161 default:
|
|
48
|
162 return sf.bddNode(var,high.or(sf,right),low.or(sf,right));
|
|
42
|
163 }
|
|
|
164 }
|
|
|
165
|
|
|
166
|
|
45
|
167 public ITLSolver not(SBDDFactoryInterface sf) {
|
|
|
168 switch(id) {
|
|
|
169 case True: return sf.falseNode();
|
|
|
170 case False: return sf.trueNode();
|
|
|
171 }
|
|
60
|
172 return sf.bddNode(var,high.toSBDD(sf).not(sf),low.toSBDD(sf).not(sf));
|
|
42
|
173 }
|
|
|
174
|
|
48
|
175 int order(ITLSolver a,ITLSolver b) {
|
|
42
|
176 return a.toString().compareTo(b.toString());
|
|
|
177 }
|
|
|
178
|
|
44
|
179 public BDDSolver toSBDD(SBDDFactoryInterface sf) {
|
|
42
|
180 return this;
|
|
|
181 }
|
|
|
182
|
|
46
|
183
|
|
|
184 static final int PAIR(int a, int b) {
|
|
|
185 return ((a + b) * (a + b + 1) / 2 + a);
|
|
|
186 }
|
|
|
187 static final int TRIPLE(int a, int b, int c) {
|
|
|
188 return (PAIR(c, PAIR(a, b)));
|
|
|
189 }
|
|
|
190
|
|
|
191 static final int NODEHASH(int lvl, int l, int h) {
|
|
|
192 return Math.abs(TRIPLE(lvl, l, h));
|
|
|
193 }
|
|
|
194
|
|
42
|
195 public int hashCode() {
|
|
46
|
196 if (hash!=-1) return hash;
|
|
48
|
197 return hash = NODEHASH(var.hashCode(),low.hashCode(),high.hashCode());
|
|
42
|
198 }
|
|
|
199
|
|
47
|
200 public boolean equals(Object o) {
|
|
48
|
201 if (o==this) return true;
|
|
47
|
202 if (o.hashCode()!=hashCode()) return false;
|
|
|
203 if (o.getClass()==this.getClass()) {
|
|
|
204 BDDSolver v = (BDDSolver)o;
|
|
|
205 switch(id) {
|
|
|
206 case True: case False: case Empty:
|
|
|
207 return id == v.id;
|
|
|
208 default:
|
|
48
|
209 return var.equals(v.var)&&low.equals(v.low)&&high.equals(v.high);
|
|
47
|
210 }
|
|
|
211 }
|
|
|
212 return false;
|
|
|
213 }
|
|
|
214
|
|
42
|
215 public BDDSolver high() {
|
|
|
216 return high;
|
|
|
217 }
|
|
|
218
|
|
|
219 public BDDSolver low() {
|
|
|
220 return low;
|
|
|
221 }
|
|
|
222
|
|
|
223 public ITLSolver var() {
|
|
|
224 return var;
|
|
|
225 }
|
|
|
226 }
|
