diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2017-06-05 12:36:26 +0200 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2017-06-05 12:36:26 +0200 |
| commit | e140ef7e5a45b23823bdf1189070573439966ac8 (patch) | |
| tree | 812a9d711e15efd51efe92792030735adaa64936 /src/base | |
| parent | 943e625e753933ee01fe3e329700752a8e0327ac (diff) | |
| download | abc-e140ef7e5a45b23823bdf1189070573439966ac8.tar.gz abc-e140ef7e5a45b23823bdf1189070573439966ac8.tar.bz2 abc-e140ef7e5a45b23823bdf1189070573439966ac8.zip | |
Bug fix in SMT handling: 'distinct' with more than two inputs.
Diffstat (limited to 'src/base')
| -rw-r--r-- | src/base/wlc/wlcBlast.c | 25 | ||||
| -rw-r--r-- | src/base/wlc/wlcReadSmt.c | 2 |
2 files changed, 26 insertions, 1 deletions
diff --git a/src/base/wlc/wlcBlast.c b/src/base/wlc/wlcBlast.c index 794efbc4..b2d0e287 100644 --- a/src/base/wlc/wlcBlast.c +++ b/src/base/wlc/wlcBlast.c @@ -1211,6 +1211,31 @@ Gia_Man_t * Wlc_NtkBitBlast( Wlc_Ntk_t * p, Vec_Int_t * vBoxIds, int iOutput, in for ( k = 1; k < nRange; k++ ) Vec_IntPush( vRes, 0 ); } + else if ( pObj->Type == WLC_OBJ_COMP_NOTEQU && Wlc_ObjFaninNum(pObj) > 2 ) + { + // find the max range + int a, b, iRes = 1, nRangeMax = Abc_MaxInt( nRange0, nRange1 ); + for ( k = 2; k < Wlc_ObjFaninNum(pObj); k++ ) + nRangeMax = Abc_MaxInt( nRangeMax, Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, k)) ) ); + // create pairwise distinct + for ( a = 0; a < Wlc_ObjFaninNum(pObj); a++ ) + for ( b = a+1; b < Wlc_ObjFaninNum(pObj); b++ ) + { + int nRange0 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, a)) ); + int nRange1 = Wlc_ObjRange( Wlc_NtkObj(p, Wlc_ObjFaninId(pObj, b)) ); + int * pFans0 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, a)) ); + int * pFans1 = Vec_IntEntryP( vBits, Wlc_ObjCopy(p, Wlc_ObjFaninId(pObj, b)) ); + int * pArg0 = Wlc_VecLoadFanins( vTemp0, pFans0, nRange0, nRangeMax, 0 ); + int * pArg1 = Wlc_VecLoadFanins( vTemp1, pFans1, nRange1, nRangeMax, 0 ); + int iLit = 0; + for ( k = 0; k < nRangeMax; k++ ) + iLit = Gia_ManHashOr( pNew, iLit, Gia_ManHashXor(pNew, pArg0[k], pArg1[k]) ); + iRes = Gia_ManHashAnd( pNew, iRes, iLit ); + } + Vec_IntFill( vRes, 1, iRes ); + for ( k = 1; k < nRange; k++ ) + Vec_IntPush( vRes, 0 ); + } else if ( pObj->Type == WLC_OBJ_COMP_EQU || pObj->Type == WLC_OBJ_COMP_NOTEQU ) { int iLit = 0, nRangeMax = Abc_MaxInt( nRange0, nRange1 ); diff --git a/src/base/wlc/wlcReadSmt.c b/src/base/wlc/wlcReadSmt.c index 69a01ab0..230b34ad 100644 --- a/src/base/wlc/wlcReadSmt.c +++ b/src/base/wlc/wlcReadSmt.c @@ -331,7 +331,7 @@ static inline int Smt_PrsCreateNode( Wlc_Ntk_t * pNtk, int Type, int fSigned, in Type == WLC_OBJ_LOGIC_OR || // 29: logic OR Type == WLC_OBJ_LOGIC_XOR || // 30: logic XOR Type == WLC_OBJ_COMP_EQU || // 31: compare equal - Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal +// Type == WLC_OBJ_COMP_NOTEQU || // 32: compare not equal -- bug fix Type == WLC_OBJ_COMP_LESS || // 33: compare less Type == WLC_OBJ_COMP_MORE || // 34: compare more Type == WLC_OBJ_COMP_LESSEQU || // 35: compare less or equal |