Enabling multi-output solving in 'pdr'.

6 files changed, 165 insertions, 129 deletions

diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index 491477dd..3c40d2d5 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -40,7 +40,7 @@ ABC_NAMESPACE_HEADER_START
 typedef struct Pdr_Par_t_ Pdr_Par_t;
 struct Pdr_Par_t_
 {
-    int iOutput;          // zero-based number of primary output to solve
+//    int iOutput;          // zero-based number of primary output to solve
     int nRecycle;         // limit on vars for recycling
     int nFrameMax;        // limit on frame count
     int nConfLimit;       // limit on SAT solver conflicts
@@ -54,6 +54,8 @@ struct Pdr_Par_t_
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output
     int fSilent;          // totally silent execution
+    int fSolveAll;        // do not stop when found a SAT output
+    int nFailOuts;        // the number of failed outputs
     int iFrame;           // explored up to this frame
     int RunId;            // PDR id in this run 
     int(*pFuncStop)(int); // callback to terminate
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index ca2ca5a0..f72983da 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -45,7 +45,7 @@ ABC_NAMESPACE_IMPL_START
 void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
 {
     memset( pPars, 0, sizeof(Pdr_Par_t) );
-    pPars->iOutput       =      -1;  // zero-based output number
+//    pPars->iOutput       =      -1;  // zero-based output number
     pPars->nRecycle      =     300;  // limit on vars for recycling
     pPars->nFrameMax     =   10000;  // limit on number of timeframes
     pPars->nTimeOut      =       0;  // timeout in seconds
@@ -552,7 +552,9 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
 {
     int fPrintClauses = 0;
     Pdr_Set_t * pCube;
+    Aig_Obj_t * pObj;
     int k, RetValue = -1;
+    int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
     clock_t clkStart = clock();
     p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
@@ -562,87 +564,132 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     {
         p->nFrames = k;
         assert( k == Vec_PtrSize(p->vSolvers)-1 );
-        RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
-        {
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                if ( p->pPars->nConfLimit )
-                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                else if ( p->pPars->fVerbose ) 
-                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
-            p->pPars->iFrame = k;
-            return -1;
-        }
-        if ( RetValue == 0 )
+        Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
         {
-            RetValue = Pdr_ManBlockCube( p, pCube );
-            if ( RetValue == -1 )
+            // skip solved outputs
+            if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
+                continue;
+            // check if the output is trivially solved
+            if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
+                continue;
+            // check if the output is trivially solved
+            if ( Aig_ObjChild0(pObj) == Aig_ManConst1(p->pAig) )
             {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                if ( p->pPars->nConfLimit )
-                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                else if ( p->pPars->fVerbose ) 
-                    Abc_Print( 1, "Computation cancelled by the callback.\n" );
-                p->pPars->iFrame = k;
-                return -1;
+                if ( !p->pPars->fSolveAll )
+                {
+                    p->pAig->pSeqModel = Abc_CexMakeTriv( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), Saig_ManPoNum(p->pAig), k*Saig_ManPoNum(p->pAig)+p->iOutCur );
+                    return 0; // SAT
+                }
+                p->pPars->nFailOuts++;
+                Abc_Print( 1, "Output %*d was trivially 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) );
+                if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
+                    return 0; // all SAT
+                continue;
             }
-            if ( RetValue == 0 )
+            // try to solve this output
+            while ( 1 )
             {
-                if ( fPrintClauses )
+                RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
+                if ( RetValue == 1 )
+                    break;
+                if ( RetValue == -1 )
                 {
-                    Abc_Print( 1, "*** Clauses after frame %d:\n", k );
-                    Pdr_ManPrintClauses( p, 0 );
+                    if ( p->pPars->fVerbose ) 
+                        Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+                        if ( p->pPars->nConfLimit )
+                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                        else if ( p->pPars->fVerbose ) 
+                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
+                    p->pPars->iFrame = k;
+                    return -1;
                 }
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                p->pPars->iFrame = k;
-                return 0; // SAT
-            }
-            if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 0, clock() - clkStart );
+                if ( RetValue == 0 )
+                {
+                    RetValue = Pdr_ManBlockCube( p, pCube );
+                    if ( RetValue == -1 )
+                    {
+                        if ( p->pPars->fVerbose ) 
+                            Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+                        if ( p->pPars->nConfLimit )
+                            Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+                        else if ( p->pPars->fVerbose ) 
+                            Abc_Print( 1, "Computation cancelled by the callback.\n" );
+                        p->pPars->iFrame = k;
+                        return -1;
+                    }
+                    if ( RetValue == 0 )
+                    {
+                        if ( fPrintClauses )
+                        {
+                            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+                            Pdr_ManPrintClauses( p, 0 );
+                        }
+                        if ( p->pPars->fVerbose ) 
+                            Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+                        p->pPars->iFrame = k;
+
+                        if ( !p->pPars->fSolveAll )
+                        {
+                            p->pAig->pSeqModel = Pdr_ManDeriveCex( 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) );
+                        if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
+                            return 0; // all SAT
+                    }
+                    if ( p->pPars->fVerbose ) 
+                        Pdr_ManPrintProgress( p, 0, clock() - clkStart );
+                }
+            } 
         }
-        else
+
+        if ( p->pPars->fVerbose ) 
+            Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+        // open a new timeframe
+        p->nQueLim = p->pPars->nRestLimit;
+        assert( pCube == NULL );
+        Pdr_ManSetPropertyOutput( p, k );
+        Pdr_ManCreateSolver( p, ++k );
+        if ( fPrintClauses )
+        {
+            Abc_Print( 1, "*** Clauses after frame %d:\n", k );
+            Pdr_ManPrintClauses( p, 0 );
+        }
+        // push clauses into this timeframe
+        RetValue = Pdr_ManPushClauses( p );
+        if ( RetValue == -1 )
         {
             if ( p->pPars->fVerbose ) 
                 Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-            // open a new timeframe
-            p->nQueLim = p->pPars->nRestLimit;
-            assert( pCube == NULL );
-            Pdr_ManSetPropertyOutput( p, k );
-            Pdr_ManCreateSolver( p, ++k );
-            if ( fPrintClauses )
-            {
-                Abc_Print( 1, "*** Clauses after frame %d:\n", k );
-                Pdr_ManPrintClauses( p, 0 );
-            }
-            // push clauses into this timeframe
-            RetValue = Pdr_ManPushClauses( p );
-            if ( RetValue == -1 )
-            {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                if ( !p->pPars->fSilent )
-                    Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
-                p->pPars->iFrame = k;
-                return -1;
-            }
-            if ( RetValue )
-            {
-                if ( p->pPars->fVerbose ) 
-                    Pdr_ManPrintProgress( p, 1, clock() - clkStart );
-                if ( !p->pPars->fSilent )
-                    Pdr_ManReportInvariant( p );
-                if ( !p->pPars->fSilent )
-                    Pdr_ManVerifyInvariant( p );
-                p->pPars->iFrame = k;
-                return 1; // UNSAT
-            }
+            if ( !p->pPars->fSilent )
+                Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
+            p->pPars->iFrame = k;
+            return -1;
+        }
+        if ( RetValue )
+        {
             if ( p->pPars->fVerbose ) 
-                Pdr_ManPrintProgress( p, 0, clock() - clkStart );
-//            clkStart = clock();
+                Pdr_ManPrintProgress( p, 1, clock() - clkStart );
+            if ( !p->pPars->fSilent )
+                Pdr_ManReportInvariant( p );
+            if ( !p->pPars->fSilent )
+                Pdr_ManVerifyInvariant( p );
+            p->pPars->iFrame = k;
+            return 1; // UNSAT
         }
+        if ( p->pPars->fVerbose ) 
+            Pdr_ManPrintProgress( p, 0, clock() - clkStart );
 
         // check termination
         if ( p->pPars->pFuncStop && p->pPars->pFuncStop(p->pPars->RunId) )
@@ -688,72 +735,43 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
   SeeAlso     []
 
 ***********************************************************************/
-int Pdr_ManSolve_( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t ** pvPrioInit, Abc_Cex_t ** ppCex )
+int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
 {
     Pdr_Man_t * p;
     int RetValue;
     clock_t clk = clock();
-    p = Pdr_ManStart( pAig, pPars, pvPrioInit? *pvPrioInit : NULL );
+    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_FREE( pAig->pSeqModel );
+    p = Pdr_ManStart( pAig, pPars, NULL );
     RetValue = Pdr_ManSolveInt( p );
-    if ( ppCex )
-        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+//    if ( ppCex )
+//        *ppCex = RetValue ? NULL : Pdr_ManDeriveCex( p );
+    if ( RetValue == 0 )
+        assert( pAig->pSeqModel != NULL || p->vCexes != NULL );
+    if ( p->vCexes )
+    {
+        assert( p->pAig->vSeqModelVec == NULL );
+        p->pAig->vSeqModelVec = p->vCexes;
+        p->vCexes = NULL;
+    }
     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;
-    if ( pvPrioInit )
-    {
-        *pvPrioInit = p->vPrio;
-        p->vPrio = NULL;
-    }
     Pdr_ManStop( p );
     pPars->iFrame--;
     return RetValue;
 }
 
-/**Function*************************************************************
-
-  Synopsis    []
-
-  Description []
-               
-  SideEffects []
-
-  SeeAlso     []
-
-***********************************************************************/
-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 );
-    if ( pPars->iOutput >= 0 )
-        Abc_Print( 1, "Output = %d. ", pPars->iOutput );
-    Abc_Print( 1, "MonoCNF = %s. SkipGen = %s.\n", 
-        pPars->fMonoCnf ? "yes" : "no", pPars->fSkipGeneral ? "yes" : "no" );
-    }
-
-/*
-    Vec_Int_t * vPrioInit = NULL;
-    int RetValue, nTimeOut;
-    if ( pPars->nTimeOut > 0 )
-        return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
-    nTimeOut = pPars->nTimeOut;
-    pPars->nTimeOut = 10;
-    RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
-    pPars->nTimeOut = nTimeOut;
-    if ( RetValue == -1 )
-        RetValue = Pdr_ManSolve_( pAig, pPars, &vPrioInit, ppCex );
-    Vec_IntFree( vPrioInit );
-    return RetValue;
-*/
-    return Pdr_ManSolve_( pAig, pPars, NULL, ppCex );
-}
-
 ////////////////////////////////////////////////////////////////////////
 ///                       END OF FILE                                ///
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index 36cea069..abc8f12b 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -76,6 +76,8 @@ struct Pdr_Man_t_
     Vec_Int_t** pvId2Vars; // for each used ObjId, maps frame into SAT var
     Vec_Ptr_t * vVar2Ids;  // for each used frame, maps SAT var into ObjId
     // data representation
+    int         iOutCur;   // current output
+    Vec_Ptr_t * vCexes;    // counter-examples for each output
     Vec_Ptr_t * vSolvers;  // SAT solvers
     Vec_Vec_t * vClauses;  // clauses by timeframe
     Pdr_Obl_t * pQueue;    // proof obligations
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 41941a37..78aa2b69 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -144,6 +144,8 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFree( p->vRes      );  // final result
     Vec_IntFree( p->vSuppLits );  // support literals
     ABC_FREE( p->pCubeJust );
+    if ( p->vCexes )
+        Vec_PtrFreeFree( p->vCexes );
     // additional AIG data-members
     if ( p->pAig->pFanData != NULL )
         Aig_ManFanoutStop( p->pAig );
@@ -173,7 +175,8 @@ Abc_Cex_t * Pdr_ManDeriveCex( Pdr_Man_t * p )
         nFrames++;
     // create the counter-example
     pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig), Saig_ManPiNum(p->pAig), nFrames );
-    pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
+//    pCex->iPo    = (p->pPars->iOutput==-1)? 0 : p->pPars->iOutput;
+    pCex->iPo    = p->iOutCur;
     pCex->iFrame = nFrames-1;
     for ( pObl = p->pQueue, f = 0; pObl; pObl = pObl->pNext, f++ )
         for ( i = pObl->pState->nLits; i < pObl->pState->nTotal; i++ )
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index 50402ee5..f0aff8bb 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -45,6 +45,8 @@ ABC_NAMESPACE_IMPL_START
 sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
 {
     sat_solver * pSat;
+    Aig_Obj_t * pObj;
+    int i;
     assert( Vec_PtrSize(p->vSolvers) == k );
     assert( Vec_VecSize(p->vClauses) == k );
     assert( Vec_IntSize(p->vActVars) == k );
@@ -55,7 +57,9 @@ sat_solver * Pdr_ManCreateSolver( Pdr_Man_t * p, int k )
     Vec_VecExpand( p->vClauses, k );
     Vec_IntPush( p->vActVars, 0 );
     // add property cone
-    Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
+//    Pdr_ObjSatVar( p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput ) );
+    Saig_ManForEachPo( p->pAig, pObj, i )
+        Pdr_ObjSatVar( p, k, pObj );
     return pSat;
 }
 
@@ -173,11 +177,15 @@ Vec_Int_t * Pdr_ManCubeToLits( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, int fCom
 void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
 {
     sat_solver * pSat;
-    int Lit, RetValue;
+    Aig_Obj_t * pObj;
+    int Lit, RetValue, i;
     pSat = Pdr_ManSolver(p, k);
-    Lit = toLitCond( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)), 1 ); // neg literal
-    RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
-    assert( RetValue == 1 );
+    Saig_ManForEachPo( p->pAig, pObj, i )
+    {
+        Lit = toLitCond( Pdr_ObjSatVar(p, k, pObj), 1 ); // neg literal
+        RetValue = sat_solver_addclause( pSat, &Lit, &Lit + 1 );
+        assert( RetValue == 1 );
+    }
     sat_solver_compress( pSat );
 }
 
@@ -279,7 +287,7 @@ int Pdr_ManCheckCube( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppPr
     if ( pCube == NULL ) // solve the property
     {
         clk = clock();
-        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) ); // pos literal (property fails)
+        Lit = toLit( Pdr_ObjSatVar(p, k, Aig_ManCo(p->pAig, p->iOutCur)) ); // pos literal (property fails)
         RetValue = sat_solver_solve( pSat, &Lit, &Lit + 1, nConfLimit, 0, 0, 0 );
         if ( RetValue == l_Undef )
             return -1;
diff --git a/src/proof/pdr/pdrTsim.c b/src/proof/pdr/pdrTsim.c
index fa65edea..fcd17fad 100644
--- a/src/proof/pdr/pdrTsim.c
+++ b/src/proof/pdr/pdrTsim.c
@@ -368,7 +368,10 @@ Pdr_Set_t * Pdr_ManTernarySim( Pdr_Man_t * p, int k, Pdr_Set_t * pCube )
     // collect CO objects
     Vec_IntClear( vCoObjs );
     if ( pCube == NULL ) // the target is the property output
-        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
+    {
+//        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, (p->pPars->iOutput==-1)?0:p->pPars->iOutput)) );
+        Vec_IntPush( vCoObjs, Aig_ObjId(Aig_ManCo(p->pAig, p->iOutCur)) );
+    }
     else // the target is the cube
     {
         for ( i = 0; i < pCube->nLits; i++ )