Experiments with reachability.

5 files changed, 459 insertions, 19 deletions

diff --git a/src/aig/llb/llb4Cluster.c b/src/aig/llb/llb4Cluster.c
new file mode 100644
index 00000000..71e044be
--- /dev/null
+++ b/src/aig/llb/llb4Cluster.c
@@ -0,0 +1,339 @@
+/**CFile****************************************************************
+
+  FileName    [llb2Cluster.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: llb2Cluster.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4FindOrder_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
+{
+    Aig_Obj_t * pFanin0, * pFanin1;
+    if ( Aig_ObjIsTravIdCurrent(pAig, pObj) )
+        return;
+    Aig_ObjSetTravIdCurrent( pAig, pObj );
+    assert( Llb_MnxBddVar(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_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
+    }
+    else
+    {
+        Llb_Nonlin4FindOrder_rec( pAig, pFanin1, vOrder, pCounter );
+        Llb_Nonlin4FindOrder_rec( pAig, pFanin0, vOrder, pCounter );
+    }
+    Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4FindOrder( Aig_Man_t * pAig )
+{
+    Vec_Int_t * vNodes = NULL;
+    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 )
+    {
+printf( "PO %d Var %d\n", i, Counter );
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+        Llb_Nonlin4FindOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+            Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+    Aig_ManCleanMarkA( pAig );
+    Vec_IntFreeP( &vNodes );
+    assert( Counter == Aig_ManObjNum(pAig) - 1 );
+    return vOrder;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives BDDs for the partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4FindPartitions( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+    Vec_Ptr_t * vRoots;
+    Aig_Obj_t * pObj;
+    DdNode * bBdd, * bBdd0, * bBdd1, * bPart;
+    int i;
+    Aig_ManCleanData( pAig );
+    // assign elementary variables
+    Aig_ManConst1(pAig)->pData = Cudd_ReadOne(dd); 
+    Aig_ManForEachPi( pAig, pObj, i )
+        pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( Llb_MnxBddVar(vOrder, pObj) >= 0 )
+        {
+            pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+            Cudd_Ref( (DdNode *)pObj->pData );
+        }
+    Aig_ManForEachPo( pAig, pObj, i )
+        pObj->pData = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObj) );
+    // compute intermediate BDDs
+    vRoots = Vec_PtrAlloc( 100 );
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bBdd1 = Cudd_NotCond( (DdNode *)Aig_ObjFanin1(pObj)->pData, Aig_ObjFaninC1(pObj) );
+        bBdd  = Cudd_bddAnd( dd, bBdd0, bBdd1 );
+        Cudd_Ref( bBdd );
+        if ( pObj->pData == NULL )
+        {
+            pObj->pData = bBdd;
+            continue;
+        }
+        // create new partition
+        bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd );  
+        if ( bPart == NULL )
+            goto finish;
+        Cudd_Ref( bPart );
+        Cudd_RecursiveDeref( dd, bBdd );
+        Vec_PtrPush( vRoots, bPart );
+    }
+    // compute register output BDDs
+    Aig_ManForEachPo( pAig, pObj, i )
+    {
+        bBdd0 = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bPart = Cudd_bddXnor( dd, (DdNode *)pObj->pData, bBdd0 );  
+        if ( bPart == NULL )
+            goto finish;
+        Cudd_Ref( bPart );
+        Vec_PtrPush( vRoots, bPart );
+//printf( "%d ", Cudd_DagSize(bPart) );
+    }
+//printf( "\n" );
+    Aig_ManForEachNode( pAig, pObj, i )
+        Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    return vRoots;
+    // early termination
+finish:
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( pObj->pData )
+            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    Vec_PtrForEachEntry( DdNode *, vRoots, bPart, i )
+        Cudd_RecursiveDeref( dd, bPart );
+    Vec_PtrFree( vRoots );
+    return NULL;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable varaibles for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4FindVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+    Vec_Int_t * vVars2Q;
+    Aig_Obj_t * pObj;
+    int i;
+    vVars2Q = Vec_IntAlloc( 0 );
+    Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
+    Saig_ManForEachLo( pAig, pObj, i )
+        Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+    Aig_ManForEachPo( pAig, pObj, i )
+        Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+    return vVars2Q;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable varaibles for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_Nonlin4CountTerms( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, DdNode * bFunc, int fCo, int fFlop )
+{
+    DdNode * bSupp;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    bSupp = Cudd_Support( dd, bFunc );  Cudd_Ref( bFunc );
+    if ( !fCo && !fFlop )
+    {
+        Saig_ManForEachPi( pAig, pObj, i )
+            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+    }
+    else if ( fCo && !fFlop )
+    {
+        Saig_ManForEachPo( pAig, pObj, i )
+            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+    }
+    else if ( !fCo && fFlop )
+    {
+        Saig_ManForEachLo( pAig, pObj, i )
+            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+    }
+    else if ( fCo && fFlop )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+            Counter += Cudd_bddLeq( dd, bSupp, Cudd_bddIthVar(dd, Llb_MnxBddVar(vOrder, pObj)) );
+    }
+    Cudd_RecursiveDeref( dd, bFunc );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable varaibles for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4PrintGroups( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, Vec_Ptr_t * vGroups )
+{
+    DdNode * bTemp;
+    int i, nSuppAll, nSuppPi, nSuppPo, nSuppLi, nSuppLo, nSuppAnd;
+    Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
+    {
+        nSuppAll = Cudd_SupportSize(dd,bTemp);
+        nSuppPi  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 0);
+        nSuppPo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 0);
+        nSuppLi  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 0, 1);
+        nSuppLo  = Llb_Nonlin4CountTerms(dd, pAig, vOrder, bTemp, 1, 1);
+        nSuppAnd = nSuppAll - (nSuppPi+nSuppPo+nSuppLi+nSuppLo);
+
+        printf( "%4d : bdd =%6d  supp =%3d  ", i, Cudd_DagSize(bTemp), nSuppAll );
+        printf( "pi =%3d ",  nSuppPi );
+        printf( "po =%3d ",  nSuppPo );
+        printf( "lo =%3d ",  nSuppLo );
+        printf( "li =%3d ",  nSuppLi );
+        printf( "and =%3d",  nSuppAnd );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4Cluster( Aig_Man_t * pAig )
+{
+    DdManager * dd;
+    Vec_Int_t * vOrder, * vVars2Q;
+    Vec_Ptr_t * vParts, * vGroups;
+    DdNode * bTemp;
+    int i;
+
+    // create the BDD manager
+    dd      = Cudd_Init( Aig_ManObjNumMax(pAig), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+//    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+    vOrder  = Llb_Nonlin4FindOrder( pAig );
+    vVars2Q = Llb_Nonlin4FindVars2Q( dd, pAig, vOrder );
+    vParts  = Llb_Nonlin4FindPartitions( dd, pAig, vOrder );
+
+    vGroups = Llb_Nonlin4Group( dd, vParts, vVars2Q, 500 );
+
+    Llb_Nonlin4PrintGroups( dd, pAig, vOrder, vGroups );
+
+    Vec_PtrForEachEntry( DdNode *, vGroups, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+
+    Vec_PtrForEachEntry( DdNode *, vParts, bTemp, i )
+        Cudd_RecursiveDeref( dd, bTemp );
+    Extra_StopManager( dd );
+//    Cudd_Quit( dd );
+
+    Vec_IntFree( vOrder );
+    Vec_IntFree( vVars2Q );
+    Vec_PtrFree( vParts );
+    Vec_PtrFree( vGroups );
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+
diff --git a/src/aig/llb/llb4Image.c b/src/aig/llb/llb4Image.c
index b882ac65..45efaead 100644
--- a/src/aig/llb/llb4Image.c
+++ b/src/aig/llb/llb4Image.c
@@ -48,6 +48,7 @@ struct Llb_Mgr_t_
 {
     DdManager *   dd;        // working BDD manager
     Vec_Int_t *   vVars2Q;   // variables to quantify
+    int           nSizeMax;  // maximum size of the cluster
     // internal
     Llb_Prt_t **  pParts;    // partitions
     Llb_Var_t **  pVars;     // variables
@@ -263,7 +264,7 @@ int Llb_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
     int i, RetValue, nSizeNew;
     // create cube to be quantified
     bCube = Llb_Nonlin4CreateCube1( p, pPart );   Cudd_Ref( bCube );
-    assert( !Cudd_IsConstant(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 );
@@ -323,9 +324,13 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
     int i, RetValue, nSuppSize;
     int iPart1 = pPart1->iPart;
     int iPart2 = pPart2->iPart;
+    int liveBeg, liveEnd;
 
     // create cube to be quantified
     bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
+
+printf( "Quantifying  " ); Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
+
 if ( fVerbose )
 {
 printf( "\n" );
@@ -334,7 +339,11 @@ Llb_Nonlin4Print( p );
 printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
 Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
 }
+liveBeg = p->dd->keys - p->dd->dead;
     bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  
+liveEnd = p->dd->keys - p->dd->dead;
+//printf( "%d ", liveEnd-liveBeg );
+
     if ( bFunc == NULL )
     {
         Cudd_RecursiveDeref( p->dd, bCube );
@@ -343,6 +352,8 @@ Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
     Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( p->dd, bCube );
 
+printf( "Createing part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc );  printf( "\n" );
+
     // create new partition
     pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
     pTemp->iPart = p->iPartFree++;
@@ -573,8 +584,15 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
     Llb_Nonlin4CheckVars( p );
     // find variable with minimum score
     Llb_MgrForEachVar( p, pVar, i )
+    {
+        if ( p->nSizeMax && pVar->nScore > p->nSizeMax )
+            continue;
+//        if ( pVarBest == NULL || Vec_IntSize(pVarBest->vParts) * pVarBest->nScore > Vec_IntSize(pVar->vParts) * pVar->nScore )
         if ( pVarBest == NULL || pVarBest->nScore > pVar->nScore )
             pVarBest = pVar;
+//        printf( "%d ", pVar->nScore );
+    }
+//printf( "\n" );
     if ( pVarBest == NULL )
         return 0;
     // find two partitions with minimum size
@@ -592,6 +610,10 @@ int Llb_Nonlin4NextPartitions( Llb_Mgr_t * p, Llb_Prt_t ** ppPart1, Llb_Prt_t **
                 pPart2Best = pPart;
         }
     }
+printf( "Selecting %d and parts %d and %d\n", pVarBest->iVar, pPart1Best->nSize, pPart2Best->nSize );
+Extra_bddPrintSupport( p->dd, pPart1Best->bFunc ); printf( "\n" );
+Extra_bddPrintSupport( p->dd, pPart2Best->bFunc ); printf( "\n" );
+
     *ppPart1 = pPart1Best;
     *ppPart2 = pPart2Best;
     return 1; 
@@ -661,13 +683,14 @@ void Llb_Nonlin4VerifyScores( Llb_Mgr_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
+Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q, int nSizeMax )
 {
     Llb_Mgr_t * p;
     DdNode * bFunc;
     int i;
     p = ABC_CALLOC( Llb_Mgr_t, 1 );
     p->dd        = dd;
+    p->nSizeMax  = nSizeMax;
     p->vVars2Q   = vVars2Q;
     p->nVars     = Cudd_ReadSize(dd);
     p->iPartFree = Vec_PtrSize(vParts);
@@ -678,7 +701,8 @@ Llb_Mgr_t * Llb_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurr
     Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
         Llb_Nonlin4AddPartition( p, i, bFunc );
     // add partition
-    Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
+    if ( bCurrent )
+        Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
     return p;
 }
 
@@ -710,11 +734,11 @@ void Llb_Nonlin4Free( Llb_Mgr_t * p )
 
 /**Function*************************************************************
 
-  Synopsis    [Performs image computation.]
+  Synopsis    []
 
-  Description [Computes image of BDDs (vFuncs).]
+  Description []
                
-  SideEffects [BDDs in vFuncs are derefed inside. The result is refed.]
+  SideEffects []
 
   SeeAlso     []
 
@@ -726,7 +750,7 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
     DdNode * bFunc, * bTemp;
     int i, nReorders;
     // start the manager
-    p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q );
+    p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q, 0 );
     // remove singles
     Llb_MgrForEachPart( p, pPart, i )
         if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
@@ -744,8 +768,8 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
         }
         if ( nReorders < Cudd_ReadReorderings(dd) )
             Llb_Nonlin4RecomputeScores( p );
-        else
-            Llb_Nonlin4VerifyScores( p );
+//        else
+//            Llb_Nonlin4VerifyScores( p );
     }
     // load partitions
     bFunc = Cudd_ReadOne(p->dd);   Cudd_Ref( bFunc );
@@ -756,11 +780,70 @@ DdNode * Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent
     }
 //    nSuppMax = p->nSuppMax;
     Llb_Nonlin4Free( p );
+//printf( "\n" );
     // return
     Cudd_Deref( bFunc );
     return bFunc;
 }
 
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax )
+{
+    Vec_Ptr_t * vGroups;
+    Llb_Prt_t * pPart, * pPart1, * pPart2;
+    Llb_Mgr_t * p;
+    int i, nReorders;
+    // start the manager
+    p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
+    // remove singles
+    Llb_MgrForEachPart( p, pPart, i )
+        if ( Llb_Nonlin4HasSingletonVars(p, pPart) )
+            Llb_Nonlin4Quantify1( p, pPart );
+    // compute scores
+    Llb_Nonlin4RecomputeScores( p );
+    // iteratively quantify variables
+    while ( Llb_Nonlin4NextPartitions(p, &pPart1, &pPart2) )
+    {
+        nReorders = Cudd_ReadReorderings(dd);
+        if ( !Llb_Nonlin4Quantify2( p, pPart1, pPart2 ) )
+        {
+            Llb_Nonlin4Free( p );
+            return NULL;
+        }
+        if ( nReorders < Cudd_ReadReorderings(dd) )
+            Llb_Nonlin4RecomputeScores( p );
+        else
+            Llb_Nonlin4VerifyScores( p );
+    }
+    // load partitions
+    vGroups = Vec_PtrAlloc( 1000 );
+    Llb_MgrForEachPart( p, pPart, i )
+    {
+        if ( Cudd_IsConstant(pPart->bFunc) )
+        {
+            assert( !Cudd_IsComplement(pPart->bFunc) );
+            continue;
+        }
+        Vec_PtrPush( vGroups, pPart->bFunc );
+        Cudd_Ref( pPart->bFunc );
+printf( "Part %d  ", pPart->iPart );
+Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
+    }
+    Llb_Nonlin4Free( p );
+    return vGroups;
+}
+
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/aig/llb/llb4Nonlin.c b/src/aig/llb/llb4Nonlin.c
index 11f5ba3e..d7b3c6c3 100644
--- a/src/aig/llb/llb4Nonlin.c
+++ b/src/aig/llb/llb4Nonlin.c
@@ -255,6 +255,8 @@ void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_In
     assert( Llb_MnxBddVar(vOrder, pObj) < 0 );
     if ( Aig_ObjIsPi(pObj) )
     {
+//        if ( Saig_ObjIsLo(pAig, pObj) )
+//            Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), (*pCounter)++ );
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
         return;
     }
@@ -345,7 +347,11 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
     }
     Aig_ManForEachPi( pAig, pObj, i )
         if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+        {
+//            if ( Saig_ObjIsLo(pAig, pObj) )
+//                Vec_IntWriteEntry( vOrder, Aig_ObjId(Saig_ObjLoToLi(pAig, pObj)), Counter++ );
             Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+        }
     assert( Counter <= Aig_ManPiNum(pAig) + Aig_ManRegNum(pAig) + (vNodes?Vec_IntSize(vNodes):0) );
     Aig_ManCleanMarkA( pAig );
     Vec_IntFreeP( &vNodes );
@@ -701,6 +707,13 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
         Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
         if ( Cudd_IsConstant(p->bCurrent) )
             break;
+/*
+        // reduce BDD size using constrain // Cudd_bddRestrict
+        p->bCurrent = Cudd_bddRestrict( p->dd, bAux = p->bCurrent, Cudd_Not(p->bReached) );   
+        Cudd_Ref( p->bCurrent );
+printf( "Before = %d.  After = %d.\n", Cudd_DagSize(bAux), Cudd_DagSize(p->bCurrent) );
+        Cudd_RecursiveDeref( p->dd, bAux );
+*/
 
         // add to the reached set
         p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );                 
@@ -715,14 +728,15 @@ int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
         Cudd_Ref( p->bReached );
         Cudd_RecursiveDeref( p->dd, bAux );  
 
+
         // report the results
         if ( p->pPars->fVerbose )
         {
             printf( "I =%5d : ",   nIters );
-            printf( "Fr =%7d  ",    nBddSizeFr );
-            printf( "ImNs =%7d  ",  nBddSizeTo );
-            printf( "ImCs =%7d  ",  nBddSizeTo2 );
-            printf( "Rea =%7d   ",  Cudd_DagSize(p->bReached) );
+            printf( "Fr =%7d  ",   nBddSizeFr );
+            printf( "ImNs =%7d  ", nBddSizeTo );
+            printf( "ImCs =%7d  ", nBddSizeTo2 );
+            printf( "Rea =%7d   ", Cudd_DagSize(p->bReached) );
             printf( "(%4d %4d)  ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
             Abc_PrintTime( 1, "T", clock() - clkIter );
         }
diff --git a/src/aig/llb/llbInt.h b/src/aig/llb/llbInt.h
index 357ddb5c..5d145831 100644
--- a/src/aig/llb/llbInt.h
+++ b/src/aig/llb/llbInt.h
@@ -184,6 +184,7 @@ extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager *
 
 /*=== llb4Image.c =======================================================*/
 extern DdNode *        Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
+extern Vec_Ptr_t *     Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vVars2Q, int nSizeMax );
 /*=== llb4Map.c =========================================================*/
 //extern Vec_Int_t *     Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
 /*=== llb4Nonlin.c ======================================================*/
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 99d44937..4af27c5c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8522,21 +8522,24 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_FrameReplaceCurrentNetwork( pAbc, pNtkRes );
     }
 */
+
 /*
     {
-        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
+        extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig );
+//        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
         extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
-        Aig_ManTerSimulate( pAig );
+//        Aig_ManTerSimulate( pAig );
+        Llb_Nonlin4Cluster( pAig );
         Aig_ManStop( pAig );
     }
 */
-/*
+
 {
-    extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
-    Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" );
+//    extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
+//    Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" );
 }
-*/
+
     return 0;
 usage:
     Abc_Print( -2, "usage: test [-CKDN] [-vwh] <file_name>\n" );