Adding switch 'pdr -o' to control using property output in induction.

4 files changed, 10 insertions, 2 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index c17f5599..aa2d5598 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -25204,7 +25204,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, "MFCDRTHGaxrmsipdgvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDRTHGaxrmsipdgovwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -25323,6 +25323,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'g':
             pPars->fSkipGeneral ^= 1;
             break;
+        case 'o':
+            pPars->fUsePropOut ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -25364,7 +25367,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdgvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDRTHG <num>] [-axrmsipdgovwzh]\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" );
@@ -25385,6 +25388,7 @@ usage:
     Abc_Print( -2, "\t-p     : toggle reusing proof-obligations in the last timeframe [default = %s]\n",     pPars->fReuseProofOblig? "yes": "no" );
     Abc_Print( -2, "\t-d     : toggle dumping invariant (valid if init state is all-0) [default = %s]\n",    pPars->fDumpInv? "yes": "no" );
     Abc_Print( -2, "\t-g     : toggle skipping expensive generalization step [default = %s]\n",              pPars->fSkipGeneral? "yes": "no" );
+    Abc_Print( -2, "\t-o     : toggle using property output as inductive hypothesis [default = %s]\n",       pPars->fUsePropOut? "yes": "no" );
     Abc_Print( -2, "\t-v     : toggle printing optimization summary [default = %s]\n",                       pPars->fVerbose? "yes": "no" );
     Abc_Print( -2, "\t-w     : toggle printing detailed stats default = %s]\n",                              pPars->fVeryVerbose? "yes": "no" );
     Abc_Print( -2, "\t-z     : toggle suppressing report about solved outputs [default = %s]\n",             pPars->fNotVerbose? "yes": "no" );
diff --git a/src/proof/pdr/pdr.h b/src/proof/pdr/pdr.h
index e4b764a1..3dffac17 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -63,6 +63,7 @@ struct Pdr_Par_t_
     int fSolveAll;        // do not stop when found a SAT output
     int fStoreCex;        // enable storing counter-examples in MO mode
     int fUseBridge;       // use bridge interface
+    int fUsePropOut;      // use property output
     int nFailOuts;        // the number of failed outputs
     int nDropOuts;        // the number of timed out outputs
     int nProveOuts;       // the number of proved outputs
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 8e81795b..5b619f4b 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -61,6 +61,7 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fMonoCnf       =       0;  // monolythic CNF
     pPars->fDumpInv       =       0;  // dump inductive invariant
     pPars->fShortest      =       0;  // forces bug traces to be shortest
+    pPars->fUsePropOut    =       1;  // use property output
     pPars->fVerbose       =       0;  // verbose output
     pPars->fVeryVerbose   =       0;  // very verbose output
     pPars->fNotVerbose    =       0;  // not printing line-by-line progress
diff --git a/src/proof/pdr/pdrSat.c b/src/proof/pdr/pdrSat.c
index f3681adb..2e6130aa 100644
--- a/src/proof/pdr/pdrSat.c
+++ b/src/proof/pdr/pdrSat.c
@@ -179,6 +179,8 @@ void Pdr_ManSetPropertyOutput( Pdr_Man_t * p, int k )
     sat_solver * pSat;
     Aig_Obj_t * pObj;
     int Lit, RetValue, i;
+    if ( !p->pPars->fUsePropOut )
+        return;
     pSat = Pdr_ManSolver(p, k);
     Saig_ManForEachPo( p->pAig, pObj, i )
     {