abc-master
 All Data Structures Namespaces Files Functions Variables Typedefs Enumerations Enumerator Friends Macros
extraUtilCube.c
Go to the documentation of this file.
1 /**CFile****************************************************************
2 
3  FileName [extraUtilCube.c]
4 
5  SystemName [ABC: Logic synthesis and verification system.]
6 
7  PackageName [extra]
8 
9  Synopsis [Permutation computation.]
10 
11  Author [Alan Mishchenko]
12 
13  Affiliation [UC Berkeley]
14 
15  Date [Ver. 1.0. Started - June 20, 2005.]
16 
17  Revision [$Id: extraUtilCube.c,v 1.0 2003/02/01 00:00:00 alanmi Exp $]
18 
19 ***********************************************************************/
20 
21 #include <stdio.h>
22 #include <stdlib.h>
23 #include <string.h>
24 #include <assert.h>
25 #include "misc/vec/vec.h"
26 #include "misc/vec/vecHsh.h"
27 
28 ABC_NAMESPACE_IMPL_START
29 
30 ////////////////////////////////////////////////////////////////////////
31 /// DECLARATIONS ///
32 ////////////////////////////////////////////////////////////////////////
33 
34 static inline void Abc_StatePush( Vec_Int_t * vData, char * pState, int k ) { int i; for ( i = 0; i < 6; i++ ) Vec_IntWriteEntry(vData, 6*k+i, ((int*)pState)[i]); }
35 static inline void Abc_StatePerm( char * pState, char * pPerm, char * pRes ) { int i; for ( i = 0; i < 24; i++ ) pRes[i] = pState[(int)pPerm[i]]; }
36 static inline void Abc_StatePrint( char * pState ) { int i; for ( i = 0; i < 24; i++ ) printf(" %2d", pState[i]); printf( "\n" ); }
37 
38 ////////////////////////////////////////////////////////////////////////
39 /// FUNCTION DEFINITIONS ///
40 ////////////////////////////////////////////////////////////////////////
41 
42 /**Function*************************************************************
43 
44  Synopsis []
45 
46  Description []
47 
48  SideEffects []
49 
50  SeeAlso []
51 
52 ***********************************************************************/
53 void Abc_EnumerateCubeStates2()
54 {
55  int pXYZ[3][9][2] = {
56  { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} },
57  { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} },
58  { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } };
59 
60  Vec_Int_t * vData = Vec_IntStart( 6 * (1 << 22) ); // 96 MB
61  Hsh_IntMan_t * vHash = Hsh_IntManStart( vData, 6, 1 << 22 ); // 32 MB
62  int i, k, v, RetValue, Beg, End, Counter = 0;
63  char pStart[24], pFirst[9][24];
64  abctime clk = Abc_Clock();
65  printf( "Enumerating states of 2x2x2 cube.\n" );
66  // init state
67  for ( v = 0; v < 24; v++ )
68  pStart[v] = v;
69  Abc_StatePush( vData, pStart, Counter );
70  RetValue = Hsh_IntManAdd( vHash, Counter );
71  assert( RetValue == Counter );
72  Counter++;
73  // first nine states
74  for ( i = 0; i < 3; i++ )
75  {
76  memcpy( pFirst[i], pStart, 24 );
77  for ( v = 0; v < 9; v++ )
78  ABC_SWAP( char, pFirst[i][pXYZ[i][v][0]-1], pFirst[i][pXYZ[i][v][1]-1] );
79  Abc_StatePush( vData, pFirst[i], Counter );
80  RetValue = Hsh_IntManAdd( vHash, Counter );
81  assert( RetValue == Counter );
82  Counter++;
83  //Abc_StatePrint( pFirst[i] );
84 
85  memcpy( pFirst[3+i], pFirst[i], 24 );
86  for ( v = 0; v < 9; v++ )
87  ABC_SWAP( char, pFirst[3+i][pXYZ[i][v][0]-1], pFirst[3+i][pXYZ[i][v][1]-1] );
88  Abc_StatePush( vData, pFirst[3+i], Counter );
89  RetValue = Hsh_IntManAdd( vHash, Counter );
90  assert( RetValue == Counter );
91  Counter++;
92  //Abc_StatePrint( pFirst[3+i] );
93 
94  memcpy( pFirst[6+i], pFirst[3+i], 24 );
95  for ( v = 0; v < 9; v++ )
96  ABC_SWAP( char, pFirst[6+i][pXYZ[i][v][0]-1], pFirst[6+i][pXYZ[i][v][1]-1] );
97  Abc_StatePush( vData, pFirst[6+i], Counter );
98  RetValue = Hsh_IntManAdd( vHash, Counter );
99  assert( RetValue == Counter );
100  Counter++;
101  //Abc_StatePrint( pFirst[6+i] );
102  }
103  printf( "Iter %2d -> %8d ", 0, 1 );
104  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
105  printf( "Iter %2d -> %8d ", 1, Counter );
106  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
107  Beg = 1; End = 10;
108  for ( i = 2; i <= 100; i++ )
109  {
110  if ( Beg == End )
111  break;
112  for ( k = Beg; k < End; k++ )
113  for ( v = 0; v < 9; v++ )
114  {
115  Abc_StatePerm( (char *)Vec_IntEntryP(vData, 6*k), pFirst[v], (char *)Vec_IntEntryP(vData, 6*Counter) );
116  RetValue = Hsh_IntManAdd( vHash, Counter );
117  if ( RetValue == Counter )
118  Counter++;
119  if ( Counter == (1<<22) )
120  {
121  printf( "Did not converge. " );
122  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
123  return;
124  }
125  }
126  Beg = End; End = Counter;
127  printf( "Iter %2d -> %8d ", i, Counter );
128  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
129  }
130  Hsh_IntManStop( vHash );
131  Vec_IntFree( vData );
132 }
133 
134 /*
135 Enumerating states of 2x2x2 cube.
136 Iter 0 -> 1 Time = 0.00 sec
137 Iter 1 -> 10 Time = 0.00 sec
138 Iter 2 -> 64 Time = 0.00 sec
139 Iter 3 -> 385 Time = 0.00 sec
140 Iter 4 -> 2232 Time = 0.00 sec
141 Iter 5 -> 12224 Time = 0.00 sec
142 Iter 6 -> 62360 Time = 0.02 sec
143 Iter 7 -> 289896 Time = 0.09 sec
144 Iter 8 -> 1159968 Time = 0.90 sec
145 Iter 9 -> 3047716 Time = 11.62 sec
146 Iter 10 -> 3671516 Time = 52.00 sec
147 Iter 11 -> 3674160 Time = 70.38 sec
148 Iter 12 -> 3674160 Time = 70.48 sec
149 */
150 
151 /**Function*************************************************************
152 
153  Synopsis []
154 
155  Description []
156 
157  SideEffects []
158 
159  SeeAlso []
160 
161 ***********************************************************************/
162 static inline int Abc_DataHasBit( word * p, word i ) { return (p[(i)>>6] & (1<<((i) & 63))) > 0; }
163 static inline void Abc_DataXorBit( word * p, word i ) { p[(i)>>6] ^= (1<<((i) & 63)); }
164 static inline int Abc_DataGetCube( word w, int i ) { return (w >> (5*i)) & 31; }
165 static inline word Abc_DataXorCube( word w, int i, int c ) { return w ^ (((word)c) << (5*i)); }
166 static inline word Abc_CubeGenerateSign( char * pState )
167 {
168  static int Var2Cor[24] = { 0, 0, 0, 1, 1, 1, 2, 2, 2, 3, 3, 3, 4, 4, 4, 5, 5, 5, -1, -1, -1, 6, 6, 6 };
169  static int Var2Per[24] = { 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, 0, 1, 2, -1, -1, -1, 0, 1, 2 };
170  word Res = 0;
171  Res = Abc_DataXorCube( Res, 0, (Var2Cor[(int)pState[ 0]] << 2) | Var2Per[(int)pState[ 0]] );
172  Res = Abc_DataXorCube( Res, 1, (Var2Cor[(int)pState[ 3]] << 2) | Var2Per[(int)pState[ 3]] );
173  Res = Abc_DataXorCube( Res, 2, (Var2Cor[(int)pState[ 6]] << 2) | Var2Per[(int)pState[ 6]] );
174  Res = Abc_DataXorCube( Res, 3, (Var2Cor[(int)pState[ 9]] << 2) | Var2Per[(int)pState[ 9]] );
175  Res = Abc_DataXorCube( Res, 4, (Var2Cor[(int)pState[12]] << 2) | Var2Per[(int)pState[12]] );
176  Res = Abc_DataXorCube( Res, 5, (Var2Cor[(int)pState[15]] << 2) | Var2Per[(int)pState[15]] );
177  Res = Abc_DataXorCube( Res, 6, (Var2Cor[(int)pState[21]] << 2) | Var2Per[(int)pState[21]] );
178  return Res;
179 }
180 
181 /**Function*************************************************************
182 
183  Synopsis []
184 
185  Description []
186 
187  SideEffects []
188 
189  SeeAlso []
190 
191 ***********************************************************************/
192 void Abc_EnumerateCubeStates()
193 {
194  int pXYZ[3][9][2] = {
195  { {3, 5}, {3,17}, {3,15}, {1, 6}, {1,16}, {1,14}, {2, 4}, {2,18}, {2,13} },
196  { {2,14}, {2,24}, {2,12}, {3,13}, {3,23}, {3,10}, {1,15}, {1,22}, {1,11} },
197  { {1,10}, {1, 7}, {1, 4}, {3,12}, {3, 9}, {3, 6}, {2,11}, {2, 8}, {2, 5} } };
198 
199  Vec_Int_t * vData = Vec_IntStart( 6 * (1 << 22) ); // 96 MB
200  word State, * pHash = ABC_CALLOC( word, 1 << 29 ); // 4 GB
201  int i, k, v, Beg, End, Counter = 0;
202  char * pPrev, * pState, pStart[24], pFirst[9][24];
203  abctime clk = Abc_Clock();
204  printf( "Enumerating states of 2x2x2 cube.\n" );
205  // init state
206  for ( v = 0; v < 24; v++ )
207  pStart[v] = v;
208  Abc_StatePush( vData, pStart, Counter );
209  Abc_DataXorBit( pHash, Abc_CubeGenerateSign(pStart) );
210  Counter++;
211  // first nine states
212  for ( i = 0; i < 3; i++ )
213  {
214  memcpy( pFirst[i], pStart, 24 );
215  for ( v = 0; v < 9; v++ )
216  ABC_SWAP( char, pFirst[i][pXYZ[i][v][0]-1], pFirst[i][pXYZ[i][v][1]-1] );
217  Abc_StatePush( vData, pFirst[i], Counter );
218  Abc_DataXorBit( pHash, Abc_CubeGenerateSign(pFirst[i]) );
219  Counter++;
220  //Abc_StatePrint( pFirst[i] );
221 
222  memcpy( pFirst[3+i], pFirst[i], 24 );
223  for ( v = 0; v < 9; v++ )
224  ABC_SWAP( char, pFirst[3+i][pXYZ[i][v][0]-1], pFirst[3+i][pXYZ[i][v][1]-1] );
225  Abc_StatePush( vData, pFirst[3+i], Counter );
226  Abc_DataXorBit( pHash, Abc_CubeGenerateSign(pFirst[3+i]) );
227  Counter++;
228  //Abc_StatePrint( pFirst[3+i] );
229 
230  memcpy( pFirst[6+i], pFirst[3+i], 24 );
231  for ( v = 0; v < 9; v++ )
232  ABC_SWAP( char, pFirst[6+i][pXYZ[i][v][0]-1], pFirst[6+i][pXYZ[i][v][1]-1] );
233  Abc_StatePush( vData, pFirst[6+i], Counter );
234  Abc_DataXorBit( pHash, Abc_CubeGenerateSign(pFirst[6+i]) );
235  Counter++;
236  //Abc_StatePrint( pFirst[6+i] );
237  }
238  printf( "Iter %2d -> %8d ", 0, 1 );
239  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
240  printf( "Iter %2d -> %8d ", 1, Counter );
241  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
242  Beg = 1; End = 10;
243  for ( i = 2; i <= 100; i++ )
244  {
245  if ( Beg == End )
246  break;
247  for ( k = Beg; k < End; k++ )
248  {
249  pPrev = (char *)Vec_IntEntryP(vData, 6*k);
250  for ( v = 0; v < 9; v++ )
251  {
252  pState = (char *)Vec_IntEntryP(vData, 6*Counter);
253  Abc_StatePerm( pPrev, pFirst[v], pState );
254  State = Abc_CubeGenerateSign( pState );
255  if ( !Abc_DataHasBit(pHash, State) )
256  Abc_DataXorBit(pHash, State), Counter++;
257  if ( Counter == (1<<22) )
258  {
259  printf( "Did not converge. " );
260  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
261  return;
262  }
263  }
264  }
265  Beg = End; End = Counter;
266  printf( "Iter %2d -> %8d ", i, Counter );
267  Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
268  }
269  Vec_IntFree( vData );
270  ABC_FREE( pHash );
271 }
272 
273 ////////////////////////////////////////////////////////////////////////
274 /// END OF FILE ///
275 ////////////////////////////////////////////////////////////////////////
276 
277 
278 ABC_NAMESPACE_IMPL_END
279 
Abc_EnumerateCubeStates
void Abc_EnumerateCubeStates()
Definition: extraUtilCube.c:192
p
static Llb_Mgr_t * p
Definition: llb3Image.c:950
Abc_DataXorBit
static void Abc_DataXorBit(word *p, word i)
Definition: extraUtilCube.c:163
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition: bblif.c:37
Abc_DataGetCube
static int Abc_DataGetCube(word w, int i)
Definition: extraUtilCube.c:164
memcpy
char * memcpy()
Abc_Clock
static abctime Abc_Clock()
Definition: abc_global.h:279
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition: abc_global.h:218
Abc_PrintTime
static void Abc_PrintTime(int level, const char *pStr, abctime time)
Definition: abc_global.h:367
Vec_IntWriteEntry
static void Vec_IntWriteEntry(Vec_Int_t *p, int i, int Entry)
Definition: bblif.c:285
Vec_IntStart
static Vec_Int_t * Vec_IntStart(int nSize)
Definition: bblif.c:172
Abc_DataHasBit
static int Abc_DataHasBit(word *p, word i)
Definition: extraUtilCube.c:162
Abc_DataXorCube
static word Abc_DataXorCube(word w, int i, int c)
Definition: extraUtilCube.c:165
Abc_StatePerm
static void Abc_StatePerm(char *pState, char *pPerm, char *pRes)
Definition: extraUtilCube.c:35
word
unsigned __int64 word
DECLARATIONS ///.
Definition: kitPerm.c:36
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition: abc_global.h:108
Counter
static int Counter
Definition: extraBddMisc.c:1877
Hsh_IntManStop
static void Hsh_IntManStop(Hsh_IntMan_t *p)
Definition: vecHsh.h:119
pPerm
static int pPerm[13719]
Definition: rwrTemp.c:32
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition: abc_global.h:107
Hsh_IntManAdd
static int Hsh_IntManAdd(Hsh_IntMan_t *p, int iData)
Definition: vecHsh.h:157
Abc_StatePrint
static void Abc_StatePrint(char *pState)
Definition: extraUtilCube.c:36
ABC_FREE
#define ABC_FREE(obj)
Definition: abc_global.h:232
ABC_CALLOC
#define ABC_CALLOC(type, num)
Definition: abc_global.h:230
Abc_EnumerateCubeStates2
void Abc_EnumerateCubeStates2()
FUNCTION DEFINITIONS ///.
Definition: extraUtilCube.c:53
Abc_StatePush
static ABC_NAMESPACE_IMPL_START void Abc_StatePush(Vec_Int_t *vData, char *pState, int k)
DECLARATIONS ///.
Definition: extraUtilCube.c:34
assert
#define assert(ex)
Definition: util_old.h:213
Vec_IntEntryP
static int * Vec_IntEntryP(Vec_Int_t *p, int i)
Definition: vecInt.h:417
Vec_IntFree
static void Vec_IntFree(Vec_Int_t *p)
Definition: bblif.c:235
Abc_CubeGenerateSign
static word Abc_CubeGenerateSign(char *pState)
Definition: extraUtilCube.c:166
Hsh_IntManStart
static Hsh_IntMan_t * Hsh_IntManStart(Vec_Int_t *vData, int nSize, int nEntries)
FUNCTION DEFINITIONS ///.
Definition: vecHsh.h:109
abctime
ABC_INT64_T abctime
Definition: abc_global.h:278
Hsh_IntMan_t_
Definition: vecHsh.h:57