001 /* Copyright 2000, 2001, Compaq Computer Corporation */
002
003 package escjava.pa.generic;
004
005 import javafe.util.*;
006
007 /* Enumerates all clauses of size k, where there are n variables.
008 */
009
010 class EnumKofN extends Disjunction {
011
012 int n,k;
013
014 public EnumKofN(int k, int n) {
015 super(-1L, 0);
016 Assert.notFalse( k <= n );
017 this.k = k;
018 this.n = n;
019 }
020
021 boolean getNext() {
022
023 if( stars == -1 ) {
024 // intitialize
025 stars = 0;
026 for(int i=k; i<n; i++) {
027 stars |= 1<<i;
028 }
029 return true;
030 }
031
032 // get next
033
034 int nb=0, ns=0, i=0;
035
036 for(i=0; i<n; i++) {
037 Assert.notFalse( nb + ns == i );
038
039 long b = 1<<i;
040 if( (stars & b) != 0 ) {
041 // was a star
042 ns++;
043 if (nb>0) {
044 // remove star
045 stars &= ~b;
046 // clear bit
047 bits &= ~b;
048 nb--;
049 break; // 0.enum(nb-1,s)
050 } else {
051 continue; // ret, done 0, nb=0
052 }
053 } else {
054 // was a bit
055 if( (bits & b) == 0 ) {
056 // was a 0, set to 1
057 bits |= b;
058 break; // 1.enum(nb-1,s)
059 } else {
060 nb++;
061 // remove bit
062 bits &= ~b;
063 // put star in
064 stars |= b;
065 continue; // ret, done bits
066 }
067 }
068 }
069 if( i==n ) return false;
070
071 // fill from i-1 to 0
072 while( ns > 0 ) {
073 ns --;
074 i--;
075 long b = 1<<i;
076 Assert.notFalse( (stars & b) != 0 );
077 }
078 Assert.notFalse( i == nb );
079
080 while( i > 0 ) {
081 i--;
082 long b = 1<<i;
083 stars &= ~b;
084 Assert.notFalse( (stars & b) == 0 );
085 Assert.notFalse( (bits & b) == 0 );
086 }
087
088 return true;
089 }
090
091 public static void main(String argv[]) {
092
093 EnumKofN e = new EnumKofN(2,3);
094
095 while( e.getNext() ) {
096 System.out.println("Bits = "+Long.toString(e.bits,2)+
097 " stars = "+Long.toString(e.stars,2));
098 }
099 }
100
101 }
102
103