diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-20 20:13:40 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2012-09-20 20:13:40 -0700 |
| commit | b5306c156677b7fffe3ec34ee061f57fc0a7671a (patch) | |
| tree | a6d4eac54a65105b37b0ad7d98fc8c5ec590ecf7 /src/proof/abs/abs.h | |
| parent | 5f09917c22f69670a62a8ea49dcaea299b4bf95a (diff) | |
| download | abc-b5306c156677b7fffe3ec34ee061f57fc0a7671a.tar.gz abc-b5306c156677b7fffe3ec34ee061f57fc0a7671a.tar.bz2 abc-b5306c156677b7fffe3ec34ee061f57fc0a7671a.zip | |
Added simplification before the concurrent call to PDR.
Diffstat (limited to 'src/proof/abs/abs.h')
| -rw-r--r-- | src/proof/abs/abs.h | 3 |
1 files changed, 2 insertions, 1 deletions
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 =========================================================*/ |