diff options
-rw-r--r-- | src/base/io/io.c | 4 | ||||
-rw-r--r-- | src/proof/abs/absPth.c | 16 |
2 files changed, 17 insertions, 3 deletions
diff --git a/src/base/io/io.c b/src/base/io/io.c index 6135805e..d6b6e91b 100644 --- a/src/base/io/io.c +++ b/src/base/io/io.c @@ -195,8 +195,8 @@ int IoCommandRead( Abc_Frame_t * pAbc, int argc, char ** argv ) pFileName = argv[globalUtilOptind]; // fix the wrong symbol for ( pTemp = pFileName; *pTemp; pTemp++ ) - if ( *pTemp == '>' ) - *pTemp = '\\'; + if ( *pTemp == '>' || *pTemp == '\\' ) + *pTemp = '/'; // read libraries Command[0] = 0; assert( strlen(pFileName) < 900 ); diff --git a/src/proof/abs/absPth.c b/src/proof/abs/absPth.c index d32cd9f5..fc3a92fe 100644 --- a/src/proof/abs/absPth.c +++ b/src/proof/abs/absPth.c @@ -20,6 +20,7 @@ #include "abs.h" #include "proof/pdr/pdr.h" +#include "proof/ssw/ssw.h" // to compile on Linux, add -lpthread to LIBS in Makefile @@ -135,9 +136,11 @@ void * Abs_ProverThread( void * pArg ) } void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose ) { + extern Aig_Man_t * Dar_ManRwsat( Aig_Man_t * pAig, int fBalance, int fVerbose ); Abs_ThData_t * pThData; + Ssw_Pars_t Pars, * pPars = &Pars; + Aig_Man_t * pAig, * pTemp; Gia_Man_t * pAbs; - Aig_Man_t * pAig; pthread_t ProverThread; int status; // disable verbosity @@ -148,6 +151,17 @@ void Gia_GlaProveAbsracted( Gia_Man_t * pGia, int fVerbose ) Gia_ManCleanValue( pGia ); pAig = Gia_ManToAigSimple( pAbs ); Gia_ManStop( pAbs ); + // simplify abstraction + Ssw_ManSetDefaultParams( pPars ); + pPars->nFramesK = 4; + pAig = Ssw_SignalCorrespondence( pTemp = pAig, pPars ); +//printf( "\n" ); +//Aig_ManPrintStats( pTemp ); +//Aig_ManPrintStats( pAig ); + Aig_ManStop( pTemp ); + // synthesize abstraction + 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; |