summaryrefslogtreecommitdiffstats
path: root/src/proof
diff options
context:
space:
mode:
Diffstat (limited to 'src/proof')
-rw-r--r--src/proof/bbr/bbrReach.c2
-rw-r--r--src/proof/fra/fraCore.c2
-rw-r--r--src/proof/live/liveness.c6
-rw-r--r--src/proof/live/liveness_sim.c2
-rw-r--r--src/proof/llb/llb2Flow.c8
-rw-r--r--src/proof/pdr/pdrCnf.c2
-rw-r--r--src/proof/pdr/pdrTsim.c12
-rw-r--r--src/proof/pdr/pdrUtil.c6
-rw-r--r--src/proof/ssw/sswBmc.c2
-rw-r--r--src/proof/ssw/sswDyn.c10
-rw-r--r--src/proof/ssw/sswLcorr.c6
-rw-r--r--src/proof/ssw/sswMan.c2
-rw-r--r--src/proof/ssw/sswSweep.c2
-rw-r--r--src/proof/ssw/sswUnique.c4
14 files changed, 33 insertions, 33 deletions
diff --git a/src/proof/bbr/bbrReach.c b/src/proof/bbr/bbrReach.c
index eda4d7cf..1cce1a90 100644
--- a/src/proof/bbr/bbrReach.c
+++ b/src/proof/bbr/bbrReach.c
@@ -563,7 +563,7 @@ int Aig_ManVerifyUsingBdds( Aig_Man_t * pInit, Saig_ParBbr_t * pPars )
vInputMap = Vec_IntAlloc( Saig_ManPiNum(pInit) );
Saig_ManForEachPi( pInit, pObj, i )
if ( pObj->pData != NULL )
- Vec_IntPush( vInputMap, Aig_ObjPioNum((Aig_Obj_t *)pObj->pData) );
+ Vec_IntPush( vInputMap, Aig_ObjCioId((Aig_Obj_t *)pObj->pData) );
else
Vec_IntPush( vInputMap, -1 );
// create new pattern
diff --git a/src/proof/fra/fraCore.c b/src/proof/fra/fraCore.c
index 2148b467..37aaa0da 100644
--- a/src/proof/fra/fraCore.c
+++ b/src/proof/fra/fraCore.c
@@ -81,7 +81,7 @@ int Fra_FraigMiterStatus( Aig_Man_t * p )
continue;
}
// check if the output is a primary input
- if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjPioNum(Aig_Regular(pChild)) < p->nTruePis )
+ if ( Aig_ObjIsCi(Aig_Regular(pChild)) && Aig_ObjCioId(Aig_Regular(pChild)) < p->nTruePis )
{
CountNonConst0++;
continue;
diff --git a/src/proof/live/liveness.c b/src/proof/live/liveness.c
index e457b3f8..654e1d68 100644
--- a/src/proof/live/liveness.c
+++ b/src/proof/live/liveness.c
@@ -527,7 +527,7 @@ Aig_Man_t * LivenessToSafetyTransformation( int mode, Abc_Ntk_t * pNtk, Aig_Man_
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{
- assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+ assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
}
@@ -830,7 +830,7 @@ Aig_Man_t * LivenessToSafetyTransformationAbs( int mode, Abc_Ntk_t * pNtk, Aig_M
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{
- assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+ assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) + Vec_IntSize( vFlops ) + 1 + liveLatch + fairLatch );
}
@@ -2256,7 +2256,7 @@ Aig_Man_t * LivenessToSafetyTransformationWithLTL( int mode, Abc_Ntk_t * pNtk, A
if( mode == FULL_BIERE_MODE || mode == IGNORE_SAFETY_KEEP_LIVENESS_MODE )
{
- assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+ assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
//assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
}
diff --git a/src/proof/live/liveness_sim.c b/src/proof/live/liveness_sim.c
index b99df807..f1ad794a 100644
--- a/src/proof/live/liveness_sim.c
+++ b/src/proof/live/liveness_sim.c
@@ -466,7 +466,7 @@ static Aig_Man_t * LivenessToSafetyTransformationSim( Abc_Ntk_t * pNtk, Aig_Man_
assert( Aig_ManCheck( pNew ) );
#ifndef DUPLICATE_CKT_DEBUG
- assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjPioNum(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
+ assert((Aig_Obj_t *)Vec_PtrEntry(pNew->vCos, Saig_ManPoNum(pNew)+Aig_ObjCioId(pObjSavedLo)-Saig_ManPiNum(p)-1) == pObjSavedLi);
assert( Saig_ManPoNum( pNew ) == 1 );
assert( Saig_ManPiNum( p ) + 1 == Saig_ManPiNum( pNew ) );
assert( Saig_ManRegNum( pNew ) == Saig_ManRegNum( p ) * 2 + 1 + liveLatch + fairLatch );
diff --git a/src/proof/llb/llb2Flow.c b/src/proof/llb/llb2Flow.c
index a1db70d3..40ca19e5 100644
--- a/src/proof/llb/llb2Flow.c
+++ b/src/proof/llb/llb2Flow.c
@@ -124,9 +124,9 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
{
if ( !Saig_ObjIsPi(p, pObj) )
continue;
- if ( piFirst[Aig_ObjPioNum(pObj)] == -1 )
- piFirst[Aig_ObjPioNum(pObj)] = i;
- piLast[Aig_ObjPioNum(pObj)] = i;
+ if ( piFirst[Aig_ObjCioId(pObj)] == -1 )
+ piFirst[Aig_ObjCioId(pObj)] = i;
+ piLast[Aig_ObjCioId(pObj)] = i;
}
}
// PIs feeding into the flops should be extended to the last frame
@@ -134,7 +134,7 @@ Vec_Ptr_t * Llb_ManCutMap( Aig_Man_t * p, Vec_Ptr_t * vResult, Vec_Ptr_t * vSupp
{
if ( !Saig_ObjIsPi(p, Aig_ObjFanin0(pObj)) )
continue;
- piLast[Aig_ObjPioNum(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1;
+ piLast[Aig_ObjCioId(Aig_ObjFanin0(pObj))] = Vec_PtrSize(vMaps)-1;
}
// set the PI map
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;
diff --git a/src/proof/ssw/sswBmc.c b/src/proof/ssw/sswBmc.c
index b2920177..ff428fa1 100644
--- a/src/proof/ssw/sswBmc.c
+++ b/src/proof/ssw/sswBmc.c
@@ -132,7 +132,7 @@ int Ssw_BmcDynamic( Aig_Man_t * pAig, int nFramesMax, int nConfLimit, int fVerbo
// start managers
assert( Saig_ManRegNum(pAig) > 0 );
- Aig_ManSetPioNumbers( pAig );
+ Aig_ManSetCioIds( pAig );
pSat = Ssw_SatStart( 0 );
pFrm = Ssw_FrmStart( pAig );
pFrm->pFrames = Aig_ManStart( Aig_ManObjNumMax(pAig) * 3 );
diff --git a/src/proof/ssw/sswDyn.c b/src/proof/ssw/sswDyn.c
index f20a7b78..617bb40f 100644
--- a/src/proof/ssw/sswDyn.c
+++ b/src/proof/ssw/sswDyn.c
@@ -113,10 +113,10 @@ void Ssw_ManCollectPos_rec( Ssw_Man_t * p, Aig_Obj_t * pObj, Vec_Int_t * vNewPos
if ( Aig_ObjIsCo(pObj) )
{
// skip if it is a register input PO
- if ( Aig_ObjPioNum(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
+ if ( Aig_ObjCioId(pObj) >= Aig_ManCoNum(p->pFrames)-Aig_ManRegNum(p->pAig) )
return;
// add the number of this constraint
- Vec_IntPush( vNewPos, Aig_ObjPioNum(pObj)/2 );
+ Vec_IntPush( vNewPos, Aig_ObjCioId(pObj)/2 );
return;
}
// visit the fanouts
@@ -225,7 +225,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
}
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) );
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
}
// set random simulation info for the second frame
@@ -236,7 +236,7 @@ void Ssw_ManSweepTransferDyn( Ssw_Man_t * p )
pObjFraig = Ssw_ObjFrame( p, pObj, f );
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) );
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, f );
}
}
@@ -386,7 +386,7 @@ clk = clock();
Ssw_ObjSetFrame( p, Aig_ManConst1(p->pAig), f, Aig_ManConst1(p->pFrames) );
Saig_ManForEachPi( p->pAig, pObj, i )
Ssw_ObjSetFrame( p, pObj, f, Aig_ObjCreateCi(p->pFrames) );
- Aig_ManSetPioNumbers( p->pFrames );
+ Aig_ManSetCioIds( p->pFrames );
// label nodes corresponding to primary inputs
Ssw_ManLabelPiNodes( p );
p->timeReduce += clock() - clk;
diff --git a/src/proof/ssw/sswLcorr.c b/src/proof/ssw/sswLcorr.c
index ec6087f0..71f148e3 100644
--- a/src/proof/ssw/sswLcorr.c
+++ b/src/proof/ssw/sswLcorr.c
@@ -59,7 +59,7 @@ void Ssw_ManSweepTransfer( Ssw_Man_t * p )
}
assert( !Aig_IsComplement(pObjFraig) );
assert( Aig_ObjIsCi(pObjFraig) );
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObjFraig) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObjFraig) );
Ssw_SmlObjSetWord( p->pSml, pObj, pInfo[0], 0, 0 );
}
}
@@ -116,7 +116,7 @@ void Ssw_SmlAddPattern( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pCand )
Value = sat_solver_var_value( p->pMSat->pSat, nVarNum );
if ( Value == 0 )
continue;
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) );
Abc_InfoSetBit( pInfo, p->nPatterns );
}
}
@@ -260,7 +260,7 @@ int Ssw_ManSweepLatch( Ssw_Man_t * p )
pTemp = Aig_NotCond( Ssw_ObjFrame(p, pRepr, 0), pRepr->fPhase ^ pObj->fPhase );
Ssw_ObjSetFrame( p, pObj, 0, pTemp );
}
- Aig_ManSetPioNumbers( p->pFrames );
+ Aig_ManSetCioIds( p->pFrames );
// prepare simulation info
assert( p->vSimInfo == NULL );
diff --git a/src/proof/ssw/sswMan.c b/src/proof/ssw/sswMan.c
index c635569d..e09e0904 100644
--- a/src/proof/ssw/sswMan.c
+++ b/src/proof/ssw/sswMan.c
@@ -48,7 +48,7 @@ Ssw_Man_t * Ssw_ManCreate( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
// prepare the sequential AIG
assert( Saig_ManRegNum(pAig) > 0 );
Aig_ManFanoutStart( pAig );
- Aig_ManSetPioNumbers( pAig );
+ Aig_ManSetCioIds( pAig );
// create interpolation manager
p = ABC_ALLOC( Ssw_Man_t, 1 );
memset( p, 0, sizeof(Ssw_Man_t) );
diff --git a/src/proof/ssw/sswSweep.c b/src/proof/ssw/sswSweep.c
index 550cb4ce..5dd7a1f2 100644
--- a/src/proof/ssw/sswSweep.c
+++ b/src/proof/ssw/sswSweep.c
@@ -167,7 +167,7 @@ void Ssw_SmlAddPatternDyn( Ssw_Man_t * p )
assert( nVarNum > 0 );
if ( sat_solver_var_value( p->pMSat->pSat, nVarNum ) )
{
- pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjPioNum(pObj) );
+ pInfo = (unsigned *)Vec_PtrEntry( p->vSimInfo, Aig_ObjCioId(pObj) );
Abc_InfoSetBit( pInfo, p->nPatterns );
}
}
diff --git a/src/proof/ssw/sswUnique.c b/src/proof/ssw/sswUnique.c
index 8e989531..1bd44a03 100644
--- a/src/proof/ssw/sswUnique.c
+++ b/src/proof/ssw/sswUnique.c
@@ -108,9 +108,9 @@ int Ssw_ManUniqueOne( Ssw_Man_t * p, Aig_Obj_t * pRepr, Aig_Obj_t * pObj, int fV
assert( Aig_ObjIsCi(pTemp) );
if ( !Saig_ObjIsLo(p->pAig, pTemp) )
continue;
- assert( Aig_ObjPioNum(pTemp) > 0 );
+ assert( Aig_ObjCioId(pTemp) > 0 );
Vec_PtrWriteEntry( p->vCommon, k++, pTemp );
- if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjPioNum(pTemp) - Saig_ManPiNum(p->pAig)) )
+ if ( Vec_IntEntry(p->vDiffPairs, Aig_ObjCioId(pTemp) - Saig_ManPiNum(p->pAig)) )
fFeasible = 1;
}
Vec_PtrShrink( p->vCommon, k );
generated by cgit v1.2.3 (git 2.25.1) at 2024-07-04 11:50:41 +0000