From ce63869fe7ebb0e22af4833454daea0c5977f32f Mon Sep 17 00:00:00 2001
From: Alan Mishchenko <alanmi@berkeley.edu>
Date: Sun, 9 Dec 2012 17:33:44 -0800
Subject: Enabling multi-output solving in 'pdr'.

---
 src/base/abci/abcDar.c  |  8 ++++----
 src/proof/pdr/pdrCore.c | 10 ++++++----
 src/proof/pdr/pdrSat.c  |  3 +++
 src/proof/pdr/pdrTsim.c |  5 ++++-
 src/proof/pdr/pdrUtil.c |  1 +
 5 files changed, 18 insertions(+), 9 deletions(-)

(limited to 'src')

diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index d45af798..6ca00d3b 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2719,7 +2719,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
     RetValue = Pdr_ManSolve( pMan, pPars );
     if ( !pPars->fSilent )
     {
-        if ( pPars->fSolveAll )
+        if ( RetValue == 1 )
+            Abc_Print( 1, "Property proved.  " );
+        else if ( pPars->fSolveAll )
         {
             int nOutputs = Saig_ManPoNum(pMan) - Saig_ManConstrNum(pMan);
             if ( pMan->vSeqModelVec == NULL || Vec_PtrCountZero(pMan->vSeqModelVec) == nOutputs )
@@ -2732,9 +2734,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
         }
         else
         {
-            if ( RetValue == 1 )
-                Abc_Print( 1, "Property proved.  " );
-            else if ( RetValue == 0 )
+            if ( RetValue == 0 )
             {
                 if ( pMan->pSeqModel == NULL )
                     Abc_Print( 1, "Abc_NtkDarPdr(): Counter-example is not available.\n" );
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 85ad580e..46288925 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -590,7 +590,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                 if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                     return 0; // all SAT
                 continue;
-            }
+            } 
             // try to solve this output
             while ( 1 )
             {
@@ -624,6 +624,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     }
                     if ( RetValue == 0 )
                     {
+                        Abc_Cex_t * pCex;
                         if ( fPrintClauses )
                         {
                             Abc_Print( 1, "*** Clauses after frame %d:\n", k );
@@ -639,12 +640,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
-                        Abc_Print( 1, "Output %*d was asserted in frame %2d (solved %*d out of %*d outputs).\n",  
-                            nOutDigits, p->iOutCur, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                         if ( p->vCexes == NULL )
                             p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
-                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, Pdr_ManDeriveCex(p) );
+                        pCex = Pdr_ManDeriveCex(p);
+                        Vec_PtrWriteEntry( p->vCexes, p->iOutCur, pCex );
+                        Abc_Print( 1, "Output %*d was asserted in frame %2d (%2d) (solved %*d out of %*d outputs).\n",  
+                            nOutDigits, p->iOutCur, pCex->iFrame, k, nOutDigits, p->pPars->nFailOuts, nOutDigits, Saig_ManPoNum(p->pAig) );
                         if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
                             return 0; // all SAT
                         Pdr_QueueClean( p );
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index f0aff8bb..8bd45026 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -182,6 +182,9 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
     pSat = Pdr_ManSolver(p, k);
     Saig_ManForEachPo( p->pAig, pObj, i )
     {
+        // skip solved outputs
+        if ( p->vCexes && Vec_PtrEntry(p->vCexes, i) )
+            continue;
         Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal
         RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
         assert( RetValue == 1 );
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index fcd17fad..1865e14b 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -350,6 +350,7 @@ void Pdr_ManPrintCex( Aig_Man_t * pAig, Vec_Int_t * vCiObjs, Vec_Int_t * vCiVals
 ***********************************************************************/
 Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
 {
+    Pdr_Set_t * pRes;
     Vec_Int_t * vPrio   = p->vPrio;    // priority flops (flop indices)
     Vec_Int_t * vPiLits = p->vLits;    // array of literals (0/1 PI values)
     Vec_Int_t * vCiObjs = p->vCiObjs;  // cone leaves (CI obj IDs)
@@ -474,7 +475,9 @@ Pdr_ManPrintCex( p->pAig, vCiObjs, vCiVals, vCi2Rem );
     Pdr_ManDeriveResult( p->pAig, vCiObjs, vCiVals, vCi2Rem, vRes, vPiLits );
     assert( Vec_IntSize(vRes) > 0 );
     p->tTsim += clock() - clk;
-    return Pdr_SetCreate( vRes, vPiLits );
+    pRes = Pdr_SetCreate( vRes, vPiLits );
+    assert( k == 0 || !Pdr_SetIsInit(pRes, -1) );
+    return pRes;
 }
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrUtil.c b/src/proof/pdr/pdrUtil.c
index c70554e3..1536c1cc 100644
--- a/src/proof/pdr/pdrUtil.c
+++ b/src/proof/pdr/pdrUtil.c
@@ -515,6 +515,7 @@ void Pdr_QueueClean( Pdr_Man_t * p )
     Pdr_Obl_t * pThis;
     while ( (pThis = Pdr_QueuePop(p)) )
         Pdr_OblDeref( pThis );
+    pThis = NULL;
 }
 
 /**Function*************************************************************
-- 
cgit v1.2.3