From 40d29e781387fdfbe8fec47e600d57a109fed1d9 Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Fri, 3 Mar 2017 12:29:15 -0800
Subject: only try scorr on small circuits

---
 src/base/wlc/wlcAbs.c | 58 +++++++++++++++++++++++++++------------------------
 1 file changed, 31 insertions(+), 27 deletions(-)

diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index 5a582663..79da6235 100644
--- 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();
-
-            Ssw_ManSetDefaultParams( pScorrPars );
-            pScorrPars->fStopWhenGone = 1;
-            pScorrPars->nFramesK = 1;
-            pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
-            assert ( pAigScorr );
-            nAnds = Aig_ManAndNum( pAigScorr); 
-            Aig_ManStop( pAigScorr );
-
-            if ( nAnds == 0 )
-            {
-                if ( pPars->fVerbose )
-                    Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
-                RetValue = 1;
-                Gia_ManStop( pGia );
-                Vec_IntFree( vPisNew );
-                Aig_ManStop( pAig );
-                break;
-            }
-            else if ( pPars->fVerbose )
-            {
-                Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
-                Abc_PrintTime( 1, "Time", Abc_Clock() - clk2 );
+            if ( Aig_ManAndNum( pAig ) <= 20000 )
+            { 
+                Aig_Man_t * pAigScorr;
+                Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
+                int nAnds;
+
+                clk2 = Abc_Clock();
+
+                Ssw_ManSetDefaultParams( pScorrPars );
+                pScorrPars->fStopWhenGone = 1;
+                pScorrPars->nFramesK = 1;
+                pAigScorr = Ssw_SignalCorrespondence( pAig, pScorrPars );
+                assert ( pAigScorr );
+                nAnds = Aig_ManAndNum( pAigScorr); 
+                Aig_ManStop( pAigScorr );
+
+                if ( nAnds == 0 )
+                {
+                    if ( pPars->fVerbose )
+                        Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk2 );
+                    RetValue = 1;
+                    Gia_ManStop( pGia );
+                    Vec_IntFree( vPisNew );
+                    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();
-- 
cgit v1.2.3