Version abc80130

1 files changed, 0 insertions, 1230 deletions

diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
deleted file mode 100644
index 29382bfb..00000000
--- a/src/misc/extra/extraBddCas.c
+++ /dev/null
@@ -1,1230 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [extraBddCas.c]
-
-  PackageName [extra]
-
-  Synopsis    [Procedures related to LUT cascade synthesis.]
-
-  Author      [Alan Mishchenko]
-
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 2.0. Started - September 1, 2003.]
-
-  Revision    [$Id: extraBddCas.c,v 1.0 2003/05/21 18:03:50 alanmi Exp $]
-
-***********************************************************************/
-
-#include "extra.h"
-
-/*---------------------------------------------------------------------------*/
-/* Constant declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Stucture declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Type declarations                                                         */
-/*---------------------------------------------------------------------------*/
-
-// the table to store cofactor operations
-#define _TABLESIZE_COF  51113
-typedef struct 
-{
-    unsigned Sign;  
-    DdNode * Arg1;  
-} _HashEntry_cof;
-_HashEntry_cof HHTable1[_TABLESIZE_COF];
-
-// the table to store the result of computation of the number of minterms
-#define _TABLESIZE_MINT  15113
-typedef struct 
-{
-    DdNode * Arg1;  
-    unsigned Arg2;  
-    unsigned Res;  
-} _HashEntry_mint;
-_HashEntry_mint HHTable2[_TABLESIZE_MINT];
-
-typedef struct 
-{
-    int      nEdges;  // the number of in-coming edges of the node
-    DdNode * bSum;    // the sum of paths of the incoming edges
-} traventry;
-
-// the signature used for hashing
-static unsigned s_Signature = 1;
-
-static int s_CutLevel = 0;
-
-/*---------------------------------------------------------------------------*/
-/* Variable declarations                                                     */
-/*---------------------------------------------------------------------------*/
-
-// because the proposed solution to the optimal encoding problem has exponential complexity
-// we limit the depth of the branch and bound procedure to 5 levels
-static int s_MaxDepth = 5;      
-
-static int s_nVarsBest;          // the number of vars in the best ordering
-static int s_VarOrderBest[32];   // storing the best ordering of vars in the "simple encoding"
-static int s_VarOrderCur[32];    // storing the current ordering of vars
- 
-// the place to store the supports of the encoded function
-static DdNode * s_Field[8][256]; // the size should be K, 2^K, where K is no less than MaxDepth
-static DdNode * s_Encoded;       // this is the original function
-static DdNode * s_VarAll;        // the set of all column variables
-static int s_MultiStart;         // the total number of encoding variables used
-// the array field now stores the supports
-
-static DdNode ** s_pbTemp;       // the temporary storage for the columns
-
-static int s_BackTracks;
-static int s_BackTrackLimit = 100;
-
-static DdNode * s_Terminal;      // the terminal value for counting minterms
-
-
-static int s_EncodingVarsLevel;
-
-
-/*---------------------------------------------------------------------------*/
-/* Macro declarations                                                        */
-/*---------------------------------------------------------------------------*/
-
-
-/**AutomaticStart*************************************************************/
-
-/*---------------------------------------------------------------------------*/
-/* Static function prototypes                                                */
-/*---------------------------------------------------------------------------*/
-
-static DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars );
-static void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level );
-// functions called from EvaluateEncodings_rec()
-static DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost );
-static DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost );
-unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll );
-static unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max );
-
-static void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited );
-static void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st_table * Visited, st_table * CutNodes );
-
-/**AutomaticEnd***************************************************************/
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of exported functions                                          */
-/*---------------------------------------------------------------------------*/
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the binary encoding of the set of function using the given vars.]
-
-  Description [Performs a straight binary encoding of the set of functions using 
-  the variable cubes formed from the given set of variables. ]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode * 
-Extra_bddEncodingBinary( 
-  DdManager * dd, 
-  DdNode ** pbFuncs,    // pbFuncs is the array of columns to be encoded
-  int nFuncs,           // nFuncs is the number of columns in the array
-  DdNode ** pbVars,     // pbVars is the array of variables to use for the codes
-  int nVars )           // nVars is the column multiplicity, [log2(nFuncs)]
-{
-    int i;
-    DdNode * bResult;
-    DdNode * bCube, * bTemp, * bProd;
-
-    assert( nVars >= Extra_Base2Log(nFuncs) );
-
-    bResult = b0;   Cudd_Ref( bResult );
-    for ( i = 0; i < nFuncs; i++ )
-    {
-        bCube   = Extra_bddBitsToCube( dd, i, nVars, pbVars, 1 );   Cudd_Ref( bCube );
-        bProd   = Cudd_bddAnd( dd, bCube, pbFuncs[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 );
-    }
-
-    Cudd_Deref( bResult );
-    return bResult;
-} /* end of Extra_bddEncodingBinary */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Solves the column encoding problem using a sophisticated method.]
-
-  Description [The encoding is based on the idea of deriving functions which 
-  depend on only one variable, which corresponds to the case of non-disjoint 
-  decompostion. It is assumed that the variables pCVars are ordered below the variables
-  representing the solumns, and the first variable pCVars[0] is the topmost one.]
-
-  SideEffects []
-
-  SeeAlso     [Extra_bddEncodingBinary]
-
-******************************************************************************/
-
-DdNode * 
-Extra_bddEncodingNonStrict( 
-  DdManager * dd, 
-  DdNode ** pbColumns,   // pbColumns is the array of columns to be encoded;
-  int nColumns,          // nColumns is the number of columns in the array
-  DdNode * bVarsCol,     // bVarsCol is the cube of variables on which the columns depend
-  DdNode ** pCVars,      // pCVars is the array of variables to use for the codes
-  int nMulti,            // nMulti is the column multiplicity, [log2(nColumns)]
-  int * pSimple )        // pSimple gets the number of code variables taken from the input varibles without change
-{
-    DdNode * bEncoded, * bResult;
-    int nVarsCol = Cudd_SupportSize(dd,bVarsCol);
-    long clk;
-
-    // cannot work with more that 32-bit codes
-    assert( nMulti < 32 );
-
-    // perform the preliminary encoding using the straight binary code
-    bEncoded = Extra_bddEncodingBinary( dd, pbColumns, nColumns, pCVars, nMulti );   Cudd_Ref( bEncoded );
-    //printf( "Node count = %d", Cudd_DagSize(bEncoded) );
-
-    // set the backgroup value for counting minterms
-    s_Terminal = b0;
-    // set the level of the encoding variables
-    s_EncodingVarsLevel = dd->invperm[pCVars[0]->index];
-
-    // the current number of backtracks
-    s_BackTracks = 0;
-    // the variables that are cofactored on the topmost level where everything starts (no vars)
-    s_Field[0][0] = b1;   
-    // the size of the best set of "simple" encoding variables found so far
-    s_nVarsBest   = 0;
-
-    // set the relation to be accessible to traversal procedures
-    s_Encoded = bEncoded;
-    // the set of all vars to be accessible to traversal procedures
-    s_VarAll  = bVarsCol;
-    // the column multiplicity
-    s_MultiStart  = nMulti;
-
-
-    clk = clock();
-    // find the simplest encoding
-    if ( nColumns > 2 )
-    EvaluateEncodings_rec( dd, bVarsCol, nVarsCol, nMulti, 1 );
-//    printf( "The number of backtracks = %d\n", s_BackTracks );
-//    s_EncSearchTime += clock() - clk;
-
-    // allocate the temporary storage for the columns
-    s_pbTemp = (DdNode **) malloc( nColumns * sizeof(DdNode *) );
-
-//    clk = clock();
-    bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
-//    s_EncComputeTime += clock() - clk;
-    
-    // delocate the preliminarily encoded set
-    Cudd_RecursiveDeref( dd, bEncoded );
-//    Cudd_RecursiveDeref( dd, aEncoded );
-
-    free( s_pbTemp );
-
-    *pSimple = s_nVarsBest;
-    Cudd_Deref( bResult );
-    return bResult;
-}
- 
-/**Function********************************************************************
-
-  Synopsis    [Collects the nodes under the cut and, for each node, computes the sum of paths leading to it from the root.]
-
-  Description [The table returned contains the set of BDD nodes pointed to under the cut
-  and, for each node, the BDD of the sum of paths leading to this node from the root
-  The sums of paths in the table are referenced. CutLevel is the first DD level 
-  considered to be under the cut.]
-
-  SideEffects []
-
-  SeeAlso     [Extra_bddNodePaths]
-
-******************************************************************************/
-st_table * Extra_bddNodePathsUnderCut( DdManager * dd, DdNode * bFunc, int CutLevel )
-{
-    st_table * Visited;  // temporary table to remember the visited nodes
-    st_table * CutNodes; // the result goes here
-    st_table * Result; // the result goes here
-    DdNode * aFunc;
-
-    s_CutLevel = CutLevel;
-
-    Result  = st_init_table(st_ptrcmp,st_ptrhash);
-    // the terminal cases
-    if ( Cudd_IsConstant( bFunc ) )
-    {
-        if ( bFunc == b1 )
-        {
-            st_insert( Result, (char*)b1, (char*)b1 );
-            Cudd_Ref( b1 );
-            Cudd_Ref( b1 );
-        }
-        else
-        {
-            st_insert( Result, (char*)b0, (char*)b0 );
-            Cudd_Ref( b0 );
-            Cudd_Ref( b0 );
-        }
-        return Result;
-    }
-
-    // create the ADD to simplify processing (no complemented edges)
-    aFunc = Cudd_BddToAdd( dd, bFunc );   Cudd_Ref( aFunc );
-
-    // Step 1: Start the tables and collect information about the nodes above the cut 
-    // this information tells how many edges point to each node
-    Visited  = st_init_table(st_ptrcmp,st_ptrhash);
-    CutNodes = st_init_table(st_ptrcmp,st_ptrhash);
-
-    CountNodeVisits_rec( dd, aFunc, Visited );
-
-    // Step 2: Traverse the BDD using the visited table and compute the sum of paths
-    CollectNodesAndComputePaths_rec( dd, aFunc, b1, Visited, CutNodes );
-
-    // at this point the table of cut nodes is ready and the table of visited is useless
-    {
-        st_generator * gen;
-        DdNode * aNode;
-        traventry * p;
-        st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
-        {
-            Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
-        }
-        st_free_table( Visited );
-    }
-
-    // go through the table CutNodes and create the BDD and the path to be returned
-    {
-        st_generator * gen;
-        DdNode * aNode, * bNode, * bSum;
-        st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) 
-        {
-            // aNode is not referenced, because aFunc is holding it
-            bNode = Cudd_addBddPattern( dd, aNode );  Cudd_Ref( bNode ); 
-            st_insert( Result, (char*)bNode, (char*)bSum );
-            // the new table takes both refs
-        }
-        st_free_table( CutNodes );
-    }
-
-    // dereference the ADD
-    Cudd_RecursiveDeref( dd, aFunc );
-
-    // return the table
-    return Result;
-
-} /* end of Extra_bddNodePathsUnderCut */
-
-/**Function********************************************************************
-
-  Synopsis    [Collects the nodes under the cut in the ADD starting from the given set of ADD nodes.]
-
-  Description [Takes the array, paNodes, of ADD nodes to start the traversal,
-  the array, pbCubes, of BDD cubes to start the traversal with in each node, 
-  and the number, nNodes, of ADD nodes and BDD cubes in paNodes and pbCubes. 
-  Returns the number of columns found. Fills in paNodesRes (pbCubesRes) 
-  with the set of ADD columns (BDD paths). These arrays should be allocated 
-  by the user.]
-
-  SideEffects []
-
-  SeeAlso     [Extra_bddNodePaths]
-
-******************************************************************************/
-int Extra_bddNodePathsUnderCutArray( DdManager * dd, DdNode ** paNodes, DdNode ** pbCubes, int nNodes, DdNode ** paNodesRes, DdNode ** pbCubesRes, int CutLevel )
-{
-    st_table * Visited;  // temporary table to remember the visited nodes
-    st_table * CutNodes; // the nodes under the cut go here
-    int i, Counter;
-
-    s_CutLevel = CutLevel;
-
-    // there should be some nodes
-    assert( nNodes > 0 );
-    if ( nNodes == 1 && Cudd_IsConstant( paNodes[0] ) )
-    {
-        if ( paNodes[0] == a1 )
-        {
-            paNodesRes[0] = a1;          Cudd_Ref( a1 );
-            pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
-        }
-        else
-        {
-            paNodesRes[0] = a0;          Cudd_Ref( a0 );
-            pbCubesRes[0] = pbCubes[0];  Cudd_Ref( pbCubes[0] );
-        }
-        return 1;
-    }
-
-    // Step 1: Start the table and collect information about the nodes above the cut 
-    // this information tells how many edges point to each node
-    CutNodes = st_init_table(st_ptrcmp,st_ptrhash);
-    Visited  = st_init_table(st_ptrcmp,st_ptrhash);
-
-    for ( i = 0; i < nNodes; i++ )
-        CountNodeVisits_rec( dd, paNodes[i], Visited );
-
-    // Step 2: Traverse the BDD using the visited table and compute the sum of paths
-    for ( i = 0; i < nNodes; i++ )
-        CollectNodesAndComputePaths_rec( dd, paNodes[i], pbCubes[i], Visited, CutNodes );
-
-    // at this point, the table of cut nodes is ready and the table of visited is useless
-    {
-        st_generator * gen;
-        DdNode * aNode;
-        traventry * p;
-        st_foreach_item( Visited, gen, (char**)&aNode, (char**)&p ) 
-        {
-            Cudd_RecursiveDeref( dd, p->bSum );
-            free( p );
-        }
-        st_free_table( Visited );
-    }
-
-    // go through the table CutNodes and create the BDD and the path to be returned
-    {
-        st_generator * gen;
-        DdNode * aNode, * bSum;
-        Counter = 0;
-        st_foreach_item( CutNodes, gen, (char**)&aNode, (char**)&bSum) 
-        {
-            paNodesRes[Counter] = aNode;   Cudd_Ref( aNode ); 
-            pbCubesRes[Counter] = bSum;
-            Counter++;
-        }
-        st_free_table( CutNodes );
-    }
-
-    // return the number of cofactors found
-    return Counter;
-
-} /* end of Extra_bddNodePathsUnderCutArray */
-
-/**Function*************************************************************
-
-  Synopsis    [Collects all the BDD nodes into the table.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void extraCollectNodes( DdNode * Func, st_table * tNodes )
-{
-    DdNode * FuncR;
-    FuncR = Cudd_Regular(Func);
-    if ( st_find_or_add( tNodes, (char*)FuncR, NULL ) )
-        return;
-    if ( cuddIsConstant(FuncR) )
-        return;
-    extraCollectNodes( cuddE(FuncR), tNodes );
-    extraCollectNodes( cuddT(FuncR), tNodes );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects all the nodes of one DD into the table.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-st_table * Extra_CollectNodes( DdNode * Func )
-{
-    st_table * tNodes;
-    tNodes = st_init_table( st_ptrcmp, st_ptrhash );
-    extraCollectNodes( Func, tNodes );
-    return tNodes;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Updates the topmost level from which the given node is referenced.]
-
-  Description [Takes the table which maps each BDD nodes (including the constants)
-  into the topmost level on which this node counts as a cofactor. Takes the topmost
-  level, on which this node counts as a cofactor (see Extra_ProfileWidthFast(). 
-  Takes the node, for which the table entry should be updated.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void extraProfileUpdateTopLevel( st_table * tNodeTopRef, int TopLevelNew, DdNode * node )
-{
-    int * pTopLevel;
-
-    if ( st_find_or_add( tNodeTopRef, (char*)node, (char***)&pTopLevel ) )
-    { // the node is already referenced
-        // the current top level should be updated if it is larger than the new level
-        if ( *pTopLevel > TopLevelNew ) 
-             *pTopLevel = TopLevelNew;
-    }
-    else
-    { // the node is not referenced
-        // its level should be set to the current new level
-        *pTopLevel = TopLevelNew;
-    }
-}
-/**Function*************************************************************
-
-  Synopsis    [Fast computation of the BDD profile.]
-
-  Description [The array to store the profile is given by the user and should
-  contain at least as many entries as there is the maximum of the BDD/ZDD
-  size of the manager PLUS ONE.
-  When we say that the widths of the DD on level L is W, we mean the following.
-  Let us create the cut between the level L-1 and the level L and count the number
-  of different DD nodes pointed to across the cut. This number is the width W.
-  From this it follows the on level 0, the width is equal to the number of external
-  pointers to the considered DDs. If there is only one DD, then the profile on 
-  level 0 is always 1. If this DD is rooted in the topmost variable, then the width
-  on level 1 is always 2, etc. The width at the level equal to dd->size is the
-  number of terminal nodes in the DD. (Because we consider the first level #0
-  and the last level #dd->size, the profile array should contain dd->size+1 entries.)
-  ]
-
-  SideEffects [This procedure will not work for BDDs w/ complement edges, only for ADDs and ZDDs]
-
-  SeeAlso     []
-
-***********************************************************************/
-int Extra_ProfileWidth( DdManager * dd, DdNode * Func, int * pProfile, int CutLevel )
-{
-    st_generator * gen;
-    st_table * tNodeTopRef; // this table stores the top level from which this node is pointed to
-    st_table * tNodes;
-    DdNode * node;
-    DdNode * nodeR;
-    int LevelStart, Limit;
-    int    i, size;
-    int WidthMax;
-  
-    // start the mapping table
-    tNodeTopRef = st_init_table(st_ptrcmp,st_ptrhash);
-    // add the topmost node to the profile
-    extraProfileUpdateTopLevel( tNodeTopRef, 0, Func );
-
-    // collect all nodes
-    tNodes = Extra_CollectNodes( Func );
-    // go though all the nodes and set the top level the cofactors are pointed from
-//    Cudd_ForeachNode( dd, Func, genDD, node )
-    st_foreach_item( tNodes, gen, (char**)&node, NULL )
-    {
-//        assert( Cudd_Regular(node) );  // this procedure works only with ADD/ZDD (not BDD w/ compl.edges)
-        nodeR = Cudd_Regular(node);
-        if ( cuddIsConstant(nodeR) )
-            continue;
-        // this node is not a constant - consider its cofactors
-        extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddE(nodeR) );
-        extraProfileUpdateTopLevel( tNodeTopRef, dd->perm[node->index]+1, cuddT(nodeR) );
-    }
-    st_free_table( tNodes );
-
-    // clean the profile
-    size = ddMax(dd->size, dd->sizeZ) + 1;
-    for ( i = 0; i < size; i++ ) 
-        pProfile[i] = 0;
-
-    // create the profile
-    st_foreach_item( tNodeTopRef, gen, (char**)&node, (char**)&LevelStart )
-    {
-        nodeR = Cudd_Regular(node);
-        Limit = (cuddIsConstant(nodeR))? dd->size: dd->perm[nodeR->index];
-        for ( i = LevelStart; i <= Limit; i++ )
-            pProfile[i]++;
-    }
-
-    if ( CutLevel != -1 && CutLevel != 0  )
-        size = CutLevel;
-
-    // get the max width
-    WidthMax = 0;
-    for ( i = 0; i < size; i++ ) 
-        if ( WidthMax < pProfile[i] )
-            WidthMax = pProfile[i];
-
-    // deref the table
-    st_free_table( tNodeTopRef );
-
-    return WidthMax;
-} /* end of Extra_ProfileWidth */
-
-
-/*---------------------------------------------------------------------------*/
-/* Definition of internal functions                                          */
-/*---------------------------------------------------------------------------*/
-
-/*---------------------------------------------------------------------------*/
-/* Definition of static functions                                            */
-/*---------------------------------------------------------------------------*/
-
-/**Function********************************************************************
-
-  Synopsis    [Computes the non-strict codes when evaluation is finished.]
-
-  Description [The information about the best code is stored in s_VarOrderBest,
-  which has s_nVarsBest entries.]
-
-  SideEffects [None]
-
-******************************************************************************/
-DdNode * CreateTheCodes_rec( DdManager * dd, DdNode * bEncoded, int Level, DdNode ** pCVars )
-// bEncoded is the preliminarily encoded set of columns
-// Level is the current level in the recursion
-// pCVars are the variables to be used for encoding
-{
-    DdNode * bRes;
-    if ( Level == s_nVarsBest )
-    { // the terminal case, when we need to remap the encoded function 
-        // from the preliminary encoded variables to the new ones
-        st_table * CutNodes;
-        int nCols;
-//        double nMints;
-/*
-#ifdef _DEBUG
-
-        {
-        DdNode * bTemp;
-        // make sure that the given number of variables is enough
-        bTemp  = Cudd_bddExistAbstract( dd, bEncoded, s_VarAll );           Cudd_Ref( bTemp );
-//        nMints = Cudd_CountMinterm( dd, bTemp, s_MultiStart );
-        nMints = Extra_CountMintermsSimple( bTemp, (1<<s_MultiStart) );
-        if ( nMints > Extra_Power2( s_MultiStart-Level ) ) 
-        {  // the number of minterms is too large to encode the columns 
-           // using the given minimum number of encoding variables
-            assert( 0 );
-        }
-        Cudd_RecursiveDeref( dd, bTemp );
-        }
-#endif
-*/
-        // get the columns to be re-encoded
-        CutNodes = Extra_bddNodePathsUnderCut( dd, bEncoded, s_EncodingVarsLevel );
-        // LUT size is the cut level because because the temporary encoding variables 
-        // are above the functional variables - this is not true!!!
-        // the temporary variables are below!
-
-        // put the entries from the table into the temporary array
-        { 
-            st_generator * gen;
-            DdNode * bColumn, * bCode;
-            nCols = 0;
-            st_foreach_item( CutNodes, gen, (char**)&bCode, (char**)&bColumn ) 
-            {
-                if ( bCode == b0 )
-                { // the unused part of the columns
-                    Cudd_RecursiveDeref( dd, bColumn );
-                    Cudd_RecursiveDeref( dd, bCode );
-                    continue;
-                }
-                else
-                {
-                    s_pbTemp[ nCols ] = bColumn; // takes ref
-                    Cudd_RecursiveDeref( dd, bCode );
-                    nCols++;
-                }
-            }
-            st_free_table( CutNodes );
-//            assert( nCols == (int)nMints );
-        }
-
-        // encode the columns
-        if ( s_MultiStart-Level == 0 ) // we reached the bottom level of recursion
-        {
-            assert( nCols       == 1 );
-//            assert( (int)nMints == 1 );
-            bRes = s_pbTemp[0];     Cudd_Ref( bRes );
-        }
-        else
-        {
-            bRes = Extra_bddEncodingBinary( dd, s_pbTemp, nCols, pCVars+Level, s_MultiStart-Level ); Cudd_Ref( bRes );
-        }
-
-        // deref the columns
-        {
-            int i;
-            for ( i = 0; i < nCols; i++ )
-                Cudd_RecursiveDeref( dd, s_pbTemp[i] );
-        }
-    }
-    else
-    {
-        // cofactor the problem as specified in the best solution
-        DdNode * bCof0,  * bCof1;
-        DdNode * bRes0,  * bRes1;
-        DdNode * bProd0, * bProd1;
-        DdNode * bTemp;
-        DdNode * bVarNext = dd->vars[ s_VarOrderBest[Level] ];
-
-        bCof0  = Cudd_Cofactor( dd, bEncoded,  Cudd_Not( bVarNext ) );   Cudd_Ref( bCof0 );
-        bCof1  = Cudd_Cofactor( dd, bEncoded,            bVarNext   );   Cudd_Ref( bCof1 );
-
-        // call recursively
-        bRes0 = CreateTheCodes_rec( dd, bCof0, Level+1, pCVars );  Cudd_Ref( bRes0 );
-        bRes1 = CreateTheCodes_rec( dd, bCof1, Level+1, pCVars );  Cudd_Ref( bRes1 );
-
-        Cudd_RecursiveDeref( dd, bCof0 );
-        Cudd_RecursiveDeref( dd, bCof1 );
-
-        // compose the result using the identity (bVarNext <=> pCVars[Level])  - this is wrong!
-        // compose the result as follows: x'y'F0 + xyF1
-        bProd0 = Cudd_bddAnd( dd, Cudd_Not(bVarNext), Cudd_Not(pCVars[Level]) );   Cudd_Ref( bProd0 );
-        bProd1 = Cudd_bddAnd( dd,          bVarNext ,          pCVars[Level]  );   Cudd_Ref( bProd1 );
-
-        bProd0 = Cudd_bddAnd( dd, bTemp = bProd0, bRes0 );   Cudd_Ref( bProd0 );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bRes0 );
-
-        bProd1 = Cudd_bddAnd( dd, bTemp = bProd1, bRes1 );   Cudd_Ref( bProd1 );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bRes1 );
-
-        bRes = Cudd_bddOr( dd, bProd0, bProd1 );             Cudd_Ref( bRes );
-
-        Cudd_RecursiveDeref( dd, bProd0 );
-        Cudd_RecursiveDeref( dd, bProd1 );
-    }
-    Cudd_Deref( bRes );
-    return bRes;
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Computes the current set of variables and counts the number of minterms.]
-
-  Description [Old implementation.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void EvaluateEncodings_rec( DdManager * dd, DdNode * bVarsCol, int nVarsCol, int nMulti, int Level )
-// bVarsCol is the set of remaining variables
-// nVarsCol is the number of remaining variables
-// nMulti is the number of encoding variables to be used
-// Level is the level of recursion, from which this function is called
-// if we successfully finish this procedure, Level also stands for how many encoding variabled we saved
-{
-    int i, k;
-    int nEntries = (1<<(Level-1)); // the number of entries in the field of the previous level
-    DdNode * bVars0, * bVars1; // the cofactors
-    unsigned nMint0, nMint1;   // the number of minterms
-    DdNode * bTempV;
-    DdNode * bVarTop;
-    int fBreak;
-
-
-    // there is no need to search above this level
-    if ( Level > s_MaxDepth )
-        return;
-
-    // if there are no variables left, quit the research
-    if ( bVarsCol == b1 )
-        return;
-
-    if ( s_BackTracks > s_BackTrackLimit )
-        return;
-
-    s_BackTracks++;
-
-    // otherwise, go through the remaining variables
-    for ( bTempV = bVarsCol; bTempV != b1; bTempV = cuddT(bTempV) )
-    {
-        // the currently tested variable
-        bVarTop = dd->vars[bTempV->index];
-
-        // put it into the array
-        s_VarOrderCur[Level-1] = bTempV->index;
-
-        // go through the entries and fill them out by cofactoring
-        fBreak = 0;
-        for ( i = 0; i < nEntries; i++ )
-        {
-            bVars0 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], Cudd_Not(bVarTop), &nMint0 );
-            Cudd_Ref( bVars0 );
-
-            if ( nMint0 > Extra_Power2( nMulti-1 ) ) 
-            {
-                // there is no way to encode - dereference and return
-                Cudd_RecursiveDeref( dd, bVars0 );
-                fBreak = 1;
-                break;
-            }
-
-            bVars1 = ComputeVarSetAndCountMinterms( dd, s_Field[Level-1][i], bVarTop, &nMint1 );
-            Cudd_Ref( bVars1 );
-
-            if ( nMint1 > Extra_Power2( nMulti-1 ) ) 
-            {
-                // there is no way to encode - dereference and return
-                Cudd_RecursiveDeref( dd, bVars0 );
-                Cudd_RecursiveDeref( dd, bVars1 );
-                fBreak = 1;
-                break;
-            }
-
-            // otherwise, add these two cofactors
-            s_Field[Level][2*i + 0] = bVars0; // takes ref
-            s_Field[Level][2*i + 1] = bVars1; // takes ref
-        } 
-
-        if ( !fBreak )
-        {
-            DdNode * bVarsRem;
-            // if we ended up here, it means that the cofactors w.r.t. variable bVarTop satisfy the condition
-            // save this situation
-            if ( s_nVarsBest < Level )
-            {
-                s_nVarsBest = Level;
-                // copy the variable assignment
-                for ( k = 0; k < Level; k++ )
-                    s_VarOrderBest[k] = s_VarOrderCur[k];
-            }
-
-            // call recursively
-            // get the new variable set
-            if ( nMulti-1 > 0 )
-            {
-                bVarsRem = Cudd_bddExistAbstract( dd, bVarsCol, bVarTop );   Cudd_Ref( bVarsRem );
-                EvaluateEncodings_rec( dd, bVarsRem, nVarsCol-1, nMulti-1, Level+1 );
-                Cudd_RecursiveDeref( dd, bVarsRem );
-            }
-        }
-
-        // deref the contents of the array
-        for ( k = 0; k < i; k++ )
-        {
-            Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 0] );
-            Cudd_RecursiveDeref( dd, s_Field[Level][2*k + 1] );
-        }
-
-        // if the solution is found, there is no need to continue
-        if ( s_nVarsBest == s_MaxDepth )
-            return;
-
-        // if the solution is found, there is no need to continue
-        if ( s_nVarsBest == s_MultiStart )
-            return;
-    }
-    // at this point, we have tried all possible directions in the space of variables
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Computes the current set of variables and counts the number of minterms.]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode * ComputeVarSetAndCountMinterms( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost )
-// takes bVars - the variables cofactored so far (some of them may be in negative polarity)
-// bVarTop - the topmost variable w.r.t. which to cofactor (may be in negative polarity)
-// returns the cost and the new set of variables (bVars & bVarTop)
-{
-    DdNode * bVarsRes;
-
-    // get the resulting set of variables
-    bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop );  Cudd_Ref( bVarsRes );
-
-    // increment signature before calling Cudd_CountCofactorMinterms()
-    s_Signature++;
-    *Cost = Extra_CountCofactorMinterms( dd, s_Encoded, bVarsRes, s_VarAll );
-
-    Cudd_Deref( bVarsRes );
-//    s_CountCalls++;
-    return bVarsRes;
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Computes the current set of variables and counts the number of minterms.]
-
-  Description [The old implementation, which is approximately 4 times slower.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode * ComputeVarSetAndCountMinterms2( DdManager * dd, DdNode * bVars, DdNode * bVarTop, unsigned * Cost )
-{
-    DdNode * bVarsRes;
-    DdNode * bCof, * bFun;
-
-    bVarsRes = Cudd_bddAnd( dd, bVars, bVarTop );             Cudd_Ref( bVarsRes );
-
-    bCof  = Cudd_Cofactor( dd, s_Encoded,  bVarsRes );        Cudd_Ref( bCof );
-    bFun  = Cudd_bddExistAbstract( dd, bCof, s_VarAll );      Cudd_Ref( bFun );
-    *Cost = (unsigned)Cudd_CountMinterm( dd, bFun, s_MultiStart );
-    Cudd_RecursiveDeref( dd, bFun );
-    Cudd_RecursiveDeref( dd, bCof );
-
-    Cudd_Deref( bVarsRes );
-//    s_CountCalls++;
-    return bVarsRes;
-}
-
-
-/**Function********************************************************************
-
-  Synopsis    [Counts the number of encoding minterms pointed to by the cofactor of the function.]
-
-  Description []
-
-  SideEffects [None]
-
-******************************************************************************/
-unsigned Extra_CountCofactorMinterms( DdManager * dd, DdNode * bFunc, DdNode * bVarsCof, DdNode * bVarsAll )
-// this function computes how many minterms depending on the encoding variables
-// are there in the cofactor of bFunc w.r.t. variables bVarsCof
-// bFunc is assumed to depend on variables s_VarsAll
-// the variables s_VarsAll should be ordered above the encoding variables
-{
-    unsigned HKey;
-    DdNode * bFuncR;
-
-    // if the function is zero, there are no minterms
-//    if ( bFunc == b0 )
-//        return 0;
-
-//    if ( st_lookup(Visited, (char*)bFunc, NULL) )
-//        return 0;
-
-//    HKey = hashKey2c( s_Signature, bFuncR );
-//    if ( HHTable1[HKey].Sign == s_Signature && HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
-//        return 0;
-
-
-    // check the hash-table 
-    bFuncR = Cudd_Regular(bFunc);
-//    HKey = hashKey2( s_Signature, bFuncR, _TABLESIZE_COF );
-    HKey = hashKey2( s_Signature, bFunc, _TABLESIZE_COF );
-    for ( ;  HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF )
-//        if ( HHTable1[HKey].Arg1 == bFuncR ) // this node is visited
-        if ( HHTable1[HKey].Arg1 == bFunc ) // this node is visited
-            return 0;
-
-
-    // if the function is already the code
-    if ( dd->perm[bFuncR->index] >= s_EncodingVarsLevel )
-    {
-//        st_insert(Visited, (char*)bFunc, NULL);
-
-//        HHTable1[HKey].Sign = s_Signature;
-//        HHTable1[HKey].Arg1 = bFuncR;
-
-        assert( HHTable1[HKey].Sign != s_Signature );
-        HHTable1[HKey].Sign = s_Signature;
-//        HHTable1[HKey].Arg1 = bFuncR;
-        HHTable1[HKey].Arg1 = bFunc;
-
-        return Extra_CountMintermsSimple( bFunc, (1<<s_MultiStart) );
-    }
-    else
-    {
-        DdNode * bFunc0,    * bFunc1;
-        DdNode * bVarsCof0, * bVarsCof1;
-        DdNode * bVarsCofR = Cudd_Regular(bVarsCof);
-        unsigned Res;
-
-        // get the levels
-        int LevelF = dd->perm[bFuncR->index];
-        int LevelC = cuddI(dd,bVarsCofR->index);
-        int LevelA = dd->perm[bVarsAll->index];
-
-        int LevelTop = LevelF;
-
-        if ( LevelTop > LevelC )
-             LevelTop = LevelC;
-
-        if ( LevelTop > LevelA )
-             LevelTop = LevelA;
-
-        // the top var in the function or in cofactoring vars always belongs to the set of all vars
-        assert( !( LevelTop == LevelF || LevelTop == LevelC ) || LevelTop == LevelA );
-
-        // cofactor the function
-        if ( LevelTop == LevelF )
-        {
-            if ( bFuncR != bFunc ) // bFunc is complemented 
-            {
-                bFunc0 = Cudd_Not( cuddE(bFuncR) );
-                bFunc1 = Cudd_Not( cuddT(bFuncR) );
-            }
-            else
-            {
-                bFunc0 = cuddE(bFuncR);
-                bFunc1 = cuddT(bFuncR);
-            }
-        }
-        else // bVars is higher in the variable order 
-            bFunc0 = bFunc1 = bFunc;
-
-        // cofactor the cube
-        if ( LevelTop == LevelC )
-        {
-            if ( bVarsCofR != bVarsCof ) // bFunc is complemented 
-            {
-                bVarsCof0 = Cudd_Not( cuddE(bVarsCofR) );
-                bVarsCof1 = Cudd_Not( cuddT(bVarsCofR) );
-            }
-            else
-            {
-                bVarsCof0 = cuddE(bVarsCofR);
-                bVarsCof1 = cuddT(bVarsCofR);
-            }
-        }
-        else // bVars is higher in the variable order 
-            bVarsCof0 = bVarsCof1 = bVarsCof;
-
-        // there are two cases: 
-        // (1) the top variable belongs to the cofactoring variables
-        // (2) the top variable does not belong to the cofactoring variables
-
-        // (1) the top variable belongs to the cofactoring variables
-        Res = 0;
-        if ( LevelTop == LevelC )
-        {
-            if ( bVarsCof1 == b0 ) // this is a negative cofactor
-            {
-                if ( bFunc0 != b0 )
-                Res = Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
-            }
-            else                        // this is a positive cofactor
-            {
-                if ( bFunc1 != b0 )
-                Res = Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
-            }
-        }
-        else
-        {
-            if ( bFunc0 != b0 )
-            Res += Extra_CountCofactorMinterms( dd, bFunc0, bVarsCof0, cuddT(bVarsAll) );
-            
-            if ( bFunc1 != b0 )
-            Res += Extra_CountCofactorMinterms( dd, bFunc1, bVarsCof1, cuddT(bVarsAll) );
-        }
-
-//        st_insert(Visited, (char*)bFunc, NULL);
-
-//        HHTable1[HKey].Sign = s_Signature;
-//        HHTable1[HKey].Arg1 = bFuncR;
-
-        // skip through the entries with the same signatures 
-        // (these might have been created at the time of recursive calls)
-        for ( ; HHTable1[HKey].Sign == s_Signature; HKey = (HKey+1) % _TABLESIZE_COF );
-        assert( HHTable1[HKey].Sign != s_Signature );
-        HHTable1[HKey].Sign = s_Signature;
-//        HHTable1[HKey].Arg1 = bFuncR;
-        HHTable1[HKey].Arg1 = bFunc;
-
-        return Res;
-    }
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Counts the number of minterms.]
-
-  Description [This function counts minterms for functions up to 32 variables
-  using a local cache. The terminal value (s_Termina) should be adjusted for
-  BDDs and ADDs.]
-
-  SideEffects [None]
-
-******************************************************************************/
-unsigned Extra_CountMintermsSimple( DdNode * bFunc, unsigned max )
-{
-    unsigned HKey;
-
-    // normalize
-    if ( Cudd_IsComplement(bFunc) )
-        return max - Extra_CountMintermsSimple( Cudd_Not(bFunc), max );
-
-    // now it is known that the function is not complemented
-    if ( cuddIsConstant(bFunc) )
-        return ((bFunc==s_Terminal)? 0: max);
-
-    // check cache
-    HKey = hashKey2( bFunc, max, _TABLESIZE_MINT );
-    if ( HHTable2[HKey].Arg1 == bFunc && HHTable2[HKey].Arg2 == max )
-        return HHTable2[HKey].Res;
-    else
-    {
-        // min = min0/2 + min1/2;
-        unsigned min = (Extra_CountMintermsSimple( cuddE(bFunc), max ) >> 1) +
-                       (Extra_CountMintermsSimple( cuddT(bFunc), max ) >> 1);
-
-        HHTable2[HKey].Arg1 = bFunc;
-        HHTable2[HKey].Arg2 = max;
-        HHTable2[HKey].Res  = min;
-
-        return min;
-    }
-}    /* end of Extra_CountMintermsSimple */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Visits the nodes.]
-
-  Description [Visits the nodes above the cut and the nodes pointed to below the cut;
-  collects the visited nodes, counts how many times each node is visited, and sets 
-  the path-sum to be the constant zero BDD.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void CountNodeVisits_rec( DdManager * dd, DdNode * aFunc, st_table * Visited )
-
-{
-    traventry * p;
-    char **slot;
-    if ( st_find_or_add(Visited, (char*)aFunc, &slot) )
-    { // the entry already exists
-        p = (traventry*) *slot;
-        // increment the counter of incoming edges
-        p->nEdges++;
-        return; 
-    }
-    // this node has not been visited
-    assert( !Cudd_IsComplement(aFunc) );
-
-    // create the new traversal entry
-    p = (traventry *) malloc( sizeof(traventry) );
-    // set the initial sum of edges to zero BDD
-    p->bSum = b0;   Cudd_Ref( b0 );
-    // set the starting number of incoming edges
-    p->nEdges = 1;
-    // set this entry into the slot
-    *slot = (char*)p;
-
-    // recur if the node is above the cut
-    if ( cuddI(dd,aFunc->index) < s_CutLevel )
-    {
-        CountNodeVisits_rec( dd, cuddE(aFunc), Visited );
-        CountNodeVisits_rec( dd, cuddT(aFunc), Visited );
-    }
-} /* end of CountNodeVisits_rec */
-
-
-/**Function********************************************************************
-
-  Synopsis    [Revisits the nodes and computes the paths.]
-
-  Description [This function visits the nodes above the cut having the goal of 
-  summing all the incomming BDD edges; when this function comes across the node 
-  below the cut, it saves this node in the CutNode table.]
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-void CollectNodesAndComputePaths_rec( DdManager * dd, DdNode * aFunc, DdNode * bCube, st_table * Visited, st_table * CutNodes )
-{    
-    // find the node in the visited table
-    DdNode * bTemp;
-    traventry * p;
-    char **slot;
-    if ( st_find_or_add(Visited, (char*)aFunc, &slot) )
-    { // the node is found
-        // get the pointer to the traversal entry
-        p = (traventry*) *slot;
-
-        // make sure that the counter of incoming edges is positive
-        assert( p->nEdges > 0 );
-
-        // add the cube to the currently accumulated cubes
-        p->bSum = Cudd_bddOr( dd, bTemp = p->bSum, bCube );  Cudd_Ref( p->bSum );
-        Cudd_RecursiveDeref( dd, bTemp );
-
-        // decrement the number of visits
-        p->nEdges--;
-
-        // if more visits to this node are expected, return
-        if ( p->nEdges ) 
-            return;
-        else // if ( p->nEdges == 0 )
-        { // this is the last visit - propagate the cube
-
-            // check where this node is
-            if ( cuddI(dd,aFunc->index) < s_CutLevel )
-            { // the node is above the cut
-                DdNode * bCube0, * bCube1;
-
-                // get the top-most variable
-                DdNode * bVarTop = dd->vars[aFunc->index];
-
-                // compute the propagated cubes
-                bCube0 = Cudd_bddAnd( dd, p->bSum, Cudd_Not( bVarTop ) );   Cudd_Ref( bCube0 );
-                bCube1 = Cudd_bddAnd( dd, p->bSum,           bVarTop   );   Cudd_Ref( bCube1 );
-
-                // call recursively
-                CollectNodesAndComputePaths_rec( dd, cuddE(aFunc), bCube0, Visited, CutNodes );
-                CollectNodesAndComputePaths_rec( dd, cuddT(aFunc), bCube1, Visited, CutNodes );
-
-                // dereference the cubes
-                Cudd_RecursiveDeref( dd, bCube0 );
-                Cudd_RecursiveDeref( dd, bCube1 );
-                return;
-            }
-            else
-            { // the node is below the cut
-                // add this node to the cut node table, if it is not yet there
-
-//                DdNode * bNode;
-//                bNode = Cudd_addBddPattern( dd, aFunc );  Cudd_Ref( bNode );
-                if ( st_find_or_add(CutNodes, (char*)aFunc, &slot) )
-                { // the node exists - should never happen
-                    assert( 0 );
-                }
-                *slot = (char*) p->bSum;   Cudd_Ref( p->bSum );
-                // the table takes the reference of bNode
-                return;
-            }
-        }
-    }
-
-    // the node does not exist in the visited table - should never happen
-    assert(0);
-
-} /* end of CollectNodesAndComputePaths_rec */
-
-
-
-////////////////////////////////////////////////////////////////////////
-///                           END OF FILE                            ///
-////////////////////////////////////////////////////////////////////////