Adding constant correspondence.

11 files changed, 73 insertions, 24 deletions

diff --git a/abclib.dsp b/abclib.dsp
index d8428658..8ac3ebca 100644
--- a/abclib.dsp
+++ b/abclib.dsp
@@ -4167,15 +4167,15 @@ SOURCE=.\src\aig\llb\llb4Cex.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\llb\llb4Cluster.c
+SOURCE=.\src\aig\llb\llb4Image.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\llb\llb4Image.c
+SOURCE=.\src\aig\llb\llb4Nonlin.c
 # End Source File
 # Begin Source File
 
-SOURCE=.\src\aig\llb\llb4Nonlin.c
+SOURCE=.\src\aig\llb\llb4Sweep.c
 # End Source File
 # Begin Source File
 
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 )
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 60d66ca8..65523c05 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -8525,25 +8525,25 @@ int Abc_CommandTest( Abc_Frame_t * pAbc, int argc, char ** argv )
     }
 */
 
-/*
+
     {
 //        extern void Llb_Nonlin4Cluster( Aig_Man_t * pAig );
 //        extern void Aig_ManTerSimulate( Aig_Man_t * pAig );
-        extern void Llb4_Nonlin4Sweep( Aig_Man_t * pAig, int nBddLimit );
+//        extern Llb4_Nonlin4SweepExperiment( Aig_Man_t * pAig );
         extern Aig_Man_t * Abc_NtkToDar( Abc_Ntk_t * pNtk, int fExors, int fRegisters );
         Aig_Man_t * pAig = Abc_NtkToDar( pNtk, 0, 0 );
 //        Aig_ManTerSimulate( pAig );
 //        Llb_Nonlin4Cluster( pAig );
-        Llb4_Nonlin4Sweep( pAig, 100 );
+//        Llb4_Nonlin4SweepExperiment( pAig );
         Aig_ManStop( pAig );
     }
-*/
+
 
 /*
 {
     extern void Ssm_ManExperiment( char * pFileIn, char * pFileOut );
 //    Ssm_ManExperiment( "m\\big2.ssim", "m\\big2_.ssim" );
-    Ssm_ManExperiment( "m\\manyclocks2.ssim", "m\\manyclocks2_.ssim" );
+    Ssm_ManExperiment( "m\\big3.ssim", "m\\big3_.ssim" );
 }
 */
     return 0;
@@ -14449,7 +14449,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     // set defaults
     Ssw_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplofdsevwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNcmplkofdsevwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -14575,6 +14575,9 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'l':
             pPars->fLatchCorr ^= 1;
             break;
+        case 'k':
+            pPars->fConstCorr ^= 1;
+            break;
         case 'o':
             pPars->fOutputCorr ^= 1;
             break;
@@ -14656,7 +14659,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: scorr [-PQFCLSIVMN <num>] [-cmplodsevwh]\n" );
+    Abc_Print( -2, "usage: scorr [-PQFCLSIVMN <num>] [-cmplkodsevwh]\n" );
     Abc_Print( -2, "\t         performs sequential sweep using K-step induction\n" );
     Abc_Print( -2, "\t-P num : max partition size (0 = no partitioning) [default = %d]\n", pPars->nPartSize );
     Abc_Print( -2, "\t-Q num : partition overlap (0 = no overlap) [default = %d]\n", pPars->nOverSize );
@@ -14673,6 +14676,7 @@ usage:
     Abc_Print( -2, "\t-m     : toggle full merge if constraints are present [default = %s]\n", pPars->fMergeFull? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle alighning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );
     Abc_Print( -2, "\t-l     : toggle doing latch correspondence [default = %s]\n", pPars->fLatchCorr? "yes": "no" );
+    Abc_Print( -2, "\t-k     : toggle doing constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
     Abc_Print( -2, "\t-o     : toggle doing \'PO correspondence\' [default = %s]\n", pPars->fOutputCorr? "yes": "no" );
 //    Abc_Print( -2, "\t-f     : toggle filtering using iterative BMC [default = %s]\n", pPars->fSemiFormal? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dynamic addition of constraints [default = %s]\n", pPars->fDynamic? "yes": "no" );
@@ -25500,7 +25504,7 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Cec_ManCorSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPrecwvh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "FCPkrecwvh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25537,6 +25541,9 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nPrefix < 0 ) 
                 goto usage;
             break;
+        case 'k':
+            pPars->fConstCorr ^= 1;
+            break;
         case 'r':
             pPars->fUseRings ^= 1;
             break;
@@ -25571,11 +25578,12 @@ int Abc_CommandAbc9Scorr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &scorr [-FCP num] [-recwvh]\n" );
+    Abc_Print( -2, "usage: &scorr [-FCP num] [-krecwvh]\n" );
     Abc_Print( -2, "\t         performs signal correpondence computation\n" );
     Abc_Print( -2, "\t-C num : the max number of conflicts at a node [default = %d]\n", pPars->nBTLimit );
     Abc_Print( -2, "\t-F num : the number of timeframes in inductive case [default = %d]\n", pPars->nFrames );
     Abc_Print( -2, "\t-P num : the number of timeframes in the prefix [default = %d]\n", pPars->nPrefix );
+    Abc_Print( -2, "\t-k     : toggle using constant correspondence [default = %s]\n", pPars->fConstCorr? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using implication rings during refinement [default = %s]\n", pPars->fUseRings? "yes": "no" );
     Abc_Print( -2, "\t-e     : toggle using equivalences as choices [default = %s]\n", pPars->fMakeChoices? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle using circuit-based SAT solver [default = %s]\n", pPars->fUseCSat? "yes": "no" );
@@ -28086,9 +28094,10 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
     Llb_ManSetDefaultParams( pPars );
     pPars->fCluster = 0;
     pPars->fReorder = 0;
-    pPars->nBddMax  = 1000;
+    pPars->nBddMax     = 100;
+    pPars->nClusterMax = 500;
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "BFTLbcryzvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "BCFTLbcryzvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -28103,6 +28112,17 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nBddMax < 0 ) 
                 goto usage;
             break;
+        case 'C':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-C\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nClusterMax = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nClusterMax < 0 ) 
+                goto usage;
+            break;
         case 'F':
             if ( globalUtilOptind >= argc )
             {
@@ -28186,9 +28206,10 @@ int Abc_CommandAbc9ReachY( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: &reachy [-BFT num] [-L file] [-bcryzvh]\n" );
+    Abc_Print( -2, "usage: &reachy [-BCFT num] [-L file] [-bcryzvh]\n" );
     Abc_Print( -2, "\t         model checking via BDD-based reachability (non-linear-QS-based)\n" );
-    Abc_Print( -2, "\t-B num : the BDD node threshold for clustering [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-B num : the max BDD size to introduce cut points [default = %d]\n", pPars->nBddMax );
+    Abc_Print( -2, "\t-C num : the max BDD size to reparameterize/cluster [default = %d]\n", pPars->nClusterMax );
     Abc_Print( -2, "\t-F num : max number of reachability iterations [default = %d]\n", pPars->nIterMax );
     Abc_Print( -2, "\t-T num : approximate time limit in seconds (0=infinite) [default = %d]\n", pPars->TimeLimit );
     Abc_Print( -2, "\t-L file: the log file name [default = %s]\n", pLogFileName ? pLogFileName : "no logging" );