diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c index 5cb503463..9114016ec 100644 --- a/src/base/abci/abc.c +++ b/src/base/abci/abc.c @@ -680,6 +680,11 @@ extern Vec_Ptr_t * Abc_NtkCollectCoNames( Abc_Ntk_t * pNtk ); extern void Extra_BitMatrixTransposeP( Vec_Wrd_t * vSimsIn, int nWordsIn, Vec_Wrd_t * vSimsOut, int nWordsOut ); +typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; +typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; +extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); +extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); + //////////////////////////////////////////////////////////////////////// /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// @@ -51320,10 +51325,6 @@ usage: ***********************************************************************/ int Abc_CommandAbc9SProve( Abc_Frame_t * pAbc, int argc, char ** argv ) { - typedef struct Wlc_Ntk_t_ Wlc_Ntk_t; - typedef struct Wlc_BstPar_t_ Wlc_BstPar_t; - extern Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pPars ); - extern int Cec_GiaProveTest( Gia_Man_t * p, int nProcs, int nTimeOut, int nTimeOut2, int nTimeOut3, int fUseUif, Wlc_Ntk_t * pWlc, int fVerbose, int fVeryVerbose, int fSilent ); Gia_Man_t * pGiaUse = pAbc->pGia, * pGiaTemp = NULL; Wlc_Ntk_t * pWlc = (Wlc_Ntk_t *)pAbc->pAbcWlc; int c, nProcs = 5, nTimeOut = 3, nTimeOut2 = 10, nTimeOut3 = 100, fUseUif = 0, fVerbose = 0, fVeryVerbose = 0, fSilent = 0; diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index f028a1324..495861d90 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1722,7 +1722,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) Wlc_ObjForEachFanin( pObj, iFanin, k ) if ( k > 0 ) fSigned &= Wlc_NtkObj(p, iFanin)->Signed; - if ( pParIn->fBlastNew && nRange0 <= 16 ) + if ( pPar->fBlastNew && nRange0 <= 16 ) { char * pNums = Wlc_NtkMuxTreeString( nRange0 ); Vec_Int_t ** pvDecs = Wlc_NtkMuxTree3DecsDerive( pNew, pFans0, nRange0, pNums ); @@ -1989,9 +1989,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) int fCompl = (pObj->Type == WLC_OBJ_COMP_MOREEQU || pObj->Type == WLC_OBJ_COMP_LESSEQU); if ( fSwap ) ABC_SWAP( int *, pArg0, pArg1 ); if ( fSigned ) - iLit = pParIn->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); + iLit = pPar->fBlastNew ? Wlc_BlastLessSigned3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLessSigned( pNew, pArg0, pArg1, nRangeMax ); else - iLit = pParIn->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); + iLit = pPar->fBlastNew ? Wlc_BlastLess3( pNew, pArg0, pArg1, nRangeMax ) : Wlc_BlastLess( pNew, pArg0, pArg1, nRangeMax ); iLit = Abc_LitNotCond( iLit, fCompl ); Vec_IntFill( vRes, 1, iLit ); for ( k = 1; k < nRange; k++ ) @@ -2124,7 +2124,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Wlc_BstPar_t * pParIn ) else if ( pObj->Type == WLC_OBJ_DEC ) { int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRange0, 0 ); - if ( pParIn->fBlastNew ) + if ( pPar->fBlastNew ) Wlc_BlastDecoder2( pNew, pArg0, nRange0, vTemp2, vRes ); else Wlc_BlastDecoder( pNew, pArg0, nRange0, vTemp2, vRes ); @@ -3015,4 +3015,3 @@ void Wlc_MultBlastTest() ABC_NAMESPACE_IMPL_END -