ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
ifDec08.c
Go to the documentation of this file.
1
20
21#include "if.h"
22#include "misc/extra/extra.h"
23#include "bool/kit/kit.h"
24
25#ifdef _MSC_VER
26# include <intrin.h>
27# define __builtin_popcount __popcnt
28#endif
29
30ABC_NAMESPACE_IMPL_START
31
32
36
37// variable swapping code
38static word PMasks[5][3] = {
39 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
40 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
41 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
42 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
43 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
44};
45// elementary truth tables
46static word Truth6[6] = {
47 ABC_CONST(0xAAAAAAAAAAAAAAAA),
48 ABC_CONST(0xCCCCCCCCCCCCCCCC),
49 ABC_CONST(0xF0F0F0F0F0F0F0F0),
50 ABC_CONST(0xFF00FF00FF00FF00),
51 ABC_CONST(0xFFFF0000FFFF0000),
52 ABC_CONST(0xFFFFFFFF00000000)
53};
54static word Truth10[10][16] = {
55 {ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA),ABC_CONST(0xAAAAAAAAAAAAAAAA)},
56 {ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC),ABC_CONST(0xCCCCCCCCCCCCCCCC)},
57 {ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0),ABC_CONST(0xF0F0F0F0F0F0F0F0)},
58 {ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00),ABC_CONST(0xFF00FF00FF00FF00)},
59 {ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000),ABC_CONST(0xFFFF0000FFFF0000)},
60 {ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000),ABC_CONST(0xFFFFFFFF00000000)},
61 {ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
62 {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
63 {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)},
64 {ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0x0000000000000000),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF),ABC_CONST(0xFFFFFFFFFFFFFFFF)}
65};
66
67extern void Kit_DsdPrintFromTruth( unsigned * pTruth, int nVars );
68extern void Extra_PrintBinary( FILE * pFile, unsigned Sign[], int nBits );
69
73
74static inline int If_Dec08WordNum( int nVars )
75{
76 return nVars <= 6 ? 1 : 1 << (nVars-6);
77}
78static void If_Dec08PrintConfigOne( unsigned z )
79{
80 unsigned t;
81 t = (z & 0xffff) | ((z & 0xffff) << 16);
82 Extra_PrintBinary( stdout, &t, 16 );
83 printf( " " );
84 Kit_DsdPrintFromTruth( &t, 4 );
85 printf( " " );
86 printf( " %d", (z >> 16) & 7 );
87 printf( " %d", (z >> 20) & 7 );
88 printf( " %d", (z >> 24) & 7 );
89 printf( " %d", (z >> 28) & 7 );
90 printf( "\n" );
91}
92void If_Dec08PrintConfig( unsigned * pZ )
93{
94 while ( *pZ )
95 If_Dec08PrintConfigOne( *pZ++ );
96}
97static inline void If_Dec08ComposeLut4( int t, word ** pF, word * pR, int nVars )
98{
99 word pC[16];
100 int m, w, v, nWords;
101 assert( nVars <= 10 );
102 nWords = If_Dec08WordNum( nVars );
103 for ( w = 0; w < nWords; w++ )
104 pR[w] = 0;
105 for ( m = 0; m < 16; m++ )
106 {
107 if ( !((t >> m) & 1) )
108 continue;
109 for ( w = 0; w < nWords; w++ )
110 pC[w] = ~(word)0;
111 for ( v = 0; v < 4; v++ )
112 for ( w = 0; w < nWords; w++ )
113 pC[w] &= ((m >> v) & 1) ? pF[v][w] : ~pF[v][w];
114 for ( w = 0; w < nWords; w++ )
115 pR[w] |= pC[w];
116 }
117}
118void If_Dec08Verify( word * pF, int nVars, unsigned * pZ )
119{
120 word pN[16][16], * pG[4];
121 int i, w, v, k, nWords;
122 unsigned z;
123 nWords = If_Dec08WordNum( nVars );
124 for ( k = 0; k < nVars; k++ )
125 for ( w = 0; w < nWords; w++ )
126 pN[k][w] = Truth10[k][w];
127 for ( i = 0; (z = pZ[i]); i++, k++ )
128 {
129 for ( v = 0; v < 4; v++ )
130 pG[v] = pN[ (z >> (16+(v<<2))) & 7 ];
131 If_Dec08ComposeLut4( (int)(z & 0xffff), pG, pN[k], nVars );
132 }
133 k--;
134 for ( w = 0; w < nWords; w++ )
135 if ( pN[k][w] != pF[w] )
136 {
137 If_Dec08PrintConfig( pZ );
138 Kit_DsdPrintFromTruth( (unsigned*)pF, nVars ); printf( "\n" );
139 Kit_DsdPrintFromTruth( (unsigned*)pN[k], nVars ); printf( "\n" );
140 printf( "Verification failed!\n" );
141 break;
142 }
143}
144
145
146// count the number of unique cofactors
147static inline int If_Dec08CofCount2( word * pF, int nVars )
148{
149 int nShift = (1 << (nVars - 3));
150 word Mask = (((word)1) << nShift) - 1;
151 word iCof0 = pF[0] & Mask;
152 word iCof1 = iCof0, iCof;
153 int i;
154 assert( nVars >= 6 && nVars <= 8 );
155// if ( nVars == 10 )
156// Mask = ~(word)0;
157 for ( i = 1; i < 8; i++ )
158 {
159 iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
160 if ( iCof == iCof0 )
161 continue;
162 if ( iCof1 == iCof0 )
163 iCof1 = iCof;
164 else if ( iCof != iCof1 )
165 return 3;
166 }
167 return 2;
168}
169static inline int If_Dec08CofCount( word * pF, int nVars )
170{
171 int nShift = (1 << (nVars - 3));
172 word Mask = (((word)1) << nShift) - 1;
173 word iCofs[16], iCof;
174 int i, c, nCofs = 1;
175// if ( nVars == 10 )
176// Mask = ~(word)0;
177 iCofs[0] = pF[0] & Mask;
178 for ( i = 1; i < 8; i++ )
179 {
180 iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
181 for ( c = 0; c < nCofs; c++ )
182 if ( iCof == iCofs[c] )
183 break;
184 if ( c == nCofs )
185 iCofs[nCofs++] = iCof;
186 }
187 return nCofs;
188}
189
190
191// variable permutation for large functions
192static inline void If_Dec08Copy( word * pOut, word * pIn, int nVars )
193{
194 int w, nWords = If_Dec08WordNum( nVars );
195 for ( w = 0; w < nWords; w++ )
196 pOut[w] = pIn[w];
197}
198static inline void If_Dec08SwapAdjacent( word * pOut, word * pIn, int iVar, int nVars )
199{
200 int i, k, nWords = If_Dec08WordNum( nVars );
201 assert( iVar < nVars - 1 );
202 if ( iVar < 5 )
203 {
204 int Shift = (1 << iVar);
205 for ( i = 0; i < nWords; i++ )
206 pOut[i] = (pIn[i] & PMasks[iVar][0]) | ((pIn[i] & PMasks[iVar][1]) << Shift) | ((pIn[i] & PMasks[iVar][2]) >> Shift);
207 }
208 else if ( iVar > 5 )
209 {
210 int Step = (1 << (iVar - 6));
211 for ( k = 0; k < nWords; k += 4*Step )
212 {
213 for ( i = 0; i < Step; i++ )
214 pOut[i] = pIn[i];
215 for ( i = 0; i < Step; i++ )
216 pOut[Step+i] = pIn[2*Step+i];
217 for ( i = 0; i < Step; i++ )
218 pOut[2*Step+i] = pIn[Step+i];
219 for ( i = 0; i < Step; i++ )
220 pOut[3*Step+i] = pIn[3*Step+i];
221 pIn += 4*Step;
222 pOut += 4*Step;
223 }
224 }
225 else // if ( iVar == 5 )
226 {
227 for ( i = 0; i < nWords; i += 2 )
228 {
229 pOut[i] = (pIn[i] & ABC_CONST(0x00000000FFFFFFFF)) | ((pIn[i+1] & ABC_CONST(0x00000000FFFFFFFF)) << 32);
230 pOut[i+1] = (pIn[i+1] & ABC_CONST(0xFFFFFFFF00000000)) | ((pIn[i] & ABC_CONST(0xFFFFFFFF00000000)) >> 32);
231 }
232 }
233}
234static inline void If_Dec08MoveTo( word * pF, int nVars, int v, int p, int Pla2Var[], int Var2Pla[] )
235{
236 word pG[16], * pIn = pF, * pOut = pG, * pTemp;
237 int iPlace0, iPlace1, Count = 0;
238 assert( Var2Pla[v] <= p );
239 while ( Var2Pla[v] != p )
240 {
241 iPlace0 = Var2Pla[v];
242 iPlace1 = Var2Pla[v]+1;
243 If_Dec08SwapAdjacent( pOut, pIn, iPlace0, nVars );
244 pTemp = pIn; pIn = pOut, pOut = pTemp;
245 Var2Pla[Pla2Var[iPlace0]]++;
246 Var2Pla[Pla2Var[iPlace1]]--;
247 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
248 Pla2Var[iPlace1] ^= Pla2Var[iPlace0];
249 Pla2Var[iPlace0] ^= Pla2Var[iPlace1];
250 Count++;
251 }
252 if ( Count & 1 )
253 If_Dec08Copy( pF, pIn, nVars );
254 assert( Pla2Var[p] == v );
255}
256/*
257// derive binary function
258static inline int If_Dec08DeriveCount2( word * pF, word * pRes, int nVars )
259{
260 int nShift = (1 << (nVars - 4));
261 word Mask = (((word)1) << nShift) - 1;
262 int i, MaskDec = 0;
263 word iCof0 = pF[0] & Mask;
264 word iCof1 = pF[0] & Mask;
265 word iCof, * pCof0, * pCof1;
266 if ( nVars == 10 )
267 Mask = ~(word)0;
268 for ( i = 1; i < 16; i++ )
269 {
270 iCof = (pF[(i * nShift) / 64] >> ((i * nShift) & 63)) & Mask;
271 if ( *pCof0 != iCof )
272 {
273 *pCof1 = iCof;
274 MaskDec |= (1 << i);
275 }
276 }
277 *pRes = ((iCof1 << nShift) | iCof0);
278 return MaskDec;
279}
280static inline word If_DecTruthStretch( word t, int nVars )
281{
282 assert( nVars > 1 );
283 if ( nVars == 1 )
284 nVars++, t = (t & 0x3) | ((t & 0x3) << 2);
285 if ( nVars == 2 )
286 nVars++, t = (t & 0xF) | ((t & 0xF) << 4);
287 if ( nVars == 3 )
288 nVars++, t = (t & 0xFF) | ((t & 0xFF) << 8);
289 if ( nVars == 4 )
290 nVars++, t = (t & 0xFFFF) | ((t & 0xFFFF) << 16);
291 if ( nVars == 5 )
292 nVars++, t = (t & 0xFFFFFFFF) | ((t & 0xFFFFFFFF) << 32);
293 assert( nVars >= 6 );
294}
295*/
296
297// support minimization
298static inline int If_DecSuppIsMinBase( int Supp )
299{
300 return (Supp & (Supp+1)) == 0;
301}
302static inline int If_Dec08HasVar( word * t, int nVars, int iVar )
303{
304 int nWords = If_Dec08WordNum( nVars );
305 assert( iVar < nVars );
306 if ( iVar < 6 )
307 {
308 int i, Shift = (1 << iVar);
309 for ( i = 0; i < nWords; i++ )
310 if ( (t[i] & ~Truth6[iVar]) != ((t[i] & Truth6[iVar]) >> Shift) )
311 return 1;
312 return 0;
313 }
314 else
315 {
316 int i, k, Step = (1 << (iVar - 6));
317 for ( k = 0; k < nWords; k += 2*Step )
318 {
319 for ( i = 0; i < Step; i++ )
320 if ( t[i] != t[Step+i] )
321 return 1;
322 t += 2*Step;
323 }
324 return 0;
325 }
326}
327static inline int If_Dec08Support( word * t, int nVars )
328{
329 int v, Supp = 0;
330 for ( v = 0; v < nVars; v++ )
331 if ( If_Dec08HasVar( t, nVars, v ) )
332 Supp |= (1 << v);
333 return Supp;
334}
335
336// checks
337void If_Dec08Cofactors( word * pF, int nVars, int iVar, word * pCof0, word * pCof1 )
338{
339 int nWords = If_Dec08WordNum( nVars );
340 assert( iVar < nVars );
341 if ( iVar < 6 )
342 {
343 int i, Shift = (1 << iVar);
344 for ( i = 0; i < nWords; i++ )
345 {
346 pCof0[i] = (pF[i] & ~Truth6[iVar]) | ((pF[i] & ~Truth6[iVar]) << Shift);
347 pCof1[i] = (pF[i] & Truth6[iVar]) | ((pF[i] & Truth6[iVar]) >> Shift);
348 }
349 return;
350 }
351 else
352 {
353 int i, k, Step = (1 << (iVar - 6));
354 for ( k = 0; k < nWords; k += 2*Step )
355 {
356 for ( i = 0; i < Step; i++ )
357 {
358 pCof0[i] = pCof0[Step+i] = pF[i];
359 pCof1[i] = pCof1[Step+i] = pF[Step+i];
360 }
361 pF += 2*Step;
362 pCof0 += 2*Step;
363 pCof1 += 2*Step;
364 }
365 return;
366 }
367}
368static inline int If_Dec08Count16( int Num16 )
369{
370 assert( Num16 < (1<<16)-1 );
371 return __builtin_popcount( Num16 & 0xffff );
372}
373static inline void If_DecVerifyPerm( int Pla2Var[10], int Var2Pla[10], int nVars )
374{
375 int i;
376 for ( i = 0; i < nVars; i++ )
377 assert( Pla2Var[Var2Pla[i]] == i );
378}
379int If_Dec08Perform( word * pF, int nVars, int fDerive )
380{
381// static int Cnt = 0;
382 word pCof0[16], pCof1[16];
383 int Pla2Var[10], Var2Pla[10], Count[210], Masks[210];
384 int i, i0,i1,i2, v, x;
385 assert( nVars >= 6 && nVars <= 8 );
386 // start arrays
387 for ( i = 0; i < nVars; i++ )
388 {
389 assert( If_Dec08HasVar( pF, nVars, i ) );
390 Pla2Var[i] = Var2Pla[i] = i;
391 }
392/*
393 Cnt++;
394//if ( Cnt == 108 )
395{
396printf( "%d\n", Cnt );
397//Extra_PrintHex( stdout, (unsigned *)pF, nVars );
398//printf( "\n" );
399Kit_DsdPrintFromTruth( (unsigned *)pF, nVars );
400printf( "\n" );
401printf( "\n" );
402}
403*/
404 // generate permutations
405 v = 0;
406 for ( i0 = 0; i0 < nVars; i0++ )
407 for ( i1 = i0+1; i1 < nVars; i1++ )
408 for ( i2 = i1+1; i2 < nVars; i2++, v++ )
409 {
410 If_Dec08MoveTo( pF, nVars, i0, nVars-1, Pla2Var, Var2Pla );
411 If_Dec08MoveTo( pF, nVars, i1, nVars-2, Pla2Var, Var2Pla );
412 If_Dec08MoveTo( pF, nVars, i2, nVars-3, Pla2Var, Var2Pla );
413 If_DecVerifyPerm( Pla2Var, Var2Pla, nVars );
414 Count[v] = If_Dec08CofCount( pF, nVars );
415 Masks[v] = (1 << i0) | (1 << i1) | (1 << i2);
416 assert( Count[v] > 1 );
417//printf( "%d ", Count[v] );
418 if ( Count[v] == 2 || Count[v] > 5 )
419 continue;
420 for ( x = 0; x < 4; x++ )
421 {
422 If_Dec08Cofactors( pF, nVars, nVars-1-x, pCof0, pCof1 );
423 if ( If_Dec08CofCount2(pCof0, nVars) <= 2 && If_Dec08CofCount2(pCof1, nVars) <= 2 )
424 {
425 Count[v] = -Count[v];
426 break;
427 }
428 }
429 }
430//printf( "\n" );
431 assert( v <= 210 );
432 // check if there are compatible bound sets
433 for ( i0 = 0; i0 < v; i0++ )
434 for ( i1 = i0+1; i1 < v; i1++ )
435 {
436 if ( If_Dec08Count16(Masks[i0] & Masks[i1]) > 8 - nVars )
437 continue;
438 if ( nVars == 8 )
439 {
440 if ( Count[i0] == 2 && Count[i1] == 2 )
441 return 1;
442 }
443 else if ( nVars == 7 )
444 {
445 if ( (Count[i0] == 2 && Count[i1] == 2) ||
446 (Count[i0] == 2 && Count[i1] < 0) ||
447 (Count[i0] < 0 && Count[i1] == 2) )
448 return 1;
449 }
450 else
451 {
452 if ( (Count[i0] == 2 && Count[i1] == 2) ||
453 (Count[i0] == 2 && Count[i1] < 0) ||
454 (Count[i0] < 0 && Count[i1] == 2) ||
455 (Count[i0] < 0 && Count[i1] < 0) )
456 return 1;
457 }
458 }
459// printf( "not found\n" );
460 return 0;
461}
462
463
475int If_CutPerformCheck08( If_Man_t * p, unsigned * pTruth, int nVars, int nLeaves, char * pStr )
476{
477 int nSupp, fDerive = 0;
478 word pF[16];
479 if ( nLeaves <= 5 )
480 return 1;
481 If_Dec08Copy( pF, (word *)pTruth, nVars );
482 nSupp = If_Dec08Support( pF, nLeaves );
483 if ( !nSupp || !If_DecSuppIsMinBase(nSupp) )
484 return 0;
485 if ( If_Dec08Perform( pF, nLeaves, fDerive ) )
486 {
487// printf( "1" );
488 return 1;
489// If_Dec08Verify( t, nLeaves, NULL );
490 }
491// printf( "0" );
492 return 0;
493}
494
498
499
500ABC_NAMESPACE_IMPL_END
501
nWords
int nWords
Definition abcNpn.c:127
ABC_CONST
#define ABC_CONST(number)
PARAMETERS ///.
Definition abc_global.h:240
ABC_NAMESPACE_IMPL_START
#define ABC_NAMESPACE_IMPL_START
Definition abc_namespaces.h:54
ABC_NAMESPACE_IMPL_END
#define ABC_NAMESPACE_IMPL_END
Definition abc_namespaces.h:55
p
Cube * p
Definition exorList.c:222
If_Dec08Cofactors
void If_Dec08Cofactors(word *pF, int nVars, int iVar, word *pCof0, word *pCof1)
Definition ifDec08.c:337
Kit_DsdPrintFromTruth
void Kit_DsdPrintFromTruth(unsigned *pTruth, int nVars)
Definition kitDsd.c:491
If_CutPerformCheck08
int If_CutPerformCheck08(If_Man_t *p, unsigned *pTruth, int nVars, int nLeaves, char *pStr)
Definition ifDec08.c:475
If_Dec08PrintConfig
void If_Dec08PrintConfig(unsigned *pZ)
Definition ifDec08.c:92
Extra_PrintBinary
void Extra_PrintBinary(FILE *pFile, unsigned Sign[], int nBits)
Definition extraUtilFile.c:516
If_Dec08Verify
void If_Dec08Verify(word *pF, int nVars, unsigned *pZ)
Definition ifDec08.c:118
If_Dec08Perform
int If_Dec08Perform(word *pF, int nVars, int fDerive)
Definition ifDec08.c:379
If_Man_t
struct If_Man_t_ If_Man_t
BASIC TYPES ///.
Definition if.h:77
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213