only try scorr on small circuits

40d29e78 · Yen-Sheng Ho · cb603c5e · 40d29e78
Commit 40d29e78 authored Mar 03, 2017 by Yen-Sheng Ho
Hide whitespace changes
Inline Side-by-side

Showing with 31 additions and 27 deletions

src/base/wlc/wlcAbs.c
+31 -27

No files found.
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1124,34 +1124,38 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
        if ( vClauses && pPars->fCheckCombUnsat )
        {
            Pdr_Man_t * pPdr2;
-            Aig_Man_t * pAigScorr;
-            Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
-            int nAnds;
-            clk2 = Abc_Clock();
+            if ( Aig_ManAndNum( pAig ) <= 20000 )
+            { 
-            Ssw_ManSetDefaultParams( pScorrPars );
+                Aig_Man_t * pAigScorr;
-            pScorrPars->fStopWhenGone = 1;
+                Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
-            pScorrPars->nFramesK = 1;
+                int nAnds;
-            pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
-            assert ( pAigScorr );
+                clk2 = Abc_Clock();
-            nAnds = Aig_ManAndNum( pAigScorr); 
-            Aig_ManStop( pAigScorr );
+                Ssw_ManSetDefaultParams( pScorrPars );
+                pScorrPars->fStopWhenGone = 1;
-            if ( nAnds == 0 )
+                pScorrPars->nFramesK = 1;
-            {
+                pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
-                if ( pPars->fVerbose )
+                assert ( pAigScorr );
-                    Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
+                nAnds = Aig_ManAndNum( pAigScorr); 
-                RetValue = 1;
+                Aig_ManStop( pAigScorr );
-                Gia_ManStop( pGia );
-                Vec_IntFree( vPisNew );
+                if ( nAnds == 0 )
-                Aig_ManStop( pAig );
+                {
-                break;
+                    if ( pPars->fVerbose )
-            }
+                        Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
-            else if ( pPars->fVerbose )
+                    RetValue = 1;
-            {
+                    Gia_ManStop( pGia );
-                Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
+                    Vec_IntFree( vPisNew );
-                Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+                    Aig_ManStop( pAig );
+                    break;
+                }
+                else if ( pPars->fVerbose )
+                {
+                    Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
+                    Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+                }
            }
            clk2 = Abc_Clock();