Cumulative changes of the last two weeks.

1 files changed, 905 insertions, 0 deletions

diff --git a/src/aig/llb/llb3Image.c b/src/aig/llb/llb3Image.c
new file mode 100644
index 00000000..d040b342
--- /dev/null
+++ b/src/aig/llb/llb3Image.c
@@ -0,0 +1,905 @@
+/**CFile****************************************************************
+
+  FileName    [llb3Image.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Computes image using partitioned structure.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llb3Image.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Llb_Var_t_ Llb_Var_t;
+struct Llb_Var_t_ 
+{
+    int           iVar;      // variable number
+    int           nScore;    // variable score
+    Vec_Int_t *   vParts;    // partitions
+};
+
+typedef struct Llb_Prt_t_ Llb_Prt_t;
+struct Llb_Prt_t_ 
+{
+    int           iPart;     // partition number
+    int           nSize;     // the number of BDD nodes
+    DdNode *      bFunc;     // the partition
+    Vec_Int_t *   vVars;     // support
+};
+
+typedef struct Llb_Mgr_t_ Llb_Mgr_t;
+struct Llb_Mgr_t_
+{
+    Aig_Man_t *   pAig;      // AIG manager
+    Vec_Ptr_t *   vLeaves;   // leaves in the AIG manager
+    Vec_Ptr_t *   vRoots;    // roots in the AIG manager
+    DdManager *   dd;        // working BDD manager
+    DdNode *      bCurrent;  // current state functions in terms of vLeaves
+    int *         pVars2Q;   // variables to quantify
+    // internal
+    Llb_Prt_t **  pParts;    // partitions
+    Llb_Var_t **  pVars;     // variables
+    int           iPartFree; // next free partition
+    int           nVars;     // the number of BDD variables
+    int           nSuppMax;  // maximum support size
+    // temporary
+    int *         pSupp;     // temporary support storage
+};
+
+static inline Llb_Var_t * Llb_MgrVar( Llb_Mgr_t * p, int i )   { return p->pVars[i];  }
+static inline Llb_Prt_t * Llb_MgrPart( Llb_Mgr_t * p, int i )  { return p->pParts[i]; }
+
+// iterator over vars
+#define Llb_MgrForEachVar( p, pVar, i )     \
+    for ( i = 0; (i < p->nVars) && (((pVar) = Llb_MgrVar(p, i)), 1); i++ ) if ( pVar == NULL ) {} else
+// iterator over parts
+#define Llb_MgrForEachPart( p, pPart, i )   \
+    for ( i = 0; (i < p->iPartFree) && (((pPart) = Llb_MgrPart(p, i)), 1); i++ ) if ( pPart == NULL ) {} else
+
+// iterator over vars of one partition
+#define Llb_PartForEachVar( p, pPart, pVar, i )   \
+    for ( i = 0; (i < Vec_IntSize(pPart->vVars)) && (((pVar) = Llb_MgrVar(p, Vec_IntEntry(pPart->vVars,i))), 1); i++ )
+// iterator over parts of one variable
+#define Llb_VarForEachPart( p, pVar, pPart, i )   \
+    for ( i = 0; (i < Vec_IntSize(pVar->vParts)) && (((pPart) = Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,i))), 1); i++ )
+
+// statistics
+int timeBuild, timeAndEx, timeOther;
+int nSuppMax;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one variable.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinRemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
+{
+    assert( p->pVars[pVar->iVar] == pVar );
+    p->pVars[pVar->iVar] = NULL;
+    Vec_IntFree( pVar->vParts );
+    ABC_FREE( pVar );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Removes one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinRemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
+{
+    assert( p->pParts[pPart->iPart] == pPart );
+    p->pParts[pPart->iPart] = NULL;
+    Vec_IntFree( pPart->vVars );
+    Cudd_RecursiveDeref( p->dd, pPart->bFunc );
+    ABC_FREE( pPart );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create cube with singleton variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_NonlinCreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
+{
+    DdNode * bCube, * bTemp;
+    Llb_Var_t * pVar;
+    int i;
+    bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
+    Llb_PartForEachVar( p, pPart, pVar, i )
+    {
+        assert( Vec_IntSize(pVar->vParts) > 0 );
+        if ( Vec_IntSize(pVar->vParts) != 1 )
+            continue;
+        assert( Vec_IntEntry(pVar->vParts, 0) == pPart->iPart );
+        bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) );    Cudd_Ref( bCube );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    Cudd_Deref( bCube );
+    return bCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create cube of variables appearing only in two partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_NonlinCreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
+{
+    DdNode * bCube, * bTemp;
+    Llb_Var_t * pVar;
+    int i;
+    bCube = Cudd_ReadOne(p->dd);   Cudd_Ref( bCube );
+    Llb_PartForEachVar( p, pPart1, pVar, i )
+    {
+        assert( Vec_IntSize(pVar->vParts) > 0 );
+        if ( Vec_IntSize(pVar->vParts) != 2 )
+            continue;
+        if ( (Vec_IntEntry(pVar->vParts, 0) == pPart1->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart2->iPart) ||
+             (Vec_IntEntry(pVar->vParts, 0) == pPart2->iPart && Vec_IntEntry(pVar->vParts, 1) == pPart1->iPart) )
+        {
+            bCube = Cudd_bddAnd( p->dd, bTemp = bCube, Cudd_bddIthVar(p->dd, pVar->iVar) );   Cudd_Ref( bCube );
+            Cudd_RecursiveDeref( p->dd, bTemp );
+        }
+    }
+    Cudd_Deref( bCube );
+    return bCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if partition has singleton variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_NonlinHasSingletonVars( Llb_Mgr_t * p, Llb_Prt_t * pPart )
+{
+    Llb_Var_t * pVar;
+    int i;
+    Llb_PartForEachVar( p, pPart, pVar, i )
+        if ( Vec_IntSize(pVar->vParts) == 1 )
+            return 1;
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if partition has singleton variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinPrint( Llb_Mgr_t * p )
+{
+    Llb_Prt_t * pPart;
+    Llb_Var_t * pVar;
+    int i, k;
+    printf( "\n" );
+    Llb_MgrForEachVar( p, pVar, i )
+    {
+        printf( "Var %3d : ", i );
+        Llb_VarForEachPart( p, pVar, pPart, k )
+            printf( "%d ", pPart->iPart );
+        printf( "\n" );
+    }
+    Llb_MgrForEachPart( p, pPart, i )
+    {
+        printf( "Part %3d : ", i );
+        Llb_PartForEachVar( p, pPart, pVar, k )
+            printf( "%d ", pVar->iVar );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Quantifies singles belonging to one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_NonlinQuantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart, int fSubset )
+{
+    Llb_Var_t * pVar;
+    Llb_Prt_t * pTemp;
+    Vec_Ptr_t * vSingles;
+    DdNode * bCube, * bTemp;
+    int i, RetValue, nSizeNew;
+    if ( fSubset )
+    {        
+        int Length;
+//        int nSuppSize = Cudd_SupportSize( p->dd, pPart->bFunc );
+//        pPart->bFunc = Cudd_SubsetHeavyBranch( p->dd, bTemp = pPart->bFunc, nSuppSize, 3*pPart->nSize/4 );  Cudd_Ref( pPart->bFunc );
+        pPart->bFunc = Cudd_LargestCube( p->dd, bTemp = pPart->bFunc, &Length );  Cudd_Ref( pPart->bFunc );
+
+        printf( "Subsetting %3d : ", pPart->iPart );
+        printf( "(Supp =%3d  Node =%5d) -> ", Cudd_SupportSize(p->dd, bTemp),        Cudd_DagSize(bTemp) );
+        printf( "(Supp =%3d  Node =%5d)\n",   Cudd_SupportSize(p->dd, pPart->bFunc), Cudd_DagSize(pPart->bFunc) );
+
+        RetValue = (Cudd_DagSize(bTemp) == Cudd_DagSize(pPart->bFunc));
+
+        Cudd_RecursiveDeref( p->dd, bTemp );
+
+        if ( RetValue )
+            return 1;
+    }
+    else
+    {
+        // create cube to be quantified
+        bCube = Llb_NonlinCreateCube1( p, pPart );   Cudd_Ref( bCube );
+//        assert( !Cudd_IsConstant(bCube) );
+        // derive new function
+        pPart->bFunc = Cudd_bddExistAbstract( p->dd, bTemp = pPart->bFunc, bCube );  Cudd_Ref( pPart->bFunc );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+        Cudd_RecursiveDeref( p->dd, bCube );
+    }
+    // get support
+    vSingles = Vec_PtrAlloc( 0 );
+    nSizeNew = Cudd_DagSize(pPart->bFunc);
+    Extra_SupportArray( p->dd, pPart->bFunc, p->pSupp );
+    Llb_PartForEachVar( p, pPart, pVar, i )
+        if ( p->pSupp[pVar->iVar] )
+        {
+            assert( Vec_IntSize(pVar->vParts) > 1 );
+            pVar->nScore -= pPart->nSize - nSizeNew;
+        }
+        else
+        {
+            RetValue = Vec_IntRemove( pVar->vParts, pPart->iPart );
+            assert( RetValue );
+            pVar->nScore -= pPart->nSize;
+            if ( Vec_IntSize(pVar->vParts) == 0 )
+                Llb_NonlinRemoveVar( p, pVar );
+            else if ( Vec_IntSize(pVar->vParts) == 1 )
+                Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
+        }
+
+    // update partition
+    pPart->nSize = nSizeNew;
+    Vec_IntClear( pPart->vVars );
+    for ( i = 0; i < p->nVars; i++ )
+        if ( p->pSupp[i] && p->pVars2Q[i] )
+            Vec_IntPush( pPart->vVars, i );
+    // remove other variables
+    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
+        Llb_NonlinQuantify1( p, pTemp, 0 );
+    Vec_PtrFree( vSingles );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Quantifies singles belonging to one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_NonlinQuantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2, int Limit )
+{
+    int fVerbose = 0;
+    Llb_Var_t * pVar;
+    Llb_Prt_t * pTemp;
+    Vec_Ptr_t * vSingles;
+    DdNode * bCube, * bFunc;
+    int i, RetValue, nSuppSize;
+    int iPart1 = pPart1->iPart;
+    int iPart2 = pPart2->iPart;
+
+    // create cube to be quantified
+    bCube = Llb_NonlinCreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
+if ( fVerbose )
+{
+printf( "\n" );
+printf( "\n" );
+Llb_NonlinPrint( p );
+printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
+Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
+}
+
+    // derive new function
+//    bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  Cudd_Ref( bFunc );
+    bFunc = Cudd_bddAndAbstractLimit( p->dd, pPart1->bFunc, pPart2->bFunc, bCube, Limit );  
+    if ( bFunc == NULL )
+    {
+/*
+        int RetValue;
+        Cudd_RecursiveDeref( p->dd, bCube );
+        if ( pPart1->nSize < pPart2->nSize )
+            RetValue = Llb_NonlinQuantify1( p, pPart1, 1 );
+        else
+            RetValue = Llb_NonlinQuantify1( p, pPart2, 1 );
+        if ( RetValue )
+            Limit = Limit + 1000;
+        Llb_NonlinQuantify2( p, pPart1, pPart2, Limit );
+*/
+        return 1;
+    }
+    Cudd_Ref( bFunc );
+    Cudd_RecursiveDeref( p->dd, bCube );
+    // create new partition
+    pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
+    pTemp->iPart = p->iPartFree++;
+    pTemp->nSize = Cudd_DagSize(bFunc);
+    pTemp->bFunc = bFunc;
+    pTemp->vVars = Vec_IntAlloc( 8 );
+    // update variables
+    Llb_PartForEachVar( p, pPart1, pVar, i )
+    {
+        RetValue = Vec_IntRemove( pVar->vParts, pPart1->iPart );
+        assert( RetValue );
+        pVar->nScore -= pPart1->nSize;
+    }
+    // update variables
+    Llb_PartForEachVar( p, pPart2, pVar, i )
+    {
+        RetValue = Vec_IntRemove( pVar->vParts, pPart2->iPart );
+        assert( RetValue );
+        pVar->nScore -= pPart2->nSize;
+    }
+    // add variables to the new partition
+    nSuppSize = 0;
+    Extra_SupportArray( p->dd, bFunc, p->pSupp );
+    for ( i = 0; i < p->nVars; i++ )
+    {
+        nSuppSize += p->pSupp[i];
+        if ( p->pSupp[i] && p->pVars2Q[i] )
+        {
+            pVar = Llb_MgrVar( p, i );
+            pVar->nScore += pTemp->nSize;
+            Vec_IntPush( pVar->vParts, pTemp->iPart );
+            Vec_IntPush( pTemp->vVars, i );
+        }
+    }
+    p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); 
+    // remove variables and collect partitions with singleton variables
+    vSingles = Vec_PtrAlloc( 0 );
+    Llb_PartForEachVar( p, pPart1, pVar, i )
+    {
+        if ( Vec_IntSize(pVar->vParts) == 0 )
+            Llb_NonlinRemoveVar( p, pVar );
+        else if ( Vec_IntSize(pVar->vParts) == 1 )
+        {
+            if ( fVerbose )
+                printf( "Adding partition %d because of var %d.\n", 
+                    Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
+            Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
+        }
+    }
+    Llb_PartForEachVar( p, pPart2, pVar, i )
+    {
+        if ( pVar == NULL )
+            continue;
+        if ( Vec_IntSize(pVar->vParts) == 0 )
+            Llb_NonlinRemoveVar( p, pVar );
+        else if ( Vec_IntSize(pVar->vParts) == 1 )
+        {
+            if ( fVerbose )
+                printf( "Adding partition %d because of var %d.\n", 
+                    Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0))->iPart, pVar->iVar );
+            Vec_PtrPushUnique( vSingles, Llb_MgrPart(p, Vec_IntEntry(pVar->vParts,0)) );
+        }
+    }
+    // remove partitions
+    Llb_NonlinRemovePart( p, pPart1 );
+    Llb_NonlinRemovePart( p, pPart2 );
+    // remove other variables
+if ( fVerbose )
+Llb_NonlinPrint( p );
+    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
+    {
+if ( fVerbose )
+printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
+        Llb_NonlinQuantify1( p, pTemp, 0 );
+    }
+if ( fVerbose )
+Llb_NonlinPrint( p );
+    Vec_PtrFree( vSingles );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes volume of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinCutNodes_rec( Aig_Man_t * p, Aig_Obj_t * pObj, Vec_Ptr_t * vNodes )
+{
+    if ( Aig_ObjIsTravIdCurrent(p, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent(p, pObj);
+    if ( Saig_ObjIsLi(p, pObj) )
+    {
+        Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
+        return;
+    }
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Llb_NonlinCutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
+    Llb_NonlinCutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes volume of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_NonlinCutNodes( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper )
+{
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    // mark the lower cut with the traversal ID
+    Aig_ManIncrementTravId(p);
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
+        Aig_ObjSetTravIdCurrent( p, pObj );
+    // count the upper cut
+    vNodes = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
+        Llb_NonlinCutNodes_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns array of BDDs for the roots in terms of the leaves.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_NonlinBuildBdds( Aig_Man_t * p, Vec_Ptr_t * vLower, Vec_Ptr_t * vUpper, DdManager * dd )
+{
+    Vec_Ptr_t * vNodes, * vResult;
+    Aig_Obj_t * pObj;
+    DdNode * bBdd0, * bBdd1, * bProd;
+    int i;
+
+    Aig_ManConst1(p)->pData = Cudd_ReadOne( dd );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vLower, pObj, i )
+        pObj->pData = Cudd_bddIthVar( dd, Aig_ObjId(pObj) );
+
+    vNodes = Llb_NonlinCutNodes( p, vLower, vUpper );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        pObj->pData = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( (DdNode *)pObj->pData );
+    }
+
+    vResult = Vec_PtrAlloc( 100 );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vUpper, pObj, i )
+    {
+        if ( Aig_ObjIsNode(pObj) )
+        {
+            bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), (DdNode *)pObj->pData );  Cudd_Ref( bProd );
+        }
+        else
+        {
+            assert( Saig_ObjIsLi(p, pObj) );
+            bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+            bProd = Cudd_bddXnor( dd, Cudd_bddIthVar(dd, Aig_ObjId(pObj)), bBdd0 );                  Cudd_Ref( bProd );
+        }
+        Vec_PtrPush( vResult, bProd );
+    }
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+
+    Vec_PtrFree( vNodes );
+    return vResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinAddPair( Llb_Mgr_t * p, DdNode * bFunc, int iPart, int iVar )
+{
+    if ( p->pVars[iVar] == NULL )
+    {
+        p->pVars[iVar] = ABC_CALLOC( Llb_Var_t, 1 );
+        p->pVars[iVar]->iVar   = iVar;
+        p->pVars[iVar]->nScore = 0;
+        p->pVars[iVar]->vParts = Vec_IntAlloc( 8 );
+    }
+    Vec_IntPush( p->pVars[iVar]->vParts, iPart );
+    Vec_IntPush( p->pParts[iPart]->vVars, iVar );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinStart( Llb_Mgr_t * p )
+{
+    Vec_Ptr_t * vRootBdds;
+    Llb_Prt_t * pPart;
+    DdNode * bFunc;
+    int i, k, nSuppSize;
+    // create and collect BDDs
+    vRootBdds = Llb_NonlinBuildBdds( p->pAig, p->vLeaves, p->vRoots, p->dd ); // come referenced
+    Vec_PtrPush( vRootBdds, p->bCurrent );
+    // add pairs (refs are consumed inside)
+    Vec_PtrForEachEntry( DdNode *, vRootBdds, bFunc, i )
+    {
+        assert( !Cudd_IsConstant(bFunc) );
+        // create partition
+        p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
+        p->pParts[i]->iPart = i;
+        p->pParts[i]->bFunc = bFunc;
+        p->pParts[i]->vVars = Vec_IntAlloc( 8 );
+        // add support dependencies
+        nSuppSize = 0;
+        Extra_SupportArray( p->dd, bFunc, p->pSupp );
+        for ( k = 0; k < p->nVars; k++ )
+        {
+            nSuppSize += p->pSupp[k];
+            if ( p->pSupp[k] && p->pVars2Q[k] )
+                Llb_NonlinAddPair( p, bFunc, i, k );
+        }
+        p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); 
+    }
+    Vec_PtrFree( vRootBdds );
+    // remove singles
+    Llb_MgrForEachPart( p, pPart, i )
+        if ( Llb_NonlinHasSingletonVars(p, pPart) )
+            Llb_NonlinQuantify1( p, pPart, 0 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks that each var appears in at least one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinCheckVars( Llb_Mgr_t * p )
+{
+    Llb_Var_t * pVar;
+    int i;
+    Llb_MgrForEachVar( p, pVar, i )
+        assert( Vec_IntSize(pVar->vParts) > 1 );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find next partition to quantify]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_NonlinNextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t ** ppPart2 )
+{
+    Llb_Var_t * pVar, * pVarBest = NULL;
+    Llb_Prt_t * pPart, * pPart1Best = NULL, * pPart2Best = NULL;
+    int i;
+    Llb_NonlinCheckVars( p );
+    // find variable with minimum score
+    Llb_MgrForEachVar( p, pVar, i )
+        if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
+            pVarBest = pVar;
+    if ( pVarBest == NULL )
+        return 0;
+    // find two partitions with minimum size
+    Llb_VarForEachPart( p, pVarBest, pPart, i )
+    {
+        if ( pPart1Best == NULL )
+            pPart1Best = pPart;
+        else if ( pPart2Best == NULL )
+            pPart2Best = pPart;
+        else if ( pPart1Best->nSize > pPart->nSize || pPart2Best->nSize > pPart->nSize )
+        {
+            if ( pPart1Best->nSize > pPart2Best->nSize )
+                pPart1Best = pPart;
+            else
+                pPart2Best = pPart;
+        }
+    }
+    *ppPart1 = pPart1Best;
+    *ppPart2 = pPart2Best;
+    return 1; 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs in the working manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinReorder( DdManager * dd, int fVerbose )
+{
+    int clk = clock();
+    if ( fVerbose )
+        Abc_Print( 1, "Reordering... Before =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+    if ( fVerbose )
+        Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    Cudd_ReduceHeap( dd, CUDD_REORDER_SYMM_SIFT, 100 );
+    if ( fVerbose )
+        Abc_Print( 1, "After =%5d. ", Cudd_ReadKeys(dd) - Cudd_ReadDead(dd) );
+    if ( fVerbose )
+        Abc_PrintTime( 1, "Time", clock() - clk );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recomputes scores after variable reordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinRecomputeScores( Llb_Mgr_t * p )
+{
+    Llb_Prt_t * pPart;
+    Llb_Var_t * pVar;
+    int i, k;
+    Llb_MgrForEachPart( p, pPart, i )
+        pPart->nSize = Cudd_DagSize(pPart->bFunc);
+    Llb_MgrForEachVar( p, pVar, i )
+    {
+        pVar->nScore = 0;
+        Llb_VarForEachPart( p, pVar, pPart, k )
+            pVar->nScore += pPart->nSize;
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Recomputes scores after variable reordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinVerifyScores( Llb_Mgr_t * p )
+{
+    Llb_Prt_t * pPart;
+    Llb_Var_t * pVar;
+    int i, k, nScore;
+    Llb_MgrForEachPart( p, pPart, i )
+        assert( pPart->nSize == Cudd_DagSize(pPart->bFunc) );
+    Llb_MgrForEachVar( p, pVar, i )
+    {
+        nScore = 0;
+        Llb_VarForEachPart( p, pVar, pPart, k )
+            nScore += pPart->nSize;
+        assert( nScore == pVar->nScore );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Mgr_t * Llb_NonlinAlloc( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, DdManager * dd, DdNode * bCurrent )
+{
+    Llb_Mgr_t * p;
+    p = ABC_CALLOC( Llb_Mgr_t, 1 );
+    p->pAig      = pAig;
+    p->vLeaves   = vLeaves;
+    p->vRoots    = vRoots;
+    p->dd        = dd;
+    p->bCurrent  = bCurrent;
+    p->pVars2Q   = pVars2Q;
+    p->nVars     = Cudd_ReadSize(dd);
+    p->iPartFree = Vec_PtrSize(vRoots) + 1;
+    p->pVars     = ABC_CALLOC( Llb_Var_t *, p->nVars );
+    p->pParts    = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree );
+    p->pSupp     = ABC_ALLOC( int, Cudd_ReadSize(dd) );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_NonlinFree( Llb_Mgr_t * p )
+{
+    Llb_Prt_t * pPart;
+    Llb_Var_t * pVar;
+    int i;
+    Llb_MgrForEachVar( p, pVar, i )
+        Llb_NonlinRemoveVar( p, pVar );
+    Llb_MgrForEachPart( p, pPart, i )
+        Llb_NonlinRemovePart( p, pPart );
+    ABC_FREE( p->pVars );
+    ABC_FREE( p->pParts );
+    ABC_FREE( p->pSupp );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs image computation.]
+
+  Description [Computes image of BDDs (vFuncs).]
+               
+  SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, Vec_Ptr_t * vRoots, int * pVars2Q, 
+    DdManager * dd, DdNode * bCurrent, int fReorder, int fVerbose, int * pOrder, int Limit )
+{
+    Llb_Prt_t * pPart, * pPart1, * pPart2;
+    Llb_Mgr_t * p;
+    DdNode * bFunc, * bTemp;
+    int i, nReorders, timeInside;
+    int clk = clock(), clk2;
+    // start the manager
+    clk2 = clock();
+    p = Llb_NonlinAlloc( pAig, vLeaves, vRoots, pVars2Q, dd, bCurrent );
+    Llb_NonlinStart( p );
+    timeBuild += clock() - clk2;
+    timeInside = clock() - clk2;
+    // compute scores
+    Llb_NonlinRecomputeScores( p );
+    // save permutation
+    memcpy( pOrder, dd->invperm, sizeof(int) * dd->size );
+    // iteratively quantify variables
+    while ( Llb_NonlinNextPartitions(p, &pPart1, &pPart2) )
+    {
+        clk2 = clock();
+        nReorders = Cudd_ReadReorderings(dd);
+        if ( Llb_NonlinQuantify2( p, pPart1, pPart2, Limit ) )
+        {
+            Llb_NonlinFree( p );
+            return NULL;
+        }
+        timeAndEx  += clock() - clk2;
+        timeInside += clock() - clk2;
+        if ( nReorders < Cudd_ReadReorderings(dd) )
+            Llb_NonlinRecomputeScores( p );
+//        else
+//            Llb_NonlinVerifyScores( p );
+    }
+    // load partitions
+    bFunc = Cudd_ReadOne(p->dd);   Cudd_Ref( bFunc );
+    Llb_MgrForEachPart( p, pPart, i )
+    {
+        bFunc = Cudd_bddAnd( p->dd, bTemp = bFunc, pPart->bFunc );   Cudd_Ref( bFunc );
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    }
+    nSuppMax = p->nSuppMax;
+    Llb_NonlinFree( p );
+    // reorder variables
+    if ( fReorder )
+        Llb_NonlinReorder( dd, fVerbose );
+    timeOther += clock() - clk - timeInside;
+    // return
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+