Adding constant correspondence.

9 files changed, 36 insertions, 8 deletions

diff --git a/src/aig/cec/cec.h b/src/aig/cec/cec.h
index e4547f5e..9e2237d7 100644
--- a/src/aig/cec/cec.h
+++ b/src/aig/cec/cec.h
@@ -68,6 +68,7 @@ struct Cec_ParSim_t_
 //    int              fFirstStop;    // stop on the first sat output
     int              fSeqSimulate;  // performs sequential simulation
     int              fLatchCorr;    // consider only latch outputs
+    int              fConstCorr;    // consider only constants
     int              fVeryVerbose;  // verbose stats
     int              fVerbose;      // verbose stats
 };
@@ -137,6 +138,7 @@ struct Cec_ParCor_t_
     int              nLevelMax;     // (scorr only) the max number of levels
     int              nStepsMax;     // (scorr only) the max number of induction steps
     int              fLatchCorr;    // consider only latch outputs
+    int              fConstCorr;    // consider only constants
     int              fUseRings;     // use rings
     int              fMakeChoices;  // use equilvaences as choices
     int              fUseCSat;      // use circuit-based solver
diff --git a/src/aig/cec/cecClass.c b/src/aig/cec/cecClass.c
index 95414851..b6118038 100644
--- a/src/aig/cec/cecClass.c
+++ b/src/aig/cec/cecClass.c
@@ -759,6 +759,17 @@ references:
                 Cec_ManSimSimDeref( p, Ent );
         }
     }
+
+    if ( p->pPars->fConstCorr )
+    {
+        Vec_IntForEachEntry( p->vRefinedC, i, k )
+        {
+            Gia_ObjSetRepr( p->pAig, i, GIA_VOID );
+            Cec_ManSimSimDeref( p, i );
+        }
+        Vec_IntClear( p->vRefinedC );
+    }
+
     if ( Vec_IntSize(p->vRefinedC) > 0 )
         Cec_ManSimProcessRefined( p, p->vRefinedC );
     assert( vInfoCis == NULL || iCiId == Gia_ManCiNum(p->pAig) );
diff --git a/src/aig/cec/cecCore.c b/src/aig/cec/cecCore.c
index 369c4a40..bf41304b 100644
--- a/src/aig/cec/cecCore.c
+++ b/src/aig/cec/cecCore.c
@@ -78,6 +78,7 @@ void Cec_ManSimSetDefaultParams( Cec_ParSim_t * p )
     p->fCheckMiter    =       0;  // the circuit is the miter
 //    p->fFirstStop     =       0;  // stop on the first sat output
     p->fDualOut       =       0;  // miter with separate outputs
+    p->fConstCorr     =       0;  // consider only constants
     p->fSeqSimulate   =       0;  // performs sequential simulation
     p->fVeryVerbose   =       0;  // verbose stats
     p->fVerbose       =       0;  // verbose stats
@@ -187,6 +188,7 @@ void Cec_ManCorSetDefaultParams( Cec_ParCor_t * p )
     p->nLevelMax      =      -1;  // (scorr only) the max number of levels
     p->nStepsMax      =      -1;  // (scorr only) the max number of induction steps
     p->fLatchCorr     =       0;  // consider only latch outputs
+    p->fConstCorr     =       0;  // consider only constants
     p->fUseRings      =       1;  // combine classes into rings
     p->fUseCSat       =       1;  // use circuit-based solver
 //    p->fFirstStop     =       0;  // stop on the first sat output
@@ -359,7 +361,7 @@ Gia_Man_t * Cec_ManSatSweeping( Gia_Man_t * pAig, Cec_ParFra_t * pPars )
     pParsSim->nWords      = pPars->nWords;
     pParsSim->nFrames     = pPars->nRounds;
     pParsSim->fCheckMiter = pPars->fCheckMiter;
-    pParsSim->fDualOut = pPars->fDualOut;
+    pParsSim->fDualOut    = pPars->fDualOut;
     pParsSim->fVerbose    = pPars->fVerbose;
     pSim = Cec_ManSimStart( p->pAig, pParsSim );
     // SAT solving
diff --git a/src/aig/cec/cecCorr.c b/src/aig/cec/cecCorr.c
index 565ca47e..59d091d8 100644
--- a/src/aig/cec/cecCorr.c
+++ b/src/aig/cec/cecCorr.c
@@ -859,6 +859,7 @@ int Cec_ManLSCorrespondenceClasses( Gia_Man_t * pAig, Cec_ParCor_t * pPars )
     pParsSim->nFrames    = pPars->nFrames;
     pParsSim->fVerbose   = pPars->fVerbose;
     pParsSim->fLatchCorr = pPars->fLatchCorr;
+    pParsSim->fConstCorr = pPars->fConstCorr;
     pParsSim->fSeqSimulate = 1;
     // create equivalence classes of registers
     pSim = Cec_ManSimStart( pAig, pParsSim );
diff --git a/src/aig/ssw/ssw.h b/src/aig/ssw/ssw.h
index 437e6ec8..e4a2619e 100644
--- a/src/aig/ssw/ssw.h
+++ b/src/aig/ssw/ssw.h
@@ -57,6 +57,7 @@ struct Ssw_Pars_t_
     int              TimeLimit;     // time out in seconds
     int              fPolarFlip;    // uses polarity adjustment
     int              fLatchCorr;    // perform register correspondence
+    int              fConstCorr;    // perform constant correspondence
     int              fOutputCorr;   // perform 'PO correspondence'
     int              fSemiFormal;   // enable semiformal filtering
 //    int              fUniqueness;   // enable uniqueness constraints
diff --git a/src/aig/ssw/sswClass.c b/src/aig/ssw/sswClass.c
index 7fd2a21b..a0e64cc0 100644
--- a/src/aig/ssw/sswClass.c
+++ b/src/aig/ssw/sswClass.c
@@ -39,6 +39,7 @@ struct Ssw_Cla_t_
     Aig_Man_t *      pAig;             // original AIG manager
     Aig_Obj_t ***    pId2Class;        // non-const classes by ID of repr node
     int *            pClassSizes;      // sizes of each equivalence class
+    int              fConstCorr;
     // statistics
     int              nClasses;         // the total number of non-const classes
     int              nCands1;          // the total number of const candidates
@@ -496,7 +497,7 @@ void Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj )
   SeeAlso     []
 
 ***********************************************************************/
-int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
+int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands, int fConstCorr )
 {
     Aig_Man_t * pAig = p->pAig;
     Aig_Obj_t ** ppTable, ** ppNexts, ** ppClassNew;
@@ -522,6 +523,8 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
             p->nCands1++;
             continue;
         }
+        if ( fConstCorr )
+            continue;
         // hash the node by its simulation info
         iEntry = p->pFuncNodeHash( p->pManData, pObj ) % nTableSize;
         // add the node to the class
@@ -590,7 +593,7 @@ int Ssw_ClassesPrepareRehash( Ssw_Cla_t * p, Vec_Ptr_t * vCands )
   SeeAlso     []
 
 ***********************************************************************/
-Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
+Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose )
 {
 //    int nFrames =  4;
 //    int nWords  =  1;
@@ -611,6 +614,7 @@ Ssw_Cla_t * Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr,
 
     // start the classes
     p = Ssw_ClassesStart( pAig );
+    p->fConstCorr = fConstCorr;
 
     // perform sequential simulation
 clk = clock();
@@ -668,7 +672,7 @@ clk = clock();
     p->pMemClassesFree = p->pMemClasses;
 
     // now it is time to refine the classes
-    Ssw_ClassesPrepareRehash( p, vCands );
+    Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
 if ( fVerbose )
 {
     printf( "Collecting candidate equivalence classes.        " );
@@ -688,7 +692,7 @@ clk = clock();
         // perform new round of simulation
         Ssw_SmlResimulateSeq( pSml );
         // check equivalence classes
-        RetValue = Ssw_ClassesPrepareRehash( p, vCands );
+        RetValue = Ssw_ClassesPrepareRehash( p, vCands, fConstCorr );
         if ( RetValue == 0 )
             break;
     }
@@ -1110,6 +1114,12 @@ int Ssw_ClassesRefineConst1( Ssw_Cla_t * p, int fRecursive )
     // check if there is a new class
     if ( Vec_PtrSize(p->vClassNew) == 0 )
         return 0;
+    if ( p->fConstCorr )
+    {
+        Vec_PtrForEachEntry( Aig_Obj_t *, p->vClassNew, pObj, i )
+            Aig_ObjSetRepr( p->pAig, pObj, NULL );
+        return 1;
+    }
     p->nCands1 -= Vec_PtrSize(p->vClassNew);
     pReprNew = (Aig_Obj_t *)Vec_PtrEntry( p->vClassNew, 0 );
     Aig_ObjSetRepr( p->pAig, pReprNew, NULL );
diff --git a/src/aig/ssw/sswCore.c b/src/aig/ssw/sswCore.c
index 76cc34fa..1f4d44d2 100644
--- a/src/aig/ssw/sswCore.c
+++ b/src/aig/ssw/sswCore.c
@@ -59,6 +59,7 @@ void Ssw_ManSetDefaultParams( Ssw_Pars_t * p )
     p->nStepsMax      =      -1;  // (scorr only) the max number of induction steps
     p->fPolarFlip     =       0;  // uses polarity adjustment
     p->fLatchCorr     =       0;  // performs register correspondence
+    p->fConstCorr     =       0;  // performs constant correspondence
     p->fOutputCorr    =       0;  // perform 'PO correspondence'
     p->fSemiFormal    =       0;  // enable semiformal filtering
     p->fDynamic       =       0;  // dynamic partitioning
@@ -465,7 +466,7 @@ Aig_Man_t * Ssw_SignalCorrespondence( Aig_Man_t * pAig, Ssw_Pars_t * pPars )
     else
     {
         // perform one round of seq simulation and generate candidate equivalence classes
-        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
+        p->ppClasses = Ssw_ClassesPrepare( pAig, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
 //        p->ppClasses = Ssw_ClassesPrepareTargets( pAig );
         if ( pPars->fLatchCorrOpt )
             p->pSml = Ssw_SmlStart( pAig, 0, 2, 1 );
diff --git a/src/aig/ssw/sswInt.h b/src/aig/ssw/sswInt.h
index 189494bc..32959e85 100644
--- a/src/aig/ssw/sswInt.h
+++ b/src/aig/ssw/sswInt.h
@@ -219,7 +219,7 @@ extern void          Ssw_ClassesCollectClass( Ssw_Cla_t * p, Aig_Obj_t * pRepr,
 extern void          Ssw_ClassesCheck( Ssw_Cla_t * p );
 extern void          Ssw_ClassesPrint( Ssw_Cla_t * p, int fVeryVerbose );
 extern void          Ssw_ClassesRemoveNode( Ssw_Cla_t * p, Aig_Obj_t * pObj );
-extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
+extern Ssw_Cla_t *   Ssw_ClassesPrepare( Aig_Man_t * pAig, int nFramesK, int fLatchCorr, int fConstCorr, int fOutputCorr, int nMaxLevs, int fVerbose );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareSimple( Aig_Man_t * pAig, int fLatchCorr, int nMaxLevs );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareFromReprs( Aig_Man_t * pAig );
 extern Ssw_Cla_t *   Ssw_ClassesPrepareTargets( Aig_Man_t * pAig );
diff --git a/src/aig/ssw/sswIslands.c b/src/aig/ssw/sswIslands.c
index d1ebe4bc..0802aca5 100644
--- a/src/aig/ssw/sswIslands.c
+++ b/src/aig/ssw/sswIslands.c
@@ -438,7 +438,7 @@ Aig_Man_t * Ssw_SecWithSimilaritySweep( Aig_Man_t * p0, Aig_Man_t * p1, Vec_Int_
     if ( p->pPars->fPartSigCorr )
         p->ppClasses = Ssw_ClassesPreparePairsSimple( pMiter, vPairsMiter );
     else
-        p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
+        p->ppClasses = Ssw_ClassesPrepare( pMiter, pPars->nFramesK, pPars->fLatchCorr, pPars->fConstCorr, pPars->fOutputCorr, pPars->nMaxLevs, pPars->fVerbose );
     if ( p->pPars->fDumpSRInit )
     {
         if ( p->pPars->fPartSigCorr )