summaryrefslogtreecommitdiffstats
path: root/src/aig
diff options
context:
space:
mode:
Diffstat (limited to 'src/aig')
-rw-r--r--src/aig/gia/giaCSat2.c3
-rw-r--r--src/aig/gia/giaSimBase.c406
2 files changed, 399 insertions, 10 deletions
diff --git a/src/aig/gia/giaCSat2.c b/src/aig/gia/giaCSat2.c
index ee0ce311..a9739e02 100644
--- a/src/aig/gia/giaCSat2.c
+++ b/src/aig/gia/giaCSat2.c
@@ -1653,9 +1653,12 @@ Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvS
p->timeTotal = Abc_Clock() - clkTotal;
if ( fVerbose )
Cbs2_ManSatPrintStats( p );
+ if ( fVerbose )
+ {
// printf( "RecCalls = %8d. RecClause = %8d. RecNonChro = %8d.\n", p->nRecCall, p->nRecClause, p->nRecNonChro );
printf( "Prop1 = %d. Prop2 = %d. Prop3 = %d. ClaConf = %d. FailJ = %d. FailC = %d. ", p->nPropCalls[0], p->nPropCalls[1], p->nPropCalls[2], p->nClauseConf, p->nFails[0], p->nFails[1] );
Abc_PrintTime( 1, "JFront", p->timeJFront );
+ }
Cbs2_ManStop( p );
*pvStatus = vStatus;
diff --git a/src/aig/gia/giaSimBase.c b/src/aig/gia/giaSimBase.c
index 1adff0be..c53c1db8 100644
--- a/src/aig/gia/giaSimBase.c
+++ b/src/aig/gia/giaSimBase.c
@@ -239,11 +239,10 @@ Vec_Wrd_t * Gia_ManSimBitPacking( Gia_Man_t * p, Vec_Int_t * vCexStore, int nCex
assert( iPat <= nCexes + nUnDecs );
Out = 0;
}
- printf( "Compressed %d CEXes into %d test patterns.\n", nCexes, iPat );
assert( iCur == Vec_IntSize(vCexStore) );
vSimsRes = Gia_ManSimCombine( Gia_ManCiNum(p), p->vSimsPi, vSimsIn, Abc_Bit6WordNum(iPat+1) );
- printf( "Combined %d words of the original info with %d words of additional info.\n",
- Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p), Abc_Bit6WordNum(iPat+1) );
+ printf( "Compressed %d CEXes into %d patterns and added %d words to available %d words.\n",
+ nCexes, iPat, Abc_Bit6WordNum(iPat+1), Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p) );
Vec_WrdFree( vSimsIn );
Vec_WrdFree( vSimsCare );
return vSimsRes;
@@ -344,7 +343,7 @@ void Gia_ManSimPatWrite( char * pFileName, Vec_Wrd_t * vSimsIn, int nWords )
for ( i = 0; i < nNodes; i++ )
Gia_ManSimPatWriteOne( pFile, Vec_WrdEntryP(vSimsIn, i*nWords), nWords );
fclose( pFile );
- printf( "Written %d words of simulation data.\n", nWords );
+ printf( "Written %d words of simulation data into file \"%s\".\n", nWords, pFileName );
}
int Gia_ManSimPatReadOne( char c )
{
@@ -405,11 +404,11 @@ void Gia_ManSimProfile( Gia_Man_t * pGia )
Vec_Wrd_t * vSims = Gia_ManSimPatSim( pGia );
int nWords = Vec_WrdSize(vSims) / Gia_ManObjNum(pGia);
int nC0s = 0, nC1s = 0, nUnique = Gia_ManSimPatHashPatterns( pGia, nWords, vSims, &nC0s, &nC1s );
- printf( "Simulating %d words leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n",
- nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
+ printf( "Simulating %d patterns leads to %d unique objects (%.2f %% out of %d), Const0 = %d. Const1 = %d.\n",
+ 64*nWords, nUnique, 100.0*nUnique/Gia_ManCandNum(pGia), Gia_ManCandNum(pGia), nC0s, nC1s );
Vec_WrdFree( vSims );
}
-void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
+void Gia_ManPatSatImprove( Gia_Man_t * p, int nWords0, int fVerbose )
{
extern Vec_Int_t * Cbs2_ManSolveMiterNc( Gia_Man_t * pAig, int nConfs, Vec_Str_t ** pvStatus, int fVerbose );
int i, Status, Counts[3] = {0};
@@ -418,7 +417,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
Vec_Str_t * vStatus = NULL;
Vec_Int_t * vCexStore = NULL;
Vec_Wrd_t * vSims = Gia_ManSimPatSim( p );
- Gia_ManSimProfile( p );
+ //Gia_ManSimProfile( p );
pGia = Gia_ManSimPatGenMiter( p, vSims );
vCexStore = Cbs2_ManSolveMiterNc( pGia, 1000, &vStatus, 0 );
Gia_ManStop( pGia );
@@ -427,7 +426,8 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
assert( Status >= -1 && Status <= 1 );
Counts[Status+1]++;
}
- printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
+ if ( fVerbose )
+ printf( "Total = %d : SAT = %d. UNSAT = %d. UNDEC = %d.\n", Counts[1]+Counts[2]+Counts[0], Counts[1], Counts[2], Counts[0] );
if ( Counts[1] == 0 )
printf( "There are no counter-examples. No need for more simulation.\n" );
else
@@ -435,7 +435,7 @@ void Gia_ManSimPat( Gia_Man_t * p, int nWords0, int fVerbose )
vSimsIn = Gia_ManSimBitPacking( p, vCexStore, Counts[1], Counts[0] );
Vec_WrdFreeP( &p->vSimsPi );
p->vSimsPi = vSimsIn;
- Gia_ManSimProfile( p );
+ //Gia_ManSimProfile( p );
}
Vec_StrFree( vStatus );
Vec_IntFree( vCexStore );
@@ -1643,6 +1643,392 @@ Vec_Int_t * Gia_RsbSetFind( word * pOffSet, word * pOnSet, Vec_Wrd_t * vSims, in
return vObjs;
}
+/**Function*************************************************************
+
+ Synopsis [Improving quality of simulation patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_SimQualityOne( Gia_Man_t * p, Vec_Int_t * vPat, int fPoOnly )
+{
+ int i, Id, Value, nWords = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
+ Vec_Wrd_t * vTemp, * vSims, * vSimsPi = Vec_WrdStart( Gia_ManCiNum(p) * nWords );
+ Vec_Int_t * vRes;
+ assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
+ Vec_IntForEachEntry( vPat, Value, i )
+ {
+ word * pSim = Vec_WrdEntryP( vSimsPi, i*nWords );
+ if ( Value )
+ Abc_TtFill( pSim, nWords );
+ Abc_TtXorBit( pSim, i+1 );
+ }
+ vTemp = p->vSimsPi;
+ p->vSimsPi = vSimsPi;
+ vSims = Gia_ManSimPatSim( p );
+ p->vSimsPi = vTemp;
+ if ( fPoOnly )
+ {
+ vRes = Vec_IntStart( Gia_ManCoNum(p) );
+ Gia_ManForEachCoId( p, Id, i )
+ {
+ word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
+ if ( pSim[0] & 1 )
+ Abc_TtNot( pSim, nWords );
+ Vec_IntWriteEntry( vRes, i, Abc_TtCountOnesVec(pSim, nWords) );
+ }
+ assert( Vec_IntSize(vRes) == Gia_ManCoNum(p) );
+ }
+ else
+ {
+ vRes = Vec_IntStart( Gia_ManObjNum(p) );
+ Gia_ManForEachAndId( p, Id )
+ {
+ word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
+ if ( pSim[0] & 1 )
+ Abc_TtNot( pSim, nWords );
+ Vec_IntWriteEntry( vRes, Id, Abc_TtCountOnesVec(pSim, nWords) );
+ }
+ assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
+ }
+ Vec_WrdFree( vSims );
+ Vec_WrdFree( vSimsPi );
+ return vRes;
+}
+void Gia_SimQualityTest( Gia_Man_t * p )
+{
+ Vec_Int_t * vPat, * vRes;
+ int k, m, nMints = (1 << Gia_ManCiNum(p));
+ assert( Gia_ManCiNum(p) <= 10 );
+ for ( m = 0; m < nMints; m++ )
+ {
+ printf( "%d : ", m );
+ Extra_PrintBinary( stdout, (unsigned*)&m, Gia_ManCiNum(p) );
+ printf( " " );
+ vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
+ for ( k = 0; k < Gia_ManCiNum(p); k++ )
+ Vec_IntPush( vPat, (m >> k) & 1 );
+ vRes = Gia_SimQualityOne( p, vPat, 1 );
+ printf( "%d ", Vec_IntSum(vRes) );
+ Vec_IntFree( vRes );
+ Vec_IntFree( vPat );
+ printf( "\n" );
+ }
+}
+Vec_Int_t * Gia_SimGenerateStats( Gia_Man_t * p )
+{
+ Vec_Int_t * vTotal = Vec_IntStart( Gia_ManObjNum(p) );
+ Vec_Int_t * vRes, * vPat;
+ int i, k, Value;
+ Abc_Random(1);
+ for ( i = 0; i < 1000; i++ )
+ {
+ vPat = Vec_IntAlloc( Gia_ManCiNum(p) );
+ for ( k = 0; k < Gia_ManCiNum(p); k++ )
+ Vec_IntPush( vPat, Abc_Random(0) & 1 );
+ vRes = Gia_SimQualityOne( p, vPat, 0 );
+ assert( Vec_IntSize(vRes) == Gia_ManObjNum(p) );
+ Vec_IntForEachEntry( vRes, Value, k )
+ Vec_IntAddToEntry( vTotal, k, Value );
+ Vec_IntFree( vRes );
+ Vec_IntFree( vPat );
+ }
+ //Vec_IntPrint( vTotal );
+ return vTotal;
+}
+double Gia_SimComputeScore( Gia_Man_t * p, Vec_Int_t * vTotal, Vec_Int_t * vThis )
+{
+ double TotalScore = 0;
+ int i, Total, This;
+ assert( Vec_IntSize(vTotal) == Vec_IntSize(vThis) );
+ Vec_IntForEachEntryTwo( vTotal, vThis, Total, This, i )
+ {
+ if ( Total == 0 )
+ Total = 1;
+ TotalScore += 1000.0*This/Total;
+ }
+ return TotalScore == 0 ? 1.0 : TotalScore/Gia_ManAndNum(p);
+}
+int Gia_SimQualityPatternsMax( Gia_Man_t * p, Vec_Int_t * vPat, int Iter, int fVerbose, Vec_Int_t * vStats )
+{
+ int k, MaxIn = -1;
+ Vec_Int_t * vTries = Vec_IntAlloc( 100 );
+ Vec_Int_t * vRes = Gia_SimQualityOne( p, vPat, 0 );
+ double Value, InitValue, MaxValue = InitValue = Gia_SimComputeScore( p, vStats, vRes );
+ Vec_IntFree( vRes );
+
+ if ( fVerbose )
+ printf( "Iter %5d : Init = %6.3f ", Iter, InitValue );
+
+ for ( k = 0; k < Gia_ManCiNum(p); k++ )
+ {
+ Vec_IntArray(vPat)[k] ^= 1;
+ //Vec_IntPrint( vPat );
+
+ vRes = Gia_SimQualityOne( p, vPat, 0 );
+ Value = Gia_SimComputeScore( p, vStats, vRes );
+ if ( MaxValue <= Value )
+ {
+ if ( MaxValue < Value )
+ Vec_IntClear( vTries );
+ Vec_IntPush( vTries, k );
+ MaxValue = Value;
+ MaxIn = k;
+ }
+ Vec_IntFree( vRes );
+
+ Vec_IntArray(vPat)[k] ^= 1;
+ }
+ MaxIn = Vec_IntSize(vTries) ? Vec_IntEntry( vTries, rand()%Vec_IntSize(vTries) ) : -1;
+ if ( fVerbose )
+ {
+ printf( "Final = %6.3f Ratio = %4.2f Tries = %5d ", MaxValue, MaxValue/InitValue, Vec_IntSize(vTries) );
+ printf( "Choosing %5d\r", MaxIn );
+ }
+ Vec_IntFree( vTries );
+ return MaxIn;
+}
+Vec_Int_t * Gia_ManPatCollectOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords )
+{
+ Vec_Int_t * vPat = Vec_IntAlloc( Gia_ManCiNum(p) ); int k;
+ for ( k = 0; k < Gia_ManCiNum(p); k++ )
+ Vec_IntPush( vPat, Abc_TtGetBit( Vec_WrdEntryP(vPatterns, k*nWords), n ) );
+ return vPat;
+}
+void Gia_ManPatUpdateOne( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int n, int nWords, Vec_Int_t * vPat )
+{
+ int k, Value;
+ Vec_IntForEachEntry( vPat, Value, k )
+ {
+ word * pSim = Vec_WrdEntryP( vPatterns, k*nWords );
+ if ( Abc_TtGetBit(pSim, n) != Value )
+ Abc_TtXorBit( pSim, n );
+ }
+}
+void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose )
+{
+ int n, k, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+ double InitValue, InitTotal = 0, FinalValue, FinalTotal = 0;
+ Vec_Int_t * vPat, * vRes, * vStats = Gia_SimGenerateStats( p );
+ Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
+ Abc_Random(1);
+ for ( n = 0; n < 64*nWords; n++ )
+ {
+ abctime clk = Abc_Clock();
+// if ( n == 32 )
+// break;
+
+ vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
+ vRes = Gia_SimQualityOne( p, vPat, 0 );
+ InitValue = Gia_SimComputeScore(p, vStats, vRes);
+ InitTotal += InitValue;
+ Vec_IntFree( vRes );
+
+ for ( k = 0; k < 100; k++ )
+ {
+ int MaxIn = Gia_SimQualityPatternsMax( p, vPat, k, fVerbose, vStats );
+ if ( MaxIn == -1 )
+ break;
+ assert( MaxIn >= 0 && MaxIn < Gia_ManCiNum(p) );
+ Vec_IntArray(vPat)[MaxIn] ^= 1;
+ }
+ //Vec_IntPrint( vPat );
+
+ vRes = Gia_SimQualityOne( p, vPat, 0 );
+ FinalValue = Gia_SimComputeScore(p, vStats, vRes);
+ FinalTotal += FinalValue;
+ Vec_IntFree( vRes );
+
+ if ( fVerbose )
+ {
+ printf( "Pat %5d : Tries = %5d InitValue = %6.3f FinalValue = %6.3f Ratio = %4.2f ",
+ n, k, InitValue, FinalValue, FinalValue/InitValue );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+
+ Gia_ManPatUpdateOne( p, vPatterns, n, nWords, vPat );
+ Vec_IntFree( vPat );
+ }
+ Vec_IntFree( vStats );
+ if ( fVerbose )
+ printf( "\n" );
+ printf( "Improved %d patterns with average init value %.2f and average final value %.2f.\n",
+ 64*nWords, 1.0*InitTotal/(64*nWords), 1.0*FinalTotal/(64*nWords) );
+ p->vSimsPi = vPatterns;
+}
+
+/**Function*************************************************************
+
+ Synopsis [Improving quality of simulation patterns.]
+
+ Description []
+
+ SideEffects []
+
+ SeeAlso []
+
+***********************************************************************/
+Vec_Int_t * Gia_SimCollectRare( Gia_Man_t * p, Vec_Wrd_t * vPatterns, int RareLimit )
+{
+ Vec_Int_t * vRareCounts = Vec_IntAlloc( 100 ); // (node, rare_count) pairs
+ int Id, nWords = Vec_WrdSize(vPatterns) / Gia_ManCiNum(p), TotalBits = 64*nWords;
+ Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
+ assert( Vec_WrdSize(vPatterns) % Gia_ManCiNum(p) == 0 );
+ p->vSimsPi = vPatterns;
+ vSims = Gia_ManSimPatSim( p );
+ p->vSimsPi = vTemp;
+ Gia_ManForEachAndId( p, Id )
+ {
+ word * pSim = Vec_WrdEntryP( vSims, Id*nWords );
+ int Count = Abc_TtCountOnesVec( pSim, nWords );
+ int fRareOne = Count < TotalBits/2; // fRareOne is 1 if rare value is 1
+ int CountRare = fRareOne ? Count : TotalBits - Count;
+ assert( CountRare <= TotalBits/2 );
+ if ( CountRare <= RareLimit )
+ Vec_IntPushTwo( vRareCounts, Abc_Var2Lit(Id, fRareOne), CountRare );
+ }
+ Vec_WrdFree( vSims );
+ return vRareCounts;
+}
+Vec_Flt_t * Gia_SimQualityImpact( Gia_Man_t * p, Vec_Int_t * vPat, Vec_Int_t * vRareCounts )
+{
+ Vec_Flt_t * vQuoIncs = Vec_FltStart( Gia_ManCiNum(p) );
+ int nWordsNew = Abc_Bit6WordNum( 1+Gia_ManCiNum(p) );
+ Vec_Wrd_t * vSimsPiNew = Vec_WrdStart( Gia_ManCiNum(p) * nWordsNew );
+ Vec_Wrd_t * vTemp, * vSims;
+ int i, k, Value, RareLit, RareCount;
+ assert( Vec_IntSize(vPat) == Gia_ManCiNum(p) );
+ Vec_IntForEachEntry( vPat, Value, i )
+ {
+ word * pSim = Vec_WrdEntryP( vSimsPiNew, i*nWordsNew );
+ if ( Value )
+ Abc_TtFill( pSim, nWordsNew );
+ Abc_TtXorBit( pSim, i+1 );
+ }
+ vTemp = p->vSimsPi;
+ p->vSimsPi = vSimsPiNew;
+ vSims = Gia_ManSimPatSim( p );
+ p->vSimsPi = vTemp;
+ Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
+ {
+ float Incrm = (float)1.0/(RareCount+1);
+ int RareObj = Abc_Lit2Var(RareLit);
+ int RareVal = Abc_LitIsCompl(RareLit);
+ word * pSim = Vec_WrdEntryP( vSims, RareObj*nWordsNew );
+ int OrigVal = pSim[0] & 1;
+ if ( OrigVal )
+ Abc_TtNot( pSim, nWordsNew );
+ for ( k = 0; k < Gia_ManCiNum(p); k++ )
+ if ( Abc_TtGetBit(pSim, k+1) ) // value changed
+ Vec_FltAddToEntry( vQuoIncs, k, OrigVal != RareVal ? Incrm : -Incrm );
+ }
+ Vec_WrdFree( vSims );
+ Vec_WrdFree( vSimsPiNew );
+ return vQuoIncs;
+}
+Vec_Int_t * Gia_SimCollectBest( Vec_Flt_t * vQuo )
+{
+ Vec_Int_t * vRes; int i;
+ float Value, ValueMax = Vec_FltFindMax( vQuo );
+ if ( ValueMax <= 0 )
+ return NULL;
+ vRes = Vec_IntAlloc( 100 ); // variables with max quo
+ Vec_FltForEachEntry( vQuo, Value, i )
+ if ( Value == ValueMax )
+ Vec_IntPush( vRes, i );
+ return vRes;
+}
+float Gia_ManPatGetQuo( Gia_Man_t * p, Vec_Int_t * vRareCounts, Vec_Wrd_t * vSims, int n, int nWords )
+{
+ float Quality = 0;
+ int RareLit, RareCount, i;
+ assert( Vec_WrdSize(vSims) == Gia_ManObjNum(p) );
+ Vec_IntForEachEntryDouble( vRareCounts, RareLit, RareCount, i )
+ {
+ float Incrm = (float)1.0/(RareCount+1);
+ int RareObj = Abc_Lit2Var(RareLit);
+ int RareVal = Abc_LitIsCompl(RareLit);
+ word * pSim = Vec_WrdEntryP( vSims, RareObj*nWords );
+ if ( Abc_TtGetBit(pSim, n) == RareVal )
+ Quality += Incrm;
+ }
+ return Quality;
+}
+float Gia_ManPatGetTotalQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords )
+{
+ float Total = 0; int n;
+ Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
+ Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
+ p->vSimsPi = vPatterns;
+ vSims = Gia_ManSimPatSim( p );
+ p->vSimsPi = vTemp;
+ for ( n = 0; n < 64*nWords; n++ )
+ Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
+ Vec_IntFree( vRareCounts );
+ Vec_WrdFree( vSims );
+ return Total;
+}
+float Gia_ManPatGetOneQuo( Gia_Man_t * p, int RareLimit, Vec_Wrd_t * vPatterns, int nWords, int n )
+{
+ float Total = 0;
+ Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
+ Vec_Wrd_t * vSims, * vTemp = p->vSimsPi;
+ p->vSimsPi = vPatterns;
+ vSims = Gia_ManSimPatSim( p );
+ p->vSimsPi = vTemp;
+ Total += Gia_ManPatGetQuo( p, vRareCounts, vSims, n, nWords );
+ Vec_IntFree( vRareCounts );
+ Vec_WrdFree( vSims );
+ return Total;
+}
+void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose )
+{
+ abctime clk = Abc_Clock();
+ float FinalTotal, InitTotal;
+ int n, nRares = 0, nChanges = 0, nWords = Vec_WrdSize(p->vSimsPi) / Gia_ManCiNum(p);
+ Vec_Wrd_t * vPatterns = p->vSimsPi; p->vSimsPi = NULL;
+ InitTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
+ for ( n = 0; n < 64*nWords; n++ )
+ {
+ abctime clk = Abc_Clock();
+ Vec_Int_t * vRareCounts = Gia_SimCollectRare( p, vPatterns, RareLimit );
+ Vec_Int_t * vPat = Gia_ManPatCollectOne( p, vPatterns, n, nWords );
+ Vec_Flt_t * vQuoIncs = Gia_SimQualityImpact( p, vPat, vRareCounts );
+ Vec_Int_t * vBest = Gia_SimCollectBest( vQuoIncs );
+ if ( fVerbose )
+ {
+ float PatQuo = Gia_ManPatGetOneQuo( p, RareLimit, vPatterns, nWords, n );
+ printf( "Pat %5d : Rare = %4d Cands = %3d Value = %8.3f Change = %8.3f ",
+ n, Vec_IntSize(vRareCounts)/2, vBest ? Vec_IntSize(vBest) : 0,
+ PatQuo, vBest ? Vec_FltEntry(vQuoIncs, Vec_IntEntry(vBest,0)) : 0 );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+ }
+ if ( vBest != NULL )
+ {
+ int VarBest = Vec_IntEntry( vBest, rand()%Vec_IntSize(vBest) );
+ Abc_TtXorBit( Vec_WrdEntryP(vPatterns, VarBest*nWords), n );
+ nChanges++;
+ }
+ nRares = Vec_IntSize(vRareCounts)/2;
+ Vec_IntFree( vRareCounts );
+ Vec_IntFree( vPat );
+ Vec_FltFree( vQuoIncs );
+ Vec_IntFreeP( &vBest );
+ }
+ if ( fVerbose )
+ printf( "\n" );
+ FinalTotal = Gia_ManPatGetTotalQuo( p, RareLimit, vPatterns, nWords );
+ p->vSimsPi = vPatterns;
+
+ printf( "Improved %d out of %d patterns using %d rare nodes: %.2f -> %.2f. ",
+ nChanges, 64*nWords, nRares, InitTotal, FinalTotal );
+ Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+}
+
////////////////////////////////////////////////////////////////////////
/// END OF FILE ///
////////////////////////////////////////////////////////////////////////