Version abc80130

1 files changed, 0 insertions, 1263 deletions

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                            ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-