diff options
author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 20:56:05 -0800 |
---|---|---|
committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-11-11 20:56:05 -0800 |
commit | 3beb36778ec35702690833e6a5d01498d1113b28 (patch) | |
tree | bf9a89c9505ee2badb4eae7983cd2f2f03f90136 /src/aig | |
parent | 9fe4c74952691c3a6cc87dc85edb43da11dd8c8e (diff) | |
download | abc-3beb36778ec35702690833e6a5d01498d1113b28.tar.gz abc-3beb36778ec35702690833e6a5d01498d1113b28.tar.bz2 abc-3beb36778ec35702690833e6a5d01498d1113b28.zip |
Enabled counter-example minimization in 'write_counter'.
Diffstat (limited to 'src/aig')
-rw-r--r-- | src/aig/saig/saig.h | 2 | ||||
-rw-r--r-- | src/aig/saig/saigAbsCba.c | 12 |
2 files changed, 10 insertions, 4 deletions
diff --git a/src/aig/saig/saig.h b/src/aig/saig/saig.h index 96fdde5e..9f98a8f9 100644 --- a/src/aig/saig/saig.h +++ b/src/aig/saig/saig.h @@ -136,7 +136,7 @@ extern Vec_Int_t * Saig_ManFlops2Classes( int nRegs, Vec_Int_t * vFlops ); extern Abc_Cex_t * Saig_ManCexRemap( Aig_Man_t * p, Aig_Man_t * pAbs, Abc_Cex_t * pCexAbs ); /*=== sswAbsCba.c ==========================================================*/ extern Vec_Int_t * Saig_ManCbaFilterFlops( Aig_Man_t * pAig, Abc_Cex_t * pAbsCex, Vec_Int_t * vFlopClasses, Vec_Int_t * vAbsFfsToAdd, int nFfsToSelect ); -extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose ); +extern Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ); extern Vec_Int_t * Saig_ManCbaFilterInputs( Aig_Man_t * pAig, int iFirstFlopPi, Abc_Cex_t * pCex, int fVerbose ); extern Vec_Int_t * Saig_ManCbaPerform( Aig_Man_t * pAig, int nInputs, Saig_ParBmc_t * pPars ); /*=== sswAbsPba.c ==========================================================*/ diff --git a/src/aig/saig/saigAbsCba.c b/src/aig/saig/saigAbsCba.c index 32b9c129..15f2bdfd 100644 --- a/src/aig/saig/saigAbsCba.c +++ b/src/aig/saig/saigAbsCba.c @@ -593,7 +593,7 @@ void Saig_ManCbaShrink( Saig_ManCba_t * p ) SeeAlso [] ***********************************************************************/ -Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fNewOrder, int fVerbose ) +Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInputs, int fVerbose ) { Saig_ManCba_t * p; Vec_Int_t * vReasons; @@ -611,8 +611,8 @@ Abc_Cex_t * Saig_ManCbaFindCexCareBits( Aig_Man_t * pAig, Abc_Cex_t * pCex, int Saig_ManCbaShrink( p ); -if ( fVerbose ) -Aig_ManPrintStats( p->pFrames ); +//if ( fVerbose ) +//Aig_ManPrintStats( p->pFrames ); if ( fVerbose ) { @@ -629,9 +629,15 @@ ABC_PRT( "Time", clock() - clk ); Saig_ManCbaStop( p ); if ( fVerbose ) +{ +printf( "Real " ); Abc_CexPrintStats( pCex ); +} if ( fVerbose ) +{ +printf( "Care " ); Abc_CexPrintStats( pCare ); +} return pCare; } |