From 7713e94a1aee256db65a1939f1daafdec61d6675 Mon Sep 17 00:00:00 2001
From: Yen-Sheng Ho <ysho@berkeley.edu>
Date: Sat, 18 Mar 2017 14:23:09 -0700
Subject: %pdra: isolated the procedure for checking comb. unsat

---
 src/base/wlc/wlcAbs.c | 86 +++++++++++++++++++++++++++++----------------------
 1 file changed, 49 insertions(+), 37 deletions(-)

(limited to 'src/base/wlc')

diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index c89ed187..3373cdd9 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -1251,6 +1251,54 @@ Aig_Man_t * Wla_ManBitBlast( Wla_Man_t * pWla, Wlc_Ntk_t * pAbs )
     return pAig;
 }
 
+int Wla_ManCheckCombUnsat( Wla_Man_t * pWla, Aig_Man_t * pAig )
+{
+    Pdr_Man_t * pPdr;
+    abctime clk;
+    int RetValue = -1;
+
+    if ( Aig_ManAndNum( pAig ) <= 20000 )
+    { 
+        Aig_Man_t * pAigScorr;
+        Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
+        int nAnds;
+
+        clk = 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 ( pWla->pPars->fVerbose )
+                Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk );
+            return 1;
+        }
+        else if ( pWla->pPars->fVerbose )
+        {
+            Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
+            Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
+        }
+    }
+
+    clk = Abc_Clock();
+
+    pWla->pPdrPars->fVerbose = 0;
+    pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL );
+    RetValue = IPdr_ManCheckCombUnsat( pPdr );
+    Pdr_ManStop( pPdr );
+    pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose;
+
+    pWla->tPdr += Abc_Clock() - clk;
+
+    return RetValue;
+}
+
 int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
 {
     abctime clk;
@@ -1259,45 +1307,9 @@ int Wla_ManSolve( Wla_Man_t * pWla, Aig_Man_t * pAig )
 
     if ( pWla->vClauses && pWla->pPars->fCheckCombUnsat )
     {
-        if ( Aig_ManAndNum( pAig ) <= 20000 )
-        { 
-            Aig_Man_t * pAigScorr;
-            Ssw_Pars_t ScorrPars, * pScorrPars = &ScorrPars;
-            int nAnds;
-
-            clk = 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 ( pWla->pPars->fVerbose )
-                    Abc_PrintTime( 1, "SCORR proved UNSAT. Time", Abc_Clock() - clk );
-                return 1;
-            }
-            else if ( pWla->pPars->fVerbose )
-            {
-                Abc_Print( 1, "SCORR failed with %d ANDs. ", nAnds);
-                Abc_PrintTime( 1, "Time", Abc_Clock() - clk );
-            }
-        }
-
         clk = Abc_Clock();
 
-        pWla->pPdrPars->fVerbose = 0;
-        pPdr = Pdr_ManStart( pAig, pWla->pPdrPars, NULL );
-        RetValue = IPdr_ManCheckCombUnsat( pPdr );
-        Pdr_ManStop( pPdr );
-        pWla->pPdrPars->fVerbose = pWla->pPars->fPdrVerbose;
-
-        pWla->tPdr += Abc_Clock() - clk;
-
+        RetValue = Wla_ManCheckCombUnsat( pWla, pAig );
         if ( RetValue == 1 )
         {
             if ( pWla->pPars->fVerbose )
-- 
cgit v1.2.3