Version abc80507

1 files changed, 1286 insertions, 0 deletions

diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
new file mode 100644
index 00000000..cfe70d15
--- /dev/null
+++ b/src/aig/bbr/bbrImage.c
@@ -0,0 +1,1286 @@
+/**CFile****************************************************************
+
+  FileName    [bbrImage.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD-based reachability analysis.]
+
+  Synopsis    [Performs image computation.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: bbrImage.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "bbr.h"
+#include "mtr.h"
+
+/* 
+    The ideas implemented in this file are inspired by the paper:
+    Pankaj Chauhan, Edmund Clarke, Somesh Jha, Jim Kukula, Tom Shiple, 
+    Helmut Veith, Dong Wang. Non-linear Quantification Scheduling in 
+    Image Computation. ICCAD, 2001.
+*/
+
+/*---------------------------------------------------------------------------*/
+/* Constant declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Stucture declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+typedef struct Bbr_ImageNode_t_  Bbr_ImageNode_t;
+typedef struct Bbr_ImagePart_t_  Bbr_ImagePart_t;
+typedef struct Bbr_ImageVar_t_   Bbr_ImageVar_t;
+
+struct Bbr_ImageTree_t_
+{
+    Bbr_ImageNode_t *   pRoot;      // the root of quantification tree
+    Bbr_ImageNode_t *   pCare;      // the leaf node with the care set
+    DdNode *            bCareSupp;  // the cube to quantify from the care
+    int                 fVerbose;   // the verbosity flag
+    int                 nNodesMax;  // the max number of nodes in one iter
+    int                 nNodesMaxT; // the overall max number of nodes
+    int                 nIter;      // the number of iterations with this tree
+};
+
+struct Bbr_ImageNode_t_
+{
+    DdManager *         dd;         // the manager 
+    DdNode *            bCube;      // the cube to quantify
+    DdNode *            bImage;     // the partial image
+    Bbr_ImageNode_t *   pNode1;     // the first branch
+    Bbr_ImageNode_t *   pNode2;     // the second branch
+    Bbr_ImagePart_t *   pPart;      // the partition (temporary)
+};
+
+struct Bbr_ImagePart_t_
+{
+    DdNode *            bFunc;      // the partition
+    DdNode *            bSupp;      // the support of this partition
+    int                 nNodes;     // the number of BDD nodes
+    short               nSupp;      // the number of support variables
+    short               iPart;      // the number of this partition
+};
+
+struct Bbr_ImageVar_t_
+{
+    int                 iNum;       // the BDD index of this variable
+    DdNode *            bParts;     // the partition numbers
+    int                 nParts;     // the number of partitions
+};
+
+/*---------------------------------------------------------------------------*/
+/* Type declarations                                                         */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Variable declarations                                                     */
+/*---------------------------------------------------------------------------*/
+
+/*---------------------------------------------------------------------------*/
+/* Macro declarations                                                        */
+/*---------------------------------------------------------------------------*/
+
+#define BDD_BLOW_UP  1000000
+
+#define     b0     Cudd_Not((dd)->one)
+#define     b1              (dd)->one
+
+#ifndef PRB
+#define PRB(dd,f)       printf("%s = ", #f); Bbr_bddPrint(dd,f); printf("\n")
+#endif
+
+/**AutomaticStart*************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Static function prototypes                                                */
+/*---------------------------------------------------------------------------*/
+
+static Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare );
+static Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+    int nParts, Bbr_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVarsNs );
+static Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd, 
+    int nParts, Bbr_ImagePart_t ** pParts, 
+    int nVars,  Bbr_ImageVar_t ** pVars );
+static void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_BuildTreeNode( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop );
+static Bbr_ImageNode_t * Bbr_MergeTopNodes( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes );
+static void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode );
+static int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode );
+static int Bbr_FindBestVariable( DdManager * dd,
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars );
+static void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 );
+static Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 );
+
+static void Bbr_bddImagePrintLatchDependency( DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars );
+static void Bbr_bddImagePrintLatchDependencyOne( DdManager * dd, DdNode * bFunc, 
+    DdNode * bVarsCs, DdNode * bVarsNs, int iPart );
+
+static void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree );
+static void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int nOffset );
+
+static void Bbr_bddPrint( DdManager * dd, DdNode * F );
+
+/**AutomaticEnd***************************************************************/
+
+
+/*---------------------------------------------------------------------------*/
+/* Definition of exported functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the image computation using tree-based scheduling.]
+
+  Description [This procedure starts the image computation. It uses
+  the given care set to test-run the image computation and creates the 
+  quantification tree by scheduling variable quantifications. The tree can 
+  be used to compute images for other care sets without rescheduling.
+  In this case, Bbr_bddImageCompute() should be called.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageTree_t * Bbr_bddImageStart( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars, int fVerbose )   // the NS and parameter variables (not quantified!)
+{
+    Bbr_ImageTree_t * pTree;
+    Bbr_ImagePart_t ** pParts;
+    Bbr_ImageVar_t ** pVars;
+    Bbr_ImageNode_t ** pNodes, * pCare;
+    int fStop, v;
+
+    if ( fVerbose && dd->size <= 80 )
+        Bbr_bddImagePrintLatchDependency( dd, bCare, nParts, pbParts, nVars, pbVars );
+
+    // create variables, partitions and leaf nodes
+    pParts = Bbr_CreateParts( dd, nParts, pbParts, bCare );
+    pVars  = Bbr_CreateVars( dd, nParts + 1, pParts, nVars, pbVars );
+    pNodes = Bbr_CreateNodes( dd, nParts + 1, pParts, dd->size, pVars );
+    pCare  = pNodes[nParts];
+
+    // process the nodes
+    while ( Bbr_BuildTreeNode( dd, nParts + 1, pNodes, dd->size, pVars, &fStop ) );
+
+    // consider the case of BDD node blowup
+    if ( fStop )
+    {
+        for ( v = 0; v < dd->size; v++ )
+            if ( pVars[v] )
+                free( pVars[v] );
+        free( pVars );
+        for ( v = 0; v <= nParts; v++ )
+            if ( pNodes[v] )
+            {
+                Bbr_DeleteParts_rec( pNodes[v] );
+                Bbr_bddImageTreeDelete_rec( pNodes[v] );
+            }
+        free( pNodes );
+        free( pParts );
+        return NULL;
+    }
+
+    // make sure the variables are gone
+    for ( v = 0; v < dd->size; v++ )
+        assert( pVars[v] == NULL );
+    FREE( pVars );
+    
+    // create the tree
+    pTree = ALLOC( Bbr_ImageTree_t, 1 );
+    memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
+    pTree->pCare = pCare;
+    pTree->fVerbose = fVerbose;
+
+    // merge the topmost nodes
+    while ( (pTree->pRoot = Bbr_MergeTopNodes( dd, nParts + 1, pNodes )) == NULL );
+
+    // make sure the nodes are gone
+    for ( v = 0; v < nParts + 1; v++ )
+        assert( pNodes[v] == NULL );
+    FREE( pNodes );
+
+//    if ( fVerbose )
+//        Bbr_bddImagePrintTree( pTree );
+
+    // set the support of the care set
+    pTree->bCareSupp = Cudd_Support( dd, bCare );  Cudd_Ref( pTree->bCareSupp );
+
+    // clean the partitions
+    Bbr_DeleteParts_rec( pTree->pRoot );
+    FREE( pParts );
+    return pTree;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare )
+{
+    DdManager * dd = pTree->pCare->dd;
+    DdNode * bSupp, * bRem;
+
+    pTree->nIter++;
+
+    // make sure the supports are okay
+    bSupp = Cudd_Support( dd, bCare );        Cudd_Ref( bSupp );
+    if ( bSupp != pTree->bCareSupp )
+    {
+        bRem = Cudd_bddExistAbstract( dd, bSupp, pTree->bCareSupp );  Cudd_Ref( bRem );
+        if ( bRem != b1 )
+        {
+printf( "Original care set support: " );
+PRB( dd, pTree->bCareSupp );
+printf( "Current care set support: " );
+PRB( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bSupp );
+            Cudd_RecursiveDeref( dd, bRem );
+            printf( "The care set depends on some vars that were not in the care set during scheduling.\n" );
+            return NULL;
+        }
+        Cudd_RecursiveDeref( dd, bRem );
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+
+    // remove the previous image
+    Cudd_RecursiveDeref( dd, pTree->pCare->bImage );
+    pTree->pCare->bImage = bCare;   Cudd_Ref( bCare );
+
+    // compute the image
+    pTree->nNodesMax = 0;
+    if ( !Bbr_bddImageCompute_rec( pTree, pTree->pRoot ) )
+        return NULL;
+    if ( pTree->nNodesMaxT < pTree->nNodesMax )
+        pTree->nNodesMaxT = pTree->nNodesMax;
+
+//    if ( pTree->fVerbose )
+//        printf( "Iter %2d : Max nodes = %5d.\n", pTree->nIter, pTree->nNodesMax );
+    return pTree->pRoot->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree )
+{
+    if ( pTree->bCareSupp )
+        Cudd_RecursiveDeref( pTree->pRoot->dd, pTree->bCareSupp );
+    Bbr_bddImageTreeDelete_rec( pTree->pRoot );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reads the image from the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageRead( Bbr_ImageTree_t * pTree )
+{
+    return pTree->pRoot->bImage;
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of internal functions                                          */
+/*---------------------------------------------------------------------------*/
+
+/**Function********************************************************************
+
+  Synopsis    [Outputs the BDD in a readable format.]
+
+  Description []
+
+  SideEffects [None]
+
+  SeeAlso     []
+
+******************************************************************************/
+void Bbr_bddPrint( DdManager * dd, DdNode * F )
+{
+    DdGen * Gen;
+    int * Cube;
+    CUDD_VALUE_TYPE Value;
+    int nVars = dd->size;
+    int fFirstCube = 1;
+    int i;
+
+    if ( F == NULL )
+    {
+        printf("NULL");
+        return;
+    }
+    if ( F == b0 )
+    {
+        printf("Constant 0");
+        return;
+    }
+    if ( F == b1 )
+    {
+        printf("Constant 1");
+        return;
+    }
+
+    Cudd_ForeachCube( dd, F, Gen, Cube, Value )
+    {
+        if ( fFirstCube )
+            fFirstCube = 0;
+        else
+//          Output << " + ";
+            printf( " + " );
+
+        for ( i = 0; i < nVars; i++ )
+            if ( Cube[i] == 0 )
+                printf( "[%d]'", i );
+//              printf( "%c'", (char)('a'+i) );
+            else if ( Cube[i] == 1 )
+                printf( "[%d]", i );
+//              printf( "%c", (char)('a'+i) );
+    }
+
+//  printf("\n");
+}
+
+/*---------------------------------------------------------------------------*/
+/* Definition of static Functions                                            */
+/*---------------------------------------------------------------------------*/
+
+/**Function*************************************************************
+
+  Synopsis    [Creates partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImagePart_t ** Bbr_CreateParts( DdManager * dd,
+    int nParts, DdNode ** pbParts, DdNode * bCare )
+{
+    Bbr_ImagePart_t ** pParts;
+    int i;
+
+    // start the partitions
+    pParts = ALLOC( Bbr_ImagePart_t *, nParts + 1 );
+    // create structures for each variable
+    for ( i = 0; i < nParts; i++ )
+    {
+        pParts[i] = ALLOC( Bbr_ImagePart_t, 1 );
+        pParts[i]->bFunc  = pbParts[i];                           Cudd_Ref( pParts[i]->bFunc );
+        pParts[i]->bSupp  = Cudd_Support( dd, pParts[i]->bFunc ); Cudd_Ref( pParts[i]->bSupp );
+        pParts[i]->nSupp  = Cudd_SupportSize( dd, pParts[i]->bSupp );
+        pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+        pParts[i]->iPart  = i;
+    }
+    // add the care set as the last partition
+    pParts[nParts] = ALLOC( Bbr_ImagePart_t, 1 );
+    pParts[nParts]->bFunc = bCare;                                     Cudd_Ref( pParts[nParts]->bFunc );
+    pParts[nParts]->bSupp = Cudd_Support( dd, pParts[nParts]->bFunc ); Cudd_Ref( pParts[nParts]->bSupp );
+    pParts[nParts]->nSupp = Cudd_SupportSize( dd, pParts[nParts]->bSupp );
+    pParts[nParts]->nNodes = Cudd_DagSize( pParts[nParts]->bFunc );
+    pParts[nParts]->iPart  = nParts;
+    return pParts;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageVar_t ** Bbr_CreateVars( DdManager * dd,
+    int nParts, Bbr_ImagePart_t ** pParts,
+    int nVars, DdNode ** pbVars )
+{
+    Bbr_ImageVar_t ** pVars;
+    DdNode ** pbFuncs;
+    DdNode * bCubeNs, * bSupp, * bParts, * bTemp, * bSuppTemp;
+    int nVarsTotal, iVar, p, Counter;
+
+    // put all the functions into one array
+    pbFuncs = ALLOC( DdNode *, nParts );
+    for ( p = 0; p < nParts; p++ )
+        pbFuncs[p] = pParts[p]->bSupp;
+    bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
+    FREE( pbFuncs );
+
+    // remove the NS vars
+    bCubeNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );        Cudd_Ref( bCubeNs );
+    bSupp = Cudd_bddExistAbstract( dd, bTemp = bSupp, bCubeNs );     Cudd_Ref( bSupp );
+    Cudd_RecursiveDeref( dd, bTemp );
+    Cudd_RecursiveDeref( dd, bCubeNs );
+
+    // get the number of I and CS variables to be quantified
+    nVarsTotal = Cudd_SupportSize( dd, bSupp );
+
+    // start the variables
+    pVars = ALLOC( Bbr_ImageVar_t *, dd->size );
+    memset( pVars, 0, sizeof(Bbr_ImageVar_t *) * dd->size );
+    // create structures for each variable
+    for ( bSuppTemp = bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        iVar = bSuppTemp->index;
+        pVars[iVar] = ALLOC( Bbr_ImageVar_t, 1 );
+        pVars[iVar]->iNum = iVar;
+        // collect all the parts this var belongs to
+        Counter = 0;
+        bParts = b1; Cudd_Ref( bParts );
+        for ( p = 0; p < nParts; p++ )
+            if ( Cudd_bddLeq( dd, pParts[p]->bSupp, dd->vars[bSuppTemp->index] ) )
+            {
+                bParts = Cudd_bddAnd( dd, bTemp = bParts, dd->vars[p] );  Cudd_Ref( bParts );
+                Cudd_RecursiveDeref( dd, bTemp );
+                Counter++;
+            }
+        pVars[iVar]->bParts = bParts; // takes ref
+        pVars[iVar]->nParts = Counter;
+    }
+    Cudd_RecursiveDeref( dd, bSupp );
+    return pVars;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t ** Bbr_CreateNodes( DdManager * dd, 
+    int nParts, Bbr_ImagePart_t ** pParts, 
+    int nVars,  Bbr_ImageVar_t ** pVars )
+{
+    Bbr_ImageNode_t ** pNodes;
+    Bbr_ImageNode_t * pNode;
+    DdNode * bTemp;
+    int i, v, iPart;
+/*
+    DdManager *         dd;       // the manager 
+    DdNode *            bCube;    // the cube to quantify
+    DdNode *            bImage;   // the partial image
+    Bbr_ImageNode_t * pNode1;   // the first branch
+    Bbr_ImageNode_t * pNode2;   // the second branch
+    Bbr_ImagePart_t * pPart;    // the partition (temporary)
+*/
+    // start the partitions
+    pNodes = ALLOC( Bbr_ImageNode_t *, nParts );
+    // create structures for each leaf nodes
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNodes[i] = ALLOC( Bbr_ImageNode_t, 1 );
+        memset( pNodes[i], 0, sizeof(Bbr_ImageNode_t) );
+        pNodes[i]->dd    = dd;
+        pNodes[i]->pPart = pParts[i];
+    }
+    // find the quantification cubes for each leaf node
+    for ( v = 0; v < nVars; v++ )
+    {
+        if ( pVars[v] == NULL )
+            continue;
+        assert( pVars[v]->nParts > 0 );
+        if ( pVars[v]->nParts > 1 )
+            continue;
+        iPart = pVars[v]->bParts->index;
+        if ( pNodes[iPart]->bCube == NULL )
+        {
+            pNodes[iPart]->bCube = dd->vars[v];   
+            Cudd_Ref( dd->vars[v] );
+        }
+        else
+        {
+            pNodes[iPart]->bCube = Cudd_bddAnd( dd, bTemp = pNodes[iPart]->bCube, dd->vars[v] );  
+            Cudd_Ref( pNodes[iPart]->bCube );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        // remove these  variables
+        Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+        FREE( pVars[v] );
+    }
+
+    // assign the leaf node images
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+        if ( pNode->bCube )
+        {
+            // update the partition
+            pParts[i]->bFunc = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bFunc, pNode->bCube );
+            Cudd_Ref( pParts[i]->bFunc );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the support the partition
+            pParts[i]->bSupp = Cudd_bddExistAbstract( dd, bTemp = pParts[i]->bSupp, pNode->bCube ); 
+            Cudd_Ref( pParts[i]->bSupp );
+            Cudd_RecursiveDeref( dd, bTemp );
+            // update the numbers
+            pParts[i]->nSupp  = Cudd_SupportSize( dd, pParts[i]->bSupp );
+            pParts[i]->nNodes = Cudd_DagSize( pParts[i]->bFunc );
+            // get rid of the cube
+            // save the last (care set) quantification cube
+            if ( i < nParts - 1 )
+            {
+                Cudd_RecursiveDeref( dd, pNode->bCube );
+                pNode->bCube = NULL;
+            }
+        }
+        // copy the function
+        pNode->bImage = pParts[i]->bFunc;   Cudd_Ref( pNode->bImage );
+    }
+/*
+    for ( i = 0; i < nParts; i++ )
+    {
+        pNode = pNodes[i];
+PRB( dd, pNode->bCube );
+PRB( dd, pNode->pPart->bFunc );
+PRB( dd, pNode->pPart->bSupp );
+printf( "\n" );
+    }
+*/
+    return pNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_DeleteParts_rec( Bbr_ImageNode_t * pNode )
+{
+    Bbr_ImagePart_t * pPart;
+    if ( pNode->pNode1 )
+        Bbr_DeleteParts_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Bbr_DeleteParts_rec( pNode->pNode2 );
+    pPart = pNode->pPart;
+    Cudd_RecursiveDeref( pNode->dd, pPart->bFunc );
+    Cudd_RecursiveDeref( pNode->dd, pPart->bSupp );
+    FREE( pNode->pPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Delete the partitions from the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete_rec( Bbr_ImageNode_t * pNode )
+{
+    if ( pNode->pNode1 )
+        Bbr_bddImageTreeDelete_rec( pNode->pNode1 );
+    if ( pNode->pNode2 )
+        Bbr_bddImageTreeDelete_rec( pNode->pNode2 );
+    if ( pNode->bCube )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bCube );
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( pNode->dd, pNode->bImage );
+    assert( pNode->pPart == NULL );
+    FREE( pNode );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recompute the image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_bddImageCompute_rec( Bbr_ImageTree_t * pTree, Bbr_ImageNode_t * pNode )
+{
+    DdManager * dd = pNode->dd;
+    DdNode * bTemp;
+    int nNodes;
+
+    // trivial case
+    if ( pNode->pNode1 == NULL )
+    {
+        if ( pNode->bCube )
+        {
+            pNode->bImage = Cudd_bddExistAbstract( dd, bTemp = pNode->bImage, pNode->bCube ); 
+            Cudd_Ref( pNode->bImage );
+            Cudd_RecursiveDeref( dd, bTemp );
+        }
+        return 1;
+    }
+
+    // compute the children
+    if ( pNode->pNode1 )
+        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode1 ) )
+            return 0;
+    if ( pNode->pNode2 )
+        if ( !Bbr_bddImageCompute_rec( pTree, pNode->pNode2 ) )
+            return 0;
+
+    // clean the old image
+    if ( pNode->bImage )
+        Cudd_RecursiveDeref( dd, pNode->bImage );
+    pNode->bImage = NULL;
+
+    // compute the new image
+    if ( pNode->bCube )
+        pNode->bImage = Cudd_bddAndAbstract( dd, 
+            pNode->pNode1->bImage, pNode->pNode2->bImage, pNode->bCube );
+    else
+        pNode->bImage = Cudd_bddAnd( dd, pNode->pNode1->bImage, pNode->pNode2->bImage );
+    Cudd_Ref( pNode->bImage );
+
+    if ( pTree->fVerbose )
+    {
+        nNodes = Cudd_DagSize( pNode->bImage );
+        if ( pTree->nNodesMax < nNodes )
+            pTree->nNodesMax = nNodes;
+    }
+    if ( dd->keys > BDD_BLOW_UP )
+        return 0;
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Builds the tree.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_BuildTreeNode( DdManager * dd, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars, int * pfStop )
+{
+    Bbr_ImageNode_t * pNode1, * pNode2;
+    Bbr_ImageVar_t * pVar;
+    Bbr_ImageNode_t * pNode;
+    DdNode * bCube, * bTemp, * bSuppTemp, * bParts;
+    int iNode1, iNode2;
+    int iVarBest, nSupp, v;
+
+    // find the best variable
+    iVarBest = Bbr_FindBestVariable( dd, nNodes, pNodes, nVars, pVars );
+    if ( iVarBest == -1 )
+        return 0;
+
+    pVar = pVars[iVarBest];
+
+    // this var cannot appear in one partition only
+    nSupp = Cudd_SupportSize( dd, pVar->bParts );
+    assert( nSupp == pVar->nParts );
+    assert( nSupp != 1 );
+
+    // if it appears in only two partitions, quantify it
+    if ( pVar->nParts == 2 )
+    {
+        // get the nodes
+        iNode1 = pVar->bParts->index;
+        iNode2 = cuddT(pVar->bParts)->index;
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // get the quantification cube
+        bCube = dd->vars[pVar->iNum];    Cudd_Ref( bCube );
+        // add the variables that appear only in these partitions
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && v != iVarBest && pVars[v]->bParts == pVars[iVarBest]->bParts )
+            {
+                // add this var
+                bCube = Cudd_bddAnd( dd, bTemp = bCube, dd->vars[pVars[v]->iNum] );   Cudd_Ref( bCube );
+                Cudd_RecursiveDeref( dd, bTemp );
+                // clean this var
+                Cudd_RecursiveDeref( dd, pVars[v]->bParts );
+                FREE( pVars[v] );
+            }
+        // clean the best var
+        Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
+        FREE( pVars[iVarBest] );
+
+        // combines two nodes
+        pNode = Bbr_CombineTwoNodes( dd, bCube, pNode1, pNode2 );
+        Cudd_RecursiveDeref( dd, bCube );
+    }
+    else // if ( pVar->nParts > 2 )
+    {
+        // find two smallest BDDs that have this var
+        Bbr_FindBestPartitions( dd, pVar->bParts, nNodes, pNodes, &iNode1, &iNode2 );
+        pNode1 = pNodes[iNode1];
+        pNode2 = pNodes[iNode2];
+
+        // it is not possible that a var appears only in these two
+        // otherwise, it would have a different cost
+        bParts = Cudd_bddAnd( dd, dd->vars[iNode1], dd->vars[iNode2] ); Cudd_Ref( bParts );
+        for ( v = 0; v < nVars; v++ )
+            if ( pVars[v] && pVars[v]->bParts == bParts )
+                assert( 0 );
+        Cudd_RecursiveDeref( dd, bParts );
+
+        // combines two nodes
+        pNode = Bbr_CombineTwoNodes( dd, b1, pNode1, pNode2 );
+    }
+
+    // clean the old nodes
+    pNodes[iNode1] = pNode;
+    pNodes[iNode2] = NULL;
+    
+    // update the variables that appear in pNode[iNode2]
+    for ( bSuppTemp = pNode2->pPart->bSupp; bSuppTemp != b1; bSuppTemp = cuddT(bSuppTemp) )
+    {
+        pVar = pVars[bSuppTemp->index];
+        if ( pVar == NULL ) // this variable is not be quantified
+            continue;
+        // quantify this var
+        assert( Cudd_bddLeq( dd, pVar->bParts, dd->vars[iNode2] ) );
+        pVar->bParts = Cudd_bddExistAbstract( dd, bTemp = pVar->bParts, dd->vars[iNode2] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // add the new var
+        pVar->bParts = Cudd_bddAnd( dd, bTemp = pVar->bParts, dd->vars[iNode1] ); Cudd_Ref( pVar->bParts );
+        Cudd_RecursiveDeref( dd, bTemp );
+        // update the score
+        pVar->nParts = Cudd_SupportSize( dd, pVar->bParts );
+    }
+
+    *pfStop = 0;
+    if ( dd->keys > BDD_BLOW_UP )
+    {
+        *pfStop = 1;
+        return 0;
+    }
+    return 1;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Merges the nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_MergeTopNodes(
+    DdManager * dd, int nNodes, Bbr_ImageNode_t ** pNodes )
+{
+    Bbr_ImageNode_t * pNode;
+    int n1 = -1, n2 = -1, n;
+
+    // find the first and the second non-empty spots
+    for ( n = 0; n < nNodes; n++ )
+        if ( pNodes[n] )
+        {
+            if ( n1 == -1 )
+                n1 = n;
+            else if ( n2 == -1 )
+            {
+                n2 = n;
+                break;
+            }
+        }
+    assert( n1 != -1 );
+    // check the situation when only one such node is detected
+    if ( n2 == -1 )
+    {
+        // save the node
+        pNode = pNodes[n1];
+        // clean the node
+        pNodes[n1] = NULL;
+        return pNode;
+    }
+  
+    // combines two nodes
+    pNode = Bbr_CombineTwoNodes( dd, b1, pNodes[n1], pNodes[n2] );
+
+    // clean the old nodes
+    pNodes[n1] = pNode;
+    pNodes[n2] = NULL;
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Merges two nodes.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageNode_t * Bbr_CombineTwoNodes( DdManager * dd, DdNode * bCube,
+    Bbr_ImageNode_t * pNode1, Bbr_ImageNode_t * pNode2 )
+{
+    Bbr_ImageNode_t * pNode;
+    Bbr_ImagePart_t * pPart;
+
+    // create a new partition
+    pPart = ALLOC( Bbr_ImagePart_t, 1 );
+    memset( pPart, 0, sizeof(Bbr_ImagePart_t) );
+    // create the function
+    pPart->bFunc = Cudd_bddAndAbstract( dd, pNode1->pPart->bFunc, pNode2->pPart->bFunc, bCube );
+    Cudd_Ref( pPart->bFunc );
+    // update the support the partition
+    pPart->bSupp = Cudd_bddAndAbstract( dd, pNode1->pPart->bSupp, pNode2->pPart->bSupp, bCube );
+    Cudd_Ref( pPart->bSupp );
+    // update the numbers
+    pPart->nSupp  = Cudd_SupportSize( dd, pPart->bSupp );
+    pPart->nNodes = Cudd_DagSize( pPart->bFunc );
+    pPart->iPart = -1;
+/*
+PRB( dd, pNode1->pPart->bSupp );
+PRB( dd, pNode2->pPart->bSupp );
+PRB( dd, pPart->bSupp );
+*/
+    // create a new node
+    pNode = ALLOC( Bbr_ImageNode_t, 1 );
+    memset( pNode, 0, sizeof(Bbr_ImageNode_t) );
+    pNode->dd     = dd;
+    pNode->pPart  = pPart;
+    pNode->pNode1 = pNode1;
+    pNode->pNode2 = pNode2;
+    // compute the image
+    pNode->bImage = Cudd_bddAndAbstract( dd, pNode1->bImage, pNode2->bImage, bCube ); 
+    Cudd_Ref( pNode->bImage );
+    // save the cube
+    if ( bCube != b1 )
+    {
+        pNode->bCube = bCube;   Cudd_Ref( bCube );
+    }
+    return pNode;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes the best variable.]
+
+  Description [The variables is the best if the sum of squares of the
+  BDD sizes of the partitions, in which it participates, is the minimum.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Bbr_FindBestVariable( DdManager * dd,
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int nVars,  Bbr_ImageVar_t ** pVars )
+{
+    DdNode * bTemp;
+    int iVarBest, v;
+    double CostBest, CostCur;
+
+    CostBest = 100000000000000;
+    iVarBest = -1;
+    for ( v = 0; v < nVars; v++ )
+        if ( pVars[v] )
+        {
+            CostCur = 0;
+            for ( bTemp = pVars[v]->bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+                CostCur += pNodes[bTemp->index]->pPart->nNodes * 
+                           pNodes[bTemp->index]->pPart->nNodes;
+            if ( CostBest > CostCur )
+            {
+                CostBest = CostCur;
+                iVarBest = v;
+            }
+        }
+    return iVarBest;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes two smallest partions that have this var.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_FindBestPartitions( DdManager * dd, DdNode * bParts, 
+    int nNodes, Bbr_ImageNode_t ** pNodes, 
+    int * piNode1, int * piNode2 )
+{
+    DdNode * bTemp;
+    int iPart1, iPart2;
+    int CostMin1, CostMin2, Cost;
+
+    // go through the partitions
+    iPart1 = iPart2 = -1;
+    CostMin1 = CostMin2 = 1000000;
+    for ( bTemp = bParts; bTemp != b1; bTemp = cuddT(bTemp) )
+    {
+        Cost = pNodes[bTemp->index]->pPart->nNodes;
+        if ( CostMin1 > Cost )
+        {
+            CostMin2 = CostMin1;    iPart2 = iPart1;
+            CostMin1 = Cost;        iPart1 = bTemp->index;
+        }
+        else if ( CostMin2 > Cost )
+        {
+            CostMin2 = Cost;        iPart2 = bTemp->index;
+        }
+    }
+
+    *piNode1 = iPart1;
+    *piNode2 = iPart2;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintLatchDependency( 
+    DdManager * dd, DdNode * bCare, // the care set
+    int nParts, DdNode ** pbParts,  // the partitions for image computation
+    int nVars, DdNode ** pbVars )   // the NS and parameter variables (not quantified!)
+{
+    int i;
+    DdNode * bVarsCs, * bVarsNs;
+
+    bVarsCs = Cudd_Support( dd, bCare );                       Cudd_Ref( bVarsCs );
+    bVarsNs = Cudd_bddComputeCube( dd, pbVars, NULL, nVars );  Cudd_Ref( bVarsNs );
+
+    printf( "The latch dependency matrix:\n" );
+    printf( "Partitions = %d   Variables: total = %d  non-quantifiable = %d\n",
+        nParts, dd->size, nVars );
+    printf( "     : " );
+    for ( i = 0; i < dd->size; i++ )
+        printf( "%d", i % 10 );
+    printf( "\n" );
+
+    for ( i = 0; i < nParts; i++ )
+        Bbr_bddImagePrintLatchDependencyOne( dd, pbParts[i], bVarsCs, bVarsNs, i );
+    Bbr_bddImagePrintLatchDependencyOne( dd, bCare, bVarsCs, bVarsNs, nParts );
+
+    Cudd_RecursiveDeref( dd, bVarsCs );
+    Cudd_RecursiveDeref( dd, bVarsNs );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints one row of the latch dependency matrix.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintLatchDependencyOne(
+    DdManager * dd, DdNode * bFunc,      // the function
+    DdNode * bVarsCs, DdNode * bVarsNs,  // the current/next state vars
+    int iPart )
+{
+    DdNode * bSupport;
+    int v;
+    bSupport = Cudd_Support( dd, bFunc );  Cudd_Ref( bSupport );
+    printf( " %3d : ", iPart );
+    for ( v = 0; v < dd->size; v++ )
+    {
+        if ( Cudd_bddLeq( dd, bSupport, dd->vars[v] ) )
+        {
+            if ( Cudd_bddLeq( dd, bVarsCs, dd->vars[v] ) )
+                printf( "c" );
+            else if ( Cudd_bddLeq( dd, bVarsNs, dd->vars[v] ) ) 
+                printf( "n" );
+            else
+                printf( "i" );
+        }
+        else
+            printf( "." );
+    }
+    printf( "\n" );
+    Cudd_RecursiveDeref( dd, bSupport );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintTree( Bbr_ImageTree_t * pTree )
+{
+    printf( "The quantification scheduling tree:\n" );
+    Bbr_bddImagePrintTree_rec( pTree->pRoot, 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Prints the tree for quenstification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImagePrintTree_rec( Bbr_ImageNode_t * pNode, int Offset )
+{
+    DdNode * Cube;
+    int i;
+
+    Cube = pNode->bCube;
+
+    if ( pNode->pNode1 == NULL )
+    {
+        printf( "<%d> ", pNode->pPart->iPart );
+        if ( Cube != NULL )
+        {
+            PRB( pNode->dd, Cube );
+        }
+        else
+            printf( "\n" );
+        return;
+    }
+
+    printf( "<*> " );
+    if ( Cube != NULL )
+    {
+        PRB( pNode->dd, Cube );
+    }
+    else
+        printf( "\n" );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Bbr_bddImagePrintTree_rec( pNode->pNode1, Offset + 1 );
+
+    for ( i = 0; i < Offset; i++ )
+        printf( "    " );
+    Bbr_bddImagePrintTree_rec( pNode->pNode2, Offset + 1 );
+}
+
+/**Function********************************************************************
+
+  Synopsis    [Computes the positive polarty cube composed of the first vars in the array.]
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+******************************************************************************/
+DdNode * Bbr_bddComputeCube( DdManager * dd, DdNode ** bXVars, int nVars )
+{
+    DdNode * bRes;
+    DdNode * bTemp;
+    int i;
+
+    bRes = b1; Cudd_Ref( bRes );
+    for ( i = 0; i < nVars; i++ )
+    {
+        bRes = Cudd_bddAnd( dd, bTemp = bRes, bXVars[i] );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+
+    Cudd_Deref( bRes );
+    return bRes;
+}
+
+
+
+
+
+struct Bbr_ImageTree2_t_
+{
+    DdManager * dd;
+    DdNode *    bRel;
+    DdNode *    bCube;
+    DdNode *    bImage;
+};
+
+/**Function*************************************************************
+
+  Synopsis    [Starts the monolithic image computation.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Bbr_ImageTree2_t * Bbr_bddImageStart2( 
+    DdManager * dd, DdNode * bCare,
+    int nParts, DdNode ** pbParts,
+    int nVars, DdNode ** pbVars, int fVerbose )
+{
+    Bbr_ImageTree2_t * pTree;
+    DdNode * bCubeAll, * bCubeNot, * bTemp;
+    int i;
+
+    pTree = ALLOC( Bbr_ImageTree2_t, 1 );
+    pTree->dd = dd;
+    pTree->bImage = NULL;
+
+    bCubeAll = Bbr_bddComputeCube( dd, dd->vars, dd->size );      Cudd_Ref( bCubeAll );
+    bCubeNot = Bbr_bddComputeCube( dd, pbVars,   nVars );         Cudd_Ref( bCubeNot );
+    pTree->bCube = Cudd_bddExistAbstract( dd, bCubeAll, bCubeNot ); Cudd_Ref( pTree->bCube );
+    Cudd_RecursiveDeref( dd, bCubeAll );
+    Cudd_RecursiveDeref( dd, bCubeNot );
+
+    // derive the monolithic relation
+    pTree->bRel = b1;   Cudd_Ref( pTree->bRel );
+    for ( i = 0; i < nParts; i++ )
+    {
+        pTree->bRel = Cudd_bddAnd( dd, bTemp = pTree->bRel, pbParts[i] ); Cudd_Ref( pTree->bRel );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Bbr_bddImageCompute2( pTree, bCare );
+    return pTree;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare )
+{
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    pTree->bImage = Cudd_bddAndAbstract( pTree->dd, pTree->bRel, bCare, pTree->bCube ); 
+    Cudd_Ref( pTree->bImage );
+    return pTree->bImage;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree )
+{
+    if ( pTree->bRel )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bRel );
+    if ( pTree->bCube )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bCube );
+    if ( pTree->bImage )
+        Cudd_RecursiveDeref( pTree->dd, pTree->bImage );
+    FREE( pTree );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns the previously computed image.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree )
+{
+    return pTree->bImage;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+