Enabled new BDD-based reachability engine 'reachy'.

abclib.dsp

@@ -4163,6 +4163,18 @@ SOURCE=.\src\aig\llb\llb3Nonlin.c
 # End Source File
 # Begin Source File
 
+SOURCE=.\src\aig\llb\llb4Image.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\llb\llb4Map.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\llb\llb4Nonlin.c
+# End Source File
+# Begin Source File
+
 SOURCE=.\src\aig\llb\llbInt.h
 # End Source File
 # End Group
@@ -4305,6 +4317,54 @@ SOURCE=.\src\aig\au\auUtil.c
 # Begin Group "ssm"
 
 # PROP Default_Filter ""
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssm.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssm.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmApi.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmClock.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmInt.h
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmRandom.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmRead.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmReset.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmSchedule.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmSimple.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmSimulate.c
+# End Source File
+# Begin Source File
+
+SOURCE=.\src\aig\ssm\ssmWrite.c
+# End Source File
 # End Group
 # End Group
 # End Group

src/aig/aig/aigDoms.c

@@ -207,9 +207,9 @@ void Aig_ManDomPrint( Aig_Sto_t * pSto )
 {
     Aig_Obj_t * pObj;
     int i;
-    Saig_ManForEachLo( pSto->pAig, pObj, i )
+    Saig_ManForEachPi( pSto->pAig, pObj, i )
     {
-        printf( "*** LO %4d %4d :\n", i, pObj->Id );
+        printf( "*** PI %4d %4d :\n", i, pObj->Id );
         Aig_ObjDomVecPrint( pSto, (Vec_Ptr_t *)Vec_PtrEntry(pSto->vDoms, pObj->Id) );
     }
 }
@@ -647,6 +647,45 @@ Aig_Sto_t * Aig_ManComputeDomsFlops( Aig_Man_t * pAig, int Limit )
     return pSto;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes multi-node dominators.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Sto_t * Aig_ManComputeDomsPis( Aig_Man_t * pAig, int Limit )
+{
+    Aig_Sto_t * pSto;
+    Vec_Ptr_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i, clk = clock();
+    pSto = Aig_ManDomStart( pAig, Limit );
+    // initialize flop inputs
+    Aig_ManForEachPo( pAig, pObj, i )
+        Aig_ObjAddTriv( pSto, pObj->Id, Vec_PtrAlloc(1) );
+    // compute internal nodes
+    vNodes = Aig_ManDfsReverse( pAig );
+    Aig_ManMarkFlopTfi( pAig );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        if ( Aig_ObjIsTravIdCurrent(pSto->pAig, pObj) )
+            Aig_ObjDomCompute( pSto, pObj );
+    Vec_PtrFree( vNodes );
+    // compute combinational inputs
+    Saig_ManForEachPi( pAig, pObj, i )
+        Aig_ObjDomCompute( pSto, pObj );
+    // print statistics
+    printf( "Nodes =%4d. PIs =%4d. Doms =%9d. Ave =%8.2f.   ", 
+        pSto->nDomNodes, Saig_ManPiNum(pSto->pAig), pSto->nDomsTotal, 
+//        pSto->nDomsFilter1, pSto->nDomsFilter2,
+        1.0 * pSto->nDomsTotal / (pSto->nDomNodes + Saig_ManPiNum(pSto->pAig)) );
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    return pSto;
+}
 
 /**Function*************************************************************
 
@@ -971,7 +1010,7 @@ void Aig_ObjDomFindGood( Aig_Sto_t * pSto )
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManComputeDomsTest( Aig_Man_t * pAig, int Num )
+void Aig_ManComputeDomsTest2( Aig_Man_t * pAig, int Num )
 {
     Aig_Sto_t * pSto;
 //    int i;
@@ -988,6 +1027,27 @@ void Aig_ManComputeDomsTest( Aig_Man_t * pAig, int Num )
     Aig_ManFanoutStop( pAig );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes multi-node dominators.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManComputeDomsTest( Aig_Man_t * pAig )
+{
+    Aig_Sto_t * pSto;
+    Aig_ManFanoutStart( pAig );
+    pSto = Aig_ManComputeDomsPis( pAig, 1 );
+    Aig_ManDomPrint( pSto );
+    Aig_ManDomStop( pSto );
+    Aig_ManFanoutStop( pAig );
+}
+
 
 
 

src/aig/aig/aigPack.c

@@ -113,10 +113,10 @@ void Aig_ManPackPrintCare( Aig_ManPack_t * p )
     Aig_ManForEachPi( p->pAig, pObj, i )
     {
         Sign = Vec_WrdEntry( p->vPiCare, i );
-        Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 );
-        printf( "\n" );
+//        Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 );
+//        printf( "\n" );
     }
-    printf( "\n" );
+//    printf( "\n" );
 }
 
 

src/aig/gia/gia.h

@@ -316,6 +316,10 @@ static inline void         Gia_ObjSetValue( Gia_Obj_t * pObj, int i )          {
 static inline int          Gia_ObjPhase( Gia_Obj_t * pObj )                    { return pObj->fPhase;                                        }
 static inline int          Gia_ObjPhaseReal( Gia_Obj_t * pObj )                { return Gia_Regular(pObj)->fPhase ^ Gia_IsComplement(pObj);  }
 
+static inline int          Gia_ManIdToCioId( Gia_Man_t * p, int Id )           { return Gia_ObjCioId( Gia_ManObj(p, Id) );                   }
+static inline int          Gia_ManCiIdToId( Gia_Man_t * p, int CiId )          { return Gia_ObjId( p, Gia_ManCi(p, CiId) );                  }
+static inline int          Gia_ManCoIdToId( Gia_Man_t * p, int CoId )          { return Gia_ObjId( p, Gia_ManCo(p, CoId) );                  }
+
 static inline int          Gia_ObjIsPi( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) < Gia_ManPiNum(p);   } 
 static inline int          Gia_ObjIsPo( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ObjIsCo(pObj) && Gia_ObjCioId(pObj) < Gia_ManPoNum(p);   } 
 static inline int          Gia_ObjIsRo( Gia_Man_t * p, Gia_Obj_t * pObj )      { return Gia_ObjIsCi(pObj) && Gia_ObjCioId(pObj) >= Gia_ManPiNum(p);  } 

src/aig/llb/llb4Image.c

+/**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_
+{
+    DdManager *   dd;        // working BDD manager
+    Vec_Int_t *   vVars2Q;   // 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_Nonlin4RemoveVar( 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_Nonlin4RemovePart( 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_Nonlin4CreateCube1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
+{
+    DdNode * bCube, * bTemp;
+    Llb_Var_t * pVar;
+    int i, TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
+    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 );
+    p->dd->TimeStop = TimeStop;
+    return bCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Create cube of variables appearing only in two partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_Nonlin4CreateCube2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
+{
+    DdNode * bCube, * bTemp;
+    Llb_Var_t * pVar;
+    int i, TimeStop;
+    TimeStop = p->dd->TimeStop; p->dd->TimeStop = 0;
+    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 );
+    p->dd->TimeStop = TimeStop;
+    return bCube;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Returns 1 if partition has singleton variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_Nonlin4HasSingletonVars( 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_Nonlin4Print( 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_Nonlin4Quantify1( Llb_Mgr_t * p, Llb_Prt_t * pPart )
+{
+    Llb_Var_t * pVar;
+    Llb_Prt_t * pTemp;
+    Vec_Ptr_t * vSingles;
+    DdNode * bCube, * bTemp;
+    int i, RetValue, nSizeNew;
+    // create cube to be quantified
+    bCube = Llb_Nonlin4CreateCube1( 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_Nonlin4RemoveVar( 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] && Vec_IntEntry(p->vVars2Q, i) )
+            Vec_IntPush( pPart->vVars, i );
+    // remove other variables
+    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
+        Llb_Nonlin4Quantify1( p, pTemp );
+    Vec_PtrFree( vSingles );
+    return 0;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Quantifies singles belonging to one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2 )
+{
+    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_Nonlin4CreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
+if ( fVerbose )
+{
+printf( "\n" );
+printf( "\n" );
+Llb_Nonlin4Print( p );
+printf( "Conjoining partitions %d and %d.\n", pPart1->iPart, pPart2->iPart );
+Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
+}
+    bFunc = Cudd_bddAndAbstract( p->dd, pPart1->bFunc, pPart2->bFunc, bCube );  
+    if ( bFunc == NULL )
+    {
+        Cudd_RecursiveDeref( p->dd, bCube );
+        return 0;
+    }
+    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] && Vec_IntEntry(p->vVars2Q, 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_Nonlin4RemoveVar( 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_Nonlin4RemoveVar( 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_Nonlin4RemovePart( p, pPart1 );
+    Llb_Nonlin4RemovePart( p, pPart2 );
+    // remove other variables
+if ( fVerbose )
+Llb_Nonlin4Print( p );
+    Vec_PtrForEachEntry( Llb_Prt_t *, vSingles, pTemp, i )
+    {
+if ( fVerbose )
+printf( "Updating partitiong %d with singlton vars.\n", pTemp->iPart );
+        Llb_Nonlin4Quantify1( p, pTemp );
+    }
+if ( fVerbose )
+Llb_Nonlin4Print( p );
+    Vec_PtrFree( vSingles );
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes volume of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4CutNodes_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_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
+        return;
+    }
+    if ( Aig_ObjIsConst1(pObj) )
+        return;
+    assert( Aig_ObjIsNode(pObj) );
+    Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin0(pObj), vNodes);
+    Llb_Nonlin4CutNodes_rec(p, Aig_ObjFanin1(pObj), vNodes);
+    Vec_PtrPush( vNodes, pObj );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Computes volume of the cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4CutNodes( 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_Nonlin4CutNodes_rec( p, pObj, vNodes );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Starts non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4AddPair( Llb_Mgr_t * p, 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_Nonlin4AddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
+{
+    int k, nSuppSize;
+    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;  Cudd_Ref( 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] && Vec_IntEntry(p->vVars2Q, k) )
+            Llb_Nonlin4AddPair( p, i, k );
+    }
+    p->nSuppMax = ABC_MAX( p->nSuppMax, nSuppSize ); 
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Checks that each var appears in at least one partition.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+**********************************************************************/
+void Llb_Nonlin4CheckVars( 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_Nonlin4NextPartitions( 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_Nonlin4CheckVars( 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    [Recomputes scores after variable reordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4RecomputeScores( 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_Nonlin4VerifyScores( 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_Nonlin4Alloc( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
+{
+    Llb_Mgr_t * p;
+    DdNode * bFunc;
+    int i;
+    p = ABC_CALLOC( Llb_Mgr_t, 1 );
+    p->dd        = dd;
+    p->vVars2Q   = vVars2Q;
+    p->nVars     = Cudd_ReadSize(dd);
+    p->iPartFree = Vec_PtrSize(vParts);
+    p->pVars     = ABC_CALLOC( Llb_Var_t *, p->nVars );
+    p->pParts    = ABC_CALLOC( Llb_Prt_t *, 2 * p->iPartFree + 2 );
+    p->pSupp     = ABC_ALLOC( int, Cudd_ReadSize(dd) );
+    // add pairs (refs are consumed inside)
+    Vec_PtrForEachEntry( DdNode *, vParts, bFunc, i )
+        Llb_Nonlin4AddPartition( p, i, bFunc );
+    // add partition
+    Llb_Nonlin4AddPartition( p, p->iPartFree++, bCurrent );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Stops non-linear quantification scheduling.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4Free( Llb_Mgr_t * p )
+{
+    Llb_Prt_t * pPart;
+    Llb_Var_t * pVar;
+    int i;
+    Llb_MgrForEachVar( p, pVar, i )
+        Llb_Nonlin4RemoveVar( p, pVar );
+    Llb_MgrForEachPart( p, pPart, i )
+        Llb_Nonlin4RemovePart( 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_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q )
+{
+    Llb_Prt_t * pPart, * pPart1, * pPart2;
+    Llb_Mgr_t * p;
+    DdNode * bFunc, * bTemp;
+    int i, nReorders;
+    // start the manager
+    p = Llb_Nonlin4Alloc( dd, vParts, bCurrent, vVars2Q );
+    // 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
+    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_Nonlin4Free( p );
+    // return
+    Cudd_Deref( bFunc );
+    return bFunc;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/llb/llb4Map.c

+/**CFile****************************************************************
+
+  FileName    [llb2Map.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: llb2Map.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+#include "abc.h"
+#include "if.h"
+
+ABC_NAMESPACE_IMPL_START
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+
+/**Function*************************************************************
+
+  Synopsis    [Returns internal nodes used in the mapping.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin )
+{
+    extern Abc_Ntk_t * Abc_NtkFromAigPhase( Aig_Man_t * pMan );
+    extern If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+    extern void        Gia_ManSetIfParsDefault( If_Par_t * pPars );
+    If_Par_t Pars, * pPars = &Pars;
+    If_Man_t * pIfMan;
+    If_Obj_t * pAnd;
+    Abc_Ntk_t * pNtk;
+    Abc_Obj_t * pNode;
+    Vec_Int_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+
+    // create ABC network
+    pNtk = Abc_NtkFromAigPhase( pAig );
+    assert( Abc_NtkIsStrash(pNtk) );
+
+    // derive mapping parameters
+    Gia_ManSetIfParsDefault( pPars );
+    pPars->nLutSize = nLutSize;
+
+    // get timing information
+    pPars->pTimesArr = Abc_NtkGetCiArrivalFloats(pNtk);
+    pPars->pTimesReq = NULL;
+
+    // perform LUT mapping
+    pIfMan = Abc_NtkToIf( pNtk, pPars );    
+    if ( pIfMan == NULL )
+    {
+        Abc_NtkDelete( pNtk );
+        return NULL;
+    }
+    if ( !If_ManPerformMapping( pIfMan ) )
+    {
+        Abc_NtkDelete( pNtk );
+        If_ManStop( pIfMan );
+        return NULL;
+    }
+
+    // mark nodes in the AIG used in the mapping
+    Aig_ManCleanMarkA( pAig );
+    Aig_ManForEachNode( pAig, pObj, i )
+    {
+        pNode = (Abc_Obj_t *)pObj->pData;
+        if ( pNode == NULL )
+            continue;
+        pAnd = (If_Obj_t *)pNode->pCopy;
+        if ( pAnd == NULL )
+            continue;
+        if ( pAnd->nRefs > 0 && (int)If_ObjCutBest(pAnd)->nLeaves >= nLutMin )
+            pObj->fMarkA = 1;
+    }
+    Abc_NtkDelete( pNtk );
+    If_ManStop( pIfMan );
+
+    // unmark flop drivers
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjFanin0(pObj)->fMarkA = 0;
+
+    // collect mapping
+    vNodes = Vec_IntAlloc( 100 );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( pObj->fMarkA )
+            Vec_IntPush( vNodes, Aig_ObjId(pObj) );
+    Aig_ManCleanMarkA( pAig );
+    return vNodes;
+}
+
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/llb/llb4Nonlin.c

+/**CFile****************************************************************
+
+  FileName    [llb2Nonlin.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: llb2Nonlin.c,v 1.00 2005/06/20 00:00:00 alanmi Exp $]
+
+***********************************************************************/
+
+#include "llbInt.h"
+
+ABC_NAMESPACE_IMPL_START
+ 
+
+////////////////////////////////////////////////////////////////////////
+///                        DECLARATIONS                              ///
+////////////////////////////////////////////////////////////////////////
+
+typedef struct Llb_Mnx_t_ Llb_Mnx_t;
+struct Llb_Mnx_t_
+{
+    // user info
+    Aig_Man_t *     pAig;           // AIG manager
+    Gia_ParLlb_t *  pPars;          // parameters
+
+    // intermediate BDDs
+    DdManager *     dd;             // BDD manager
+    DdNode *        bBad;           // bad states in terms of CIs
+    DdNode *        bReached;       // reached states 
+    DdNode *        bCurrent;       // from states
+    DdNode *        bNext;          // to states
+    Vec_Ptr_t *     vRings;         // onion rings in ddR
+    Vec_Ptr_t *     vRoots;         // BDDs for partitions
+
+    // structural info
+    Vec_Int_t *     vOrder;         // for each object ID, its BDD variable number or -1
+    Vec_Int_t *     vVars2Q;        // 1 if variable is quantifiable; 0 othervise
+
+    int             timeImage;
+    int             timeRemap;
+    int             timeReo;
+    int             timeOther;
+    int             timeTotal;
+};
+
+static inline int Llb_MnxBddVar( Vec_Int_t * vOrder, Aig_Obj_t * pObj ) { return Vec_IntEntry(vOrder, Aig_ObjId(pObj)); }
+
+//extern int timeBuild, timeAndEx, timeOther;
+//extern int nSuppMax;
+
+////////////////////////////////////////////////////////////////////////
+///                     FUNCTION DEFINITIONS                         ///
+////////////////////////////////////////////////////////////////////////
+ 
+/**Function*************************************************************
+
+  Synopsis    [Computes bad in working manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_Nonlin4ComputeBad( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+    Vec_Ptr_t * vNodes;
+    DdNode * bBdd, * bBdd0, * bBdd1, * bTemp, * bResult;
+    Aig_Obj_t * pObj;
+    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) );
+    // compute internal nodes
+    vNodes = Aig_ManDfsNodes( pAig, (Aig_Obj_t **)Vec_PtrArray(pAig->vPos), Saig_ManPoNum(pAig) );
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+    {
+        if ( !Aig_ObjIsNode(pObj) )
+            continue;
+        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 );
+        if ( bBdd == NULL )
+        {
+            Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+                if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
+                    Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+            Vec_PtrFree( vNodes );
+            return NULL;
+        }
+        Cudd_Ref( bBdd );
+        pObj->pData = bBdd;
+    }
+    // quantify PIs of each PO
+    bResult = Cudd_ReadLogicZero( dd );  Cudd_Ref( bResult );
+    Saig_ManForEachPo( pAig, pObj, i )
+    {
+        bBdd0   = Cudd_NotCond( (DdNode *)Aig_ObjFanin0(pObj)->pData, Aig_ObjFaninC0(pObj) );
+        bResult = Cudd_bddOr( dd, bTemp = bResult, bBdd0 );     
+        if ( bResult == NULL )
+        {
+            Cudd_RecursiveDeref( dd, bTemp );
+            break;
+        }
+        Cudd_Ref( bResult );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    // deref
+    Vec_PtrForEachEntry( Aig_Obj_t *, vNodes, pObj, i )
+        if ( Aig_ObjIsNode(pObj) && pObj->pData != NULL )
+            Cudd_RecursiveDeref( dd, (DdNode *)pObj->pData );
+    Vec_PtrFree( vNodes );
+    if ( bResult )
+        Cudd_Deref( bResult );
+//if ( bResult )
+//printf( "Bad state = %d.\n", Cudd_DagSize(bResult) );
+    return bResult;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Derives BDDs for the partitions.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Ptr_t * Llb_Nonlin4DerivePartitions( 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 );
+        }
+    Saig_ManForEachLi( 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 );
+        if ( bBdd == NULL )
+            goto finish;
+        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 );
+//printf( "%d ", Cudd_DagSize(bPart) );
+    }
+    // compute register output BDDs
+    Saig_ManForEachLi( 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    [Find simple variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
+{
+    Vec_Int_t * vOrder;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
+    Aig_ManForEachPi( pAig, pObj, i )
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+    Saig_ManForEachLi( pAig, pObj, i )
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+    return vOrder;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4CreateOrderSmart_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_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
+    }
+    else
+    {
+        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
+        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
+    }
+    if ( pObj->fMarkA )
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Collect nodes with the given fanout count.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
+{
+    Vec_Int_t * vNodes;
+    Aig_Obj_t * pObj;
+    int i;
+    Aig_ManCleanMarkA( pAig );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( Aig_ObjRefs(pObj) >= nFans )
+            pObj->fMarkA = 1;
+    // unmark flop drivers
+    Saig_ManForEachLi( pAig, pObj, i )
+        Aig_ObjFanin0(pObj)->fMarkA = 0;
+    // collect mapping
+    vNodes = Vec_IntAlloc( 100 );
+    Aig_ManForEachNode( pAig, pObj, i )
+        if ( pObj->fMarkA )
+            Vec_IntPush( vNodes, Aig_ObjId(pObj) );
+    Aig_ManCleanMarkA( pAig );
+    return vNodes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Find good static variable ordering.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
+{
+    Vec_Int_t * vNodes = NULL;
+    Vec_Int_t * vOrder;
+    Aig_Obj_t * pObj;
+    int i, Counter = 0;
+/*
+    // mark internal nodes to be used
+    Aig_ManCleanMarkA( pAig );
+    vNodes = Llb_Nonlin4CollectHighRefNodes( pAig, 4 );
+    Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
+        pObj->fMarkA = 1;
+printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
+*/
+
+    // collect nodes in the order
+    vOrder = Vec_IntStartFull( Aig_ManObjNumMax(pAig) );
+    Aig_ManIncrementTravId( pAig );
+    Aig_ObjSetTravIdCurrent( pAig, Aig_ManConst1(pAig) );
+    Saig_ManForEachLi( pAig, pObj, i )
+    {
+        Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
+        Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
+    }
+    Aig_ManForEachPi( pAig, pObj, i )
+        if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
+            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 );
+    return vOrder;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Creates quantifiable varaibles for both types of traversal.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Llb_Nonlin4CreateVars2Q( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, int fForward )
+{
+    Vec_Int_t * vVars2Q;
+    Aig_Obj_t * pObj;
+    int i;
+    vVars2Q = Vec_IntAlloc( 0 );
+    Vec_IntFill( vVars2Q, Cudd_ReadSize(dd), 1 );
+    if ( fForward )
+    {
+        Saig_ManForEachLi( pAig, pObj, i )
+            Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+    }
+    else
+    {
+        Aig_ManForEachPi( pAig, pObj, i )
+            Vec_IntWriteEntry( vVars2Q, Llb_MnxBddVar(vOrder, pObj), 0 );
+    }
+    return vVars2Q;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute initial state in terms of current state variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+    DdNode ** pVarsX, ** pVarsY;
+    Aig_Obj_t * pObjLo, * pObjLi;
+    int i;
+    pVarsX = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
+    pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
+    Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
+    {
+        pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) );
+        pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
+    }
+    Cudd_SetVarMap( dd, pVarsX, pVarsY, Aig_ManRegNum(pAig) );
+    ABC_FREE( pVarsX );
+    ABC_FREE( pVarsY );
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute initial state in terms of current state variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_Nonlin4ComputeInitState( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder )
+{
+    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_ManForEachLo( pAig, pObj, i )
+    {
+        bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(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 bRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Compute initial state in terms of current state variables.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+DdNode * Llb_Nonlin4ComputeCube( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrder, char * pValues )
+{
+    Aig_Obj_t * pObj, * pObjLi;
+    DdNode * bRes, * bVar, * bTemp;
+    int i, TimeStop;
+    TimeStop = dd->TimeStop;  dd->TimeStop = 0;
+    bRes = Cudd_ReadOne( dd );   Cudd_Ref( bRes );
+    Saig_ManForEachLo( pAig, pObj, i )
+    {
+        if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 2 )
+            continue;
+        // get the correspoding flop input variable
+        pObjLi = Saig_ObjLoToLi(pAig, pObj);
+        bVar = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
+        if ( pValues[Llb_MnxBddVar(vOrder, pObj)] == 0 )
+            bVar = Cudd_Not(bVar);
+        // create cube
+        bRes = Cudd_bddAnd( dd, bTemp = bRes, bVar );  Cudd_Ref( bRes );
+        Cudd_RecursiveDeref( dd, bTemp );
+    }
+    Cudd_Deref( bRes );
+    dd->TimeStop = TimeStop;
+    return bRes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Derives counter-example by backward reachability.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Abc_Cex_t * Llb_Nonlin4DeriveCex( Llb_Mnx_t * p )
+{
+    Abc_Cex_t * pCex;
+    Aig_Obj_t * pObj;
+    DdNode * bState, * bImage, * bOneCube, * bRing;
+    int i, v, RetValue, nPiOffset;
+    char * pValues = ABC_ALLOC( char, Cudd_ReadSize(p->dd) );
+    assert( Vec_PtrSize(p->vRings) > 0 );
+    // disable the timeout
+    p->dd->TimeStop  = 0;
+
+    // update quantifiable vars
+    Vec_IntFreeP( &p->vVars2Q );
+    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, p->pAig, p->vOrder, 0 );
+
+    // allocate room for the counter-example
+    pCex = Abc_CexAlloc( Saig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Vec_PtrSize(p->vRings) );
+    pCex->iFrame = Vec_PtrSize(p->vRings) - 1;
+    pCex->iPo = -1;
+
+    // get the last cube
+    bOneCube = Cudd_bddIntersect( p->dd, (DdNode *)Vec_PtrEntryLast(p->vRings), p->bBad );  Cudd_Ref( bOneCube );
+    RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
+    Cudd_RecursiveDeref( p->dd, bOneCube );
+    assert( RetValue );
+
+    // write PIs of counter-example
+    nPiOffset = Saig_ManRegNum(p->pAig) + Saig_ManPiNum(p->pAig) * (Vec_PtrSize(p->vRings) - 1);
+    Saig_ManForEachPi( p->pAig, pObj, i )
+        if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
+            Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+
+    // write state in terms of NS variables
+    if ( Vec_PtrSize(p->vRings) > 1 )
+    {
+        bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues );   Cudd_Ref( bState );
+    }
+    // perform backward analysis
+    Vec_PtrForEachEntryReverse( DdNode *, p->vRings, bRing, v )
+    { 
+        if ( v == Vec_PtrSize(p->vRings) - 1 )
+            continue;
+        // compute the next states
+        bImage = Llb_Nonlin4Image( p->dd, p->vRoots, bState, p->vVars2Q );
+        assert( bImage != NULL );
+        Cudd_Ref( bImage );
+        Cudd_RecursiveDeref( p->dd, bState );
+
+        // intersect with the previous set
+        bOneCube = Cudd_bddIntersect( p->dd, bImage, bRing );                Cudd_Ref( bOneCube );
+        Cudd_RecursiveDeref( p->dd, bImage );
+
+        // find any assignment of the BDD
+        RetValue = Cudd_bddPickOneCube( p->dd, bOneCube, pValues );
+        Cudd_RecursiveDeref( p->dd, bOneCube );
+        assert( RetValue );
+
+        // write PIs of counter-example
+        nPiOffset -= Saig_ManPiNum(p->pAig);
+        Saig_ManForEachPi( p->pAig, pObj, i )
+            if ( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 1 )
+                Aig_InfoSetBit( pCex->pData, nPiOffset + i );
+
+        // check that we get the init state
+        if ( v == 0 )
+        {
+            Saig_ManForEachLo( p->pAig, pObj, i )
+                assert( pValues[Llb_MnxBddVar(p->vOrder, pObj)] == 0 );
+            break;
+        }
+
+        // write state in terms of NS variables
+        bState = Llb_Nonlin4ComputeCube( p->dd, p->pAig, p->vOrder, pValues );   Cudd_Ref( bState );
+    }
+    assert( nPiOffset == Saig_ManRegNum(p->pAig) );
+    // update the output number
+//Abc_CexPrint( pCex );
+    RetValue = Saig_ManFindFailedPoCex( p->pAig, pCex );
+    assert( RetValue >= 0 && RetValue < Saig_ManPoNum(p->pAig) ); // invalid CEX!!!
+    pCex->iPo = RetValue;
+    // cleanup
+    ABC_FREE( pValues );
+    return pCex;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Perform reachability with hints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_Nonlin4Reachability( Llb_Mnx_t * p )
+{ 
+    DdNode * bAux;
+    int nIters, nBddSizeFr, nBddSizeTo, nBddSizeTo2;
+    int clkTemp, clkIter, clk = clock();
+    assert( Aig_ManRegNum(p->pAig) > 0 );
+
+    // compute time to stop
+    if ( p->pPars->TimeLimit )
+        p->pPars->TimeTarget = clock() + p->pPars->TimeLimit * CLOCKS_PER_SEC;
+    else
+        p->pPars->TimeTarget = 0;
+    // set the stop time parameter
+    p->dd->TimeStop  = p->pPars->TimeTarget;
+
+    // create bad state in the ring manager
+    if ( !p->pPars->fSkipOutCheck )
+    {
+        p->bBad = Llb_Nonlin4ComputeBad( p->dd, p->pAig, p->vOrder );          
+        if ( p->bBad == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during constructing the bad states.\n", p->pPars->TimeLimit );
+            p->pPars->iFrame = -1;
+            return -1;
+        }
+        Cudd_Ref( p->bBad );
+    }
+
+    // compute the starting set of states
+    p->bCurrent = Llb_Nonlin4ComputeInitState( p->dd, p->pAig, p->vOrder );  Cudd_Ref( p->bCurrent );
+    p->bReached = p->bCurrent;                                               Cudd_Ref( p->bCurrent );
+    for ( nIters = 0; nIters < p->pPars->nIterMax; nIters++ )
+    { 
+        clkIter = clock();
+        // check the runtime limit
+        if ( p->pPars->TimeLimit && clock() >= p->pPars->TimeTarget )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
+
+        // save the onion ring
+        Vec_PtrPush( p->vRings, p->bCurrent );   Cudd_Ref( p->bCurrent );
+
+        // check it for bad states
+        if ( !p->pPars->fSkipOutCheck && !Cudd_bddLeq( p->dd, p->bCurrent, Cudd_Not(p->bBad) ) ) 
+        {
+            assert( p->pAig->pSeqModel == NULL );
+            if ( !p->pPars->fBackward )
+                p->pAig->pSeqModel = Llb_Nonlin4DeriveCex( p ); 
+            if ( !p->pPars->fSilent )
+            {
+                if ( !p->pPars->fBackward )
+                    printf( "Output %d was asserted in frame %d (use \"write_counter\" to dump a witness).  ", p->pAig->pSeqModel->iPo, nIters );
+                else
+                    printf( "Output ??? was asserted in frame %d (counter-example is not produced).  ", nIters );
+                Abc_PrintTime( 1, "Time", clock() - clk );
+            }
+            p->pPars->iFrame = nIters - 1;
+            return 0;
+        }
+
+        // compute the next states
+        clkTemp = clock();
+        p->bNext = Llb_Nonlin4Image( p->dd, p->vRoots, p->bCurrent, p->vVars2Q );
+        if ( p->bNext == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in quantification.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
+        Cudd_Ref( p->bNext );
+        p->timeImage += clock() - clkTemp;
+
+        // remap into current states
+        clkTemp = clock();
+        p->bNext = Cudd_bddVarMap( p->dd, bAux = p->bNext );
+        if ( p->bNext == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during remapping next states.\n",  p->pPars->TimeLimit );
+            Cudd_RecursiveDeref( p->dd, bAux );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
+        Cudd_Ref( p->bNext );
+        Cudd_RecursiveDeref( p->dd, bAux );
+        p->timeRemap += clock() - clkTemp;
+
+        // collect statistics
+        if ( p->pPars->fVerbose )
+        {
+            nBddSizeFr  = Cudd_DagSize( p->bCurrent );
+            nBddSizeTo  = Cudd_DagSize( bAux );
+            nBddSizeTo2 = Cudd_DagSize( p->bNext );
+        }
+        Cudd_RecursiveDeref( p->dd, p->bCurrent ); p->bCurrent = NULL;
+
+        // derive new states
+        p->bCurrent = Cudd_bddAnd( p->dd, p->bNext, Cudd_Not(p->bReached) );     
+        if ( p->bCurrent == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            return -1;
+        }
+        Cudd_Ref( p->bCurrent );
+        Cudd_RecursiveDeref( p->dd, p->bNext ); p->bNext = NULL;
+        if ( Cudd_IsConstant(p->bCurrent) )
+            break;
+
+        // add to the reached set
+        p->bReached = Cudd_bddOr( p->dd, bAux = p->bReached, p->bCurrent );                 
+        if ( p->bReached == NULL )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached timeout (%d seconds) during image computation in transfer 1.\n",  p->pPars->TimeLimit );
+            p->pPars->iFrame = nIters - 1;
+            Cudd_RecursiveDeref( p->dd, bAux );  
+            return -1;
+        }
+        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( "(%4d %4d)  ", Cudd_ReadReorderings(p->dd), Cudd_ReadGarbageCollections(p->dd) );
+            Abc_PrintTime( 1, "T", clock() - clkIter );
+        }
+/*
+        if ( pPars->fVerbose )
+        {
+            double nMints = Cudd_CountMinterm(p->dd, bReached, Saig_ManRegNum(p->pAig) );
+//            Extra_bddPrint( p->dd, bReached );printf( "\n" );
+            printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
+            fflush( stdout ); 
+        }
+*/
+        if ( nIters == p->pPars->nIterMax - 1 )
+        {
+            if ( !p->pPars->fSilent )
+                printf( "Reached limit on the number of timeframes (%d).\n",  p->pPars->nIterMax );
+            p->pPars->iFrame = nIters;
+            return -1;
+        }
+    }
+    
+    // report the stats
+    if ( p->pPars->fVerbose )
+    {
+        double nMints = Cudd_CountMinterm(p->dd, p->bReached, Saig_ManRegNum(p->pAig) );
+        if ( p->bCurrent && Cudd_IsConstant(p->bCurrent) )
+            printf( "Reachability analysis completed after %d frames.\n", nIters );
+        else
+            printf( "Reachability analysis is stopped after %d frames.\n", nIters );
+        printf( "Reachable states = %.0f. (Ratio = %.4f %%)\n", nMints, 100.0*nMints/pow(2.0, Saig_ManRegNum(p->pAig)) );
+        fflush( stdout ); 
+    }
+    if ( p->bCurrent == NULL || !Cudd_IsConstant(p->bCurrent) )
+    {
+        if ( !p->pPars->fSilent )
+            printf( "Verified only for states reachable in %d frames.  ", nIters );
+        p->pPars->iFrame = p->pPars->nIterMax;
+        return -1; // undecided
+    }
+    // report
+    if ( !p->pPars->fSilent )
+        printf( "The miter is proved unreachable after %d iterations.  ", nIters );
+    p->pPars->iFrame = nIters - 1;
+    Abc_PrintTime( 1, "Time", clock() - clk );
+    return 1; // unreachable
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Reorders BDDs in the working manager.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_Nonlin4Reorder( DdManager * dd, int fTwice, 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) );
+    if ( fTwice )
+    {
+        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    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
+{
+    Llb_Mnx_t * p;
+    p = ABC_CALLOC( Llb_Mnx_t, 1 );
+    p->pAig    = pAig;
+    p->pPars   = pPars;
+//    p->vOrder  = Llb_Nonlin4CreateOrderSimple( pAig );
+    p->vOrder  = Llb_Nonlin4CreateOrderSmart( pAig );
+    p->dd      = Cudd_Init( Vec_IntSize(p->vOrder), 0, CUDD_UNIQUE_SLOTS, CUDD_CACHE_SLOTS, 0 );
+    Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
+    Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 );
+    p->vRoots  = Llb_Nonlin4DerivePartitions( p->dd, pAig, p->vOrder );
+    p->vRings  = Vec_PtrAlloc( 100 );
+    if ( pPars->fReorder )
+        Llb_Nonlin4Reorder( p->dd, 0, 1 );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Llb_MnxStop( Llb_Mnx_t * p )
+{
+    DdNode * bTemp;
+    int i;
+    if ( p->pPars->fVerbose ) 
+    {
+        p->timeReo = Cudd_ReadReorderingTime(p->dd);
+        p->timeOther = p->timeTotal - p->timeImage - p->timeRemap;
+        ABC_PRTP( "Image    ", p->timeImage, p->timeTotal );
+        ABC_PRTP( "Remap    ", p->timeRemap, p->timeTotal );
+        ABC_PRTP( "Other    ", p->timeOther, p->timeTotal );
+        ABC_PRTP( "TOTAL    ", p->timeTotal, p->timeTotal );
+        ABC_PRTP( "  reo    ", p->timeReo,   p->timeTotal );
+    }
+    // remove BDDs
+    if ( p->bBad )
+        Cudd_RecursiveDeref( p->dd, p->bBad );
+    if ( p->bReached )
+        Cudd_RecursiveDeref( p->dd, p->bReached );
+    if ( p->bCurrent )
+        Cudd_RecursiveDeref( p->dd, p->bCurrent );
+    if ( p->bNext )
+        Cudd_RecursiveDeref( p->dd, p->bNext );
+    Vec_PtrForEachEntry( DdNode *, p->vRings, bTemp, i )
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    Vec_PtrForEachEntry( DdNode *, p->vRoots, bTemp, i )
+        Cudd_RecursiveDeref( p->dd, bTemp );
+    // remove arrays
+    Vec_PtrFree( p->vRings );
+    Vec_PtrFree( p->vRoots );
+    Extra_StopManager( p->dd );
+    Vec_IntFreeP( &p->vOrder );
+    Vec_IntFreeP( &p->vVars2Q );
+    ABC_FREE( p );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Finds balanced cut.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
+{
+    Llb_Mnx_t * pMnn;
+    int RetValue = -1;
+    if ( pPars->fVerbose )
+    Aig_ManPrintStats( pAig );
+    if ( !pPars->fSkipReach )
+    {
+        int clk = clock();
+        pMnn = Llb_MnxStart( pAig, pPars );
+        RetValue = Llb_Nonlin4Reachability( pMnn );
+        pMnn->timeTotal = clock() - clk;
+        Llb_MnxStop( pMnn );
+    }
+    return RetValue;
+}
+
+////////////////////////////////////////////////////////////////////////
+///                       END OF FILE                                ///
+////////////////////////////////////////////////////////////////////////
+
+
+ABC_NAMESPACE_IMPL_END
+

src/aig/llb/llbInt.h

@@ -176,12 +176,20 @@ extern DdManager *     Llb_NonlinImageStart( Aig_Man_t * pAig, Vec_Ptr_t * vLeav
 extern DdNode *        Llb_NonlinImageCompute( DdNode * bCurrent, int fReorder, int fDrop, int fVerbose, int * pOrder );
 extern void            Llb_NonlinImageQuit();
 
-/*=== llb3Image.c ======================================================*/
+/*=== llb3Image.c =======================================================*/
 extern 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, int TimeTarget );
 /*=== llb3Nonlin.c ======================================================*/
 extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
 
+/*=== llb4Image.c =======================================================*/
+extern DdNode *        Llb_Nonlin4Image( DdManager * dd, Vec_Ptr_t * vParts, DdNode * bCurrent, Vec_Int_t * vVars2Q );
+/*=== llb4Map.c =========================================================*/
+//extern Vec_Int_t *     Llb_AigMap( Aig_Man_t * pAig, int nLutSize, int nLutMin );
+/*=== llb4Nonlin.c ======================================================*/
+extern int             Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
+
+
 ABC_NAMESPACE_HEADER_END
 
 

src/aig/llb/module.make

@@ -16,4 +16,6 @@ SRC +=    src/aig/llb/llb.c \
     src/aig/llb/llb2Flow.c \
     src/aig/llb/llb2Image.c \
     src/aig/llb/llb3Image.c \
-    src/aig/llb/llb3Nonlin.c
+    src/aig/llb/llb3Nonlin.c \
+    src/aig/llb/llb4Image.c \
+    src/aig/llb/llb4Nonlin.c

src/base/abci/abc.c

@@ -373,6 +373,7 @@ static int Abc_CommandAbc9Posplit            ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9ReachM             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReachP             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReachN             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9ReachY             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Undo               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Test               ( Abc_Frame_t * pAbc, int argc, char ** argv );
 
@@ -784,6 +785,7 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachm",       Abc_CommandAbc9ReachM,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachp",       Abc_CommandAbc9ReachP,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&reachn",       Abc_CommandAbc9ReachN,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&reachy",       Abc_CommandAbc9ReachY,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&undo",         Abc_CommandAbc9Undo,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&test",         Abc_CommandAbc9Test,         0 );
 
@@ -8529,6 +8531,12 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
         Aig_ManStop( pAig );
     }
 */
+/*
+{
+    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" );
@@ -27968,6 +27976,137 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
+int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    Gia_ParLlb_t Pars, * pPars = &Pars;
+    Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
+    Aig_Man_t * pMan;
+    char * pLogFileName = NULL;
+    int c;
+    extern int Llb_Nonlin4CoreReach( Aig_Man_t * pAig, Gia_ParLlb_t * pPars );
+
+    // set defaults
+    Llb_ManSetDefaultParams( pPars );
+    pPars->fReorder = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nBddMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nBddMax < 0 ) 
+                goto usage;
+            break;
+        case 'F':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-F\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nIterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nIterMax < 0 ) 
+                goto usage;
+            break;
+        case 'T':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-T\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->TimeLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->TimeLimit < 0 ) 
+                goto usage;
+            break;
+        case 'L':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-L\" should be followed by a file name.\n" );
+                goto usage;
+            }
+            pLogFileName = argv[globalUtilOptind];
+            globalUtilOptind++;
+            break;
+        case 'r':
+            pPars->fReorder ^= 1;
+            break;
+        case 'y':
+            pPars->fSkipOutCheck ^= 1;
+            break;
+        case 'z':
+            pPars->fSkipReach ^= 1;
+            break;
+        case 'v':
+            pPars->fVerbose ^= 1;
+            break;
+        case 'w':
+            pPars->fVeryVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) == 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): The current AIG has no latches.\n" );
+        return 0;
+    }
+    if ( Gia_ManObjNum(pAbc->pGia) >= (1<<16) )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9ReachN(): Currently cannot handle AIGs with more than %d objects.\n", (1<<16) );
+        return 0;
+    }
+    pMan          = Gia_ManToAigSimple( pAbc->pGia );
+    pAbc->Status  = Llb_Nonlin4CoreReach( pMan, pPars );
+    pAbc->nFrames = pPars->iFrame;
+    Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
+    if ( pLogFileName )
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
+    Aig_ManStop( pMan );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-ryzvh]\n" );
+    Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
+    Abc_Print( -2, "\t-B num : the BDD node increase when hints kick in [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
+    Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
+    Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );
+    Abc_Print( -2, "\t-r     : enable additional BDD var reordering before image [default = %s]\n", pPars->fReorder? "yes": "no" );  
+    Abc_Print( -2, "\t-y     : skip checking property outputs [default = %s]\n", pPars->fSkipOutCheck? "yes": "no" );  
+    Abc_Print( -2, "\t-z     : skip reachability (run preparation phase only) [default = %s]\n", pPars->fSkipReach? "yes": "no" );  
+    Abc_Print( -2, "\t-v     : prints verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" );  
+//    Abc_Print( -2, "\t-w     : prints additional information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" );  
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 int Abc_CommandAbc9Undo( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     int c;

src/base/abci/abcIf.c

@@ -30,7 +30,7 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
-static If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
+extern If_Man_t *  Abc_NtkToIf( Abc_Ntk_t * pNtk, If_Par_t * pPars );
 static Abc_Ntk_t * Abc_NtkFromIf( If_Man_t * pIfMan, Abc_Ntk_t * pNtk );
 extern Abc_Obj_t * Abc_NodeFromIf_rec( Abc_Ntk_t * pNtkNew, If_Man_t * pIfMan, If_Obj_t * pIfObj, Vec_Int_t * vCover );
 static Hop_Obj_t * Abc_NodeIfToHop( Hop_Man_t * pHopMan, If_Man_t * pIfMan, If_Obj_t * pIfObj );

src/bdd/cudd/cuddCompose.c

@@ -1251,6 +1251,9 @@ cuddBddVarMapRecur(
         return(Cudd_NotCond(res,F != f));
     }
 
+    if ( manager->TimeStop && manager->TimeStop < clock() )
+        return NULL;
+
     /* Split and recur on children of this node. */
     T = cuddBddVarMapRecur(manager,cuddT(F));
     if (T == NULL) return(NULL);

src/misc/vec/vecVec.h

@@ -64,6 +64,8 @@ struct Vec_Vec_t_
     for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
 #define Vec_VecForEachLevelReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop )          \
     for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Ptr_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
+#define Vec_VecForEachLevelTwo( vGlob1, vGlob2, vVec1, vVec2, i )                                                 \
+    for ( i = 0; (i < Vec_VecSize(vGlob1)) && (((vVec1) = (Vec_Ptr_t*)Vec_VecEntry(vGlob1, i)), 1) && (((vVec2) = (Vec_Ptr_t*)Vec_VecEntry(vGlob2, i)), 1); i++ )
 
 // iterators through levels 
 #define Vec_VecForEachLevelInt( vGlob, vVec, i )                                              \
@@ -78,6 +80,8 @@ struct Vec_Vec_t_
     for ( i = Vec_VecSize(vGlob)-1; (i >= 0) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
 #define Vec_VecForEachLevelIntReverseStartStop( vGlob, vVec, i, LevelStart, LevelStop )       \
     for ( i = LevelStart-1; (i >= LevelStop) && (((vVec) = (Vec_Int_t*)Vec_VecEntry(vGlob, i)), 1); i-- )
+#define Vec_VecForEachLevelIntTwo( vGlob1, vGlob2, vVec1, vVec2, i )                          \
+    for ( i = 0; (i < Vec_VecSize(vGlob1)) && (((vVec1) = (Vec_Int_t*)Vec_VecEntry(vGlob1, i)), 1) && (((vVec2) = (Vec_Int_t*)Vec_VecEntry(vGlob2, i)), 1); i++ )
 
 // iteratores through entries
 #define Vec_VecForEachEntry( Type, vGlob, pEntry, i, k )                                      \