From 4c90af0f10f3d79a084988c0fbdd915725160e94 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 25 Jun 2021 07:05:38 -0700 Subject: Potential upgrade to 'dsec'. --- src/proof/fra/fraSec.c | 24 ++++++++++++++++++++++++ 1 file changed, 24 insertions(+) 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" @@ -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 ) { -- cgit v1.2.3