ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dauNonDsd.c
Go to the documentation of this file.
1
20
21#include "dauInt.h"
22#include "misc/util/utilTruth.h"
23#include "misc/extra/extra.h"
24
25ABC_NAMESPACE_IMPL_START
26
30
34
46int Dau_DecCheckSetTop5( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp )
47{
48 word Cof[2][64], Value;
49 word MaskFF = (((word)1) << (1 << nVarsF)) - 1;
50 int ShiftF = 6 - nVarsF, MaskF = (1 << ShiftF) - 1;
51 int pVarsS[16], pVarsB[16];
52 int nMints = (1 << nVarsB);
53 int nMintsB = (1 <<(nVarsB-nVarsS));
54 int nMintsS = (1 << nVarsS);
55 int s, b, v, m, Mint, MintB, MintS;
56 assert( nVars == nVarsB + nVarsF );
57 assert( nVars <= 16 );
58 assert( nVarsS <= 6 );
59 assert( nVarsF >= 1 && nVarsF <= 5 );
60 // collect bound/shared variables
61 for ( s = b = v = 0; v < nVarsB; v++ )
62 if ( (uMaskS >> v) & 1 )
63 pVarsB[v] = -1, pVarsS[v] = s++;
64 else
65 pVarsS[v] = -1, pVarsB[v] = b++;
66 assert( s == nVarsS );
67 assert( b == nVarsB-nVarsS );
68 // clean minterm storage
69 for ( s = 0; s < nMintsS; s++ )
70 Cof[0][s] = Cof[1][s] = ~(word)0;
71 // iterate through bound set minters
72 for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
73 {
74 // find minterm value
75 Value = (p[Mint>>ShiftF] >> ((Mint&MaskF)<<nVarsF)) & MaskFF;
76 // check if this cof already appeared
77 if ( !~Cof[0][MintS] || Cof[0][MintS] == Value )
78 Cof[0][MintS] = Value;
79 else if ( !~Cof[1][MintS] || Cof[1][MintS] == Value )
80 {
81 Cof[1][MintS] = Value;
82 if ( pDec )
83 {
84 int iMintB = MintS * nMintsB + MintB;
85 pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));
86 }
87 }
88 else
89 return 0;
90 // find next minterm
91 v = pSched[m];
92 Mint ^= (1 << v);
93 if ( (uMaskS >> v) & 1 ) // shared variable
94 MintS ^= (1 << pVarsS[v]);
95 else
96 MintB ^= (1 << pVarsB[v]);
97 }
98 // create composition function
99 if ( pComp )
100 {
101 for ( s = 0; s < nMintsS; s++ )
102 {
103 pComp[s>>ShiftF] |= (Cof[0][s] << ((s&MaskF) << nVarsF));
104 if ( ~Cof[1][s] )
105 pComp[(s+nMintsS)>>ShiftF] |= (Cof[1][s] << (((s+nMintsS)&MaskF) << nVarsF));
106 else
107 pComp[(s+nMintsS)>>ShiftF] |= (Cof[0][s] << (((s+nMintsS)&MaskF) << nVarsF));
108 }
109 if ( nVarsF + nVarsS + 1 < 6 )
110 pComp[0] = Abc_Tt6Stretch( pComp[0], nVarsF + nVarsS + 1 );
111 }
112 if ( pDec && nVarsB < 6 )
113 pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
114 return 1;
115}
116int Dau_DecCheckSetTop6( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp )
117{
118 word * Cof[2][64];
119 int nWordsF = Abc_TtWordNum(nVarsF);
120 int pVarsS[16], pVarsB[16];
121 int nMints = (1 << nVarsB);
122 int nMintsB = (1 <<(nVarsB-nVarsS));
123 int nMintsS = (1 << nVarsS);
124 int s, b, v, m, Mint, MintB, MintS;
125 assert( nVars == nVarsB + nVarsF );
126 assert( nVars <= 16 );
127 assert( nVarsS <= 6 );
128 assert( nVarsF >= 6 );
129 // collect bound/shared variables
130 for ( s = b = v = 0; v < nVarsB; v++ )
131 if ( (uMaskS >> v) & 1 )
132 pVarsB[v] = -1, pVarsS[v] = s++;
133 else
134 pVarsS[v] = -1, pVarsB[v] = b++;
135 assert( s == nVarsS );
136 assert( b == nVarsB-nVarsS );
137 // clean minterm storage
138 for ( s = 0; s < nMintsS; s++ )
139 Cof[0][s] = Cof[1][s] = NULL;
140 // iterate through bound set minters
141 for ( MintS = MintB = Mint = m = 0; m < nMints; m++ )
142 {
143 // check if this cof already appeared
144 if ( !Cof[0][MintS] || !memcmp(Cof[0][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
145 Cof[0][MintS] = p + Mint * nWordsF;
146 else if ( !Cof[1][MintS] || !memcmp(Cof[1][MintS], p + Mint * nWordsF, sizeof(word) * nWordsF) )
147 {
148 Cof[1][MintS] = p + Mint * nWordsF;
149 if ( pDec )
150 {
151 int iMintB = MintS * nMintsB + MintB;
152 pDec[iMintB>>6] |= (((word)1)<<(iMintB & 63));
153 }
154 }
155 else
156 return 0;
157 // find next minterm
158 v = pSched[m];
159 Mint ^= (1 << v);
160 if ( (uMaskS >> v) & 1 ) // shared variable
161 MintS ^= (1 << pVarsS[v]);
162 else
163 MintB ^= (1 << pVarsB[v]);
164 }
165 // create composition function
166 if ( pComp )
167 {
168 for ( s = 0; s < nMintsS; s++ )
169 {
170 memcpy( pComp + s * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
171 if ( Cof[1][s] )
172 memcpy( pComp + (s+nMintsS) * nWordsF, Cof[1][s], sizeof(word) * nWordsF );
173 else
174 memcpy( pComp + (s+nMintsS) * nWordsF, Cof[0][s], sizeof(word) * nWordsF );
175 }
176 }
177 if ( pDec && nVarsB < 6 )
178 pDec[0] = Abc_Tt6Stretch( pDec[0], nVarsB );
179 return 1;
180}
181static inline int Dau_DecCheckSetTop( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int * pSched, word * pDec, word * pComp )
182{
183 if ( nVarsF < 6 )
184 return Dau_DecCheckSetTop5( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp );
185 else
186 return Dau_DecCheckSetTop6( p, nVars, nVarsF, nVarsB, nVarsS, uMaskS, pSched, pDec, pComp );
187}
188
200static inline void Dau_DecGetMinterm( word * p, int g, int nVarsS, int uMaskAll )
201{
202 int m, c, v;
203 for ( m = c = v = 0; v < nVarsS; v++ )
204 if ( !((uMaskAll >> v) & 1) ) // not shared bound set variable
205 {
206 if ( (g >> v) & 1 )
207 m |= (1 << c);
208 c++;
209 }
210 assert( c >= 2 );
211 p[m>>6] |= (((word)1)<<(m & 63));
212}
213static inline int Dau_DecCheckSet5( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
214{
215 int fFound0 = 0, fFound1 = 0;
216 int g, gMax = (1 << (nVars - nVarsF));
217 int Shift = 6 - nVarsF, Mask = (1 << Shift) - 1;
218 word Mask2 = (((word)1) << (1 << nVarsF)) - 1;
219 word Cof0 = 0, Cof1 = 0, Value;
220 assert( nVarsF >= 1 && nVarsF <= 5 );
221 if ( pDec ) *pDec = 0;
222 for ( g = 0; g < gMax; g++ )
223 if ( (g & uMaskAll) == uMaskValue ) // this minterm g matches shared variable minterm uMaskValue
224 {
225 Value = (p[g>>Shift] >> ((g&Mask)<<nVarsF)) & Mask2;
226 if ( !fFound0 )
227 Cof0 = Value, fFound0 = 1;
228 else if ( Cof0 == Value )
229 continue;
230 else if ( !fFound1 )
231 {
232 Cof1 = Value, fFound1 = 1;
233 if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
234 }
235 else if ( Cof1 == Value )
236 {
237 if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
238 continue;
239 }
240 else
241 return 0;
242 }
243 if ( pCof0 )
244 {
245 assert( fFound0 );
246 Cof1 = fFound1 ? Cof1 : Cof0;
247 *pCof0 = Abc_Tt6Stretch( Cof0, nVarsF );
248 *pCof1 = Abc_Tt6Stretch( Cof1, nVarsF );
249 }
250 return 1;
251}
252static inline int Dau_DecCheckSet6( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
253{
254 int fFound0 = 0, fFound1 = 0;
255 int g, gMax = (1 << (nVars - nVarsF));
256 int nWords = Abc_TtWordNum(nVarsF);
257 word * Cof0 = NULL, * Cof1 = NULL;
258 assert( nVarsF >= 6 && nVarsF <= nVars - 2 );
259 if ( pDec ) *pDec = 0;
260 for ( g = 0; g < gMax; g++ )
261 if ( (g & uMaskAll) == uMaskValue )
262 {
263 if ( !fFound0 )
264 Cof0 = p + g * nWords, fFound0 = 1;
265 else if ( !memcmp(Cof0, p + g * nWords, sizeof(word) * nWords) )
266 continue;
267 else if ( !fFound1 )
268 {
269 Cof1 = p + g * nWords, fFound1 = 1;
270 if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
271 }
272 else if ( !memcmp(Cof1, p + g * nWords, sizeof(word) * nWords) )
273 {
274 if ( pDec ) Dau_DecGetMinterm( pDec, g, nVars-nVarsF, uMaskAll );
275 continue;
276 }
277 else
278 return 0;
279 }
280 if ( pCof0 )
281 {
282 assert( fFound0 );
283 Cof1 = fFound1 ? Cof1 : Cof0;
284 memcpy( pCof0, Cof0, sizeof(word) * nWords );
285 memcpy( pCof1, Cof1, sizeof(word) * nWords );
286 }
287 return 1;
288}
289static inline int Dau_DecCheckSetAny( word * p, int nVars, int nVarsF, int uMaskAll, int uMaskValue, word * pCof0, word * pCof1, word * pDec )
290{
291 assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
292 if ( nVarsF < 6 )
293 return Dau_DecCheckSet5( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
294 else
295 return Dau_DecCheckSet6( p, nVars, nVarsF, uMaskAll, uMaskValue, pCof0, pCof1, pDec );
296}
297int Dau_DecCheckSetTopOld( word * p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word ** pCof0, word ** pCof1, word ** pDec )
298{
299 int i, pVarsS[16];
300 int v, m, mMax = (1 << nVarsS), uMaskValue;
301 assert( nVars >= 3 && nVars <= 16 );
302 assert( nVars == nVarsF + nVarsB );
303 assert( nVarsF >= 1 && nVarsF <= nVars - 2 );
304 assert( nVarsB >= 2 && nVarsB <= nVars - 1 );
305 assert( nVarsS >= 0 && nVarsS <= nVarsB - 2 );
306 if ( nVarsS == 0 )
307 return Dau_DecCheckSetAny( p, nVars, nVarsF, 0, 0, pCof0? pCof0[0] : 0, pCof1? pCof1[0] : 0, pDec? pDec[0] : 0 );
308 // collect shared variables
309 assert( maskS > 0 && maskS < (1 << nVarsB) );
310 for ( i = 0, v = 0; v < nVarsB; v++ )
311 if ( (maskS >> v) & 1 )
312 pVarsS[i++] = v;
313 assert( i == nVarsS );
314 // go through shared set minterms
315 for ( m = 0; m < mMax; m++ )
316 {
317 // generate share set mask
318 uMaskValue = 0;
319 for ( v = 0; v < nVarsS; v++ )
320 if ( (m >> v) & 1 )
321 uMaskValue |= (1 << pVarsS[v]);
322 assert( (maskS & uMaskValue) == uMaskValue );
323 // check decomposition
324 if ( !Dau_DecCheckSetAny( p, nVars, nVarsF, maskS, uMaskValue, pCof0? pCof0[m] : 0, pCof1? pCof1[m] : 0, pDec? pDec[m] : 0 ) )
325 return 0;
326 }
327 return 1;
328}
329
330
342static inline unsigned Dau_DecCreateSet( int * pVarsB, int sizeB, int maskS )
343{
344 unsigned uSet = 0; int v;
345 for ( v = 0; v < sizeB; v++ )
346 {
347 uSet |= (1 << (pVarsB[v] << 1));
348 if ( (maskS >> v) & 1 )
349 uSet |= (1 << ((pVarsB[v] << 1)+1));
350 }
351 return uSet;
352}
353static inline int Dau_DecSetHas01( unsigned Mask )
354{
355 return (Mask & ((~Mask) >> 1) & 0x55555555);
356}
357static inline int Dau_DecSetIsContained( Vec_Int_t * vSets, unsigned New )
358// Old=abcD contains New=abcDE
359// Old=abcD contains New=abCD
360{
361 unsigned Old;
362 int i, Entry;
363 Vec_IntForEachEntry( vSets, Entry, i )
364 {
365 Old = (unsigned)Entry;
366 if ( (Old & ~New) == 0 && !Dau_DecSetHas01(~Old & New))
367 return 1;
368 }
369 return 0;
370}
371void Dau_DecSortSet( unsigned set, int nVars, int * pnUnique, int * pnShared, int * pnFree )
372{
373 int v;
374 int nUnique = 0, nShared = 0, nFree = 0;
375 for ( v = 0; v < nVars; v++ )
376 {
377 int Value = ((set >> (v << 1)) & 3);
378 if ( Value == 1 )
379 nUnique++;
380 else if ( Value == 3 )
381 nShared++;
382 else if ( Value == 0 )
383 nFree++;
384 else assert( 0 );
385 }
386 *pnUnique = nUnique;
387 *pnShared = nShared;
388 *pnFree = nFree;
389}
390void Dau_DecPrintSet( unsigned set, int nVars, int fNewLine )
391{
392 int v, Counter = 0;
393 int nUnique = 0, nShared = 0, nFree = 0;
394 Dau_DecSortSet( set, nVars, &nUnique, &nShared, &nFree );
395 printf( "S =%2d D =%2d C =%2d ", nShared, nUnique+nShared, nShared+nFree+1 );
396
397 printf( "x=" );
398 for ( v = 0; v < nVars; v++ )
399 {
400 int Value = ((set >> (v << 1)) & 3);
401 if ( Value == 1 )
402 printf( "%c", 'a' + v ), Counter++;
403 else if ( Value == 3 )
404 printf( "%c", 'A' + v ), Counter++;
405 else assert( Value == 0 );
406 }
407 printf( " y=x" );
408 for ( v = 0; v < nVars; v++ )
409 {
410 int Value = ((set >> (v << 1)) & 3);
411 if ( Value == 0 )
412 printf( "%c", 'a' + v ), Counter++;
413 else if ( Value == 3 )
414 printf( "%c", 'A' + v ), Counter++;
415 }
416 for ( ; Counter < 15; Counter++ )
417 printf( " " );
418 if ( fNewLine )
419 printf( "\n" );
420}
421unsigned Dau_DecReadSet( char * pStr )
422{
423 unsigned uSet = 0; int v;
424 for ( v = 0; pStr[v]; v++ )
425 {
426 if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
427 uSet |= (1 << ((pStr[v] - 'a') << 1));
428 else if ( pStr[v] >= 'A' && pStr[v] <= 'Z' )
429 uSet |= (1 << ((pStr[v] - 'a') << 1)) | (1 << (((pStr[v] - 'a') << 1)+1));
430 else break;
431 }
432 return uSet;
433}
434void Dau_DecPrintSets( Vec_Int_t * vSets, int nVars )
435{
436 int i, Entry;
437 printf( "The %d-variable set family contains %d sets:\n", nVars, Vec_IntSize(vSets) );
438 Vec_IntForEachEntry( vSets, Entry, i )
439 Dau_DecPrintSet( (unsigned)Entry, nVars, 1 );
440 printf( "\n" );
441}
442
454void Dau_DecMoveFreeToLSB( word * p, int nVars, int * V2P, int * P2V, int maskB, int sizeB )
455{
456 int v, c = 0;
457 for ( v = 0; v < nVars; v++ )
458 if ( !((maskB >> v) & 1) )
459 Abc_TtMoveVar( p, nVars, V2P, P2V, v, c++ );
460 assert( c == nVars - sizeB );
461}
462Vec_Int_t * Dau_DecFindSets_int( word * pInit, int nVars, int * pSched[16] )
463{
464 Vec_Int_t * vSets = Vec_IntAlloc( 32 );
465 int V2P[16], P2V[16], pVarsB[16];
466 int Limit = (1 << nVars);
467 int c, v, sizeB, sizeS, maskB, maskS;
468 unsigned setMixed;
469 word p[1<<10];
470 memcpy( p, pInit, sizeof(word) * Abc_TtWordNum(nVars) );
471 for ( v = 0; v < nVars; v++ )
472 assert( Abc_TtHasVar( p, nVars, v ) );
473 // initialize permutation
474 for ( v = 0; v < nVars; v++ )
475 V2P[v] = P2V[v] = v;
476 // iterate through bound sets of each size in increasing order
477 for ( sizeB = 2; sizeB < nVars; sizeB++ ) // bound set size
478 for ( maskB = 0; maskB < Limit; maskB++ ) // bound set
479 if ( Abc_TtBitCount16(maskB) == sizeB )
480 {
481 // permute variables to have bound set on top
482 Dau_DecMoveFreeToLSB( p, nVars, V2P, P2V, maskB, sizeB );
483 // collect bound set vars on levels nVars-sizeB to nVars-1
484 for ( c = 0; c < sizeB; c++ )
485 pVarsB[c] = P2V[nVars-sizeB+c];
486 // check disjoint
487// if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, 0, 0, NULL, NULL, NULL) )
488 if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, 0, 0, pSched[sizeB], NULL, NULL) )
489 {
490 Vec_IntPush( vSets, Dau_DecCreateSet(pVarsB, sizeB, 0) );
491 continue;
492 }
493 if ( sizeB == 2 )
494 continue;
495 // iterate through shared sets of each size in the increasing order
496 for ( sizeS = 1; sizeS <= sizeB - 2; sizeS++ ) // shared set size
497 if ( sizeS <= 3 )
498// sizeS = 1;
499 for ( maskS = 0; maskS < (1 << sizeB); maskS++ ) // shared set
500 if ( Abc_TtBitCount16(maskS) == sizeS )
501 {
502 setMixed = Dau_DecCreateSet( pVarsB, sizeB, maskS );
503// printf( "Considering %10d ", setMixed );
504// Dau_DecPrintSet( setMixed, nVars );
505 // check if it exists
506 if ( Dau_DecSetIsContained(vSets, setMixed) )
507 continue;
508 // check if it can be added
509// if ( Dau_DecCheckSetTopOld(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, NULL, NULL, NULL) )
510 if ( Dau_DecCheckSetTop(p, nVars, nVars-sizeB, sizeB, sizeS, maskS, pSched[sizeB], NULL, NULL) )
511 Vec_IntPush( vSets, setMixed );
512 }
513 }
514 return vSets;
515}
516Vec_Int_t * Dau_DecFindSets( word * pInit, int nVars )
517{
518 Vec_Int_t * vSets;
519 int v, * pSched[16] = {NULL};
520 for ( v = 2; v < nVars; v++ )
521 pSched[v] = Extra_GreyCodeSchedule( v );
522 vSets = Dau_DecFindSets_int( pInit, nVars, pSched );
523 for ( v = 2; v < nVars; v++ )
524 ABC_FREE( pSched[v] );
525 return vSets;
526}
527void Dau_DecFindSetsTest2()
528{
529 Vec_Int_t * vSets;
530 word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
531 word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
532 word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
533// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
534// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
535// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
536// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
537// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
538 int nVars = 5;
539
540 vSets = Dau_DecFindSets( &t, nVars );
541 Dau_DecPrintSets( vSets, nVars );
542 Vec_IntFree( vSets );
543}
544
545
557void Dau_DecVarReplace( char * pStr, int * pPerm, int nVars )
558{
559 int v;
560 for ( v = 0; pStr[v]; v++ )
561 if ( pStr[v] >= 'a' && pStr[v] <= 'z' )
562 {
563 assert( pStr[v] - 'a' < nVars );
564 pStr[v] = 'a' + pPerm[pStr[v] - 'a'];
565 }
566}
567
579int Dau_DecDecomposeSet( word * pInit, int nVars, unsigned uSet, word * pComp, word * pDec, int * pPermC, int * pPermD, int * pnVarsC, int * pnVarsD, int * pnVarsS )
580{
581 word p[1<<13], Cof[64], Cof0[64], Cof1[64], Decs[64];
582 word * pCof0[64], * pCof1[64], * pDecs[64], MintC, MintD;
583 int V2P[16], P2V[16], pVarsU[16], pVarsS[16], pVarsF[16];
584 int nVarsU = 0, nVarsS = 0, nVarsF = 0;
585 int nWords = Abc_TtWordNum(nVars);
586 int v, d, c, Status, nDecs;
587 assert( nVars <= 16 );
588 for ( v = 0; v < nVars; v++ )
589 V2P[v] = P2V[v] = v;
590 memcpy( p, pInit, sizeof(word) * nWords );
591 // sort variables
592 for ( v = 0; v < nVars; v++ )
593 {
594 int Value = (uSet >> (v<<1)) & 3;
595 if ( Value == 0 )
596 pVarsF[nVarsF++] = v;
597 else if ( Value == 1 )
598 pVarsU[nVarsU++] = v;
599 else if ( Value == 3 )
600 pVarsS[nVarsS++] = v;
601 else assert(0);
602 }
603 assert( nVarsS >= 0 && nVarsS <= 6 );
604 assert( nVarsF + nVarsS + 1 <= 6 );
605 assert( nVarsU + nVarsS <= 6 );
606 // init space for decomposition functions
607 nDecs = (1 << nVarsS);
608 for ( d = 0; d < nDecs; d++ )
609 {
610 pCof0[d] = Cof0 + d;
611 pCof1[d] = Cof1 + d;
612 pDecs[d] = Decs + d;
613 }
614 // permute variables
615 c = 0;
616 for ( v = 0; v < nVarsF; v++ )
617 Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsF[v], c++ );
618 for ( v = 0; v < nVarsS; v++ )
619 Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsS[v], c++ );
620 for ( v = 0; v < nVarsU; v++ )
621 Abc_TtMoveVar( p, nVars, V2P, P2V, pVarsU[v], c++ );
622 assert( c == nVars );
623 // check decomposition
624 Status = Dau_DecCheckSetTopOld( p, nVars, nVarsF, nVarsS+nVarsU, nVarsS, Abc_InfoMask(nVarsS), pCof0, pCof1, pDecs );
625 if ( !Status )
626 return 0;
627 // compute cofactors
628 assert( nVarsF + nVarsS < 6 );
629 for ( d = 0; d < nDecs; d++ )
630 {
631 Cof[d] = (pCof1[d][0] & s_Truths6[nVarsF + nVarsS]) | (pCof0[d][0] & ~s_Truths6[nVarsF + nVarsS]);
632 pDecs[d][0] = Abc_Tt6Stretch( pDecs[d][0], nVarsU );
633 }
634 // compute the resulting functions
635 pComp[0] = 0;
636 pDec[0] = 0;
637 for ( d = 0; d < nDecs; d++ )
638 {
639 // compute minterms for composition/decomposition function
640 MintC = MintD = ~((word)0);
641 for ( v = 0; v < nVarsS; v++ )
642 {
643 MintC &= ((d >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
644 MintD &= ((d >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
645 }
646 // derive functions
647 pComp[0] |= MintC & Cof[d];
648 pDec[0] |= MintD & pDecs[d][0];
649 }
650 // derive variable permutations
651 if ( pPermC )
652 {
653 for ( v = 0; v < nVarsF; v++ )
654 pPermC[v] = pVarsF[v];
655 for ( v = 0; v < nVarsS; v++ )
656 pPermC[nVarsF+v] = pVarsS[v];
657 pPermC[nVarsF + nVarsS] = nVars;
658 }
659 if ( pPermD )
660 {
661 for ( v = 0; v < nVarsU; v++ )
662 pPermD[v] = pVarsU[v];
663 for ( v = 0; v < nVarsS; v++ )
664 pPermD[nVarsU+v] = pVarsS[v];
665 }
666 if ( pnVarsC )
667 *pnVarsC = nVarsF + nVarsS + 1;
668 if ( pnVarsD )
669 *pnVarsD = nVarsU + nVarsS;
670 if ( pnVarsS )
671 *pnVarsS = nVarsS;
672 return 1;
673}
674
675
687int Dau_DecVerify( word * pInit, int nVars, char * pDsdC, char * pDsdD )
688{
689 word pC[1<<13], pD[1<<13], pRes[1<<13]; // max = 16
690 int nWordsC = Abc_TtWordNum(nVars+1);
691 int nWordsD = Abc_TtWordNum(nVars);
692 assert( nVars < 16 );
693 memcpy( pC, Dau_DsdToTruth(pDsdC, nVars+1), sizeof(word) * nWordsC );
694 memcpy( pD, Dau_DsdToTruth(pDsdD, nVars), sizeof(word) * nWordsD );
695 if ( nVars >= 6 )
696 {
697 assert( nWordsD >= 1 );
698 assert( nWordsC > 1 );
699 Abc_TtMux( pRes, pD, pC + nWordsD, pC, nWordsD );
700 }
701 else
702 {
703 word pC0 = Abc_Tt6Stretch( pC[0], nVars );
704 word pC1 = Abc_Tt6Stretch( (pC[0] >> (1 << nVars)), nVars );
705 Abc_TtMux( pRes, pD, &pC1, &pC0, nWordsD );
706 }
707 if ( !Abc_TtEqual(pInit, pRes, nWordsD) )
708 printf( " Verification failed" );
709// else
710// printf( " Verification successful" );
711 printf( "\n" );
712 return 1;
713}
714int Dau_DecPerform6( word * p, int nVars, unsigned uSet )
715{
716 word tComp = 0, tDec = 0, tDec0, tComp0, tComp1, FuncC, FuncD;
717 char pDsdC[1000], pDsdD[1000];
718 int pPermC[16], pPermD[16];
719 int nVarsC, nVarsD, nVarsS, nVarsU, nVarsF, nPairs;
720 int i, m, v, status, ResC, ResD, Counter = 0;
721 status = Dau_DecDecomposeSet( p, nVars, uSet, &tComp, &tDec0, pPermC, pPermD, &nVarsC, &nVarsD, &nVarsS );
722 if ( !status )
723 {
724 printf( " Decomposition does not exist\n" );
725 return 0;
726 }
727 nVarsU = nVarsD - nVarsS;
728 nVarsF = nVarsC - nVarsS - 1;
729 tComp0 = Abc_Tt6Cofactor0( tComp, nVarsF + nVarsS );
730 tComp1 = Abc_Tt6Cofactor1( tComp, nVarsF + nVarsS );
731 nPairs = 1 << (1 << nVarsS);
732 for ( i = 0; i < nPairs; i++ )
733 {
734 if ( i & 1 )
735 continue;
736 // create miterms with this polarity
737 FuncC = FuncD = 0;
738 for ( m = 0; m < (1 << nVarsS); m++ )
739 {
740 word MintC, MintD;
741 if ( !((i >> m) & 1) )
742 continue;
743 MintC = MintD = ~(word)0;
744 for ( v = 0; v < nVarsS; v++ )
745 {
746 MintC &= ((m >> v) & 1) ? s_Truths6[nVarsF+v] : ~s_Truths6[nVarsF+v];
747 MintD &= ((m >> v) & 1) ? s_Truths6[nVarsU+v] : ~s_Truths6[nVarsU+v];
748 }
749 FuncC |= MintC;
750 FuncD |= MintD;
751 }
752 // uncomplement given variables
753 tComp = (~s_Truths6[nVarsF + nVarsS] & ((tComp0 & ~FuncC) | (tComp1 & FuncC))) | (s_Truths6[nVarsF + nVarsS] & ((tComp1 & ~FuncC) | (tComp0 & FuncC)));
754 tDec = tDec0 ^ FuncD;
755 // decompose
756 ResC = Dau_DsdDecompose( &tComp, nVarsC, 0, 1, pDsdC );
757 ResD = Dau_DsdDecompose( &tDec, nVarsD, 0, 1, pDsdD );
758 // replace variables
759 Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
760 Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
761 // report
762// printf( " " );
763 printf( "%3d : ", Counter++ );
764 printf( "%24s ", pDsdD );
765 printf( "%24s ", pDsdC );
766 Dau_DecVerify( p, nVars, pDsdC, pDsdD );
767 }
768 return 1;
769}
770
771int Dau_DecPerform( word * pInit, int nVars, unsigned uSet )
772{
773 word p[1<<10], pDec[1<<10], pComp[1<<10]; // at most 2^10 words
774 char pDsdC[5000], pDsdD[5000]; // at most 2^12 hex digits
775 int nVarsU, nVarsS, nVarsF, nVarsC = 0, nVarsD = 0;
776 int V2P[16], P2V[16], pPermC[16], pPermD[16], * pSched;
777 int v, i, status, ResC, ResD;
778 int nWords = Abc_TtWordNum(nVars);
779 assert( nVars <= 16 );
780 // backup the function
781 memcpy( p, pInit, sizeof(word) * nWords );
782 // get variable numbers
783 Dau_DecSortSet( uSet, nVars, &nVarsU, &nVarsS, &nVarsF );
784 // permute function and order variables
785 for ( v = 0; v < nVars; v++ )
786 V2P[v] = P2V[v] = v;
787 for ( i = v = 0; v < nVars; v++ )
788 if ( ((uSet >> (v<<1)) & 3) == 0 ) // free first
789 Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
790 for ( v = 0; v < nVars; v++ )
791 if ( ((uSet >> (v<<1)) & 3) == 3 ) // share second
792 Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermC[nVarsC++] = v;
793 pPermC[nVarsC++] = nVars;
794 for ( v = 0; v < nVars; v++ )
795 if ( ((uSet >> (v<<1)) & 3) == 1 ) // unique last
796 Abc_TtMoveVar( p, nVars, V2P, P2V, v, i++ ), pPermD[nVarsD++] = v;
797 for ( v = 0; v < nVarsS; v++ )
798 pPermD[nVarsD++] = pPermC[nVarsF+v];
799 assert( nVarsD == nVarsU + nVarsS );
800 assert( nVarsC == nVarsF + nVarsS + 1 );
801 assert( i == nVars );
802 // decompose
803 pSched = Extra_GreyCodeSchedule( nVarsU + nVarsS );
804 memset( pDec, 0, sizeof(word) * Abc_TtWordNum(nVarsD) );
805 memset( pComp, 0, sizeof(word) * Abc_TtWordNum(nVarsC) );
806 status = Dau_DecCheckSetTop( p, nVars, nVarsF, nVarsU + nVarsS, nVarsS, nVarsS ? Abc_InfoMask(nVarsS) : 0, pSched, pDec, pComp );
807 ABC_FREE( pSched );
808 if ( !status )
809 {
810 printf( " Decomposition does not exist\n" );
811 return 0;
812 }
813// Dau_DsdPrintFromTruth( stdout, pC, nVars+1 ); //printf( "\n" );
814// Dau_DsdPrintFromTruth( stdout, pD, nVars ); //printf( "\n" );
815// Kit_DsdPrintFromTruth( (unsigned *)pComp, 6 ); printf( "\n" );
816// Kit_DsdPrintFromTruth( (unsigned *)pDec, 6 ); printf( "\n" );
817 // decompose
818 ResC = Dau_DsdDecompose( pComp, nVarsC, 0, 1, pDsdC );
819 ResD = Dau_DsdDecompose( pDec, nVarsD, 0, 1, pDsdD );
820 // replace variables
821 Dau_DecVarReplace( pDsdD, pPermD, nVarsD );
822 Dau_DecVarReplace( pDsdC, pPermC, nVarsC );
823 // report
824 printf( " " );
825 printf( "%3d : ", 0 );
826 printf( "%24s ", pDsdD );
827 printf( "%24s ", pDsdC );
828 Dau_DecVerify( pInit, nVars, pDsdC, pDsdD );
829 return 1;
830}
831void Dau_DecTrySets( word * pInit, int nVars, int fVerbose )
832{
833 Vec_Int_t * vSets;
834 int i, Entry;
835 assert( nVars <= 16 );
836 vSets = Dau_DecFindSets( pInit, nVars );
837 if ( !fVerbose )
838 {
839 Vec_IntFree( vSets );
840 return;
841 }
842 Dau_DsdPrintFromTruth( pInit, nVars );
843 printf( "This %d-variable function has %d decomposable variable sets:\n", nVars, Vec_IntSize(vSets) );
844 Vec_IntForEachEntry( vSets, Entry, i )
845 {
846 unsigned uSet = (unsigned)Entry;
847 printf( "Set %4d : ", i );
848 if ( nVars > 6 )
849 {
850 Dau_DecPrintSet( uSet, nVars, 0 );
851 Dau_DecPerform( pInit, nVars, uSet );
852 }
853 else
854 {
855 Dau_DecPrintSet( uSet, nVars, 1 );
856 Dau_DecPerform6( pInit, nVars, uSet );
857 }
858 }
859 Vec_IntFree( vSets );
860// printf( "\n" );
861}
862
863void Dau_DecFindSetsTest3()
864{
865 word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
866 word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
867 word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
868// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
869 int nVars = 6;
870 char * pStr = "Bcd";
871// char * pStr = "Abcd";
872// char * pStr = "ab";
873 unsigned uSet = Dau_DecReadSet( pStr );
874 Dau_DecPerform6( &t, nVars, uSet );
875}
876
877void Dau_DecFindSetsTest()
878{
879 int nVars = 6;
880// word a0 = (~s_Truths6[1] & s_Truths6[2]) | (s_Truths6[1] & s_Truths6[3]);
881// word a1 = (~s_Truths6[1] & s_Truths6[4]) | (s_Truths6[1] & s_Truths6[5]);
882// word t = (~s_Truths6[0] & a0) | (s_Truths6[0] & a1);
883// word t = ABC_CONST(0x7EFFFFFFFFFFFF7E); // and(gam1,gam2)
884// word t = ABC_CONST(0xB0F0BBFFB0F0BAFE); // some funct
885// word t = ABC_CONST(0x00000000901FFFFF); // some funct
886 word t = ABC_CONST(0x000030F00D0D3FFF); // some funct
887// word t = ABC_CONST(0x00000000690006FF); // some funct
888// word t = ABC_CONST(0x7000F80007FF0FFF); // some funct
889// word t = ABC_CONST(0x4133CB334133CB33); // some funct 5 var
890// word t = ABC_CONST(0x2B0228022B022802); // 5-var non-dec0x0F7700000F770000
891// word t = ABC_CONST(0x0F7700000F770000); // (!<(ab)cd>e)
892// word t = ABC_CONST(0x7F00000000000000); // (!(abc)def)
893 Dau_DecTrySets( &t, nVars, 1 );
894}
895
896
900
901
902ABC_NAMESPACE_IMPL_END
903
nWords
int nWords
Definition abcNpn.c:127
ABC_FREE
#define ABC_FREE(obj)
Definition abc_global.h:267
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
Vec_Int_t
typedefABC_NAMESPACE_IMPL_START struct Vec_Int_t_ Vec_Int_t
DECLARATIONS ///.
Definition bblif.c:37
Dau_DecVarReplace
void Dau_DecVarReplace(char *pStr, int *pPerm, int nVars)
Definition dauNonDsd.c:557
Dau_DecPrintSet
void Dau_DecPrintSet(unsigned set, int nVars, int fNewLine)
Definition dauNonDsd.c:390
Dau_DecVerify
int Dau_DecVerify(word *pInit, int nVars, char *pDsdC, char *pDsdD)
Definition dauNonDsd.c:687
Dau_DecPerform
int Dau_DecPerform(word *pInit, int nVars, unsigned uSet)
Definition dauNonDsd.c:771
Dau_DecFindSets
Vec_Int_t * Dau_DecFindSets(word *pInit, int nVars)
Definition dauNonDsd.c:516
Dau_DecCheckSetTopOld
int Dau_DecCheckSetTopOld(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int maskS, word **pCof0, word **pCof1, word **pDec)
Definition dauNonDsd.c:297
Dau_DecReadSet
unsigned Dau_DecReadSet(char *pStr)
Definition dauNonDsd.c:421
Dau_DecPerform6
int Dau_DecPerform6(word *p, int nVars, unsigned uSet)
Definition dauNonDsd.c:714
Dau_DecMoveFreeToLSB
void Dau_DecMoveFreeToLSB(word *p, int nVars, int *V2P, int *P2V, int maskB, int sizeB)
Definition dauNonDsd.c:454
Dau_DecDecomposeSet
int Dau_DecDecomposeSet(word *pInit, int nVars, unsigned uSet, word *pComp, word *pDec, int *pPermC, int *pPermD, int *pnVarsC, int *pnVarsD, int *pnVarsS)
Definition dauNonDsd.c:579
Dau_DecCheckSetTop5
ABC_NAMESPACE_IMPL_START int Dau_DecCheckSetTop5(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
DECLARATIONS ///.
Definition dauNonDsd.c:46
Dau_DecPrintSets
void Dau_DecPrintSets(Vec_Int_t *vSets, int nVars)
Definition dauNonDsd.c:434
Dau_DecFindSetsTest2
void Dau_DecFindSetsTest2()
Definition dauNonDsd.c:527
Dau_DecCheckSetTop6
int Dau_DecCheckSetTop6(word *p, int nVars, int nVarsF, int nVarsB, int nVarsS, int uMaskS, int *pSched, word *pDec, word *pComp)
Definition dauNonDsd.c:116
Dau_DecFindSetsTest3
void Dau_DecFindSetsTest3()
Definition dauNonDsd.c:863
Dau_DecFindSetsTest
void Dau_DecFindSetsTest()
Definition dauNonDsd.c:877
Dau_DecTrySets
void Dau_DecTrySets(word *pInit, int nVars, int fVerbose)
Definition dauNonDsd.c:831
Dau_DecFindSets_int
Vec_Int_t * Dau_DecFindSets_int(word *pInit, int nVars, int *pSched[16])
Definition dauNonDsd.c:462
Dau_DecSortSet
void Dau_DecSortSet(unsigned set, int nVars, int *pnUnique, int *pnShared, int *pnFree)
Definition dauNonDsd.c:371
Dau_DsdToTruth
word * Dau_DsdToTruth(char *p, int nVars)
Definition dauDsd.c:609
Dau_DsdDecompose
int Dau_DsdDecompose(word *pTruth, int nVarsInit, int fSplitPrime, int fWriteTruth, char *pRes)
Definition dauDsd.c:1912
Dau_DsdPrintFromTruth
void Dau_DsdPrintFromTruth(word *pTruth, int nVarsInit)
Definition dauDsd.c:1968
p
Cube * p
Definition exorList.c:222
a0
#define a0
Definition extraBdd.h:79
a1
#define a1
Definition extraBdd.h:80
Extra_GreyCodeSchedule
int * Extra_GreyCodeSchedule(int n)
Definition extraUtilMisc.c:2170
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
memset
char * memset()
memcmp
int memcmp()
Vec_IntForEachEntry
#define Vec_IntForEachEntry(vVec, Entry, i)
MACRO DEFINITIONS ///.
Definition vecInt.h:54