Adding dump of trivial abstraction map at the beginning in &gla -m.

2 files changed, 82 insertions, 1 deletions

diff --git a/src/opt/sbd/sbd.c b/src/opt/sbd/sbd.c
index 4d86d2ee..5c5b1f2b 100644
--- a/src/opt/sbd/sbd.c
+++ b/src/opt/sbd/sbd.c
@@ -19,6 +19,7 @@
 ***********************************************************************/
 
 #include "sbdInt.h"
+#include "misc/vec/vecHsh.h"
 
 ABC_NAMESPACE_IMPL_START
 
@@ -42,6 +43,68 @@ ABC_NAMESPACE_IMPL_START
   SeeAlso     []
 
 ***********************************************************************/
+int Sbd_CountConfigVars( Vec_Int_t * vSet, int nVars )
+{
+    int i, k, Entry = 0, Entry2, Count = 0, Below;
+    int Prev = Vec_IntEntry( vSet, 0 );
+    Vec_IntForEachEntryStart( vSet, Entry, i, 1 )
+    {
+        assert( 2*Prev >= Entry );
+        if ( 2*Prev == Entry )
+        {
+            Prev = Entry;
+            continue;
+        }
+        Below = nVars; 
+        Vec_IntForEachEntryStart( vSet, Entry2, k, i )
+            Below += Entry2;
+        Count += Below * (2*Prev - 1);
+        Prev = Entry;
+    }
+    Count += nVars * 2*Prev;
+    return Vec_IntSum(vSet) < nVars - 1 ? 0 : Count;
+}
+void Sbd_CountTopos()
+{
+    Hsh_VecMan_t * p = Hsh_VecManStart( 100000 ); // hash table for arrays
+    Vec_Int_t * vSet = Vec_IntAlloc( 100 );
+    int i, k, e, Start, Stop;
+    Start = Hsh_VecManAdd( p, vSet );
+    for ( i = 1; i < 9; i++ )
+    {
+        Stop = Hsh_VecSize( p );
+        for ( e = Start; e < Stop; e++ )
+        {
+            Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+            Vec_IntClear( vSet );
+            Vec_IntAppend( vSet, vTemp );
+            for ( k = 0; k < Vec_IntSize(vSet); k++ )
+            {
+                // skip if the number of entries on this level is equal to the number of fanins on the previous level
+                if ( k ? (Vec_IntEntry(vSet, k) == 2*Vec_IntEntry(vSet, k-1)) : (Vec_IntEntry(vSet, 0) > 0) )
+                    continue;
+                Vec_IntAddToEntry( vSet, k, 1 );
+                Hsh_VecManAdd( p, vSet );
+                Vec_IntAddToEntry( vSet, k, -1 );
+            }
+            Vec_IntPush( vSet, 1 );
+            Hsh_VecManAdd( p, vSet );
+        }
+        printf( "%2d : This = %8d  All = %8d\n", i, Hsh_VecSize(p) - Stop, Hsh_VecSize(p) );
+        if ( 0 )
+        {
+            for ( e = Stop; e < Hsh_VecSize(p); e++ )
+            {
+                Vec_Int_t * vTemp = Hsh_VecReadEntry( p, e );
+                printf( "Params = %3d.  ", Sbd_CountConfigVars(vTemp, 5) );
+                Vec_IntPrint( vTemp );
+            }
+        }
+        Start = Stop;
+    }
+    Vec_IntFree( vSet );
+    Hsh_VecManStop( p );
+}
 
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/abs/absGla.c b/src/proof/abs/absGla.c
index 97a8b644..420adfc3 100644
--- a/src/proof/abs/absGla.c
+++ b/src/proof/abs/absGla.c
@@ -1539,9 +1539,27 @@ int Gia_ManPerformGla( Gia_Man_t * pAig, Abs_Par_t * pPars )
         Abc_Print( 1, "LrnStart = %d  LrnDelta = %d  LrnRatio = %d %%  Skip = %d  SimpleCNF = %d  Dump = %d\n", 
             pPars->nLearnedStart, pPars->nLearnedDelta, pPars->nLearnedPerce, pPars->fUseSkip, pPars->fUseSimple, pPars->fDumpVabs|pPars->fDumpMabs );
         if ( pPars->fDumpVabs || pPars->fDumpMabs )
-            Abc_Print( 1, "%s will be dumped into file \"%s\".\n", 
+            Abc_Print( 1, "%s will be continously dumped into file \"%s\".\n", 
                 pPars->fDumpVabs ? "Abstracted model" : "Miter with abstraction map",
                 Ga2_GlaGetFileName(p, pPars->fDumpVabs) );
+        if ( pPars->fDumpMabs )
+        {
+            // create trivial abstraction map
+            Gia_Obj_t * pObj; 
+            char * pFileName = Ga2_GlaGetFileName(p, 0);
+            Vec_Int_t * vMap = pAig->vGateClasses; pAig->vGateClasses = NULL;
+            pAig->vGateClasses = Vec_IntStart( Gia_ManObjNum(pAig) );
+            Vec_IntWriteEntry( pAig->vGateClasses, 0, 1 );
+            Gia_ManForEachAnd( pAig, pObj, i )
+                Vec_IntWriteEntry( pAig->vGateClasses, i, 1 );
+            Gia_ManForEachRo( pAig, pObj, i )
+                Vec_IntWriteEntry( pAig->vGateClasses, Gia_ObjId(pAig, pObj), 1 );
+            Gia_AigerWrite( pAig, pFileName, 0, 0 );
+            Vec_IntFree( pAig->vGateClasses );
+            pAig->vGateClasses = vMap;
+            if ( p->pPars->fVerbose )
+                Abc_Print( 1, "Dumping miter with abstraction map into file \"%s\"...\n", pFileName );
+        }
         Abc_Print( 1, " Frame   %%   Abs  PPI   FF   LUT   Confl  Cex   Vars   Clas   Lrns     Time        Mem\n" );
     }
     // iterate unrolling