From b5306c156677b7fffe3ec34ee061f57fc0a7671a Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Thu, 20 Sep 2012 20:13:40 -0700 Subject: Added simplification before the concurrent call to PDR. --- src/proof/abs/abs.h | 3 ++- 1 file changed, 2 insertions(+), 1 deletion(-) (limited to 'src/proof/abs/abs.h') 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 =========================================================*/ -- cgit v1.2.3