diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2021-06-25 07:05:38 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2021-06-25 07:05:38 -0700 |
| commit | 4c90af0f10f3d79a084988c0fbdd915725160e94 (patch) | |
| tree | 27d66fc964c6595d691adaff6797fcd55b162fe7 /src/proof/fra | |
| parent | 28ba2c52137883b4acc46b2d31edf717822e543f (diff) | |
| download | abc-4c90af0f10f3d79a084988c0fbdd915725160e94.tar.gz abc-4c90af0f10f3d79a084988c0fbdd915725160e94.tar.bz2 abc-4c90af0f10f3d79a084988c0fbdd915725160e94.zip | |
Potential upgrade to 'dsec'.
Diffstat (limited to 'src/proof/fra')
| -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 ) { |