001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.pa.generic;
004
005 import java.util.Random;
006 import java.util.Hashtable;
007 import java.util.Enumeration;
008 import java.util.Vector;
009
010 import javafe.util.Set;
011 import javafe.util.Location;
012 import javafe.util.Assert;
013 import javafe.util.StackVector;
014
015 import mocha.wrappers.jbdd.*;
016
017 /* Abstractor that is like EnumMaxClausesFindMinAbstractor,
018 but only enumerates enough maximal clauses to ensure that
019 all invariants of length k are found.
020 */
021
022
023
024 public class EnumNFindK implements Abstractor {
025
026 private /*@ non_null @*/ jbddManager bddManager;
027
028 private int k;
029 private /*@ non_null @*/ jbdd R;
030 private /*@ non_null @*/ Vector clauses = new Vector();
031 private /*@ non_null @*/ Vector disj = new Vector();
032 // invariant: R = conjunction of clauses
033 // clauses are bdds, disj are Disjunctions, otherwise identical
034
035 //private Prover prover;
036
037 private boolean noisy = Boolean.getBoolean("PANOISY");
038 private static boolean invLeqK = Boolean.getBoolean("INVLEQK");
039
040 private final long seed = 0xcafcaf;
041 private /*@ non_null @*/ Random random = new Random(seed);
042
043 static {
044 System.out.println("invLeqK="+invLeqK);
045 }
046
047 public EnumNFindK(/*@ non_null @*/ jbddManager bddManager, int k) {
048 if( k > bddManager.jbdd_num_vars() ) {
049 k = bddManager.jbdd_num_vars();
050 }
051 this.k = k;
052 // bddManager.jbdd_num_vars
053 this.bddManager = bddManager;
054 R = bddManager.jbdd_zero();
055 clauses.addElement( R );
056 disj.addElement(new Disjunction()); // Yields Disjunction for false
057 }
058
059 public /*@ non_null @*/ jbdd get() {
060 return R;
061 }
062
063 public /*@ non_null @*/ Vector getClauses() {
064 return clauses;
065 }
066
067 private void add(/*@ non_null @*/ Disjunction d,
068 /*@ non_null @*/ DisjunctionProver disjProver)
069 {
070 jbdd b = disjProver.disjToBdd(d);
071 R = jbdd.jbdd_and( R, b, true, true );
072 clauses.addElement(b);
073 disj.addElement(d);
074 }
075
076 public boolean union(/*@ non_null @*/ Prover prover) {
077
078 int nclauses=0, kclauses=0;
079
080 Vector oldDisj = disj;
081 jbdd oldR = R;
082
083 R = bddManager.jbdd_one();
084 clauses = new Vector();
085 disj = new Vector();
086
087 //this.prover = prover;
088 DisjunctionProver disjProver = new DisjunctionProver( prover, bddManager );
089
090 for(int i=0; i<oldDisj.size(); i++) {
091 Disjunction d = (Disjunction)oldDisj.elementAt(i);
092 if( disjProver.check(d) ) {
093 if( noisy )
094 say("Invariant still valid: "+disjProver.printClause(d));
095 add(d, disjProver);
096 }
097 }
098 if( disj.size() == oldDisj.size() ) {
099 // all of the old invariants are still invariants
100 // so reachable space is not any bigger,
101 // and certainly cannot be any smaller
102 return true;
103 }
104
105 for(EnumKofN enumKofN = new EnumKofN(k, bddManager.jbdd_num_vars());
106 enumKofN.getNext(); ) {
107
108 kclauses++;
109
110 if( disjProver.quickCheck(enumKofN) == DisjunctionProver.UNKNOWN ) {
111
112 if( noisy ) say("kbdd = "+disjProver.printClause( enumKofN ));
113
114 // Try to find extension to n-string that is unknown
115
116 Disjunction nd = new Disjunction(enumKofN);
117 if( !extendToMaxDisjUnknown(nd,0,disjProver) ) {
118 Assert.fail("Problem extending "+disjProver.printClause( enumKofN )
119 +" to maximal disjunction of unknown validity");
120 }
121
122 Assert.notFalse(disjProver.quickCheck(nd) == DisjunctionProver.UNKNOWN );
123 nclauses++;
124
125 if( noisy ) {
126 say("nbdd = "+disjProver.printClause( nd) +" quickcheck "+ disjProver.quickCheck(nd));
127 }
128
129 Assert.notFalse( disjProver.quickCheck(nd) != DisjunctionProver.INVALID );
130
131 if( disjProver.check(nd)) {
132 // nd valid, find subset that is valid
133 long usedBits = ~(-1L << bddManager.jbdd_num_vars());
134 findMinDisjValid( nd, disjProver, enumKofN.stars & usedBits);
135 findMinDisjValid( nd, disjProver,~enumKofN.stars & usedBits);
136
137 if( !invLeqK || size(nd) <= k ) {
138 if( !disj.contains(nd) ) {
139 if( noisy )
140 say("Invariant: "+disjProver.printClause(nd));
141 add(nd, disjProver);
142 } else {
143 if( noisy )
144 say("Repeated invariant: "+disjProver.printClause(nd));
145 }
146 } else {
147 if( noisy )
148 say("invariant too long: "
149 +disjProver.printClause(nd));
150 }
151 }
152
153 Assert.notFalse( disjProver.quickCheck(enumKofN) != Prover.UNKNOWN );
154 }
155 }
156
157 System.out.println("kClauses="+kclauses
158 +" nClauses="+nclauses);
159 System.out.println("Prover: "+prover.report());
160
161 return oldR.jbdd_equal( R );
162 }
163
164 // requires d valid, mutates d, leaves it valid
165 private void findMinDisjValid( /*@ non_null @*/ Disjunction d,
166 /*@ non_null @*/ DisjunctionProver disjProver,
167 long dropWhich)
168 {
169 if( noisy )
170 say( "findMinClauseValid("+disjProver.printClause(d)
171 +", "+Long.toBinaryString(dropWhich)+")");
172
173 for(int i=0; i<64; i++) {
174 long b = 1L<<i;
175
176 if( (dropWhich & b) == 0 ) continue;
177 if( (d.stars & b) != 0 ) continue;
178
179 long oldStars = d.stars;
180 long oldBits = d.bits;
181
182 d.stars |= b;
183 d.bits &= ~b;
184
185 //if( noisy ) say( "findMinClauseValid checking "+disjProver.printClause(d));
186 if( disjProver.check(d) ) continue;
187
188 // could not drop, but it back
189 d.stars = oldStars;
190 d.bits = oldBits;
191 }
192
193 if( noisy )
194 say( "findMinClauseValid returning "+disjProver.printClause(d));
195
196 }
197
198 private boolean extendToMaxDisjUnknown(/*@ non_null @*/ Disjunction nd, int i,
199 /*@ non_null @*/ DisjunctionProver disjProver) {
200 //say("extendToMaxDisjUnknown("+disjProver.printClause( nd)+","+i+")");
201
202 Assert.notFalse(disjProver.quickCheck(nd) == DisjunctionProver.UNKNOWN );
203
204 long bit = (1L<<i);
205 if( i == bddManager.jbdd_num_vars() ) {
206 return true;
207 } else if( (nd.stars & bit) == 0 ) {
208 // not a star at this bit, go to next
209 return extendToMaxDisjUnknown(nd, i+1, disjProver);
210 } else {
211 nd.stars &= ~bit;
212 long r = random.nextLong();
213 for(int sign=0; sign<2; sign++) {
214 nd.bits = (nd.bits & ~bit) | (r & bit);
215 if( disjProver.quickCheck(nd) == DisjunctionProver.UNKNOWN &&
216 extendToMaxDisjUnknown(nd, i+1, disjProver)) {
217 // can extend
218 return true;
219 }
220 // failed to extend, try other choice for bit
221 r = ~r;
222 }
223 // both choices did not work, but star back in and backtrack
224
225 nd.stars |= bit;
226 return false; // could not extend
227 }
228 }
229
230 private void say(String s) {
231 if( noisy ) {
232 System.out.println(s);
233 }
234 }
235
236 /* UNUSED
237 // return size of a disjunction
238 static private int size(jbdd b) {
239 int s=0;
240 while( !b.jbdd_is_tautology(true) && !b.jbdd_is_tautology(false)) {
241 jbdd t = b.jbdd_then();
242 if( t.jbdd_is_tautology(true)) {
243 //t.jbdd_free();
244 t = b.jbdd_else();
245 }
246 //if( s != 0 ) b.jbdd_free();
247 s++;
248 b = t;
249 }
250 return s;
251 }
252 */
253
254 // return size of a disjunction
255 private int size(/*@ non_null @*/ Disjunction d) {
256 int s=0;
257 for(int i=0; i<bddManager.jbdd_num_vars(); i++) {
258 if( (d.stars & (1L<<i)) == 0) s++;
259 }
260 return s;
261 }
262
263 /*@ non_null @*/ jbdd longsToBdd(long stars, long bits) {
264 // Put choice into a bdd,
265 jbdd t = bddManager.jbdd_zero();
266 for( int i=bddManager.jbdd_num_vars()-1; i>=0; i-- ) {
267 long b = 1L<<i;
268 if( (stars & b) == 0 ) {
269 // no star
270 jbdd varBdd = bddManager.jbdd_get_variable( i );
271 jbdd t2 = jbdd.jbdd_or( t, varBdd, true, (bits & b) != 0 );
272 // t.jbdd_free();
273 t = t2;
274 }
275 }
276 return t;
277 }
278 }