Integrating SAT-based CEX minimization (bug fix).

src/aig/gia/giaCex.c

@@ -518,7 +518,7 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int
 {
     abctime clk = Abc_Clock();
     int n, i, iFirstVar, iLit, status;
-    Vec_Int_t * vLits;
+    Vec_Int_t * vLits = NULL, * vTemp;
     sat_solver * pSat;
     Cnf_Dat_t * pCnf;
     int nFinal, * pFinal;
@@ -547,14 +547,17 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int
     status = sat_solver_addclause( pSat, &iLit, &iLit + 1 );
     assert( status );
     // create literals
-    vLits = Vec_IntAlloc( 100 );
+    vTemp = 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)) );
+        Vec_IntPush( vTemp, 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++ )
     {
+        Vec_IntFreeP( &vLits );
+
+        vLits = Vec_IntDup( vTemp );
         if ( n ) Vec_IntReverseOrder( vLits );
 
         // SAT-based minimization
@@ -596,7 +599,8 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimizeAig( Gia_Man_t * p, Abc_Cex_t * pCex, int
         Bmc_CexPrint( pCexBest, pCexBest->nPis, 0 );
     }
     // cleanup
-    Vec_IntFree( vLits );
+    Vec_IntFreeP( &vLits );
+    Vec_IntFreeP( &vTemp );
     sat_solver_delete( pSat );
     Cnf_DataFree( pCnf );
     Gia_ManStop( pFrames );

src/base/io/io.c

@@ -2492,8 +2492,8 @@ usage:
     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-u     : use SAT-based CEX minimization [default = %s]\n", fUseSatBased? "yes": "no" );
+    fprintf( pAbc->Err, "\t-m     : minimize CEX by dropping don't-care values [default = %s]\n", fMinimize? "yes": "no" );
+    fprintf( pAbc->Err, "\t-u     : use fast 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" );

src/sat/bmc/bmcCexCare.c

@@ -439,11 +439,7 @@ Abc_Cex_t * Bmc_CexCareSatBasedMinimize( Aig_Man_t * p, int nRealPis, Abc_Cex_t
         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" );
+    // unfortunately, cannot verify - ternary simulation does not work
     Gia_ManStop( pGia );
     return pCexMin;
 }