casCore.c 40.7 KB
Newer Older
Alan Mishchenko committed
1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24
/**CFile****************************************************************

  FileName    [casCore.c]

  SystemName  [ABC: Logic synthesis and verification system.]

  PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]

  Synopsis    [Entrance into the implementation.]

  Author      [Alan Mishchenko]
  
  Affiliation [UC Berkeley]

  Date        [Ver. 1.0. Started - Spring 2002.]

  Revision    [$Id: casCore.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $]

***********************************************************************/

#include <stdio.h>
#include <stdlib.h>
#include <string.h>

25 26 27
#include "base/main/main.h"
#include "base/cmd/cmd.h"
#include "misc/extra/extraBdd.h"
Alan Mishchenko committed
28 29
#include "cas.h"

30 31 32
ABC_NAMESPACE_IMPL_START


Alan Mishchenko committed
33 34 35 36 37 38 39 40 41 42 43 44 45 46 47 48 49 50 51 52 53 54 55 56 57 58
////////////////////////////////////////////////////////////////////////
///                      static functions                            ///
////////////////////////////////////////////////////////////////////////

DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose );
DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc );
DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew );

extern int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose );

void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName );

DdNode * Cudd_bddTransferPermute( DdManager * ddSource, DdManager * ddDestination, DdNode * f, int * Permute );

////////////////////////////////////////////////////////////////////////
///                      static varibles                             ///
////////////////////////////////////////////////////////////////////////

//static FILE * pTable = NULL;
//static long s_RemappingTime = 0;

////////////////////////////////////////////////////////////////////////
///                      debugging macros                            ///
////////////////////////////////////////////////////////////////////////

#define PRD(p)       printf( "\nDECOMPOSITION TREE:\n\n" ); PrintDecEntry( (p), 0 ) 
Alan Mishchenko committed
59
#define PRB_(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
Alan Mishchenko committed
60 61 62 63 64 65 66 67 68 69 70 71 72 73 74 75 76 77 78 79 80 81 82 83
#define PRK(f,n)     Cudd_PrintKMap(stdout,dd,(f),Cudd_Not(f),(n),NULL,0); printf( "K-map for function" #f "\n\n" )
#define PRK2(f,g,n)  Cudd_PrintKMap(stdout,dd,(f),(g),(n),NULL,0); printf( "K-map for function <" #f ", " #g ">\n\n" ) 


////////////////////////////////////////////////////////////////////////
///                     EXTERNAL FUNCTIONS                           ///
////////////////////////////////////////////////////////////////////////

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
int Abc_CascadeExperiment( char * pFileGeneric, DdManager * dd, DdNode ** pOutputs, int nInputs, int nOutputs, int nLutSize, int fCheck, int fVerbose )
{
    int i;
    int nVars = nInputs;
    int nOuts = nOutputs;
84
    abctime clk1;
Alan Mishchenko committed
85 86 87 88 89 90 91 92 93 94 95 96 97 98 99 100 101 102 103 104 105 106 107 108 109 110 111 112 113

    int      nVarsEnc;              // the number of additional variables to encode outputs
    DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars

    int      nNames;               // the total number of all inputs
    char *   pNames[MAXINPUTS];     // the temporary storage for the input (and output encoding) names

    DdNode * aFunc;                 // the encoded 0-1 BDD containing all the outputs

    char FileNameIni[100];
    char FileNameFin[100];
    char Buffer[100];

    
//pTable = fopen( "stats.txt", "a+" );
//fprintf( pTable, "%s ", pFileGeneric );
//fprintf( pTable, "%d ", nVars );
//fprintf( pTable, "%d ", nOuts );


    // assign the file names
    strcpy( FileNameIni, pFileGeneric );
    strcat( FileNameIni, "_ENC.blif" );

    strcpy( FileNameFin, pFileGeneric );
    strcat( FileNameFin, "_LUT.blif" );


    // create the variables to encode the outputs
114
    nVarsEnc = Abc_Base2Log( nOuts );
Alan Mishchenko committed
115 116 117 118 119 120 121 122 123 124 125 126 127 128 129 130 131 132 133 134 135 136 137 138 139 140 141 142
    for ( i = 0; i < nVarsEnc; i++ )
        pbVarsEnc[i] = Cudd_bddNewVarAtLevel( dd, i );


    // store the input names
    nNames  = nVars + nVarsEnc;
    for ( i = 0; i < nVars; i++ )
    {
//      pNames[i] = Extra_UtilStrsav( pFunc->pInputNames[i] );
        sprintf( Buffer, "pi%03d", i );
        pNames[i] = Extra_UtilStrsav( Buffer );
    }
    // set the encoding variable name
    for ( ; i < nNames; i++ )
    {       
        sprintf( Buffer, "OutEnc_%02d", i-nVars );
        pNames[i] = Extra_UtilStrsav( Buffer );
    }


    // print the variable order
//  printf( "\n" );
//  printf( "Variable order is: " );
//  for ( i = 0; i < dd->size; i++ )
//      printf( " %d", dd->invperm[i] );
//  printf( "\n" );

    // derive the single-output function
143
    clk1 = Abc_Clock();
Alan Mishchenko committed
144 145 146
    aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose );  Cudd_Ref( aFunc );
//  aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
//  if ( fVerbose )
147
//  printf( "Single-output function computation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
148 149 150 151 152 153 154 155 156 157
 
//fprintf( pTable, "%d ", Cudd_SharingSize( pOutputs, nOutputs ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pOutputs, nOutputs) );

    // dispose of the multiple-output function
//  Extra_Dissolve( pFunc );
 
    // reorder the single output function
//    if ( fVerbose )
//  printf( "Reordering variables...\n");
158
    clk1 = Abc_Clock();
Alan Mishchenko committed
159 160 161 162 163 164 165 166 167 168 169 170
//  if ( fVerbose )
//  printf( "Node count before = %6d\n", Cudd_DagSize( aFunc ) );
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SIFT,1);
    Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
    Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(dd, CUDD_REORDER_SYMM_SIFT,1);
    if ( fVerbose )
    printf( "MTBDD reordered = %6d nodes\n", Cudd_DagSize( aFunc ) );
    if ( fVerbose )
171
    printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
172 173 174 175 176 177 178 179 180
//  printf( "\n" );
//  printf( "Variable order is: " );
//  for ( i = 0; i < dd->size; i++ )
//      printf( " %d", dd->invperm[i] );
//  printf( "\n" );
//fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthMax(dd, aFunc) );

    // write the single-output function into BLIF for verification
181
    clk1 = Abc_Clock();
Alan Mishchenko committed
182 183 184
    if ( fCheck )
    WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
//    if ( fVerbose )
185
//  printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
186 187 188 189

/*
    ///////////////////////////////////////////////////////////////////
    // verification of single output function
190
    clk1 = Abc_Clock();
Alan Mishchenko committed
191 192 193 194 195 196 197 198 199 200 201 202 203 204 205 206 207 208 209 210 211 212 213 214 215 216
    {
        BFunc g_Func;
        DdNode * aRes;

        g_Func.dd = dd;
        g_Func.FileInput = Extra_UtilStrsav(FileNameIni);

        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 

        aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );

        if ( aRes != aFunc )
            printf( "\nVerification FAILED!\n");
        else
            printf( "\nVerification okay!\n");
        
        Cudd_RecursiveDeref( dd, aRes );

        // delocate
        Extra_Dissolve( &g_Func );
    }
217
    printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
218 219 220 221 222 223 224 225 226
    ///////////////////////////////////////////////////////////////////
*/

    if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
        return 0;

/*
    ///////////////////////////////////////////////////////////////////
    // verification of the decomposed LUT network
227
    clk1 = Abc_Clock();
Alan Mishchenko committed
228 229 230 231 232 233 234 235 236 237 238 239 240 241 242 243 244 245 246 247 248 249 250 251 252 253
    {
        BFunc g_Func;
        DdNode * aRes;

        g_Func.dd = dd;
        g_Func.FileInput = Extra_UtilStrsav(FileNameFin);

        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 

        aRes = Cudd_BddToAdd( dd, g_Func.pOutputs[0] );  Cudd_Ref( aRes );

        if ( aRes != aFunc )
            printf( "\nFinal verification FAILED!\n");
        else
            printf( "\nFinal verification okay!\n");
        
        Cudd_RecursiveDeref( dd, aRes );
 
        // delocate 
        Extra_Dissolve( &g_Func );
    }
254
    printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
255 256 257 258 259 260 261 262 263 264 265 266 267 268 269
    ///////////////////////////////////////////////////////////////////
*/
 
    // verify the results
    if ( fCheck )
    {
        char Command[200];
        sprintf( Command, "cec %s %s", FileNameIni, FileNameFin );
        Cmd_CommandExecute( Abc_FrameGetGlobalFrame(), Command );
    }

    Cudd_RecursiveDeref( dd, aFunc );

    // release the names
    for ( i = 0; i < nNames; i++ )
Alan Mishchenko committed
270
        ABC_FREE( pNames[i] );
Alan Mishchenko committed
271 272 273 274 275 276 277 278 279 280 281 282 283 284 285 286 287 288 289 290 291 292 293 294 295 296 297 298 299 300 301 302 303 304 305 306 307 308 309 310 311 312 313 314 315 316 317 318 319 320 321 322 323 324 325 326 327


//fprintf( pTable, "\n" );
//fclose( pTable );

    return 1;
}

#if 0

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void Experiment2( BFunc * pFunc )
{
    int i, x, RetValue;
    int nVars = pFunc->nInputs;
    int nOuts = pFunc->nOutputs;
    DdManager * dd = pFunc->dd;
    long clk1;

//  int      nVarsEnc;              // the number of additional variables to encode outputs
//  DdNode * pbVarsEnc[MAXOUTPUTS]; // the BDDs of the encoding vars

    int      nNames;               // the total number of all inputs
    char *   pNames[MAXINPUTS];     // the temporary storage for the input (and output encoding) names

    DdNode * aFunc;                 // the encoded 0-1 BDD containing all the outputs

    char FileNameIni[100];
    char FileNameFin[100];
    char Buffer[100];

    DdManager * DdNew;

//pTable = fopen( "stats.txt", "a+" );
//fprintf( pTable, "%s ", pFunc->FileGeneric );
//fprintf( pTable, "%d ", nVars );
//fprintf( pTable, "%d ", nOuts );


    // assign the file names
    strcpy( FileNameIni, pFunc->FileGeneric );
    strcat( FileNameIni, "_ENC.blif" );

    strcpy( FileNameFin, pFunc->FileGeneric );
    strcat( FileNameFin, "_LUT.blif" );

    // derive the single-output function IN THE NEW MANAGER
328
    clk1 = Abc_Clock();
Alan Mishchenko committed
329 330
//  aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
    aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew );  Cudd_Ref( aFunc );
331 332
    printf( "Single-output function derivation time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
//  s_RemappingTime = Abc_Clock() - clk1;
Alan Mishchenko committed
333 334 335 336 337 338

    // dispose of the multiple-output function
    Extra_Dissolve( pFunc );

    // reorder the single output function
    printf( "\nReordering variables in the new manager...\n");
339
    clk1 = Abc_Clock();
Alan Mishchenko committed
340 341 342 343 344
    printf( "Node count before = %d\n", Cudd_DagSize( aFunc ) );
//  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SIFT,1);
    Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(DdNew, CUDD_REORDER_SYMM_SIFT,1);
    printf( "Node count after  = %d\n", Cudd_DagSize( aFunc ) );
345
    printf( "Variable reordering time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
346 347 348 349 350 351 352 353 354 355 356 357 358 359 360 361 362
    printf( "\n" );

//fprintf( pTable, "%d ", Cudd_DagSize( aFunc ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthMax(DdNew, aFunc) );


    // create the names to be used with the new manager
    nNames = DdNew->size;
    for ( x = 0; x < nNames; x++ )
    {
        sprintf( Buffer, "v%02d", x );
        pNames[x] = Extra_UtilStrsav( Buffer );
    }



    // write the single-output function into BLIF for verification
363
    clk1 = Abc_Clock();
Alan Mishchenko committed
364
    WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni );
365
    printf( "Single-output function writing time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
366 367 368 369


    ///////////////////////////////////////////////////////////////////
    // verification of single output function
370
    clk1 = Abc_Clock();
Alan Mishchenko committed
371 372 373 374 375 376 377 378 379 380 381 382 383 384 385 386 387 388 389 390 391 392 393 394 395 396
    {
        BFunc g_Func;
        DdNode * aRes;

        g_Func.dd = DdNew;
        g_Func.FileInput = Extra_UtilStrsav(FileNameIni);

        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 

        aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] );  Cudd_Ref( aRes );

        if ( aRes != aFunc )
            printf( "\nVerification FAILED!\n");
        else
            printf( "\nVerification okay!\n");
        
        Cudd_RecursiveDeref( DdNew, aRes );

        // delocate
        Extra_Dissolve( &g_Func );
    }
397
    printf( "Preliminary verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
398 399 400 401 402 403 404 405
    ///////////////////////////////////////////////////////////////////


    CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 );

/*
    ///////////////////////////////////////////////////////////////////
    // verification of the decomposed LUT network
406
    clk1 = Abc_Clock();
Alan Mishchenko committed
407 408 409 410 411 412 413 414 415 416 417 418 419 420 421 422 423 424 425 426 427 428 429 430 431 432
    {
        BFunc g_Func;
        DdNode * aRes;

        g_Func.dd = DdNew;
        g_Func.FileInput = Extra_UtilStrsav(FileNameFin);

        if ( Extra_ReadFile( &g_Func ) == 0 )
        {
            printf( "\nSomething did not work out while reading the input file for verification\n");
            Extra_Dissolve( &g_Func );
            return;
        } 

        aRes = Cudd_BddToAdd( DdNew, g_Func.pOutputs[0] );  Cudd_Ref( aRes );

        if ( aRes != aFunc )
            printf( "\nFinal verification FAILED!\n");
        else
            printf( "\nFinal verification okay!\n");
        
        Cudd_RecursiveDeref( DdNew, aRes );

        // delocate
        Extra_Dissolve( &g_Func );
    }
433
    printf( "Final verification time = %.2f sec\n", (float)(Abc_Clock() - clk1)/(float)(CLOCKS_PER_SEC) );
Alan Mishchenko committed
434 435 436 437 438 439 440 441
    ///////////////////////////////////////////////////////////////////
*/


    Cudd_RecursiveDeref( DdNew, aFunc );

    // release the names
    for ( i = 0; i < nNames; i++ )
Alan Mishchenko committed
442
        ABC_FREE( pNames[i] );
Alan Mishchenko committed
443 444 445 446 447 448 449 450 451 452 453 454 455 456 457 458 459 460 461 462 463


    
    /////////////////////////////////////////////////////////////////////
    // check for remaining references in the package
    RetValue = Cudd_CheckZeroRef( DdNew );
    printf( "\nThe number of referenced nodes in the new manager = %d\n", RetValue );
    Cudd_Quit( DdNew );

//fprintf( pTable, "\n" );
//fclose( pTable );

} 

#endif

////////////////////////////////////////////////////////////////////////
///                       SINGLE OUTPUT FUNCTION                     ///
////////////////////////////////////////////////////////////////////////

// the bit count for the first 256 integer numbers
Alan Mishchenko committed
464 465 466 467 468 469 470 471 472 473
//static unsigned char BitCount8[256] = {
//    0,1,1,2,1,2,2,3,1,2,2,3,2,3,3,4,1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,
//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
//    1,2,2,3,2,3,3,4,2,3,3,4,3,4,4,5,2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,
//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
//    2,3,3,4,3,4,4,5,3,4,4,5,4,5,5,6,3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,
//    3,4,4,5,4,5,5,6,4,5,5,6,5,6,6,7,4,5,5,6,5,6,6,7,5,6,6,7,6,7,7,8
//};
Alan Mishchenko committed
474 475 476 477 478 479 480 481 482 483 484 485 486 487 488 489 490 491 492 493 494 495 496 497 498 499 500 501 502 503 504 505 506 507 508 509 510 511 512 513 514 515 516 517 518 519 520 521 522 523 524 525 526 527 528 529 530 531 532 533 534 535 536 537 538 539 540 541 542 543 544 545 546 547 548 549 550 551 552 553 554 555 556 557 558 559 560 561 562 563 564 565 566 567 568 569 570 571 572 573 574 575 576 577 578 579 580 581 582 583 584 585 586 587 588 589 590 591 592 593 594 595 596 597 598 599 600 601 602 603 604 605 606 607 608 609 610 611 612 613 614 615 616 617 618 619 620 621 622 623 624 625 626 627 628 629 630 631 632 633 634 635 636 637 638 639 640 641 642 643 644 645 646 647 648 649 650 651 652 653 654 655 656 657 658 659 660 661 662 663 664 665 666 667 668 669 670 671 672 673 674 675 676 677 678 679 680 681 682 683 684 685 686 687 688 689 690 691 692 693 694 695 696 697 698 699 700 701 702 703 704 705

/////////////////////////////////////////////////////////////
static int s_SuppSize[MAXOUTPUTS];
int CompareSupports( int *ptrX, int *ptrY )
{
    return ( s_SuppSize[*ptrY] - s_SuppSize[*ptrX] );
}
/////////////////////////////////////////////////////////////

 
/////////////////////////////////////////////////////////////
static int s_MintOnes[MAXOUTPUTS];
int CompareMinterms( int *ptrX, int *ptrY )
{
    return ( s_MintOnes[*ptrY] - s_MintOnes[*ptrX] );
}
/////////////////////////////////////////////////////////////

int GrayCode ( int BinCode )
{ 
  return BinCode ^ ( BinCode >> 1 );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc, int fVerbose )
{
    int i;
    DdNode * bResult, * aResult;
    DdNode * bCube, * bTemp, * bProd;

    int Order[MAXOUTPUTS];
//  int OrderMint[MAXOUTPUTS];
 
    // sort the output according to their support size
    for ( i = 0; i < nOuts; i++ )
    {
        s_SuppSize[i] = Cudd_SupportSize( dd, pbOuts[i] );
//      s_MintOnes[i] = BitCount8[i];
        Order[i]      = i;
//      OrderMint[i]  = i;
    }
    
    // order the outputs
    qsort( (void*)Order,     nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareSupports );
    // order the outputs
//  qsort( (void*)OrderMint, nOuts, sizeof(int), (int(*)(const void*, const void*)) CompareMinterms );


    bResult = b0;   Cudd_Ref( bResult );
    for ( i = 0; i < nOuts; i++ )
    {
//      bCube   = Cudd_bddBitsToCube( dd, OrderMint[i], nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
//      bProd   = Cudd_bddAnd( dd, bCube, pbOuts[Order[nOuts-1-i]] );         Cudd_Ref( bProd );
        bCube   = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc, 1 );   Cudd_Ref( bCube );
        bProd   = Cudd_bddAnd( dd, bCube, pbOuts[Order[i]] );         Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bCube );

        bResult = Cudd_bddOr( dd, bProd, bTemp = bResult );           Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }

    // convert to the ADD
if ( fVerbose )
printf( "Single BDD size = %6d nodes\n", Cudd_DagSize(bResult) );
    aResult = Cudd_BddToAdd( dd, bResult );  Cudd_Ref( aResult );
    Cudd_RecursiveDeref( dd, bResult );
if ( fVerbose )
printf( "MTBDD           = %6d nodes\n", Cudd_DagSize(aResult) );
    Cudd_Deref( aResult );
    return aResult;
}
/*
DdNode * GetSingleOutputFunction( DdManager * dd, DdNode ** pbOuts, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
{
    int i;
    DdNode * bResult, * aResult;
    DdNode * bCube, * bTemp, * bProd;

    bResult = b0;   Cudd_Ref( bResult );
    for ( i = 0; i < nOuts; i++ )
    {
//      bCube   = Extra_bddBitsToCube( dd, i, nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
        bCube   = Extra_bddBitsToCube( dd, nOuts-1-i, nVarsEnc, pbVarsEnc );   Cudd_Ref( bCube );
        bProd   = Cudd_bddAnd( dd, bCube, pbOuts[i] );                Cudd_Ref( bProd );
        Cudd_RecursiveDeref( dd, bCube );

        bResult = Cudd_bddOr( dd, bProd, bTemp = bResult );           Cudd_Ref( bResult );
        Cudd_RecursiveDeref( dd, bTemp );
        Cudd_RecursiveDeref( dd, bProd );
    }

    // conver to the ADD
    aResult = Cudd_BddToAdd( dd, bResult );  Cudd_Ref( aResult );
    Cudd_RecursiveDeref( dd, bResult );

    Cudd_Deref( aResult );
    return aResult;
}
*/


////////////////////////////////////////////////////////////////////////
///                        INPUT REMAPPING                           ///
////////////////////////////////////////////////////////////////////////


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * GetSingleOutputFunctionRemapped( DdManager * dd, DdNode ** pOutputs, int nOuts, DdNode ** pbVarsEnc, int nVarsEnc )
// returns the ADD of the remapped function
{
    static int Permute[MAXINPUTS];
    static DdNode * pRemapped[MAXOUTPUTS];

    DdNode * bSupp, * bTemp;
    int i, Counter;
    DdNode * bFunc;
    DdNode * aFunc;

    Cudd_AutodynDisable(dd);

    // perform the remapping
    for ( i = 0; i < nOuts; i++ )
    {
        // get support
        bSupp = Cudd_Support( dd, pOutputs[i] );    Cudd_Ref( bSupp );

        // create the variable map
        Counter = 0;
        for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
            Permute[bTemp->index] = Counter++;

        // transfer the BDD and remap it
        pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute );  Cudd_Ref( pRemapped[i] );

        // remove support
        Cudd_RecursiveDeref( dd, bSupp );
    }
    
    // perform the encoding
    bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc );   Cudd_Ref( bFunc );

    // convert to ADD
    aFunc = Cudd_BddToAdd( dd, bFunc );  Cudd_Ref( aFunc );
    Cudd_RecursiveDeref( dd, bFunc );

    // deref the intermediate results
    for ( i = 0; i < nOuts; i++ )
        Cudd_RecursiveDeref( dd, pRemapped[i] );

    Cudd_Deref( aFunc );
    return aFunc;
}


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
DdNode * GetSingleOutputFunctionRemappedNewDD( DdManager * dd, DdNode ** pOutputs, int nOuts, DdManager ** DdNew )
// returns the ADD of the remapped function
{
    static int Permute[MAXINPUTS];
    static DdNode * pRemapped[MAXOUTPUTS];

    static DdNode * pbVarsEnc[MAXINPUTS];
    int nVarsEnc;

    DdManager * ddnew;

    DdNode * bSupp, * bTemp;
    int i, v, Counter;
    DdNode * bFunc;

    // these are in the new manager
    DdNode * bFuncNew;
    DdNode * aFuncNew;

    int nVarsMax = 0;

    // perform the remapping and write the DDs into the new manager
    for ( i = 0; i < nOuts; i++ )
    {
        // get support
        bSupp = Cudd_Support( dd, pOutputs[i] );    Cudd_Ref( bSupp );

        // create the variable map
        // to remap the DD into the upper part of the manager
        Counter = 0;
        for ( bTemp = bSupp; bTemp != dd->one; bTemp = cuddT(bTemp) )
            Permute[bTemp->index] = dd->invperm[Counter++];

        // transfer the BDD and remap it
        pRemapped[i] = Cudd_bddPermute( dd, pOutputs[i], Permute );  Cudd_Ref( pRemapped[i] );

        // remove support
        Cudd_RecursiveDeref( dd, bSupp );


        // determine the largest support size
        if ( nVarsMax < Counter )
            nVarsMax = Counter;
    }
    
    // select the encoding variables to follow immediately after the original variables
706
    nVarsEnc = Abc_Base2Log(nOuts);
Alan Mishchenko committed
707 708 709 710 711 712 713 714 715 716 717 718 719 720 721 722 723 724 725 726 727 728 729 730 731 732 733 734 735 736 737 738 739 740 741 742 743 744 745 746 747 748 749 750 751 752 753 754 755 756 757 758 759 760 761 762 763 764 765 766 767 768 769 770 771 772 773 774 775 776 777 778 779 780 781 782 783 784 785 786 787 788 789 790 791 792 793 794 795 796 797 798 799 800 801 802 803 804 805 806 807 808 809 810 811 812 813 814 815 816 817 818 819 820 821 822 823
/*
    for ( v = 0; v < nVarsEnc; v++ )
        if ( nVarsMax + v < dd->size )
            pbVarsEnc[v] = dd->var[ dd->invperm[nVarsMax+v] ];
        else
            pbVarsEnc[v] = Cudd_bddNewVar( dd );
*/
    // create the new variables on top of the manager
    for ( v = 0; v < nVarsEnc; v++ )
        pbVarsEnc[v] = Cudd_bddNewVarAtLevel( dd, v );

//fprintf( pTable, "%d ", Cudd_SharingSize( pRemapped, nOuts ) );
//fprintf( pTable, "%d ", Extra_ProfileWidthSharingMax(dd, pRemapped, nOuts) );


    // perform the encoding
    bFunc = Extra_bddEncodingBinary( dd, pRemapped, nOuts, pbVarsEnc, nVarsEnc );   Cudd_Ref( bFunc );


    // find the cross-manager permutation
    // the variable from the level v in the old manager 
    // should become a variable number v in the new manager
    for ( v = 0; v < nVarsMax + nVarsEnc; v++ )
        Permute[dd->invperm[v]] = v;


    ///////////////////////////////////////////////////////////////////////////////
    // start the new manager
    ddnew = Cudd_Init( nVarsMax + nVarsEnc, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
//  Cudd_AutodynDisable(ddnew);
    Cudd_AutodynEnable(dd, CUDD_REORDER_SYMM_SIFT);

    // transfer it to the new manager
    bFuncNew = Cudd_bddTransferPermute( dd, ddnew, bFunc, Permute );      Cudd_Ref( bFuncNew );
    ///////////////////////////////////////////////////////////////////////////////


    // deref the intermediate results in the old manager
    Cudd_RecursiveDeref( dd, bFunc );
    for ( i = 0; i < nOuts; i++ )
        Cudd_RecursiveDeref( dd, pRemapped[i] );


    ///////////////////////////////////////////////////////////////////////////////
    // convert to ADD in the new manager
    aFuncNew = Cudd_BddToAdd( ddnew, bFuncNew );  Cudd_Ref( aFuncNew );
    Cudd_RecursiveDeref( ddnew, bFuncNew );

    // return the manager
    *DdNew = ddnew;
    ///////////////////////////////////////////////////////////////////////////////

    Cudd_Deref( aFuncNew );
    return aFuncNew;
}

////////////////////////////////////////////////////////////////////////
///                        BLIF WRITING FUNCTIONS                    ///
////////////////////////////////////////////////////////////////////////

void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );


/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void WriteSingleOutputFunctionBlif( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName )
{
    int i;
    FILE * pFile;

    // start the file
    pFile = fopen( FileName, "w" );
    fprintf( pFile, ".model %s\n", FileName );

    fprintf( pFile, ".inputs" );
    for ( i = 0; i < nNames; i++ )
        fprintf( pFile, " %s", pNames[i] );
    fprintf( pFile, "\n" );
    fprintf( pFile, ".outputs F" );
    fprintf( pFile, "\n" );

    // write the DD into the file
    WriteDDintoBLIFfile( pFile, aFunc, "F", "", pNames );

    fprintf( pFile, ".end\n" );
    fclose( pFile );
}

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
// writes the main part of the BLIF file 
// Func is a BDD or a 0-1 ADD to be written
// OutputName is the name of the output
// Prefix is attached to each intermendiate signal to make it unique
// InputNames are the names of the input signals
// (some part of the code is borrowed from Cudd_DumpDot())
{
    int i;
824 825
    st__table * visited;
    st__generator * gen = NULL;
Alan Mishchenko committed
826 827 828 829
    long refAddr, diff, mask;
    DdNode * Node, * Else, * ElseR, * Then;

    /* Initialize symbol table for visited nodes. */
830
    visited = st__init_table( st__ptrcmp, st__ptrhash );
Alan Mishchenko committed
831 832 833 834 835 836 837 838 839 840 841 842 843 844 845 846 847 848

    /* Collect all the nodes of this DD in the symbol table. */
    cuddCollectNodes( Cudd_Regular(Func), visited );

    /* Find how many most significant hex digits are identical
       ** in the addresses of all the nodes. Build a mask based
       ** on this knowledge, so that digits that carry no information
       ** will not be printed. This is done in two steps.
       **  1. We scan the symbol table to find the bits that differ
       **     in at least 2 addresses.
       **  2. We choose one of the possible masks. There are 8 possible
       **     masks for 32-bit integer, and 16 possible masks for 64-bit
       **     integers.
     */

    /* Find the bits that are different. */
    refAddr = ( long )Cudd_Regular(Func);
    diff = 0;
849 850
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
Alan Mishchenko committed
851 852 853
    {
        diff |= refAddr ^ ( long ) Node;
    }
854
    st__free_gen( gen );
Alan Mishchenko committed
855 856 857 858 859 860 861 862 863 864 865 866 867 868 869 870
    gen = NULL;

    /* Choose the mask. */
    for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
    {
        mask = ( 1 << i ) - 1;
        if ( diff <= mask )
            break;
    }


    // write the buffer for the output
    fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(Func) ) / sizeof(DdNode), OutputName ); 
    fprintf( pFile, "%s 1\n", (Cudd_IsComplement(Func))? "0": "1" );


871 872
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
Alan Mishchenko committed
873 874 875 876 877 878 879 880 881 882 883 884 885 886 887 888 889 890 891 892 893 894 895 896 897 898 899 900 901 902 903 904 905 906
    {
        if ( Node->index == CUDD_MAXINDEX )
        {
            // write the terminal node
            fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
            fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
            continue;
        }

        Else  = cuddE(Node);
        ElseR = Cudd_Regular(Else);
        Then  = cuddT(Node);

        assert( InputNames[Node->index] );
        if ( Else == ElseR )
        { // no inverter
            fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],                           
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
        }
        else
        { // inverter
            int * pSlot;
            fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],                         
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );

            // if the inverter is written, skip
907
            if ( ! st__find( visited, (char *)ElseR, (char ***)&pSlot ) )
Alan Mishchenko committed
908 909 910 911 912 913 914 915 916 917 918
                assert( 0 );
            if ( *pSlot )
                continue;
            *pSlot = 1;

            fprintf( pFile, ".names %s%lx %s%lx_i\n",  
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode)   );
            fprintf( pFile, "0 1\n" );
        }
    }
919
    st__free_gen( gen );
Alan Mishchenko committed
920
    gen = NULL;
921
    st__free_table( visited );
Alan Mishchenko committed
922 923 924 925 926 927 928 929 930 931 932 933 934 935 936 937 938 939 940 941 942 943 944 945 946 947 948
}




static DdManager * s_ddmin;

/**Function*************************************************************

  Synopsis    []

  Description []
               
  SideEffects []

  SeeAlso     []

***********************************************************************/
void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames )
// writes the main part of the BLIF file 
// Func is a BDD or a 0-1 ADD to be written
// OutputName is the name of the output
// Prefix is attached to each intermendiate signal to make it unique
// InputNames are the names of the input signals
// (some part of the code is borrowed from Cudd_DumpDot())
{
    int i;
949 950
    st__table * visited;
    st__generator * gen = NULL;
Alan Mishchenko committed
951 952 953 954 955 956
    long refAddr, diff, mask;
    DdNode * Node, * Else, * ElseR, * Then;


    ///////////////////////////////////////////////////////////////
    DdNode * bFmin;
957
    abctime clk1;
Alan Mishchenko committed
958 959 960 961

    if ( s_ddmin == NULL )
        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);

962
    clk1 = Abc_Clock();
Alan Mishchenko committed
963 964 965 966 967 968 969 970 971 972 973 974
    bFmin = Cudd_bddTransfer( dd, s_ddmin, Func );  Cudd_Ref( bFmin );

    // reorder
    printf( "Nodes before = %d.   ", Cudd_DagSize(bFmin) ); 
    Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT,1);
//  Cudd_ReduceHeap(s_ddmin,CUDD_REORDER_SYMM_SIFT_CONV,1);
    printf( "Nodes after  = %d.  \n", Cudd_DagSize(bFmin) ); 
    ///////////////////////////////////////////////////////////////



    /* Initialize symbol table for visited nodes. */
975
    visited = st__init_table( st__ptrcmp, st__ptrhash );
Alan Mishchenko committed
976 977 978 979 980 981 982 983 984 985 986 987 988 989 990 991 992 993

    /* Collect all the nodes of this DD in the symbol table. */
    cuddCollectNodes( Cudd_Regular(bFmin), visited );

    /* Find how many most significant hex digits are identical
       ** in the addresses of all the nodes. Build a mask based
       ** on this knowledge, so that digits that carry no information
       ** will not be printed. This is done in two steps.
       **  1. We scan the symbol table to find the bits that differ
       **     in at least 2 addresses.
       **  2. We choose one of the possible masks. There are 8 possible
       **     masks for 32-bit integer, and 16 possible masks for 64-bit
       **     integers.
     */

    /* Find the bits that are different. */
    refAddr = ( long )Cudd_Regular(bFmin);
    diff = 0;
994 995
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
Alan Mishchenko committed
996 997 998
    {
        diff |= refAddr ^ ( long ) Node;
    }
999
    st__free_gen( gen );
Alan Mishchenko committed
1000 1001 1002 1003 1004 1005 1006 1007 1008 1009 1010 1011 1012 1013 1014 1015
    gen = NULL;

    /* Choose the mask. */
    for ( i = 0; ( unsigned ) i < 8 * sizeof( long ); i += 4 )
    {
        mask = ( 1 << i ) - 1;
        if ( diff <= mask )
            break;
    }


    // write the buffer for the output
    fprintf( pFile, ".names %s%lx %s\n", Prefix, ( mask & (long)Cudd_Regular(bFmin) ) / sizeof(DdNode), OutputName ); 
    fprintf( pFile, "%s 1\n", (Cudd_IsComplement(bFmin))? "0": "1" );


1016 1017
    gen = st__init_gen( visited );
    while ( st__gen( gen, ( const char ** ) &Node, NULL ) )
Alan Mishchenko committed
1018 1019 1020 1021 1022 1023 1024 1025 1026 1027 1028 1029 1030 1031 1032 1033 1034 1035 1036 1037 1038 1039 1040 1041 1042 1043 1044 1045 1046 1047 1048 1049 1050 1051 1052 1053 1054 1055
    {
        if ( Node->index == CUDD_MAXINDEX )
        {
            // write the terminal node
            fprintf( pFile, ".names %s%lx\n", Prefix, ( mask & (long)Node ) / sizeof(DdNode) );
            fprintf( pFile, " %s\n", (cuddV(Node) == 0.0)? "0": "1" );
            continue;
        }

        Else  = cuddE(Node);
        ElseR = Cudd_Regular(Else);
        Then  = cuddT(Node);

        assert( InputNames[Node->index] );
        if ( Else == ElseR )
        { // no inverter
            fprintf( pFile, ".names %s %s%lx %s%lx %s%lx\n", InputNames[Node->index],                           
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );
        }
        else
        { // inverter
            fprintf( pFile, ".names %s %s%lx_i %s%lx %s%lx\n", InputNames[Node->index],                         
                              Prefix, ( mask & (long)ElseR ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Then  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)Node  ) / sizeof(DdNode)   );
            fprintf( pFile, "01- 1\n" );
            fprintf( pFile, "1-1 1\n" );

            fprintf( pFile, ".names %s%lx %s%lx_i\n",  
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode),
                              Prefix, ( mask & (long)ElseR  ) / sizeof(DdNode)   );
            fprintf( pFile, "0 1\n" );
        }
    }
1056
    st__free_gen( gen );
Alan Mishchenko committed
1057
    gen = NULL;
1058
    st__free_table( visited );
Alan Mishchenko committed
1059 1060 1061 1062 1063 1064 1065 1066 1067 1068 1069 1070 1071 1072


    //////////////////////////////////////////////////
    Cudd_RecursiveDeref( s_ddmin, bFmin );
    //////////////////////////////////////////////////
}




////////////////////////////////////////////////////////////////////////
///                    TRANSFER WITH MAPPING                         ///
////////////////////////////////////////////////////////////////////////
static DdNode * cuddBddTransferPermuteRecur
1073
ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st__table * table, int * Permute ));
Alan Mishchenko committed
1074 1075 1076 1077 1078 1079 1080 1081 1082 1083 1084 1085 1086 1087 1088 1089 1090 1091 1092 1093 1094 1095 1096 1097 1098 1099 1100 1101 1102 1103 1104 1105 1106 1107 1108 1109 1110 1111 1112 1113 1114 1115 1116 1117 1118 1119 1120 1121 1122 1123 1124 1125 1126 1127 1128 1129 1130

static DdNode * cuddBddTransferPermute
ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute));

/**Function********************************************************************

  Synopsis    [Convert a BDD from a manager to another one.]

  Description [Convert a BDD from a manager to another one. The orders of the
  variables in the two managers may be different. Returns a
  pointer to the BDD in the destination manager if successful; NULL
  otherwise. The i-th entry in the array Permute tells what is the index
  of the i-th variable from the old manager in the new manager.]

  SideEffects [None]

  SeeAlso     []

******************************************************************************/
DdNode *
Cudd_bddTransferPermute( DdManager * ddSource,
                  DdManager * ddDestination, DdNode * f, int * Permute )
{
    DdNode *res;
    do
    {
        ddDestination->reordered = 0;
        res = cuddBddTransferPermute( ddSource, ddDestination, f, Permute );
    }
    while ( ddDestination->reordered == 1 );
    return ( res );

}                               /* end of Cudd_bddTransferPermute */


/*---------------------------------------------------------------------------*/
/* Definition of internal functions                                          */
/*---------------------------------------------------------------------------*/


/**Function********************************************************************

  Synopsis    [Convert a BDD from a manager to another one.]

  Description [Convert a BDD from a manager to another one. Returns a
  pointer to the BDD in the destination manager if successful; NULL
  otherwise.]

  SideEffects [None]

  SeeAlso     [Cudd_bddTransferPermute]

******************************************************************************/
DdNode *
cuddBddTransferPermute( DdManager * ddS, DdManager * ddD, DdNode * f, int * Permute )
{
    DdNode *res;
1131 1132
    st__table *table = NULL;
    st__generator *gen = NULL;
Alan Mishchenko committed
1133 1134
    DdNode *key, *value;

1135
    table = st__init_table( st__ptrcmp, st__ptrhash );
Alan Mishchenko committed
1136 1137 1138 1139 1140 1141 1142 1143 1144
    if ( table == NULL )
        goto failure;
    res = cuddBddTransferPermuteRecur( ddS, ddD, f, table, Permute );
    if ( res != NULL )
        cuddRef( res );

    /* Dereference all elements in the table and dispose of the table.
       ** This must be done also if res is NULL to avoid leaks in case of
       ** reordering. */
1145
    gen = st__init_gen( table );
Alan Mishchenko committed
1146 1147
    if ( gen == NULL )
        goto failure;
1148
    while ( st__gen( gen, ( const char ** ) &key, ( char ** ) &value ) )
Alan Mishchenko committed
1149 1150 1151
    {
        Cudd_RecursiveDeref( ddD, value );
    }
1152
    st__free_gen( gen );
Alan Mishchenko committed
1153
    gen = NULL;
1154
    st__free_table( table );
Alan Mishchenko committed
1155 1156 1157 1158 1159 1160 1161 1162
    table = NULL;

    if ( res != NULL )
        cuddDeref( res );
    return ( res );

  failure:
    if ( table != NULL )
1163
        st__free_table( table );
Alan Mishchenko committed
1164
    if ( gen != NULL )
1165
        st__free_gen( gen );
Alan Mishchenko committed
1166 1167 1168 1169 1170 1171 1172 1173 1174 1175 1176 1177 1178 1179 1180 1181 1182 1183 1184
    return ( NULL );

}                               /* end of cuddBddTransferPermute */


/**Function********************************************************************

  Synopsis    [Performs the recursive step of Cudd_bddTransferPermute.]

  Description [Performs the recursive step of Cudd_bddTransferPermute.
  Returns a pointer to the result if successful; NULL otherwise.]

  SideEffects [None]

  SeeAlso     [cuddBddTransferPermute]

******************************************************************************/
static DdNode *
cuddBddTransferPermuteRecur( DdManager * ddS,
1185
                      DdManager * ddD, DdNode * f, st__table * table, int * Permute )
Alan Mishchenko committed
1186 1187 1188 1189 1190 1191 1192 1193 1194 1195 1196 1197 1198 1199 1200 1201 1202 1203 1204
{
    DdNode *ft, *fe, *t, *e, *var, *res;
    DdNode *one, *zero;
    int index;
    int comple = 0;

    statLine( ddD );
    one = DD_ONE( ddD );
    comple = Cudd_IsComplement( f );

    /* Trivial cases. */
    if ( Cudd_IsConstant( f ) )
        return ( Cudd_NotCond( one, comple ) );

    /* Make canonical to increase the utilization of the cache. */
    f = Cudd_NotCond( f, comple );
    /* Now f is a regular pointer to a non-constant node. */

    /* Check the cache. */
1205
    if ( st__lookup( table, ( char * ) f, ( char ** ) &res ) )
Alan Mishchenko committed
1206 1207 1208 1209 1210 1211 1212 1213 1214 1215 1216 1217 1218 1219 1220 1221 1222 1223 1224 1225 1226 1227 1228 1229 1230 1231 1232 1233 1234 1235 1236 1237 1238 1239 1240 1241 1242 1243 1244 1245 1246
        return ( Cudd_NotCond( res, comple ) );

    /* Recursive step. */
    index = Permute[f->index];
    ft = cuddT( f );
    fe = cuddE( f );

    t = cuddBddTransferPermuteRecur( ddS, ddD, ft, table, Permute );
    if ( t == NULL )
    {
        return ( NULL );
    }
    cuddRef( t );

    e = cuddBddTransferPermuteRecur( ddS, ddD, fe, table, Permute );
    if ( e == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        return ( NULL );
    }
    cuddRef( e );

    zero = Cudd_Not( one );
    var = cuddUniqueInter( ddD, index, one, zero );
    if ( var == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        Cudd_RecursiveDeref( ddD, e );
        return ( NULL );
    }
    res = cuddBddIteRecur( ddD, var, t, e );
    if ( res == NULL )
    {
        Cudd_RecursiveDeref( ddD, t );
        Cudd_RecursiveDeref( ddD, e );
        return ( NULL );
    }
    cuddRef( res );
    Cudd_RecursiveDeref( ddD, t );
    Cudd_RecursiveDeref( ddD, e );

1247 1248
    if ( st__add_direct( table, ( char * ) f, ( char * ) res ) ==
         st__OUT_OF_MEM )
Alan Mishchenko committed
1249 1250 1251 1252 1253 1254 1255 1256 1257 1258 1259 1260 1261 1262 1263
    {
        Cudd_RecursiveDeref( ddD, res );
        return ( NULL );
    }
    return ( Cudd_NotCond( res, comple ) );

}                               /* end of cuddBddTransferPermuteRecur */

////////////////////////////////////////////////////////////////////////
///                           END OF FILE                            ///
////////////////////////////////////////////////////////////////////////




1264 1265
ABC_NAMESPACE_IMPL_END