Version abc70818

src/aig/fra/fra.h

@@ -49,8 +49,9 @@ extern "C" {
 ////////////////////////////////////////////////////////////////////////
 
 typedef struct Fra_Par_t_   Fra_Par_t;
-typedef struct Fra_Cla_t_   Fra_Cla_t;
 typedef struct Fra_Man_t_   Fra_Man_t;
+typedef struct Fra_Cla_t_   Fra_Cla_t;
+typedef struct Fra_Sml_t_   Fra_Sml_t;
 
 // FRAIG parameters
 struct Fra_Par_t_
@@ -72,6 +73,7 @@ struct Fra_Par_t_
     int              nFramesK;          // the number of timeframes to unroll
     int              fRewrite;          // use rewriting for constraint reduction
     int              fLatchCorr;        // computes latch correspondence only
+    int              fUseImps;          // use implications
 };
 
 // FRAIG equivalence classes
@@ -88,6 +90,19 @@ struct Fra_Cla_t_
     Vec_Ptr_t *      vClassNew;         // new equivalence class(es) after splitting
     int              nPairs;            // the number of pairs of nodes
     int              fRefinement;       // set to 1 when refinement has happened
+    Vec_Int_t *      vImps;             // implications
+};
+
+// simulation manager
+struct Fra_Sml_t_
+{
+    Aig_Man_t *      pAig;              // the original AIG manager
+    int              nFrames;           // the number of times frames
+    int              nWordsFrame;       // the number of words in each time frame
+    int              nWordsTotal;       // the total number of words at a node
+    int              nSimRounds;        // statistics
+    int              timeSim;           // statistics
+    unsigned         pData[0];          // simulation data for the nodes
 };
 
 // FRAIG manager
@@ -101,17 +116,14 @@ struct Fra_Man_t_
     // mapping AIG into FRAIG
     int              nFramesAll;        // the number of timeframes used
     Aig_Obj_t **     pMemFraig;         // memory allocated for points to the fraig nodes
+    // equivalence classes 
+    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
     // simulation info
-    void *           pSim;              // the simulation manager
-    unsigned *       pSimWords;         // memory for simulation information
-    int              nSimWords;         // the number of simulation words
+    Fra_Sml_t *      pSml;              // simulation manager
     // counter example storage
     int              nPatWords;         // the number of words in the counter example
     unsigned *       pPatWords;         // the counter example
-    int *            pPatScores;        // the scores of each pattern
-    // equivalence classes 
-    Fra_Cla_t *      pCla;              // representation of (candidate) equivalent nodes
-    // equivalence checking
+    // satisfiability solving
     sat_solver *     pSat;              // SAT solver
     int              nSatVars;          // the number of variables currently used
     Vec_Ptr_t *      vPiVars;           // the PIs of the cone used 
@@ -140,6 +152,8 @@ struct Fra_Man_t_
     int              nSpeculs;   
     int              nChoices;
     int              nChoicesFake;
+    int              nSatCallsRecent;
+    int              nSatCallsSkipped;
     // runtime
     int              timeSim;
     int              timeTrav;
@@ -158,8 +172,8 @@ struct Fra_Man_t_
 ///                      MACRO DEFINITIONS                           ///
 ////////////////////////////////////////////////////////////////////////
 
-static inline unsigned *   Fra_ObjSim( Aig_Obj_t * pObj )   { return ((Fra_Man_t *)pObj->pData)->pSimWords + ((Fra_Man_t *)pObj->pData)->nSimWords * pObj->Id;   }
-static inline unsigned     Fra_ObjRandomSim()               { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
+static inline unsigned *   Fra_ObjSim( Fra_Sml_t * p, int Id )                           { return p->pData + p->nWordsTotal * Id; }
+static inline unsigned     Fra_ObjRandomSim()                                            { return (rand() << 24) ^ (rand() << 12) ^ rand();                                                   }
 
 static inline Aig_Obj_t *  Fra_ObjFraig( Aig_Obj_t * pObj, int i )                       { return ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i];  }
 static inline void         Fra_ObjSetFraig( Aig_Obj_t * pObj, int i, Aig_Obj_t * pNode ) { ((Fra_Man_t *)pObj->pData)->pMemFraig[((Fra_Man_t *)pObj->pData)->nFramesAll*pObj->Id + i] = pNode; }
@@ -196,6 +210,7 @@ extern int                 Fra_ClassesCountLits( Fra_Cla_t * p );
 extern int                 Fra_ClassesCountPairs( Fra_Cla_t * p );
 extern void                Fra_ClassesTest( Fra_Cla_t * p, int Id1, int Id2 );
 extern void                Fra_ClassesLatchCorr( Fra_Man_t * p );
+extern void                Fra_ClassesPostprocess( Fra_Cla_t * p );
 /*=== fraCnf.c ========================================================*/
 extern void                Fra_NodeAddToSolver( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
 /*=== fraCore.c ========================================================*/
@@ -203,9 +218,14 @@ extern Aig_Man_t *         Fra_FraigPerform( Aig_Man_t * pManAig, Fra_Par_t * pP
 extern Aig_Man_t *         Fra_FraigChoice( Aig_Man_t * pManAig );
 extern void                Fra_FraigSweep( Fra_Man_t * pManAig );
 extern int                 Fra_FraigMiterStatus( Aig_Man_t * p );
-/*=== fraDfs.c ========================================================*/
+/*=== fraImp.c ========================================================*/
+extern Vec_Int_t *         Fra_ImpDerive( Fra_Man_t * p, int nImpMaxLimit, int nImpUseLimit, int fLatchCorr );
+extern void                Fra_ImpAddToSolver( Fra_Man_t * p, Vec_Int_t * vImps, int * pSatVarNums );
+extern int                 Fra_ImpCheckForNode( Fra_Man_t * p, Vec_Int_t * vImps, Aig_Obj_t * pNode, int Pos );
+extern int                 Fra_ImpRefineUsingCex( Fra_Man_t * p, Vec_Int_t * vImps );
+extern void                Fra_ImpCompactArray( Vec_Int_t * vImps );
 /*=== fraInd.c ========================================================*/
-extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter );
+extern Aig_Man_t *         Fra_FraigInduction( Aig_Man_t * p, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter );
 /*=== fraMan.c ========================================================*/
 extern void                Fra_ParamsDefault( Fra_Par_t * pParams );
 extern void                Fra_ParamsDefaultSeq( Fra_Par_t * pParams );
@@ -217,6 +237,7 @@ extern void                Fra_ManStop( Fra_Man_t * p );
 extern void                Fra_ManPrint( Fra_Man_t * p );
 /*=== fraSat.c ========================================================*/
 extern int                 Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew );
+extern int                 Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR );
 extern int                 Fra_NodeIsConst( Fra_Man_t * p, Aig_Obj_t * pNew );
 /*=== fraSec.c ========================================================*/
 extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbose, int fVeryVerbose );
@@ -224,10 +245,15 @@ extern int                 Fra_FraigSec( Aig_Man_t * p, int nFrames, int fVerbos
 extern int                 Fra_NodeHasZeroSim( Aig_Obj_t * pObj );
 extern int                 Fra_NodeCompareSims( Aig_Obj_t * pObj0, Aig_Obj_t * pObj1 );
 extern unsigned            Fra_NodeHashSims( Aig_Obj_t * pObj );
-extern void                Fra_SavePattern( Fra_Man_t * p );
-extern void                Fra_Simulate( Fra_Man_t * p, int fInit );
-extern void                Fra_Resimulate( Fra_Man_t * p );
 extern int                 Fra_CheckOutputSims( Fra_Man_t * p );
+extern void                Fra_SavePattern( Fra_Man_t * p );
+extern void                Fra_SmlSimulate( Fra_Man_t * p, int fInit );
+extern void                Fra_SmlResimulate( Fra_Man_t * p );
+extern Fra_Sml_t *         Fra_SmlStart( Aig_Man_t * pAig, int nFrames, int nWordsFrame );
+extern void                Fra_SmlStop( Fra_Sml_t * p );
+extern Fra_Sml_t *         Fra_SmlSimulateSeq( Aig_Man_t * pAig, int nFrames, int nWords );
+extern Fra_Sml_t *         Fra_SmlSimulateComb( Aig_Man_t * pAig, int nWords );
+
 
 #ifdef __cplusplus
 }

src/aig/fra/fraClass.c

@@ -90,6 +90,7 @@ void Fra_ClassesStop( Fra_Cla_t * p )
     if ( p->vClassOld )    Vec_PtrFree( p->vClassOld );
     if ( p->vClasses1 )    Vec_PtrFree( p->vClasses1 );
     if ( p->vClasses )     Vec_PtrFree( p->vClasses );
+    if ( p->vImps )        Vec_IntFree( p->vImps );
     free( p );
 }
 
@@ -597,6 +598,93 @@ void Fra_ClassesLatchCorr( Fra_Man_t * p )
     p->pCla->pMemClassesFree = p->pCla->pMemClasses + 2*nEntries;
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Counts the number of 1s in the XOR of simulation data.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+static inline int Fra_SmlNodeNotEquWeight( Fra_Sml_t * p, int Left, int Right )
+{
+    unsigned * pSimL, * pSimR;
+    int k, Counter = 0;
+    pSimL = Fra_ObjSim( p, Left );
+    pSimR = Fra_ObjSim( p, Right );
+    for ( k = 0; k < p->nWordsTotal; k++ )
+        Counter += Aig_WordCountOnes( pSimL[k] ^ pSimR[k] );
+    return Counter;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Postprocesses the classes by removing half of the less useful.]
+
+  Description []
+               
+  SideEffects [] 
+
+  SeeAlso     []
+
+***********************************************************************/
+void Fra_ClassesPostprocess( Fra_Cla_t * p )
+{
+    int Ratio = 2;
+    Fra_Sml_t * pComb;
+    Aig_Obj_t * pObj, * pRepr, ** ppClass;
+    int * pWeights, WeightMax = 0, i, k, c;
+    // perform combinational simulation
+    pComb = Fra_SmlSimulateComb( p->pAig, 32 );
+    // compute the weight of each node in the classes
+    pWeights = ALLOC( int, Aig_ManObjIdMax(p->pAig) + 1 );
+    memset( pWeights, 0, sizeof(int) * (Aig_ManObjIdMax(p->pAig) + 1) );
+    Aig_ManForEachObj( p->pAig, pObj, i )
+    { 
+        pRepr = Fra_ClassObjRepr( pObj );
+        if ( pRepr == NULL )
+            continue;
+        pWeights[i] = Fra_SmlNodeNotEquWeight( pComb, pRepr->Id, pObj->Id );
+        WeightMax = AIG_MAX( WeightMax, pWeights[i] );
+    }
+    Fra_SmlStop( pComb );
+    printf( "Before: Const = %6d. Class = %6d.  ", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
+    // remove nodes from classes whose weight is less than WeightMax/Ratio
+    k = 0;
+    Vec_PtrForEachEntry( p->vClasses1, pObj, i )
+    {
+        if ( pWeights[pObj->Id] >= WeightMax/Ratio )
+            Vec_PtrWriteEntry( p->vClasses1, k++, pObj );
+        else
+            Fra_ClassObjSetRepr( pObj, NULL );
+    }
+    Vec_PtrShrink( p->vClasses1, k );
+    // in each class, compact the nodes
+    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+    {
+        k = 1;
+        for ( c = 1; ppClass[c]; c++ )
+        {
+            if ( pWeights[ppClass[c]->Id] >= WeightMax/Ratio )
+                ppClass[k++] = ppClass[c];
+            else
+                Fra_ClassObjSetRepr( ppClass[c], NULL );
+        }
+        ppClass[k] = NULL;
+    }
+    // remove classes with only repr
+    k = 0;
+    Vec_PtrForEachEntry( p->vClasses, ppClass, i )
+        if ( ppClass[1] != NULL )
+            Vec_PtrWriteEntry( p->vClasses, k++, ppClass );
+    Vec_PtrShrink( p->vClasses, k );
+    printf( "After: Const = %6d. Class = %6d. \n", Vec_PtrSize(p->vClasses1), Vec_PtrSize(p->vClasses) );
+    free( pWeights );
+}
+
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////

src/aig/fra/fraCore.c

@@ -142,7 +142,10 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     pObjReprFraig = Fra_ObjFraig( pObjRepr, p->pPars->nFramesK );
     // if the fraiged nodes are the same, return
     if ( Aig_Regular(pObjFraig) == Aig_Regular(pObjReprFraig) )
+    {
+        p->nSatCallsSkipped++;
         return;
+    }
     assert( p->pPars->nFramesK || Aig_Regular(pObjFraig) != Aig_ManConst1(p->pManFraig) );
     // if they are proved different, the c-ex will be in p->pPatWords
     RetValue = Fra_NodesAreEquiv( p, Aig_Regular(pObjReprFraig), Aig_Regular(pObjFraig) );
@@ -177,7 +180,7 @@ static inline void Fra_FraigNode( Fra_Man_t * p, Aig_Obj_t * pObj )
     if ( p->vTimeouts )
         Vec_PtrPush( p->vTimeouts, pObj );
     // simulate the counter-example and return the Fraig node
-    Fra_Resimulate( p );
+    Fra_SmlResimulate( p );
     if ( Fra_ClassObjRepr(pObj) == pObjRepr )
         printf( "Fra_FraigNode(): Error in class refinement!\n" );
     assert( Fra_ClassObjRepr(pObj) != pObjRepr );
@@ -198,13 +201,18 @@ void Fra_FraigSweep( Fra_Man_t * p )
 {
     ProgressBar * pProgress;
     Aig_Obj_t * pObj, * pObjNew;
-    int i, k = 0;
-    // duplicate internal nodes
-    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
+    int i, k = 0, Pos = 0;
     // fraig latch outputs
     Aig_ManForEachLoSeq( p->pManAig, pObj, i )
+    {
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->fUseImps )
+            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
+    }
+    if ( p->pPars->fLatchCorr )
+        return;
     // fraig internal nodes
+    pProgress = Extra_ProgressBarStart( stdout, Aig_ManObjIdMax(p->pManAig) );
     Aig_ManForEachNode( p->pManAig, pObj, i )
     {
         Extra_ProgressBarUpdate( pProgress, i, NULL );
@@ -217,6 +225,8 @@ void Fra_FraigSweep( Fra_Man_t * p )
             continue;
         // perform fraiging
         Fra_FraigNode( p, pObj );
+        if ( p->pPars->fUseImps )
+            Pos = Fra_ImpCheckForNode( p, p->pCla->vImps, pObj, Pos );
     }
     Extra_ProgressBarStop( pProgress );
     // try to prove the outputs of the miter
@@ -224,6 +234,9 @@ void Fra_FraigSweep( Fra_Man_t * p )
 //    Fra_MiterStatus( p->pManFraig );
 //    if ( p->pPars->fProve && p->pManFraig->pData == NULL )
 //        Fra_MiterProve( p );
+    // compress implications after processing all of them
+    if ( p->pPars->fUseImps )
+        Fra_ImpCompactArray( p->pCla->vImps );
 }
 
 /**Function*************************************************************
@@ -248,7 +261,8 @@ clk = clock();
     assert( Aig_ManLatchNum(pManAig) == 0 );
     p = Fra_ManStart( pManAig, pPars );
     p->pManFraig = Fra_ManPrepareComb( p );
-    Fra_Simulate( p, 0 );
+    p->pSml = Fra_SmlStart( pManAig, 1, pPars->nSimWords );
+    Fra_SmlSimulate( p, 0 );
     if ( p->pPars->fChoicing )
         Aig_ManReprStart( p->pManFraig, Aig_ManObjIdMax(p->pManAig)+1 );
     // collect initial states

src/aig/fra/fraInd.c

@@ -198,13 +198,14 @@ Aig_Man_t * Fra_FramesWithClasses( Fra_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose, int * pnIter )
+Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose, int * pnIter )
 {
     Fra_Man_t * p;
     Fra_Par_t Pars, * pPars = &Pars; 
     Aig_Obj_t * pObj;
     Cnf_Dat_t * pCnf;
     Aig_Man_t * pManAigNew;
+//    Vec_Int_t * vImps;
     int nIter, i, clk = clock(), clk2;
 
     if ( Aig_ManNodeNum(pManAig) == 0 )
@@ -223,15 +224,26 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
     pPars->fVerbose   = fVerbose;
     pPars->fRewrite   = fRewrite;
     pPars->fLatchCorr = fLatchCorr;
+    pPars->fUseImps   = fUseImps;
 
     // start the fraig manager for this run
     p = Fra_ManStart( pManAig, pPars );
     // derive and refine e-classes using K initialized frames
-//    if ( fLatchCorr )
-//        Fra_ClassesLatchCorr( p );
-//    else
-        Fra_Simulate( p, 1 );
-    // refine e-classes using sequential simulation?
+//    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+//    Fra_SmlSimulate( p, 1 );
+
+    // remember that strange bug: r iscas/blif/s5378.blif    ; st; ssw -F 4; sec -F 10
+    // refine the classes with more simulation rounds
+    p->pSml = Fra_SmlSimulateSeq( pManAig, 32, 2 );  
+    Fra_ClassesPrepare( p->pCla, p->pPars->fLatchCorr );
+//    Fra_ClassesPostprocess( p->pCla );
+    // allocate new simulation manager for simulating counter-examples
+    Fra_SmlStop( p->pSml );
+    p->pSml = Fra_SmlStart( pManAig, pPars->nFramesK + 1, pPars->nSimWords );
+
+    // select the most expressive implications
+    if ( pPars->fUseImps )
+        p->pCla->vImps = Fra_ImpDerive( p, 5000000, 5000, pPars->fLatchCorr );
  
     p->nLitsZero = Vec_PtrSize( p->pCla->vClasses1 );
     p->nLitsBeg  = Fra_ClassesCountLits( p->pCla );
@@ -251,18 +263,13 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         // perform AIG rewriting
         if ( p->pPars->fRewrite )
             Fra_FraigInductionRewrite( p );
-        // report the intermediate results
-        if ( fVerbose )
-        {
-            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  N = %6d. NR = %6d.\n", 
-                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
-                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
-                Aig_ManNodeNum(p->pManAig), Aig_ManNodeNum(p->pManFraig) );
-        }
 
+        // bug:  r iscas/blif/s1238.blif    ; st; ssw -v
         // convert the manager to SAT solver (the last nLatches outputs are inputs)
-//        pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
-        pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        if ( pPars->fUseImps )
+            pCnf = Cnf_DeriveSimple( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
+        else
+            pCnf = Cnf_Derive( p->pManFraig, Aig_ManRegNum(p->pManFraig) );
 //Cnf_DataWriteIntoFile( pCnf, "temp.cnf", 1 );
 
         p->pSat = Cnf_DataWriteIntoSolver( pCnf );
@@ -270,6 +277,12 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         assert( p->pSat != NULL );
         if ( p->pSat == NULL )
             printf( "Fra_FraigInduction(): Computed CNF is not valid.\n" );
+        if ( pPars->fUseImps )
+        {
+            Fra_ImpAddToSolver( p, p->pCla->vImps, pCnf->pVarNums );
+            if ( p->pSat == NULL )
+                printf( "Fra_FraigInduction(): Adding implicationsn to CNF led to a conflict.\n" );
+        }
 
         // set the pointers to the manager
         Aig_ManForEachObj( p->pManFraig, pObj, i )
@@ -295,9 +308,20 @@ Aig_Man_t * Fra_FraigInduction( Aig_Man_t * pManAig, int nFramesK, int fRewrite,
         }
         Cnf_DataFree( pCnf );
 */
+        // report the intermediate results
+        if ( fVerbose )
+        {
+            printf( "%3d : Const = %6d. Class = %6d.  L = %6d. LR = %6d.  I = %6d. NR = %6d.\n", 
+                nIter, Vec_PtrSize(p->pCla->vClasses1), Vec_PtrSize(p->pCla->vClasses), 
+                Fra_ClassesCountLits(p->pCla), p->pManFraig->nAsserts,
+                p->pCla->vImps? Vec_IntSize(p->pCla->vImps) : 0, Aig_ManNodeNum(p->pManFraig) );
+        }
 
         // perform sweeping
+        p->nSatCallsRecent = 0;
+        p->nSatCallsSkipped = 0;
         Fra_FraigSweep( p );
+//        printf( "Recent SAT called = %d. Skipped = %d.\n", p->nSatCallsRecent, p->nSatCallsSkipped );
         assert( p->vTimeouts == NULL );
         if ( p->vTimeouts )
            printf( "Fra_FraigInduction(): SAT solver timed out!\n" );

src/aig/fra/fraMan.c

@@ -77,8 +77,6 @@ void Fra_ParamsDefaultSeq( Fra_Par_t * pPars )
     pPars->fPatScores       =       0;  // enables simulation pattern scoring
     pPars->MaxScore         =      25;  // max score after which resimulation is used
     pPars->fDoSparse        =       1;  // skips sparse functions
-//    pPars->dActConeRatio    =    0.05;  // the ratio of cone to be bumped
-//    pPars->dActConeBumpMax  =     5.0;  // the largest bump of activity
     pPars->dActConeRatio    =     0.3;  // the ratio of cone to be bumped
     pPars->dActConeBumpMax  =    10.0;  // the largest bump of activity
     pPars->nBTLimitNode     =10000000;  // conflict limit at a node
@@ -112,15 +110,9 @@ Fra_Man_t * Fra_ManStart( Aig_Man_t * pManAig, Fra_Par_t * pPars )
     p->pManAig    = pManAig;
     p->nSizeAlloc = Aig_ManObjIdMax( pManAig ) + 1;
     p->nFramesAll = pPars->nFramesK + 1;
-    // allocate simulation info
-    p->nSimWords  = pPars->nSimWords * p->nFramesAll;
-    p->pSimWords  = ALLOC( unsigned, p->nSizeAlloc * p->nSimWords );
-    // clean simulation info of the constant node
-    memset( p->pSimWords, 0, sizeof(unsigned) * p->nSizeAlloc * p->nSimWords );
     // allocate storage for sim pattern
     p->nPatWords  = Aig_BitWordNum( Aig_ManPiNum(pManAig) * p->nFramesAll );
     p->pPatWords  = ALLOC( unsigned, p->nPatWords ); 
-    p->pPatScores = ALLOC( int, 32 * p->nSimWords ); 
     p->vPiVars    = Vec_PtrAlloc( 100 );
     // equivalence classes
     p->pCla       = Fra_ClassesStart( pManAig );
@@ -238,21 +230,20 @@ void Fra_ManFinalizeComb( Fra_Man_t * p )
 void Fra_ManStop( Fra_Man_t * p )
 {
     int i;
+    if ( p->pPars->fVerbose )
+        Fra_ManPrint( p );
     for ( i = 0; i < p->nSizeAlloc; i++ )
         if ( p->pMemFanins[i] && p->pMemFanins[i] != (void *)1 )
             Vec_PtrFree( p->pMemFanins[i] );
-    if ( p->pPars->fVerbose )
-        Fra_ManPrint( p );
     if ( p->vTimeouts ) Vec_PtrFree( p->vTimeouts );
     if ( p->vPiVars )   Vec_PtrFree( p->vPiVars );
     if ( p->pSat )      sat_solver_delete( p->pSat );
     if ( p->pCla  )     Fra_ClassesStop( p->pCla );
+    if ( p->pSml )      Fra_SmlStop( p->pSml );
     FREE( p->pMemFraig );
     FREE( p->pMemFanins );
     FREE( p->pMemSatNums );
-    FREE( p->pPatScores );
     FREE( p->pPatWords );
-    FREE( p->pSimWords );
     free( p );
 }
 
@@ -269,16 +260,16 @@ void Fra_ManStop( Fra_Man_t * p )
 ***********************************************************************/
 void Fra_ManPrint( Fra_Man_t * p )
 {
-    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*((p->nSimWords+2)*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
+    double nMemory = 1.0*Aig_ManObjIdMax(p->pManAig)*(p->pSml->nWordsTotal*sizeof(unsigned)+6*sizeof(void*))/(1<<20);
     printf( "SimWord = %d. Round = %d.  Mem = %0.2f Mb.  LitBeg = %d.  LitEnd = %d. (%6.2f %%).\n", 
-        p->nSimWords, p->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
+        p->pPars->nSimWords, p->pSml->nSimRounds, nMemory, p->nLitsBeg, p->nLitsEnd, 100.0*p->nLitsEnd/p->nLitsBeg );
     printf( "Proof = %d. Cex = %d. Fail = %d. FailReal = %d. Zero = %d. C-lim = %d. Vars = %d.\n", 
         p->nSatProof, p->nSatCallsSat, p->nSatFails, p->nSatFailsReal, p->nLitsZero, p->pPars->nBTLimitNode, p->nSatVars );
     printf( "NBeg = %d. NEnd = %d. (Gain = %6.2f %%).  RBeg = %d. REnd = %d. (Gain = %6.2f %%).\n", 
         p->nNodesBeg, p->nNodesEnd, 100.0*(p->nNodesBeg-p->nNodesEnd)/p->nNodesBeg, 
         p->nRegsBeg, p->nRegsEnd, 100.0*(p->nRegsBeg-p->nRegsEnd)/p->nRegsBeg );
     if ( p->pSat ) Sat_SolverPrintStats( stdout, p->pSat );
-    PRT( "AIG simulation  ", p->timeSim  );
+    PRT( "AIG simulation  ", p->pSml->timeSim  );
     PRT( "AIG traversal   ", p->timeTrav );
     if ( p->timeRwr )
     {

src/aig/fra/fraSat.c

@@ -66,6 +66,7 @@ int Fra_NodesAreEquiv( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew )
     }
 
     p->nSatCalls++;
+    p->nSatCallsRecent++;
 
     // make sure the solver is allocated and has enough variables
     if ( p->pSat == NULL )
@@ -188,6 +189,110 @@ p->timeSatFail += clock() - clk;
 
 /**Function*************************************************************
 
+  Synopsis    [Runs the result of test for pObj => pNew.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Fra_NodesAreImp( Fra_Man_t * p, Aig_Obj_t * pOld, Aig_Obj_t * pNew, int fComplL, int fComplR )
+{
+    int pLits[4], RetValue, RetValue1, nBTLimit, clk, clk2 = clock();
+    int status;
+
+    // make sure the nodes are not complemented
+    assert( !Aig_IsComplement(pNew) );
+    assert( !Aig_IsComplement(pOld) );
+    assert( pNew != pOld );
+
+    // if at least one of the nodes is a failed node, perform adjustments:
+    // if the backtrack limit is small, simply skip this node
+    // if the backtrack limit is > 10, take the quare root of the limit
+    nBTLimit = p->pPars->nBTLimitNode;
+/*
+    if ( !p->pPars->fSpeculate && p->pPars->nFramesK == 0 && (nBTLimit > 0 && (pOld->fMarkB || pNew->fMarkB)) )
+    {
+        p->nSatFails++;
+        // fail immediately
+//        return -1;
+        if ( nBTLimit <= 10 )
+            return -1;
+        nBTLimit = (int)pow(nBTLimit, 0.7);
+    }
+*/
+    p->nSatCalls++;
+
+    // make sure the solver is allocated and has enough variables
+    if ( p->pSat == NULL )
+    {
+        p->pSat = sat_solver_new();
+        p->nSatVars = 1;
+        sat_solver_setnvars( p->pSat, 1000 );
+    }
+
+    // if the nodes do not have SAT variables, allocate them
+    Fra_NodeAddToSolver( p, pOld, pNew );
+
+    if ( p->pSat->qtail != p->pSat->qhead )
+    {
+        status = sat_solver_simplify(p->pSat);
+        assert( status != 0 );
+        assert( p->pSat->qtail == p->pSat->qhead );
+    }
+
+    // prepare variable activity
+    if ( p->pPars->fConeBias )
+        Fra_SetActivityFactors( p, pOld, pNew ); 
+
+    // solve under assumptions
+    // A = 1; B = 0     OR     A = 1; B = 1 
+clk = clock();
+//    pLits[0] = toLitCond( Fra_ObjSatNum(pOld), 0 );
+//    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), pOld->fPhase == pNew->fPhase );
+    pLits[0] = toLitCond( Fra_ObjSatNum(pOld),  fComplL );
+    pLits[1] = toLitCond( Fra_ObjSatNum(pNew), !fComplR );
+//Sat_SolverWriteDimacs( p->pSat, "temp.cnf", pLits, pLits + 2, 1 );
+    RetValue1 = sat_solver_solve( p->pSat, pLits, pLits + 2, 
+        (sint64)nBTLimit, (sint64)0, 
+        p->nBTLimitGlobal, p->nInsLimitGlobal );
+p->timeSat += clock() - clk;
+    if ( RetValue1 == l_False )
+    {
+p->timeSatUnsat += clock() - clk;
+        pLits[0] = lit_neg( pLits[0] );
+        pLits[1] = lit_neg( pLits[1] );
+        RetValue = sat_solver_addclause( p->pSat, pLits, pLits + 2 );
+        assert( RetValue );
+        // continue solving the other implication
+        p->nSatCallsUnsat++;
+    }
+    else if ( RetValue1 == l_True )
+    {
+p->timeSatSat += clock() - clk;
+        Fra_SavePattern( p );
+        p->nSatCallsSat++;
+        return 0;
+    }
+    else // if ( RetValue1 == l_Undef )
+    {
+p->timeSatFail += clock() - clk;
+        // mark the node as the failed node
+        if ( pOld != p->pManFraig->pConst1 ) 
+            pOld->fMarkB = 1;
+        pNew->fMarkB = 1;
+        p->nSatFailsReal++;
+        return -1;
+    }
+    // return SAT proof
+    p->nSatProof++;
+    return 1;
+}
+
+/**Function*************************************************************
+
   Synopsis    [Runs equivalence test for one node.]
 
   Description [Returns the fraiged node.]

src/aig/fra/fraSec.c

@@ -47,7 +47,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
     {
         nFrames = nFramesFix;
         // perform seq sweeping for one frame number
-        pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+        pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
     }
     else
     {
@@ -55,7 +55,7 @@ int Fra_FraigSec( Aig_Man_t * p, int nFramesFix, int fVerbose, int fVeryVerbose
         for ( nFrames = 1; ; nFrames++ )
         {
 clk = clock();
-            pNew = Fra_FraigInduction( p, nFrames, 0, 0, fVeryVerbose, &nIter );
+            pNew = Fra_FraigInduction( p, nFrames, 0, 0, 0, fVeryVerbose, &nIter );
             RetValue = Fra_FraigMiterStatus( pNew );
             if ( fVerbose )
             {

src/base/abci/abc.c

@@ -10974,11 +10974,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     int nFramesK;
     int fExdc;
-    int fImp;
+    int fUseImps;
     int fRewrite;
     int fLatchCorr;
     int fVerbose;
-    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fLatchCorr, int fVerbose );
+    extern Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFrames, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose );
 
     pNtk = Abc_FrameReadNtk(pAbc);
     pOut = Abc_FrameReadOut(pAbc);
@@ -10987,7 +10987,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     nFramesK   = 1;
     fExdc      = 1;
-    fImp       = 0;
+    fUseImps   = 0;
     fRewrite   = 0;
     fLatchCorr = 0;
     fVerbose   = 0;
@@ -11011,7 +11011,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
             fExdc ^= 1;
             break;
         case 'i':
-            fImp ^= 1;
+            fUseImps ^= 1;
             break;
         case 'r':
             fRewrite ^= 1;
@@ -11048,7 +11048,7 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 
     // get the new network
-    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fLatchCorr, fVerbose );
+    pNtkRes = Abc_NtkSeqSweep( pNtk, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose );
     if ( pNtkRes == NULL )
     {
         fprintf( pErr, "Sequential sweeping has failed.\n" );
@@ -11059,11 +11059,11 @@ int Abc_CommandSeqSweep( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    fprintf( pErr, "usage: ssweep [-F num] [-lrvh]\n" );
+    fprintf( pErr, "usage: ssweep [-F num] [-ilrvh]\n" );
     fprintf( pErr, "\t         performs sequential sweep using K-step induction\n" );
     fprintf( pErr, "\t-F num : number of time frames for induction (1=simple) [default = %d]\n", nFramesK );
 //    fprintf( pErr, "\t-e     : toggle writing EXDC network [default = %s]\n", fExdc? "yes": "no" );
-//    fprintf( pErr, "\t-i     : toggle computing implications [default = %s]\n", fImp? "yes": "no" );
+    fprintf( pErr, "\t-i     : toggle using implications [default = %s]\n", fUseImps? "yes": "no" );
     fprintf( pErr, "\t-l     : toggle latch correspondence only [default = %s]\n", fLatchCorr? "yes": "no" );
     fprintf( pErr, "\t-r     : toggle AIG rewriting [default = %s]\n", fRewrite? "yes": "no" );
     fprintf( pErr, "\t-v     : toggle verbose output [default = %s]\n", fVerbose? "yes": "no" );

src/base/abci/abcDar.c

@@ -892,16 +892,26 @@ int Abc_NtkDSat( Abc_Ntk_t * pNtk, sint64 nConfLimit, sint64 nInsLimit, int fVer
   SeeAlso     []
 
 ***********************************************************************/
-Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fLatchCorr, int fVerbose )
+Abc_Ntk_t * Abc_NtkSeqSweep( Abc_Ntk_t * pNtk, int nFramesK, int fRewrite, int fUseImps, int fLatchCorr, int fVerbose )
 {
-    Abc_Ntk_t * pNtkAig;
+    Fraig_Params_t Params;
+    Abc_Ntk_t * pNtkAig, * pNtkFraig;
     Aig_Man_t * pMan, * pTemp;
-    pMan = Abc_NtkToDar( pNtk, 1 );
+
+    // preprocess the miter by fraiging it
+    // (note that for each functional class, fraiging leaves one representative;
+    // so fraiging does not reduce the number of functions represented by nodes
+    Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
+    pNtkFraig = Abc_NtkFraig( pNtk, &Params, 0, 0 );
+//    pNtkFraig = Abc_NtkDup( pNtk );
+
+    pMan = Abc_NtkToDar( pNtkFraig, 1 );
+    Abc_NtkDelete( pNtkFraig );
     if ( pMan == NULL )
         return NULL;
-//    pMan->nRegs = Abc_NtkLatchNum(pNtk);
 
-    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fLatchCorr, fVerbose, NULL );
+    pMan = Fra_FraigInduction( pTemp = pMan, nFramesK, fRewrite, fUseImps, fLatchCorr, fVerbose, NULL );
     Aig_ManStop( pTemp );
 
     if ( Aig_ManRegNum(pMan) < Abc_NtkLatchNum(pNtk) )
@@ -960,6 +970,7 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, int nFrames, int fVerbo
     // (note that for each functional class, fraiging leaves one representative;
     // so fraiging does not reduce the number of functions represented by nodes
     Fraig_ParamsSetDefault( &Params );
+    Params.nBTLimit = 100000;
     pMiter = Abc_NtkFraig( pTemp = pMiter, &Params, 0, 0 );
     Abc_NtkDelete( pTemp );