Improvements to BDD reachability.

2 files changed, 589 insertions, 1 deletions

diff --git a/src/aig/llb/llb4Sweep.c b/src/aig/llb/llb4Sweep.c
new file mode 100644
index 00000000..d13c366f
--- /dev/null
+++ b/src/aig/llb/llb4Sweep.c
@@ -0,0 +1,588 @@
+/**CFile****************************************************************
+
+  FileName    [llb2Sweep.c]
+
+  SystemName  [ABC: Logic synthesis and verification system.]
+
+  PackageName [BDD based reachability.]
+
+  Synopsis    [Non-linear quantification scheduling.]
+
+  Author      [Alan Mishchenko]
+  
+  Affiliation [UC Berkeley]
+
+  Date        [Ver. 1.0. Started - June 20, 2005.]
+
+  Revision    [$Id: llb2Sweep.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4SweepOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter, int fSaveAll )
+{
+    Aig_Obj_t * pFanin0, * pFanin1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent( pAig, pObj );
+    assert( Llb_ObjBddVar(vOrder, pObj) < 0 );
+    if ( Aig_ObjIsPi(pObj) )
+    {
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+        return;
+    }
+    // try fanins with higher level first
+    pFanin0 = Aig_ObjFanin0(pObj);
+    pFanin1 = Aig_ObjFanin1(pObj);
+//    if ( pFanin0->Level > pFanin1->Level || (pFanin0->Level == pFanin1->Level && pFanin0->Id < pFanin1->Id) )
+    if ( pFanin0->Level > pFanin1->Level )
+    {
+        Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
+        Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
+    }
+    else
+    {
+        Llb_Nonlin4SweepOrder_rec( pAig, pFanin1, vOrder, pCounter, fSaveAll );
+        Llb_Nonlin4SweepOrder_rec( pAig, pFanin0, vOrder, pCounter, fSaveAll );
+    }
+    if ( fSaveAll || pObj->fMarkA )
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4SweepOrder( Aig_Man_t * pAig, int * pCounter, int fSaveAll )
+{
+    Vec_Int_t * vOrder;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    // collect nodes in the order
+    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
+    Aig_ManIncrementTravId( pAig );
+    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+        Llb_Nonlin4SweepOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter, fSaveAll );
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
+            Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+//    assert( Counter == Aig_ManObjNum(pAig) - 1 ); // no dangling nodes
+    if ( pCounter )
+        *pCounter = Counter - Aig_ManPiNum(pAig) - Aig_ManPoNum(pAig);
+    return vOrder;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD sweep on the netlist.]
+
+  Description [Returns AIG with internal cut points labeled with fMarkA.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb4_Nonlin4SweepCutpoints( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nBddLimit, int fVerbose )
+{
+    DdManager * dd;
+    DdNode * bFunc0, * bFunc1, * bFunc;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0, Counter1 = 0;
+    dd = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    // assign elementary variables
+    Aig_ManCleanData( pAig );
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
+    // sweep internal nodes
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+/*
+        if ( pObj->nRefs >= 4 )
+        {
+            bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );  Cudd_Ref( bFunc );
+            pObj->pData = bFunc;
+            Counter1++;
+            continue;
+        }
+*/
+        bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+        if ( Cudd_DagSize(bFunc) > nBddLimit )
+        {
+//            if ( fVerbose )
+//                printf( "Node %5d : Beg =%5d. ", i, Cudd_DagSize(bFunc) );
+
+            // add cutpoint at a larger one
+            Cudd_RecursiveDeref( dd, bFunc );
+            if ( Cudd_DagSize(bFunc0) >= Cudd_DagSize(bFunc1) )
+            {
+                Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin0(pObj)->pData );
+                bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin0(pObj)) );
+                Aig_ObjFanin0(pObj)->pData = bFunc;  Cudd_Ref( bFunc );
+                Aig_ObjFanin0(pObj)->fMarkA = 1;
+
+//                if ( fVerbose )
+//                    printf( "Ref =%3d  ", Aig_ObjFanin0(pObj)->nRefs );
+            }
+            else
+            {
+                Cudd_RecursiveDeref( dd, (DdNode *)Aig_ObjFanin1(pObj)->pData );
+                bFunc = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, Aig_ObjFanin1(pObj)) );
+                Aig_ObjFanin1(pObj)->pData = bFunc;  Cudd_Ref( bFunc );
+                Aig_ObjFanin1(pObj)->fMarkA = 1;
+
+//                if ( fVerbose )
+//                    printf( "Ref =%3d  ", Aig_ObjFanin1(pObj)->nRefs );
+            }
+            // perform new operation
+            bFunc0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+            bFunc1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+            bFunc  = Cudd_bddAnd( dd, bFunc0, bFunc1 );  Cudd_Ref( bFunc );
+//            assert( Cudd_DagSize(bFunc) <= nBddLimit );
+
+//            if ( fVerbose )
+//                printf( "End =%5d.\n", Cudd_DagSize(bFunc) );
+            Counter++;
+        }
+        pObj->pData = bFunc;
+//printf( "%d ", Cudd_DagSize(bFunc) );
+    }
+//printf( "\n" );
+    // clean up
+    Aig_ManForEachNode( pAig, pObj, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    Extra_StopManager( dd );
+//    Aig_ManCleanMarkA( pAig );
+    if ( fVerbose )
+    printf( "Added %d cut points.  Used %d high fanout points.\n", Counter, Counter1 );
+    return Counter + Counter1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives BDDs for the partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_Nonlin4SweepPartitions_rec( DdManager * dd, Aig_Obj_t * pObj, Vec_Int_t * vOrder, Vec_Ptr_t * vRoots )
+{
+    DdNode * bBdd, * bBdd0, * bBdd1, * bPart, * vVar;
+    if ( Aig_ObjIsConst1(pObj) )
+        return Cudd_ReadOne(dd); 
+    if ( Aig_ObjIsPi(pObj) )
+        return Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
+    if ( pObj->pData )
+        return (DdNode *)pObj->pData;
+    if ( Aig_ObjIsPo(pObj) )
+    {
+        bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
+        bPart = Cudd_bddXnor( dd, Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) ), bBdd0 );  Cudd_Ref( bPart );
+        Vec_PtrPush( vRoots, bPart );
+        return NULL;
+    }
+    bBdd0 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin0(pObj), vOrder, vRoots), Aig_ObjFaninC0(pObj) );
+    bBdd1 = Cudd_NotCond( Llb_Nonlin4SweepPartitions_rec(dd, Aig_ObjFanin1(pObj), vOrder, vRoots), Aig_ObjFaninC1(pObj) );
+    bBdd  = Cudd_bddAnd( dd, bBdd0, bBdd1 );   Cudd_Ref( bBdd );
+    if ( Llb_ObjBddVar(vOrder, pObj) >= 0 )
+    {
+        vVar  = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
+        bPart = Cudd_bddXnor( dd, vVar, bBdd );  Cudd_Ref( bPart );
+        Vec_PtrPush( vRoots, bPart );
+        Cudd_RecursiveDeref( dd, bBdd );
+        bBdd = vVar;  Cudd_Ref( vVar );
+    }
+    pObj->pData = bBdd;
+    return bBdd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives BDDs for the partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4SweepPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fTransition )
+{
+    Vec_Ptr_t * vRoots;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManCleanData( pAig );
+    vRoots = Vec_PtrAlloc( 100 );
+    if ( fTransition )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+            Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
+    }
+    else
+    {
+        Saig_ManForEachPo( pAig, pObj, i )
+            Llb_Nonlin4SweepPartitions_rec( dd, pObj, vOrder, vRoots );
+    }
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( pObj->pData )
+            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    return vRoots;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Get bad state monitor.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb4_Nonlin4SweepBadMonitor( Aig_Man_t * pAig, Vec_Int_t * vOrder, DdManager * dd )
+{
+    Aig_Obj_t * pObj;
+    DdNode * bRes, * bVar, * bTemp;
+    int i, TimeStop;
+    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
+    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        bVar = Cudd_bddIthVar( dd, Llb_ObjBddVar(vOrder, pObj) );
+        bRes = Cudd_bddAnd( dd, bTemp = bRes, Cudd_Not(bVar) );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bRes );
+    dd->TimeStop = TimeStop;
+    return Cudd_Not(bRes);
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable variables for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4SweepVars2Q( Aig_Man_t * pAig, Vec_Int_t * vOrder, int fAddLis )
+{
+    Vec_Int_t * vVars2Q;
+    Aig_Obj_t * pObj;
+    int i;
+    vVars2Q = Vec_IntAlloc( 0 );
+    Vec_IntFill( vVars2Q, Aig_ManObjNumMax(pAig), 1 );
+    // add flop outputs
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
+    // add flop inputs
+    if ( fAddLis )
+    Saig_ManForEachLi( pAig, pObj, i )
+        Vec_IntWriteEntry( vVars2Q, Llb_ObjBddVar(vOrder, pObj), 0 );
+    return vVars2Q;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Multiply every partition by the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4SweepDeref( DdManager * dd, Vec_Ptr_t * vParts )
+{
+    DdNode * bFunc;
+    int i;
+    Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
+        Cudd_RecursiveDeref( dd, bFunc );
+    Vec_PtrFree( vParts );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Multiply every partition by the cube.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4SweepPrint( Vec_Ptr_t * vFuncs )
+{
+    DdNode * bFunc;
+    int i;
+    printf( "(%d) ", Vec_PtrSize(vFuncs) );
+    Vec_PtrForEachEntry( DdNode *, vFuncs, bFunc, i )
+        printf( "%d ", Cudd_DagSize(bFunc) );
+    printf( "\n" );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes bad states.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Llb4_Nonlin4SweepBadStates( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars )
+{
+    DdManager * dd;
+    Vec_Ptr_t * vParts;
+    Vec_Int_t * vVars2Q;
+    DdNode * bMonitor, * bImage;
+    // get quantifiable variables
+    vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 0 );
+    // start BDD manager and create partitions 
+    dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 0 );
+//printf( "Outputs: " );
+//Llb_Nonlin4SweepPrint( vParts );
+    // compute image of the partitions
+    bMonitor = Llb4_Nonlin4SweepBadMonitor( pAig, vOrder, dd );  Cudd_Ref( bMonitor );
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    bImage = Llb_Nonlin4Image( dd, vParts, bMonitor, vVars2Q );  Cudd_Ref( bImage );
+    Cudd_RecursiveDeref( dd, bMonitor );
+    Llb_Nonlin4SweepDeref( dd, vParts );
+    Vec_IntFree( vVars2Q );
+    // save image and return
+    dd->bFunc = bImage;
+    return dd;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes clusters.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdManager * Llb4_Nonlin4SweepGroups( Aig_Man_t * pAig, Vec_Int_t * vOrder, int nVars, Vec_Ptr_t ** pvGroups, int nBddLimitClp, int fVerbose )
+{
+    DdManager * dd;
+    Vec_Ptr_t * vParts;
+    Vec_Int_t * vVars2Q;
+    // get quantifiable variables
+    vVars2Q = Llb_Nonlin4SweepVars2Q( pAig, vOrder, 1 );
+    // start BDD manager and create partitions 
+    dd = Cudd_Init( nVars, 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    vParts = Llb_Nonlin4SweepPartitions( dd, pAig, vOrder, 1 );
+//printf( "Transitions: " );
+//Llb_Nonlin4SweepPrint( vParts );
+    // compute image of the partitions
+
+    Cudd_AutodynEnable( dd,  CUDD_REORDER_SYMM_SIFT );
+    *pvGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, nBddLimitClp );
+    Llb_Nonlin4SweepDeref( dd, vParts );
+//    *pvGroups = vParts;
+
+if ( fVerbose )
+{
+printf( "Groups: " );
+Llb_Nonlin4SweepPrint( *pvGroups );
+}
+
+    Vec_IntFree( vVars2Q );
+    return dd;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable variables for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4SweepPrintSuppProfile( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups, int fVerbose )
+{
+    Aig_Obj_t * pObj;
+    int i, * pSupp;
+    int nSuppAll = 0, nSuppPi = 0, nSuppPo = 0, nSuppLi = 0, nSuppLo = 0, nSuppAnd = 0;
+
+    pSupp = ABC_CALLOC( int, Cudd_ReadSize(dd) );
+    Extra_VectorSupportArray( dd, (DdNode **)Vec_PtrArray(vGroups), Vec_PtrSize(vGroups), pSupp );
+
+    Aig_ManForEachObj( pAig, pObj, i )
+    {
+        if ( Llb_ObjBddVar(vOrder, pObj) < 0 )
+            continue;
+        // remove variables that do not participate
+        if ( pSupp[Llb_ObjBddVar(vOrder, pObj)] == 0 )
+        {
+            if ( Aig_ObjIsNode(pObj) )
+                Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), -1 );
+            continue;
+        }
+        nSuppAll++;
+        if ( Saig_ObjIsPi(pAig, pObj) )
+            nSuppPi++;
+        else if ( Saig_ObjIsLo(pAig, pObj) )
+            nSuppLo++;
+        else if ( Saig_ObjIsPo(pAig, pObj) )
+            nSuppPo++;
+        else if ( Saig_ObjIsLi(pAig, pObj) )
+            nSuppLi++;
+        else
+            nSuppAnd++;
+    }
+    ABC_FREE( pSupp );
+
+    if ( fVerbose )
+    {
+    printf( "Groups =%3d  ", Vec_PtrSize(vGroups) );
+    printf( "Variables: all =%4d ",  nSuppAll );
+    printf( "pi =%4d ",  nSuppPi );
+    printf( "po =%4d ",  nSuppPo );
+    printf( "lo =%4d ",  nSuppLo );
+    printf( "li =%4d ",  nSuppLi );
+    printf( "and =%4d",  nSuppAnd );
+    printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD sweep on the netlist.]
+
+  Description [Returns BDD manager, ordering, clusters, and bad states 
+  inside dd->bFunc.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nSweepMax, int nClusterMax, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int fVerbose )
+{
+    DdManager * ddBad, * ddWork;
+    Vec_Ptr_t * vGroups;
+    Vec_Int_t * vOrder;
+    int Counter, nCutPoints;
+
+    // get the original ordering
+    Aig_ManCleanMarkA( pAig );
+    vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 1 );
+    assert( Counter == Aig_ManNodeNum(pAig) );
+    // mark the nodes
+    nCutPoints = Llb4_Nonlin4SweepCutpoints( pAig, vOrder, nSweepMax, fVerbose );
+    Vec_IntFree( vOrder );
+    // get better ordering
+    vOrder = Llb_Nonlin4SweepOrder( pAig, &Counter, 0 );
+    assert( Counter == nCutPoints );
+    Aig_ManCleanMarkA( pAig );
+    // compute the BAD states
+    ddBad = Llb4_Nonlin4SweepBadStates( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig) );
+    // compute the clusters
+    ddWork = Llb4_Nonlin4SweepGroups( pAig, vOrder, nCutPoints + Aig_ManPiNum(pAig) + Aig_ManPoNum(pAig), &vGroups, nClusterMax, fVerbose );
+    // transfer the result from the Bad manager
+//printf( "Bad before = %d.\n", Cudd_DagSize(ddBad->bFunc) );
+    ddWork->bFunc = Cudd_bddTransfer( ddBad, ddWork, ddBad->bFunc );   Cudd_Ref( ddWork->bFunc );
+    Cudd_RecursiveDeref( ddBad, ddBad->bFunc );  ddBad->bFunc = NULL;
+    Extra_StopManager( ddBad );
+    // update ordering to exclude quantified variables
+//printf( "Bad after = %d.\n", Cudd_DagSize(ddWork->bFunc) );
+
+    Llb_Nonlin4SweepPrintSuppProfile( ddWork, pAig, vOrder, vGroups, fVerbose );
+
+    // return the result
+    *pdd = ddWork;
+    *pvOrder = vOrder;
+    *pvGroups = vGroups;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs BDD sweep on the netlist.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig )
+{
+    DdManager * dd;
+    Vec_Int_t * vOrder;
+    Vec_Ptr_t * vGroups;
+    Llb4_Nonlin4Sweep( pAig, 100, 500, &dd, &vOrder, &vGroups, 1 );
+
+    Llb_Nonlin4SweepDeref( dd, vGroups );
+
+    Cudd_RecursiveDeref( dd, dd->bFunc );
+    Extra_StopManager( dd );
+    Vec_IntFree( vOrder );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/bdd/cudd/cuddInt.h b/src/bdd/cudd/cuddInt.h
index 09892ba5..229030ca 100644
--- a/src/bdd/cudd/cuddInt.h
+++ b/src/bdd/cudd/cuddInt.h
@@ -147,7 +147,7 @@ ABC_NAMESPACE_HEADER_START
 #define DD_SIFT_MAX_VAR         1000
 #define DD_SIFT_MAX_SWAPS       2000000
 #define DD_DEFAULT_RECOMB       0
-#define DD_MAX_REORDER_GROWTH   1.2
+#define DD_MAX_REORDER_GROWTH   1.1
 #define DD_FIRST_REORDER        4004    /* 4 for the constants */
 #define DD_DYN_RATIO            2       /* when to dynamically reorder */