Trying anothe resource limit in scorr.

src/base/abci/abc.c

@@ -23196,7 +23196,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, "PQFCLSIVMNXRcmplkodsefqvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "PQFCLSIVMNXRBcmplkodsefqvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -23332,7 +23332,17 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nSkip < 0 )
                 goto usage;
             break;
-
+        case 'B':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-B\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nSkipLimit = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nSkipLimit < 0 )
+                goto usage;
+            break;
         case 'c':
             pPars->fConstrs ^= 1;
             break;
@@ -23454,7 +23464,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: scorr [-PQFCLSIVMNXR <num>] [-cmplkodsefqvwh]\n" );
+    Abc_Print( -2, "usage: scorr [-PQFCLSIVMNXRB <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 );
@@ -23469,6 +23479,7 @@ int Abc_CommandSeqSweep2( Abc_Frame_t * pAbc, int argc, char ** argv )
     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-B num : the limit on the size of constraints to skip [default = %d]\n", pPars->nSkipLimit );
     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" );

src/proof/ssw/ssw.h

@@ -75,6 +75,7 @@ struct Ssw_Pars_t_
     int              fEquivDump2;   // enables dumping equivalences
     int              fStopWhenGone; // stop when PO output is not a candidate constant
     int              nSkip;
+    int              nSkipLimit;
     // optimized latch correspondence
     int              fLatchCorrOpt; // perform register correspondence (optimized)
     int              nSatVarMax;    // max number of SAT vars before recycling SAT solver (optimized latch corr only)

src/proof/ssw/sswAig.c

@@ -75,6 +75,57 @@ void Ssw_FrmStop( Ssw_Frm_t * p )
     ABC_FREE( p );
 }
 
+/**Function*************************************************************
+
+  Synopsis    [Computes the size of two-output cone.]
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
+int Aig_ObjDeref_rec( Aig_Obj_t * pNode )
+{
+    int Counter = 1;
+    assert( pNode->nRefs > 0 );
+    if ( --pNode->nRefs > 0 )
+        return 0;
+    assert( pNode->nRefs == 0 );
+    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
+        return 0;
+    Counter += Aig_ObjDeref_rec( Aig_ObjFanin0(pNode) );
+    Counter += Aig_ObjDeref_rec( Aig_ObjFanin1(pNode) );
+    return Counter;
+}
+int Aig_ObjRef_rec( Aig_Obj_t * pNode )
+{
+    int Counter = 1;
+    assert( pNode->nRefs >= 0 );
+    if ( pNode->nRefs++ > 0 )
+        return 0;
+    assert( pNode->nRefs == 1 );
+    if ( Aig_ObjIsCi(pNode) || Aig_ObjIsConst1(pNode) )
+        return 0;
+    Counter += Aig_ObjRef_rec( Aig_ObjFanin0(pNode) );
+    Counter += Aig_ObjRef_rec( Aig_ObjFanin1(pNode) );
+    return Counter;
+}
+int Aig_ManConeSize( Aig_Obj_t * pNode0, Aig_Obj_t * pNode1 )
+{
+    pNode0 = Aig_Regular(pNode0);
+    pNode1 = Aig_Regular(pNode1);
+    Aig_ObjRef( pNode0 );
+    Aig_ObjRef( pNode1 );
+    int Count0 = Aig_ObjDeref_rec(pNode0) + Aig_ObjDeref_rec(pNode1);
+    int Count1 = Aig_ObjRef_rec(pNode0)   + Aig_ObjRef_rec(pNode1);   
+    Aig_ObjDeref( pNode0 );
+    Aig_ObjDeref( pNode1 );     
+    assert( Count0 == Count1 );
+    return Count0;
+}
+
 /**Function*************************************************************
 
   Synopsis    [Performs speculative reduction for one node.]
@@ -120,7 +171,13 @@ static inline void Ssw_FramesConstrainNode( Ssw_Man_t * p, Aig_Man_t * pFrames,
     // add the constraint
     if ( fTwoPos )
     {
-        if ( p->pPars->nSkip == 0 ||rand() % p->pPars->nSkip == 0 ) {
+        if ( p->pPars->nSkipLimit ) {
+            if ( Aig_ManConeSize(pObjNew, pObjNew2) < p->pPars->nSkipLimit ) {
+                Aig_ObjCreateCo( pFrames, pObjNew2 );
+                Aig_ObjCreateCo( pFrames, pObjNew );
+            }
+        }
+        else if ( p->pPars->nSkip == 0 || rand() % p->pPars->nSkip == 0 ) {
             Aig_ObjCreateCo( pFrames, pObjNew2 );
             Aig_ObjCreateCo( pFrames, pObjNew );
         }
@@ -193,7 +250,6 @@ Aig_Man_t * Ssw_FramesWithClasses( Ssw_Man_t * p )
     // add the POs for the latch outputs of the last frame
     Saig_ManForEachLo( p->pAig, pObj, i )
         Aig_ObjCreateCo( pFrames, Ssw_ObjFrame( p, pObj, p->pPars->nFramesK ) );
-
     // remove dangling nodes
     Aig_ManCleanup( pFrames );
     // make sure the satisfying assignment is node assigned