diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-25 18:19:06 -0700 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2018-03-25 18:19:06 -0700 |
commit | a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0 (patch) | |
tree | e56de4cf3568983deb75e90bd9a9cb8e17f29ee8 /src | |
parent | e639e8fd1ba990f782385b294a6cb5a21844f688 (diff) | |
download | abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.tar.gz abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.tar.bz2 abc-a2d59be3f7f05c4757ade8b3b6f9fdf425de5cc0.zip |
Integrating SAT-based CEX minimization (bug fix).
Diffstat (limited to 'src')
-rw-r--r-- | src/aig/gia/giaCex.c | 12 | ||||
-rw-r--r-- | src/base/io/io.c | 4 | ||||
-rw-r--r-- | src/sat/bmc/bmcCexCare.c | 6 |
3 files changed, 11 insertions, 11 deletions
diff --git a/src/aig/gia/giaCex.c b/src/aig/gia/giaCex.c index edd5c87d..b0e72284 100644 --- a/src/aig/gia/giaCex.c +++ b/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 ); diff --git a/src/base/io/io.c b/src/base/io/io.c index 11b1fa57..5133ef0d 100644 --- a/src/base/io/io.c +++ b/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" ); diff --git a/src/sat/bmc/bmcCexCare.c b/src/sat/bmc/bmcCexCare.c index 8db92444..c274b04c 100644 --- a/src/sat/bmc/bmcCexCare.c +++ b/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; } |