    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    }