extraBddCas.c

Go to the documentation of this file.

 
#include "extraBdd.h"
 
ABC_NAMESPACE_IMPL_START
 
 
/*---------------------------------------------------------------------------*/
/* 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                                                        */
/*---------------------------------------------------------------------------*/
 

 
/*---------------------------------------------------------------------------*/
/* 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 );

 
 
/*---------------------------------------------------------------------------*/
/* Definition of exported functions                                          */
/*---------------------------------------------------------------------------*/

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 >= Abc_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 */
 

 
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);
    abctime 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 = Abc_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 += Abc_Clock() - clk;
 
    // allocate the temporary storage for the columns
    s_pbTemp = (DdNode **)ABC_ALLOC( char, nColumns * sizeof(DdNode *) );
 
//  clk = Abc_Clock();
    bResult = CreateTheCodes_rec( dd, bEncoded, 0, pCVars );   Cudd_Ref( bResult );
//  s_EncComputeTime += Abc_Clock() - clk;
    
    // delocate the preliminarily encoded set
    Cudd_RecursiveDeref( dd, bEncoded );
//  Cudd_RecursiveDeref( dd, aEncoded );
 
    ABC_FREE( s_pbTemp );
 
    *pSimple = s_nVarsBest;
    Cudd_Deref( bResult );
    return bResult;
}
 
 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, (const char**)&aNode, (char**)&p )
        {
            Cudd_RecursiveDeref( dd, p->bSum );
            ABC_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, (const 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 */

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, (const char**)&aNode, (char**)&p )
        {
            Cudd_RecursiveDeref( dd, p->bSum );
            ABC_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, (const 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 */

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 );
}

 st__table * Extra_CollectNodes( DdNode * Func )
{
    st__table * tNodes;
    tNodes = st__init_table( st__ptrcmp, st__ptrhash );
    extraCollectNodes( Func, tNodes );
    return tNodes;
}

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;
    }
}

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, (const 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, (const 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                                            */
/*---------------------------------------------------------------------------*/

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, (const 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;
}

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
}

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;
}

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;
}
 

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;
    }
}

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

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 *) ABC_ALLOC( char, 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 */
 

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

ABC_NAMESPACE_IMPL_END