diff options
Diffstat (limited to 'src/proof/pdr')
| -rw-r--r-- | src/proof/pdr/pdrCnf.c | 2 | ||||
| -rw-r--r-- | src/proof/pdr/pdrTsim.c | 12 | ||||
| -rw-r--r-- | src/proof/pdr/pdrUtil.c | 6 |
3 files changed, 10 insertions, 10 deletions
diff --git a/src/proof/pdr/pdrCnf.c b/src/proof/pdr/pdrCnf.c index fcad15e0..2b039c01 100644 --- a/src/proof/pdr/pdrCnf.c +++ b/src/proof/pdr/pdrCnf.c @@ -202,7 +202,7 @@ static inline int Pdr_ObjRegNum2( Pdr_Man_t * p, int k, int iSatVar ) return -1; pObj = Aig_ManObj( p->pAig, ObjId ); if ( Saig_ObjIsLi( p->pAig, pObj ) ) - return Aig_ObjPioNum(pObj)-Saig_ManPoNum(p->pAig); + return Aig_ObjCioId(pObj)-Saig_ManPoNum(p->pAig); assert( 0 ); // should be called for register inputs only return -1; } diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c index 0547c308..cf4756d1 100644 --- a/src/proof/pdr/pdrTsim.c +++ b/src/proof/pdr/pdrTsim.c @@ -289,14 +289,14 @@ void Pdr_ManDeriveResult( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCi { if ( Saig_ObjIsPi(pAig, pObj) ) { - Lit = toLitCond( Aig_ObjPioNum(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); + Lit = toLitCond( Aig_ObjCioId(pObj), (Vec_IntEntry(vCiVals, i) == 0) ); Vec_IntPush( vPiLits, Lit ); continue; } assert( Saig_ObjIsLo(pAig, pObj) ); if ( Aig_ObjIsTravIdCurrent(pAig, pObj) ) continue; - Lit = toLitCond( Aig_ObjPioNum(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); + Lit = toLitCond( Aig_ObjCioId(pObj) - Saig_ManPiNum(pAig), (Vec_IntEntry(vCiVals, i) == 0) ); Vec_IntPush( vRes, Lit ); } if ( Vec_IntSize(vRes) == 0 ) @@ -323,10 +323,10 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals pBuff[i] = '-'; pBuff[i] = 0; Aig_ManForEachObjVec( vCiObjs, pAig, pObj, i ) - pBuff[Aig_ObjPioNum(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); + pBuff[Aig_ObjCioId(pObj)] = (Vec_IntEntry(vCiVals, i)? '1':'0'); if ( vCi2Rem ) Aig_ManForEachObjVec( vCi2Rem, pAig, pObj, i ) - pBuff[Aig_ObjPioNum(pObj)] = 'x'; + pBuff[Aig_ObjCioId(pObj)] = 'x'; Abc_Print( 1, "%s\n", pBuff ); ABC_FREE( pBuff ); } @@ -406,7 +406,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); { if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; - Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); if ( vPrio != NULL && Vec_IntEntry( vPrio, Entry ) != 0 ) continue; Vec_IntClear( vUndo ); @@ -420,7 +420,7 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, NULL ); { if ( !Saig_ObjIsLo( p->pAig, pObj ) ) continue; - Entry = Aig_ObjPioNum(pObj) - Saig_ManPiNum(p->pAig); + Entry = Aig_ObjCioId(pObj) - Saig_ManPiNum(p->pAig); if ( vPrio == NULL || Vec_IntEntry( vPrio, Entry ) == 0 ) continue; Vec_IntClear( vUndo ); diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c index 9a2cffb2..a47bc9f0 100644 --- a/src/proof/pdr/pdrUtil.c +++ b/src/proof/pdr/pdrUtil.c @@ -616,11 +616,11 @@ int Pdr_NtkFindSatAssign_rec( Aig_Man_t * pAig, Aig_Obj_t * pNode, int Value, Pd if ( Aig_ObjIsCi(pNode) ) { // if ( vSuppLits ) -// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjPioNum(pNode), !Value ) ); +// Vec_IntPush( vSuppLits, Abc_Var2Lit( Aig_ObjCioId(pNode), !Value ) ); if ( Saig_ObjIsLo(pAig, pNode) ) { -// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), !Value ); - pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjPioNum(pNode) - Saig_ManPiNum(pAig), Value ); +// pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), !Value ); + pCube->Lits[pCube->nLits++] = Abc_Var2Lit( Aig_ObjCioId(pNode) - Saig_ManPiNum(pAig), Value ); pCube->Sign |= ((word)1 << (pCube->Lits[pCube->nLits-1] % 63)); } return 1; |