Experiment with bit-packing.

2 files changed, 372 insertions, 7 deletions

diff --git a/src/aig/aig/aigJust.c b/src/aig/aig/aigJust.c
index c6b3a8c0..87ea8f69 100644
--- a/src/aig/aig/aigJust.c
+++ b/src/aig/aig/aigJust.c
@@ -230,6 +230,13 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi
     return Aig_ObjTerSimulate_rec( pAig, pNode );
 }
 
+
+typedef struct Aig_ManPack_t_ Aig_ManPack_t;
+extern Aig_ManPack_t *        Aig_ManPackStart( Aig_Man_t * pAig );
+extern void                   Aig_ManPackStop( Aig_ManPack_t * p );
+extern void                   Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits );
+extern Vec_Int_t *            Aig_ManPackConstNodes( Aig_ManPack_t * p );
+
 /**Function*************************************************************
 
   Synopsis    [Testing of the framework.]
@@ -241,24 +248,29 @@ int Aig_ObjTerSimulate( Aig_Man_t * pAig, Aig_Obj_t * pNode, Vec_Int_t * vSuppLi
   SeeAlso     []
 
 ***********************************************************************/
-void Aig_ManTerSimulate( Aig_Man_t * pAig )
+void Aig_ManJustExperiment( Aig_Man_t * pAig )
 {
-    Vec_Int_t * vSuppLits;
+    Aig_ManPack_t * pPack;
+    Vec_Int_t * vSuppLits, * vNodes;
     Aig_Obj_t * pObj;
     int i, clk = clock(), Count0 = 0, Count0f = 0, Count1 = 0, Count1f = 0;
     int nTotalLits = 0;
     vSuppLits = Vec_IntAlloc( 100 );
-    Aig_ManForEachPo( pAig, pObj, i )
+    pPack = Aig_ManPackStart( pAig );
+    vNodes = Aig_ManPackConstNodes( pPack );
+//    Aig_ManForEachPo( pAig, pObj, i )
+    Aig_ManForEachNodeVec( pAig, vNodes, pObj, i )
     {
         if ( pObj->fPhase ) // const 1
         {
             if ( Aig_ObjFindSatAssign(pAig, pObj, 0, vSuppLits) )
             {
 //                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL0 );
-                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
-                    printf( "Justification error!\n" );
+//                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL0 )
+//                    printf( "Justification error!\n" );
                 Count0++;
                 nTotalLits += Vec_IntSize(vSuppLits);
+                Aig_ManPackAddPattern( pPack, vSuppLits );
             }
             else
                 Count0f++;
@@ -268,10 +280,11 @@ void Aig_ManTerSimulate( Aig_Man_t * pAig )
             if ( Aig_ObjFindSatAssign(pAig, pObj, 1, vSuppLits) )
             {
 //                assert( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) == AIG_VAL1 );
-                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
-                    printf( "Justification error!\n" );
+//                if ( Aig_ObjTerSimulate(pAig, pObj, vSuppLits) != AIG_VAL1 )
+//                    printf( "Justification error!\n" );
                 Count1++;
                 nTotalLits += Vec_IntSize(vSuppLits);
+                Aig_ManPackAddPattern( pPack, vSuppLits );
             }
             else
                 Count1f++;
@@ -282,6 +295,8 @@ void Aig_ManTerSimulate( Aig_Man_t * pAig )
         Aig_ManPoNum(pAig), Count0, Count0f, Count1, Count1f, 100.0*(Count0+Count1)/Aig_ManPoNum(pAig), 1.0*nTotalLits/(Count0+Count1) );
     Abc_PrintTime( 1, "T", clock() - clk );
     Aig_ManCleanMarkAB( pAig );
+    Aig_ManPackStop( pPack );
+    Vec_IntFree( vNodes );
 }
 
 
diff --git a/src/aig/aig/aigPack.c b/src/aig/aig/aigPack.c
index 8d7b54df..493e4995 100644
--- a/src/aig/aig/aigPack.c
+++ b/src/aig/aig/aigPack.c
@@ -27,6 +27,25 @@ ABC_NAMESPACE_IMPL_START
 ///                        DECLARATIONS                              ///
 ////////////////////////////////////////////////////////////////////////
 
+// resubstitution manager
+typedef struct Aig_ManPack_t_ Aig_ManPack_t;
+struct Aig_ManPack_t_
+{
+    Aig_Man_t *        pAig;        // working manager 
+    Vec_Wrd_t *        vSigns;      // object signatures
+    Vec_Wrd_t *        vPiPats;     // PI assignments
+    Vec_Wrd_t *        vPiCare;     // PI care set
+    int                iPatCur;     // current pattern
+    int                fVerbose;    // verbosiness flag
+    // statistics
+    int                nPatTotal;   // number of all patterns
+    int                nPatSkip;    // number of skipped patterns
+    int                nPatRepeat;  // number of repeated patterns
+};
+
+static inline int Aig_Word6CountOnes( word t )  { return Aig_WordCountOnes( (unsigned)(t >> 32) ) + Aig_WordCountOnes( (unsigned)(t & 0xFFFFFFFF) ); }
+static inline int Aig_Word6HasOneBit( word t )  { return (t & (t-1)) == 0; }
+
 
 ////////////////////////////////////////////////////////////////////////
 ///                     FUNCTION DEFINITIONS                         ///
@@ -43,7 +62,338 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+Aig_ManPack_t * Aig_ManPackAlloc( Aig_Man_t * pAig )
+{
+    Aig_ManPack_t * p;
+    p = ABC_CALLOC( Aig_ManPack_t, 1 );
+    p->pAig    = pAig;
+    p->vSigns  = Vec_WrdStart( Aig_ManObjNumMax(pAig) );
+    p->vPiPats = Vec_WrdStart( Aig_ManPiNum(pAig) );
+    p->vPiCare = Vec_WrdStart( Aig_ManPiNum(pAig) );
+    p->iPatCur = 1;
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ManPackCountCares( Aig_ManPack_t * p )
+{
+    Aig_Obj_t * pObj;
+    int i, Total = 0;
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        Total += Aig_Word6CountOnes( Vec_WrdEntry(p->vPiCare, i) );
+    return Total;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackPrintCare( Aig_ManPack_t * p )
+{
+    Aig_Obj_t * pObj;
+    word Sign;
+    int i;
+    Aig_ManForEachPi( p->pAig, pObj, i )
+    {
+        Sign = Vec_WrdEntry( p->vPiCare, i );
+        Extra_PrintBinary( stdout, (unsigned *)&Sign, 64 );
+        printf( "\n" );
+    }
+    printf( "\n" );
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackFree( Aig_ManPack_t * p )
+{
+//    Aig_ManPackPrintCare( p );
+    printf( "Patterns: " );
+    printf( "Total = %6d. ",   p->nPatTotal );
+    printf( "Skipped = %6d. ", p->nPatSkip );
+    printf( "Cares = %6.2f %%  ", 100.0*Aig_ManPackCountCares(p)/Aig_ManPiNum(p->pAig)/64 );
+    printf( "\n" );
+    Vec_WrdFree( p->vSigns );
+    Vec_WrdFree( p->vPiPats );
+    Vec_WrdFree( p->vPiCare );
+    ABC_FREE( p );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackSetRandom( Aig_ManPack_t * p )
+{
+    Aig_Obj_t * pObj;
+    word Sign;
+    int i;
+    Aig_ManForEachPi( p->pAig, pObj, i )
+    {
+        Sign = (((word)Aig_ManRandom(0)) << 32) | ((word)Aig_ManRandom(0));
+        Vec_WrdWriteEntry( p->vPiPats, i, Sign << 1 );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackSimulate( Aig_ManPack_t * p )
+{
+    Aig_Obj_t * pObj;
+    word Sign, Sign0, Sign1;
+    int i;
+    // set the constant
+    Vec_WrdWriteEntry( p->vSigns, 0, (word)~0 );
+    // transfer into the array
+    Aig_ManForEachPi( p->pAig, pObj, i )
+        Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Vec_WrdEntry(p->vPiPats, i) );
+    // simulate internal nodes
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        Sign0 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId0(pObj) );
+        Sign1 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId1(pObj) );
+        if ( Aig_ObjFaninC0(pObj) && Aig_ObjFaninC1(pObj) )
+            Sign = ~(Sign0 | Sign1);
+        else if ( Aig_ObjFaninC0(pObj) )
+            Sign = ~Sign0 &  Sign1;
+        else if ( Aig_ObjFaninC1(pObj) )
+            Sign =  Sign0 & ~Sign1;
+        else
+            Sign =  Sign0 &  Sign1;
+        Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Sign );
+    }
+    // set the outputs
+    Aig_ManForEachPo( p->pAig, pObj, i )
+    {
+        Sign0 = Vec_WrdEntry( p->vSigns, Aig_ObjFaninId0(pObj) );
+        Sign  = Aig_ObjFaninC0(pObj) ? ~Sign0 : Sign0;
+        Vec_WrdWriteEntry( p->vSigns, Aig_ObjId(pObj), Sign );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
 
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackPrintStats( Aig_ManPack_t * p )
+{
+    word Sign;
+    Aig_Obj_t * pObj;
+    int i, Total, Count, Counts[33] = {0}; // the number of nodes having that many patterns
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        Sign  = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) );
+        Count = Aig_Word6CountOnes( Sign );
+        if ( Count > 32 )
+            Count = 64 - Count;
+        Counts[Count]++;        
+    }
+    // print statistics
+    Total = 0;
+    for ( i = 0; i <= 32; i++ )
+    {
+        Total += Counts[i];
+        printf( "%2d : ", i );
+        printf( "%6d  ", Counts[i] );
+        printf( "%6.1f %%", 100.0*Counts[i]/Aig_ManNodeNum(p->pAig) );
+        printf( "%6.1f %%", 100.0*Total/Aig_ManNodeNum(p->pAig) );
+        printf( "\n" );
+    }
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Vec_Int_t * Aig_ManPackConstNodes( Aig_ManPack_t * p )
+{
+    Vec_Int_t * vNodes;
+    Aig_Obj_t * pObj;
+    word Sign;
+    int i;
+    vNodes = Vec_IntAlloc( 1000 );
+    Aig_ManForEachNode( p->pAig, pObj, i )
+    {
+        Sign  = Vec_WrdEntry( p->vSigns, Aig_ObjId(pObj) );
+        if ( Sign == 0 || ~Sign == 0 || Aig_Word6HasOneBit(Sign) || Aig_Word6HasOneBit(~Sign) )
+            Vec_IntPush( vNodes, Aig_ObjId(pObj) );
+    }
+    return vNodes;
+}
+
+
+/**Function*************************************************************
+
+  Synopsis    [Packs patterns into array of simulation info.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+*************************************`**********************************/
+int Aig_ManPackAddPatternTry( Aig_ManPack_t * p, int iBit, Vec_Int_t * vLits )
+{
+    word * pInfo, * pPres;
+    int i, Lit;
+    Vec_IntForEachEntry( vLits, Lit, i )
+    {
+        pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
+        pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
+        if ( Aig_InfoHasBit( (unsigned *)pPres, iBit ) && 
+             Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
+             return 0;
+    }
+    Vec_IntForEachEntry( vLits, Lit, i )
+    {
+        pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
+        pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
+        Aig_InfoSetBit( (unsigned *)pPres, iBit );
+        if ( Aig_InfoHasBit( (unsigned *)pInfo, iBit ) == Aig_LitIsCompl(Lit) )
+             Aig_InfoXorBit( (unsigned *)pInfo, iBit );
+    }
+    return 1;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackAddPattern( Aig_ManPack_t * p, Vec_Int_t * vLits )
+{
+    int k;
+    for ( k = 1; k < 64; k++ )
+        if ( Aig_ManPackAddPatternTry( p, k, vLits ) )
+            break;
+    if ( k == 64 )
+    {
+/*
+        word * pInfo, * pPres;
+        int i, Lit;
+        Vec_IntForEachEntry( vLits, Lit, i )
+            printf( "%d", Aig_LitIsCompl(Lit) );
+        printf( "\n\n" );
+        for ( k = 1; k < 64; k++ )
+        {
+            Vec_IntForEachEntry( vLits, Lit, i )
+            {
+                pInfo = Vec_WrdEntryP( p->vPiPats, Aig_Lit2Var(Lit) );
+                pPres = Vec_WrdEntryP( p->vPiCare, Aig_Lit2Var(Lit) );
+                if ( Aig_InfoHasBit( (unsigned *)pPres, k ) )
+                    printf( "%d", Aig_InfoHasBit( (unsigned *)pInfo, k ) );
+                else
+                    printf( "-" );
+            }
+            printf( "\n" );
+        }
+*/
+        p->nPatSkip++;
+    }
+    p->nPatTotal++;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_ManPack_t * Aig_ManPackStart( Aig_Man_t * pAig )
+{
+    Aig_ManPack_t * p;
+    p = Aig_ManPackAlloc( pAig );
+    Aig_ManPackSetRandom( p );
+    Aig_ManPackSimulate( p );
+    Aig_ManPackPrintStats( p );
+    return p;
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_ManPackStop( Aig_ManPack_t * p )
+{
+    Aig_ManPackSimulate( p );
+    Aig_ManPackPrintStats( p );
+    Aig_ManPackFree( p );
+}
 
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///