Version abc80130

88 files changed, 174 insertions, 2817 deletions

diff --git a/src/bdd/cas/cas.h b/src/bdd/cas/cas.h
deleted file mode 100644
index fcc9f890..00000000
--- a/src/bdd/cas/cas.h
+++ /dev/null
@@ -1,62 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [cas.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: cas.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __CAS_H__
-#define __CAS_H__
-
-#ifdef __cplusplus
-extern "C" {
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-#define MAXINPUTS   1024
-#define MAXOUTPUTS  1024
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== zzz.c ==========================================================*/
- 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/bdd/cas/casCore.c b/src/bdd/cas/casCore.c
deleted file mode 100644
index 579235b1..00000000
--- a/src/bdd/cas/casCore.c
+++ /dev/null
@@ -1,1263 +0,0 @@
-/**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>
-#include <time.h>
-
-#include "extra.h"
-#include "cas.h"
-
-////////////////////////////////////////////////////////////////////////
-///                      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 ) 
-#define PRB(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
-#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;
-    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];
-
-    
-//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
-    nVarsEnc = Extra_Base2Log( nOuts );
-    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
-    clk1 = clock();
-    aFunc = GetSingleOutputFunction( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc, fVerbose );  Cudd_Ref( aFunc );
-//  aFunc = GetSingleOutputFunctionRemapped( dd, pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
-//  if ( fVerbose )
-//  printf( "Single-output function computation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
- 
-//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");
-    clk1 = clock();
-//  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 )
-    printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-//  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
-    clk1 = clock();
-    if ( fCheck )
-    WriteSingleOutputFunctionBlif( dd, aFunc, pNames, nNames, FileNameIni );
-//    if ( fVerbose )
-//  printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-
-/*
-    ///////////////////////////////////////////////////////////////////
-    // verification of single output function
-    clk1 = clock();
-    {
-        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 );
-    }
-    printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    ///////////////////////////////////////////////////////////////////
-*/
-
-    if ( !CreateDecomposedNetwork( dd, aFunc, pNames, nNames, FileNameFin, nLutSize, fCheck, fVerbose ) )
-        return 0;
-
-/*
-    ///////////////////////////////////////////////////////////////////
-    // verification of the decomposed LUT network
-    clk1 = clock();
-    {
-        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 );
-    }
-    printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    ///////////////////////////////////////////////////////////////////
-*/
- 
-    // verify the results
-    if ( fCheck )
-    {
-        extern int Cmd_CommandExecute( void * pAbc, char * sCommand );
-        extern void * Abc_FrameGetGlobalFrame();
-        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++ )
-        free( pNames[i] );
-
-
-//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
-    clk1 = clock();
-//  aFunc = GetSingleOutputFunction( dd, pFunc->pOutputs, nOuts, pbVarsEnc, nVarsEnc );  Cudd_Ref( aFunc );
-    aFunc = GetSingleOutputFunctionRemappedNewDD( dd, pFunc->pOutputs, nOuts, &DdNew );  Cudd_Ref( aFunc );
-    printf( "Single-output function derivation time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-//  s_RemappingTime = clock() - clk1;
-
-    // dispose of the multiple-output function
-    Extra_Dissolve( pFunc );
-
-    // reorder the single output function
-    printf( "\nReordering variables in the new manager...\n");
-    clk1 = clock();
-    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 ) );
-    printf( "Variable reordering time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    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
-    clk1 = clock();
-    WriteSingleOutputFunctionBlif( DdNew, aFunc, pNames, nNames, FileNameIni );
-    printf( "Single-output function writing time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-
-
-    ///////////////////////////////////////////////////////////////////
-    // verification of single output function
-    clk1 = clock();
-    {
-        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 );
-    }
-    printf( "Preliminary verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    ///////////////////////////////////////////////////////////////////
-
-
-    CreateDecomposedNetwork( DdNew, aFunc, pNames, nNames, FileNameFin, nLutSize, 0 );
-
-/*
-    ///////////////////////////////////////////////////////////////////
-    // verification of the decomposed LUT network
-    clk1 = clock();
-    {
-        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 );
-    }
-    printf( "Final verification time = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    ///////////////////////////////////////////////////////////////////
-*/
-
-
-    Cudd_RecursiveDeref( DdNew, aFunc );
-
-    // release the names
-    for ( i = 0; i < nNames; i++ )
-        free( pNames[i] );
-
-
-    
-    /////////////////////////////////////////////////////////////////////
-    // 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
-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
-};
-
-/////////////////////////////////////////////////////////////
-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;
-    int nSuppPrev = -1;
-    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;
-    int nSuppPrev = -1;
-    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
-    nVarsEnc = Extra_Base2Log(nOuts);
-/*
-    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;
-    st_table * visited;
-    st_generator * gen = NULL;
-    long refAddr, diff, mask;
-    DdNode * Node, * Else, * ElseR, * Then;
-
-    /* Initialize symbol table for visited nodes. */
-    visited = st_init_table( st_ptrcmp, st_ptrhash );
-
-    /* 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;
-    gen = st_init_gen( visited );
-    while ( st_gen( gen, ( char ** ) &Node, NULL ) )
-    {
-        diff |= refAddr ^ ( long ) Node;
-    }
-    st_free_gen( gen );
-    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" );
-
-
-    gen = st_init_gen( visited );
-    while ( st_gen( gen, ( char ** ) &Node, NULL ) )
-    {
-        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
-            if ( !st_find( visited, (char *)ElseR, (char ***)&pSlot ) )
-                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" );
-        }
-    }
-    st_free_gen( gen );
-    gen = NULL;
-    st_free_table( visited );
-}
-
-
-
-
-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;
-    st_table * visited;
-    st_generator * gen = NULL;
-    long refAddr, diff, mask;
-    DdNode * Node, * Else, * ElseR, * Then;
-
-
-    ///////////////////////////////////////////////////////////////
-    DdNode * bFmin;
-    int clk1;
-
-    if ( s_ddmin == NULL )
-        s_ddmin = Cudd_Init( dd->size, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0);
-
-    clk1 = clock();
-    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. */
-    visited = st_init_table( st_ptrcmp, st_ptrhash );
-
-    /* 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;
-    gen = st_init_gen( visited );
-    while ( st_gen( gen, ( char ** ) &Node, NULL ) )
-    {
-        diff |= refAddr ^ ( long ) Node;
-    }
-    st_free_gen( gen );
-    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" );
-
-
-    gen = st_init_gen( visited );
-    while ( st_gen( gen, ( char ** ) &Node, NULL ) )
-    {
-        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" );
-        }
-    }
-    st_free_gen( gen );
-    gen = NULL;
-    st_free_table( visited );
-
-
-    //////////////////////////////////////////////////
-    Cudd_RecursiveDeref( s_ddmin, bFmin );
-    //////////////////////////////////////////////////
-}
-
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                    TRANSFER WITH MAPPING                         ///
-////////////////////////////////////////////////////////////////////////
-static DdNode * cuddBddTransferPermuteRecur
-ARGS((DdManager * ddS, DdManager * ddD, DdNode * f, st_table * table, int * Permute ));
-
-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;
-    st_table *table = NULL;
-    st_generator *gen = NULL;
-    DdNode *key, *value;
-
-    table = st_init_table( st_ptrcmp, st_ptrhash );
-    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. */
-    gen = st_init_gen( table );
-    if ( gen == NULL )
-        goto failure;
-    while ( st_gen( gen, ( char ** ) &key, ( char ** ) &value ) )
-    {
-        Cudd_RecursiveDeref( ddD, value );
-    }
-    st_free_gen( gen );
-    gen = NULL;
-    st_free_table( table );
-    table = NULL;
-
-    if ( res != NULL )
-        cuddDeref( res );
-    return ( res );
-
-  failure:
-    if ( table != NULL )
-        st_free_table( table );
-    if ( gen != NULL )
-        st_free_gen( gen );
-    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,
-                      DdManager * ddD, DdNode * f, st_table * table, int * Permute )
-{
-    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. */
-    if ( st_lookup( table, ( char * ) f, ( char ** ) &res ) )
-        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 );
-
-    if ( st_add_direct( table, ( char * ) f, ( char * ) res ) ==
-         ST_OUT_OF_MEM )
-    {
-        Cudd_RecursiveDeref( ddD, res );
-        return ( NULL );
-    }
-    return ( Cudd_NotCond( res, comple ) );
-
-}                               /* end of cuddBddTransferPermuteRecur */
-
-////////////////////////////////////////////////////////////////////////
-///                           END OF FILE                            ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-
diff --git a/src/bdd/cas/casDec.c b/src/bdd/cas/casDec.c
deleted file mode 100644
index a1eb5f36..00000000
--- a/src/bdd/cas/casDec.c
+++ /dev/null
@@ -1,508 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [casDec.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [CASCADE: Decomposition of shared BDDs into a LUT cascade.]
-
-  Synopsis    [BDD-based decomposition with encoding.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - Spring 2002.]
-
-  Revision    [$Id: casDec.c,v 1.0 2002/01/01 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include <stdio.h>
-#include <string.h>
-#include <stdlib.h>
-#include <time.h>
-
-#include "extra.h"
-#include "cas.h"
-
-////////////////////////////////////////////////////////////////////////
-///                      type definitions                            ///
-////////////////////////////////////////////////////////////////////////
-
-typedef struct
-{
-    int nIns;                // the number of LUT variables
-    int nInsP;               // the number of inputs coming from the previous LUT
-    int nCols;               // the number of columns in this LUT
-    int nMulti;              // the column multiplicity, [log2(nCols)]
-    int nSimple;             // the number of outputs implemented as direct connections to inputs of the previous block
-    int Level;               // the starting level in the ADD in this LUT
-
-//  DdNode ** pbVarsIn[32];  // the BDDs of the elementary input variables
-//  DdNode ** pbVarsOut[32]; // the BDDs of the elementary output variables 
-
-//  char * pNamesIn[32];     // the names of input variables
-//  char * pNamesOut[32];    // the names of output variables
-
-    DdNode ** pbCols;        // the array of columns represented by BDDs
-    DdNode ** pbCodes;       // the array of codes (in terms of pbVarsOut)
-    DdNode ** paNodes;       // the array of starting ADD nodes on the next level (also referenced)
-
-    DdNode * bRelation;      // the relation after encoding
-
-    // the relation depends on the three groups of variables:
-    // (1) variables on top represent the outputs of the previous cascade
-    // (2) variables in the middle represent the primary inputs
-    // (3) variables below (CVars) represent the codes
-    //
-    // the replacement is done after computing the relation
-} LUT;
-
-
-////////////////////////////////////////////////////////////////////////
-///                      static functions                            ///
-////////////////////////////////////////////////////////////////////////
-
-// the LUT-2-BLIF writing function
-void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName );
-
-// the function to write a DD (BDD or ADD) as a network of MUXES
-extern void WriteDDintoBLIFfile( FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
-extern void WriteDDintoBLIFfileReorder( DdManager * dd, FILE * pFile, DdNode * Func, char * OutputName, char * Prefix, char ** InputNames );
-
-////////////////////////////////////////////////////////////////////////
-///                      static varibles                             ///
-////////////////////////////////////////////////////////////////////////
-
-static int s_LutSize = 15;
-static int s_nFuncVars; 
-
-long s_EncodingTime;
-
-long s_EncSearchTime;
-long s_EncComputeTime;
-
-////////////////////////////////////
-// temporary output variables
-//FILE * pTable;
-//long s_ReadingTime;
-//long s_RemappingTime;
-////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      debugging macros                            ///
-////////////////////////////////////////////////////////////////////////
-
-#define PRB(f)       printf( #f " = " ); Cudd_bddPrint(dd,f); printf( "\n" )
-#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                           ///
-////////////////////////////////////////////////////////////////////////
-
-int CreateDecomposedNetwork( DdManager * dd, DdNode * aFunc, char ** pNames, int nNames, char * FileName, int nLutSize, int fCheck, int fVerbose )
-// aFunc is a 0-1 ADD for the given function
-// pNames (nNames) are the input variable names
-// FileName is the name of the output file for the LUT network
-// dynamic variable reordering should be disabled when this function is running
-{
-    static LUT * pLuts[MAXINPUTS];   // the LUT cascade
-    static int Profile[MAXINPUTS];   // the profile filled in with the info about the BDD width
-    static int Permute[MAXINPUTS];   // the array to store a temporary permutation of variables
-
-    LUT * p;               // the current LUT
-    int i, v;
-
-    DdNode * bCVars[32];   // these are variables for the codes
-
-    int nVarsRem;          // the number of remaining variables
-    int PrevMulti;         // column multiplicity on the previous level
-    int fLastLut;          // flag to signal the last LUT
-    int nLuts;
-    int nLutsTotal = 0;
-    int nLutOutputs = 0;
-    int nLutOutputsOrig = 0;
-
-    long clk1;
-
-    s_LutSize = nLutSize;
-
-    s_nFuncVars = nNames;
-
-    // get the profile
-    clk1 = clock();
-    Extra_ProfileWidth( dd, aFunc, Profile, -1 );
-
-
-//  for ( v = 0; v < nNames; v++ )
-//      printf( "Level = %2d, Width = %2d\n", v+1, Profile[v] );
-
-
-//printf( "\n" );
-
-    // mark-up the LUTs
-    // assuming that the manager has exactly nNames vars (new vars have not been introduced yet)
-    nVarsRem  = nNames;     // the number of remaining variables
-    PrevMulti = 0;          // column multiplicity on the previous level
-    fLastLut  = 0;
-    nLuts     = 0;
-    do
-    {
-        p = (LUT*) malloc( sizeof(LUT) );
-        memset( p, 0, sizeof(LUT) );
-
-        if ( nVarsRem + PrevMulti <= s_LutSize ) // this is the last LUT
-        {
-            p->nIns   = nVarsRem + PrevMulti;
-            p->nInsP  = PrevMulti;
-            p->nCols  = 2;
-            p->nMulti = 1;
-            p->Level  = nNames-nVarsRem;
-
-            nVarsRem  = 0;
-            PrevMulti = 1;
-
-            fLastLut  = 1;
-        }
-        else // this is not the last LUT
-        {
-            p->nIns   = s_LutSize;
-            p->nInsP  = PrevMulti;
-            p->nCols  = Profile[nNames-(nVarsRem-(s_LutSize-PrevMulti))];
-            p->nMulti = Extra_Base2Log(p->nCols);
-            p->Level  = nNames-nVarsRem;
-
-            nVarsRem  = nVarsRem-(s_LutSize-PrevMulti);
-            PrevMulti = p->nMulti;
-        }
-        
-        if ( p->nMulti >= s_LutSize )
-        {
-            printf( "The LUT size is too small\n" );
-            return 0;
-        }
-
-        nLutOutputsOrig += p->nMulti;
-
-
-//if ( fVerbose )
-//printf( "Stage %2d: In = %3d, InP = %3d, Cols = %5d, Multi = %2d, Level = %2d\n", 
-//       nLuts+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->Level );
-
-
-        // there should be as many columns, codes, and nodes, as there are columns on this level
-        p->pbCols  = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-        p->pbCodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-        p->paNodes = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-
-        pLuts[nLuts] = p;
-        nLuts++;
-    }
-    while ( !fLastLut );
-
-
-//if ( fVerbose )
-//printf( "The number of cascades = %d\n", nLuts );
-
-
-//fprintf( pTable, "%d ", nLuts );
-
-
-    // add the new variables at the bottom
-    for ( i = 0; i < s_LutSize; i++ )
-        bCVars[i] = Cudd_bddNewVar(dd);
-
-    // for each LUT - assign the LUT and encode the columns
-    s_EncodingTime = 0;
-    for ( i = 0; i < nLuts; i++ )
-    {
-        int RetValue;
-        DdNode * bVars[32];    
-        int nVars;
-        DdNode * bVarsInCube;
-        DdNode * bVarsCCube;
-        DdNode * bVarsCube;
-        int CutLevel;
-
-        p = pLuts[i];
-
-        // compute the columns of this LUT starting from the given set of nodes with the given codes
-        // (these codes have been remapped to depend on the topmost variables in the manager)
-        // for the first LUT, start with the constant 1 BDD
-        CutLevel = p->Level + p->nIns - p->nInsP;
-        if ( i == 0 )
-            RetValue = Extra_bddNodePathsUnderCutArray( 
-                            dd, &aFunc, &(b1), 1, 
-                            p->paNodes, p->pbCols, CutLevel );
-        else
-            RetValue = Extra_bddNodePathsUnderCutArray( 
-                            dd, pLuts[i-1]->paNodes, pLuts[i-1]->pbCodes, pLuts[i-1]->nCols, 
-                            p->paNodes, p->pbCols, CutLevel );
-        assert( RetValue == p->nCols );
-        // at this point, we have filled out p->paNodes[] and p->pbCols[] of this LUT
-        // pLuts[i-1]->paNodes depended on normal vars
-        // pLuts[i-1]->pbCodes depended on the topmost variables 
-        // the resulting p->paNodes depend on normal ADD nodes
-        // the resulting p->pbCols depend on normal vars and topmost variables in the manager
-
-        // perform the encoding
-
-        // create the cube of these variables
-        // collect the topmost variables of the manager
-        nVars = p->nInsP;
-        for ( v = 0; v < nVars; v++ )
-            bVars[v] = dd->vars[ dd->invperm[v] ];
-        bVarsCCube  = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 );    Cudd_Ref( bVarsCCube );
-
-        // collect the primary input variables involved in this LUT
-        nVars = p->nIns - p->nInsP;
-        for ( v = 0; v < nVars; v++ )
-            bVars[v] = dd->vars[ dd->invperm[p->Level+v] ];
-        bVarsInCube = Extra_bddBitsToCube( dd, (1<<nVars)-1, nVars, bVars, 1 );    Cudd_Ref( bVarsInCube );
-
-        // get the cube
-        bVarsCube   = Cudd_bddAnd( dd, bVarsInCube, bVarsCCube );              Cudd_Ref( bVarsCube );
-        Cudd_RecursiveDeref( dd, bVarsInCube );
-        Cudd_RecursiveDeref( dd, bVarsCCube );
-
-        // get the encoding relation
-        if ( i == nLuts -1 )
-        {
-            DdNode * bVar;
-            assert( p->nMulti == 1 );
-            assert( p->nCols == 2 );
-            assert( Cudd_IsConstant( p->paNodes[0] ) );
-            assert( Cudd_IsConstant( p->paNodes[1] ) );
-
-            bVar = ( p->paNodes[0] == a1 )? bCVars[0]: Cudd_Not( bCVars[0] );
-            p->bRelation = Cudd_bddIte( dd, bVar, p->pbCols[0], p->pbCols[1] );  Cudd_Ref( p->bRelation );
-        }
-        else
-        {
-            long clk2 = clock();
-//          p->bRelation = PerformTheEncoding( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
-            p->bRelation = Extra_bddEncodingNonStrict( dd, p->pbCols, p->nCols, bVarsCube, bCVars, p->nMulti, &p->nSimple );  Cudd_Ref( p->bRelation );
-            s_EncodingTime += clock() - clk2;
-        }
-
-        // update the number of LUT outputs
-        nLutOutputs += (p->nMulti - p->nSimple);
-        nLutsTotal += p->nMulti;
-
-//if ( fVerbose )
-//printf( "Stage %2d: Simple = %d\n", i+1, p->nSimple );
-
-if ( fVerbose )
-printf( "Stage %3d: In = %3d  InP = %3d  Cols = %5d  Multi = %2d  Simple = %2d  Level = %3d\n", 
-       i+1, p->nIns, p->nInsP, p->nCols, p->nMulti, p->nSimple, p->Level );
-
-        // get the codes from the relation (these are not necessarily cubes)
-        {
-            int c;
-            for ( c = 0; c < p->nCols; c++ )
-            {
-                p->pbCodes[c] = Cudd_bddAndAbstract( dd, p->bRelation, p->pbCols[c], bVarsCube ); Cudd_Ref( p->pbCodes[c] );
-            }
-        }
-
-        Cudd_RecursiveDeref( dd, bVarsCube );
-
-        // remap the codes to depend on the topmost varibles of the manager
-        // useful as a preparation for the next step
-        {
-            DdNode ** pbTemp;
-            int k, v;
-
-            pbTemp = (DdNode **) malloc( p->nCols * sizeof(DdNode *) );
-
-            // create the identical permutation
-            for ( v = 0; v < dd->size; v++ )
-                Permute[v] = v;
-
-            // use the topmost variables of the manager 
-            // to represent the previous level codes
-            for ( v = 0; v < p->nMulti; v++ )
-                Permute[bCVars[v]->index] = dd->invperm[v];
-
-            Extra_bddPermuteArray( dd, p->pbCodes, pbTemp, p->nCols, Permute );
-            // the array pbTemp comes already referenced
-
-            // deref the old codes and assign the new ones
-            for ( k = 0; k < p->nCols; k++ )
-            {
-                Cudd_RecursiveDeref( dd, p->pbCodes[k] );
-                p->pbCodes[k] = pbTemp[k];
-            }
-            free( pbTemp );
-        }
-    } 
-    if ( fVerbose )
-    printf( "LUTs: Total = %5d. Final = %5d. Simple = %5d. (%6.2f %%)  ", 
-        nLutsTotal, nLutOutputs, nLutsTotal-nLutOutputs, 100.0*(nLutsTotal-nLutOutputs)/nLutsTotal );
-    if ( fVerbose )
-    printf( "Memory = %6.2f Mb\n", 1.0*nLutOutputs*(1<<nLutSize)/(1<<20) );
-//  printf( "\n" );
-
-//fprintf( pTable, "%d ", nLutOutputsOrig );
-//fprintf( pTable, "%d ", nLutOutputs );
-
-    if ( fVerbose )
-    {
-    printf( "Pure decomposition time   = %.2f sec\n", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
-    printf( "Encoding time             = %.2f sec\n", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
-//  printf( "Encoding search time      = %.2f sec\n", (float)(s_EncSearchTime)/(float)(CLOCKS_PER_SEC) );
-//  printf( "Encoding compute time     = %.2f sec\n", (float)(s_EncComputeTime)/(float)(CLOCKS_PER_SEC) );
-    }
-
-
-//fprintf( pTable, "%.2f ", (float)(s_ReadingTime)/(float)(CLOCKS_PER_SEC) );
-//fprintf( pTable, "%.2f ", (float)(clock() - clk1 - s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
-//fprintf( pTable, "%.2f ", (float)(s_EncodingTime)/(float)(CLOCKS_PER_SEC) );
-//fprintf( pTable, "%.2f ", (float)(s_RemappingTime)/(float)(CLOCKS_PER_SEC) );
-
-
-    // write LUTs into the BLIF file
-    clk1 = clock();
-    if ( fCheck )
-    {
-        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
-        WriteLUTSintoBLIFfile( pFile, dd, pLuts, nLuts, bCVars, pNames, nNames, FileName );
-
-        fprintf( pFile, ".end\n" );
-        fclose( pFile );
-        if ( fVerbose )
-        printf( "Output file writing time  = %.2f sec\n", (float)(clock() - clk1)/(float)(CLOCKS_PER_SEC) );
-    }
-
-
-    // updo the LUT cascade
-    for ( i = 0; i < nLuts; i++ )
-    {
-        p = pLuts[i];
-        for ( v = 0; v < p->nCols; v++ )
-        {
-            Cudd_RecursiveDeref( dd, p->pbCols[v] );
-            Cudd_RecursiveDeref( dd, p->pbCodes[v] );
-            Cudd_RecursiveDeref( dd, p->paNodes[v] );
-        }
-        Cudd_RecursiveDeref( dd, p->bRelation );
-
-        free( p->pbCols );
-        free( p->pbCodes );
-        free( p->paNodes );
-        free( p );
-    }
-
-    return 1;
-}
- 
-void WriteLUTSintoBLIFfile( FILE * pFile, DdManager * dd, LUT ** pLuts, int nLuts, DdNode ** bCVars, char ** pNames, int nNames, char * FileName )
-{
-    int i, v, o;
-    static char * pNamesLocalIn[MAXINPUTS];
-    static char * pNamesLocalOut[MAXINPUTS];
-    static char Buffer[100];
-    DdNode * bCube, * bCof, * bFunc;
-    LUT * p;
-
-    // go through all the LUTs
-    for ( i = 0; i < nLuts; i++ )
-    {
-        // get the pointer to the LUT
-        p = pLuts[i];
-
-        if ( i == nLuts -1 )
-        {
-            assert( p->nMulti == 1 );
-        }
-
-
-        fprintf( pFile, "#----------------- LUT #%d ----------------------\n", i );
-
-
-        // fill in the names for the current LUT
-
-        // write the outputs of the previous LUT
-        if ( i != 0 )
-        for ( v = 0; v < p->nInsP; v++ )
-        {
-            sprintf( Buffer, "LUT%02d_%02d", i-1, v );
-            pNamesLocalIn[dd->invperm[v]] = Extra_UtilStrsav( Buffer );
-        }
-        // write the primary inputs of the current LUT
-        for ( v = 0; v < p->nIns - p->nInsP; v++ )
-            pNamesLocalIn[dd->invperm[p->Level+v]] = Extra_UtilStrsav( pNames[dd->invperm[p->Level+v]] );
-        // write the outputs of the current LUT
-        for ( v = 0; v < p->nMulti; v++ )
-        {
-            sprintf( Buffer, "LUT%02d_%02d", i, v );
-            if ( i != nLuts - 1 )
-                pNamesLocalOut[v] = Extra_UtilStrsav( Buffer );
-            else 
-                pNamesLocalOut[v] = Extra_UtilStrsav( "F" );
-        }
-
-
-        // write LUT outputs
-
-        // get the prefix
-        sprintf( Buffer, "L%02d_", i );
-
-        // get the cube of encoding variables
-        bCube = Extra_bddBitsToCube( dd, (1<<p->nMulti)-1, p->nMulti, bCVars, 1 );   Cudd_Ref( bCube );
-
-        // write each output of the LUT
-        for ( o = 0; o < p->nMulti; o++ )
-        {
-            // get the cofactor of this output
-            bCof = Cudd_Cofactor( dd, p->bRelation, bCVars[o] );  Cudd_Ref( bCof );
-            // quantify the remaining variables to get the function
-            bFunc = Cudd_bddExistAbstract( dd, bCof, bCube );     Cudd_Ref( bFunc );
-            Cudd_RecursiveDeref( dd, bCof );
-            
-            // write BLIF
-            sprintf( Buffer, "L%02d_%02d_", i, o );
-
-//          WriteDDintoBLIFfileReorder( dd, pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
-            // does not work well; the advantage is marginal (30%), the run time is huge...
-
-            WriteDDintoBLIFfile( pFile, bFunc, pNamesLocalOut[o], Buffer, pNamesLocalIn );
-            Cudd_RecursiveDeref( dd, bFunc );
-        }
-        Cudd_RecursiveDeref( dd, bCube );
-
-        // clean up the previous local names
-        for ( v = 0; v < dd->size; v++ )
-        {
-            if ( pNamesLocalIn[v] )
-                free( pNamesLocalIn[v] );
-            pNamesLocalIn[v] = NULL;
-        }
-        for ( v = 0; v < p->nMulti; v++ )
-            free( pNamesLocalOut[v] );
-    }
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                           END OF FILE                            ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-
diff --git a/src/bdd/cas/module.make b/src/bdd/cas/module.make
deleted file mode 100644
index 7830e47f..00000000
--- a/src/bdd/cas/module.make
+++ /dev/null
@@ -1,3 +0,0 @@
-SRC +=    src/bdd/cas/casCore.c \
-    src/bdd/cas/casDec.c
-
diff --git a/src/bdd/cudd/cuddAPI.c b/src/bdd/cudd/cuddAPI.c
index a16b82cf..2acde7cd 100644
--- a/src/bdd/cudd/cuddAPI.c
+++ b/src/bdd/cudd/cuddAPI.c
@@ -164,7 +164,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddAddAbs.c b/src/bdd/cudd/cuddAddAbs.c
index b256ad0f..27039908 100644
--- a/src/bdd/cudd/cuddAddAbs.c
+++ b/src/bdd/cudd/cuddAddAbs.c
@@ -32,7 +32,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddAddApply.c b/src/bdd/cudd/cuddAddApply.c
index 60c06de6..67649913 100644
--- a/src/bdd/cudd/cuddAddApply.c
+++ b/src/bdd/cudd/cuddAddApply.c
@@ -42,7 +42,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddAddFind.c b/src/bdd/cudd/cuddAddFind.c
index 0469b014..3399527a 100644
--- a/src/bdd/cudd/cuddAddFind.c
+++ b/src/bdd/cudd/cuddAddFind.c
@@ -27,7 +27,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddAddInv.c b/src/bdd/cudd/cuddAddInv.c
index fc4a340b..cb6dbfbe 100644
--- a/src/bdd/cudd/cuddAddInv.c
+++ b/src/bdd/cudd/cuddAddInv.c
@@ -24,7 +24,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddAddIte.c b/src/bdd/cudd/cuddAddIte.c
index 71f8070f..77c4d18a 100644
--- a/src/bdd/cudd/cuddAddIte.c
+++ b/src/bdd/cudd/cuddAddIte.c
@@ -33,7 +33,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddAddNeg.c b/src/bdd/cudd/cuddAddNeg.c
index bdb08ddc..2420df64 100644
--- a/src/bdd/cudd/cuddAddNeg.c
+++ b/src/bdd/cudd/cuddAddNeg.c
@@ -26,7 +26,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddAddWalsh.c b/src/bdd/cudd/cuddAddWalsh.c
index c6a67e34..980ee215 100644
--- a/src/bdd/cudd/cuddAddWalsh.c
+++ b/src/bdd/cudd/cuddAddWalsh.c
@@ -26,7 +26,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddAndAbs.c b/src/bdd/cudd/cuddAndAbs.c
index 5ec47beb..3a6ce85f 100644
--- a/src/bdd/cudd/cuddAndAbs.c
+++ b/src/bdd/cudd/cuddAndAbs.c
@@ -24,7 +24,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddAnneal.c b/src/bdd/cudd/cuddAnneal.c
index 3d8b56b9..dfc81e86 100644
--- a/src/bdd/cudd/cuddAnneal.c
+++ b/src/bdd/cudd/cuddAnneal.c
@@ -35,7 +35,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddApa.c b/src/bdd/cudd/cuddApa.c
index 47ab51e8..805a4dde 100644
--- a/src/bdd/cudd/cuddApa.c
+++ b/src/bdd/cudd/cuddApa.c
@@ -28,7 +28,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddApprox.c b/src/bdd/cudd/cuddApprox.c
index debcf48b..eb6813ff 100644
--- a/src/bdd/cudd/cuddApprox.c
+++ b/src/bdd/cudd/cuddApprox.c
@@ -51,7 +51,7 @@
 #else
 #define DBL_MAX_EXP 1024
 #endif
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddBddAbs.c b/src/bdd/cudd/cuddBddAbs.c
index 9552464e..20a8f15a 100644
--- a/src/bdd/cudd/cuddBddAbs.c
+++ b/src/bdd/cudd/cuddBddAbs.c
@@ -35,7 +35,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddBddCorr.c b/src/bdd/cudd/cuddBddCorr.c
index c99324a8..47395ec7 100644
--- a/src/bdd/cudd/cuddBddCorr.c
+++ b/src/bdd/cudd/cuddBddCorr.c
@@ -30,7 +30,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddBddIte.c b/src/bdd/cudd/cuddBddIte.c
index b44e40de..fe0c6500 100644
--- a/src/bdd/cudd/cuddBddIte.c
+++ b/src/bdd/cudd/cuddBddIte.c
@@ -44,7 +44,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddBridge.c b/src/bdd/cudd/cuddBridge.c
index ccc0893f..e7e5c89f 100644
--- a/src/bdd/cudd/cuddBridge.c
+++ b/src/bdd/cudd/cuddBridge.c
@@ -44,7 +44,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddCache.c b/src/bdd/cudd/cuddCache.c
index d9e40921..6598948a 100644
--- a/src/bdd/cudd/cuddCache.c
+++ b/src/bdd/cudd/cuddCache.c
@@ -36,7 +36,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddCheck.c b/src/bdd/cudd/cuddCheck.c
index aec8246d..3db08dd6 100644
--- a/src/bdd/cudd/cuddCheck.c
+++ b/src/bdd/cudd/cuddCheck.c
@@ -34,7 +34,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddClip.c b/src/bdd/cudd/cuddClip.c
index 4da296ef..3c728a56 100644
--- a/src/bdd/cudd/cuddClip.c
+++ b/src/bdd/cudd/cuddClip.c
@@ -33,7 +33,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddCof.c b/src/bdd/cudd/cuddCof.c
index f79e3f91..0dfeff6c 100644
--- a/src/bdd/cudd/cuddCof.c
+++ b/src/bdd/cudd/cuddCof.c
@@ -29,7 +29,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddCompose.c b/src/bdd/cudd/cuddCompose.c
index 8c858051..11c6cb7b 100644
--- a/src/bdd/cudd/cuddCompose.c
+++ b/src/bdd/cudd/cuddCompose.c
@@ -55,7 +55,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddDecomp.c b/src/bdd/cudd/cuddDecomp.c
index 4fde7392..d9c28482 100644
--- a/src/bdd/cudd/cuddDecomp.c
+++ b/src/bdd/cudd/cuddDecomp.c
@@ -34,7 +34,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddEssent.c b/src/bdd/cudd/cuddEssent.c
index db4b8b49..7bd48c5a 100644
--- a/src/bdd/cudd/cuddEssent.c
+++ b/src/bdd/cudd/cuddEssent.c
@@ -25,7 +25,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddExact.c b/src/bdd/cudd/cuddExact.c
index 6852be68..6a81406b 100644
--- a/src/bdd/cudd/cuddExact.c
+++ b/src/bdd/cudd/cuddExact.c
@@ -40,7 +40,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddExport.c b/src/bdd/cudd/cuddExport.c
index d148be42..d7b9645b 100644
--- a/src/bdd/cudd/cuddExport.c
+++ b/src/bdd/cudd/cuddExport.c
@@ -35,7 +35,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddGenCof.c b/src/bdd/cudd/cuddGenCof.c
index 142ee27e..59ae55d7 100644
--- a/src/bdd/cudd/cuddGenCof.c
+++ b/src/bdd/cudd/cuddGenCof.c
@@ -46,7 +46,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddGenetic.c b/src/bdd/cudd/cuddGenetic.c
index 9fe03dad..8341dcbd 100644
--- a/src/bdd/cudd/cuddGenetic.c
+++ b/src/bdd/cudd/cuddGenetic.c
@@ -53,7 +53,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddGroup.c b/src/bdd/cudd/cuddGroup.c
index 81c05d2c..f84f7881 100644
--- a/src/bdd/cudd/cuddGroup.c
+++ b/src/bdd/cudd/cuddGroup.c
@@ -49,7 +49,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddHarwell.c b/src/bdd/cudd/cuddHarwell.c
index 063f1922..10746186 100644
--- a/src/bdd/cudd/cuddHarwell.c
+++ b/src/bdd/cudd/cuddHarwell.c
@@ -21,7 +21,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddInit.c b/src/bdd/cudd/cuddInit.c
index 8e06a425..aec8d286 100644
--- a/src/bdd/cudd/cuddInit.c
+++ b/src/bdd/cudd/cuddInit.c
@@ -29,7 +29,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #define CUDD_MAIN
 #include    "cuddInt.h"
 #undef CUDD_MAIN
diff --git a/src/bdd/cudd/cuddInteract.c b/src/bdd/cudd/cuddInteract.c
index 96613639..5a4ec79a 100644
--- a/src/bdd/cudd/cuddInteract.c
+++ b/src/bdd/cudd/cuddInteract.c
@@ -47,7 +47,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddLCache.c b/src/bdd/cudd/cuddLCache.c
index 8bd37ba0..72fbd48a 100644
--- a/src/bdd/cudd/cuddLCache.c
+++ b/src/bdd/cudd/cuddLCache.c
@@ -45,7 +45,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddLevelQ.c b/src/bdd/cudd/cuddLevelQ.c
index 3cc8e8d8..c4c621e7 100644
--- a/src/bdd/cudd/cuddLevelQ.c
+++ b/src/bdd/cudd/cuddLevelQ.c
@@ -50,7 +50,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddLinear.c b/src/bdd/cudd/cuddLinear.c
index 7f6b3678..cec7c255 100644
--- a/src/bdd/cudd/cuddLinear.c
+++ b/src/bdd/cudd/cuddLinear.c
@@ -34,7 +34,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddLiteral.c b/src/bdd/cudd/cuddLiteral.c
index 43740690..69594486 100644
--- a/src/bdd/cudd/cuddLiteral.c
+++ b/src/bdd/cudd/cuddLiteral.c
@@ -25,7 +25,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddMatMult.c b/src/bdd/cudd/cuddMatMult.c
index 345e7921..b10975ec 100644
--- a/src/bdd/cudd/cuddMatMult.c
+++ b/src/bdd/cudd/cuddMatMult.c
@@ -29,7 +29,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddPriority.c b/src/bdd/cudd/cuddPriority.c
index 788fc712..bb0b83d3 100644
--- a/src/bdd/cudd/cuddPriority.c
+++ b/src/bdd/cudd/cuddPriority.c
@@ -43,7 +43,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddRead.c b/src/bdd/cudd/cuddRead.c
index 2c4a86d8..eea4c7f3 100644
--- a/src/bdd/cudd/cuddRead.c
+++ b/src/bdd/cudd/cuddRead.c
@@ -23,7 +23,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddRef.c b/src/bdd/cudd/cuddRef.c
index a9241f3d..af08d048 100644
--- a/src/bdd/cudd/cuddRef.c
+++ b/src/bdd/cudd/cuddRef.c
@@ -38,7 +38,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddReorder.c b/src/bdd/cudd/cuddReorder.c
index 1387196f..e2b3470b 100644
--- a/src/bdd/cudd/cuddReorder.c
+++ b/src/bdd/cudd/cuddReorder.c
@@ -45,7 +45,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSat.c b/src/bdd/cudd/cuddSat.c
index 1755a1c1..dde33a5b 100644
--- a/src/bdd/cudd/cuddSat.c
+++ b/src/bdd/cudd/cuddSat.c
@@ -42,7 +42,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSign.c b/src/bdd/cudd/cuddSign.c
index fcaa65c4..62477e7f 100644
--- a/src/bdd/cudd/cuddSign.c
+++ b/src/bdd/cudd/cuddSign.c
@@ -25,7 +25,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/cudd/cuddSolve.c b/src/bdd/cudd/cuddSolve.c
index d9c4a2e7..058e0c08 100644
--- a/src/bdd/cudd/cuddSolve.c
+++ b/src/bdd/cudd/cuddSolve.c
@@ -28,7 +28,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSplit.c b/src/bdd/cudd/cuddSplit.c
index e21ea7cb..af7d6372 100644
--- a/src/bdd/cudd/cuddSplit.c
+++ b/src/bdd/cudd/cuddSplit.c
@@ -32,7 +32,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSubsetHB.c b/src/bdd/cudd/cuddSubsetHB.c
index 24d41ce5..43aaf744 100644
--- a/src/bdd/cudd/cuddSubsetHB.c
+++ b/src/bdd/cudd/cuddSubsetHB.c
@@ -46,7 +46,7 @@
 #else
 #define DBL_MAX_EXP 1024
 #endif
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSubsetSP.c b/src/bdd/cudd/cuddSubsetSP.c
index 55ee3470..0f7209dd 100644
--- a/src/bdd/cudd/cuddSubsetSP.c
+++ b/src/bdd/cudd/cuddSubsetSP.c
@@ -41,7 +41,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddSymmetry.c b/src/bdd/cudd/cuddSymmetry.c
index e5488b17..7b2013e4 100644
--- a/src/bdd/cudd/cuddSymmetry.c
+++ b/src/bdd/cudd/cuddSymmetry.c
@@ -38,7 +38,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddTable.c b/src/bdd/cudd/cuddTable.c
index 7f14aed1..b118b76a 100644
--- a/src/bdd/cudd/cuddTable.c
+++ b/src/bdd/cudd/cuddTable.c
@@ -54,7 +54,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddUtil.c b/src/bdd/cudd/cuddUtil.c
index d5fa18e2..c366d534 100644
--- a/src/bdd/cudd/cuddUtil.c
+++ b/src/bdd/cudd/cuddUtil.c
@@ -76,7 +76,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddWindow.c b/src/bdd/cudd/cuddWindow.c
index 9ceb79b2..3e6d5686 100644
--- a/src/bdd/cudd/cuddWindow.c
+++ b/src/bdd/cudd/cuddWindow.c
@@ -31,7 +31,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddCount.c b/src/bdd/cudd/cuddZddCount.c
index 6c6ec1df..29cf0c14 100644
--- a/src/bdd/cudd/cuddZddCount.c
+++ b/src/bdd/cudd/cuddZddCount.c
@@ -34,7 +34,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddFuncs.c b/src/bdd/cudd/cuddZddFuncs.c
index 9dc27a95..f938e1de 100644
--- a/src/bdd/cudd/cuddZddFuncs.c
+++ b/src/bdd/cudd/cuddZddFuncs.c
@@ -48,7 +48,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddGroup.c b/src/bdd/cudd/cuddZddGroup.c
index 621fa43f..35f28881 100644
--- a/src/bdd/cudd/cuddZddGroup.c
+++ b/src/bdd/cudd/cuddZddGroup.c
@@ -40,7 +40,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddIsop.c b/src/bdd/cudd/cuddZddIsop.c
index f4b057ea..0918461c 100644
--- a/src/bdd/cudd/cuddZddIsop.c
+++ b/src/bdd/cudd/cuddZddIsop.c
@@ -34,7 +34,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddLin.c b/src/bdd/cudd/cuddZddLin.c
index ef2cd298..9369bb05 100644
--- a/src/bdd/cudd/cuddZddLin.c
+++ b/src/bdd/cudd/cuddZddLin.c
@@ -32,7 +32,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddMisc.c b/src/bdd/cudd/cuddZddMisc.c
index 6a4ddd09..d55bb768 100644
--- a/src/bdd/cudd/cuddZddMisc.c
+++ b/src/bdd/cudd/cuddZddMisc.c
@@ -33,7 +33,7 @@
 ******************************************************************************/
 
 #include    <math.h>
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddPort.c b/src/bdd/cudd/cuddZddPort.c
index 6d4a3236..1700ab2b 100644
--- a/src/bdd/cudd/cuddZddPort.c
+++ b/src/bdd/cudd/cuddZddPort.c
@@ -32,7 +32,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddReord.c b/src/bdd/cudd/cuddZddReord.c
index e2da37f2..e14ae2ad 100644
--- a/src/bdd/cudd/cuddZddReord.c
+++ b/src/bdd/cudd/cuddZddReord.c
@@ -46,7 +46,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddSetop.c b/src/bdd/cudd/cuddZddSetop.c
index f1bd72f3..cf05210f 100644
--- a/src/bdd/cudd/cuddZddSetop.c
+++ b/src/bdd/cudd/cuddZddSetop.c
@@ -46,7 +46,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddSymm.c b/src/bdd/cudd/cuddZddSymm.c
index 54019892..c9ffaab4 100644
--- a/src/bdd/cudd/cuddZddSymm.c
+++ b/src/bdd/cudd/cuddZddSymm.c
@@ -40,7 +40,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/cuddZddUtil.c b/src/bdd/cudd/cuddZddUtil.c
index 616d16d4..0795f123 100644
--- a/src/bdd/cudd/cuddZddUtil.c
+++ b/src/bdd/cudd/cuddZddUtil.c
@@ -35,7 +35,7 @@
 
 ******************************************************************************/
 
-#include    "util_hack.h"
+#include    "util.h"
 #include    "cuddInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/cudd/testcudd.c b/src/bdd/cudd/testcudd.c
index d8affadc..451bb190 100644
--- a/src/bdd/cudd/testcudd.c
+++ b/src/bdd/cudd/testcudd.c
@@ -23,7 +23,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "cuddInt.h"
 
 
diff --git a/src/bdd/dsd/dsd.h b/src/bdd/dsd/dsd.h
index b73b81ab..5396bacd 100644
--- a/src/bdd/dsd/dsd.h
+++ b/src/bdd/dsd/dsd.h
@@ -28,12 +28,8 @@
 #ifndef __DSD_H__
 #define __DSD_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 ////////////////////////////////////////////////////////////////////////
-///                      TYPEDEF DEFINITIONS                         ///
+///                      TYPEDEF DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Dsd_Manager_t_   Dsd_Manager_t;
@@ -59,14 +55,14 @@ enum Dsd_Type_t_ {
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 // complementation and testing for pointers for decomposition entries
-#define Dsd_IsComplement(p)  (((int)((unsigned long) (p) & 01)))
-#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned long)(p) & ~01)) 
-#define Dsd_Not(p)           ((Dsd_Node_t *)((unsigned long)(p) ^ 01)) 
-#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((unsigned long)(p) ^ (c)))
+#define Dsd_IsComplement(p)  (((int)((long) (p) & 01)))
+#define Dsd_Regular(p)       ((Dsd_Node_t *)((unsigned)(p) & ~01)) 
+#define Dsd_Not(p)           ((Dsd_Node_t *)((long)(p) ^ 01)) 
+#define Dsd_NotCond(p,c)     ((Dsd_Node_t *)((long)(p) ^ (c)))
 
 ////////////////////////////////////////////////////////////////////////
 ///                         ITERATORS                                ///
@@ -80,7 +76,7 @@ enum Dsd_Type_t_ {
           Index++ )
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== dsdApi.c =======================================================*/
@@ -95,7 +91,6 @@ extern void            Dsd_NodeSetMark( Dsd_Node_t * p, int Mark );
 extern DdManager *     Dsd_ManagerReadDd( Dsd_Manager_t * pMan );
 extern Dsd_Node_t *    Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i );
 extern Dsd_Node_t *    Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i );
-extern Dsd_Node_t *    Dsd_ManagerReadConst1( Dsd_Manager_t * pMan );
 /*=== dsdMan.c =======================================================*/
 extern Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose );
 extern void            Dsd_ManagerStop( Dsd_Manager_t * dMan );
@@ -105,7 +100,6 @@ extern Dsd_Node_t *    Dsd_DecomposeOne( Dsd_Manager_t * pDsdMan, DdNode * bFunc
 /*=== dsdTree.c =======================================================*/
 extern void            Dsd_TreeNodeGetInfo( Dsd_Manager_t * dMan, int * DepthMax, int * GateSizeMax );
 extern void            Dsd_TreeNodeGetInfoOne( Dsd_Node_t * pNode, int * DepthMax, int * GateSizeMax );
-extern int             Dsd_TreeGetAigCost( Dsd_Node_t * pNode );
 extern int             Dsd_TreeCountNonTerminalNodes( Dsd_Manager_t * dMan );
 extern int             Dsd_TreeCountNonTerminalNodesOne( Dsd_Node_t * pRoot );
 extern int             Dsd_TreeCountPrimeNodes( Dsd_Manager_t * pDsdMan );
@@ -114,16 +108,11 @@ extern int             Dsd_TreeCollectDecomposableVars( Dsd_Manager_t * dMan, in
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfs( Dsd_Manager_t * dMan, int * pnNodes );
 extern Dsd_Node_t **   Dsd_TreeCollectNodesDfsOne( Dsd_Manager_t * pDsdMan, Dsd_Node_t * pNode, int * pnNodes );
 extern void            Dsd_TreePrint( FILE * pFile, Dsd_Manager_t * dMan, char * pInputNames[], char * pOutputNames[], int fShortNames, int Output );
-extern void            Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode );
 /*=== dsdLocal.c =======================================================*/
 extern DdNode *        Dsd_TreeGetPrimeFunction( DdManager * dd, Dsd_Node_t * pNode );
 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
+
+#endif
\ No newline at end of file
diff --git a/src/bdd/dsd/dsdApi.c b/src/bdd/dsd/dsdApi.c
index d1c90e23..daf3080f 100644
--- a/src/bdd/dsd/dsdApi.c
+++ b/src/bdd/dsd/dsdApi.c
@@ -23,7 +23,7 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -89,7 +89,6 @@ void          Dsd_NodeSetMark( Dsd_Node_t * p, int Mark ){ p->Mark = Mark;     }
 ***********************************************************************/
 Dsd_Node_t *  Dsd_ManagerReadRoot( Dsd_Manager_t * pMan, int i )  { return pMan->pRoots[i];  } 
 Dsd_Node_t *  Dsd_ManagerReadInput( Dsd_Manager_t * pMan, int i ) { return pMan->pInputs[i]; } 
-Dsd_Node_t *  Dsd_ManagerReadConst1( Dsd_Manager_t * pMan )       { return pMan->pConst1;    } 
 DdManager *   Dsd_ManagerReadDd( Dsd_Manager_t * pMan )           { return pMan->dd;         } 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/bdd/dsd/dsdCheck.c b/src/bdd/dsd/dsdCheck.c
index 58b824d2..608aa2e3 100644
--- a/src/bdd/dsd/dsdCheck.c
+++ b/src/bdd/dsd/dsdCheck.c
@@ -43,7 +43,7 @@ static Dds_Cache_t * pCache;
 static int Dsd_CheckRootFunctionIdentity_rec( DdManager * dd, DdNode * bF1, DdNode * bF2, DdNode * bC1, DdNode * bC2 );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function********************************************************************
@@ -82,7 +82,7 @@ void Dsd_CheckCacheAllocate( int nEntries )
 
 /**Function********************************************************************
 
-  Synopsis    [Deallocates the local cache.]
+  Synopsis    [Delocates the local cache.]
 
   Description []
 
diff --git a/src/bdd/dsd/dsdInt.h b/src/bdd/dsd/dsdInt.h
index 62ce7e99..5008c24e 100644
--- a/src/bdd/dsd/dsdInt.h
+++ b/src/bdd/dsd/dsdInt.h
@@ -23,7 +23,7 @@
 #include "dsd.h"
 
 ////////////////////////////////////////////////////////////////////////
-///                      TYPEDEF DEFINITIONS                         ///
+///                      TYPEDEF DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
  
 typedef unsigned char byte;
@@ -42,7 +42,6 @@ struct Dsd_Manager_t_
     int            nRootsAlloc;// the number of primary outputs
     Dsd_Node_t **  pInputs;    // the primary input nodes
     Dsd_Node_t **  pRoots;     // the primary output nodes
-    Dsd_Node_t *   pConst1;    // the constant node
     int            fVerbose;   // the verbosity level 
 };
 
@@ -59,7 +58,7 @@ struct Dsd_Node_t_
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 #define MAXINPUTS 1000
@@ -83,9 +82,9 @@ extern void         Dsd_TreeNodeDelete( DdManager * dd, Dsd_Node_t * pNode );
 extern void         Dsd_TreeUnmark( Dsd_Manager_t * dMan );
 extern DdNode *     Dsd_TreeGetPrimeFunctionOld( DdManager * dd, Dsd_Node_t * pNode, int fRemap );
 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                           END OF FILE                            ///
 ////////////////////////////////////////////////////////////////////////
 
+
+#endif
\ No newline at end of file
diff --git a/src/bdd/dsd/dsdMan.c b/src/bdd/dsd/dsdMan.c
index 6e43f0f4..4529e75a 100644
--- a/src/bdd/dsd/dsdMan.c
+++ b/src/bdd/dsd/dsdMan.c
@@ -73,7 +73,6 @@ Dsd_Manager_t * Dsd_ManagerStart( DdManager * dd, int nSuppMax, int fVerbose )
     pNode->G = b1;  Cudd_Ref( pNode->G );
     pNode->S = b1;  Cudd_Ref( pNode->S );
     st_insert( dMan->Table, (char*)b1, (char*)pNode );
-    dMan->pConst1 = pNode;
 
     Dsd_CheckCacheAllocate( 5000 );
     return dMan;
diff --git a/src/bdd/dsd/dsdProc.c b/src/bdd/dsd/dsdProc.c
index 543ad387..08c029e1 100644
--- a/src/bdd/dsd/dsdProc.c
+++ b/src/bdd/dsd/dsdProc.c
@@ -1255,7 +1255,7 @@ EXIT:
     s_CacheEntries++;
 
 
-/*
+#if 0
     if ( dsdKernelVerifyDecomposition(dd, pThis) == 0 )
     {
         // write the function, for which verification does not work
@@ -1277,7 +1277,7 @@ EXIT:
         cuddWriteFunctionSop( stdout, dd, zNewFunc, -1, dd->size, "1", s_pVarMask );
         Cudd_RecursiveDerefZdd( dd, zNewFunc );
     }
-*/
+#endif
 
     }
 
diff --git a/src/bdd/dsd/dsdTree.c b/src/bdd/dsd/dsdTree.c
index 2855d68d..7905cbdd 100644
--- a/src/bdd/dsd/dsdTree.c
+++ b/src/bdd/dsd/dsdTree.c
@@ -29,7 +29,7 @@ static int  Dsd_TreeCountPrimeNodes_rec( Dsd_Node_t * pNode );
 static int  Dsd_TreeCollectDecomposableVars_rec( DdManager * dd, Dsd_Node_t * pNode, int * pVars, int * nVars );
 static void Dsd_TreeCollectNodesDfs_rec( Dsd_Node_t * pNode, Dsd_Node_t * ppNodes[], int * pnNodes );
 static void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fCcmp, char * pInputNames[], char * pOutputName, int nOffset, int * pSigCounter, int fShortNames );
-static void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter );
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                      STATIC VARIABLES                            ///
@@ -243,58 +243,6 @@ void Dsd_TreeGetInfo_rec( Dsd_Node_t * pNode, int RankCur )
 
 /**Function*************************************************************
 
-  Synopsis    [Counts AIG nodes needed to implement this node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dsd_TreeGetAigCost_rec( Dsd_Node_t * pNode )
-{
-    int i, Counter = 0;
-
-    assert( pNode );
-    assert( !Dsd_IsComplement( pNode ) );
-    assert( pNode->nVisits >= 0 );
-
-    if ( pNode->nDecs < 2 )
-        return 0;
-
-    // we don't want the two-input gates to count for non-decomposable blocks
-    if ( pNode->Type == DSD_NODE_OR )
-        Counter += pNode->nDecs - 1;
-    else if ( pNode->Type == DSD_NODE_EXOR )
-        Counter += 3*(pNode->nDecs - 1);
-    else if ( pNode->Type == DSD_NODE_PRIME && pNode->nDecs == 3 )
-        Counter += 3;
-
-    // call recursively
-    for ( i = 0; i < pNode->nDecs; i++ )
-        Counter += Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode->pDecs[i]) );
-    return Counter;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Counts AIG nodes needed to implement this node.]
-
-  Description [Assumes that the only primes of the DSD tree are MUXes.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Dsd_TreeGetAigCost( Dsd_Node_t * pNode )
-{
-    return Dsd_TreeGetAigCost_rec( Dsd_Regular(pNode) );
-}
-
-/**Function*************************************************************
-
   Synopsis    [Counts non-terminal nodes of the DSD tree.]
 
   Description [Nonterminal nodes include all the nodes with the
@@ -683,21 +631,27 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
         pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
 
     Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
-    if ( !fComp )
-        fprintf( pFile, "%s = ", pOutputName );
-    else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
+    fprintf( pFile, "%s: ", pOutputName );
     pInputNums = ALLOC( int, pNode->nDecs );
     if ( pNode->Type == DSD_NODE_CONST1 )
     {
-         fprintf( pFile, " Constant 1.\n" );
+        if ( fComp )
+            fprintf( pFile, " Constant 0.\n" );
+        else
+            fprintf( pFile, " Constant 1.\n" );
     }
     else if ( pNode->Type == DSD_NODE_BUF )
     {
+        if ( fComp )
+            fprintf( pFile, " NOT(" );
+        else
+            fprintf( pFile, " " );
         if ( fShortNames )
-            fprintf( pFile, "%d", 'a' + pNode->S->index );
+            fprintf( pFile, "%d", pNode->S->index );
         else
             fprintf( pFile, "%s", pInputNames[pNode->S->index] );
+        if ( fComp )
+            fprintf( pFile, ")" );
         fprintf( pFile, "\n" );
     }
     else if ( pNode->Type == DSD_NODE_PRIME )
@@ -710,25 +664,25 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             fCompNew = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
                     fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
+                fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -736,39 +690,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( pInputNums[i] )
             {
                 pInput   = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_OR )
     {
         // print the line
-        fprintf( pFile, "OR(" );
+        if ( fComp )
+            fprintf( pFile, "AND(" );
+        else
+            fprintf( pFile, "OR(" );
         for ( i = 0; i < pNode->nDecs; i++ )
         {
             pInput = Dsd_Regular( pNode->pDecs[i] );
             fCompNew  = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
-                    fprintf( pFile, "%c", 'a' + pInput->S->index );
+                    fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
+                fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -776,208 +734,43 @@ void Dsd_TreePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pInp
             if ( pInputNums[i] )
             {
                 pInput = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew  = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fComp ^ fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     else if ( pNode->Type == DSD_NODE_EXOR )
     {
         // print the line
-        fprintf( pFile, "EXOR(" );
+        if ( fComp )
+            fprintf( pFile, "NEXOR(" );
+        else
+            fprintf( pFile, "EXOR(" );
         for ( i = 0; i < pNode->nDecs; i++ )
         {
             pInput = Dsd_Regular( pNode->pDecs[i] );
             fCompNew  = (int)( pInput != pNode->pDecs[i] );
             if ( i )
                 fprintf( pFile, "," );
-            if ( fCompNew )
-                fprintf( pFile, " NOT(" );
-            else
-                fprintf( pFile, " " );
             if ( pInput->Type == DSD_NODE_BUF )
             {
                 pInputNums[i] = 0;
+                if ( fCompNew )
+                    fprintf( pFile, " NOT(" );
+                else
+                    fprintf( pFile, " " );
                 if ( fShortNames )
-                    fprintf( pFile, "%c", 'a' + pInput->S->index );
+                    fprintf( pFile, "%d", pInput->S->index );
                 else
                     fprintf( pFile, "%s", pInputNames[pInput->S->index] );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, "<%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, ")" );
-        }
-        fprintf( pFile, " )\n" );
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
-            }
-    }
-    free( pInputNums );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints the decompostion tree into file.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dsd_NodePrint( FILE * pFile, Dsd_Node_t * pNode )
-{
-    Dsd_Node_t * pNodeR;
-    int SigCounter = 1;
-    pNodeR = Dsd_Regular(pNode);
-    Dsd_NodePrint_rec( pFile, pNodeR, pNodeR != pNode, "F", 0, &SigCounter );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Prints one node of the decomposition tree.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOutputName, int nOffset, int * pSigCounter )
-{
-    char Buffer[100];
-    Dsd_Node_t * pInput;
-    int * pInputNums;
-    int fCompNew, i;
-
-    assert( pNode->Type == DSD_NODE_BUF || pNode->Type == DSD_NODE_CONST1 || 
-        pNode->Type == DSD_NODE_PRIME || pNode->Type == DSD_NODE_OR || pNode->Type == DSD_NODE_EXOR ); 
-
-    Extra_PrintSymbols( pFile, ' ', nOffset, 0 );
-    if ( !fComp )
-        fprintf( pFile, "%s = ", pOutputName );
-    else
-        fprintf( pFile, "NOT(%s) = ", pOutputName );
-    pInputNums = ALLOC( int, pNode->nDecs );
-    if ( pNode->Type == DSD_NODE_CONST1 )
-    {
-        fprintf( pFile, " Constant 1.\n" );
-    }
-    else if ( pNode->Type == DSD_NODE_BUF )
-    {
-        fprintf( pFile, " " );
-        fprintf( pFile, "%c", 'a' + pNode->S->index );
-        fprintf( pFile, "\n" );
-    }
-    else if ( pNode->Type == DSD_NODE_PRIME )
-    {
-        // print the line
-        fprintf( pFile, "PRIME(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput   = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew = (int)( pInput != pNode->pDecs[i] );
-            assert( fCompNew == 0 );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, " <%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
-        }
-        fprintf( pFile, " )\n" );
-/*
-        fprintf( pFile, " )  " );  
-        {
-            DdNode * bLocal;
-            bLocal = Dsd_TreeGetPrimeFunction( dd, pNodeDsd );  Cudd_Ref( bLocal );
-            Extra_bddPrint( dd, bLocal );
-            Cudd_RecursiveDeref( dd, bLocal );
-        }
-*/
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput   = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
-            }
-    }
-    else if ( pNode->Type == DSD_NODE_OR )
-    {
-        // print the line
-        fprintf( pFile, "OR(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew  = (int)( pInput != pNode->pDecs[i] );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
-            }
-            else
-            {
-                pInputNums[i] = (*pSigCounter)++;
-                fprintf( pFile, " <%d>", pInputNums[i] );
-            }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
-        }
-        fprintf( pFile, " )\n" );
-        // call recursively for the following blocks
-        for ( i = 0; i < pNode->nDecs; i++ )
-            if ( pInputNums[i] )
-            {
-                pInput = Dsd_Regular( pNode->pDecs[i] );
-                sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
-            }
-    }
-    else if ( pNode->Type == DSD_NODE_EXOR )
-    {
-        // print the line
-        fprintf( pFile, "EXOR(" );
-        for ( i = 0; i < pNode->nDecs; i++ )
-        {
-            pInput = Dsd_Regular( pNode->pDecs[i] );
-            fCompNew  = (int)( pInput != pNode->pDecs[i] );
-            assert( fCompNew == 0 );
-            if ( i )
-                fprintf( pFile, "," );
-            if ( pInput->Type == DSD_NODE_BUF )
-            {
-                pInputNums[i] = 0;
-                fprintf( pFile, " %c", 'a' + pInput->S->index );
+                if ( fCompNew )
+                    fprintf( pFile, ")" );
             }
             else
             {
                 pInputNums[i] = (*pSigCounter)++;
                 fprintf( pFile, " <%d>", pInputNums[i] );
             }
-            if ( fCompNew )
-                fprintf( pFile, "\'" );
         }
         fprintf( pFile, " )\n" );
         // call recursively for the following blocks
@@ -985,8 +778,9 @@ void Dsd_NodePrint_rec( FILE * pFile, Dsd_Node_t * pNode, int fComp, char * pOut
             if ( pInputNums[i] )
             {
                 pInput = Dsd_Regular( pNode->pDecs[i] );
+                fCompNew  = (int)( pInput != pNode->pDecs[i] );
                 sprintf( Buffer, "<%d>", pInputNums[i] );
-                Dsd_NodePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), 0, Buffer, nOffset + 6, pSigCounter );
+                Dsd_TreePrint_rec( pFile, Dsd_Regular( pNode->pDecs[i] ), fCompNew, pInputNames, Buffer, nOffset + 6, pSigCounter, fShortNames );
             }
     }
     free( pInputNums );
diff --git a/src/bdd/epd/epd.c b/src/bdd/epd/epd.c
index a80240bc..a843b986 100644
--- a/src/bdd/epd/epd.c
+++ b/src/bdd/epd/epd.c
@@ -25,7 +25,7 @@
 #include <stdlib.h>
 #include <string.h>
 #include <math.h>
-#include "util_hack.h"
+#include "util.h"
 #include "epd.h"
 
 
diff --git a/src/bdd/mtr/mtrBasic.c b/src/bdd/mtr/mtrBasic.c
index 94105282..2aec8d6b 100644
--- a/src/bdd/mtr/mtrBasic.c
+++ b/src/bdd/mtr/mtrBasic.c
@@ -33,7 +33,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "mtrInt.h"
 
 
diff --git a/src/bdd/mtr/mtrGroup.c b/src/bdd/mtr/mtrGroup.c
index 363b776b..ae9c5c2f 100644
--- a/src/bdd/mtr/mtrGroup.c
+++ b/src/bdd/mtr/mtrGroup.c
@@ -33,7 +33,7 @@
 
 ******************************************************************************/
 
-#include "util_hack.h"
+#include "util.h"
 #include "mtrInt.h"
 
 /*---------------------------------------------------------------------------*/
diff --git a/src/bdd/parse/module.make b/src/bdd/parse/module.make
index 4f590f01..ea535e6e 100644
--- a/src/bdd/parse/module.make
+++ b/src/bdd/parse/module.make
@@ -1,3 +1,2 @@
 SRC +=  src/bdd/parse/parseCore.c \
-    src/bdd/parse/parseEqn.c \
     src/bdd/parse/parseStack.c
diff --git a/src/bdd/parse/parse.h b/src/bdd/parse/parse.h
index 4923fbdd..8364e782 100644
--- a/src/bdd/parse/parse.h
+++ b/src/bdd/parse/parse.h
@@ -36,19 +36,18 @@
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== parseCore.c =============================================================*/
 extern DdNode * Parse_FormulaParser( FILE * pOutput, char * pFormula, int nVars, int nRanks, 
       char * ppVarNames[], DdManager * dd, DdNode * pbVars[] );
 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/bdd/parse/parseCore.c b/src/bdd/parse/parseCore.c
index 21a37070..d60687a3 100644
--- a/src/bdd/parse/parseCore.c
+++ b/src/bdd/parse/parseCore.c
@@ -89,7 +89,7 @@
 static DdNode * Parse_ParserPerformTopOp( DdManager * dd, Parse_StackFn_t * pStackFn, int Oper );
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
diff --git a/src/bdd/parse/parseEqn.c b/src/bdd/parse/parseEqn.c
deleted file mode 100644
index 02d83966..00000000
--- a/src/bdd/parse/parseEqn.c
+++ /dev/null
@@ -1,349 +0,0 @@
-/**CFile****************************************************************
-
-  FileNameIn  [parseEqn.c]
-
-  PackageName [ABC: Logic synthesis and verification system.]
-
-  Synopsis    [Boolean formula parser.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - December 18, 2006.]
-
-  Revision    [$Id: parseEqn.c,v 1.0 2006/12/18 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-#include "parseInt.h"
-#include "vec.h"
-#include "hop.h"
-
-// the list of operation symbols to be used in expressions
-#define PARSE_EQN_SYM_OPEN    '('   // opening paranthesis
-#define PARSE_EQN_SYM_CLOSE   ')'   // closing paranthesis
-#define PARSE_EQN_SYM_CONST0  '0'   // constant 0
-#define PARSE_EQN_SYM_CONST1  '1'   // constant 1
-#define PARSE_EQN_SYM_NEG     '!'   // negation before the variable
-#define PARSE_EQN_SYM_AND     '*'   // logic AND
-#define PARSE_EQN_SYM_OR      '+'   // logic OR
-
-// the list of opcodes (also specifying operation precedence)
-#define PARSE_EQN_OPER_NEG    10    // negation
-#define PARSE_EQN_OPER_AND     9    // logic AND
-#define PARSE_EQN_OPER_OR      7    // logic OR
-#define PARSE_EQN_OPER_MARK    1    // OpStack token standing for an opening paranthesis
-
-// these are values of the internal Flag
-#define PARSE_EQN_FLAG_START   1    // after the opening parenthesis 
-#define PARSE_EQN_FLAG_VAR     2    // after operation is received
-#define PARSE_EQN_FLAG_OPER    3    // after operation symbol is received
-#define PARSE_EQN_FLAG_ERROR   4    // when error is detected
-
-#define PARSE_EQN_STACKSIZE 1000
-
-static Hop_Obj_t * Parse_ParserPerformTopOp( Hop_Man_t * pMan, Parse_StackFn_t * pStackFn, int Oper );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the AIG corresponding to the equation.]
-
-  Description [Takes the stream to output messages, the formula, the vector
-  of variable names and the AIG manager.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Parse_FormulaParserEqn( FILE * pOutput, char * pFormInit, Vec_Ptr_t * vVarNames, Hop_Man_t * pMan )
-{
-    char * pFormula;
-    Parse_StackFn_t * pStackFn;
-    Parse_StackOp_t * pStackOp;
-    Hop_Obj_t * gFunc;
-    char * pTemp, * pName;
-    int nParans, fFound, Flag;
-    int Oper, Oper1, Oper2;
-    int i, v;
-
-    // make sure that the number of opening and closing parantheses is the same
-    nParans = 0;
-    for ( pTemp = pFormInit; *pTemp; pTemp++ )
-        if ( *pTemp == '(' )
-            nParans++;
-        else if ( *pTemp == ')' )
-            nParans--;
-    if ( nParans != 0 )
-    {
-        fprintf( pOutput, "Parse_FormulaParserEqn(): Different number of opening and closing parantheses ().\n" );
-        return NULL;
-    }
-
-    // copy the formula
-    pFormula = ALLOC( char, strlen(pFormInit) + 3 );
-    sprintf( pFormula, "(%s)", pFormInit );
-
-    // start the stacks
-    pStackFn = Parse_StackFnStart( PARSE_EQN_STACKSIZE );
-    pStackOp = Parse_StackOpStart( PARSE_EQN_STACKSIZE );
-
-    Flag = PARSE_EQN_FLAG_START;
-    for ( pTemp = pFormula; *pTemp; pTemp++ )
-    {
-        switch ( *pTemp )
-        {
-        // skip all spaces, tabs, and end-of-lines
-        case ' ':
-        case '\t':
-        case '\r':
-        case '\n':
-            continue;
-        case PARSE_EQN_SYM_CONST0:
-            Parse_StackFnPush( pStackFn, Hop_ManConst0(pMan) );  // Cudd_Ref( b0 );
-            if ( Flag == PARSE_EQN_FLAG_VAR )
-            {
-                fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 0.\n" );
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break;
-            }
-            Flag = PARSE_EQN_FLAG_VAR; 
-            break;
-        case PARSE_EQN_SYM_CONST1:
-            Parse_StackFnPush( pStackFn, Hop_ManConst1(pMan) );  //  Cudd_Ref( b1 );
-            if ( Flag == PARSE_EQN_FLAG_VAR )
-            {
-                fprintf( pOutput, "Parse_FormulaParserEqn(): No operation symbol before constant 1.\n" );
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break;
-            }
-            Flag = PARSE_EQN_FLAG_VAR; 
-            break;
-        case PARSE_EQN_SYM_NEG:
-            if ( Flag == PARSE_EQN_FLAG_VAR )
-            {// if NEGBEF follows a variable, AND is assumed
-                Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
-                Flag = PARSE_EQN_FLAG_OPER;
-            }
-            Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_NEG );
-            break;
-        case PARSE_EQN_SYM_AND:
-        case PARSE_EQN_SYM_OR:
-            if ( Flag != PARSE_EQN_FLAG_VAR )
-            {
-                fprintf( pOutput, "Parse_FormulaParserEqn(): There is no variable before AND, EXOR, or OR.\n" );
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break;
-            }
-            if ( *pTemp == PARSE_EQN_SYM_AND )
-                Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
-            else //if ( *pTemp == PARSE_EQN_SYM_OR )
-                Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_OR );
-            Flag = PARSE_EQN_FLAG_OPER; 
-            break;
-        case PARSE_EQN_SYM_OPEN:
-            if ( Flag == PARSE_EQN_FLAG_VAR )
-            {
-//                Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_AND );
-                fprintf( pOutput, "Parse_FormulaParserEqn(): An opening paranthesis follows a var without operation sign.\n" ); 
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break; 
-            }
-            Parse_StackOpPush( pStackOp, PARSE_EQN_OPER_MARK );
-            // after an opening bracket, it feels like starting over again
-            Flag = PARSE_EQN_FLAG_START; 
-            break;
-        case PARSE_EQN_SYM_CLOSE:
-            if ( !Parse_StackOpIsEmpty( pStackOp ) )
-            {
-                while ( 1 )
-                {
-                    if ( Parse_StackOpIsEmpty( pStackOp ) )
-                    {
-                        fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" );
-                        Flag = PARSE_EQN_FLAG_ERROR; 
-                        break;
-                    }
-                    Oper = Parse_StackOpPop( pStackOp );
-                    if ( Oper == PARSE_EQN_OPER_MARK )
-                        break;
-
-                    // perform the given operation
-                    if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper ) == NULL )
-                    {
-                        fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
-                        free( pFormula );
-                        return NULL;
-                    }
-                }
-            }
-            else
-            {
-                fprintf( pOutput, "Parse_FormulaParserEqn(): There is no opening paranthesis\n" );
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break;
-            }
-            if ( Flag != PARSE_EQN_FLAG_ERROR )
-                Flag = PARSE_EQN_FLAG_VAR; 
-            break;
-
-
-        default:
-            // scan the next name
-            for ( i = 0; pTemp[i] && 
-                         pTemp[i] != ' ' && pTemp[i] != '\t' && pTemp[i] != '\r' && pTemp[i] != '\n' &&
-                         pTemp[i] != PARSE_EQN_SYM_AND && pTemp[i] != PARSE_EQN_SYM_OR && pTemp[i] != PARSE_EQN_SYM_CLOSE; i++ )
-              {
-                    if ( pTemp[i] == PARSE_EQN_SYM_NEG || pTemp[i] == PARSE_EQN_SYM_OPEN )
-                    {
-                        fprintf( pOutput, "Parse_FormulaParserEqn(): The negation sign or an opening paranthesis inside the variable name.\n" );
-                        Flag = PARSE_EQN_FLAG_ERROR; 
-                        break;
-                    }
-              }
-            // variable name is found
-            fFound = 0;
-            Vec_PtrForEachEntry( vVarNames, pName, v )
-                if ( strncmp(pTemp, pName, i) == 0 && strlen(pName) == (unsigned)i )
-                {
-                    pTemp += i-1;
-                    fFound = 1;
-                    break;
-                }
-            if ( !fFound )
-            { 
-                fprintf( pOutput, "Parse_FormulaParserEqn(): The parser cannot find var \"%s\" in the input var list.\n", pTemp ); 
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break; 
-            }
-            if ( Flag == PARSE_EQN_FLAG_VAR )
-            {
-                fprintf( pOutput, "Parse_FormulaParserEqn(): The variable name \"%s\" follows another var without operation sign.\n", pTemp ); 
-                Flag = PARSE_EQN_FLAG_ERROR; 
-                break; 
-            }
-            Parse_StackFnPush( pStackFn, Hop_IthVar( pMan, v ) ); // Cudd_Ref( pbVars[v] );
-            Flag = PARSE_EQN_FLAG_VAR; 
-            break;
-        }
-
-        if ( Flag == PARSE_EQN_FLAG_ERROR )
-            break;      // error exit
-        else if ( Flag == PARSE_EQN_FLAG_START )
-            continue;  //  go on parsing
-        else if ( Flag == PARSE_EQN_FLAG_VAR )
-            while ( 1 )
-            {  // check if there are negations in the OpStack     
-                if ( Parse_StackOpIsEmpty(pStackOp) )
-                    break;
-                Oper = Parse_StackOpPop( pStackOp );
-                if ( Oper != PARSE_EQN_OPER_NEG )
-                {
-                    Parse_StackOpPush( pStackOp, Oper );
-                    break;
-                }
-                else
-                {
-                      Parse_StackFnPush( pStackFn, Hop_Not(Parse_StackFnPop(pStackFn)) );
-                }
-            }
-        else // if ( Flag == PARSE_EQN_FLAG_OPER )
-            while ( 1 )
-            {  // execute all the operations in the OpStack
-               // with precedence higher or equal than the last one
-                Oper1 = Parse_StackOpPop( pStackOp ); // the last operation
-                if ( Parse_StackOpIsEmpty(pStackOp) ) 
-                {  // if it is the only operation, push it back
-                    Parse_StackOpPush( pStackOp, Oper1 );
-                    break;
-                }
-                Oper2 = Parse_StackOpPop( pStackOp ); // the operation before the last one
-                if ( Oper2 >= Oper1 )  
-                {  // if Oper2 precedence is higher or equal, execute it
-                    if ( Parse_ParserPerformTopOp( pMan, pStackFn, Oper2 ) == NULL )
-                    {
-                        fprintf( pOutput, "Parse_FormulaParserEqn(): Unknown operation\n" );
-                        free( pFormula );
-                        return NULL;
-                    }
-                    Parse_StackOpPush( pStackOp,  Oper1 );     // push the last operation back
-                }
-                else
-                {  // if Oper2 precedence is lower, push them back and done
-                    Parse_StackOpPush( pStackOp, Oper2 );
-                    Parse_StackOpPush( pStackOp, Oper1 );
-                    break;
-                }
-            }
-    }
-
-    if ( Flag != PARSE_EQN_FLAG_ERROR )
-    {
-        if ( !Parse_StackFnIsEmpty(pStackFn) )
-        {    
-            gFunc = Parse_StackFnPop(pStackFn);
-            if ( Parse_StackFnIsEmpty(pStackFn) )
-                if ( Parse_StackOpIsEmpty(pStackOp) )
-                {
-                    Parse_StackFnFree(pStackFn);
-                    Parse_StackOpFree(pStackOp);
-//                    Cudd_Deref( gFunc );
-                    free( pFormula );
-                    return gFunc;
-                }
-                else
-                    fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the operation stack\n" );
-            else
-                fprintf( pOutput, "Parse_FormulaParserEqn(): Something is left in the function stack\n" );
-        }
-        else
-            fprintf( pOutput, "Parse_FormulaParserEqn(): The input string is empty\n" );
-    }
-    free( pFormula );
-    return NULL;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs the operation on the top entries in the stack.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Hop_Obj_t * Parse_ParserPerformTopOp( Hop_Man_t * pMan, Parse_StackFn_t * pStackFn, int Oper )
-{
-    Hop_Obj_t * gArg1, * gArg2, * gFunc;
-    // perform the given operation
-    gArg2 = Parse_StackFnPop( pStackFn );
-    gArg1 = Parse_StackFnPop( pStackFn );
-    if ( Oper == PARSE_EQN_OPER_AND )
-        gFunc = Hop_And( pMan, gArg1, gArg2 );
-    else if ( Oper == PARSE_EQN_OPER_OR )
-        gFunc = Hop_Or( pMan, gArg1, gArg2 );
-    else
-        return NULL;
-//    Cudd_Ref( gFunc );
-//    Cudd_RecursiveDeref( dd, gArg1 );
-//    Cudd_RecursiveDeref( dd, gArg2 );
-    Parse_StackFnPush( pStackFn,  gFunc );
-    return gFunc;
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
diff --git a/src/bdd/parse/parseInt.h b/src/bdd/parse/parseInt.h
index 17f48375..6e6c49b0 100644
--- a/src/bdd/parse/parseInt.h
+++ b/src/bdd/parse/parseInt.h
@@ -47,18 +47,18 @@ typedef struct ParseStackOpStruct    Parse_StackOp_t;    // the operation stack
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                       MACRO DEFINITIONS                          ///
+///                       MACRO DEFITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /*=== parseStack.c =============================================================*/
 extern Parse_StackFn_t *  Parse_StackFnStart  ( int nDepth );
 extern bool               Parse_StackFnIsEmpty( Parse_StackFn_t * p );
-extern void               Parse_StackFnPush   ( Parse_StackFn_t * p, void * bFunc );
-extern void *             Parse_StackFnPop    ( Parse_StackFn_t * p );
+extern void               Parse_StackFnPush   ( Parse_StackFn_t * p, DdNode * bFunc );
+extern DdNode *           Parse_StackFnPop    ( Parse_StackFn_t * p );
 extern void               Parse_StackFnFree   ( Parse_StackFn_t * p );
 
 extern Parse_StackOp_t *  Parse_StackOpStart  ( int nDepth );
@@ -67,8 +67,7 @@ extern void               Parse_StackOpPush   ( Parse_StackOp_t * p, int Oper );
 extern int                Parse_StackOpPop    ( Parse_StackOp_t * p );
 extern void               Parse_StackOpFree   ( Parse_StackOp_t * p );
 
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
+#endif
diff --git a/src/bdd/parse/parseStack.c b/src/bdd/parse/parseStack.c
index cd7cd7e3..8329070e 100644
--- a/src/bdd/parse/parseStack.c
+++ b/src/bdd/parse/parseStack.c
@@ -24,7 +24,7 @@
 
 struct ParseStackFnStruct
 {
-    void **     pData;        // the array of elements
+    DdNode **     pData;        // the array of elements
     int           Top;          // the index
     int           Size;         // the stack size
 };
@@ -37,7 +37,7 @@ struct ParseStackOpStruct
 };
 
 ////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
+///                     FUNCTION DEFITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
 /**Function*************************************************************
@@ -56,7 +56,7 @@ Parse_StackFn_t * Parse_StackFnStart( int nDepth )
     Parse_StackFn_t * p;
     p = ALLOC( Parse_StackFn_t, 1 );
     memset( p, 0, sizeof(Parse_StackFn_t) );
-    p->pData = ALLOC( void *, nDepth );
+    p->pData = ALLOC( DdNode *, nDepth );
     p->Size = nDepth;
     return p;
 }
@@ -88,7 +88,7 @@ bool Parse_StackFnIsEmpty( Parse_StackFn_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-void Parse_StackFnPush( Parse_StackFn_t * p, void * bFunc )
+void Parse_StackFnPush( Parse_StackFn_t * p, DdNode * bFunc )
 {
     if ( p->Top >= p->Size )
     {
@@ -109,7 +109,7 @@ void Parse_StackFnPush( Parse_StackFn_t * p, void * bFunc )
   SeeAlso     []
 
 ***********************************************************************/
-void * Parse_StackFnPop( Parse_StackFn_t * p )
+DdNode * Parse_StackFnPop( Parse_StackFn_t * p )
 {
     if ( p->Top == 0 )
     {
diff --git a/src/bdd/reo/module.make b/src/bdd/reo/module.make
index 3a636980..7eb41e0e 100644
--- a/src/bdd/reo/module.make
+++ b/src/bdd/reo/module.make
@@ -1,7 +1,6 @@
 SRC +=    src/bdd/reo/reoApi.c \
     src/bdd/reo/reoCore.c \
     src/bdd/reo/reoProfile.c \
-    src/bdd/reo/reoShuffle.c \
     src/bdd/reo/reoSift.c \
     src/bdd/reo/reoSwap.c \
     src/bdd/reo/reoTransfer.c \
diff --git a/src/bdd/reo/reo.h b/src/bdd/reo/reo.h
index 1a31242a..7e4be855 100644
--- a/src/bdd/reo/reo.h
+++ b/src/bdd/reo/reo.h
@@ -19,16 +19,10 @@
 #ifndef __REO_H__
 #define __REO_H__
 
-#ifdef __cplusplus
-extern "C" {
-#endif
-
 #include <stdio.h>
 #include <stdlib.h>
 #include "extra.h"
 
-//#pragma warning( disable : 4514 )
-
 ////////////////////////////////////////////////////////////////////////
 ///                     MACRO DEFINITIONS                            ///
 ////////////////////////////////////////////////////////////////////////
@@ -93,9 +87,9 @@ struct _reo_plane
 struct _reo_hash
 {
     int         Sign;            // signature of the current cache operation
-    reo_unit *  Arg1;            // the first argument
-    reo_unit *  Arg2;            // the second argument
-    reo_unit *  Arg3;            // the third argument
+    unsigned    Arg1;            // the first argument
+    unsigned    Arg2;            // the second argument
+    unsigned    Arg3;            // the second argument
 };
 
 struct _reo_man
@@ -172,8 +166,8 @@ struct _reo_man
 
 // used to manipulate units
 #define Unit_Regular(u)     ((reo_unit *)((unsigned long)(u) & ~01))
-#define Unit_Not(u)         ((reo_unit *)((unsigned long)(u) ^ 01))
-#define Unit_NotCond(u,c)   ((reo_unit *)((unsigned long)(u) ^ (c)))
+#define Unit_Not(u)         ((reo_unit *)((long)(u) ^ 01))
+#define Unit_NotCond(u,c)   ((reo_unit *)((long)(u) ^ (c)))
 #define Unit_IsConstant(u)  ((int)((u)->lev == REO_CONST_LEVEL))
 
 ////////////////////////////////////////////////////////////////////////
@@ -221,12 +215,8 @@ extern DdNode *   Extra_ReorderCudd( DdManager * dd, DdNode * aFunc, int pPermut
 extern int        Extra_bddReorderTest( DdManager * dd, DdNode * bF ); 
 extern int        Extra_addReorderTest( DdManager * dd, DdNode * aF ); 
 
-#ifdef __cplusplus
-}
-#endif
-
-#endif
-
 ////////////////////////////////////////////////////////////////////////
 ///                         END OF FILE                              ///
 ////////////////////////////////////////////////////////////////////////
+
+#endif
diff --git a/src/bdd/reo/reoProfile.c b/src/bdd/reo/reoProfile.c
index 84a0bc19..b38575f0 100644
--- a/src/bdd/reo/reoProfile.c
+++ b/src/bdd/reo/reoProfile.c
@@ -330,7 +330,7 @@ void reoProfileWidthPrint( reo_man * p )
              WidthMax = p->pPlanes[i].statsWidth;
         TotalWidth += p->pPlanes[i].statsWidth;
     }
-    assert( p->nWidthCur == TotalWidth );
+    assert( p->nWidthCur = TotalWidth );
     printf( "WIDTH:  " );
     printf( "Maximum = %5d.  ", WidthMax );
     printf( "Total = %7d.  ", p->nWidthCur );
diff --git a/src/bdd/reo/reoShuffle.c b/src/bdd/reo/reoShuffle.c
deleted file mode 100644
index 8dab67a4..00000000
--- a/src/bdd/reo/reoShuffle.c
+++ /dev/null
@@ -1,224 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [reoShuffle.c]
-
-  PackageName [REO: A specialized DD reordering engine.]
-
-  Synopsis    [Implementation of the two-variable swap.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - October 15, 2002.]
-
-  Revision    [$Id: reoShuffle.c,v 1.0 2002/15/10 03:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "reo.h"
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DEFINITIONS                          ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure is similar to Cudd_ShuffleHeap() and Cudd_bddPermute().]
-
-  Description [The first argument is the REO manager. The 2nd/3d
-  arguments are the function and its CUDD manager. The last argument
-  is the permutation to be implemented. The i-th entry of the permutation 
-  array contains the index of the variable that should be brought to the 
-  i-th level.  The size of the array should be equal or greater to 
-  the number of variables currently in use (that is, the size of CUDD
-  manager and the size of REO manager).]
-
-  SideEffects [Note that the resulting BDD is not referenced.]
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * reoShuffle( reo_man * p, DdManager * dd, DdNode * bFunc, int * pPerm, int * pPermInv )
-{
-    DdNode * bFuncRes = NULL;
-    int i, k, v;
-
-    if ( Cudd_IsConstant(bFunc) )
-        return bFunc;
-
-    // set the initial parameters
-    p->dd    = dd;
-    p->nSupp = Cudd_SupportSize( dd, bFunc );
-    p->nTops = 1;
-//    p->nNodesBeg = Cudd_DagSize( bFunc );
-
-    // set the starting permutation
-    for ( i = 0; i < p->nSupp; i++ )
-    {
-        p->pOrderInt[i] = i;
-        p->pMapToPlanes[ dd->invperm[i] ] = i;
-        p->pMapToDdVarsFinal[i] = dd->invperm[i];
-    }
-
-    // set the initial parameters
-    p->nUnitsUsed = 0;
-    p->nNodesCur  = 0;
-    p->fThisIsAdd = 0;
-    p->Signature++;
-
-    // transfer the function from the CUDD package into REO's internal data structure
-    p->pTops[0] = reoTransferNodesToUnits_rec( p, bFunc );
-//    assert( p->nNodesBeg == p->nNodesCur );
-
-    // reorder one variable at a time
-    for ( i = 0; i < p->nSupp; i++ )
-    {
-        if ( p->pOrderInt[i] == pPerm[i] )
-            continue;
-        // find where is variable number pPerm[i]
-        for ( k = i + 1; k < p->nSupp; k++ )
-            if ( pPerm[i] == p->pOrderInt[k] )
-                break;
-        if ( k == p->nSupp )
-        {
-            printf( "reoShuffle() Error: Cannot find a variable.\n" );
-            goto finish;
-        }
-        // move the variable up
-        for ( v = k - 1; v >= i; v-- )
-        {
-            reoReorderSwapAdjacentVars( p, v, 1 );
-            // check if the number of nodes is not too large
-            if ( p->nNodesCur > 10000 )
-            {
-                printf( "reoShuffle() Error: BDD size is too large.\n" );
-                goto finish;
-            }
-        }
-        assert( p->pOrderInt[i] == pPerm[i] );
-    }
-
-    // set the initial parameters
-    p->nRefNodes  = 0;
-    p->nNodesCur  = 0;
-    p->Signature++;
-    // transfer the BDDs from REO's internal data structure to CUDD
-    bFuncRes = reoTransferUnitsToNodes_rec( p, p->pTops[0] ); Cudd_Ref( bFuncRes );
-    // undo the DDs referenced for storing in the cache
-    for ( i = 0; i < p->nRefNodes; i++ )
-        Cudd_RecursiveDeref( dd, p->pRefNodes[i] );
-
-    // verify zero refs of the terminal nodes
-//    assert( reoRecursiveDeref( p->pTops[0] ) );
-//    assert( reoCheckZeroRefs( &(p->pPlanes[p->nSupp]) ) );
-
-    // perform verification
-    if ( p->fVerify )
-    {
-        DdNode * bFuncPerm;
-        bFuncPerm = Cudd_bddPermute( dd, bFunc, pPermInv );  Cudd_Ref( bFuncPerm );
-        if ( bFuncPerm != bFuncRes )
-        {
-            printf( "REO: Internal verification has failed!\n" );
-            fflush( stdout );
-        }
-        Cudd_RecursiveDeref( dd, bFuncPerm );
-    }
-
-    // recycle the data structure
-    for ( i = 0; i <= p->nSupp; i++ )
-        reoUnitsRecycleUnitList( p, p->pPlanes + i );
-
-finish :
-    if ( bFuncRes )
-        Cudd_Deref( bFuncRes );
-    return bFuncRes;
-}
-
-
-
-/**Function*************************************************************
-
-  Synopsis    [Reorders the DD using REO and CUDD.]
-
-  Description [This function can be used to test the performance of the reordering package.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Extra_ShuffleTest( reo_man * pReo, DdManager * dd, DdNode * Func )
-{
-//    extern int runtime1, runtime2;
-
-    DdNode * Temp, * bRemap;
-    int nSuppSize, OffSet, Num, i, clk;
-    int pOrder[1000], pOrderInv[1000];
-    assert( dd->size < 1000 );
-
-    srand( 0x12341234 );
-    nSuppSize = Cudd_SupportSize( dd, Func );
-    if ( nSuppSize < 2 )
-        return;
-
-    for ( i = 0; i < nSuppSize; i++ )
-        pOrder[i] = i;
-    for ( i = 0; i < 120; i++ )
-    {
-        OffSet = rand() % (nSuppSize - 1);
-        Num = pOrder[OffSet];
-        pOrder[OffSet] = pOrder[OffSet+1];
-        pOrder[OffSet+1] = Num;
-    }
-    for ( i = 0; i < nSuppSize; i++ )
-        pOrderInv[pOrder[i]] = i;
-
-/*
-    printf( "Permutation: " );
-    for ( i = 0; i < nSuppSize; i++ )
-        printf( "%d ", pOrder[i] );
-    printf( "\n" );
-    printf( "Inverse permutation: " );
-    for ( i = 0; i < nSuppSize; i++ )
-        printf( "%d ", pOrderInv[i] );
-    printf( "\n" );
-*/
-
-    // create permutation
-//    Extra_ReorderSetVerification( pReo, 1 );
-    bRemap = Extra_bddRemapUp( dd, Func );  Cudd_Ref( bRemap );
-
-clk = clock();
-    Temp  = reoShuffle( pReo, dd, bRemap, pOrder, pOrderInv );  Cudd_Ref( Temp );
-//runtime1 += clock() - clk;
-
-//printf( "Initial = %d. Final = %d.\n", Cudd_DagSize(bRemap), Cudd_DagSize(Temp)  );
-
-    {
-        DdNode * bFuncPerm;
-clk = clock();
-        bFuncPerm = Cudd_bddPermute( dd, bRemap, pOrderInv );  Cudd_Ref( bFuncPerm );
-//runtime2 += clock() - clk;
-        if ( bFuncPerm != Temp )
-        {
-            printf( "REO: Internal verification has failed!\n" );
-            fflush( stdout );
-        }
-        Cudd_RecursiveDeref( dd, bFuncPerm );
-    }
-
-    Cudd_RecursiveDeref( dd, Temp );
-    Cudd_RecursiveDeref( dd, bRemap );
-}
-
-
-////////////////////////////////////////////////////////////////////////
-///                         END OF FILE                              ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/bdd/reo/reoSwap.c b/src/bdd/reo/reoSwap.c
index 4afa650c..cb730d8e 100644
--- a/src/bdd/reo/reoSwap.c
+++ b/src/bdd/reo/reoSwap.c
@@ -271,9 +271,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                    HKey = (HKey+1) % p->nTableSize );
             assert( p->HTable[HKey].Sign != p->Signature );
             p->HTable[HKey].Sign = p->Signature;
-            p->HTable[HKey].Arg1 = pUnitE;
-            p->HTable[HKey].Arg2 = pUnitT;
-            p->HTable[HKey].Arg3 = pUnit;
+            p->HTable[HKey].Arg1 = (unsigned)pUnitE;
+            p->HTable[HKey].Arg2 = (unsigned)pUnitT;
+            p->HTable[HKey].Arg3 = (unsigned)pUnit;
 
             nNodesUpMovedDown++;
 
@@ -512,10 +512,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew1E, pNew1T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pNew1E && p->HTable[HKey].Arg2 == pNew1T )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pNew1E && p->HTable[HKey].Arg2 == (unsigned)pNew1T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane20 = p->HTable[HKey].Arg3;
+                pNewPlane20 = (reo_unit *)p->HTable[HKey].Arg3;
                 assert( pNewPlane20->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -549,9 +549,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = pNew1E;
-                p->HTable[HKey].Arg2 = pNew1T;
-                p->HTable[HKey].Arg3 = pNewPlane20;
+                p->HTable[HKey].Arg1 = (unsigned)pNew1E;
+                p->HTable[HKey].Arg2 = (unsigned)pNew1T;
+                p->HTable[HKey].Arg3 = (unsigned)pNewPlane20;
 
                 nNodesUnrefAdded++;
                         
@@ -637,10 +637,10 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
             for (  HKey = hashKey3(p->Signature, pNew2E, pNew2T, p->nTableSize);
                    p->HTable[HKey].Sign == p->Signature;
                    HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pNew2E && p->HTable[HKey].Arg2 == pNew2T )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pNew2E && p->HTable[HKey].Arg2 == (unsigned)pNew2T )
             { // the entry is present 
                 // assign this entry
-                pNewPlane21 = p->HTable[HKey].Arg3;
+                pNewPlane21 = (reo_unit *)p->HTable[HKey].Arg3;
                 assert( pNewPlane21->lev == lev1 );
                 fFound = 1;
                 p->HashSuccess++;
@@ -675,9 +675,9 @@ double reoReorderSwapAdjacentVars( reo_man * p, int lev0, int fMovingUp )
                 // add this entry to cache
                 assert( p->HTable[HKey].Sign != p->Signature );
                 p->HTable[HKey].Sign = p->Signature;
-                p->HTable[HKey].Arg1 = pNew2E;
-                p->HTable[HKey].Arg2 = pNew2T;
-                p->HTable[HKey].Arg3 = pNewPlane21;
+                p->HTable[HKey].Arg1 = (unsigned)pNew2E;
+                p->HTable[HKey].Arg2 = (unsigned)pNew2T;
+                p->HTable[HKey].Arg3 = (unsigned)pNewPlane21;
 
                 nNodesUnrefAdded++;
 
diff --git a/src/bdd/reo/reoTransfer.c b/src/bdd/reo/reoTransfer.c
index 65d31d01..752cd3d7 100644
--- a/src/bdd/reo/reoTransfer.c
+++ b/src/bdd/reo/reoTransfer.c
@@ -51,9 +51,9 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
     {
         // search cache - use linear probing
         for ( HKey = hashKey2(p->Signature,F,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == (reo_unit *)F )
+            if ( p->HTable[HKey].Arg1 == (unsigned)F )
             {
-                pUnit = p->HTable[HKey].Arg2;  
+                pUnit = (reo_unit*) p->HTable[HKey].Arg2;  
                 assert( pUnit );
                 // increment the edge counter
                 pUnit->n++;
@@ -93,8 +93,8 @@ reo_unit * reoTransferNodesToUnits_rec( reo_man * p, DdNode * F )
         // might have been used. Make sure that its signature is different.
         for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
         p->HTable[HKey].Sign = p->Signature;
-        p->HTable[HKey].Arg1 = (reo_unit *)F;
-        p->HTable[HKey].Arg2 = pUnit;
+        p->HTable[HKey].Arg1 = (unsigned)F;
+        p->HTable[HKey].Arg2 = (unsigned)pUnit;
     }
 
     // increment the counter of nodes
@@ -126,7 +126,7 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
     if ( pUnit->n != 1 )
     {
         for ( HKey = hashKey2(p->Signature,pUnit,p->nTableSize); p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize )
-            if ( p->HTable[HKey].Arg1 == pUnit )
+            if ( p->HTable[HKey].Arg1 == (unsigned)pUnit )
             {
                 bRes = (DdNode*) p->HTable[HKey].Arg2;  
                 assert( bRes );
@@ -179,8 +179,8 @@ DdNode * reoTransferUnitsToNodes_rec( reo_man * p, reo_unit * pUnit )
          // might have been used. Make sure that its signature is different.
          for ( ; p->HTable[HKey].Sign == p->Signature; HKey = (HKey+1) % p->nTableSize );
          p->HTable[HKey].Sign = p->Signature;
-         p->HTable[HKey].Arg1 = pUnit;
-         p->HTable[HKey].Arg2 = (reo_unit *)bRes;  
+         p->HTable[HKey].Arg1 = (unsigned)pUnit;
+         p->HTable[HKey].Arg2 = (unsigned)bRes;  
 
          // add the DD to the referenced DD list in order to be able to store it in cache
          p->pRefNodes[p->nRefNodes++] = bRes;  Cudd_Ref( bRes );