diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-21 20:08:05 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-05-21 20:08:05 -0700 |
| commit | 0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650 (patch) | |
| tree | 7b73de1f0e5f22fa08456eac21dc208ceeb971e1 /src/base/wlc/wlcBlast.c | |
| parent | 34c5ac88d4c2ca440a716892c9fd0045b78662c9 (diff) | |
| download | abc-0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650.tar.gz abc-0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650.tar.bz2 abc-0f29f0aec9b6b8fe3a0b83ed52cb1dda38819650.zip | |
Improving SMT-LIB parser.
Diffstat (limited to 'src/base/wlc/wlcBlast.c')
| -rw-r--r-- | src/base/wlc/wlcBlast.c | 14 |
1 files changed, 12 insertions, 2 deletions
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 ); |