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

2 files changed, 42 insertions, 17 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;