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    }