diff options
| author | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-01 12:35:34 +0700 |
|---|---|---|
| committer | Alan Mishchenko <alanmi@berkeley.edu> | 2011-08-01 12:35:34 +0700 |
| commit | 820a147ef1e8ff307c3d4e675001372e8f636404 (patch) | |
| tree | 00112747e075531f04a8326e2654791a75fddd9b /src/aig/saig/saigRefSat.c | |
| parent | 957b9f0173d70a1b750f1ef09580065b9285761c (diff) | |
| download | abc-820a147ef1e8ff307c3d4e675001372e8f636404.tar.gz abc-820a147ef1e8ff307c3d4e675001372e8f636404.tar.bz2 abc-820a147ef1e8ff307c3d4e675001372e8f636404.zip | |
Removed useless typecasts related to changes in Vec_VecEntry().
Diffstat (limited to 'src/aig/saig/saigRefSat.c')
| -rw-r--r-- | src/aig/saig/saigRefSat.c | 22 |
1 files changed, 11 insertions, 11 deletions
diff --git a/src/aig/saig/saigRefSat.c b/src/aig/saig/saigRefSat.c index 27c243b5..d117c643 100644 --- a/src/aig/saig/saigRefSat.c +++ b/src/aig/saig/saigRefSat.c @@ -286,10 +286,10 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu { // collect nodes starting from the roots Aig_ManIncrementTravId( pAig ); - vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f ); + vRoots = Vec_VecEntryInt( vFrameCos, f ); Aig_ManForEachNodeVec( pAig, vRoots, pObj, i ) Saig_ManUnrollCollect_rec( pAig, pObj, - (Vec_Int_t *)Vec_VecEntry(vFrameObjs, f), + Vec_VecEntryInt(vFrameObjs, f), (Vec_Int_t *)(f ? Vec_VecEntry(vFrameCos, f-1) : NULL) ); } @@ -304,7 +304,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu for ( f = 0; f <= pCex->iFrame; f++ ) { // construct - vObjs = (Vec_Int_t *)Vec_VecEntry( vFrameObjs, f ); + vObjs = Vec_VecEntryInt( vFrameObjs, f ); Aig_ManForEachNodeVec( pAig, vObjs, pObj, i ) { if ( Aig_ObjIsNode(pObj) ) @@ -331,7 +331,7 @@ Aig_Man_t * Saig_ManUnrollWithCex( Aig_Man_t * pAig, Abc_Cex_t * pCex, int nInpu if ( f == pCex->iFrame ) break; // transfer - vRoots = (Vec_Int_t *)Vec_VecEntry( vFrameCos, f ); + vRoots = Vec_VecEntryInt( vFrameCos, f ); Aig_ManForEachNodeVec( pAig, vRoots, pObj, i ) Saig_ObjLiToLo( pAig, pObj )->pData = pObj->pData; } @@ -574,7 +574,7 @@ Abc_Cex_t * Saig_RefManRunSat( Saig_RefMan_t * p, int fNewOrder ) Vec_IntPush( vAssumps, Entry ); for ( i = 0; i < Vec_VecSize(vLits); i++ ) - printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); printf( "\n" ); if ( p->fVerbose ) @@ -624,7 +624,7 @@ clk = clock(); Vec_IntPush( vAssumps, Entry ); // for ( i = 0; i < Vec_VecSize(vLits); i++ ) -// printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); +// printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); // printf( "\n" ); if ( p->fVerbose ) @@ -655,12 +655,12 @@ clk = clock(); continue; // UNSAT - remove literals - Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) ); + Vec_IntClear( Vec_VecEntryInt(vLits, f) ); Counter--; } for ( i = 0; i < Vec_VecSize(vLits); i++ ) - printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); printf( "\n" ); if ( p->fVerbose ) @@ -787,7 +787,7 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) // derive literals vLits = Saig_RefManOrderLiterals( p, vVar2PiId, vAssumps ); for ( i = 0; i < Vec_VecSize(vLits); i++ ) - printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); printf( "\n" ); // create different sets of assumptions @@ -808,12 +808,12 @@ Vec_Int_t * Saig_RefManRefineWithSat( Saig_RefMan_t * p, Vec_Int_t * vAigPis ) continue; // UNSAT - remove literals - Vec_IntClear( (Vec_Int_t *)Vec_VecEntry(vLits, f) ); + Vec_IntClear( Vec_VecEntryInt(vLits, f) ); Counter--; } for ( i = 0; i < Vec_VecSize(vLits); i++ ) - printf( "%d ", Vec_IntSize( (Vec_Int_t *)Vec_VecEntry(vLits, i) ) ); + printf( "%d ", Vec_IntSize( Vec_VecEntryInt(vLits, i) ) ); printf( "\n" ); // create assumptions |