Enabling multi-output solving in 'pdr'.

src/base/abci/abc.c

@@ -22321,10 +22321,11 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCRTrmsdgvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTarmsdgvwh" ) ) != EOF )
     {
         switch ( c )
         {
+/*
         case 'O':
             if ( globalUtilOptind >= argc )
             {
@@ -22336,6 +22337,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->iOutput < 0 )
                 goto usage;
             break;
+*/
         case 'M':
             if ( globalUtilOptind >= argc )
             {
@@ -22391,6 +22393,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOut < 0 )
                 goto usage;
             break;
+        case 'a':
+            pPars->fSolveAll ^= 1;
+            break;
         case 'r':
             pPars->fTwoRounds ^= 1;
             break;
@@ -22432,12 +22437,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 )
@@ -22446,6 +22454,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             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->nFrames = pPars->iFrame;
@@ -22453,16 +22462,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-OMFCRT<num] [-rmsdgvwh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCRT<num] [-armsdgvwh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron Bradley (http://ecee.colorado.edu/~bradleya/ic3/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
-    Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" );
+//    Abc_Print( -2, "\t-O num : the zero-based number of the primary output to solve [default = all]\n" );
     Abc_Print( -2, "\t-M num : limit on unused vars to trigger SAT solver recycling [default = %d]\n", pPars->nRecycle );
     Abc_Print( -2, "\t-F num : limit on timeframes explored to stop computation [default = %d]\n", pPars->nFrameMax );
     Abc_Print( -2, "\t-C num : limit on conflicts in one SAT call (0 = no limit) [default = %d]\n", pPars->nConfLimit );
     Abc_Print( -2, "\t-R num : limit on proof obligations before a restart (0 = no limit) [default = %d]\n", pPars->nRestLimit );
     Abc_Print( -2, "\t-T num : approximate timeout in seconds (0 = no limit) [default = %d]\n", pPars->nTimeOut );
+    Abc_Print( -2, "\t-a     : toggle solving all outputs even if one of them is SAT [default = %s]\n", pPars->fSolveAll? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n", pPars->fTwoRounds? "yes": "no" );
     Abc_Print( -2, "\t-m     : toggle using monolythic CNF computation [default = %s]\n", pPars->fMonoCnf? "yes": "no" );
     Abc_Print( -2, "\t-s     : toggle creating only shortest counter-examples [default = %s]\n", pPars->fShortest? "yes": "no" );

src/base/abci/abcDar.c

@@ -2717,6 +2717,7 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
         Abc_Print( 1, "Converting network into AIG has failed.\n" );
         return -1;
     }
+/*
     // perform ORing the primary outputs
     if ( pPars->iOutput == -1 )
     {
@@ -2728,6 +2729,9 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars, Abc_Cex_t ** ppCex )
     }
     else
         RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
+*/
+    RetValue = Pdr_ManSolve( pMan, pPars, ppCex );
+
     // output the result
     if ( !pPars->fSilent )
     {

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

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,7 +564,39 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     {
         p->nFrames = k;
         assert( k == Vec_PtrSize(p->vSolvers)-1 );
+        Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
+        {
+            // 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->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;
+            }
+            // try to solve this output
+            while ( 1 )
+            {
                 RetValue = Pdr_ManCheckCube( p, k, NULL, &pCube, p->pPars->nConfLimit );
+                if ( RetValue == 1 )
+                    break;
                 if ( RetValue == -1 )
                 {
                     if ( p->pPars->fVerbose ) 
@@ -598,13 +632,28 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         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
@@ -641,8 +690,6 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         }
         if ( p->pPars->fVerbose ) 
             Pdr_ManPrintProgress( p, 0, clock() - clkStart );
-//            clkStart = clock();
-        }
 
         // 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                                ///
 ////////////////////////////////////////////////////////////////////////

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

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++ )

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
+    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;

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++ )