1 files changed, 69 insertions, 50 deletions

diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index b03a248e..8e3ab01a 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -66,65 +66,24 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+Aig_Man_t * Ssw_SignalCorrespondenceRefine( Ssw_Man_t * p )
 {
     Aig_Man_t * pAigNew;
-    Ssw_Man_t * p;
-    int RetValue, nIter, clk, clkTotal = clock();
-    // reset random numbers
-    Aig_ManRandom( 1 );
-
-    // consider the case of empty AIG
-    if ( Aig_ManNodeNum(pAig) == 0 )
-    {
-        pPars->nIters = 0;
-        // Ntl_ManFinalize() needs the following to satisfy an assertion
-        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
-        return Aig_ManDupOrdered(pAig);
-    }
-
-    // check and update parameters
-    assert( Aig_ManRegNum(pAig) > 0 );
-    assert( pPars->nFramesK > 0 );
-    if ( pPars->nFramesK > 1 )
-        pPars->fSkipCheck = 0;
-
-    // perform partitioning
-    if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
-         || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
-        return Ssw_SignalCorrespondencePart( pAig, pPars );
-
-    // start the choicing manager
-    p = Ssw_ManCreate( pAig, pPars );
-    // compute candidate equivalence classes
-//    p->pPars->nConstrs = 1;
-    if ( p->pPars->nConstrs == 0 )
-    {
-        // perform one round of seq simulation and generate candidate equivalence classes
-        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
-        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
-        Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
-    }
-    else
-    {
-        // create trivial equivalence classes with all nodes being candidates for constant 1
-        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
-        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
-    }
-
+    int RetValue, nIter;
+    int clk, clkTotal = clock();
     // get the starting stats
     p->nLitsBeg  = Ssw_ClassesLitNum( p->ppClasses );
-    p->nNodesBeg = Aig_ManNodeNum(pAig);
-    p->nRegsBeg  = Aig_ManRegNum(pAig);
+    p->nNodesBeg = Aig_ManNodeNum(p->pAig);
+    p->nRegsBeg  = Aig_ManRegNum(p->pAig);
     // refine classes using BMC
-    if ( pPars->fVerbose )
+    if ( p->pPars->fVerbose )
     {
         printf( "Before BMC: " );
         Ssw_ClassesPrint( p->ppClasses, 0 );
     }
     Ssw_ManSweepBmc( p );
     Ssw_ManCleanup( p );
-    if ( pPars->fVerbose )
+    if ( p->pPars->fVerbose )
     {
         printf( "After  BMC: " );
         Ssw_ClassesPrint( p->ppClasses, 0 );
@@ -134,7 +93,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     {
 clk = clock();
         RetValue = Ssw_ManSweep( p );
-        if ( pPars->fVerbose )
+        if ( p->pPars->fVerbose )
         {
             printf( "%3d : Const = %6d. Cl = %6d. LR = %6d. NR = %6d. F = %5d. ", 
                 nIter, Ssw_ClassesCand1Num(p->ppClasses), Ssw_ClassesClassNum(p->ppClasses), 
@@ -150,12 +109,72 @@ clk = clock();
     } 
     p->pPars->nIters = nIter + 1;
 p->timeTotal = clock() - clkTotal;
-    pAigNew = Aig_ManDupRepr( pAig, 0 );
+    pAigNew = Aig_ManDupRepr( p->pAig, 0 );
     Aig_ManSeqCleanup( pAigNew );
     // get the final stats
     p->nLitsEnd  = Ssw_ClassesLitNum( p->ppClasses );
     p->nNodesEnd = Aig_ManNodeNum(pAigNew);
     p->nRegsEnd  = Aig_ManRegNum(pAigNew);
+    return pAigNew;
+}
+
+/**Function*************************************************************
+
+  Synopsis    [Performs computation of signal correspondence with constraints.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
+{
+    Ssw_Pars_t Pars;
+    Aig_Man_t * pAigNew;
+    Ssw_Man_t * p;
+    // reset random numbers
+    Aig_ManRandom( 1 );
+    // if parameters are not given, create them
+    if ( pPars == NULL )
+        Ssw_ManSetDefaultParams( pPars = &Pars );
+    // consider the case of empty AIG
+    if ( Aig_ManNodeNum(pAig) == 0 )
+    {
+        pPars->nIters = 0;
+        // Ntl_ManFinalize() needs the following to satisfy an assertion
+        Aig_ManReprStart( pAig,Aig_ManObjNumMax(pAig) );
+        return Aig_ManDupOrdered(pAig);
+    }
+    // check and update parameters
+    assert( Aig_ManRegNum(pAig) > 0 );
+    assert( pPars->nFramesK > 0 );
+    if ( pPars->nFramesK > 1 )
+        pPars->fSkipCheck = 0;
+    // perform partitioning
+    if ( (pPars->nPartSize > 0 && pPars->nPartSize < Aig_ManRegNum(pAig))
+         || (pAig->vClockDoms && Vec_VecSize(pAig->vClockDoms) > 0)  )
+        return Ssw_SignalCorrespondencePart( pAig, pPars );
+    // start the induction manager
+    p = Ssw_ManCreate( pAig, pPars );
+    // compute candidate equivalence classes
+//    p->pPars->nConstrs = 1;
+    if ( p->pPars->nConstrs == 0 )
+    {
+        // perform one round of seq simulation and generate candidate equivalence classes
+        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->fLatchCorr, pPars->nMaxLevs, pPars->fVerbose );
+        p->pSml = Ssw_SmlStart( pAig, 0, p->nFrames + p->pPars->nFramesAddSim, 1 );
+        Ssw_ClassesSetData( p->ppClasses, p->pSml, Ssw_SmlNodeHash, Ssw_SmlNodeIsConst, Ssw_SmlNodesAreEqual );
+    }
+    else
+    {
+        // create trivial equivalence classes with all nodes being candidates for constant 1
+        p->ppClasses = Ssw_ClassesPrepareSimple( pAig, pPars->fLatchCorr, pPars->nMaxLevs );
+        Ssw_ClassesSetData( p->ppClasses, NULL, NULL, Ssw_NodeIsConstCex, Ssw_NodesAreEqualCex );
+    }
+    // perform refinement of classes
+    pAigNew = Ssw_SignalCorrespondenceRefine( p );    
     // cleanup
     Ssw_ManStop( p );
     return pAigNew;