Enabling multi-output solving in 'pdr'.

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:

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 )
+        {
+            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;
 }

src/misc/util/utilCex.c

@@ -261,8 +261,9 @@ void Abc_CexPrintStats( Abc_Cex_t * p )
     }
     for ( k = 0; k < p->nBits; k++ )
         Counter += Abc_InfoHasBit(p->pData, k);
-    printf( "CEX: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits =%8d  nOnes =%8d (%5.2f %%)\n", 
-        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
+    printf( "CEX: Po =%4d  Frame =%4d  FF = %d  PI = %d  Bit =%8d  1s =%8d (%5.2f %%)\n", 
+        p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, 
+        Counter, 100.0 * Counter / (p->nBits - p->nRegs) );
 }
 void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
 {
@@ -278,7 +279,7 @@ void Abc_CexPrintStatsInputs( Abc_Cex_t * p, int nInputs )
         if ( (k - p->nRegs) % p->nPis < nInputs )
             Counter2 += Abc_InfoHasBit(p->pData, k);
     }
-    printf( "CEX: iPo = %d  iFrame = %d  nRegs = %d  nPis = %d  nBits =%8d  nOnes =%8d (%5.2f %%)  nOnesIn =%8d (%5.2f %%)\n", 
+    printf( "CEX: Po =%4d  Frame =%4d  FF = %d  PI = %d  Bit =%8d  1s =%8d (%5.2f %%) 1sIn =%8d (%5.2f %%)\n", 
         p->iPo, p->iFrame, p->nRegs, p->nPis, p->nBits, 
         Counter,  100.0 * Counter  / (p->nBits - p->nRegs), 
         Counter2, 100.0 * Counter2 / (p->nBits - p->nRegs - (p->iFrame + 1) * (p->nPis - nInputs)) );

src/proof/abs/absOldRef.c

@@ -134,7 +134,6 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
         pSecPar->fVerbose       = fVerbose;
         RetValue = Fra_FraigSec( pAbs, pSecPar, NULL );
 */
-        Abc_Cex_t * pCex = NULL;
         Aig_Man_t * pAbsOrpos = Saig_ManDupOrpos( pAbs );
         Pdr_Par_t Pars, * pPars = &Pars;
         Pdr_ManSetDefaultParams( pPars );
@@ -142,11 +141,12 @@ Aig_Man_t * Saig_ManCexRefine( Aig_Man_t * p, Aig_Man_t * pAbs, Vec_Int_t * vFlo
         pPars->fVerbose = fVerbose;
         if ( pPars->fVerbose )
             printf( "Running property directed reachability...\n" );
-        RetValue = Pdr_ManSolve( pAbsOrpos, pPars, &pCex );
-        if ( pCex )
-            pCex->iPo = Saig_ManFindFailedPoCex( pAbs, pCex );
+        RetValue = Pdr_ManSolve( pAbsOrpos, pPars );
+        if ( pAbsOrpos->pSeqModel )
+            pAbsOrpos->pSeqModel->iPo = Saig_ManFindFailedPoCex( pAbs, pAbsOrpos->pSeqModel );
+        pAbs->pSeqModel = pAbsOrpos->pSeqModel;
+        pAbsOrpos->pSeqModel = NULL;
         Aig_ManStop( pAbsOrpos );
-        pAbs->pSeqModel = pCex;
         if ( RetValue )
             *piRetValue = 1;
 

src/proof/abs/absPth.c

@@ -107,8 +107,7 @@ void * Abs_ProverThread( void * pArg )
     pPars->fSilent   = 1;
     pPars->RunId     = pThData->RunId;
     pPars->pFuncStop = Abs_CallBackToStop;
-    RetValue = Pdr_ManSolve( pThData->pAig, pPars, NULL );
-//    RetValue = Pdr_ManSolve_test( pAig, pPars, NULL );
+    RetValue = Pdr_ManSolve( pThData->pAig, pPars );
     // update the result
     if ( RetValue == 1 )
     {

src/proof/fra/fraSec.c

@@ -589,19 +589,15 @@ ABC_PRT( "Time", clock() - clk );
     // try PDR
     if ( pParSec->fUsePdr && RetValue == -1 && Aig_ManRegNum(pNew) > 0 )
     {
-        Abc_Cex_t * pCex = NULL;
-        Aig_Man_t * pNewOrpos = Saig_ManDupOrpos( pNew );
         Pdr_Par_t Pars, * pPars = &Pars;
         Pdr_ManSetDefaultParams( pPars );
         pPars->nTimeOut = pParSec->nPdrTimeout;
         pPars->fVerbose = pParSec->fVerbose;
         if ( pParSec->fVerbose )
             printf( "Running property directed reachability...\n" );
-        RetValue = Pdr_ManSolve( pNewOrpos, pPars, &pCex );
-        if ( pCex )
-            pCex->iPo = Saig_ManFindFailedPoCex( pNew, pCex );
-        Aig_ManStop( pNewOrpos );
-        pNew->pSeqModel = pCex;
+        RetValue = Pdr_ManSolve( pNew, pPars );
+        if ( pNew->pSeqModel )
+            pNew->pSeqModel->iPo = Saig_ManFindFailedPoCex( pNew, pNew->pSeqModel );
     }
 
 finish:

src/proof/pdr/pdr.h

@@ -71,7 +71,7 @@ struct Pdr_Par_t_
 
 /*=== pdrCore.c ==========================================================*/
 extern void               Pdr_ManSetDefaultParams( Pdr_Par_t * pPars );
-extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex );
+extern int                Pdr_ManSolve( Aig_Man_t * p, Pdr_Par_t * pPars );
 
 
 ABC_NAMESPACE_HEADER_END

src/proof/pdr/pdrCore.c

@@ -635,7 +635,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 
                         if ( !p->pPars->fSolveAll )
                         {
-                            p->pAig->pSeqModel = Pdr_ManDeriveCex( p );
+                            p->pAig->pSeqModel = Pdr_ManDeriveCex(p);
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
@@ -647,6 +647,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
+                        Pdr_QueueClean( p );
+                        pCube = NULL;
+                        break; // keep solving
                     }
                     if ( p->pPars->fVerbose ) 
                         Pdr_ManPrintProgress( p, 0, clock() - clkStart );
@@ -735,7 +738,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
+int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
 {
     Pdr_Man_t * p;
     int RetValue;
@@ -743,16 +746,19 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     if ( pPars->fVerbose )
     {
 //    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
-        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueueMax = %d. TimeMax = %d. ", 
-            pPars->nRecycle, pPars->nFrameMax, pPars->nRestLimit, pPars->nTimeOut );
-        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", 
-            pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
+        Abc_Print( 1, "VarMax = %d. FrameMax = %d. QueMax = %d. TimeMax = %d. ", 
+            pPars->nRecycle, 
+            pPars->nFrameMax, 
+            pPars->nRestLimit, 
+            pPars->nTimeOut );
+        Abc_Print( 1, "MonoCNF = %s. SkipGen = %s. SolveAll = %s.\n", 
+            pPars->fMonoCnf ?     "yes" : "no", 
+            pPars->fSkipGeneral ? "yes" : "no", 
+            pPars->fSolveAll ?    "yes" : "no" );
     }
     ABC_FREE( pAig->pSeqModel );
     p = Pdr_ManStart( pAig, pPars, NULL );
     RetValue = Pdr_ManSolveInt( p );
-//    if ( ppCex )
-//        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
     if ( RetValue == 0 )
         assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
     if ( p->vCexes )
@@ -763,9 +769,6 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     }
     if ( p->pPars->fDumpInv )
         Pdr_ManDumpClauses( p, (char *)"inv.pla", RetValue==1 );
-//    if ( *ppCex && pPars->fVerbose )
-//        Abc_Print( 1, "Found counter-example in frame %d after exploring %d frames.\n", 
-//            (*ppCex)->iFrame, p->nFrames );
     p->tTotal += clock() - clk;
     Pdr_ManStop( p );
     pPars->iFrame--;

src/proof/pdr/pdrInt.h

@@ -187,6 +187,7 @@ extern void            Pdr_OblDeref( Pdr_Obl_t * p );
 extern int             Pdr_QueueIsEmpty( Pdr_Man_t * p );
 extern Pdr_Obl_t *     Pdr_QueueHead( Pdr_Man_t * p );
 extern Pdr_Obl_t *     Pdr_QueuePop( Pdr_Man_t * p );
+extern void            Pdr_QueueClean( Pdr_Man_t * p );
 extern void            Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl );
 extern void            Pdr_QueuePrint( Pdr_Man_t * p );
 extern void            Pdr_QueueStop( Pdr_Man_t * p );

src/proof/pdr/pdrMan.c

@@ -188,6 +188,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
             Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
         }
     assert( f == nFrames );
+    if ( !Saig_ManVerifyCex(p->pAig, pCex) )
+        printf( "CEX for output %d is not valid.\n", p->iOutCur );
     return pCex;
 }
 

src/proof/pdr/pdrUtil.c

@@ -510,6 +510,24 @@ Pdr_Obl_t * Pdr_QueuePop( Pdr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
+void Pdr_QueueClean( Pdr_Man_t * p )
+{
+    Pdr_Obl_t * pThis;
+    while ( (pThis = Pdr_QueuePop(p)) )
+        Pdr_OblDeref( pThis );
+}
+
+/**Function*************************************************************
+
+  Synopsis    []
+
+  Description []
+               
+  SideEffects []
+
+  SeeAlso     []
+
+***********************************************************************/
 void Pdr_QueuePush( Pdr_Man_t * p, Pdr_Obl_t * pObl )
 {
     Pdr_Obl_t * pTemp, ** ppPrev;