From 0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Sat, 21 May 2016 20:08:05 -0700 Subject: Improving SMT-LIB parser. --- src/base/wlc/wlcBlast.c | 14 ++++++++++++-- 1 file changed, 12 insertions(+), 2 deletions(-) (limited to 'src/base/wlc/wlcBlast.c') diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 16044e67..5ef7ef14 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -777,7 +777,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple // blast in the topological order Wlc_NtkForEachObj( p, pObj, i ) { -// char * pName = Wlc_ObjName(p, i); +// char * pName1 = Wlc_ObjName(p, i); +// char * pName2 = Wlc_ObjFaninNum(pObj) ? Wlc_ObjName(p, Wlc_ObjFaninId0(pObj)) : NULL; + nAndPrev = Gia_ManAndNum(pNew); nRange = Wlc_ObjRange( pObj ); nRange0 = Wlc_ObjFaninNum(pObj) > 0 ? Wlc_ObjRange( Wlc_ObjFanin0(p, pObj) ) : -1; @@ -1007,7 +1009,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple else if ( pObj->Type == WLC_OBJ_BIT_ZEROPAD || pObj->Type == WLC_OBJ_BIT_SIGNEXT ) { int Pad = pObj->Type == WLC_OBJ_BIT_ZEROPAD ? 0 : pFans0[nRange0-1]; - assert( nRange0 < nRange ); + assert( nRange0 <= nRange ); for ( k = 0; k < nRange0; k++ ) Vec_IntPush( vRes, pFans0[k] ); for ( ; k < nRange; k++ ) @@ -1020,6 +1022,14 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple for ( k = 1; k < nRange; k++ ) Vec_IntPush( vRes, 0 ); } + else if ( pObj->Type == WLC_OBJ_LOGIC_IMPL ) + { + int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); + int iLit1 = Wlc_BlastReduction( pNew, pFans1, nRange1, WLC_OBJ_REDUCT_OR ); + Vec_IntFill( vRes, 1, Gia_ManHashOr(pNew, Abc_LitNot(iLit0), iLit1) ); + for ( k = 1; k < nRange; k++ ) + Vec_IntPush( vRes, 0 ); + } else if ( pObj->Type == WLC_OBJ_LOGIC_AND ) { int iLit0 = Wlc_BlastReduction( pNew, pFans0, nRange0, WLC_OBJ_REDUCT_OR ); -- cgit v1.2.3