Enabling multi-output solving in 'pdr'.

2 files changed, 42 insertions, 56 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index e7fe63e9..4b7f21bd 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -2292,13 +2292,21 @@ int Abc_CommandPrintStatus( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
     Abc_Print( 1,"Status = %d  Frames = %d   ", pAbc->Status, pAbc->nFrames );
-    if ( pAbc->pCex == NULL )
+    if ( pAbc->pCex == NULL && pAbc->vCexVec == NULL )
         Abc_Print( 1,"Cex is not defined.\n" );
     else
-        Abc_Print( 1,"Cex: PIs = %d  Regs = %d  PO = %d  Frame = %d  Bits = %d\n",
-            pAbc->pCex->nPis, pAbc->pCex->nRegs,
-            pAbc->pCex->iPo, pAbc->pCex->iFrame,
-            pAbc->pCex->nBits );
+    {
+        if ( pAbc->pCex )
+            Abc_CexPrintStats( pAbc->pCex );
+        if ( pAbc->vCexVec )
+        {
+            Abc_Cex_t * pTemp;
+            printf( "\n" );
+            Vec_PtrForEachEntry( Abc_Cex_t *, pAbc->vCexVec, pTemp, c )
+                if ( pTemp )
+                    Abc_CexPrintStats( pTemp );
+        }
+    }
     return 0;
 
 usage:
@@ -20920,7 +20928,10 @@ int Abc_CommandBmc3( Abc_Frame_t * pAbc, int argc, char ** argv )
         }
     }
     if ( pNtk->vSeqModelVec )
+    {
         Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+        pAbc->nFrames = -1;
+    }
     return 0;
 
 usage:
@@ -22314,10 +22325,9 @@ usage:
 ***********************************************************************/
 int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
 {
-    extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+    extern int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars );
     Pdr_Par_t Pars, * pPars = &Pars;
     Abc_Ntk_t * pNtk = Abc_FrameReadNtk(pAbc);
-    Abc_Cex_t * pCex = NULL;
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
@@ -22437,28 +22447,15 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         Abc_Print( -2, "The current network is not an AIG (run \"strash\").\n");
         return 0;
     }
-/*
-    if ( pPars->iOutput != -1 && (pPars->iOutput < 0 || pPars->iOutput >= Abc_NtkPoNum(pNtk)) )
-    {
-        Abc_Print( -2, "Output index (%d) is incorrect (can be 0 through %d).\n",
-            pPars->iOutput, Abc_NtkPoNum(pNtk)-1 );
-        return 0;
-    }
-*/
-/*
-    if ( Abc_NtkPoNum(pNtk) != 1 && pPars->fVerbose )
-    {
-        if ( pPars->iOutput == -1 )
-            Abc_Print( -2, "The %d property outputs are ORed together.\n", Abc_NtkPoNum(pNtk) );
-        else
-            Abc_Print( -2, "Working on the primary output with zero-based number %d (out of %d).\n",
-                pPars->iOutput, Abc_NtkPoNum(pNtk) );
-    }
-*/
     // run the procedure
-    pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars, &pCex );
+    pAbc->Status  = Abc_NtkDarPdr( pNtk, pPars );
     pAbc->nFrames = pPars->iFrame;
-    Abc_FrameReplaceCex( pAbc, &pCex );
+    Abc_FrameReplaceCex( pAbc, &pNtk->pSeqModel );
+    if ( pNtk->vSeqModelVec )
+    {
+        Abc_FrameReplaceCexVec( pAbc, &pNtk->vSeqModelVec );
+        pAbc->nFrames = -1;
+    }
     return 0;
 
 usage:
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index 496855c2..742f90bb 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2705,57 +2705,46 @@ int Abc_NtkDarSec( Abc_Ntk_t * pNtk1, Abc_Ntk_t * pNtk2, Fra_Sec_t * pSecPar )
   SeeAlso     []
 
 ***********************************************************************/
-int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
 {
     int RetValue = -1;
     clock_t clk = clock();
     Aig_Man_t * pMan;
-    *ppCex = NULL;
     pMan = Abc_NtkToDar( pNtk, 0, 1 );
     if ( pMan == NULL )
     {
         Abc_Print( 1, "Converting network into AIG has failed.\n" );
         return -1;
     }
-/*
-    // perform ORing the primary outputs
-    if ( pPars->iOutput == -1 )
-    {
-        Aig_Man_t * pTemp = Saig_ManDupOrpos( pMan );
-        RetValue = Pdr_ManSolve( pTemp, pPars, ppCex );
-        if ( RetValue == 0 )
-            (*ppCex)->iPo = Saig_ManFindFailedPoCex( pMan, *ppCex );
-        Aig_ManStop( pTemp );
-    }
-    else
-        RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
-*/
-    RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
-
-    // output the result
+    RetValue = Pdr_ManSolve( pMan, pPars );
     if ( !pPars->fSilent )
     {
         if ( RetValue == 1 )
             Abc_Print( 1, "Property proved.  " );
         else if ( RetValue == 0 )
-            Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+        {
+            if ( pMan->pSeqModel == NULL )
+                Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
+            else
+            {
+                Abc_Print( 1, "Output %d of miter \"%s\" was asserted in frame %d.  ", pMan->pSeqModel->iPo, pNtk->pName, pMan->pSeqModel->iFrame );
+                if ( !Saig_ManVerifyCex( pMan, pMan->pSeqModel ) )
+                    Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+            }
+        }
         else if ( RetValue == -1 )
             Abc_Print( 1, "Property UNDECIDED.  " );
         else
             assert( 0 );
         ABC_PRT( "Time", clock() - clk );
     }
-
-//    ABC_FREE( pNtk->pSeqModel );
-//    pNtk->pSeqModel = pMan->pSeqModel; pMan->pSeqModel = NULL;
-    if ( ppCex )
-        *ppCex = pMan->pSeqModel;
-    else
-        ABC_FREE( pMan->pSeqModel );
+    ABC_FREE( pNtk->pSeqModel );
+    pNtk->pSeqModel = pMan->pSeqModel;
     pMan->pSeqModel = NULL;
-
-    if ( *ppCex && !Saig_ManVerifyCex( pMan, *ppCex ) )
-        Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example verification has FAILED.\n" );
+    if ( pNtk->vSeqModelVec )
+        Vec_PtrFreeFree( pNtk->vSeqModelVec );
+    pNtk->vSeqModelVec = pMan->vSeqModelVec;
+    pMan->vSeqModelVec = NULL;
     Aig_ManStop( pMan );
     return RetValue;
 }