Integrating SAT-based CEX minimization.

4 files changed, 145 insertions, 10 deletions

diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c
index 88e8c717..edd5c87d 100644
--- a/src/aig/gia/giaCex.c
+++ b/src/aig/gia/giaCex.c
@@ -422,8 +422,8 @@ Gia_Man_t * Gia_ManFramesForCexMin( Gia_Man_t * p, int nFrames )
     Gia_ManForEachCo( p, pObj, i )
         Gia_ManAppendCo( pFrames, Gia_ObjFanin0Copy(pObj) );
     pFrames = Gia_ManCleanup( pTemp = pFrames );
-    printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", 
-        Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
+    //printf( "Before cleanup = %d nodes. After cleanup = %d nodes.\n", 
+    //    Gia_ManAndNum(pTemp), Gia_ManAndNum(pFrames) );
     Gia_ManStop( pTemp );
     return pFrames;
 }
@@ -499,6 +499,110 @@ void Gia_ManMinCex( Gia_Man_t * p, Abc_Cex_t * pCex )
     Gia_ManStop( pFrames );
 }
 
+
+Abc_Cex_t * Bmc_CexCareDeriveCex( Abc_Cex_t * pCex, int iFirstVar, int * pLits, int nLits )
+{
+    Abc_Cex_t * pCexMin; int i;
+    pCexMin = Abc_CexAlloc( pCex->nRegs, pCex->nPis, pCex->iFrame + 1 );
+    pCexMin->iPo    = pCex->iPo;
+    pCexMin->iFrame = pCex->iFrame;
+    for ( i = 0; i < nLits; i++ )
+    {
+        int PiNum = Abc_Lit2Var(pLits[i]) - iFirstVar;
+        assert( PiNum >= 0 && PiNum < pCex->nBits - pCex->nRegs );
+        Abc_InfoSetBit( pCexMin->pData, pCexMin->nRegs + PiNum );
+    }
+    return pCexMin;
+}
+Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose )
+{
+    abctime clk = Abc_Clock();
+    int n, i, iFirstVar, iLit, status;
+    Vec_Int_t * vLits;
+    sat_solver * pSat;
+    Cnf_Dat_t * pCnf;
+    int nFinal, * pFinal;
+    Abc_Cex_t * pCexBest = NULL; 
+    int CountBest = 0;
+    Gia_Man_t * pFrames;
+
+    // CEX minimization
+    clk = Abc_Clock();
+    pCexBest = Bmc_CexCareMinimizeAig( p, Gia_ManPiNum(p), pCex, 1, 1, fVerbose );
+    for ( i = pCexBest->nRegs; i < pCexBest->nBits; i++ )
+        CountBest += Abc_InfoHasBit(pCexBest->pData, i);
+    if ( fVerbose )
+    {
+        printf( "Care bits = %d. ", CountBest );
+        Abc_PrintTime( 1, "Non-SAT-based CEX minimization", Abc_Clock() - clk );
+    }
+
+    // SAT instance
+    clk = Abc_Clock();
+    pFrames = Gia_ManFramesForCexMin( p, pCex->iFrame + 1 );
+    pCnf = (Cnf_Dat_t*)Mf_ManGenerateCnf( pFrames, 8, 0, 0, 0, 0 );
+    iFirstVar = pCnf->nVars - (pCex->iFrame+1) * pCex->nPis;
+    pSat = (sat_solver*)Cnf_DataWriteIntoSolver( pCnf, 1, 0 );
+    iLit = Abc_Var2Lit( 1, 1 );
+    status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
+    assert( status );
+    // create literals
+    vLits = Vec_IntAlloc( 100 );
+    for ( i = pCex->nRegs; i < pCex->nBits; i++ )
+        Vec_IntPush( vLits, Abc_Var2Lit(iFirstVar + i - pCex->nRegs, !Abc_InfoHasBit(pCex->pData, i)) );
+    if ( fVerbose )
+    Abc_PrintTime( 1, "Constructing SAT solver", Abc_Clock() - clk );
+
+    for ( n = 0; n < 2; n++ )
+    {
+        if ( n ) Vec_IntReverseOrder( vLits );
+
+        // SAT-based minimization
+        clk = Abc_Clock();
+        status = sat_solver_solve( pSat, Vec_IntArray(vLits), Vec_IntLimit(vLits), 0, 0, 0, 0 );
+        nFinal = sat_solver_final( pSat, &pFinal );
+        if ( fVerbose )
+        {
+            printf( "Status %s   Selected %5d assumptions out of %5d.  ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
+            Abc_PrintTime( 1, "Analyze_final", Abc_Clock() - clk );
+        }
+        if ( CountBest > nFinal )
+        {
+            CountBest = nFinal;
+            ABC_FREE( pCexBest );
+            pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, pFinal, nFinal );
+        }
+        if ( !fHighEffort )
+            continue;
+
+        // SAT-based minimization
+        clk = Abc_Clock();
+        nFinal = sat_solver_minimize_assumptions( pSat, Vec_IntArray(vLits), Vec_IntSize(vLits), 0 );
+        if ( fVerbose )
+        {
+            printf( "Status %s   Selected %5d assumptions out of %5d.  ", status == l_False ? "OK ":"BUG", nFinal, Vec_IntSize(vLits) );
+            Abc_PrintTime( 1, "LEXUNSAT     ", Abc_Clock() - clk );
+        }
+        if ( CountBest > nFinal )
+        {
+            CountBest = nFinal;
+            ABC_FREE( pCexBest );
+            pCexBest = Bmc_CexCareDeriveCex( pCex, iFirstVar, Vec_IntArray(vLits), nFinal );
+        }
+    }
+    if ( fVerbose )
+    {
+        printf( "Final    :    " );
+        Bmc_CexPrint( pCexBest, pCexBest->nPis, 0 );
+    }
+    // cleanup
+    Vec_IntFree( vLits );
+    sat_solver_delete( pSat );
+    Cnf_DataFree( pCnf );
+    Gia_ManStop( pFrames );
+    return pCexBest;
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/io/io.c b/src/base/io/io.c
index b047bf92..11b1fa57 100644
--- a/src/base/io/io.c
+++ b/src/base/io/io.c
@@ -2310,6 +2310,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
     char * pFileName;
     int c, fNames  = 0;
     int fMinimize  = 0;
+    int fUseSatBased = 0;
+    int fHighEffort = 0;
     int fUseOldMin = 0;
     int fCheckCex  = 0;
     int forceSeq   = 0;
@@ -2318,7 +2320,7 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
     int fVerbose   = 0;
 
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "snmocafvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "snmueocafvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -2331,6 +2333,12 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
             case 'm':
                 fMinimize ^= 1;
                 break;
+            case 'u':
+                fUseSatBased ^= 1;
+                break;
+            case 'e':
+                fHighEffort ^= 1;
+                break;
             case 'o':
                 fUseOldMin ^= 1;
                 break;
@@ -2419,6 +2427,8 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
                     if ( fCheckCex )
                         Bmc_CexCareVerify( pAig, pCex, pCare, fVerbose );
                 }
+                else if ( fUseSatBased )
+                    pCare = Bmc_CexCareSatBasedMinimize( pAig, Saig_ManPiNum(pAig), pCex, fHighEffort, fCheckCex, fVerbose );
                 else
                     pCare = Bmc_CexCareMinimize( pAig, Saig_ManPiNum(pAig), pCex, 4, fCheckCex, fVerbose );
                 Aig_ManStop( pAig );
@@ -2477,19 +2487,21 @@ int IoCommandWriteCex( Abc_Frame_t * pAbc, int argc, char **argv )
     return 0;
 
 usage:
-    fprintf( pAbc->Err, "usage: write_cex [-snmocfvh] <file>\n" );
-    fprintf( pAbc->Err, "\t         saves counter-example derived by \"sat\", \"iprove\", or \"dprove\"\n" );
-    fprintf( pAbc->Err, "\t         the file contains values for each PI in the natural order\n" );
-    fprintf( pAbc->Err, "\t-s     : always report a sequential ctrex (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
+    fprintf( pAbc->Err, "usage: write_cex [-snmueocfvh] <file>\n" );
+    fprintf( pAbc->Err, "\t         saves counter-example (CEX) derived by \"sat\", \"iprove\", \"dprove\", etc\n" );
+    fprintf( pAbc->Err, "\t         the output file <file> contains values for each PI in natural order\n" );
+    fprintf( pAbc->Err, "\t-s     : always report a sequential CEX (cycle 0 for comb) [default = %s]\n", forceSeq? "yes": "no" );
     fprintf( pAbc->Err, "\t-n     : write input names into the file [default = %s]\n", fNames? "yes": "no" );
     fprintf( pAbc->Err, "\t-m     : minimize counter-example by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
-    fprintf( pAbc->Err, "\t-o     : use old counter-example minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
-    fprintf( pAbc->Err, "\t-c     : check generated counter-example using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
+    fprintf( pAbc->Err, "\t-u     : use SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
+    fprintf( pAbc->Err, "\t-e     : use high-effort SAT-based CEX minimization [default = %s]\n", fHighEffort? "yes": "no" );
+    fprintf( pAbc->Err, "\t-o     : use old CEX minimization algorithm [default = %s]\n", fUseOldMin? "yes": "no" );
+    fprintf( pAbc->Err, "\t-c     : check generated CEX using ternary simulation [default = %s]\n", fCheckCex? "yes": "no" );
     fprintf( pAbc->Err, "\t-a     : print cex in AIGER 1.9 format [default = %s].\n", fAiger? "yes": "no" );
     fprintf( pAbc->Err, "\t-f     : enable printing flop values in each timeframe [default = %s].\n", fPrintFull? "yes": "no" );  
     fprintf( pAbc->Err, "\t-v     : enable verbose output [default = %s].\n", fVerbose? "yes": "no" );  
     fprintf( pAbc->Err, "\t-h     : print the help massage\n" );
-    fprintf( pAbc->Err, "\tfile   : the name of the file to write\n" );
+    fprintf( pAbc->Err, "\t<file> : the name of the file to write\n" );
     return 1;
 }
 
diff --git a/src/sat/bmc/bmc.h b/src/sat/bmc/bmc.h
index 1d5180f3..71a33595 100644
--- a/src/sat/bmc/bmc.h
+++ b/src/sat/bmc/bmc.h
@@ -217,6 +217,8 @@ extern Abc_Cex_t *       Bmc_CexCareExtendToObjects( Gia_Man_t * p, Abc_Cex_t *
 extern Abc_Cex_t *       Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
 extern Abc_Cex_t *       Bmc_CexCareMinimizeAig( Gia_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int nTryCexes, int fCheck, int fVerbose );
 extern void              Bmc_CexCareVerify( Aig_Man_t * p, Abc_Cex_t * pCex, Abc_Cex_t * pCexMin, int fVerbose );
+extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose );
+extern Abc_Cex_t *       Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int fHighEffort, int fVerbose );
 /*=== bmcCexCut.c ==========================================================*/
 extern Gia_Man_t *       Bmc_GiaTargetStates( Gia_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
 extern Aig_Man_t *       Bmc_AigTargetStates( Aig_Man_t * p, Abc_Cex_t * pCex, int iFrBeg, int iFrEnd, int fCombOnly, int fGenAll, int fAllFrames, int fVerbose );
diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c
index cc3e85ea..8db92444 100644
--- a/src/sat/bmc/bmcCexCare.c
+++ b/src/sat/bmc/bmcCexCare.c
@@ -430,6 +430,23 @@ Abc_Cex_t * Bmc_CexCareMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex,
     Gia_ManStop( pGia );
     return pCexMin;
 }
+Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t * pCex, int fHighEffort, int fCheck, int fVerbose )
+{
+    Gia_Man_t * pGia = Gia_ManFromAigSimple( p );
+    Abc_Cex_t * pCexMin = Bmc_CexCareSatBasedMinimizeAig( pGia, pCex, fHighEffort, fVerbose );
+    if ( pCexMin == NULL )
+    {
+        Gia_ManStop( pGia );
+        return NULL;
+    }
+    // verify and return
+    if ( !Bmc_CexVerify( pGia, pCex, pCexMin ) )
+        printf( "Counter-example verification has failed.\n" );
+    else if ( fCheck ) 
+        printf( "Counter-example verification succeeded.\n" );
+    Gia_ManStop( pGia );
+    return pCexMin;
+}
 
 /**Function*************************************************************