diff options
Diffstat (limited to 'src')
| -rw-r--r-- | src/proof/fra/fraSec.c | 24 |
1 files changed, 24 insertions, 0 deletions
diff --git a/src/proof/fra/fraSec.c b/src/proof/fra/fraSec.c index 7e382fc8..eadd06c9 100644 --- a/src/proof/fra/fraSec.c +++ b/src/proof/fra/fraSec.c @@ -20,6 +20,7 @@ #include "fra.h" #include "aig/ioa/ioa.h" +#include "aig/gia/giaAig.h" #include "proof/int/int.h" #include "proof/ssw/ssw.h" #include "aig/saig/saig.h" @@ -92,6 +93,28 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p ) SeeAlso [] ***********************************************************************/ +Aig_Man_t * Fra_FraigEquivence2( Aig_Man_t * pAig, int nConfs, int fVerbose ) +{ + extern Gia_Man_t * Cec4_ManSimulateTest3( Gia_Man_t * p, int nBTLimit, int fVerbose ); + Gia_Man_t * pGia = Gia_ManFromAig( pAig ); + Gia_Man_t * pGiaNew = Cec4_ManSimulateTest3( pGia, nConfs, 0 ); + Aig_Man_t * pAigNew = Gia_ManToAig( pGiaNew, 0 ); + Gia_ManStop( pGiaNew ); + Gia_ManStop( pGia ); + return pAigNew; +} + +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ int Fra_FraigSec( Aig_Man_t * p, Fra_Sec_t * pParSec, Aig_Man_t ** ppResult ) { Ssw_Pars_t Pars2, * pPars2 = &Pars2; @@ -267,6 +290,7 @@ ABC_PRT( "Time", Abc_Clock() - clk ); { clk = Abc_Clock(); pNew = Fra_FraigEquivence( pTemp = pNew, 100, 0 ); + //pNew = Fra_FraigEquivence2( pTemp = pNew, 100, 0 ); Aig_ManStop( pTemp ); if ( pParSec->fVerbose ) { |