diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-07 15:05:21 -0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2016-06-07 15:05:21 -0700 |
| commit | 820a48b2cb61131f527af7b6fe3ae1c566c4356f (patch) | |
| tree | eb33efcc0af0ed9b0e618d4a3fbd19793ae06dcd /src/base | |
| parent | 4efbd7b3ca360ba35c48e9306c92ad93c4c47af1 (diff) | |
| download | abc-820a48b2cb61131f527af7b6fe3ae1c566c4356f.tar.gz abc-820a48b2cb61131f527af7b6fe3ae1c566c4356f.tar.bz2 abc-820a48b2cb61131f527af7b6fe3ae1c566c4356f.zip | |
Changes to Wlc to accommodate signed signals in SMT-LIB.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/wlc/wlc.h | 2 | ||||
| -rw-r--r-- | src/base/wlc/wlcBlast.c | 14 |
2 files changed, 9 insertions, 7 deletions
diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h index 7fe091d9..51152fa8 100644 --- a/src/base/wlc/wlc.h +++ b/src/base/wlc/wlc.h @@ -199,6 +199,8 @@ static inline int Wlc_ObjRangeIsReversed( Wlc_Obj_t * p ) static inline int Wlc_ObjIsSigned( Wlc_Obj_t * p ) { return p->Signed; } static inline int Wlc_ObjIsSignedFanin01( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ){ return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : (Wlc_ObjFanin0(p, pObj)->Signed && Wlc_ObjFanin1(p, pObj)->Signed); } +static inline int Wlc_ObjIsSignedFanin0( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : Wlc_ObjFanin0(p, pObj)->Signed; } +static inline int Wlc_ObjIsSignedFanin1( Wlc_Ntk_t * p, Wlc_Obj_t * pObj ) { return p->fSmtLib ? Wlc_ObjIsSigned(pObj) : Wlc_ObjFanin1(p, pObj)->Signed; } static inline int Wlc_ObjSign( Wlc_Obj_t * p ) { return Abc_Var2Lit( Wlc_ObjRange(p), Wlc_ObjIsSigned(p) ); } static inline int * Wlc_ObjConstValue( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_CONST); return Wlc_ObjFanins(p); } static inline int Wlc_ObjTableId( Wlc_Obj_t * p ) { assert(p->Type == WLC_OBJ_TABLE); return p->Fanins[1]; } diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 727e3d26..59562432 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -873,7 +873,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, else if ( pObj->Type == WLC_OBJ_BUF ) { int nRangeMax = Abc_MaxInt( nRange0, nRange ); - int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) ); for ( k = 0; k < nRange; k++ ) Vec_IntPush( vRes, pArg0[k] ); } @@ -928,9 +928,9 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, pObj->Type == WLC_OBJ_SHIFT_L || pObj->Type == WLC_OBJ_SHIFT_LA ) { int nRangeMax = Abc_MaxInt( nRange, nRange0 ); - int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) ); if ( pObj->Type == WLC_OBJ_SHIFT_R || pObj->Type == WLC_OBJ_SHIFT_RA ) - Wlc_BlastShiftRight( pNew, pArg0, nRangeMax, pFans1, nRange1, Wlc_ObjFanin0(p, pObj)->Signed && pObj->Type == WLC_OBJ_SHIFT_RA, vRes ); + Wlc_BlastShiftRight( pNew, pArg0, nRangeMax, pFans1, nRange1, Wlc_ObjIsSignedFanin0(p, pObj) && pObj->Type == WLC_OBJ_SHIFT_RA, vRes ); else Wlc_BlastShiftLeft( pNew, pArg0, nRangeMax, pFans1, nRange1, 0, vRes ); Vec_IntShrink( vRes, nRange ); @@ -948,7 +948,7 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, else if ( pObj->Type == WLC_OBJ_BIT_NOT ) { int nRangeMax = Abc_MaxInt( nRange, nRange0 ); - int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) ); for ( k = 0; k < nRange; k++ ) Vec_IntPush( vRes, Abc_LitNot(pArg0[k]) ); } @@ -1151,15 +1151,15 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int fGiaSimple, else if ( pObj->Type == WLC_OBJ_ARI_MINUS ) { int nRangeMax = Abc_MaxInt( nRange0, nRange ); - int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) ); Wlc_BlastMinus( pNew, pArg0, nRangeMax, vRes ); Vec_IntShrink( vRes, nRange ); } else if ( pObj->Type == WLC_OBJ_ARI_POWER ) { int nRangeMax = Abc_MaxInt(nRange0, nRange); - int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjFanin0(p, pObj)->Signed ); - int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange1, Wlc_ObjFanin1(p, pObj)->Signed ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, Wlc_ObjIsSignedFanin0(p, pObj) ); + int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRange1, Wlc_ObjIsSignedFanin1(p, pObj) ); Wlc_BlastPower( pNew, pArg0, nRangeMax, pArg1, nRange1, vTemp2, vRes ); Vec_IntShrink( vRes, nRange ); } |