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 }