Further improvements to reachability.

src/aig/llb/llb4Image.c

@@ -116,6 +116,7 @@ void Llb_Nonlin4RemoveVar( Llb_Mgr_t * p, Llb_Var_t * pVar )
 ***********************************************************************/
 void Llb_Nonlin4RemovePart( Llb_Mgr_t * p, Llb_Prt_t * pPart )
 {
+//printf( "Removing %d\n", pPart->iPart );
     assert( p->pParts[pPart->iPart] == pPart );
     p->pParts[pPart->iPart] = NULL;
     Vec_IntFree( pPart->vVars );
@@ -329,7 +330,7 @@ int Llb_Nonlin4Quantify2( Llb_Mgr_t * p, Llb_Prt_t * pPart1, Llb_Prt_t * pPart2
     // create cube to be quantified
     bCube = Llb_Nonlin4CreateCube2( p, pPart1, pPart2 );   Cudd_Ref( bCube );
 
-printf( "Quantifying  " ); Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
+//printf( "Quantifying  " ); Extra_bddPrintSupport( p->dd, bCube );  printf( "\n" );
 
 if ( fVerbose )
 {
@@ -352,7 +353,9 @@ liveEnd = p->dd->keys - p->dd->dead;
     Cudd_Ref( bFunc );
     Cudd_RecursiveDeref( p->dd, bCube );
 
-printf( "Createing part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc );  printf( "\n" );
+//printf( "Creating part %d ", p->iPartFree ); Extra_bddPrintSupport( p->dd, bFunc );  printf( "\n" );
+
+//printf( "Creating %d\n", p->iPartFree );
 
     // create new partition
     pTemp = p->pParts[p->iPartFree] = ABC_CALLOC( Llb_Prt_t, 1 );
@@ -530,6 +533,7 @@ void Llb_Nonlin4AddPartition( Llb_Mgr_t * p, int i, DdNode * bFunc )
 {
     int k, nSuppSize;
     assert( !Cudd_IsConstant(bFunc) );
+//printf( "Creating init %d\n", i );
     // create partition
     p->pParts[i] = ABC_CALLOC( Llb_Prt_t, 1 );
     p->pParts[i]->iPart = i;
@@ -610,9 +614,9 @@ 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" );
+//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;
@@ -802,7 +806,7 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
     Vec_Ptr_t * vGroups;
     Llb_Prt_t * pPart, * pPart1, * pPart2;
     Llb_Mgr_t * p;
-    int i, nReorders;
+    int i, nReorders, clk = clock();
     // start the manager
     p = Llb_Nonlin4Alloc( dd, vParts, NULL, vVars2Q, nSizeMax );
     // remove singles
@@ -822,24 +826,28 @@ Vec_Ptr_t * Llb_Nonlin4Group( DdManager * dd, Vec_Ptr_t * vParts, Vec_Int_t * vV
         }
         if ( nReorders < Cudd_ReadReorderings(dd) )
             Llb_Nonlin4RecomputeScores( p );
-        else
-            Llb_Nonlin4VerifyScores( p );
+//        else
+//            Llb_Nonlin4VerifyScores( p );
     }
     // load partitions
     vGroups = Vec_PtrAlloc( 1000 );
     Llb_MgrForEachPart( p, pPart, i )
     {
+//printf( "Iteration %d ", pPart->iPart );
         if ( Cudd_IsConstant(pPart->bFunc) )
         {
+//printf( "Constant\n" );
             assert( !Cudd_IsComplement(pPart->bFunc) );
             continue;
         }
+//printf( "\n" );
         Vec_PtrPush( vGroups, pPart->bFunc );
         Cudd_Ref( pPart->bFunc );
-printf( "Part %d  ", pPart->iPart );
-Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
+//printf( "Part %d  ", pPart->iPart );
+//Extra_bddPrintSupport( p->dd, pPart->bFunc ); printf( "\n" );
     }
     Llb_Nonlin4Free( p );
+Abc_PrintTime( 1, "Reparametrization time", clock() - clk );
     return vGroups;
 }
 

src/aig/llb/llb4Nonlin.c

@@ -246,7 +246,7 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSimple( Aig_Man_t * pAig )
   SeeAlso     []
 
 ***********************************************************************/
-void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_Int_t * vOrder, int * pCounter )
+void Llb_Nonlin4CreateOrder_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) )
@@ -266,13 +266,13 @@ void Llb_Nonlin4CreateOrderSmart_rec( Aig_Man_t * pAig, Aig_Obj_t * pObj, Vec_In
 //    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 );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
     }
     else
     {
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin1, vOrder, pCounter );
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, pFanin0, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin1, vOrder, pCounter );
+        Llb_Nonlin4CreateOrder_rec( pAig, pFanin0, vOrder, pCounter );
     }
     if ( pObj->fMarkA )
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), (*pCounter)++ );
@@ -321,7 +321,7 @@ Vec_Int_t * Llb_Nonlin4CollectHighRefNodes( Aig_Man_t * pAig, int nFans )
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
+Vec_Int_t * Llb_Nonlin4CreateOrder( Aig_Man_t * pAig )
 {
     Vec_Int_t * vNodes = NULL;
     Vec_Int_t * vOrder;
@@ -335,7 +335,6 @@ Vec_Int_t * Llb_Nonlin4CreateOrderSmart( Aig_Man_t * pAig )
         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 );
@@ -343,7 +342,7 @@ printf( "Techmapping added %d pivots.\n", Vec_IntSize(vNodes) );
     Saig_ManForEachLi( pAig, pObj, i )
     {
         Vec_IntWriteEntry( vOrder, Aig_ObjId(pObj), Counter++ );
-        Llb_Nonlin4CreateOrderSmart_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
+        Llb_Nonlin4CreateOrder_rec( pAig, Aig_ObjFanin0(pObj), vOrder, &Counter );
     }
     Aig_ManForEachPi( pAig, pObj, i )
         if ( Llb_MnxBddVar(vOrder, pObj) < 0 )
@@ -410,6 +409,8 @@ void Llb_Nonlin4SetupVarMap( DdManager * dd, Aig_Man_t * pAig, Vec_Int_t * vOrde
     pVarsY = ABC_ALLOC( DdNode *, Cudd_ReadSize(dd) );
     Saig_ManForEachLiLo( pAig, pObjLo, pObjLi, i )
     {
+        assert( Llb_MnxBddVar(vOrder, pObjLo) >= 0 );
+        assert( Llb_MnxBddVar(vOrder, pObjLi) >= 0 );
         pVarsX[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLo) );
         pVarsY[i] = Cudd_bddIthVar( dd, Llb_MnxBddVar(vOrder, pObjLi) );
     }
@@ -830,14 +831,25 @@ Llb_Mnx_t * Llb_MnxStart( Aig_Man_t * pAig, Gia_ParLlb_t * pPars )
     p = ABC_CALLOC( Llb_Mnx_t, 1 );
     p->pAig    = pAig;
     p->pPars   = pPars;
+
+    if ( pPars->fCluster )
+    {
+        Llb_Nonlin4Cluster( p->pAig, &p->dd, &p->vOrder, &p->vRoots, pPars->nBddMax, pPars->fVerbose );
+        Cudd_AutodynEnable( p->dd,  CUDD_REORDER_SYMM_SIFT );
+    }
+    else
+    {
 //    p->vOrder  = Llb_Nonlin4CreateOrderSimple( pAig );
-    p->vOrder  = Llb_Nonlin4CreateOrderSmart( pAig );
+        p->vOrder  = Llb_Nonlin4CreateOrder( 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 );
+    }
+
+    Llb_Nonlin4SetupVarMap( p->dd, pAig, p->vOrder );
+    p->vVars2Q = Llb_Nonlin4CreateVars2Q( p->dd, pAig, p->vOrder, 1 );
     p->vRings  = Vec_PtrAlloc( 100 );
+
     if ( pPars->fReorder )
         Llb_Nonlin4Reorder( p->dd, 0, 1 );
     return p;

src/aig/llb/llbInt.h

@@ -182,6 +182,8 @@ extern DdNode *        Llb_NonlinImage( Aig_Man_t * pAig, Vec_Ptr_t * vLeaves, V
 /*=== llb3Nonlin.c ======================================================*/
 extern DdNode *        Llb_NonlinComputeInitState( Aig_Man_t * pAig, DdManager * dd );
 
+/*=== llb4Cluster.c =======================================================*/
+extern void            Llb_Nonlin4Cluster( Aig_Man_t * pAig, DdManager ** pdd, Vec_Int_t ** pvOrder, Vec_Ptr_t ** pvGroups, int nBddMax, int fVerbose );
 /*=== 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 );

src/base/abci/abc.c

@@ -8525,19 +8525,19 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
 
 /*
     {
-        extern void Llb_Nonlin4Cluster( 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 );
-        Llb_Nonlin4Cluster( pAig );
+//        Llb_Nonlin4Cluster( pAig );
         Aig_ManStop( pAig );
     }
 */
 
 {
 //    extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
-//    Ssm_ManExperiment( "m\\big1.ssim", "m\\big1_.ssim" );
+//    Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
 }
 
     return 0;
@@ -27990,9 +27990,11 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // set defaults
     Llb_ManSetDefaultParams( pPars );
+    pPars->fCluster = 0;
     pPars->fReorder = 0;
+    pPars->nBddMax  = 1000;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLryzvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLcryzvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28038,6 +28040,9 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
             pLogFileName = argv[globalUtilOptind];
             globalUtilOptind++;
             break;
+        case 'c':
+            pPars->fCluster ^= 1;
+            break;
         case 'r':
             pPars->fReorder ^= 1;
             break;
@@ -28079,17 +28084,18 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
     pAbc->nFrames = pPars->iFrame;
     Abc_FrameReplaceCex( pAbc, &pMan->pSeqModel );
     if ( pLogFileName )
-        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachn" );
+        Abc_NtkWriteLogFile( pLogFileName, pAbc->pCex, pAbc->Status, pAbc->nFrames, "&reachy" );
     Aig_ManStop( pMan );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-ryzvh]\n" );
+    Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-cryzvh]\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-B num : the BDD node threshold for clustering [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-c     : enable reparametrization clustering [default = %s]\n", pPars->fCluster? "yes": "no" );  
     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" );