Version abc60211

1 files changed, 84 insertions, 41 deletions

diff --git a/src/sat/aig/fraigEngine.c b/src/sat/aig/fraigEngine.c
index 6214bf3b..17468e8f 100644
--- a/src/sat/aig/fraigEngine.c
+++ b/src/sat/aig/fraigEngine.c
@@ -30,6 +30,39 @@
 
 /**Function*************************************************************
 
+  Synopsis    [Simulates all nodes using random simulation for the first time.]
+
+  Description [Assigns the original simulation info and the storage for the
+  future simulation info.]
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
+{
+    Aig_SimInfo_t * pInfoPi, * pInfoAll;
+    assert( !p->pInfo && !p->pInfoTemp );
+    // create random PI info
+    pInfoPi = Aig_SimInfoAlloc( Aig_ManPiNum(p), p->pParam->nPatsRand, 0 );
+    Aig_SimInfoRandom( pInfoPi );
+    // allocate sim info for all nodes
+    pInfoAll = Aig_SimInfoAlloc( Aig_ManNodeNum(p), p->pParam->nPatsRand, 1 );
+    // simulate though the circuit
+    Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
+    // detect classes
+    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
+    Aig_SimInfoFree( pInfoAll );
+    // save simulation info
+    p->pInfo     = pInfoPi;
+    p->pInfoPi   = Aig_SimInfoAlloc( Aig_ManPiNum(p),   Aig_ManPiNum(p)+1,  0 );
+    p->pInfoTemp = Aig_SimInfoAlloc( Aig_ManNodeNum(p), Aig_ManPiNum(p)+1,  1 );
+    p->pPatMask  = Aig_PatternAlloc( Aig_ManPiNum(p)+1 );
+}
+
+/**Function*************************************************************
+
   Synopsis    [Starts the simulation engine for the first time.]
 
   Description [Tries several random patterns and their distance-1 
@@ -43,15 +76,55 @@
 void Aig_EngineSimulateFirst( Aig_Man_t * p )
 {
     Aig_Pattern_t * pPat;
-    int i;
-    assert( Vec_PtrSize(p->vPats) == 0 );
-    for ( i = 0; i < p->nPatsMax; i++ )
+    int i, Counter;
+
+    // simulate the pattern of all zeros
+    pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); 
+    Aig_PatternClean( pPat );
+    Vec_PtrPush( p->vPats, pPat );
+    if ( !Aig_EngineSimulate( p ) )
+        return;
+
+    // simulate the pattern of all ones
+    pPat = Aig_PatternAlloc( Aig_ManPiNum(p) ); 
+    Aig_PatternFill( pPat );
+    Vec_PtrPush( p->vPats, pPat );
+    if ( !Aig_EngineSimulate( p ) )
+        return;
+
+    // simulate random until the number of new patterns is reasonable
+    do {
+        // generate random PI siminfo
+        Aig_SimInfoRandom( p->pInfoPi );
+        // simulate this info
+        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+        // split the classes and collect the new patterns
+        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, NULL );
+        if ( Vec_VecSize(p->vClasses) == 0 )
+            return;
+        // count the number of useful patterns
+        Counter = Aig_PatternCount(p->pPatMask);
+    }
+    while ( Counter > p->nPatsMax/2 );
+
+    // perform targetted simulation
+    for ( i = 0; i < 3; i++ )
     {
-        pPat = Aig_PatternAlloc( Aig_ManPiNum(p) );
-        Aig_PatternRandom( pPat );
-        Vec_PtrPush( p->vPats, pPat );
-        if ( !Aig_EngineSimulate( p ) )
+        assert( Vec_PtrSize(p->vPats) == 0 );
+        // generate random PI siminfo
+        Aig_SimInfoRandom( p->pInfoPi );
+        // simulate this info
+        Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
+        // split the classes and collect the new patterns
+        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
+        if ( Vec_VecSize(p->vClasses) == 0 )
             return;
+        // simulate the remaining patters
+        if ( Vec_PtrSize(p->vPats) > 0 )
+            if ( !Aig_EngineSimulate( p ) )
+                return;
     }
 }
 
@@ -79,51 +152,21 @@ int Aig_EngineSimulate( Aig_Man_t * p )
     {
         // get the pattern and create new siminfo
         pPat = Vec_PtrPop(p->vPats);
+        assert( pPat->nBits == Aig_ManPiNum(p) );
         // create the new siminfo
         Aig_SimInfoFromPattern( p->pInfoPi, pPat );
-        // free the patter
+        // free the pattern
         Aig_PatternFree( pPat );
 
         // simulate this info
         Aig_ManSimulateInfo( p, p->pInfoPi, p->pInfoTemp );
         // split the classes and collect the new patterns
-        Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses );
+        if ( Aig_ManUpdateClasses( p, p->pInfoTemp, p->vClasses, p->pPatMask ) )
+            Aig_ManCollectPatterns( p, p->pInfoTemp, p->pPatMask, p->vPats );
     }
     return Vec_VecSize(p->vClasses) > 0;
 }
 
-/**Function*************************************************************
-
-  Synopsis    [Simulates all nodes using random simulation for the first time.]
-
-  Description [Assigns the original simulation info and the storage for the
-  future simulation info.]
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-void Aig_EngineSimulateRandomFirst( Aig_Man_t * p )
-{
-    Aig_SimInfo_t * pInfoPi, * pInfoAll;
-    assert( !p->pInfo && !p->pInfoTemp );
-    // create random PI info
-    pInfoPi = Aig_SimInfoAlloc( p->vPis->nSize, Aig_BitWordNum(p->pParam->nPatsRand), 0 );
-    Aig_SimInfoRandom( pInfoPi );
-    // allocate sim info for all nodes
-    pInfoAll = Aig_SimInfoAlloc( p->vNodes->nSize, pInfoPi->nWords, 1 );
-    // simulate though the circuit
-    Aig_ManSimulateInfo( p, pInfoPi, pInfoAll );
-    // detect classes
-    p->vClasses = Aig_ManDeriveClassesFirst( p, pInfoAll );
-    Aig_SimInfoFree( pInfoAll );
-    // save simulation info
-    p->pInfo     = pInfoPi;
-    p->pInfoPi   = Aig_SimInfoAlloc( p->vPis->nSize,   Aig_BitWordNum(p->vPis->nSize),  0 );
-    p->pInfoTemp = Aig_SimInfoAlloc( p->vNodes->nSize, Aig_BitWordNum(p->vPis->nSize),  1 );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////