Adding runtime limit per output to multi-output DPR (pdr -H <num_sec>).

8 files changed, 117 insertions, 22 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 90d6b454..c19faa52 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -22641,7 +22641,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     int c;
     Pdr_ManSetDefaultParams( pPars );
     Extra_UtilGetoptReset();
-    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGaxrmsdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCRTGHaxrmsdgvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -22711,6 +22711,17 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
             if ( pPars->nTimeOutGap < 0 )
                 goto usage;
             break;
+        case 'H':
+            if ( globalUtilOptind >= argc )
+            {
+                Abc_Print( -1, "Command line switch \"-H\" should be followed by an integer.\n" );
+                goto usage;
+            }
+            pPars->nTimeOutOne = atoi(argv[globalUtilOptind]);
+            globalUtilOptind++;
+            if ( pPars->nTimeOutOne < 0 )
+                goto usage;
+            break;
         case 'a':
             pPars->fSolveAll ^= 1;
             break;
@@ -22773,7 +22784,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCRTG <num>] [-axrmsdgvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCRTGH <num>] [-axrmsdgvwzh]\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" );
@@ -22783,6 +22794,7 @@ usage:
     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-G num : approximate runtime gap since the last CEX (0 = no limit) [default = %d]\n",  pPars->nTimeOutGap );
+    Abc_Print( -2, "\t-H num : approximate runtime per output (with \"-a\") [default = %d]\n",               pPars->nTimeOutOne );
     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-x     : toggle storing CEXes when solving all outputs [default = %s]\n",              pPars->fStoreCex? "yes": "no" );
     Abc_Print( -2, "\t-r     : toggle using more effort in generalization [default = %s]\n",                 pPars->fTwoRounds? "yes": "no" );
diff --git a/src/base/abci/abcDar.c b/src/base/abci/abcDar.c
index abf08599..c351df45 100644
--- a/src/base/abci/abcDar.c
+++ b/src/base/abci/abcDar.c
@@ -2176,8 +2176,12 @@ int Abc_NtkDarBmc3( Abc_Ntk_t * pNtk, Saig_ParBmc_t * pPars, int fOrDecomp )
             else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
                 Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
             else
-                Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT.   ", 
-                    nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+            {
+                Abc_Print( 1, "Some outputs are SAT (%d out of %d)", nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
+                if ( pPars->nDropOuts )
+                    Abc_Print( 1, " while others timed out (%d out of %d)", pPars->nDropOuts, nOutputs );
+                Abc_Print( 1, ".   " );
+            }
             if ( pNtk->vSeqModelVec )
                 Vec_PtrFreeFree( pNtk->vSeqModelVec );
             pNtk->vSeqModelVec = pMan->vSeqModelVec;  pMan->vSeqModelVec = NULL;
@@ -2743,22 +2747,15 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
         return -1;
     }
     RetValue = Pdr_ManSolve( pMan, pPars );
+    pPars->nDropOuts = Saig_ManPoNum(pMan) - pPars->nProveOuts - pPars->nFailOuts;
     if ( !pPars->fSilent )
     {
-        if ( RetValue == 1 )
+        if ( pPars->fSolveAll )
+            Abc_Print( 1, "Properties:  All = %d. Proved = %d. Disproved = %d. Undecided = %d.   ", 
+                Saig_ManPoNum(pMan), pPars->nProveOuts, pPars->nFailOuts, pPars->nDropOuts );
+        else 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 )
-                Abc_Print( 1, "None of the %d outputs is found to be SAT.   ", nOutputs );
-            else if ( Vec_PtrCountZero(pMan->vSeqModelVec) == 0 )
-                Abc_Print( 1, "All %d outputs are found to be SAT.   ", nOutputs );
-            else
-                Abc_Print( 1, "Some outputs (%d out of %d) are found to be SAT.   ", 
-                    nOutputs - Vec_PtrCountZero(pMan->vSeqModelVec), nOutputs );
-        }
-        else
+        else 
         {
             if ( RetValue == 0 )
             {
@@ -2777,6 +2774,22 @@ int Abc_NtkDarPdr( Abc_Ntk_t * pNtk, Pdr_Par_t * pPars )
                 assert( 0 );
         }
         ABC_PRT( "Time", clock() - clk );
+/*
+        Abc_Print( 1, "Status: " );
+        if ( pPars->pOutMap )
+        {
+            int i;
+            for ( i = 0; i < Saig_ManPoNum(pMan); i++ )
+                if ( pPars->pOutMap[i] == 1 )
+                    Abc_Print( 1, "%d=%s ", i, "unsat" );
+                else if ( pPars->pOutMap[i] == 0 )
+                    Abc_Print( 1, "%d=%s ", i, "sat" );
+                else if ( pPars->pOutMap[i] < 0 )
+                    Abc_Print( 1, "%d=%s ", i, "undec" );
+                else assert( 0 );
+        }
+        Abc_Print( 1, "\n" );
+*/
     }
     ABC_FREE( pNtk->pSeqModel );
     pNtk->pSeqModel = pMan->pSeqModel;
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index cfb13356..97a71512 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -47,6 +47,7 @@ struct Pdr_Par_t_
     int nRestLimit;       // limit on the number of proof-obligations
     int nTimeOut;         // timeout in seconds
     int nTimeOutGap;      // approximate timeout in seconds since the last change
+    int nTimeOutOne;      // approximate timeout in seconds per one output
     int fTwoRounds;       // use two rounds for generalization
     int fMonoCnf;         // monolythic CNF
     int fDumpInv;         // dump inductive invariant
@@ -59,11 +60,14 @@ struct Pdr_Par_t_
     int fSolveAll;        // do not stop when found a SAT output
     int fStoreCex;        // enable storing counter-examples in MO mode
     int nFailOuts;        // the number of failed outputs
+    int nDropOuts;        // the number of timed out outputs
+    int nProveOuts;       // the number of proved outputs
     int iFrame;           // explored up to this frame
     int RunId;            // PDR id in this run 
     int(*pFuncStop)(int); // callback to terminate
     int(*pFuncOnFail)(int,Abc_Cex_t*); // called for a failed output in MO mode
     clock_t timeLastSolved; // the time when the last output was solved
+    int * pOutMap;        // in the multi-output mode, contains status for each PO (0 = sat; 1 = unsat; negative = undecided)
 };
 
 ////////////////////////////////////////////////////////////////////////
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 3df1d7de..43cc4527 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -60,6 +60,8 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fVeryVerbose   =       0;  // very verbose output
     pPars->fNotVerbose    =       0;  // not printing line-by-line progress
     pPars->iFrame         =      -1;  // explored up to this frame
+    pPars->nFailOuts      =       0;  // the number of disproved outputs
+    pPars->nDropOuts      =       0;  // the number of timed out outputs
     pPars->timeLastSolved =       0;  // last one solved
 }
 
@@ -536,6 +538,8 @@ int Pdr_ManBlockCube( Pdr_Man_t * p, Pdr_Set_t * pCube )
             return -1;
         if ( p->timeToStop && clock() > p->timeToStop )
             return -1;
+        if ( p->timeToStopOne && clock() > p->timeToStopOne )
+            return -1;
     }
     return 1;
 }
@@ -558,7 +562,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
     Aig_Obj_t * pObj;
     int k, RetValue = -1;
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(p->pAig) );
-    clock_t clkStart = clock();
+    clock_t clkStart = clock(), clkOne = 0;
     p->timeToStop = p->pPars->nTimeOut ? p->pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     assert( Vec_PtrSize(p->vSolvers) == 0 );
     // create the first timeframe
@@ -570,9 +574,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
         assert( k == Vec_PtrSize(p->vSolvers)-1 );
         Saig_ManForEachPo( p->pAig, pObj, p->iOutCur )
         {
-            // skip solved outputs
+            // skip disproved outputs
             if ( p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) )
                 continue;
+            // skip output whose time has run out
+            if ( p->pTime4Outs && p->pTime4Outs[p->iOutCur] == 0 )
+                continue;
             // check if the output is trivially solved
             if ( Aig_ObjChild0(pObj) == Aig_ManConst0(p->pAig) )
                 continue;
@@ -585,6 +592,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     return 0; // SAT
                 }
                 p->pPars->nFailOuts++;
+                if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
                 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 )
@@ -600,12 +608,18 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                     p->pPars->iFrame = k;
                     return -1;
                 }
-                if ( p->pPars->nFailOuts == Saig_ManPoNum(p->pAig) )
-                    return 0; // all SAT
+                if ( p->pPars->nFailOuts + p->pPars->nDropOuts == Saig_ManPoNum(p->pAig) )
+                    return p->pPars->nFailOuts ? 0 : -1; // SAT or UNDEC
                 p->pPars->timeLastSolved = clock();
                 continue;
             } 
             // try to solve this output
+            if ( p->pTime4Outs )
+            {
+                assert( p->pTime4Outs[p->iOutCur] > 0 );
+                clkOne = clock();
+                p->timeToStopOne = p->pTime4Outs[p->iOutCur] + clock();
+            }
             while ( 1 )
             {
                 if ( p->pPars->nTimeOutGap && p->pPars->timeLastSolved && clock() > p->pPars->timeLastSolved + p->pPars->nTimeOutGap * CLOCKS_PER_SEC )
@@ -642,6 +656,12 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             Abc_Print( 1, "Reached conflict limit (%d).\n",  p->pPars->nConfLimit );
                         else if ( p->timeToStop && clock() > p->timeToStop )
                             Abc_Print( 1, "Reached timeout (%d seconds).\n",  p->pPars->nTimeOut );
+                        else if ( p->timeToStopOne && clock() > p->timeToStopOne )
+                        {
+                            Pdr_QueueClean( p );
+                            pCube = NULL;
+                            break; // keep solving
+                        }
                         else if ( p->pPars->fVerbose ) 
                             Abc_Print( 1, "Computation cancelled by the callback.\n" );
                         p->pPars->iFrame = k;
@@ -664,6 +684,7 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                             return 0; // SAT
                         }
                         p->pPars->nFailOuts++;
+                        if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = 0;
                         if ( p->vCexes == NULL )
                             p->vCexes = Vec_PtrStart( Saig_ManPoNum(p->pAig) );
                         assert( Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL );
@@ -690,6 +711,18 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
                         Pdr_ManPrintProgress( p, 0, clock() - clkStart );
                 }
             } 
+            if ( p->pTime4Outs )
+            {
+                clock_t timeSince = clock() - clkOne;
+                assert( p->pTime4Outs[p->iOutCur] > 0 );
+                p->pTime4Outs[p->iOutCur] = (p->pTime4Outs[p->iOutCur] > timeSince) ? p->pTime4Outs[p->iOutCur] - timeSince : 0;
+                if ( p->pTime4Outs[p->iOutCur] == 0 && p->vCexes && Vec_PtrEntry(p->vCexes, p->iOutCur) == NULL )
+                {
+                    p->pPars->nDropOuts++;
+                    if ( p->pPars->pOutMap ) p->pPars->pOutMap[p->iOutCur] = -1;
+//                    printf( "Dropping output %d.\n", p->iOutCur );
+                }
+            }
         }
 
         if ( p->pPars->fVerbose ) 
@@ -729,6 +762,13 @@ int Pdr_ManSolveInt( Pdr_Man_t * p )
             if ( !p->pPars->fSilent )
                 Pdr_ManVerifyInvariant( p );
             p->pPars->iFrame = k;
+            // count the number of UNSAT outputs
+            p->pPars->nProveOuts = Saig_ManPoNum(p->pAig) - p->pPars->nFailOuts - p->pPars->nDropOuts;
+            // convert previously 'unknown' into 'unsat'
+            if ( p->pPars->pOutMap )
+                for ( k = 0; k < Saig_ManPoNum(p->pAig); k++ )
+                    if ( p->pPars->pOutMap[k] == -2 ) // unknown
+                        p->pPars->pOutMap[k] = 1; // unsat
             return p->vCexes ? 0 : 1; // UNSAT
         }
         if ( p->pPars->fVerbose ) 
@@ -798,6 +838,10 @@ int Pdr_ManSolve( Aig_Man_t * pAig, Pdr_Par_t * pPars )
     Pdr_Man_t * p;
     int RetValue;
     clock_t clk = clock();
+    if ( pPars->nTimeOutOne )
+        pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
+    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
+        pPars->nTimeOutOne = 0;
     if ( pPars->fVerbose )
     {
 //    Abc_Print( 1, "Running PDR by Niklas Een (aka IC3 by Aaron Bradley) with these parameters:\n" );
diff --git a/src/proof/pdr/pdrInt.h b/src/proof/pdr/pdrInt.h
index f6d3d170..03d522d3 100644
--- a/src/proof/pdr/pdrInt.h
+++ b/src/proof/pdr/pdrInt.h
@@ -97,6 +97,7 @@ struct Pdr_Man_t_
     Vec_Int_t * vRes;      // final result
     Vec_Int_t * vSuppLits; // support literals
     Pdr_Set_t * pCubeJust; // justification
+    clock_t *   pTime4Outs;// timeout per output
     // statistics
     int         nBlocks;   // the number of times blockState was called
     int         nObligs;   // the number of proof obligations derived
@@ -115,6 +116,7 @@ struct Pdr_Man_t_
     int         nQueLim;
     // runtime
     time_t      timeToStop;
+    time_t      timeToStopOne;
     // time stats
     clock_t     tSat;
     clock_t     tSatSat;
diff --git a/src/proof/pdr/pdrInv.c b/src/proof/pdr/pdrInv.c
index ee87f262..bb8d110d 100644
--- a/src/proof/pdr/pdrInv.c
+++ b/src/proof/pdr/pdrInv.c
@@ -83,6 +83,8 @@ void Pdr_ManPrintProgress( Pdr_Man_t * p, int fClose, clock_t Time )
     Abc_Print( 1, "%10.2f sec", 1.0*Time/CLOCKS_PER_SEC );
     if ( p->pPars->fSolveAll )
         Abc_Print( 1, "  CEX =%4d", p->pPars->nFailOuts );
+    if ( p->pPars->nTimeOutOne )
+        Abc_Print( 1, "  T/O =%3d", p->pPars->nDropOuts );
     Abc_Print( 1, "%s", fClose ? "\n":"\r" );
     if ( fClose )
         p->nQueMax = 0;
diff --git a/src/proof/pdr/pdrMan.c b/src/proof/pdr/pdrMan.c
index 95e7641b..51be5e17 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -73,6 +73,21 @@ Pdr_Man_t * Pdr_ManStart( Aig_Man_t * pAig, Pdr_Par_t * pPars, Vec_Int_t * vPrio
         Aig_ManFanoutStart( pAig );
     if ( pAig->pTerSimData == NULL )
         pAig->pTerSimData = ABC_CALLOC( unsigned, 1 + (Aig_ManObjNumMax(pAig) / 16) );
+    // time spent on each outputs
+    if ( pPars->nTimeOutOne )
+    {
+        int i;
+        p->pTime4Outs = ABC_ALLOC( clock_t, Saig_ManPoNum(pAig) );
+        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
+            p->pTime4Outs[i] = pPars->nTimeOutOne * CLOCKS_PER_SEC;
+    }
+    if ( pPars->fSolveAll )
+    {
+        int i;
+        pPars->pOutMap = ABC_ALLOC( int, Saig_ManPoNum(pAig) );
+        for ( i = 0; i < Saig_ManPoNum(pAig); i++ )
+            pPars->pOutMap[i] = -2; // unknown
+    }
     return p;
 }
 
@@ -144,6 +159,7 @@ void Pdr_ManStop( Pdr_Man_t * p )
     Vec_IntFree( p->vRes      );  // final result
     Vec_IntFree( p->vSuppLits );  // support literals
     ABC_FREE( p->pCubeJust );
+    ABC_FREE( p->pTime4Outs );
     if ( p->vCexes )
         Vec_PtrFreeFree( p->vCexes );
     // additional AIG data-members
diff --git a/src/sat/bmc/bmcBmc3.c b/src/sat/bmc/bmcBmc3.c
index 96fff2af..424e08c9 100644
--- a/src/sat/bmc/bmcBmc3.c
+++ b/src/sat/bmc/bmcBmc3.c
@@ -1393,10 +1393,12 @@ int Saig_ManBmcScalable( Aig_Man_t * pAig, Saig_ParBmc_t * pPars )
     int nOutDigits = Abc_Base10Log( Saig_ManPoNum(pAig) );
     int i, f, k, Lit, status;
     clock_t clk, clk2, clkOther = 0, clkTotal = clock();
-    clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne;
+    clock_t nTimeUnsat = 0, nTimeSat = 0, nTimeUndec = 0, clkOne = 0;
     clock_t nTimeToStopNG, nTimeToStop;
     if ( pPars->nTimeOutOne )
         pPars->nTimeOut = pPars->nTimeOutOne * Saig_ManPoNum(pAig);
+    if ( pPars->nTimeOutOne && !pPars->fSolveAll )
+        pPars->nTimeOutOne = 0;
     nTimeToStopNG = pPars->nTimeOut ? pPars->nTimeOut * CLOCKS_PER_SEC + clock(): 0;
     nTimeToStop   = Saig_ManBmcTimeToStop( pPars, nTimeToStopNG );
     // create BMC manager