Improvements to 'satclp'.

src/base/abci/abc.c

@@ -3130,7 +3130,7 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
     int nCostMax   = 20000000;
     int fCanon     = 0;
     int fReverse   = 0;
-    int fCnfShared = 1;
+    int fCnfShared = 0;
     int fVerbose   = 0;
     int c;
 
@@ -3225,13 +3225,13 @@ int Abc_CommandSatClp( Abc_Frame_t * pAbc, int argc, char ** argv )
 usage:
     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-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-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 (non-canonical only) [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;
 }

src/base/abci/abcCollapse.c

@@ -817,7 +817,7 @@ 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;
         }
-        if ( fCnfShared )
+        if ( fCnfShared && !fCanon )
             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 );

src/sat/bmc/bmcClp.c

@@ -628,7 +628,7 @@ int Bmc_ComputeCanonical( sat_solver * pSat, Vec_Int_t * vLits, Vec_Int_t * vTem
   SeeAlso     []
 
 ***********************************************************************/
-Vec_Str_t * Bmc_CollapseOneInt( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose, int fCompl )
+Vec_Str_t * Bmc_CollapseOneInt2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose, int fCompl )
 {
     int fPrintMinterm = 0;
     int nVars = Gia_ManCiNum(p);
@@ -786,16 +786,16 @@ cleanup:
         Bmc_CollapseIrredundant( vSop, Vec_StrSize(vSop)/(nVars +3), nVars );
     return vSop;
 }
-Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+Vec_Str_t * Bmc_CollapseOneOld2( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     Vec_Str_t * vSopOn, * vSopOff;
     int nCubesOn = ABC_INFINITY;
     int nCubesOff = ABC_INFINITY;
-    vSopOn = Bmc_CollapseOneInt( p, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose, 0 );
+    vSopOn = Bmc_CollapseOneInt2( p, nCubeLim, nBTLimit, fCanon, fReverse, fVerbose, 0 );
     if ( vSopOn )
         nCubesOn = Vec_StrCountEntry(vSopOn,'\n');
     Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
-    vSopOff = Bmc_CollapseOneInt( p, Abc_MinInt(nCubeLim, nCubesOn), nBTLimit, fCanon, fReverse, fVerbose, 1 );
+    vSopOff = Bmc_CollapseOneInt2( p, Abc_MinInt(nCubeLim, nCubesOn), nBTLimit, fCanon, fReverse, fVerbose, 1 );
     Gia_ObjFlipFaninC0( Gia_ManPo(p, 0) );
     if ( vSopOff )
         nCubesOff = Vec_StrCountEntry(vSopOff,'\n');
@@ -827,6 +827,182 @@ Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int f
   SeeAlso     []
 
 ***********************************************************************/
+Vec_Str_t * Bmc_CollapseOneOld( Gia_Man_t * p, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
+{
+    int fVeryVerbose = fVerbose;
+    int nVars = Gia_ManCiNum(p);
+    Cnf_Dat_t * pCnf = Mf_ManGenerateCnf( p, 8, 0, 0, 0 );
+    sat_solver * pSat[2]      = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
+    sat_solver * pSatClean[2] = { (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0), (sat_solver *)Cnf_DataWriteIntoSolver(pCnf, 1, 0) };
+    Vec_Str_t * vSop[2]   = { Vec_StrAlloc(1000),  Vec_StrAlloc(1000)  }, * vRes = NULL;
+    Vec_Int_t * vLitsC[2] = { Vec_IntAlloc(nVars), Vec_IntAlloc(nVars) };
+    Vec_Int_t * vVars = Vec_IntAlloc( nVars );
+    Vec_Int_t * vLits = Vec_IntAlloc( nVars );
+    Vec_Int_t * vNums = Vec_IntAlloc( nVars );
+    Vec_Int_t * vCube = Vec_IntAlloc( nVars );
+    int n, v, iVar, iLit, iCiVarBeg, iCube = 0, Start, status;
+    abctime clk = 0, Time[2][2] = {{0}};
+    int fComplete[2] = {0};
+
+    // collect CI variables
+    iCiVarBeg = pCnf->nVars - nVars;// - 1;
+    if ( fReverse )
+        for ( v = nVars - 1; v >= 0; v-- )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+    else
+        for ( v = 0; v < nVars; v++ )
+            Vec_IntPush( vVars, iCiVarBeg + v );
+
+    // check that on-set/off-set is sat
+    for ( n = 0; n < 2; n++ )
+    {
+        iLit = Abc_Var2Lit( 1, n ); // n=0 => F=1   n=1 => F=0
+        status = sat_solver_solve( pSat[n], &iLit, &iLit + 1, nBTLimit, 0, 0, 0 );
+        if ( status == l_Undef )
+            goto cleanup; // timeout
+        if ( status == l_False )
+        {
+            Vec_StrClear( vSop[0] );
+            Vec_StrPrintStr( vSop[0], n ? " 1\n" : " 0\n" );
+            Vec_StrPush( vSop[0], '\0' );
+            fComplete[0] = 1;
+            goto cleanup; // const0/1
+        }
+        // start with all negative literals
+        Vec_IntForEachEntry( vVars, iVar, v )
+            Vec_IntPush( vLitsC[n], Abc_Var2Lit(iVar, 1) );
+        // add literals to the solver
+        status = sat_solver_addclause( pSat[n], &iLit, &iLit + 1 );
+        assert( status );
+        status = sat_solver_addclause( pSatClean[n], &iLit, &iLit + 1 );
+        assert( status );
+        // start cover
+        Vec_StrPush( vSop[n], '\0' );
+    }
+
+    // compute cube pairs
+    for ( iCube = 0; nCubeLim == 0 || iCube < nCubeLim; iCube++ )
+    {
+        for ( n = 0; n < 2; n++ )
+        {
+            if ( fVeryVerbose ) clk = Abc_Clock();
+            // get the assignment
+            if ( fCanon )
+                status = Bmc_ComputeCanonical( pSat[n], vLitsC[n], vCube, nBTLimit );
+            else
+            {
+                sat_solver_clean_polarity( pSat[n], Vec_IntArray(vVars), Vec_IntSize(vVars) );
+                status = sat_solver_solve( pSat[n], NULL, NULL, 0, 0, 0, 0 );
+            }
+            if ( fVeryVerbose ) Time[n][0] += Abc_Clock() - clk;
+            if ( status == l_Undef )
+                goto cleanup; // timeout
+            if ( status == l_False )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            // collect values
+            Vec_IntClear( vLits );
+            Vec_IntClear( vLitsC[n] );
+            Vec_IntForEachEntry( vVars, iVar, v )
+            {
+                iLit = Abc_Var2Lit(iVar, !sat_solver_var_value(pSat[n], iVar));
+                Vec_IntPush( vLits, iLit );
+                Vec_IntPush( vLitsC[n], iLit );
+            }
+            // expand the values
+            if ( fVeryVerbose ) clk = Abc_Clock();
+            status = Bmc_CollapseExpand( pSatClean[!n], pSat[n], vLits, vNums, vCube, nBTLimit, fCanon, -1 );
+            if ( fVeryVerbose ) Time[n][1] += Abc_Clock() - clk;
+            if ( status < 0 )
+                goto cleanup; // timeout
+            // collect cube
+            Vec_StrPop( vSop[n] );
+            Start = Vec_StrSize( vSop[n] );
+            Vec_StrFillExtra( vSop[n], Start + nVars + 4, '-' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 0, ' ' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 1, (char)(n ? '0' : '1') );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 2, '\n' );
+            Vec_StrWriteEntry( vSop[n], Start + nVars + 3, '\0' );
+            Vec_IntClear( vCube );
+            Vec_IntForEachEntry( vNums, iVar, v )
+            {
+                iLit = Vec_IntEntry( vLits, iVar );
+                Vec_IntPush( vCube, Abc_LitNot(iLit) );
+                if ( fReverse )
+                    Vec_StrWriteEntry( vSop[n], Start + nVars - iVar - 1, (char)('0' + !Abc_LitIsCompl(iLit)) );
+                else 
+                    Vec_StrWriteEntry( vSop[n], Start + iVar, (char)('0' + !Abc_LitIsCompl(iLit)) );
+            }
+            // add cube
+            status = sat_solver_addclause( pSat[n], Vec_IntArray(vCube), Vec_IntLimit(vCube) );
+            if ( status == 0 )
+            {
+                fComplete[n] = 1;
+                break;
+            }
+            assert( status == 1 );
+        }
+        if ( fComplete[0] || fComplete[1] )
+            break;
+    }
+cleanup:
+    Vec_IntFree( vVars );
+    Vec_IntFree( vLits );
+    Vec_IntFree( vLitsC[0] );
+    Vec_IntFree( vLitsC[1] );
+    Vec_IntFree( vNums );
+    Vec_IntFree( vCube );
+    Cnf_DataFree( pCnf );
+    sat_solver_delete( pSat[0] );
+    sat_solver_delete( pSat[1] );
+    sat_solver_delete( pSatClean[0] );
+    sat_solver_delete( pSatClean[1] );
+    assert( !fComplete[0] || !fComplete[1] );
+    if ( fComplete[0] || fComplete[1] ) // one of the cover is computed
+    {
+        vRes = vSop[fComplete[1]]; vSop[fComplete[1]] = NULL;
+        if ( iCube > 1 )
+//            Bmc_CollapseIrredundant( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+            Bmc_CollapseIrredundantFull( vRes, Vec_StrSize(vRes)/(nVars +3), nVars );
+    }
+    if ( fVeryVerbose )
+    {
+        int fProfile = 0;
+        printf( "Processed output with %d supp vars. ", nVars );
+        if ( vRes == NULL )
+            printf( "The resulting SOP exceeded %d cubes.\n", nCubeLim );
+        else 
+            printf( "The best cover contains %d cubes.\n", Vec_StrSize(vRes)/(nVars +3) );
+        Abc_PrintTime( 1, "Onset  minterm", Time[0][0] );
+        Abc_PrintTime( 1, "Onset  expand ", Time[0][1] );
+        Abc_PrintTime( 1, "Offset minterm", Time[1][0] );
+        Abc_PrintTime( 1, "Offset expand ", Time[1][1] );
+        if ( fProfile )
+        {
+            Abc_PrintTime( 1, "Expand check1 ", clkCheck1 ); clkCheck1 = 0;
+            Abc_PrintTime( 1, "Expand check2 ", clkCheck2 ); clkCheck2 = 0;
+            Abc_PrintTime( 1, "Expand sat    ", clkCheckS ); clkCheckS = 0;
+            Abc_PrintTime( 1, "Expand unsat  ", clkCheckU ); clkCheckU = 0;
+        }
+    }
+    Vec_StrFreeP( &vSop[0] );
+    Vec_StrFreeP( &vSop[1] );
+    return vRes;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [This code computes on-set and off-set simultaneously.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 Vec_Str_t * Bmc_CollapseOne_int3( sat_solver * pSat0, sat_solver * pSat1, sat_solver * pSat2, sat_solver * pSat3, int nVars, int nCubeLim, int nBTLimit, int fCanon, int fReverse, int fVerbose )
 {
     int fVeryVerbose = fVerbose;