luke
/
abc
mirror of https://github.com/YosysHQ/abc.git
1
0
Fork 0
Code Issues Packages Projects Releases Wiki Activity

Potential upgrade to 'dsec'.

This commit is contained in:
Alan Mishchenko 2021-06-25 07:05:38 -07:00
parent 28ba2c5213
commit 4c90af0f10
1 changed files with 24 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

24
src/proof/fra/fraSec.c
View File

@ -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"
@ -81,6 +82,28 @@ void Fra_SecSetDefaultParams( Fra_Sec_t * p )
p->fReportSolution = 0; // enables specialized format for reporting solution
}
/**Function*************************************************************
Synopsis []
Description []
SideEffects []
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 []
@ -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 )
{