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