Adding constant correspondence.

4 files changed, 17 insertions, 1 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 );