%pdra: added an option -u for checking comb. unsat

5 files changed, 54 insertions, 5 deletions

diff --git a/src/base/wlc/wlc.h b/src/base/wlc/wlc.h
index f5dbba42..699d2d9b 100644
--- a/src/base/wlc/wlc.h
+++ b/src/base/wlc/wlc.h
@@ -177,6 +177,7 @@ struct Wlc_Par_t_
     int                    fPdra;              // Use pdr -nct
     int                    fProofRefine;       // Use proof-based refinement
     int                    fHybrid;            // Use a hybrid of CBR and PBR
+    int                    fCheckCombUnsat;    // Check if ABS becomes comb. unsat
     int                    fVerbose;           // verbose output
     int                    fPdrVerbose;        // verbose output
 };
diff --git a/src/base/wlc/wlcAbs.c b/src/base/wlc/wlcAbs.c
index fdc04e50..776770de 100644
--- a/src/base/wlc/wlcAbs.c
+++ b/src/base/wlc/wlcAbs.c
@@ -33,6 +33,7 @@ ABC_NAMESPACE_IMPL_START
 extern Vec_Vec_t *   IPdr_ManSaveClauses( Pdr_Man_t * p, int fDropLast );
 extern int           IPdr_ManRestore( Pdr_Man_t * p, Vec_Vec_t * vClauses, Vec_Int_t * vMap );
 extern int           IPdr_ManSolveInt( Pdr_Man_t * p, int fCheckClauses, int fPushClauses );
+extern int           IPdr_ManCheckCombUnsat( Pdr_Man_t * p );
 
 typedef struct Int_Pair_t_       Int_Pair_t;
 struct Int_Pair_t_
@@ -1111,20 +1112,49 @@ int Wlc_NtkPdrAbs( Wlc_Ntk_t * p, Wlc_Par_t * pPars )
             Gia_ManPrintStats( pGia, NULL );
         }
         Wlc_NtkFree( pAbs );
+        // Gia_AigerWrite( pGia, "abs.aig", 0, 0 );
 
         // try to prove abstracted GIA by converting it to AIG and calling PDR
         pAig = Gia_ManToAigSimple( pGia );
 
-        pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
-        clk2 = Abc_Clock();
 
+        if ( vClauses && pPars->fCheckCombUnsat )
+        {
+            clk2 = Abc_Clock();
+
+            Pdr_Man_t * pPdr2;
+            pPdrPars->fVerbose = 0;
+            pPdr2 = Pdr_ManStart( pAig, pPdrPars, NULL );
+            RetValue = IPdr_ManCheckCombUnsat( pPdr2 );
+            Pdr_ManStop( pPdr2 );
+            pPdrPars->fVerbose = pPars->fPdrVerbose;
+
+            tPdr += Abc_Clock() - clk2;
+
+            if ( RetValue == 1 )
+            {
+                if ( pPars->fVerbose )
+                    Abc_PrintTime( 1,  "ABS becomes combinationally UNSAT. Time", Abc_Clock() - clk2 );
+                Gia_ManStop( pGia );
+                Vec_IntFree( vPisNew );
+                Aig_ManStop( pAig );
+                break;
+            }
+            
+            if ( pPars->fVerbose )
+                Abc_PrintTime( 1, "Check comb. unsat failed. Time", Abc_Clock() - clk2 );
+        }
+
+        clk2 = Abc_Clock();
+        pPdr = Pdr_ManStart( pAig, pPdrPars, NULL );
         if ( vClauses ) {
             assert( Vec_VecSize( vClauses) >= 2 ); 
             IPdr_ManRestore( pPdr, vClauses, vMap );
         }
         Vec_IntFreeP( &vMap );
 
-        RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
+        if ( !vClauses || RetValue != 1 )
+            RetValue = IPdr_ManSolveInt( pPdr, pPars->fCheckClauses, pPars->fPushClauses );
         pPdr->tTotal += Abc_Clock() - clk2;
         tPdr += pPdr->tTotal;
 
diff --git a/src/base/wlc/wlcCom.c b/src/base/wlc/wlcCom.c
index 38f919d4..a10310d4 100644
--- a/src/base/wlc/wlcCom.c
+++ b/src/base/wlc/wlcCom.c
@@ -462,7 +462,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Wlc_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmxvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "AMXFILabrcpmuxvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -553,6 +553,9 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'm':
             pPars->fMFFC ^= 1;
             break;
+        case 'u':
+            pPars->fCheckCombUnsat ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -573,7 +576,7 @@ int Abc_CommandPdrAbs( Abc_Frame_t * pAbc, int argc, char ** argv )
     Wlc_NtkPdrAbs( pNtk, pPars );
     return 0;
 usage:
-    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxvwh]\n" );
+    Abc_Print( -2, "usage: %%pdra [-AMXFIL num] [-abrcpmxuvwh]\n" );
     Abc_Print( -2, "\t         abstraction for word-level networks\n" );
     Abc_Print( -2, "\t-A num : minimum bit-width of an adder/subtractor to abstract [default = %d]\n", pPars->nBitsAdd );
     Abc_Print( -2, "\t-M num : minimum bit-width of a multiplier to abstract [default = %d]\n",        pPars->nBitsMul );
@@ -586,6 +589,7 @@ usage:
     Abc_Print( -2, "\t-b     : toggle using proof-based refinement [default = %s]\n",                  pPars->fProofRefine? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using both cex-based and proof-based refinement [default = %s]\n",                  pPars->fHybrid? "yes": "no" );
     Abc_Print( -2, "\t-c     : toggle checking clauses in the reloaded trace [default = %s]\n",        pPars->fCheckClauses? "yes": "no" );
+    Abc_Print( -2, "\t-u     : toggle checking combinationally unsat [default = %s]\n",                pPars->fCheckCombUnsat? "yes": "no" );
     Abc_Print( -2, "\t-p     : toggle pushing clauses in the reloaded trace [default = %s]\n",         pPars->fPushClauses? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle refining the whole MFFC of a PPI [default = %s]\n",              pPars->fMFFC? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing verbose information [default = %s]\n",                  pPars->fVerbose? "yes": "no" );
diff --git a/src/base/wlc/wlcNtk.c b/src/base/wlc/wlcNtk.c
index 89699949..e6f25f1e 100644
--- a/src/base/wlc/wlcNtk.c
+++ b/src/base/wlc/wlcNtk.c
@@ -121,6 +121,7 @@ void Wlc_ManSetDefaultParams( Wlc_Par_t * pPars )
     pPars->fPdra         =            0;   // Use pdr -nct 
     pPars->fProofRefine  =            0;   // Use proof-based refinement
     pPars->fHybrid       =            1;   // Use a hybrid of CBR and PBR
+    pPars->fCheckCombUnsat =          0;   // Check if ABS becomes comb. unsat
     pPars->fVerbose      =            0;   // verbose output`
     pPars->fPdrVerbose   =            0;   // show verbose PDR output
 }
diff --git a/src/proof/pdr/pdrIncr.c b/src/proof/pdr/pdrIncr.c
index 8ca8e29e..a4045768 100644
--- a/src/proof/pdr/pdrIncr.c
+++ b/src/proof/pdr/pdrIncr.c
@@ -738,6 +738,19 @@ int IPdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     return RetValue;
 }
 
+int IPdr_ManCheckCombUnsat( Pdr_Man_t * p )
+{
+    int iFrame, RetValue = -1;
+
+    Pdr_ManCreateSolver( p, (iFrame = 0) );
+    Pdr_ManCreateSolver( p, (iFrame = 1) );
+
+    p->nFrames = iFrame;
+    p->iUseFrame = Abc_MaxInt(iFrame, 1);
+
+    RetValue = Pdr_ManCheckCube( p, iFrame, NULL, NULL, p->pPars->nConfLimit, 0, 1 );
+    return RetValue;
+}
 
 /**Function*************************************************************