From d4f073bad759874161e2de5952ef7d466bc3eb07 Mon Sep 17 00:00:00 2001 From: Alan Mishchenko Date: Fri, 22 Oct 2021 00:00:01 -0700 Subject: Various changes. --- src/aig/gia/gia.h | 7 +++ src/aig/gia/giaMan.c | 1 + src/aig/gia/giaPat2.c | 148 +++++++++++++++++++++++++++++++--------------- src/aig/gia/giaSimBase.c | 78 ++++++++++++++++++++++++ src/aig/gia/giaStoch.c | 20 ------- src/base/acb/acbFunc.c | 2 + src/misc/util/utilTruth.h | 30 +++++----- src/misc/vec/vecPtr.h | 20 +++++++ src/misc/vec/vecWrd.h | 4 ++ 9 files changed, 228 insertions(+), 82 deletions(-) diff --git a/src/aig/gia/gia.h b/src/aig/gia/gia.h index fb924ce5..5548def6 100644 --- a/src/aig/gia/gia.h +++ b/src/aig/gia/gia.h @@ -217,6 +217,7 @@ struct Gia_Man_t_ Vec_Int_t * vClassOld; Vec_Int_t * vClassNew; Vec_Int_t * vPats; + Vec_Bit_t * vPolars; // incremental simulation int fIncrSim; int iNextPi; @@ -1592,6 +1593,12 @@ extern int Gia_ManIncrSimCheckEqual( Gia_Man_t * p, int iLit0, i /*=== giaSimBase.c ============================================================*/ extern Vec_Wrd_t * Gia_ManSimPatSim( Gia_Man_t * p ); extern Vec_Wrd_t * Gia_ManSimPatSimOut( Gia_Man_t * pGia, Vec_Wrd_t * vSimsPi, int fOuts ); +extern void Gia_ManSim2ArrayOne( Vec_Wrd_t * vSimsPi, Vec_Int_t * vRes ); +extern Vec_Wec_t * Gia_ManSim2Array( Vec_Ptr_t * vSims ); +extern Vec_Wrd_t * Gia_ManArray2SimOne( Vec_Int_t * vRes ); +extern Vec_Ptr_t * Gia_ManArray2Sim( Vec_Wec_t * vRes ); +extern void Gia_ManPtrWrdDumpBin( char * pFileName, Vec_Ptr_t * p, int fVerbose ); +extern Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose ); /*=== giaSpeedup.c ============================================================*/ extern float Gia_ManDelayTraceLut( Gia_Man_t * p ); extern float Gia_ManDelayTraceLutPrint( Gia_Man_t * p, int fVerbose ); diff --git a/src/aig/gia/giaMan.c b/src/aig/gia/giaMan.c index 464835e4..a40673a7 100644 --- a/src/aig/gia/giaMan.c +++ b/src/aig/gia/giaMan.c @@ -95,6 +95,7 @@ void Gia_ManStop( Gia_Man_t * p ) Vec_IntFreeP( &p->vClassNew ); Vec_IntFreeP( &p->vClassOld ); Vec_IntFreeP( &p->vPats ); + Vec_BitFreeP( &p->vPolars ); Vec_WrdFreeP( &p->vSims ); Vec_WrdFreeP( &p->vSimsT ); Vec_WrdFreeP( &p->vSimsPi ); diff --git a/src/aig/gia/giaPat2.c b/src/aig/gia/giaPat2.c index 3151ed22..094bdee1 100644 --- a/src/aig/gia/giaPat2.c +++ b/src/aig/gia/giaPat2.c @@ -78,6 +78,8 @@ static inline char Min_LitValL( Min_Man_t * p, int i ) { return Vec_ static inline void Min_LitSetValL( Min_Man_t * p, int i, char v ){ assert(v==0 || v==1); Vec_StrWriteEntry(&p->vValsL, i, v); Vec_StrWriteEntry(&p->vValsL, i^1, (char)!v); Vec_IntPush(&p->vVis, Abc_Lit2Var(i)); } static inline void Min_ObjCleanValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] = 0x0202; } static inline void Min_ObjMarkValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0404; } +static inline void Min_ObjMark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] |= 0x0808; } +static inline void Min_ObjUnmark2ValL( Min_Man_t * p, int i ) { ((short *)Vec_StrArray(&p->vValsL))[i] &= 0xF7F7; } static inline int Min_LitIsCi( Min_Man_t * p, int v ) { return v > 1 && v < p->FirstAndLit; } static inline int Min_LitIsNode( Min_Man_t * p, int v ) { return v >= p->FirstAndLit && v < p->FirstCoLit; } @@ -270,7 +272,7 @@ char Min_LitVerify_rec( Min_Man_t * p, int iLit ) int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitVerify_rec( p, iLit0 ); char Val1 = Min_LitVerify_rec( p, iLit1 ); - assert( Min_LitIsNode(p, iLit) ); // internal node + assert( Val0 < 3 && Val1 < 3 ); if ( Min_LitIsXor(iLit, iLit0, iLit1) ) Val = Min_XsimXor( Val0, Val1 ); else @@ -280,8 +282,11 @@ char Min_LitVerify_rec( Min_Man_t * p, int iLit ) Val ^= Abc_LitIsCompl(iLit); Min_LitSetValL( p, iLit, Val ); } + else + Vec_IntPush( &p->vVis, Abc_Lit2Var(iLit) ); + Min_ObjMark2ValL( p, Abc_Lit2Var(iLit) ); } - return Val; + return Val&3; } char Min_LitVerify( Min_Man_t * p, int iLit, Vec_Int_t * vLits ) { @@ -313,7 +318,7 @@ void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits ) Vec_IntForEachEntryReverse( &p->vVis, iObj, i ) { int iLit = Abc_Var2Lit( iObj, 0 ); - int Value = Min_LitValL(p, iLit); + int Value = 7 & Min_LitValL(p, iLit); if ( Value >= 4 ) { if ( Min_LitIsCi(p, iLit) ) @@ -324,7 +329,7 @@ void Min_LitMinimize( Min_Man_t * p, int iLit, Vec_Int_t * vLits ) int iLit1 = Min_LitFan(p, iLit^1); char Val0 = Min_LitValL( p, iLit0 ); char Val1 = Min_LitValL( p, iLit1 ); - if ( Value == 5 ) // value == 1 + if ( Value&1 ) // value == 1 { assert( (Val0&1) && (Val1&1) ); Min_ObjMarkValL( p, Abc_Lit2Var(iLit0) ); @@ -610,7 +615,7 @@ int Min_LitJustify_rec( Min_Man_t * p, int iLit ) } int Min_LitJustify( Min_Man_t * p, int iLit ) { - int Res, fCheck = 1; + int Res, fCheck = 0; Vec_IntClear( &p->vPat ); if ( iLit < 2 ) return 1; assert( !Min_LitIsCo(p, iLit) ); @@ -621,7 +626,6 @@ int Min_LitJustify( Min_Man_t * p, int iLit ) Min_ManCleanVisitedValL( p ); if ( Res ) { - Vec_IntSort( &p->vPat, 0 ); if ( fCheck && Min_LitVerify(p, iLit, &p->vPat) != 1 ) printf( "Verification FAILED for literal %d.\n", iLit ); //else @@ -912,7 +916,7 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie if ( 1 ) // minimization { //printf( "%d -> ", Vec_IntSize(vPatBest) ); - for ( i = 0; i < 10; i++ ) + for ( i = 0; i < 20; i++ ) { Min_LitMinimize( pNew, Min_ObjLit0(pNew, iObj), vLits ); if ( Vec_IntSize(vPatBest) > Vec_IntSize(&pNew->vPat) ) @@ -921,6 +925,7 @@ Vec_Wec_t * Min_ManComputeCexes( Gia_Man_t * p, Vec_Int_t * vOuts0, int nMaxTrie //printf( "%d ", Vec_IntSize(vPatBest) ); } assert( Vec_IntSize(vPatBest) > 0 ); + Vec_IntSort( vPatBest, 0 ); nCurrCexes += Min_ManAccumulate( vCexes, nOuts*nMinCexes, (nOuts+1)*nMinCexes, vPatBest ); nGoodCalls++; } @@ -1054,46 +1059,69 @@ int Min_ManBitPackOne( Vec_Wrd_t * vSimsPi, int iPat0, int nWords, Vec_Int_t * v break; return iPat; } -Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose ) +Vec_Ptr_t * Min_ReloadCexes( Vec_Wec_t * vCexes, int nMinCexes ) +{ + Vec_Ptr_t * vRes = Vec_PtrAlloc( Vec_WecSize(vCexes) ); + int i, c, nOuts = Vec_WecSize(vCexes)/nMinCexes; + for ( i = 0; i < nMinCexes; i++ ) + for ( c = 0; c < nOuts; c++ ) + { + Vec_Int_t * vLevel = Vec_WecEntry( vCexes, c*nMinCexes+i ); + if ( Vec_IntSize(vLevel) ) + Vec_PtrPush( vRes, vLevel ); + } + return vRes; +} + +Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, int nWords0, Vec_Wec_t * vCexes, int fRandom, int nMinCexes, Vec_Int_t * vScores, int fVerbose ) { abctime clk = Abc_Clock(); int fVeryVerbose = 0; Vec_Wrd_t * vSimsPi = NULL; Vec_Int_t * vLevel; int w, nBits, nTotal = 0, fFailed = ABC_INFINITY; - Vec_Int_t * vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes ); - assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) ); - assert( Vec_WecSize(vCexes)%nMinCexes == 0 ); - Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) ); + Vec_Int_t * vOrder = NULL; + Vec_Ptr_t * vReload = NULL; + if ( 0 ) + { + vOrder = Vec_IntStartNatural( Vec_WecSize(vCexes)/nMinCexes ); + assert( Vec_IntSize(vOrder) == Vec_IntSize(vScores) ); + assert( Vec_WecSize(vCexes)%nMinCexes == 0 ); + Abc_MergeSortCost2Reverse( Vec_IntArray(vOrder), Vec_IntSize(vOrder), Vec_IntArray(vScores) ); + } + else + vReload = Min_ReloadCexes( vCexes, nMinCexes ); if ( fVerbose ) printf( "Packing: " ); - //for ( w = 1; fFailed > 100; w++ ) - for ( w = 1; fFailed > 0; w++ ) + for ( w = nWords0 ? nWords0 : 1; nWords0 ? w <= nWords0 : fFailed > 0; w++ ) { - int i, k, iOut, iPatUsed, iPat = 0; + int i, iPatUsed, iPat = 0; + //int k, iOut; Vec_WrdFreeP( &vSimsPi ); vSimsPi = fRandom ? Vec_WrdStartRandom(2 * Gia_ManCiNum(p) * w) : Vec_WrdStart(2 * Gia_ManCiNum(p) * w); Vec_WrdShrink( vSimsPi, Vec_WrdSize(vSimsPi)/2 ); Abc_TtClear( Vec_WrdLimit(vSimsPi), Vec_WrdSize(vSimsPi) ); fFailed = nTotal = 0; - Vec_IntForEachEntry( vOrder, iOut, k ) - Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes ) + //Vec_IntForEachEntry( vOrder, iOut, k ) + //Vec_WecForEachLevelStartStop( vCexes, vLevel, i, iOut*nMinCexes, (iOut+1)*nMinCexes ) + Vec_PtrForEachEntry( Vec_Int_t *, vReload, vLevel, i ) { - if ( fVeryVerbose && i%nMinCexes == 0 ) - printf( "\n" ); + //if ( fVeryVerbose && i%nMinCexes == 0 ) + // printf( "\n" ); if ( Vec_IntSize(vLevel) == 0 ) continue; iPatUsed = Min_ManBitPackOne( vSimsPi, iPat, w, vLevel ); fFailed += iPatUsed == iPat; - iPat = (iPatUsed + 1) % (64*w - 1); - if ( fVeryVerbose ) - printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed ); - if ( fVeryVerbose ) - Vec_IntPrint( vLevel ); + iPat = (iPatUsed + 1) % (64*(w-1) - 1); + //if ( fVeryVerbose ) + //printf( "Adding output %3d cex %3d to pattern %3d ", i/nMinCexes, i%nMinCexes, iPatUsed ); + //if ( fVeryVerbose ) + //Vec_IntPrint( vLevel ); nTotal++; } if ( fVerbose ) printf( "W = %d (F = %d) ", w, fFailed ); +// printf( "Failed patterns = %d\n", fFailed ); } if ( fVerbose ) printf( "Total = %d\n", nTotal ); @@ -1104,7 +1132,8 @@ Vec_Wrd_t * Min_ManBitPack( Gia_Man_t * p, Vec_Wec_t * vCexes, int fRandom, int Vec_WrdSize(vSimsPi)/Gia_ManCiNum(p), nBits, 100.0*nBits/64/Vec_WrdSize(vSimsPi) ); Abc_PrintTime( 1, "Time", Abc_Clock() - clk ); } - Vec_IntFree( vOrder ); + Vec_IntFreeP( &vOrder ); + Vec_PtrFreeP( &vReload ); return vSimsPi; } @@ -1205,37 +1234,42 @@ Vec_Int_t * Min_ManGetUnsolved( Gia_Man_t * p ) Gia_ManForEachCoDriverId( p, Driver, i ) if ( Driver > 0 ) Vec_IntPush( vRes, i ); + if ( Vec_IntSize(vRes) == 0 ) + Vec_IntFreeP( &vRes ); return vRes; } -Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose ) +Vec_Wrd_t * Min_ManRemapSims( int nInputs, Vec_Int_t * vMap, Vec_Wrd_t * vSimsPi ) { - abctime clk = Abc_Clock(); - Vec_Int_t * vStats[3] = {0}; int i, iObj; - extern Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose ); - Gia_Man_t * pSwp = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 ); - abctime clkSweep = Abc_Clock() - clk; - int nArgs = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n", - nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0; - Vec_Int_t * vOuts = Min_ManGetUnsolved( pSwp ); - Gia_Man_t * pSwp2 = Gia_ManDupSelectedOutputs( pSwp, vOuts ); + int i, iObj, nWords = Vec_WrdSize(vSimsPi)/Vec_IntSize(vMap); + Vec_Wrd_t * vSimsNew = Vec_WrdStart( 2 * nInputs * nWords ); + assert( Vec_WrdSize(vSimsPi)%Vec_IntSize(vMap) == 0 ); + Vec_WrdShrink( vSimsNew, Vec_WrdSize(vSimsNew)/2 ); + Vec_IntForEachEntry( vMap, iObj, i ) + { + Abc_TtCopy( Vec_WrdArray(vSimsNew) + (iObj-1)*nWords, Vec_WrdArray(vSimsPi) + i*nWords, nWords, 0 ); + Abc_TtCopy( Vec_WrdLimit(vSimsNew) + (iObj-1)*nWords, Vec_WrdLimit(vSimsPi) + i*nWords, nWords, 0 ); + } + return vSimsNew; +} +Vec_Wrd_t * Gia_ManCollectSims( Gia_Man_t * pSwp, int nWords, Vec_Int_t * vOuts, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose ) +{ + Vec_Int_t * vStats[3] = {0}; int i, iObj; + Vec_Int_t * vMap = Vec_IntAlloc( 100 ); + Gia_Man_t * pSwp2 = Gia_ManDupCones2( pSwp, Vec_IntArray(vOuts), Vec_IntSize(vOuts), vMap ); Vec_Wec_t * vCexes = Min_ManComputeCexes( pSwp2, NULL, nMaxTries, nMinCexes, vStats, fUseSim, fUseSat, fVerbose ); - Vec_Wrd_t * vSimsPi = Min_ManBitPack( p, vCexes, 1, nMinCexes, vStats[0], fVerbose ); + Vec_Wrd_t * vSimsPi = Min_ManBitPack( pSwp2, nWords, vCexes, 1, nMinCexes, vStats[0], fVerbose ); Vec_Wrd_t * vSimsPo = Gia_ManSimPatSimOut( pSwp2, vSimsPi, 1 ); Vec_Int_t * vCounts = Patt_ManOutputErrorCoverage( vSimsPo, Vec_IntSize(vOuts) ); if ( fVerbose ) - { Patt_ManProfileErrorsOne( vSimsPo, Vec_IntSize(vOuts) ); - Abc_PrintTime( 1, "Sweep time", clkSweep ); - Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); - } - if ( 0 ) + if ( fVeryVerbose ) { printf( "Unsolved = %4d ", Vec_IntSize(vOuts) ); Gia_ManPrintStats( pSwp2, NULL ); Vec_IntForEachEntry( vOuts, iObj, i ) { printf( "%4d : ", i ); - printf( "Out = %5d ", iObj ); + printf( "Out = %5d ", Vec_IntEntry(vMap, i) ); printf( "SimAll =%8d ", Vec_IntEntry(vStats[0], i) ); printf( "SimGood =%8d ", Vec_IntEntry(vStats[1], i) ); printf( "PatsAll =%8d ", Vec_IntEntry(vStats[2], i) ); @@ -1250,20 +1284,40 @@ Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, Vec_IntFree( vCounts ); Vec_WrdFree( vSimsPo ); Vec_WecFree( vCexes ); - Vec_IntFree( vOuts ); - Gia_ManStop( pSwp ); Gia_ManStop( pSwp2 ); + //printf( "Compressing inputs: %5d -> %5d\n", Gia_ManCiNum(pSwp), Vec_IntSize(vMap) ); + vSimsPi = Min_ManRemapSims( Gia_ManCiNum(pSwp), vMap, vSimsPo = vSimsPi ); + Vec_WrdFree( vSimsPo ); + Vec_IntFree( vMap ); + return vSimsPi; +} +Vec_Wrd_t * Min_ManCollect( Gia_Man_t * p, int nConf, int nConf2, int nMaxTries, int nMinCexes, int fUseSim, int fUseSat, int fVerbose, int fVeryVerbose ) +{ + abctime clk = Abc_Clock(); + extern Gia_Man_t * Cec4_ManSimulateTest4( Gia_Man_t * p, int nBTLimit, int nBTLimitPo, int fVerbose ); + Gia_Man_t * pSwp = Cec4_ManSimulateTest4( p, nConf, nConf2, 0 ); + abctime clkSweep = Abc_Clock() - clk; + int nArgs = fVerbose ? printf( "Generating patterns: Conf = %d (%d). Tries = %d. Pats = %d. Sim = %d. SAT = %d.\n", + nConf, nConf2, nMaxTries, nMinCexes, fUseSim, fUseSat ) : 0; + Vec_Int_t * vOuts = Min_ManGetUnsolved( pSwp ); + Vec_Wrd_t * vSimsPi = vOuts ? Gia_ManCollectSims( pSwp, 0, vOuts, nMaxTries, nMinCexes, fUseSim, fUseSat, fVerbose, fVeryVerbose ) : NULL; + if ( vOuts == NULL ) + printf( "There is no satisfiable outputs.\n" ); + if ( fVerbose ) + Abc_PrintTime( 1, "Sweep time", clkSweep ); + if ( fVerbose ) + Abc_PrintTime( 1, "Total time", Abc_Clock() - clk ); + Vec_IntFreeP( &vOuts ); + Gia_ManStop( pSwp ); nArgs = 0; return vSimsPi; } void Min_ManTest2( Gia_Man_t * p ) { - Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 1, 0 ); + Vec_Wrd_t * vSimsPi = Min_ManCollect( p, 100000, 100000, 10000, 20, 1, 0, 1, 1 ); Vec_WrdFreeP( &vSimsPi ); } - - //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c index a9706742..c31064fe 100644 --- a/src/aig/gia/giaSimBase.c +++ b/src/aig/gia/giaSimBase.c @@ -2622,6 +2622,84 @@ void Gia_ManSimArrayTest( Vec_Wrd_t * vSimsPi ) } Vec_PtrFree( vTemp ); } + + +/**Function************************************************************* + + Synopsis [Serialization.] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +void Gia_ManPtrWrdDumpBin( char * pFileName, Vec_Ptr_t * p, int fVerbose ) +{ + Vec_Wrd_t * vLevel; + int i, nSize, RetValue; + FILE * pFile = fopen( pFileName, "wb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for writing.\n", pFileName ); + return; + } + nSize = Vec_PtrSize(p); + RetValue = fwrite( &nSize, 1, sizeof(int), pFile ); + Vec_PtrForEachEntry( Vec_Wrd_t *, p, vLevel, i ) + { + nSize = Vec_WrdSize(vLevel); + RetValue += fwrite( &nSize, 1, sizeof(int), pFile ); + RetValue += fwrite( Vec_WrdArray(vLevel), 1, sizeof(word)*nSize, pFile ); + } + fclose( pFile ); + if ( fVerbose ) + printf( "Written %d arrays into file \"%s\".\n", Vec_PtrSize(p), pFileName ); +} +Vec_Ptr_t * Gia_ManPtrWrdReadBin( char * pFileName, int fVerbose ) +{ + Vec_Ptr_t * p = NULL; Vec_Wrd_t * vLevel; int i, nSize, RetValue; + FILE * pFile = fopen( pFileName, "rb" ); + if ( pFile == NULL ) + { + printf( "Cannot open file \"%s\" for reading.\n", pFileName ); + return NULL; + } + fseek( pFile, 0, SEEK_END ); + nSize = ftell( pFile ); + if ( nSize == 0 ) + { + printf( "The input file is empty.\n" ); + fclose( pFile ); + return NULL; + } + if ( nSize % (int)sizeof(int) > 0 ) + { + printf( "Cannot read file with integers because it is not aligned at 4 bytes (remainder = %d).\n", nSize % (int)sizeof(int) ); + fclose( pFile ); + return NULL; + } + rewind( pFile ); + RetValue = fread( &nSize, 1, sizeof(int), pFile ); + assert( RetValue == 4 ); + p = Vec_PtrAlloc( nSize ); + for ( i = 0; i < nSize; i++ ) + Vec_PtrPush( p, Vec_WrdAlloc(100) ); + Vec_PtrForEachEntry( Vec_Wrd_t *, p, vLevel, i ) + { + RetValue = fread( &nSize, 1, sizeof(int), pFile ); + assert( RetValue == 4 ); + Vec_WrdFill( vLevel, nSize, 0 ); + RetValue = fread( Vec_WrdArray(vLevel), 1, sizeof(word)*nSize, pFile ); + assert( RetValue == 8*nSize ); + } + fclose( pFile ); + if ( fVerbose ) + printf( "Read %d arrays from file \"%s\".\n", Vec_PtrSize(p), pFileName ); + return p; +} + //////////////////////////////////////////////////////////////////////// /// END OF FILE /// //////////////////////////////////////////////////////////////////////// diff --git a/src/aig/gia/giaStoch.c b/src/aig/gia/giaStoch.c index 063bf985..94f53998 100644 --- a/src/aig/gia/giaStoch.c +++ b/src/aig/gia/giaStoch.c @@ -32,26 +32,6 @@ ABC_NAMESPACE_IMPL_START /// FUNCTION DEFINITIONS /// //////////////////////////////////////////////////////////////////////// -/**Function************************************************************* - - Synopsis [] - - Description [] - - SideEffects [] - - SeeAlso [] - -***********************************************************************/ -static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) ) ___unused; -static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) ) -{ - void * pItem; int i; - Vec_PtrForEachEntry( void *, p, pItem, i ) - pFuncItemFree( pItem ); - Vec_PtrFree( p ); -} - /**Function************************************************************* Synopsis [] diff --git a/src/base/acb/acbFunc.c b/src/base/acb/acbFunc.c index a1d6568c..3c0bb5f0 100644 --- a/src/base/acb/acbFunc.c +++ b/src/base/acb/acbFunc.c @@ -506,6 +506,7 @@ Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fN // create names if ( fNames ) { + pNew->vPolars = Vec_BitStart( Gia_ManObjNum(pNew) ); pNew->vNamesNode = Vec_PtrStart( Gia_ManObjNum(pNew) ); Vec_IntForEachEntry( vMap, iLit, Token ) { @@ -514,6 +515,7 @@ Gia_Man_t * Gia_FileSimpleParse( Vec_Int_t * vBuffer, Abc_Nam_t * pNames, int fN sprintf( Buffer, "%c_%s", Abc_LitIsCompl(iLit) ? 'c' : 'd', Abc_NamStr(pNames, Token) ); assert( Vec_PtrEntry(pNew->vNamesNode, Abc_Lit2Var(iLit)) == NULL ); Vec_PtrWriteEntry( pNew->vNamesNode, Abc_Lit2Var(iLit), Abc_UtilStrsav(Buffer) ); + Vec_BitWriteEntry( pNew->vPolars, Abc_Lit2Var(iLit), Abc_LitIsCompl(iLit) ); } } else diff --git a/src/misc/util/utilTruth.h b/src/misc/util/utilTruth.h index dbc0e5a0..d9efa55f 100644 --- a/src/misc/util/utilTruth.h +++ b/src/misc/util/utilTruth.h @@ -2106,12 +2106,15 @@ static inline int Abc_TtCountOnes( word x ) x = x + (x >> 32); return (int)(x & 0xFF); } +static inline int Abc_TtCountOnes2( word x ) +{ + return x ? Abc_TtCountOnes(x) : 0; +} static inline int Abc_TtCountOnesVec( word * x, int nWords ) { int w, Count = 0; for ( w = 0; w < nWords; w++ ) - if ( x[w] ) - Count += Abc_TtCountOnes( x[w] ); + Count += Abc_TtCountOnes2( x[w] ); return Count; } static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, int fCompl ) @@ -2120,14 +2123,12 @@ static inline int Abc_TtCountOnesVecMask( word * x, word * pMask, int nWords, in if ( fCompl ) { for ( w = 0; w < nWords; w++ ) - if ( pMask[w] & ~x[w] ) - Count += Abc_TtCountOnes( pMask[w] & ~x[w] ); + Count += Abc_TtCountOnes2( pMask[w] & ~x[w] ); } else { for ( w = 0; w < nWords; w++ ) - if ( pMask[w] & x[w] ) - Count += Abc_TtCountOnes( pMask[w] & x[w] ); + Count += Abc_TtCountOnes2( pMask[w] & x[w] ); } return Count; } @@ -2136,24 +2137,23 @@ static inline int Abc_TtCountOnesVecMask2( word * x0, word * x1, int fComp0, int int w, Count = 0; if ( !fComp0 && !fComp1 ) for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x0[w] & x1[w] ); + Count += Abc_TtCountOnes2( pMask[w] & x0[w] & x1[w] ); else if ( fComp0 && !fComp1 ) for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & x1[w] ); + Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] & x1[w] ); else if ( !fComp0 && fComp1 ) for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & x0[w] & ~x1[w] ); + Count += Abc_TtCountOnes2( pMask[w] & x0[w] & ~x1[w] ); else for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & ~x0[w] & ~x1[w] ); + Count += Abc_TtCountOnes2( pMask[w] & ~x0[w] & ~x1[w] ); return Count; } static inline int Abc_TtCountOnesVecXor( word * x, word * y, int nWords ) { int w, Count = 0; for ( w = 0; w < nWords; w++ ) - if ( x[w] ^ y[w] ) - Count += Abc_TtCountOnes( x[w] ^ y[w] ); + Count += Abc_TtCountOnes2( x[w] ^ y[w] ); return Count; } static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, word * pMask, int nWords ) @@ -2161,10 +2161,10 @@ static inline int Abc_TtCountOnesVecXorMask( word * x, word * y, int fCompl, wor int w, Count = 0; if ( fCompl ) for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ ~y[w]) ); + Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ ~y[w]) ); else for ( w = 0; w < nWords; w++ ) - Count += Abc_TtCountOnes( pMask[w] & (x[w] ^ y[w]) ); + Count += Abc_TtCountOnes2( pMask[w] & (x[w] ^ y[w]) ); return Count; } static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nWords ) @@ -2173,7 +2173,7 @@ static inline int Abc_TtAndXorSum( word * pOut, word * pIn1, word * pIn2, int nW for ( w = 0; w < nWords; w++ ) { pOut[w] &= pIn1[w] ^ pIn2[w]; - Count += Abc_TtCountOnes( pOut[w] ); + Count += Abc_TtCountOnes2( pOut[w] ); } return Count; } diff --git a/src/misc/vec/vecPtr.h b/src/misc/vec/vecPtr.h index 565e0474..0f024f68 100644 --- a/src/misc/vec/vecPtr.h +++ b/src/misc/vec/vecPtr.h @@ -605,6 +605,26 @@ static inline void Vec_PtrFreeFree( Vec_Ptr_t * p ) Vec_PtrFree( p ); } +/**Function************************************************************* + + Synopsis [] + + Description [] + + SideEffects [] + + SeeAlso [] + +***********************************************************************/ +static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) ) ___unused; +static void Vec_PtrFreeFunc( Vec_Ptr_t * p, void (*pFuncItemFree)(void *) ) +{ + void * pItem; int i; + Vec_PtrForEachEntry( void *, p, pItem, i ) + if ( pItem ) pFuncItemFree( pItem ); + Vec_PtrFree( p ); +} + /**Function************************************************************* Synopsis [Copies the interger array.] diff --git a/src/misc/vec/vecWrd.h b/src/misc/vec/vecWrd.h index 32c78626..8275702a 100644 --- a/src/misc/vec/vecWrd.h +++ b/src/misc/vec/vecWrd.h @@ -382,6 +382,10 @@ static inline int Vec_WrdSize( Vec_Wrd_t * p ) { return p->nSize; } +static inline int Vec_WrdChangeSize( Vec_Wrd_t * p, int Shift ) +{ + return p->nSize += Shift; +} /**Function************************************************************* -- cgit v1.2.3