Major restructuring of the code.

7 files changed, 0 insertions, 2472 deletions

diff --git a/src/aig/bbr/bbr.h b/src/aig/bbr/bbr.h
deleted file mode 100644
index bb83ac95..00000000
--- a/src/aig/bbr/bbr.h
+++ /dev/null
@@ -1,93 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [bbr.h]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD-based reachability analysis.]
-
-  Synopsis    [External declarations.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: bbr.h,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
- 
-#ifndef __BBR_H__
-#define __BBR_H__
-
-
-////////////////////////////////////////////////////////////////////////
-///                          INCLUDES                                ///
-////////////////////////////////////////////////////////////////////////
-
-#include <stdio.h>
-#include "aig.h"
-#include "saig.h"
-#include "cuddInt.h"
-
-////////////////////////////////////////////////////////////////////////
-///                         PARAMETERS                               ///
-////////////////////////////////////////////////////////////////////////
-
-
-
-ABC_NAMESPACE_HEADER_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                         BASIC TYPES                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                      MACRO DEFINITIONS                           ///
-////////////////////////////////////////////////////////////////////////
-
-static inline DdNode * Aig_ObjGlobalBdd( Aig_Obj_t * pObj )  { return (DdNode *)pObj->pData; }
-
-////////////////////////////////////////////////////////////////////////
-///                    FUNCTION DECLARATIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/*=== bbrImage.c ==========================================================*/
-typedef struct Bbr_ImageTree_t_  Bbr_ImageTree_t;
-extern Bbr_ImageTree_t * Bbr_bddImageStart( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int nBddMax, int fVerbose );
-extern DdNode *    Bbr_bddImageCompute( Bbr_ImageTree_t * pTree, DdNode * bCare );
-extern void        Bbr_bddImageTreeDelete( Bbr_ImageTree_t * pTree );
-extern DdNode *    Bbr_bddImageRead( Bbr_ImageTree_t * pTree );
-typedef struct Bbr_ImageTree2_t_  Bbr_ImageTree2_t;
-extern Bbr_ImageTree2_t * Bbr_bddImageStart2( 
-    DdManager * dd, DdNode * bCare,
-    int nParts, DdNode ** pbParts,
-    int nVars, DdNode ** pbVars, int fVerbose );
-extern DdNode *    Bbr_bddImageCompute2( Bbr_ImageTree2_t * pTree, DdNode * bCare );
-extern void        Bbr_bddImageTreeDelete2( Bbr_ImageTree2_t * pTree );
-extern DdNode *    Bbr_bddImageRead2( Bbr_ImageTree2_t * pTree );
-/*=== bbrNtbdd.c ==========================================================*/
-extern void        Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd );
-extern int         Aig_ManSizeOfGlobalBdds( Aig_Man_t * p );
-extern DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose );
-/*=== bbrReach.c ==========================================================*/
-extern int         Aig_ManVerifyUsingBdds( Aig_Man_t * p, Saig_ParBbr_t * pPars );
-extern void        Bbr_ManSetDefaultParams( Saig_ParBbr_t * p );
-
-
-
-ABC_NAMESPACE_HEADER_END
-
-
-
-#endif
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
diff --git a/src/aig/bbr/bbrCex.c b/src/aig/bbr/bbrCex.c
deleted file mode 100644
index 4a1a1d67..00000000
--- a/src/aig/bbr/bbrCex.c
+++ /dev/null
@@ -1,172 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [bbrCex.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD-based reachability analysis.]
-
-  Synopsis    [Procedures to derive a satisfiable counter-example.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: bbrCex.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "bbr.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the counter-example using the set of reached states.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
-    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst,
-    int iOutput, int fVerbose, int fSilent )
-{
-    Abc_Cex_t * pCex;
-    Aig_Obj_t * pObj;
-    Bbr_ImageTree_t * pTree;
-    DdNode * bCubeNs, * bState, * bImage;
-    DdNode * bTemp, * bVar, * bRing;
-    int i, v, RetValue, nPiOffset;
-    char * pValues;
-    int clk = clock();
-//printf( "\nDeriving counter-example.\n" );
-
-    // allocate room for the counter-example
-    pCex = Abc_CexAlloc( Saig_ManRegNum(p), Saig_ManPiNum(p), Vec_PtrSize(vOnionRings)+1 );
-    pCex->iFrame = Vec_PtrSize(vOnionRings);
-    pCex->iPo = iOutput;
-    nPiOffset = Saig_ManRegNum(p) + Saig_ManPiNum(p) * Vec_PtrSize(vOnionRings);
-
-    // create the cube of NS variables
-    bCubeNs  = Bbr_bddComputeRangeCube( dd, Saig_ManCiNum(p), Saig_ManCiNum(p)+Saig_ManRegNum(p) );    Cudd_Ref( bCubeNs );
-    pTree = Bbr_bddImageStart( dd, bCubeNs, Saig_ManRegNum(p), pbParts, Saig_ManCiNum(p), dd->vars, 100000000, fVerbose );
-    Cudd_RecursiveDeref( dd, bCubeNs );
-    if ( pTree == NULL )
-    {
-        if ( !fSilent )
-            printf( "BDDs blew up during qualitification scheduling.  " );
-        return NULL;
-    }
-
-    // allocate room for the cube
-    pValues = ABC_ALLOC( char, dd->size );
-
-    // get the last cube
-    RetValue = Cudd_bddPickOneCube( dd, bCubeFirst, pValues );
-    assert( RetValue );
-
-    // write PIs of counter-example
-    Saig_ManForEachPi( p, pObj, i )
-        if ( pValues[i] == 1 )
-            Aig_InfoSetBit( pCex->pData, nPiOffset + i );
-    nPiOffset -= Saig_ManPiNum(p);
-
-    // write state in terms of NS variables
-    bState = (dd)->one; Cudd_Ref( bState );
-    Saig_ManForEachLo( p, pObj, i )
-    {
-        bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
-        bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
-        Cudd_RecursiveDeref( dd, bTemp ); 
-    }
-
-    // perform backward analysis
-    Vec_PtrForEachEntryReverse( DdNode *, vOnionRings, bRing, v )
-    { 
-        // compute the next states
-        bImage = Bbr_bddImageCompute( pTree, bState );           
-        if ( bImage == NULL )
-        {
-            Cudd_RecursiveDeref( dd, bState );
-            if ( !fSilent )
-                printf( "BDDs blew up during image computation.  " );
-            Bbr_bddImageTreeDelete( pTree );
-            ABC_FREE( pValues );
-            return NULL;
-        }
-        Cudd_Ref( bImage );
-        Cudd_RecursiveDeref( dd, bState );
-
-        // intersect with the previous set
-        bImage = Cudd_bddAnd( dd, bTemp = bImage, bRing );  Cudd_Ref( bImage );
-        Cudd_RecursiveDeref( dd, bTemp );
-
-        // find any assignment of the BDD
-        RetValue = Cudd_bddPickOneCube( dd, bImage, pValues );
-        assert( RetValue );
-        Cudd_RecursiveDeref( dd, bImage );
-
-        // write PIs of counter-example
-        Saig_ManForEachPi( p, pObj, i )
-            if ( pValues[i] == 1 )
-                Aig_InfoSetBit( pCex->pData, nPiOffset + i );
-        nPiOffset -= Saig_ManPiNum(p);
-
-        // check that we get the init state
-        if ( v == 0 )
-        {
-            Saig_ManForEachLo( p, pObj, i )
-                assert( pValues[Saig_ManPiNum(p)+i] == 0 );
-            break;
-        }
-
-        // write state in terms of NS variables
-        bState = (dd)->one; Cudd_Ref( bState );
-        Saig_ManForEachLo( p, pObj, i )
-        {
-            bVar = Cudd_NotCond( dd->vars[Saig_ManCiNum(p)+i], pValues[Saig_ManPiNum(p)+i] != 1 );
-            bState = Cudd_bddAnd( dd, bTemp = bState, bVar );  Cudd_Ref( bState );
-            Cudd_RecursiveDeref( dd, bTemp ); 
-        }
-    }
-    // cleanup
-    Bbr_bddImageTreeDelete( pTree );
-    ABC_FREE( pValues );
-    // verify the counter example
-    if ( Vec_PtrSize(vOnionRings) < 1000 )
-    {
-    RetValue = Saig_ManVerifyCex( p, pCex );
-    if ( RetValue == 0 && !fSilent )
-        printf( "Aig_ManVerifyUsingBdds(): Counter-example verification has FAILED.\n" );
-    }
-    if ( fVerbose && !fSilent )
-    {
-    ABC_PRT( "Counter-example generation time", clock() - clk );
-    }
-    return pCex;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/bbr/bbrImage.c b/src/aig/bbr/bbrImage.c
deleted file mode 100644
index 8b18d84d..00000000
--- a/src/aig/bbr/bbrImage.c
+++ /dev/null
@@ -1,1327 +0,0 @@
-/**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"
-
-ABC_NAMESPACE_IMPL_START
- 
-
-/* 
-    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
-    int                 nBddMax;    // the number of node to stop
-};
-
-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     b0     Cudd_Not((dd)->one)
-#define     b1              (dd)->one
-
-#ifndef ABC_PRB
-#define ABC_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, int nBddMax );
-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 nBddMax, 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, nBddMax ) );
-
-    // consider the case of BDD node blowup
-    if ( fStop )
-    {
-        for ( v = 0; v < dd->size; v++ )
-            if ( pVars[v] )
-                ABC_FREE( pVars[v] );
-        ABC_FREE( pVars );
-        for ( v = 0; v <= nParts; v++ )
-            if ( pNodes[v] )
-            {
-                Bbr_DeleteParts_rec( pNodes[v] );
-                Bbr_bddImageTreeDelete_rec( pNodes[v] );
-            }
-        ABC_FREE( pNodes );
-        ABC_FREE( pParts );
-        return NULL;
-    }
-
-    // make sure the variables are gone
-    for ( v = 0; v < dd->size; v++ )
-        assert( pVars[v] == NULL );
-    ABC_FREE( pVars );
-    
-    // create the tree
-    pTree = ABC_ALLOC( Bbr_ImageTree_t, 1 );
-    memset( pTree, 0, sizeof(Bbr_ImageTree_t) );
-    pTree->pCare = pCare;
-    pTree->nBddMax = nBddMax;
-    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 );
-    ABC_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 );
-    ABC_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: " );
-ABC_PRB( dd, pTree->bCareSupp );
-printf( "Current care set support: " );
-ABC_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 );
-    ABC_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 = ABC_ALLOC( Bbr_ImagePart_t *, nParts + 1 );
-    // create structures for each variable
-    for ( i = 0; i < nParts; i++ )
-    {
-        pParts[i] = ABC_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] = ABC_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 = ABC_ALLOC( DdNode *, nParts );
-    for ( p = 0; p < nParts; p++ )
-        pbFuncs[p] = pParts[p]->bSupp;
-    bSupp = Cudd_VectorSupport( dd, pbFuncs, nParts );  Cudd_Ref( bSupp );
-    ABC_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 = ABC_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] = ABC_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 = ABC_ALLOC( Bbr_ImageNode_t *, nParts );
-    // create structures for each leaf nodes
-    for ( i = 0; i < nParts; i++ )
-    {
-        pNodes[i] = ABC_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 );
-        ABC_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];
-ABC_PRB( dd, pNode->bCube );
-ABC_PRB( dd, pNode->pPart->bFunc );
-ABC_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 );
-    ABC_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 );
-    ABC_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-dd->dead > (unsigned)pTree->nBddMax )
-        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, int nBddMax )
-{
-    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;
-/*
-for ( v = 0; v < nVars; v++ )
-{
-    DdNode * bSupp;
-    if ( pVars[v] == NULL )
-        continue;
-    printf( "%3d :", v );
-    printf( "%3d ", pVars[v]->nParts );
-    bSupp = Cudd_Support( dd, pVars[v]->bParts );  Cudd_Ref( bSupp );
-    Bbr_bddPrint( dd, bSupp ); printf( "\n" );
-    Cudd_RecursiveDeref( dd, bSupp );
-}
-*/
-    pVar = pVars[iVarBest];
-
-    // this var cannot appear in one partition only
-    nSupp = Cudd_SupportSize( dd, pVar->bParts );
-    assert( nSupp == pVar->nParts );
-    assert( nSupp != 1 );
-//printf( "var = %d  supp = %d\n\n", iVarBest, nSupp );
-
-    // 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 );
-                ABC_FREE( pVars[v] );
-            }
-        // clean the best var
-        Cudd_RecursiveDeref( dd, pVars[iVarBest]->bParts );
-        ABC_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];
-//printf( "smallest bdds with this var: %d %d\n", iNode1, 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;
-//printf( "Removing node %d (leaving node %d)\n", iNode2, iNode1 );
-    
-    // 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-dd->dead > (unsigned)nBddMax )
-    {
-        *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 = ABC_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;
-/*
-ABC_PRB( dd, pNode1->pPart->bSupp );
-ABC_PRB( dd, pNode2->pPart->bSupp );
-ABC_PRB( dd, pPart->bSupp );
-*/
-    // create a new node
-    pNode = ABC_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.0;
-    iVarBest = -1;
-
-    // check if there are two-variable partitions
-    for ( v = 0; v < nVars; v++ )
-        if ( pVars[v] && pVars[v]->nParts == 2 )
-        {
-            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;
-            }
-        }
-    if ( iVarBest >= 0 )
-        return iVarBest;
-
-    // find other partition
-    for ( v = 0; v < nVars; v++ )
-        if ( pVars[v] )
-        {
-            assert( pVars[v]->nParts > 1 );
-            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 )
-        {
-            ABC_PRB( pNode->dd, Cube );
-        }
-        else
-            printf( "\n" );
-        return;
-    }
-
-    printf( "<*> " );
-    if ( Cube != NULL )
-    {
-        ABC_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 = ABC_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 );
-    ABC_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                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/bbr/bbrNtbdd.c b/src/aig/bbr/bbrNtbdd.c
deleted file mode 100644
index 09456df0..00000000
--- a/src/aig/bbr/bbrNtbdd.c
+++ /dev/null
@@ -1,218 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [bbrNtbdd.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD-based reachability analysis.]
-
-  Synopsis    [Procedures to construct global BDDs for the network.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: bbrNtbdd.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "bbr.h"
-//#include "bar.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-typedef char ProgressBar;
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-static inline void     Aig_ObjSetGlobalBdd( Aig_Obj_t * pObj, DdNode * bFunc )   { pObj->pData = bFunc; }
-static inline void     Aig_ObjCleanGlobalBdd( DdManager * dd, Aig_Obj_t * pObj ) { Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData ); pObj->pData = NULL; }
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [Derives the global BDD for one AIG node.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Bbr_NodeGlobalBdds_rec( DdManager * dd, Aig_Obj_t * pNode, int nBddSizeMax, int fDropInternal, ProgressBar * pProgress, int * pCounter, int fVerbose )
-{
-    DdNode * bFunc, * bFunc0, * bFunc1;
-    assert( !Aig_IsComplement(pNode) );
-    if ( Cudd_ReadKeys(dd)-Cudd_ReadDead(dd) > (unsigned)nBddSizeMax )
-    {
-//        Extra_ProgressBarStop( pProgress );
-        if ( fVerbose )
-        printf( "The number of live nodes reached %d.\n", nBddSizeMax );
-        fflush( stdout );
-        return NULL;
-    }
-    // if the result is available return
-    if ( Aig_ObjGlobalBdd(pNode) == NULL )
-    {
-        // compute the result for both branches
-        bFunc0 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
-        if ( bFunc0 == NULL )
-            return NULL;
-        Cudd_Ref( bFunc0 );
-        bFunc1 = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin1(pNode), nBddSizeMax, fDropInternal, pProgress, pCounter, fVerbose ); 
-        if ( bFunc1 == NULL )
-            return NULL;
-        Cudd_Ref( bFunc1 );
-        bFunc0 = Cudd_NotCond( bFunc0, Aig_ObjFaninC0(pNode) );
-        bFunc1 = Cudd_NotCond( bFunc1, Aig_ObjFaninC1(pNode) );
-        // get the final result
-        bFunc = Cudd_bddAnd( dd, bFunc0, bFunc1 );   Cudd_Ref( bFunc );
-        Cudd_RecursiveDeref( dd, bFunc0 );
-        Cudd_RecursiveDeref( dd, bFunc1 );
-        // add the number of used nodes
-        (*pCounter)++;
-        // set the result
-        assert( Aig_ObjGlobalBdd(pNode) == NULL );
-        Aig_ObjSetGlobalBdd( pNode, bFunc );
-        // increment the progress bar
-//        if ( pProgress )
-//            Extra_ProgressBarUpdate( pProgress, *pCounter, NULL );
-    }
-    // prepare the return value
-    bFunc = Aig_ObjGlobalBdd(pNode);
-    // dereference BDD at the node
-    if ( --pNode->nRefs == 0 && fDropInternal )
-    {
-        Cudd_Deref( bFunc );
-        Aig_ObjSetGlobalBdd( pNode, NULL );
-    }
-    return bFunc;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Frees the global BDDs of the network.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_ManFreeGlobalBdds( Aig_Man_t * p, DdManager * dd ) 
-{ 
-    Aig_Obj_t * pObj;
-    int i;
-    Aig_ManForEachObj( p, pObj, i )
-        if ( Aig_ObjGlobalBdd(pObj) )
-            Aig_ObjCleanGlobalBdd( dd, pObj );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Returns the shared size of global BDDs of the COs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManSizeOfGlobalBdds( Aig_Man_t * p ) 
-{
-    Vec_Ptr_t * vFuncsGlob;
-    Aig_Obj_t * pObj;
-    int RetValue, i;
-    // complement the global functions
-    vFuncsGlob = Vec_PtrAlloc( Aig_ManPoNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-        Vec_PtrPush( vFuncsGlob, Aig_ObjGlobalBdd(pObj) );
-    RetValue = Cudd_SharingSize( (DdNode **)Vec_PtrArray(vFuncsGlob), Vec_PtrSize(vFuncsGlob) );
-    Vec_PtrFree( vFuncsGlob );
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Recursively computes global BDDs for the AIG in the manager.]
-
-  Description [On exit, BDDs are stored in the pNode->pData fields.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdManager * Aig_ManComputeGlobalBdds( Aig_Man_t * p, int nBddSizeMax, int fDropInternal, int fReorder, int fVerbose )
-{
-    ProgressBar * pProgress = NULL;
-    Aig_Obj_t * pObj;
-    DdManager * dd;
-    DdNode * bFunc;
-    int i, Counter;
-    // start the manager
-    dd = Cudd_Init( Aig_ManPiNum(p), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
-    // set reordering
-    if ( fReorder )
-        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
-    // prepare to construct global BDDs
-    Aig_ManCleanData( p );
-    // assign the constant node BDD
-    Aig_ObjSetGlobalBdd( Aig_ManConst1(p), dd->one );   Cudd_Ref( dd->one );
-    // set the elementary variables
-    Aig_ManForEachPi( p, pObj, i )
-    {
-        Aig_ObjSetGlobalBdd( pObj, dd->vars[i] );  Cudd_Ref( dd->vars[i] );
-    }
-
-    // collect the global functions of the COs
-    Counter = 0;
-    // construct the BDDs
-//    pProgress = Extra_ProgressBarStart( stdout, Aig_ManNodeNum(p) );
-    Aig_ManForEachPo( p, pObj, i )
-    {
-        bFunc = Bbr_NodeGlobalBdds_rec( dd, Aig_ObjFanin0(pObj), nBddSizeMax, fDropInternal, pProgress, &Counter, fVerbose );
-        if ( bFunc == NULL )
-        {
-            if ( fVerbose )
-            printf( "Constructing global BDDs is aborted.\n" );
-            Aig_ManFreeGlobalBdds( p, dd );
-            Cudd_Quit( dd ); 
-            // reset references
-            Aig_ManResetRefs( p );
-            return NULL;
-        }
-        bFunc = Cudd_NotCond( bFunc, Aig_ObjFaninC0(pObj) );  Cudd_Ref( bFunc ); 
-        Aig_ObjSetGlobalBdd( pObj, bFunc );
-    }
-//    Extra_ProgressBarStop( pProgress );
-    // reset references
-    Aig_ManResetRefs( p );
-    // reorder one more time
-    if ( fReorder )
-    {
-        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 1 );
-        Cudd_AutodynDisable( dd );
-    }
-//    Cudd_PrintInfo( dd, stdout );
-    return dd;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/bbr/bbrReach.c b/src/aig/bbr/bbrReach.c
deleted file mode 100644
index 9c6dced3..00000000
--- a/src/aig/bbr/bbrReach.c
+++ /dev/null
@@ -1,606 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [bbrReach.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName [BDD-based reachability analysis.]
-
-  Synopsis    [Procedures to perform reachability analysis.]
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: bbrReach.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "bbr.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-extern Abc_Cex_t * Aig_ManVerifyUsingBddsCountExample( Aig_Man_t * p, DdManager * dd, 
-    DdNode ** pbParts, Vec_Ptr_t * vOnionRings, DdNode * bCubeFirst, 
-    int iOutput, int fVerbose, int fSilent );
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    [This procedure sets default resynthesis parameters.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Bbr_ManSetDefaultParams( Saig_ParBbr_t * p )
-{
-    memset( p, 0, sizeof(Saig_ParBbr_t) );
-    p->TimeLimit     =     0;
-    p->nBddMax       = 50000;
-    p->nIterMax      =  1000;
-    p->fPartition    =     1;
-    p->fReorder      =     1;
-    p->fReorderImage =     1;
-    p->fVerbose      =     0;
-    p->fSilent       =     0;
-    p->iFrame        =    -1;
-}
-
-/**Function********************************************************************
-
-  Synopsis    [Performs the reordering-sensitive step of Extra_bddMove().]
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-******************************************************************************/
-DdNode * Bbr_bddComputeRangeCube( DdManager * dd, int iStart, int iStop )
-{
-    DdNode * bTemp, * bProd;
-    int i;
-    assert( iStart <= iStop );
-    assert( iStart >= 0 && iStart <= dd->size );
-    assert( iStop >= 0  && iStop  <= dd->size );
-    bProd = (dd)->one;         Cudd_Ref( bProd );
-    for ( i = iStart; i < iStop; i++ )
-    {
-        bProd = Cudd_bddAnd( dd, bTemp = bProd, dd->vars[i] );      Cudd_Ref( bProd );
-        Cudd_RecursiveDeref( dd, bTemp ); 
-    }
-    Cudd_Deref( bProd );
-    return bProd;
-}
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Bbr_StopManager( DdManager * dd )
-{
-    int RetValue;
-    // check for remaining references in the package
-    RetValue = Cudd_CheckZeroRef( dd );
-    if ( RetValue > 0 )
-        printf( "\nThe number of referenced nodes = %d\n\n", RetValue );
-//  Cudd_PrintInfo( dd, stdout );
-    Cudd_Quit( dd );
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the initial state and sets up the variable map.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode * Aig_ManInitStateVarMap( DdManager * dd, Aig_Man_t * p, int fVerbose )
-{
-    DdNode ** pbVarsX, ** pbVarsY;
-    DdNode * bTemp, * bProd;
-    Aig_Obj_t * pLatch;
-    int i;
-
-    // set the variable mapping for Cudd_bddVarMap()
-    pbVarsX = ABC_ALLOC( DdNode *, dd->size );
-    pbVarsY = ABC_ALLOC( DdNode *, dd->size );
-    bProd = (dd)->one;         Cudd_Ref( bProd );
-    Saig_ManForEachLo( p, pLatch, i )
-    {
-        pbVarsX[i] = dd->vars[ Saig_ManPiNum(p) + i ];
-        pbVarsY[i] = dd->vars[ Saig_ManCiNum(p) + i ];
-        // get the initial value of the latch
-        bProd = Cudd_bddAnd( dd, bTemp = bProd, Cudd_Not(pbVarsX[i]) );      Cudd_Ref( bProd );
-        Cudd_RecursiveDeref( dd, bTemp ); 
-    }
-    Cudd_SetVarMap( dd, pbVarsX, pbVarsY, Saig_ManRegNum(p) );
-    ABC_FREE( pbVarsX );
-    ABC_FREE( pbVarsY );
-
-    Cudd_Deref( bProd );
-    return bProd;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the array of output BDDs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode ** Aig_ManCreateOutputs( DdManager * dd, Aig_Man_t * p )
-{
-    DdNode ** pbOutputs;
-    Aig_Obj_t * pNode;
-    int i;
-    // compute the transition relation
-    pbOutputs = ABC_ALLOC( DdNode *, Saig_ManPoNum(p) );
-    Saig_ManForEachPo( p, pNode, i )
-    {
-        pbOutputs[i] = Aig_ObjGlobalBdd(pNode);  Cudd_Ref( pbOutputs[i] );
-    }
-    return pbOutputs;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Collects the array of partition BDDs.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-DdNode ** Aig_ManCreatePartitions( DdManager * dd, Aig_Man_t * p, int fReorder, int fVerbose )
-{
-    DdNode ** pbParts;
-    DdNode * bVar;
-    Aig_Obj_t * pNode;
-    int i;
-
-    // extand the BDD manager to represent NS variables
-    assert( dd->size == Saig_ManCiNum(p) );
-    Cudd_bddIthVar( dd, Saig_ManCiNum(p) + Saig_ManRegNum(p) - 1 );
-
-    // enable reordering
-    if ( fReorder )
-        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
-    else
-        Cudd_AutodynDisable( dd );
-
-    // compute the transition relation
-    pbParts = ABC_ALLOC( DdNode *, Saig_ManRegNum(p) );
-    Saig_ManForEachLi( p, pNode, i )
-    {
-        bVar  = Cudd_bddIthVar( dd, Saig_ManCiNum(p) + i );
-        pbParts[i] = Cudd_bddXnor( dd, bVar, Aig_ObjGlobalBdd(pNode) );  Cudd_Ref( pbParts[i] );
-    }
-    // free global BDDs
-    Aig_ManFreeGlobalBdds( p, dd );
-
-    // reorder and disable reordering
-    if ( fReorder )
-    {
-        if ( fVerbose )
-            fprintf( stdout, "BDD nodes in the partitions before reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
-        Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
-        Cudd_AutodynDisable( dd );
-        if ( fVerbose )
-            fprintf( stdout, "BDD nodes in the partitions after reordering %d.\n", Cudd_SharingSize(pbParts,Saig_ManRegNum(p)) );
-    }
-    return pbParts;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Computes the set of unreachable states.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManComputeReachable( DdManager * dd, Aig_Man_t * p, DdNode ** pbParts, DdNode * bInitial, DdNode ** pbOutputs, Saig_ParBbr_t * pPars, int fCheckOutputs )
-{
-    int fInternalReorder = 0;
-    Bbr_ImageTree_t * pTree = NULL; // Suppress "might be used uninitialized"
-    Bbr_ImageTree2_t * pTree2 = NULL; // Supprses "might be used uninitialized"
-    DdNode * bReached, * bCubeCs;
-    DdNode * bCurrent;
-    DdNode * bNext = NULL; // Suppress "might be used uninitialized"
-    DdNode * bTemp;
-    Cudd_ReorderingType method;
-    int i, nIters, nBddSize = 0, status;
-    int nThreshold = 10000, clk = clock();
-    Vec_Ptr_t * vOnionRings;
-
-    status = Cudd_ReorderingStatus( dd, &method );
-    if ( status )
-        Cudd_AutodynDisable( dd );
-
-    // start the image computation
-    bCubeCs  = Bbr_bddComputeRangeCube( dd, Saig_ManPiNum(p), Saig_ManCiNum(p) );    Cudd_Ref( bCubeCs );
-    if ( pPars->fPartition )
-        pTree = Bbr_bddImageStart( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->nBddMax, pPars->fVerbose );
-    else
-        pTree2 = Bbr_bddImageStart2( dd, bCubeCs, Saig_ManRegNum(p), pbParts, Saig_ManRegNum(p), dd->vars+Saig_ManCiNum(p), pPars->fVerbose );
-    Cudd_RecursiveDeref( dd, bCubeCs );
-    if ( pTree == NULL )
-    {
-        if ( !pPars->fSilent )
-            printf( "BDDs blew up during qualitification scheduling.  " );
-        return -1;
-    }
-
-    if ( status )
-        Cudd_AutodynEnable( dd, method );
-
-    // start the onion rings
-    vOnionRings = Vec_PtrAlloc( 1000 );
-
-    // perform reachability analysis
-    bCurrent = bInitial;   Cudd_Ref( bCurrent );
-    bReached = bInitial;   Cudd_Ref( bReached );
-    Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
-    for ( nIters = 0; nIters < pPars->nIterMax; nIters++ )
-    { 
-        // check the runtime limit
-        if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
-        {
-            printf( "Reached timeout after image computation (%d seconds).\n",  pPars->TimeLimit );
-            Vec_PtrFree( vOnionRings );
-            // undo the image tree
-            if ( pPars->fPartition )
-                Bbr_bddImageTreeDelete( pTree );
-            else
-                Bbr_bddImageTreeDelete2( pTree2 );
-            pPars->iFrame = nIters - 1;
-            return -1;
-        }
-
-        // compute the next states
-        if ( pPars->fPartition )
-            bNext = Bbr_bddImageCompute( pTree, bCurrent );           
-        else
-            bNext = Bbr_bddImageCompute2( pTree2, bCurrent );  
-        if ( bNext == NULL )
-        {
-            if ( !pPars->fSilent )
-                printf( "BDDs blew up during image computation.  " );
-            if ( pPars->fPartition )
-                Bbr_bddImageTreeDelete( pTree );
-            else
-                Bbr_bddImageTreeDelete2( pTree2 );
-            Vec_PtrFree( vOnionRings );
-            pPars->iFrame = nIters - 1;
-            return -1;
-        }
-        Cudd_Ref( bNext );
-        Cudd_RecursiveDeref( dd, bCurrent );
-
-        // remap these states into the current state vars
-        bNext = Cudd_bddVarMap( dd, bTemp = bNext );                    Cudd_Ref( bNext );
-        Cudd_RecursiveDeref( dd, bTemp );
-        // check if there are any new states
-        if ( Cudd_bddLeq( dd, bNext, bReached ) )
-            break;
-        // check the BDD size
-        nBddSize = Cudd_DagSize(bNext);
-        if ( nBddSize > pPars->nBddMax )
-            break;
-        // check the result
-        for ( i = 0; i < Saig_ManPoNum(p); i++ )
-        {
-            if ( fCheckOutputs && !Cudd_bddLeq( dd, bNext, Cudd_Not(pbOutputs[i]) ) )
-            {
-                DdNode * bIntersect;
-                bIntersect = Cudd_bddIntersect( dd, bNext, pbOutputs[i] );  Cudd_Ref( bIntersect );
-                assert( p->pSeqModel == NULL );
-                p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
-                    vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
-                Cudd_RecursiveDeref( dd, bIntersect );
-                if ( !pPars->fSilent )
-                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness). ", i, Vec_PtrSize(vOnionRings) );
-                Cudd_RecursiveDeref( dd, bReached );
-                bReached = NULL;
-                pPars->iFrame = nIters;
-                break;
-            }
-        }
-        if ( i < Saig_ManPoNum(p) )
-            break;
-        // get the new states
-        bCurrent = Cudd_bddAnd( dd, bNext, Cudd_Not(bReached) );        Cudd_Ref( bCurrent );
-        Vec_PtrPush( vOnionRings, bCurrent );  Cudd_Ref( bCurrent );
-        // minimize the new states with the reached states
-//        bCurrent = Cudd_bddConstrain( dd, bTemp = bCurrent, Cudd_Not(bReached) ); Cudd_Ref( bCurrent );
-//        Cudd_RecursiveDeref( dd, bTemp );
-        // add to the reached states
-        bReached = Cudd_bddOr( dd, bTemp = bReached, bNext );           Cudd_Ref( bReached );
-        Cudd_RecursiveDeref( dd, bTemp );
-        Cudd_RecursiveDeref( dd, bNext );
-        if ( pPars->fVerbose )
-            fprintf( stdout, "Frame = %3d. BDD = %5d. ", nIters, nBddSize );
-        if ( fInternalReorder && pPars->fReorder && nBddSize > nThreshold )
-        {
-            if ( pPars->fVerbose )
-                fprintf( stdout, "Reordering... Before = %5d. ", Cudd_DagSize(bReached) );
-            Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
-            Cudd_AutodynDisable( dd );
-            if ( pPars->fVerbose )
-                fprintf( stdout, "After = %5d.\r", Cudd_DagSize(bReached) );
-            nThreshold *= 2;
-        }
-        if ( pPars->fVerbose )
-//            fprintf( stdout, "\r" );
-            fprintf( stdout, "\n" );
-
-        if ( pPars->fVerbose )
-        {
-            double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
-//            Extra_bddPrint( dd, bReached );printf( "\n" );
-            fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
-            fflush( stdout ); 
-        }
-
-    }
-    Cudd_RecursiveDeref( dd, bNext );
-    // free the onion rings
-    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
-        Cudd_RecursiveDeref( dd, bTemp );
-    Vec_PtrFree( vOnionRings );
-    // undo the image tree
-    if ( pPars->fPartition )
-        Bbr_bddImageTreeDelete( pTree );
-    else
-        Bbr_bddImageTreeDelete2( pTree2 );
-    if ( bReached == NULL )
-        return 0; // proved reachable
-    // report the stats
-    if ( pPars->fVerbose )
-    {
-        double nMints = Cudd_CountMinterm(dd, bReached, Saig_ManRegNum(p) );
-        if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
-            fprintf( stdout, "Reachability analysis is stopped after %d frames.\n", nIters );
-        else
-            fprintf( stdout, "Reachability analysis completed after %d frames.\n", nIters );
-        fprintf( stdout, "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p)) );
-        fflush( stdout );
-    }
-//ABC_PRB( dd, bReached );
-    Cudd_RecursiveDeref( dd, bReached );
-    if ( nIters > pPars->nIterMax || nBddSize > pPars->nBddMax )
-    {
-        if ( !pPars->fSilent )
-            printf( "Verified only for states reachable in %d frames.  ", nIters );
-        return -1; // undecided
-    }
-    if ( !pPars->fSilent )
-        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
-    pPars->iFrame = nIters - 1;
-    return 1; // unreachable
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs reachability to see if any PO can be asserted.]
-
-  Description []
-               
-  SideEffects []
- 
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManVerifyUsingBdds_int( Aig_Man_t * p, Saig_ParBbr_t * pPars )
-{
-    int fCheckOutputs = !pPars->fSkipOutCheck;
-    DdManager * dd;
-    DdNode ** pbParts, ** pbOutputs;
-    DdNode * bInitial, * bTemp;
-    int RetValue, i, clk = clock();
-    Vec_Ptr_t * vOnionRings;
-
-    assert( Saig_ManRegNum(p) > 0 );
-
-    // compute the global BDDs of the latches
-    dd = Aig_ManComputeGlobalBdds( p, pPars->nBddMax, 1, pPars->fReorder, pPars->fVerbose );    
-    if ( dd == NULL )
-    {
-        if ( !pPars->fSilent )
-            printf( "The number of intermediate BDD nodes exceeded the limit (%d).\n", pPars->nBddMax );
-        return -1;
-    }
-    if ( pPars->fVerbose )
-        printf( "Shared BDD size is %6d nodes.\n", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
-
-    // check the runtime limit
-    if ( pPars->TimeLimit && ((float)pPars->TimeLimit <= (float)(clock()-clk)/(float)(CLOCKS_PER_SEC)) )
-    {
-        printf( "Reached timeout after constructing global BDDs (%d seconds).\n",  pPars->TimeLimit );
-        Cudd_Quit( dd );
-        return -1;
-    }
-
-    // start the onion rings
-    vOnionRings = Vec_PtrAlloc( 1000 );
-
-    // save outputs
-    pbOutputs = Aig_ManCreateOutputs( dd, p );
-
-    // create partitions
-    pbParts = Aig_ManCreatePartitions( dd, p, pPars->fReorder, pPars->fVerbose );
-
-    // create the initial state and the variable map
-    bInitial  = Aig_ManInitStateVarMap( dd, p, pPars->fVerbose );  Cudd_Ref( bInitial );
-
-    // set reordering
-    if ( pPars->fReorderImage )
-        Cudd_AutodynEnable( dd, CUDD_REORDER_SYMM_SIFT );
-
-    // check the result
-    RetValue = -1;
-    for ( i = 0; i < Saig_ManPoNum(p); i++ )
-    {
-        if ( fCheckOutputs && !Cudd_bddLeq( dd, bInitial, Cudd_Not(pbOutputs[i]) ) )
-        {
-            DdNode * bIntersect;
-            bIntersect = Cudd_bddIntersect( dd, bInitial, pbOutputs[i] );  Cudd_Ref( bIntersect );
-            assert( p->pSeqModel == NULL );
-            p->pSeqModel = Aig_ManVerifyUsingBddsCountExample( p, dd, pbParts, 
-                vOnionRings, bIntersect, i, pPars->fVerbose, pPars->fSilent ); 
-            Cudd_RecursiveDeref( dd, bIntersect );
-            if ( !pPars->fSilent )
-                printf( "The miter output %d is proved REACHABLE in the initial state (use \"write_counter\" to dump a witness). ", i );
-            RetValue = 0;
-            break;
-        }
-    }
-    // free the onion rings
-    Vec_PtrForEachEntry( DdNode *, vOnionRings, bTemp, i )
-        Cudd_RecursiveDeref( dd, bTemp );
-    Vec_PtrFree( vOnionRings );
-    // explore reachable states
-    if ( RetValue == -1 )
-        RetValue = Aig_ManComputeReachable( dd, p, pbParts, bInitial, pbOutputs, pPars, fCheckOutputs ); 
-
-    // cleanup
-    Cudd_RecursiveDeref( dd, bInitial );
-    for ( i = 0; i < Saig_ManRegNum(p); i++ )
-        Cudd_RecursiveDeref( dd, pbParts[i] );
-    ABC_FREE( pbParts );
-    for ( i = 0; i < Saig_ManPoNum(p); i++ )
-        Cudd_RecursiveDeref( dd, pbOutputs[i] );
-    ABC_FREE( pbOutputs );
-//    if ( RetValue == -1 )
-        Cudd_Quit( dd );
-//    else
-//        Bbr_StopManager( dd );
-
-    // report the runtime
-    if ( !pPars->fSilent )
-    {
-    ABC_PRT( "Time", clock() - clk );
-    fflush( stdout );
-    }
-    return RetValue;
-}
-
-/**Function*************************************************************
-
-  Synopsis    [Performs reachability to see if any PO can be asserted.]
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
-{
-    Abc_Cex_t * pCexOld, * pCexNew;
-    Aig_Man_t * p;
-    Aig_Obj_t * pObj;
-    Vec_Int_t * vInputMap;
-    int i, k, Entry, iBitOld, iBitNew, RetValue;
-//    pPars->fVerbose = 1;
-    // check if there are PIs without fanout
-    Saig_ManForEachPi( pInit, pObj, i )
-        if ( Aig_ObjRefs(pObj) == 0 )
-            break;
-    if ( i == Saig_ManPiNum(pInit) )
-        return Aig_ManVerifyUsingBdds_int( pInit, pPars );
-    // create new AIG
-    p = Aig_ManDupTrim( pInit );
-    assert( Aig_ManPiNum(p) < Aig_ManPiNum(pInit) );
-    assert( Aig_ManRegNum(p) == Aig_ManRegNum(pInit) );
-    RetValue = Aig_ManVerifyUsingBdds_int( p, pPars );
-    if ( RetValue != 0 )
-    {
-        Aig_ManStop( p );
-        return RetValue;
-    }
-    // the problem is satisfiable - remap the pattern
-    pCexOld = p->pSeqModel;
-    assert( pCexOld != NULL );
-    // create input map
-    vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
-    Saig_ManForEachPi( pInit, pObj, i )
-        if ( pObj->pData != NULL )
-            Vec_IntPush( vInputMap, Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) );
-        else
-            Vec_IntPush( vInputMap, -1 );
-    // create new pattern
-    pCexNew = Abc_CexAlloc( Saig_ManRegNum(pInit), Saig_ManPiNum(pInit), pCexOld->iFrame+1 );
-    pCexNew->iFrame = pCexOld->iFrame;
-    pCexNew->iPo    = pCexOld->iPo;
-    // copy the bit-data
-    for ( iBitOld = 0; iBitOld < pCexOld->nRegs; iBitOld++ )
-        if ( Aig_InfoHasBit( pCexOld->pData, iBitOld ) )
-            Aig_InfoSetBit( pCexNew->pData, iBitOld );
-    // copy the primary input data
-    iBitNew = iBitOld;
-    for ( i = 0; i <= pCexNew->iFrame; i++ )
-    {
-        Vec_IntForEachEntry( vInputMap, Entry, k )
-        {
-            if ( Entry == -1 )
-                continue;
-            if ( Aig_InfoHasBit( pCexOld->pData, iBitOld + Entry ) )
-                Aig_InfoSetBit( pCexNew->pData, iBitNew + k );
-        }
-        iBitOld += Saig_ManPiNum(p);
-        iBitNew += Saig_ManPiNum(pInit);
-    }
-    assert( iBitOld < iBitNew );
-    assert( iBitOld == pCexOld->nBits );
-    assert( iBitNew == pCexNew->nBits );
-    Vec_IntFree( vInputMap );
-    pInit->pSeqModel = pCexNew;
-    Aig_ManStop( p );
-    return 0;
-}
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/bbr/bbr_.c b/src/aig/bbr/bbr_.c
deleted file mode 100644
index df934f7d..00000000
--- a/src/aig/bbr/bbr_.c
+++ /dev/null
@@ -1,52 +0,0 @@
-/**CFile****************************************************************
-
-  FileName    [.c]
-
-  SystemName  [ABC: Logic synthesis and verification system.]
-
-  PackageName []
-
-  Synopsis    []
-
-  Author      [Alan Mishchenko]
-  
-  Affiliation [UC Berkeley]
-
-  Date        [Ver. 1.0. Started - June 20, 2005.]
-
-  Revision    [$Id: .c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
-
-***********************************************************************/
-
-#include "__Int.h"
-
-ABC_NAMESPACE_IMPL_START
-
-
-////////////////////////////////////////////////////////////////////////
-///                        DECLARATIONS                              ///
-////////////////////////////////////////////////////////////////////////
-
-////////////////////////////////////////////////////////////////////////
-///                     FUNCTION DEFINITIONS                         ///
-////////////////////////////////////////////////////////////////////////
-
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-
-////////////////////////////////////////////////////////////////////////
-///                       END OF FILE                                ///
-////////////////////////////////////////////////////////////////////////
-
-
-ABC_NAMESPACE_IMPL_END
-
diff --git a/src/aig/bbr/module.make b/src/aig/bbr/module.make
deleted file mode 100644
index dce30a21..00000000
--- a/src/aig/bbr/module.make
+++ /dev/null
@@ -1,4 +0,0 @@
-SRC +=    src/aig/bbr/bbrCex.c \
-    src/aig/bbr/bbrImage.c \
-    src/aig/bbr/bbrNtbdd.c \
-    src/aig/bbr/bbrReach.c