Version abc70127

5 files changed, 20 insertions, 8 deletions

diff --git a/src/opt/res/resCore.c b/src/opt/res/resCore.c
index 6340b175..5f814c3a 100644
--- a/src/opt/res/resCore.c
+++ b/src/opt/res/resCore.c
@@ -200,8 +200,11 @@ p->timeAig += clock() - clk;
 
         if ( p->pPars->fVeryVerbose )
         {
-            printf( "%5d : ", pObj->Id );
-            printf( "Win = %3d/%4d/%3d ", Vec_PtrSize(p->pWin->vLeaves), Vec_VecSizeSize(p->pWin->vLevels), Vec_PtrSize(p->pWin->vRoots) );
+            printf( "%5d (lev=%2d) : ", pObj->Id, pObj->Level );
+            printf( "Win = %3d/%3d/%4d/%3d   ", 
+                Vec_PtrSize(p->pWin->vLeaves) - p->pWin->nLeavesPlus, 
+                p->pWin->nLeavesPlus, Vec_VecSizeSize(p->pWin->vLevels), 
+                Vec_PtrSize(p->pWin->vRoots) );
             printf( "D = %3d ", Vec_PtrSize(p->pWin->vDivs) );
             printf( "D+ = %3d ", p->pWin->nDivsPlus );
             printf( "AIG = %4d ", Abc_NtkNodeNum(p->pAig) );
@@ -242,12 +245,13 @@ p->timeSat += clock() - clk;
 //                printf( " Sat\n" );
                 continue;
             }
+            p->nProvedSets++;
 //            printf( " Unsat\n" );
+            continue;
 
             // write it into a file
 //            Sto_ManDumpClauses( p->pCnf, "trace.cnf" );
 
-            p->nProvedSets++;
 
             // interplate the problem if it was UNSAT
 clk = clock();
diff --git a/src/opt/res/resDivs.c b/src/opt/res/resDivs.c
index a18764ed..bff91983 100644
--- a/src/opt/res/resDivs.c
+++ b/src/opt/res/resDivs.c
@@ -60,6 +60,8 @@ void Res_WinDivisors( Res_Win_t * p, int nLevDivMax )
     // mark the MFFC of the node (does not increment trav ID)
     Res_WinVisitMffc( p );
 
+    // what about the fanouts of the leaves!!!
+
     // go through all the legal levels and check if their fanouts can be divisors
     p->nDivsPlus = 0;
     Vec_VecForEachEntryStartStop( p->vLevels, pObj, i, k, 0, p->nLevDivMax - 1 )
diff --git a/src/opt/res/resInt.h b/src/opt/res/resInt.h
index f5c64f8e..54251722 100644
--- a/src/opt/res/resInt.h
+++ b/src/opt/res/resInt.h
@@ -48,6 +48,7 @@ struct Res_Win_t_
     int              nLevLeaves; // the level where leaves begin
     int              nLevDivMax; // the maximum divisor level
     int              nDivsPlus;  // the number of additional divisors
+    int              nLeavesPlus;// the number of additional leaves
     Abc_Obj_t *      pNode;      // the node in the center
     // the window data
     Vec_Vec_t *      vLevels;    // nodes by level
diff --git a/src/opt/res/resSim.c b/src/opt/res/resSim.c
index 27a6c1f0..81267540 100644
--- a/src/opt/res/resSim.c
+++ b/src/opt/res/resSim.c
@@ -141,12 +141,11 @@ void Res_SimSetRandom( Res_Sim_t * p )
 {
     Abc_Obj_t * pObj;
     unsigned * pInfo;
-    int i, w;
+    int i;
     Abc_NtkForEachPi( p->pAig, pObj, i )
     {
         pInfo = Vec_PtrEntry( p->vPats, pObj->Id );
-        for ( w = 0; w < p->nWords; w++ )
-            pInfo[w] = Abc_InfoRandom();
+        Abc_InfoRandom( pInfo, p->nWords );
     }
 }
 
@@ -478,7 +477,7 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
     // prepare the manager
     Res_SimAdjust( p, pAig );
     // collect 0/1 simulation info
-    for ( Limit = 0; Limit < 100; Limit++ )
+    for ( Limit = 0; Limit < 10; Limit++ )
     {
         Res_SimSetRandom( p );
         Res_SimPerformRound( p );
@@ -489,10 +488,14 @@ int Res_SimPrepare( Res_Sim_t * p, Abc_Ntk_t * pAig )
     }
 //    printf( "%d   ", Limit );
     // report the last set of patterns
-//    Res_SimReportOne( p );
+    Res_SimReportOne( p );
+    printf( "\n" );
     // quit if there is not enough
     if ( p->nPats0 < 4 || p->nPats1 < 4 )
+    {
+//        Res_SimReportOne( p );
         return 0;
+    }
     // create bit-matrix info
     if ( p->nPats0 < p->nPats )
         Res_SimPadSimInfo( p->vPats0, p->nPats0, p->nWords );
diff --git a/src/opt/res/resWin.c b/src/opt/res/resWin.c
index b5fe0641..fa74b219 100644
--- a/src/opt/res/resWin.c
+++ b/src/opt/res/resWin.c
@@ -243,6 +243,7 @@ void Res_WinAddMissing_rec( Res_Win_t * p, Abc_Obj_t * pObj )
         return;
     if ( !Abc_NodeIsTravIdCurrent(pObj) || (int)pObj->Level <= p->nLevLeaves )
     {
+        p->nLeavesPlus++;
         Vec_PtrPush( p->vLeaves, pObj );
         pObj->fMarkA = 1;
         return;
@@ -349,6 +350,7 @@ int Res_WinCompute( Abc_Obj_t * pNode, int nWinTfiMax, int nWinTfoMax, Res_Win_t
     p->pNode = pNode;
     p->nWinTfiMax = nWinTfiMax;
     p->nWinTfoMax = nWinTfoMax;
+    p->nLeavesPlus = 0;
     p->nLevLeaves = ABC_MAX( 0, ((int)p->pNode->Level) - p->nWinTfiMax - 1 );
     // collect the nodes in TFI cone of pNode above the level of leaves (p->nLevLeaves)
     Res_WinCollectNodeTfi( p );