Improving simulation patterns by local search.

3 files changed, 528 insertions, 38 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                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 4498f390..8d93c4fd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -416,7 +416,8 @@ static int Abc_CommandAbc9MLGen              ( Abc_Frame_t * pAbc, int argc, cha
 static int Abc_CommandAbc9MLTest             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9ReadSim            ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9WriteSim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
-static int Abc_CommandAbc9SimPat             ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9PrintSim           ( Abc_Frame_t * pAbc, int argc, char ** argv );
+static int Abc_CommandAbc9GenSim             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SimRsb             ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9Resim              ( Abc_Frame_t * pAbc, int argc, char ** argv );
 static int Abc_CommandAbc9SpecI              ( Abc_Frame_t * pAbc, int argc, char ** argv );
@@ -1131,9 +1132,10 @@ void Abc_Init( Abc_Frame_t * pAbc )
     Cmd_CommandAdd( pAbc, "ABC9",         "&sim3",         Abc_CommandAbc9Sim3,         0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mlgen",        Abc_CommandAbc9MLGen,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&mltest",       Abc_CommandAbc9MLTest,       0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&read_sim",     Abc_CommandAbc9ReadSim,      0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&write_sim",    Abc_CommandAbc9WriteSim,     0 );
-    Cmd_CommandAdd( pAbc, "ABC9",         "&simpat",       Abc_CommandAbc9SimPat,       0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_read",     Abc_CommandAbc9ReadSim,      0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_write",    Abc_CommandAbc9WriteSim,     0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_print",    Abc_CommandAbc9PrintSim,     0 );
+    Cmd_CommandAdd( pAbc, "ABC9",         "&sim_gen",      Abc_CommandAbc9GenSim,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&simrsb",       Abc_CommandAbc9SimRsb,       0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&resim",        Abc_CommandAbc9Resim,        0 );
     Cmd_CommandAdd( pAbc, "ABC9",         "&speci",        Abc_CommandAbc9SpecI,        0 );
@@ -32832,13 +32834,6 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     pArgvNew = argv + globalUtilOptind;
     nArgcNew = argc - globalUtilOptind;
-    if ( nArgcNew == 0 )
-    {
-        Gia_ManRandom( 1 );
-        pAbc->pGia->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pAbc->pGia) * nWords );
-        printf( "Generated %d random patterns (%d 64-bit words) for each input of the AIG.\n", 64*nWords, nWords );
-        return 0;
-    }
     if ( nArgcNew != 1 )
     {
         Abc_Print( -1, "File name is not given on the command line.\n" );
@@ -32875,7 +32870,7 @@ int Abc_CommandAbc9ReadSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &read_sim [-W num] [-ovh] <file>\n" );
+    Abc_Print( -2, "usage: &sim_read [-W num] [-ovh] <file>\n" );
     Abc_Print( -2, "\t         reads simulation patterns from file\n" );
     Abc_Print( -2, "\t-W num : the number of words to simulate [default = %d]\n", nWords );
     Abc_Print( -2, "\t-o     : toggle reading output information [default = %s]\n", fOutputs? "yes": "no" );
@@ -32954,7 +32949,7 @@ int Abc_CommandAbc9WriteSim( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &write_sim [-vh] <file>\n" );
+    Abc_Print( -2, "usage: &sim_write [-vh] <file>\n" );
     Abc_Print( -2, "\t         writes simulation patterns into a file\n" );
     Abc_Print( -2, "\t-o     : toggle writing output information [default = %s]\n", fOutputs? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
@@ -32974,12 +32969,69 @@ usage:
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
+int Abc_CommandAbc9PrintSim( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern void Gia_ManSimPat( Gia_Man_t * pGia, int nWords, int fVerbose );
-    int c, nWords = 4, fVerbose = 0;
+    extern void Gia_ManSimProfile( Gia_Man_t * pGia );
+    int c, fVerbose = 0;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "Wvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "vh" ) ) != EOF )
+    {
+        switch ( c )
+        {
+        case 'v':
+            fVerbose ^= 1;
+            break;
+        case 'h':
+            goto usage;
+        default:
+            goto usage;
+        }
+    }
+    if ( pAbc->pGia == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9PrintSim(): There is no AIG.\n" );
+        return 1;
+    }
+    if ( Gia_ManRegNum(pAbc->pGia) > 0 )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9PrintSim(): This command works only for combinational AIGs.\n" );
+        return 0;
+    }
+    if ( pAbc->pGia->vSimsPi == NULL )
+    {
+        Abc_Print( -1, "Abc_CommandAbc9PrintSim(): Simulation patterns are not defined.\n" );
+        return 0;
+    }
+    Gia_ManSimProfile( pAbc->pGia );
+    return 0;
+
+usage:
+    Abc_Print( -2, "usage: &sim_print [-vh]\n" );
+    Abc_Print( -2, "\t         writes simulation patterns into a file\n" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "\t-h     : print the command usage\n");
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Abc_CommandAbc9GenSim( Abc_Frame_t * pAbc, int argc, char ** argv )
+{
+    extern void Gia_ManPatSatImprove( Gia_Man_t * pGia, int nWords, int fVerbose );
+    extern void Gia_ManPatDistImprove( Gia_Man_t * p, int fVerbose );
+    extern void Gia_ManPatRareImprove( Gia_Man_t * p, int RareLimit, int fVerbose );
+    int c, nWords = 4, nRare = -1, fDist = 0, fSatBased = 0, fVerbose = 0;
+    Extra_UtilGetoptReset();
+    while ( ( c = Extra_UtilGetopt( argc, argv, "WRsdvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -32994,6 +33046,23 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( nWords < 0 )
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            nRare = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( nRare < 0 )
+                goto usage;
+            break;
+        case 's':
+            fSatBased ^= 1;
+            break;
+        case 'd':
+            fDist ^= 1;
+            break;
         case 'v':
             fVerbose ^= 1;
             break;
@@ -33005,27 +33074,59 @@ int Abc_CommandAbc9SimPat( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
     if ( pAbc->pGia == NULL )
     {
-        Abc_Print( -1, "Abc_CommandAbc9SimPat(): There is no AIG.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9GenSim(): There is no AIG.\n" );
         return 1;
     }
     if ( Gia_ManRegNum(pAbc->pGia) > 0 )
     {
-        Abc_Print( -1, "Abc_CommandAbc9SimPat(): This command works only for combinational AIGs.\n" );
+        Abc_Print( -1, "Abc_CommandAbc9GenSim(): This command works only for combinational AIGs.\n" );
         return 0;
     }
-    if ( pAbc->pGia->vSimsPi == NULL )
+    if ( fSatBased )
     {
-        Abc_Print( -1, "Abc_CommandAbc9SimPat(): Does not have simulation information available.\n" );
-        return 0;
+        if ( pAbc->pGia->vSimsPi == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
+            return 0;
+        }
+        Gia_ManPatSatImprove( pAbc->pGia, nWords, fVerbose );
+    }
+    else if ( fDist )
+    {
+        if ( pAbc->pGia->vSimsPi == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
+            return 0;
+        }
+        Gia_ManPatDistImprove( pAbc->pGia, fVerbose );
     }
-    Gia_ManSimPat( pAbc->pGia, nWords, fVerbose );
+    else if ( nRare >= 0 )
+    {
+        if ( pAbc->pGia->vSimsPi == NULL )
+        {
+            Abc_Print( -1, "Abc_CommandAbc9GenSim(): Does not have simulation information available.\n" );
+            return 0;
+        }
+        Gia_ManPatRareImprove( pAbc->pGia, nRare, fVerbose );
+    }
+    else
+    {
+        Abc_Random(1);
+        Vec_WrdFreeP( &pAbc->pGia->vSimsPi );
+        pAbc->pGia->vSimsPi = Vec_WrdStartRandom( Gia_ManCiNum(pAbc->pGia) * nWords );
+        printf( "Generated %d random patterns (%d 64-bit data words) for each input of the AIG.\n", 64*nWords, nWords );
+    }
+    Gia_ManSimProfile( pAbc->pGia );
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &simpat [-W num] [-vh]\n" );
-    Abc_Print( -2, "\t         performs simulation of the AIG\n" );
-    Abc_Print( -2, "\t-W num : the number of frames to simulate [default = %d]\n", nWords );
-    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n", fVerbose? "yes": "no" );
+    Abc_Print( -2, "usage: &sim_gen [-WR num] [-sdvh]\n" );
+    Abc_Print( -2, "\t         generates random simulation patterns\n" );
+    Abc_Print( -2, "\t-W num : the number of 64-bit words of simulation info [default = %d]\n",            nWords );
+    Abc_Print( -2, "\t-R num : the rarity parameter used to define scope [default = %d]\n",                nRare );
+    Abc_Print( -2, "\t-s     : toggle using SAT-based improvement of available patterns [default = %s]\n", fSatBased? "yes": "no" );
+    Abc_Print( -2, "\t-d     : toggle using one improvement of available patterns [default = %s]\n",       fDist? "yes": "no" );
+    Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                      fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-h     : print the command usage\n");
     return 1;
 }
@@ -47689,7 +47790,7 @@ int Abc_CommandAbc9Test( Abc_Frame_t * pAbc, int argc, char ** argv )
 //        return 1;
 //    }
 //    Abc_FrameUpdateGia( pAbc, Abc_Procedure(pAbc->pGia) );
-    //Gia_ManStructExperiment( pAbc->pGia );
+//    Gia_SimQualityTest( pAbc->pGia );
     return 0;
 usage:
     Abc_Print( -2, "usage: &test [-FW num] [-svh]\n" );