diff options
| -rw-r--r-- | src/base/abci/abc.c | 8 | ||||
| -rw-r--r-- | src/proof/abs/abs.h | 3 | ||||
| -rw-r--r-- | src/proof/abs/absGla.c | 2 | ||||
| -rw-r--r-- | src/proof/abs/absPth.c | 23 |
4 files changed, 22 insertions, 14 deletions
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index acb220aa..fb431bf7 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -28164,7 +28164,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) int c, fNewAlgo = 1; Abs_ParSetDefaults( pPars ); Extra_UtilGetoptReset(); - while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpqwvh" ) ) != EOF ) + while ( ( c = Extra_UtilGetopt( argc, argv, "FSCLDETRPBAtfardmnscbpquwvh" ) ) != EOF ) { switch ( c ) { @@ -28323,6 +28323,9 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) case 'q': pPars->fCallProver ^= 1; break; + case 'u': + pPars->fSimpProver ^= 1; + break; case 'v': pPars->fVerbose ^= 1; break; @@ -28371,7 +28374,7 @@ int Abc_CommandAbc9Gla( Abc_Frame_t * pAbc, int argc, char ** argv ) return 0; usage: - Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fardmnscbpqwvh]\n" ); + Abc_Print( -2, "usage: &gla [-FSCLDETRPB num] [-A file] [-fardmnscbpquwvh]\n" ); Abc_Print( -2, "\t fixed-time-frame gate-level proof- and cex-based abstraction\n" ); Abc_Print( -2, "\t-F num : the max number of timeframes to unroll [default = %d]\n", pPars->nFramesMax ); Abc_Print( -2, "\t-S num : the starting time frame (0=unused) [default = %d]\n", pPars->nFramesStart ); @@ -28395,6 +28398,7 @@ usage: Abc_Print( -2, "\t-b : toggle CNF construction without hashing [default = %s]\n", pPars->fSkipHash? "yes": "no" ); Abc_Print( -2, "\t-p : toggle using full-proof for UNSAT cores [default = %s]\n", pPars->fUseFullProof? "yes": "no" ); Abc_Print( -2, "\t-q : toggle calling the prover [default = %s]\n", pPars->fCallProver? "yes": "no" ); + Abc_Print( -2, "\t-u : toggle enabling simplifation before calling the prover [default = %s]\n", pPars->fSimpProver? "yes": "no" ); Abc_Print( -2, "\t-v : toggle printing verbose information [default = %s]\n", pPars->fVerbose? "yes": "no" ); Abc_Print( -2, "\t-w : toggle printing more verbose information [default = %s]\n", pPars->fVeryVerbose? "yes": "no" ); Abc_Print( -2, "\t-h : print the command usage\n"); diff --git a/src/proof/abs/abs.h b/src/proof/abs/abs.h index 11eda38c..5b4f89be 100644 --- a/src/proof/abs/abs.h +++ b/src/proof/abs/abs.h @@ -69,6 +69,7 @@ struct Abs_Par_t_ int fDumpVabs; // dumps the abstracted model int fDumpMabs; // dumps the original AIG with abstraction map int fCallProver; // calls the prover + int fSimpProver; // calls simplification before prover char * pFileVabs; // dumps the abstracted model into this file int fVerbose; // verbose flag int fVeryVerbose; // print additional information @@ -108,7 +109,7 @@ extern int Gia_ManPerformGlaOld( Gia_Man_t * p, Abs_Par_t * pPars, /*=== absIter.c =========================================================*/ extern Gia_Man_t * Gia_ManShrinkGla( Gia_Man_t * p, int nFrameMax, int nTimeOut, int fUsePdr, int fUseSat, int fUseBdd, int fVerbose ); /*=== absPth.c =========================================================*/ -extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ); +extern void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose ); extern void Gia_GlaProveCancel( int fVerbose ); extern int Gia_GlaProveCheck( int fVerbose ); /*=== absVta.c =========================================================*/ diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c index 80ef6ccf..2b2cb8ea 100644 --- a/src/proof/abs/absGla.c +++ b/src/proof/abs/absGla.c @@ -1797,7 +1797,7 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars ) if ( iFrameTryToProve >= 0 ) Gia_GlaProveCancel( pPars->fVerbose ); // prove new one - Gia_GlaProveAbsracted( pAig, pPars->fVeryVerbose ); + Gia_GlaProveAbsracted( pAig, pPars->fSimpProver, pPars->fVeryVerbose ); iFrameTryToProve = f; p->nPdrCalls++; } diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index fc3a92fe..d1fed950 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -46,9 +46,9 @@ ABC_NAMESPACE_IMPL_START #ifndef ABC_USE_PTHREADS -void Gia_GlaProveAbsracted( Gia_Man_t * p, int fVerbose ) {} -void Gia_GlaProveCancel( int fVerbose ) {} -int Gia_GlaProveCheck( int fVerbose ) { return 0; } +void Gia_GlaProveAbsracted( Gia_Man_t * p, int fSimpProver, int fVerbose ) {} +void Gia_GlaProveCancel( int fVerbose ) {} +int Gia_GlaProveCheck( int fVerbose ) { return 0; } #else // pthreads are used @@ -134,7 +134,7 @@ void * Abs_ProverThread( void * pArg ) assert(0); return NULL; } -void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose ) +void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fSimpProver, int fVerbose ) { extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); Abs_ThData_t * pThData; @@ -152,16 +152,19 @@ void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose ) pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); // simplify abstraction - Ssw_ManSetDefaultParams( pPars ); - pPars->nFramesK = 4; - pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars ); + if ( fSimpProver ) + { + Ssw_ManSetDefaultParams( pPars ); + pPars->nFramesK = 4; + pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars ); //printf( "\n" ); //Aig_ManPrintStats( pTemp ); //Aig_ManPrintStats( pAig ); - Aig_ManStop( pTemp ); + Aig_ManStop( pTemp ); + } // synthesize abstraction - pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); - Aig_ManStop( pTemp ); +// pAig = Dar_ManRwsat( pTemp = pAig, 0, 0 ); +// Aig_ManStop( pTemp ); // reset the proof status = pthread_mutex_lock(&g_mutex); assert( status == 0 ); g_fAbstractionProved = 0; |