Added switch to PDR to disable expensive generalization step.

src/base/abci/abc.c

@@ -20213,7 +20213,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, "OMFCTrmsdvwh" ) ) != EOF )
+    while ( ( c = Extra_UtilGetopt( argc, argv, "OMFCTrmsdgvwh" ) ) != EOF )
     {
         switch ( c )
         {
@@ -20284,6 +20284,9 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
         case 'd':
             pPars->fDumpInv ^= 1;
             break;
+        case 'g':
+            pPars->fSkipGeneral ^= 1;
+            break;
         case 'v':
             pPars->fVerbose ^= 1;
             break;
@@ -20331,7 +20334,7 @@ int Abc_CommandPdr( Abc_Frame_t * pAbc, int argc, char ** argv )
     return 0;
 
 usage:
-    Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdvwh]\n" );
+    Abc_Print( -2, "usage: pdr [-OMFCT<num] [-rmsdgvwh]\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" );
@@ -20344,6 +20347,7 @@ usage:
     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" );
     Abc_Print( -2, "\t-d     : toggle dumping inductive invariant [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-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-h     : print the command usage\n");

src/sat/pdr/pdr.h

@@ -49,6 +49,7 @@ struct Pdr_Par_t_
     int fMonoCnf;     // monolythic CNF
     int fDumpInv;     // dump inductive invariant
     int fShortest;    // forces bug traces to be shortest
+    int fSkipGeneral; // skips expensive generalization step
     int fVerbose;     // verbose output
     int fVeryVerbose; // very verbose output
     int iFrame;       // explored up to this frame

src/sat/pdr/pdrCore.c

@@ -302,89 +302,93 @@ int Pdr_ManGeneralize( Pdr_Man_t * p, int k, Pdr_Set_t * pCube, Pdr_Set_t ** ppP
         p->tGeneral += clock() - clk;
         return 0;
     }
+
     // reduce clause using assumptions
 //    pCubeMin = Pdr_SetDup( pCube );
     pCubeMin = Pdr_ManReduceClause( p, k, pCube );
     if ( pCubeMin == NULL )
         pCubeMin = Pdr_SetDup( pCube );
 
-    // sort literals by their occurences
-    pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-
-    // try removing literals
-    for ( j = 0; j < pCubeMin->nLits; j++ )
+    // perform generalization
+    if ( !p->pPars->fSkipGeneral )
     {
-        // use ordering
-//        i = j;
-        i = pOrder[j];
-
-        // check init state
-        assert( pCubeMin->Lits[i] != -1 );
-        if ( Pdr_SetIsInit(pCubeMin, i) )
-            continue;
-        // try removing this literal
-        Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-        RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
+        // sort literals by their occurences
+        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        // try removing literals
+        for ( j = 0; j < pCubeMin->nLits; j++ )
         {
-            Pdr_SetDeref( pCubeMin );
-            return -1;
-        }
-        pCubeMin->Lits[i] = Lit;
-        if ( RetValue == 0 )
-            continue;
+            // use ordering
+    //        i = j;
+            i = pOrder[j];
 
-        // remove j-th entry
-        for ( n = j; n < pCubeMin->nLits-1; n++ )
-            pOrder[n] = pOrder[n+1];
-        j--;
+            // check init state
+            assert( pCubeMin->Lits[i] != -1 );
+            if ( Pdr_SetIsInit(pCubeMin, i) )
+                continue;
+            // try removing this literal
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            if ( RetValue == -1 )
+            {
+                Pdr_SetDeref( pCubeMin );
+                return -1;
+            }
+            pCubeMin->Lits[i] = Lit;
+            if ( RetValue == 0 )
+                continue;
 
-        // success - update the cube
-        pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-        Pdr_SetDeref( pCubeTmp );
-        assert( pCubeMin->nLits > 0 );
-        i--;
+            // remove j-th entry
+            for ( n = j; n < pCubeMin->nLits-1; n++ )
+                pOrder[n] = pOrder[n+1];
+            j--;
 
-        // get the ordering by decreasing priorit
-        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
-    }
+            // success - update the cube
+            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+            Pdr_SetDeref( pCubeTmp );
+            assert( pCubeMin->nLits > 0 );
+            i--;
 
-    if ( p->pPars->fTwoRounds )
-    for ( j = 0; j < pCubeMin->nLits; j++ )
-    {
-        // use ordering
-//        i = j;
-        i = pOrder[j];
+            // get the ordering by decreasing priorit
+            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        }
 
-        // check init state
-        assert( pCubeMin->Lits[i] != -1 );
-        if ( Pdr_SetIsInit(pCubeMin, i) )
-            continue;
-        // try removing this literal
-        Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
-        RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
-        if ( RetValue == -1 )
+        if ( p->pPars->fTwoRounds )
+        for ( j = 0; j < pCubeMin->nLits; j++ )
         {
-            Pdr_SetDeref( pCubeMin );
-            return -1;
-        }
-        pCubeMin->Lits[i] = Lit;
-        if ( RetValue == 0 )
-            continue;
+            // use ordering
+    //        i = j;
+            i = pOrder[j];
 
-        // remove j-th entry
-        for ( n = j; n < pCubeMin->nLits-1; n++ )
-            pOrder[n] = pOrder[n+1];
-        j--;
+            // check init state
+            assert( pCubeMin->Lits[i] != -1 );
+            if ( Pdr_SetIsInit(pCubeMin, i) )
+                continue;
+            // try removing this literal
+            Lit = pCubeMin->Lits[i]; pCubeMin->Lits[i] = -1; 
+            RetValue = Pdr_ManCheckCube( p, k, pCubeMin, NULL, p->pPars->nConfLimit );
+            if ( RetValue == -1 )
+            {
+                Pdr_SetDeref( pCubeMin );
+                return -1;
+            }
+            pCubeMin->Lits[i] = Lit;
+            if ( RetValue == 0 )
+                continue;
 
-        // success - update the cube
-        pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
-        Pdr_SetDeref( pCubeTmp );
-        assert( pCubeMin->nLits > 0 );
-        i--;
+            // remove j-th entry
+            for ( n = j; n < pCubeMin->nLits-1; n++ )
+                pOrder[n] = pOrder[n+1];
+            j--;
 
-        // get the ordering by decreasing priorit
-        pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+            // success - update the cube
+            pCubeMin = Pdr_SetCreateFrom( pCubeTmp = pCubeMin, i );
+            Pdr_SetDeref( pCubeTmp );
+            assert( pCubeMin->nLits > 0 );
+            i--;
+
+            // get the ordering by decreasing priorit
+            pOrder = Pdr_ManSortByPriority( p, pCubeMin );
+        }
     }
 
     assert( ppCubeMin != NULL );