Version abc70217

1 files changed, 1230 insertions, 0 deletions

diff --git a/src/misc/extra/extraBddCas.c b/src/misc/extra/extraBddCas.c
new file mode 100644
index 00000000..29382bfb
--- /dev/null
+++ b/src/misc/extra/extraBddCas.c
@@ -0,0 +1,1230 @@
+/**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                            ///
+////////////////////////////////////////////////////////////////////////