Promising alternative of CEX minimization in 'pdr'.

4 files changed, 57 insertions, 37 deletions

diff --git a/src/base/abci/abc.c b/src/base/abci/abc.c
index 44e4bc16..52684f8c 100644
--- a/src/base/abci/abc.c
+++ b/src/base/abci/abc.c
@@ -26171,7 +26171,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, "MFCDQTHGSaxrmuyfsipdegjonctvwzh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "MFCDQTHGSaxrmuyfsipdegjonctkvwzh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -26328,6 +26328,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 't':
             pPars->fUseAbs ^= 1;
             break;
+        case 'k':
+            pPars->fUseSimpleRef ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -26369,7 +26372,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctvwzh]\n" );
+    Abc_Print( -2, "usage: pdr [-MFCDQTHGS <num>] [-axrmuyfsipdegjonctkvwzh]\n" );
     Abc_Print( -2, "\t         model checking using property directed reachability (aka IC3)\n" );
     Abc_Print( -2, "\t         pioneered by Aaron R. Bradley (http://theory.stanford.edu/~arbrad/)\n" );
     Abc_Print( -2, "\t         with improvements by Niklas Een (http://een.se/niklas/)\n" );
@@ -26400,6 +26403,7 @@ usage:
     Abc_Print( -2, "\t-n     : * toggle skipping \'down\' in generalization [default = %s]\n",                 pPars->fSkipDown? "yes": "no" );
     Abc_Print( -2, "\t-c     : * toggle handling CTGs in \'down\' [default = %s]\n",                           pPars->fCtgs? "yes": "no" );
     Abc_Print( -2, "\t-t     : toggle using abstraction [default = %s]\n",                                   pPars->fUseAbs? "yes": "no" );
+    Abc_Print( -2, "\t-k     : toggle using simplified refinement [default = %s]\n",                         pPars->fUseSimpleRef? "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 534e8e4b..51b04606 100644
--- a/src/proof/pdr/pdr.h
+++ b/src/proof/pdr/pdr.h
@@ -65,6 +65,7 @@ struct Pdr_Par_t_
     int fSkipDown;        // skips the application of down
     int fCtgs;            // handle CTGs in down
     int fUseAbs;          // use abstraction 
+    int fUseSimpleRef;    // simplified CEX refinement
     int fVerbose;         // verbose output`
     int fVeryVerbose;     // very verbose output
     int fNotVerbose;      // not printing line by line progress
diff --git a/src/proof/pdr/pdrCore.c b/src/proof/pdr/pdrCore.c
index 40e86727..efb4154f 100644
--- a/src/proof/pdr/pdrCore.c
+++ b/src/proof/pdr/pdrCore.c
@@ -60,8 +60,6 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->nRestLimit     =       0;  // limit on the number of proof-obligations
     pPars->nRandomSeed   = 91648253;  // value to seed the SAT solver with
     pPars->fTwoRounds     =       0;  // use two rounds for generalization
-    pPars->fSkipDown      =       1;  // apply down in generalization
-    pPars->fCtgs          =       0;  // handle CTGs in down
     pPars->fMonoCnf       =       0;  // monolythic CNF
     pPars->fNewXSim       =       0;  // updated X-valued simulation
     pPars->fFlopPrio      =       0;  // use structural flop priorities
@@ -70,6 +68,10 @@ void Pdr_ManSetDefaultParams( Pdr_Par_t * pPars )
     pPars->fUseSupp       =       1;  // using support variables in the invariant
     pPars->fShortest      =       0;  // forces bug traces to be shortest
     pPars->fUsePropOut    =       1;  // use property output
+    pPars->fSkipDown      =       1;  // apply down in generalization
+    pPars->fCtgs          =       0;  // handle CTGs in down
+    pPars->fUseAbs        =       0;  // use abstraction 
+    pPars->fUseSimpleRef  =       0;  // simplified CEX refinement
     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/pdrMan.c b/src/proof/pdr/pdrMan.c
index abe8c0a8..a076223b 100644
--- a/src/proof/pdr/pdrMan.c
+++ b/src/proof/pdr/pdrMan.c
@@ -482,45 +482,58 @@ Abc_Cex_t * Pdr_ManDeriveCexAbs( Pdr_Man_t * p )
     }
     if ( Vec_IntSize(p->vMapPpi2Ff) == 0 ) // no PPIs -- this is a real CEX
         return Pdr_ManDeriveCex(p);
-    // create the counter-example
-    pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
-    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++ )
+    if ( p->pPars->fUseSimpleRef )
+    {
+        // rely on ternary simulation to perform refinement
+        Vec_IntForEachEntry( p->vMapPpi2Ff, Flop, i )
         {
-            Lit = pObl->pState->Lits[i];
-            if ( lit_sign(Lit) )
-                continue;
-            if ( lit_var(Lit) < nPis ) // PI literal
-                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
-            else
-            {
-                int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
-                assert( iPPI < pCex->nPis );
-                Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
-            }
+            assert( Vec_IntEntry(p->vAbsFlops, Flop) == 0 );
+            Vec_IntWriteEntry( p->vAbsFlops, Flop, 1 );
+            nFfRefined++;
         }
-    assert( f == nFrames );
-    // perform CEX minimization
-    pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
-    pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
-    Gia_ManStop( pAbs );
-    assert( pCexCare->nPis == pCex->nPis );
-    Abc_CexFree( pCex );
-    // detect care PPIs
-    for ( f = 0; f < nFrames; f++ )
+    }
+    else
     {
-        for ( i = nPis; i < pCexCare->nPis; i++ )
-            if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+        // create the counter-example
+        pCex = Abc_CexAlloc( Aig_ManRegNum(p->pAig) - Vec_IntSize(p->vMapPpi2Ff), Saig_ManPiNum(p->pAig) + Vec_IntSize(p->vMapPpi2Ff), nFrames );
+        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++ )
             {
-                if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
-                    Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
+                Lit = pObl->pState->Lits[i];
+                if ( lit_sign(Lit) )
+                    continue;
+                if ( lit_var(Lit) < nPis ) // PI literal
+                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + lit_var(Lit) );
+                else
+                {
+                    int iPPI = nPis + Vec_IntEntry(p->vMapFf2Ppi, lit_var(Lit) - nPis);
+                    assert( iPPI < pCex->nPis );
+                    Abc_InfoSetBit( pCex->pData, pCex->nRegs + f * pCex->nPis + iPPI );
+                }
             }
+        assert( f == nFrames );
+        // perform CEX minimization
+        pAbs = Gia_ManDupAbs( p->pGia, p->vMapPpi2Ff, p->vMapFf2Ppi );
+        pCexCare = Bmc_CexCareMinimizeAig( pAbs, nPis, pCex, 1, 0, 0 );
+        Gia_ManStop( pAbs );
+        assert( pCexCare->nPis == pCex->nPis );
+        Abc_CexFree( pCex );
+        // detect care PPIs
+        for ( f = 0; f < nFrames; f++ )
+        {
+            for ( i = nPis; i < pCexCare->nPis; i++ )
+                if ( Abc_InfoHasBit(pCexCare->pData, pCexCare->nRegs + pCexCare->nPis * f + i) )
+                {
+                    if ( Vec_IntEntry(p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis)) == 0 ) // currently abstracted
+                        Vec_IntWriteEntry( p->vAbsFlops, Vec_IntEntry(p->vMapPpi2Ff, i-nPis), 1 ), nFfRefined++;
+                }
+        }
+        Abc_CexFree( pCexCare );
+        if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
+            return Pdr_ManDeriveCex(p);
     }
-    Abc_CexFree( pCexCare );
-    if ( nFfRefined == 0 ) // no refinement -- this is a real CEX
-        return Pdr_ManDeriveCex(p);
     //printf( "CEX-based refinement refined %d flops.\n", nFfRefined );
     p->nCexesTotal++;
     p->nCexes++;