ABC: A System for Sequential Synthesis and Verification
 
Loading...
Searching...
No Matches
dauDsd2.c
Go to the documentation of this file.
1
20
21#include "dauInt.h"
22#include "misc/util/utilTruth.h"
23
24ABC_NAMESPACE_IMPL_START
25
29
30#include DSD_MAX_VAR 12
31#include DSD_MAX_WRD ((DSD_MAX_VAR > 6) ? (1 << (DSD_MAX_VAR-6)) : 1)
32
33typedef struct Dua_Obj_t_ Dua_Obj_t;
34struct Dua_Obj_t_
35{
36 int Type; // dec type (1=var; 2=and; 3=xor; 4=mux; 5=prime)
37 int nFans; // fanin count
38 char pFans[DSD_MAX_VAR]; // fanins
39};
40
41typedef struct Dua_Dsd_t_ Dua_Dsd_t;
42struct Dua_Dsd_t_
43{
44 int nSupp; // original variables
45 int nVars; // remaining variables
46 int nWords; // largest non-dec prime
47 int nObjs; // object count
48 int iRoot; // the root of the tree
49 Dua_Obj_t pObjs[DSD_MAX_VAR]; // objects
50 word pTruth[DSD_MAX_WRD]; // original/current truth table
51};
52
56
69static inline word Abc_Tt6HalfUnShuffleVars( word t, int iVar, int fCof1 )
70{
71 static word Masks[6] = {
72 ABC_CONST(0x5555555555555555),
73 ABC_CONST(0x3333333333333333),
74 ABC_CONST(0x0F0F0F0F0F0F0F0F),
75 ABC_CONST(0x00FF00FF00FF00FF),
76 ABC_CONST(0x0000FFFF0000FFFF),
77 ABC_CONST(0x00000000FFFFFFFF)
78 };
79 int v, s = (1 << iVar);
80 t = (t >> (fCof1 ? 0 : s)) & Masks[iVar];
81 for ( v = iVar, s = (1 << v); v < 5; v++, s <<= 1 )
82 t = ((t >> s) | t) & Masks[v+1];
83 return t;
84}
85
86static inline void Abc_TtHalfUnShuffleVars( word * pTruth, int nVars, int iVar, int jVar, int fCof1 )
87{
88 int w, nWords = Abc_TtWordNum( nVars );
89 if ( iVar == jVar )
90 return;
91 assert( iVar < jVar );
92 if ( iVar < 5 )
93 {
94 for ( w = 0; w < nWords; w++ )
95 pTruth[w] = Abc_Tt6HalfUnShuffleVars( pTruth[w], iVar, fCof1 );
96 iVar = 5;
97 }
98 if ( jVar < 6 )
99 {
100 for ( w = 0; w < nWords; w++ )
101 pTruth[w] = (pTruth[w] << 32) | pTruth[w];
102 return;
103 }
104 if ( iVar == 5 )
105 {
106 unsigned * pTruthU = (unsigned *)pTruth;
107 for ( w = 0; w < nWords; w += 2 )
108 pTruthU[w] = pTruthU[w+1];
109 iVar = 6;
110 }
111 {
112 word * pLimit = pTruth + nWords;
113 int i, iStep = Abc_TtWordNum(iVar);
114 int j, jStep = Abc_TtWordNum(jVar);
115 for ( ; pTruth < pLimit; pTruth += jStep )
116 for ( i = 0; i < jStep; i += iStep )
117 for ( j = 0; j < iStep; j++ )
118 pTruth[w++] = pTruth[iStep + i + j];
119 assert( w == (nWords >> 1) );
120 return;
121 }
122}
123
135void Dua_DsdInit( Dua_Dsd_t * pRes, word * pTruth, int nVars )
136{
137 int i;
138 pRes->nSupp = nVars;
139 pRes->nVars = nVars;
140 pRes->nWords = Abc_TtWordNum( nVars );
141 pRes->nObjs = 1;
142 pRes->iRoot = Abc_Var2Lit( 0, 0 );
143 pRes->pObjs[0].Type = 5;
144 pRes->pObjs[0].nFans = nVars;
145 for ( i = 0; i < nVars; i++ )
146 pRes->pObjs[0].pFans[i] = (char)Abc_Var2Lit( i, 0 );
147 memcpy( pRes->pTruth, pTruth, sizeof(word) * pRes->nWords );
148}
149
161// returns 1 if the truth table was complemented
162int Dua_DsdTryConst( word * pTruth, int nVars )
163{
164 if ( !(pTruth[0] & 1) )
165 return 0;
166 Abc_TtNot( pTruth, Abc_TtWordNum(nVars) );
167 return 1;
168}
169int Dua_DsdTryVar( word * pTruth, int nWords, int iVar )
170{
171 int nWordsI = Abc_TtWordNum(iVar);
172 word c0 = (iVar < 6) ? Abc_Tt6Cofactor0( pTruth[0], iVar ) : pTruth[0];
173 word c1 = (iVar < 6) ? Abc_Tt6Cofactor1( pTruth[0], iVar ) : pTruth[nWords];
174 if ( c0 != c1 )
175 {
176 if ( c1 < c0 && c1 < ~c1 ) // flip
177 {
178 Abc_TtFlip( pTruth, nWords, iVar );
179 return 0;
180 }
181 if ( ~c1 < c0 && ~c1 < c1 ) // flip and compl
182 {
183 Abc_TtFlipNot( pTruth, nWords, iVar );
184 return 1;
185 }
186 }
187 if ( iVar < 6 )
188 {
189 word * pLimit = pTruth + nWords;
190 for ( pTruth++; pTruth < pLimit; pTruth++ )
191 {
192 c0 = Abc_Tt6Cofactor0( pTruth[0], iVar );
193 c1 = Abc_Tt6Cofactor1( pTruth[0], iVar );
194 if ( c0 == c1 )
195 continue;
196 if ( c0 < c1 )
197 return 0;
198 for ( ; pTruth < pLimit; pTruth++ )
199 pTruth[0] = Abc_Tt6Flip( pTruth[0], iVar );
200 return 0;
201 }
202 }
203 else
204 {
205 for ( ; pTruth < pLimit; pTruth += (nWordsI << 1) )
206 for ( w = 0; w < nWordsI; w++ )
207 {
208 c0 = pTruth[0];
209 c1 = pTruth[nWordsI];
210 if ( c0 == c1 )
211 continue;
212 if ( c0 < c1 )
213 return 0;
214 for ( ; pTruth < pLimit; pTruth += (nWordsI << 1) )
215 for ( ; w < nWordsI; w++ )
216 ABC_SWAP( word, pTruth[0], pTruth[nWordsI] );
217 return 0;
218 }
219 }
220 assert( 0 );
221 return -1;
222}
223int Dua_DsdCheckCof0Const0( word * pTruth, int nWords, int iVar )
224{
225 if ( nWords == 1 )
226 return (pTruth[0] & s_Truths6Neg[iVar]) == 0;
227 if ( iVar <= 5 )
228 {
229 int w;
230 for ( w = 0; w < nWords; w++ )
231 if ( (pTruth[w] & s_Truths6Neg[iVar]) )
232 return 0;
233 return 1;
234 }
235 else // if ( iVar > 5 )
236 {
237 word * pLimit = pTruth + nWords;
238 int i, iStep = Abc_TtWordNum(iVar);
239 for ( ; pTruth < pLimit; pTruth += (iStep << 1) )
240 for ( i = 0; i < iStep; i++ )
241 if ( pTruth[i] )
242 return 0;
243 return 1;
244 }
245}
246int Dua_DsdCheckCofsEqualNot( word * pTruth, int nWords, int iVar )
247{
248 if ( nWords == 1 )
249 return (pTruth[0] & s_Truths6Neg[iVar]) == ((~pTruth[0] & s_Truths6[iVar]) >> (1 << iVar));
250 if ( iVar <= 5 )
251 {
252 int w, shift = (1 << iVar);
253 for ( w = 0; w < nWords; w++ )
254 if ( (pTruth[w] & s_Truths6Neg[iVar]) != ((~pTruth[w] & s_Truths6[iVar]) >> shift) )
255 return 0;
256 return 1;
257 }
258 else // if ( iVar > 5 )
259 {
260 word * pLimit = pTruth + nWords;
261 int i, iStep = Abc_TtWordNum(iVar);
262 for ( ; pTruth < pLimit; pTruth += (iStep << 1) )
263 for ( i = 0; i < iStep; i++ )
264 if ( pTruth[i] != ~pTruth[i + iStep] )
265 return 0;
266 return 1;
267 }
268}
269int Dua_DsdOneVar( Dua_Dsd_t * pRes )
270{
271 int v, fCompl, fChange = 1;
272 fCompl = Dua_DsdTryConst( pRes->pTruth, pRes->nWords );
273 while ( fChange && pRes->nVars > 2 )
274 {
275 fChange = 0;
276 for ( v = 0; v < pRes->nVars; v++ )
277 {
278 fCompl ^= Dua_DsdTryVar( pRes->pTruth, pRes->nWords, v );
279 if ( Dua_DsdCheckCof0Const0( pRes->pTruth, pRes->nWords, v ) )
280 {
281 fChange = 1;
282 // record AND(v, F)
283 }
284 else if ( Dua_DsdCheckCofsEqualNot( pRes->pTruth, pRes->nWords, v ) )
285 {
286 fChange = 1;
287 // record XOR(v, F)
288 }
289 }
290 }
291 return fCompl;
292}
293
305int Dua_DsdTrySwap( word * pTruth, int nWords, int iVar )
306{
307 static word s_PMasks[5][3] = {
308 { ABC_CONST(0x9999999999999999), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444) },
309 { ABC_CONST(0xC3C3C3C3C3C3C3C3), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030) },
310 { ABC_CONST(0xF00FF00FF00FF00F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00) },
311 { ABC_CONST(0xFF0000FFFF0000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000) },
312 { ABC_CONST(0xFFFF00000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000) }
313 };
314 if ( iVar < 5 )
315 {
316 int Shift = (1 << iVar);
317 word c01, c10, * pLimit = pTruth + nWords;
318 for ( ; pTruth < pLimit; pTruth++ )
319 {
320 c01 = (pTruth[0] & s_PMasks[iVar][1]);
321 c10 = (pTruth[0] & s_PMasks[iVar][2]) >> Shift;
322 if ( c01 == c10 )
323 continue;
324 if ( c01 < c10 )
325 return 0;
326 pTruth[0] = (pTruth[0] & s_PMasks[iVar][0]) | ((pTruth[0] & s_PMasks[iVar][1]) << Shift) | ((pTruth[0] & s_PMasks[iVar][2]) >> Shift);
327 return 1;
328 }
329 }
330 else if ( iVar == 5 )
331 {
332 unsigned * pTruthU = (unsigned *)pTruth;
333 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
334 for ( ; pTruthU < pLimitU; pTruthU += 4 )
335 {
336 c01 = pTruthU[1];
337 c10 = pTruthU[2];
338 if ( c01 == c10 )
339 continue;
340 if ( c01 < c10 )
341 return 0;
342 for ( ; pTruthU < pLimitU; pTruthU += 4 )
343 ABC_SWAP( unsigned, pTruthU[1], pTruthU[2] );
344 return 1;
345 }
346 }
347 else // if ( iVar > 5 )
348 {
349 word * pLimit = pTruth + nWords;
350 int i, iStep = Abc_TtWordNum(iVar);
351 for ( ; pTruth < pLimit; pTruth += 4*iStep )
352 for ( i = 0; i < iStep; i++ )
353 {
354 c01 = pTruth[i + iStep];
355 c10 = pTruth[i + 2*iStep];
356 if ( c01 == c10 )
357 continue;
358 if ( c01 < c10 )
359 return 0;
360 for ( ; pTruth < pLimit; pTruth += 4*iStep )
361 for ( ; i < iStep; i++ )
362 ABC_SWAP( word, pTruth[1], pTruth[2] );
363 return 1;
364 }
365 }
366 return 2;
367}
368int Dua_DsdCheckDecomp( word * pTruth, int nWords, int iVar )
369{
370 static word s_PMasks[5][4] = {
371 { ABC_CONST(0x1111111111111111), ABC_CONST(0x2222222222222222), ABC_CONST(0x4444444444444444), ABC_CONST(0x8888888888888888) },
372 { ABC_CONST(0x0303030303030303), ABC_CONST(0x0C0C0C0C0C0C0C0C), ABC_CONST(0x3030303030303030), ABC_CONST(0xC0C0C0C0C0C0C0C0) },
373 { ABC_CONST(0x000F000F000F000F), ABC_CONST(0x00F000F000F000F0), ABC_CONST(0x0F000F000F000F00), ABC_CONST(0xF000F000F000F000) },
374 { ABC_CONST(0x000000FF000000FF), ABC_CONST(0x0000FF000000FF00), ABC_CONST(0x00FF000000FF0000), ABC_CONST(0xFF000000FF000000) },
375 { ABC_CONST(0x000000000000FFFF), ABC_CONST(0x00000000FFFF0000), ABC_CONST(0x0000FFFF00000000), ABC_CONST(0xFFFF000000000000) }
376 };
377 int fC0eC1 = 1, fC0eC3 = 1;
378 if ( iVar < 5 )
379 {
380 int Shift = (1 << iVar);
381 word c01, c10, * pLimit = pTruth + nWords;
382 for ( ; pTruth < pLimit; pTruth++ )
383 {
384 if ( fC0eC1 && (pTruth[0] & s_PMasks[iVar][0]) != ((pTruth[0] & s_PMasks[iVar][1]) >> Shift) )
385 fC0eC1 = 0;
386 if ( fC0eC3 && (pTruth[0] & s_PMasks[iVar][0]) != ((pTruth[0] & s_PMasks[iVar][3]) >> (3*Shift)) )
387 fC0eC3 = 0;
388 if ( !fC0eC1 && !fC0eC3 )
389 return 0;
390 }
391 }
392 if ( iVar == 5 )
393 {
394 unsigned * pTruthU = (unsigned *)pTruth;
395 unsigned * pLimitU = (unsigned *)(pTruth + nWords);
396 for ( ; pTruthU < pLimitU; pTruthU += 4 )
397 {
398 if ( fC0eC1 && pTruthU[0] != pTruthU[1] )
399 fC0eC1 = 0;
400 if ( fC0eC3 && pTruthU[0] != pTruthU[3] )
401 fC0eC3 = 0;
402 if ( !fC0eC1 && !fC0eC3 )
403 return 0;
404 }
405 }
406 else // if ( iVar > 5 )
407 {
408 word * pLimit = pTruth + nWords;
409 int i, iStep = Abc_TtWordNum(iVar);
410 for ( ; pTruth < pLimit; pTruth += 4*iStep )
411 for ( i = 0; i < iStep; i++ )
412 {
413 if ( fC0eC1 && pTruth[0] != pTruth[1] )
414 fC0eC1 = 0;
415 if ( fC0eC3 && pTruth[0] != pTruth[3] )
416 fC0eC3 = 0;
417 if ( !fC0eC1 && !fC0eC3 )
418 return 0;
419 }
420 }
421 assert( fC0eC1 != fC0eC3 );
422 return fC0eC1 ? 1 : 2;
423}
424
425// returns 1 if decomposition detected
426int Dua_DsdTwoVars( Dua_Dsd_t * pRes )
427{
428 int v, RetValue, fChange = 1;
429 while ( fChange && pRes->nVars > 2 )
430 {
431 fChange = 0;
432 for ( v = 0; v < pRes->nVars - 1; v++ )
433 {
434 RetValue = Dua_DsdTrySwap( pRes->pTruth, pRes->nWords, v );
435 if ( RetValue == 1 )
436 fChange = 1;
437 if ( RetValue != 2 )
438 continue;
439 // vars are symmetric, check decomp
440 RetValue = Dua_DsdCheckDecomp( pRes->pTruth, pRes->nWords, v );
441 if ( RetValue == 0 )
442 continue;
443 if ( RetValue == 1 )
444 {
445 fChange = 1;
446 // record AND(a, b)
447 }
448 else
449 {
450 fChange = 1;
451 // record XOR(a, b)
452 }
453 }
454 }
455}
456
468word Dua_DsdRangeVars( word * pTruth, int nVars, int iVar, int jVar, int fPerform )
469{
470 int Part, nParts = 1 << (nVars - jVar);
471 int Mint, nMints = 1 << (jVar - iVar);
472 word MaskOne, MaskAll = 0;
473 assert( jVar - iVar > 2 );
474 assert( jVar - iVar < 7 );
475 if ( iVar < 6 )
476 {
477 int Shift = 6 - iVar, MaskF = (1 << Shift) - 1, iMint = 0;
478 word MaskFF = (((word)1) << (1 << iVar)) - 1;
479 word Cof0, Cof1, Value;
480 for ( Part = 0; Part < nParts; Part++ )
481 {
482 MaskOne = 0;
483 Cof0 = Cof1 = ~(word)0;
484 for ( Mint = 0; Mint < nMints; Mint++, iMint++ )
485 {
486 Value = (pTruth[iMint>>Shift] >> ((iMint & MaskF)<<iVar)) & MaskFF;
487 if ( !~Cof0 || Cof0 == Value )
488 Cof0 = Value;
489 else if ( !~Cof1 || Cof1 == Value )
490 {
491 Cof1 = Value;
492 MaskOne |= ((word)1) << Mint;
493 }
494 else
495 return 0;
496 }
497 if ( Part == 0 )
498 MaskAll = MaskOne;
499 else if ( MaskAll != MaskOne )
500 return 0;
501 if ( fPerform )
502 {
503 assert( ~Cof0 && ~Cof1 );
504 Mint = 2 * Part;
505 Value = (pTruth[Mint>>Shift] >> ((Mint & MaskF)<<nVarsF)) & MaskFF;
506 pTruth[Mint>>Shift] ^= (Value ^ Cof0) << ((Mint & MaskF)<<nVarsF)
507 Mint = 2 * Part + 1;
508 Value = (pTruth[Mint>>Shift] >> ((Mint & MaskF)<<nVarsF)) & MaskFF;
509 pTruth[Mint>>Shift] ^= (Value ^ Cof1) << ((Mint & MaskF)<<nVarsF)
510 }
511 }
512 // stretch
513 if ( nVars - (jVar - iVar) + 1 < 6 )
514 pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars - (jVar - iVar) + 1 );
515 }
516 else
517 {
518 int nWordsF = Abc_TtWordNum(iVar);
519 int iWord = 0, nBytes = sizeof(word) * nWordsF;
520 word * pCof0, * pCof1;
521 for ( Part = 0; Part < nParts; Part++ )
522 {
523 MaskOne = 0;
524 pCof0 = pCof1 = NULL;
525 for ( Mint = 0; Mint < nMints; Mint++, iWord += nWordsF )
526 {
527 if ( !pCof0 || !memcmp(pCof0, pTruth + iWord, (size_t)nBytes) )
528 pCof0 = pTruth + iWord;
529 else if ( !pCof1 || !memcmp(pCof1, pTruth + iWord, (size_t)nBytes) )
530 {
531 pCof1 = pTruth + iWord;
532 MaskOne |= ((word)1) << Mint;
533 }
534 else
535 return 0;
536 }
537 if ( Part == 0 )
538 MaskAll = MaskOne;
539 else if ( MaskAll != MaskOne )
540 return 0;
541 if ( fPerform )
542 {
543 assert( pCof0 && pCof1 );
544 memcpy( pTruth + (2 * Part + 0) * nWordsF, pCof0, (size_t)nBytes );
545 memcpy( pTruth + (2 * Part + 1) * nWordsF, pCof1, (size_t)nBytes );
546 }
547 }
548 }
549 return MaskAll;
550}
551
563int Dua_DsdRangeVars0( word * pTruth, int nVars, int iVar, int fPerform )
564{
565 int i, nParts = 1 << (nVars - iVar);
566 assert( iVar > 2 && iVar < nVars );
567 if ( iVar == 3 )
568 {
569 unsigned char * pTruthP = (unsigned char *)pTruth, Dfunc = pTruthP[0];
570 for ( i = 1; i < nParts; i++ )
571 if ( pTruthP[i] != Dfunc && pTruthP[i] != ~Dfunc )
572 return 0;
573 }
574 else if ( iVar == 4 )
575 {
576 unsigned short * pTruthP = (unsigned short *)pTruth, Dfunc = pTruthP[0];
577 for ( i = 1; i < nParts; i++ )
578 if ( pTruthP[i] != Dfunc && pTruthP[i] != ~Dfunc )
579 return 0;
580 }
581 else if ( iVar == 5 )
582 {
583 unsigned int * pTruthP = (unsigned int *)pTruth, Dfunc = pTruthP[0];
584 for ( i = 1; i < nParts; i++ )
585 if ( pTruthP[i] != Dfunc && pTruthP[i] != ~Dfunc )
586 return 0;
587 }
588 else
589 {
590 int nStep = 1 << (6 - iVar);
591 assert( iVar >= 6 );
592 for ( i = 1; i < nParts; i++ )
593 if ( !Abc_TtEqual(pTruth, pTruth + i * nStep, nStep) && !Abc_TtEqualNot(pTruth, pTruth + i * nStep, nStep) )
594 return 0;
595 }
596 return 1;
597}
598void Dua_DsdRangeVars0Derive( word * pTruth, int nVars, int iVar )
599{
600 int i, nParts = 1 << (nVars - iVar);
601 assert( iVar > 2 && iVar < nVars );
602 if ( iVar == 3 )
603 {
604 unsigned char * pTruthP = (unsigned char *)pTruth, Dfunc = pTruthP[0];
605 for ( i = 0; i < nParts; i++ )
606 if ( Abc_TtGetBit(pTruth, i) ^ (pTruthP[i] != Dfunc) )
607 Abc_TtXorBit(pTruth, i);
608 }
609 else if ( iVar == 4 )
610 {
611 unsigned short * pTruthP = (unsigned short *)pTruth, Dfunc = pTruthP[0];
612 for ( i = 0; i < nParts; i++ )
613 if ( Abc_TtGetBit(pTruth, i) ^ (pTruthP[i] != Dfunc) )
614 Abc_TtXorBit(pTruth, i);
615 }
616 else if ( iVar == 5 )
617 {
618 unsigned int * pTruthP = (unsigned int *)pTruth, Dfunc = pTruthP[0];
619 for ( i = 0; i < nParts; i++ )
620 if ( Abc_TtGetBit(pTruth, i) ^ (pTruthP[i] != Dfunc) )
621 Abc_TtXorBit(pTruth, i);
622 }
623 else
624 {
625 word Dfunc = pTruth[0];
626 assert( iVar == 6 );
627 for ( i = 0; i < nParts; i++ )
628 if ( Abc_TtGetBit(pTruth, i) ^ (pTruth[i] != Dfunc) )
629 Abc_TtXorBit(pTruth, i);
630 }
631 // stretch
632 if ( nVars - iVar + 1 < 6 )
633 pTruth[0] = Abc_Tt6Stretch( pTruth[0], nVars - iVar + 1 < 6 );
634}
635
647void Dua_DsdTest( word * pTruth, int nVar )
648{
649 Dua_Dsd_t Res, * pRes = &Res;
650 Dua_DsdInit( pRes, pTruth, nVars );
651}
652
656
657
658ABC_NAMESPACE_IMPL_END
659
660
nWords
int nWords
Definition abcNpn.c:127
ABC_SWAP
#define ABC_SWAP(Type, a, b)
Definition abc_global.h:253
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
Dua_DsdTryVar
int Dua_DsdTryVar(word *pTruth, int nWords, int iVar)
Definition dauDsd2.c:169
Dua_DsdRangeVars
word Dua_DsdRangeVars(word *pTruth, int nVars, int iVar, int jVar, int fPerform)
Definition dauDsd2.c:468
Dua_DsdTwoVars
int Dua_DsdTwoVars(Dua_Dsd_t *pRes)
Definition dauDsd2.c:426
Dua_DsdCheckCofsEqualNot
int Dua_DsdCheckCofsEqualNot(word *pTruth, int nWords, int iVar)
Definition dauDsd2.c:246
Dua_Dsd_t
struct Dua_Dsd_t_ Dua_Dsd_t
Definition dauDsd2.c:41
Dua_DsdInit
void Dua_DsdInit(Dua_Dsd_t *pRes, word *pTruth, int nVars)
Definition dauDsd2.c:135
Dua_Obj_t
typedefABC_NAMESPACE_IMPL_START struct Dua_Obj_t_ Dua_Obj_t
DECLARATIONS ///.
Definition dauDsd2.c:33
Dua_DsdOneVar
int Dua_DsdOneVar(Dua_Dsd_t *pRes)
Definition dauDsd2.c:269
Dua_DsdTrySwap
int Dua_DsdTrySwap(word *pTruth, int nWords, int iVar)
Definition dauDsd2.c:305
Dua_DsdRangeVars0Derive
void Dua_DsdRangeVars0Derive(word *pTruth, int nVars, int iVar)
Definition dauDsd2.c:598
Dua_DsdCheckDecomp
int Dua_DsdCheckDecomp(word *pTruth, int nWords, int iVar)
Definition dauDsd2.c:368
Dua_DsdTest
void Dua_DsdTest(word *pTruth, int nVar)
Definition dauDsd2.c:647
Dua_DsdRangeVars0
int Dua_DsdRangeVars0(word *pTruth, int nVars, int iVar, int fPerform)
Definition dauDsd2.c:563
Dua_DsdTryConst
int Dua_DsdTryConst(word *pTruth, int nVars)
Definition dauDsd2.c:162
Dua_DsdCheckCof0Const0
int Dua_DsdCheckCof0Const0(word *pTruth, int nWords, int iVar)
Definition dauDsd2.c:223
word
unsigned __int64 word
DECLARATIONS ///.
Definition kitPerm.c:36
Dua_Dsd_t_
Definition dauDsd2.c:43
Dua_Dsd_t_::nVars
int nVars
Definition dauDsd2.c:45
Dua_Dsd_t_::nWords
int nWords
Definition dauDsd2.c:46
Dua_Dsd_t_::iRoot
int iRoot
Definition dauDsd2.c:48
Dua_Dsd_t_::nSupp
int nSupp
Definition dauDsd2.c:44
Dua_Dsd_t_::nObjs
int nObjs
Definition dauDsd2.c:47
Dua_Dsd_t_::pTruth
word pTruth[DSD_MAX_WRD]
Definition dauDsd2.c:50
Dua_Dsd_t_::pObjs
Dua_Obj_t pObjs[DSD_MAX_VAR]
Definition dauDsd2.c:49
Dua_Obj_t_
Definition dauDsd2.c:35
Dua_Obj_t_::Type
int Type
Definition dauDsd2.c:36
Dua_Obj_t_::pFans
char pFans[DSD_MAX_VAR]
Definition dauDsd2.c:38
Dua_Obj_t_::nFans
int nFans
Definition dauDsd2.c:37
assert
#define assert(ex)
Definition util_old.h:213
memcpy
char * memcpy()
memcmp
int memcmp()