Improvements to 'satclp'.

4 files changed, 57 insertions, 40 deletions

diff --git a/src/base/abc/abc.h b/src/base/abc/abc.h
index 55624ec2..09d12e0b 100644
--- a/src/base/abc/abc.h
+++ b/src/base/abc/abc.h
@@ -600,7 +600,7 @@ extern ABC_DLL int                Abc_NtkCheckUniqueCoNames( Abc_Ntk_t * pNtk );
 extern ABC_DLL int                Abc_NtkCheckUniqueCioNames( Abc_Ntk_t * pNtk );
 /*=== abcCollapse.c ==========================================================*/
 extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapse( Abc_Ntk_t * pNtk, int fBddSizeMax, int fDualRail, int fReorder, int fVerbose );
-extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose );
+extern ABC_DLL Abc_Ntk_t *        Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose );
 /*=== abcCut.c ==========================================================*/
 extern ABC_DLL void *             Abc_NodeGetCutsRecursive( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
 extern ABC_DLL void *             Abc_NodeGetCuts( void * p, Abc_Obj_t * pObj, int fDag, int fTree );
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 0a72b4b6..03c01bc0 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -3125,17 +3125,18 @@ usage:
 int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc), * pNtkRes;
-    int nCubeLim =        0;
-    int nBTLimit =  1000000;
-    int nCostMax = 20000000;
-    int fCanon   = 0;
-    int fReverse = 0;
-    int fVerbose = 0;
+    int nCubeLim   =        0;
+    int nBTLimit   =  1000000;
+    int nCostMax   = 20000000;
+    int fCanon     = 0;
+    int fReverse   = 0;
+    int fCnfShared = 1;
+    int fVerbose   = 0;
     int c;
 
     // set defaults
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "CLZcrsvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -3178,6 +3179,9 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'r':
             fReverse ^= 1;
             break;
+        case 's':
+            fCnfShared ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -3202,11 +3206,11 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
 
     // get the new network
     if ( Abc_NtkIsStrash(pNtk) )
-        pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+        pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
     else
     {
         pNtk = Abc_NtkStrash( pNtk, 0, 0, 0 );
-        pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+        pNtkRes = Abc_NtkCollapseSat( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
         Abc_NtkDelete( pNtk );
     }
     if ( pNtkRes == NULL )
@@ -3219,13 +3223,14 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: satclp [-CLZ num] [-crvh]\n" );
+    Abc_Print( -2, "usage: satclp [-CLZ num] [-crsvh]\n" );
     Abc_Print( -2, "\t         performs SAT based collapsing\n" );
     Abc_Print( -2, "\t-C num : the limit on the SOP size of one output [default = %d]\n", nCubeLim );
     Abc_Print( -2, "\t-L num : the limit on the number of conflicts in one SAT call [default = %d]\n", nBTLimit );
     Abc_Print( -2, "\t-Z num : the limit on the cost of the largest output [default = %d]\n", nCostMax );
     Abc_Print( -2, "\t-c     : toggles using canonical ISOP computation [default = %s]\n", fCanon? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggles using reverse veriable ordering [default = %s]\n", fReverse? "yes": "no" );
+    Abc_Print( -2, "\t-s     : toggles shared CNF computation [default = %s]\n", fCnfShared? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggles printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
diff --git a/src/base/abci/abcCollapse.c b/src/base/abci/abcCollapse.c
index 653618c5..77ca4f50 100644
--- a/src/base/abci/abcCollapse.c
+++ b/src/base/abci/abcCollapse.c
@@ -598,9 +598,9 @@ Gia_Man_t * Abc_NtkClpGia( Abc_Ntk_t * pNtk )
 ***********************************************************************/
 #define Abc_NtkSopForEachCube( pSop, nVars, pCube )  for ( pCube = (pSop); *pCube; pCube += (nVars) + 3 )
 
-int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
+int Abc_NtkCollapseReduce( Vec_Str_t * vSop, Vec_Int_t * vSupp, Vec_Int_t * vClass, Vec_Wec_t * vSupps )
 {
-    int j = 0, k, iVar, nVars = Vec_IntSize(vSupp);
+    int j = 0, i, k, iCo, iVar, nVars = Vec_IntSize(vSupp);
     char * pCube, * pSop = Vec_StrArray(vSop);
     Vec_Int_t * vPres = Vec_IntStart( nVars );
     Abc_NtkSopForEachCube( pSop, nVars, pCube )
@@ -620,11 +620,15 @@ int Abc_NtkCollapseCountVars( Vec_Str_t * vSop, Vec_Int_t * vSupp )
     Vec_StrWriteEntry( vSop, j++, '\0' );
     Vec_StrShrink( vSop, j );
     // reduce support
-    j = 0;
-    Vec_IntForEachEntry( vSupp, iVar, k )
-        if ( Vec_IntEntry(vPres, k) )
-            Vec_IntWriteEntry( vSupp, j++, iVar );
-    Vec_IntShrink( vSupp, j );
+    Vec_IntForEachEntry( vClass, iCo, i )
+    {
+        j = 0;
+        vSupp = Vec_WecEntry( vSupps, iCo );
+        Vec_IntForEachEntry( vSupp, iVar, k )
+            if ( Vec_IntEntry(vPres, k) )
+                Vec_IntWriteEntry( vSupp, j++, iVar );
+        Vec_IntShrink( vSupp, j );
+    }
     Vec_IntFree( vPres );
 //    if ( Vec_IntSize(vSupp) != Abc_SopGetVarNum(Vec_StrArray(vSop)) )
 //        printf( "Mismatch!!!\n" );
@@ -705,7 +709,7 @@ sat_solver * Abc_NtkClpDeriveSatSolver( Cnf_Dat_t * pCnf, int iCoObjId, Vec_Int_
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose )
+Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps )
 {
     Vec_Str_t * vSop;
     abctime clk = Abc_Clock();
@@ -719,15 +723,15 @@ Vec_Str_t * Abc_NtkClpGiaOne( Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit
         return NULL;
     if ( Vec_StrSize(vSop) == 4 ) // constant
         Vec_IntClear(vSupp);
-//    else
-//        Abc_NtkCollapseCountVars( vSop, vSupp );
+    else
+        Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
     if ( fVerbose )
         printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
     if ( fVerbose )
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return vSop; 
 }
-Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose )
+Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCubeLim, int nBTLimit, int fCanon, int fReverse, Vec_Int_t * vSupp, Vec_Int_t * vMap, int fVerbose, Vec_Int_t * vClass, Vec_Wec_t * vSupps )
 {
     Vec_Str_t * vSop;
     sat_solver * pSat, * pSat1 = NULL, * pSat2 = NULL, * pSat3 = NULL;
@@ -761,15 +765,15 @@ Vec_Str_t * Abc_NtkClpGiaOne2( Cnf_Dat_t * pCnf, Gia_Man_t * p, int iCo, int nCu
         return NULL;
     if ( Vec_StrSize(vSop) == 4 ) // constant
         Vec_IntClear(vSupp);
-//    else
-//        Abc_NtkCollapseCountVars( vSop, vSupp );
+    else
+        Abc_NtkCollapseReduce( vSop, vSupp, vClass, vSupps );
     if ( fVerbose )
         printf( "Supp new = %4d. Sop = %4d.  ", Vec_IntSize(vSupp), Vec_StrSize(vSop)/(Vec_IntSize(vSupp) +3) );
     if ( fVerbose )
         Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
     return vSop; 
 }
-Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * vSupps, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
 {
     ProgressBar * pProgress;
     abctime clk = Abc_Clock();
@@ -777,8 +781,8 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
     Vec_Int_t * vReprs, * vClass, * vReprSuppSizes;
     int i, k, Entry, iCo, * pOrder;
     Vec_Wec_t * vClasses;
-    Cnf_Dat_t * pCnf;
-    Vec_Int_t * vMap;
+    Cnf_Dat_t * pCnf = NULL;
+    Vec_Int_t * vMap = NULL;
     // derive classes of outputs
     vClasses = Gia_ManIsoStrashReduceInt( p, vSupps, 0 );
     if ( fVerbose )
@@ -794,8 +798,11 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
     pOrder = Abc_MergeSortCost( Vec_IntArray(vReprSuppSizes), Vec_IntSize(vReprSuppSizes) );
     Vec_IntFree( vReprSuppSizes );
     // consider SOPs for representatives
-    vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
-    pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 );
+    if ( fCnfShared )
+    {
+        vMap = Vec_IntStartFull( Gia_ManObjNum(p) );
+        pCnf = Mf_ManGenerateCnf( p, 8, 1, 0, 0 );
+    }
     vSopsRepr = Vec_PtrStart( Vec_IntSize(vReprs) );
     pProgress = Extra_ProgressBarStart( stdout, Vec_IntSize(vReprs) );
     Extra_ProgressBarUpdate( pProgress, 0, NULL );
@@ -810,8 +817,10 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
             Vec_PtrWriteEntry( vSopsRepr, iEntry, (void *)(ABC_PTRINT_T)1 );
             continue;
         }
-      vSop  = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose );
-//      vSop  = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose );
+        if ( fCnfShared )
+            vSop = Abc_NtkClpGiaOne2( pCnf, p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, vMap, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
+        else
+            vSop = Abc_NtkClpGiaOne( p, iCoThis, nCubeLim, nBTLimit, fCanon, fReverse, vSupp, i ? 0 : fVerbose, Vec_WecEntry(vClasses, iEntry), vSupps );
         if ( vSop == NULL )
             goto finish;
         assert( Vec_IntSize( Vec_WecEntry(vSupps, iCoThis) ) == Abc_SopGetVarNum(Vec_StrArray(vSop)) );
@@ -820,8 +829,11 @@ Vec_Ptr_t * Abc_GiaDeriveSops( Abc_Ntk_t * pNtkNew, Gia_Man_t * p, Vec_Wec_t * v
         Vec_StrFree( vSop );
     }
     Extra_ProgressBarStop( pProgress );
-    Cnf_DataFree( pCnf );
-    Vec_IntFree( vMap );
+    if ( fCnfShared )
+    {
+        Cnf_DataFree( pCnf );
+        Vec_IntFree( vMap );
+    }
     // derive SOPs for each output
     vSops = Vec_PtrStart( Gia_ManCoNum(p) );
     Vec_WecForEachLevel ( vClasses, vClass, i )
@@ -845,7 +857,7 @@ finish:
     Vec_PtrFree( vSopsRepr );
     return vSops;
 }
-Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
     Gia_Man_t * pGia;
@@ -874,7 +886,7 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
         }
     }
     pNtkNew = Abc_NtkStartFrom( pNtk, ABC_NTK_LOGIC, ABC_FUNC_SOP );
-    vSops   = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+    vSops   = Abc_GiaDeriveSops( pNtkNew, pGia, vSupps, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
     Gia_ManStop( pGia );
     if ( vSops == NULL )
     {
@@ -917,11 +929,11 @@ Abc_Ntk_t * Abc_NtkFromSopsInt( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, in
     Vec_PtrFree( vSops );
     return pNtkNew;
 }
-Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fVerbose )
+Abc_Ntk_t * Abc_NtkCollapseSat( Abc_Ntk_t * pNtk, int nCubeLim, int nBTLimit, int nCostMax, int fCanon, int fReverse, int fCnfShared, int fVerbose )
 {
     Abc_Ntk_t * pNtkNew;
     assert( Abc_NtkIsStrash(pNtk) );
-    pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fVerbose );
+    pNtkNew = Abc_NtkFromSopsInt( pNtk, nCubeLim, nBTLimit, nCostMax, fCanon, fReverse, fCnfShared, fVerbose );
     if ( pNtkNew == NULL )
         return NULL;
     if ( pNtk->pExdc )
diff --git a/src/sat/bmc/bmcClp.c b/src/sat/bmc/bmcClp.c
index fbff7679..f7d43e60 100644
--- a/src/sat/bmc/bmcClp.c
+++ b/src/sat/bmc/bmcClp.c
@@ -1103,6 +1103,7 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV
             Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
             Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
             Vec_IntClear( vCube );
+            Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
             Vec_IntForEachEntry( vNums, iVar, v )
             {
                 int iLit = Vec_IntEntry( vLits, iVar );
@@ -1113,7 +1114,6 @@ Vec_Str_t * Bmc_CollapseOne_int2( sat_solver * pSat1, sat_solver * pSat2, int nV
                     Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
             }
             // add cube
-            Vec_IntPush( vCube, Abc_Var2Lit( iOOVars[n], 0 ) );
 //            status = sat_solver_addclause( pSat, Vec_IntArray(vCube), Vec_IntLimit(vCube) );
             status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
             if ( status == 0 )
@@ -1230,8 +1230,8 @@ Vec_Str_t * Bmc_CollapseOne_int( sat_solver * pSat, int nVars, int nCubeLim, int
             if ( fVeryVerbose ) clk = Abc_Clock();
             // get the assignment
             sat_solver_clean_polarity( pSat, Vec_IntArray(vVars), Vec_IntSize(vVars) );
-            pLits[0] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
-            pLits[1] = Abc_Var2Lit( iOutVar, n );    // set output
+            pLits[0] = Abc_Var2Lit( iOutVar, n );    // set output
+            pLits[1] = Abc_Var2Lit( iOOVars[n], 1 ); // enable clauses
             status = sat_solver_solve( pSat, pLits, pLits + 2, 0, 0, 0, 0 );
             if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
             if ( status == l_Undef )