Experiment with "scorr".

berkeley-abc · Nov 17, 2024 · 1f3cf0a · 1f3cf0a
1 parent 3aff0af
commit 1f3cf0a
Show file tree

Hide file tree

Showing 3 changed files with 22 additions and 4 deletions.
diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
@@ -23148,7 +23148,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, "PQFCLSIVMNXcmplkodsefqvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNXRcmplkodsefqvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23273,6 +23273,18 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nLimitMax < 0 )
                 goto usage;
             break;
+        case 'R':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-R\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSkip = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSkip < 0 )
+                goto usage;
+            break;
+
         case 'c':
             pPars->fConstrs ^= 1;
             break;
@@ -23394,7 +23406,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: scorr [-PQFCLSIVMNX <num>] [-cmplkodsefqvwh]\n" );
+    Abc_Print( -2, "usage: scorr [-PQFCLSIVMNXR <num>] [-cmplkodsefqvwh]\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 );
@@ -23408,6 +23420,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     Abc_Print( -2, "\t-M num : min call num needed to recycle the SAT solver [default = %d]\n", pPars->nRecycleCalls2 );
     Abc_Print( -2, "\t-N num : set last <num> POs to be constraints (use with -c) [default = %d]\n", nConstrs );
     Abc_Print( -2, "\t-X num : the number of iterations of little or no improvement [default = %d]\n", pPars->nLimitMax );
+    Abc_Print( -2, "\t-R num : the number used to skip some constraints [default = %d]\n", pPars->nSkip );
     Abc_Print( -2, "\t-c     : toggle using explicit constraints [default = %s]\n", pPars->fConstrs? "yes": "no" );
     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 aligning polarity of SAT variables [default = %s]\n", pPars->fPolarFlip? "yes": "no" );

diff --git a/src/proof/ssw/ssw.h b/src/proof/ssw/ssw.h
@@ -74,6 +74,7 @@ struct Ssw_Pars_t_
     int              fEquivDump;    // enables dumping equivalences
     int              fEquivDump2;   // enables dumping equivalences
     int              fStopWhenGone; // stop when PO output is not a candidate constant
+    int              nSkip;
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
     int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)

diff --git a/src/proof/ssw/sswAig.c b/src/proof/ssw/sswAig.c
@@ -120,8 +120,10 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // add the constraint
     if ( fTwoPos )
     {
-        Aig_ObjCreateCo( pFrames, pObjNew2 );
-        Aig_ObjCreateCo( pFrames, pObjNew );
+        if ( p->pPars->nSkip == 0 ||rand() % p->pPars->nSkip == 0 ) {
+            Aig_ObjCreateCo( pFrames, pObjNew2 );
+            Aig_ObjCreateCo( pFrames, pObjNew );
+        }
     }
     else
     {
@@ -158,6 +160,8 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
         Ssw_ObjSetFrame( p, pObj, 0, Aig_ObjCreateCi(pFrames) );
     // add timeframes
     iLits = 0;
+    if ( p->pPars->nSkip )
+        srand(1);
     for ( f = 0; f < p->pPars->nFramesK; f++ )
     {
         // map constants and PIs